[STATEMENT]
lemma S_diff_T_diff: "S x - S (x / 2) \<le> T x - 2 * T (x / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
note fin = fin[of _ x]
[PROOF STATE]
proof (state)
this:
?X \<subseteq> {n. real n \<le> x} \<Longrightarrow> finite ?X

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have T_diff_eq:
    "T x - 2 * T (x / 2) = sum_upto (\<lambda>n. a n * (\<lfloor>x / n\<rfloor> - 2 * \<lfloor>x / (2 * n)\<rfloor>)) (x / 2) +
        (\<Sum>n | n > 0 \<and> real n \<in> {x/2<..x}. a n * \<lfloor>x / n\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T x - 2 * T (x / 2) = sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)
[PROOF STEP]
unfolding T_def dirichlet_prod'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>m. a m * real_of_int \<lfloor>x / real m\<rfloor>) x - 2 * sum_upto (\<lambda>m. a m * real_of_int \<lfloor>x / 2 / real m\<rfloor>) (x / 2) = sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)
[PROOF STEP]
by (subst split[where \<alpha> = "1/2"])
       (simp_all add: sum_upto_def sum_subtractf ring_distribs
                      sum_distrib_left sum_distrib_right mult_ac)
[PROOF STATE]
proof (state)
this:
T x - 2 * T (x / 2) = sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have "S x - S (x / 2) = (\<Sum>n | n > 0 \<and> real n \<in> {x/2<..x}. a n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S x - S (x / 2) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n)
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto a x - sum_upto a (x / 2) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n)
[PROOF STEP]
by (subst split[where \<alpha> = "1 / 2"]) (auto simp: sum_upto_def)
[PROOF STATE]
proof (state)
this:
S x - S (x / 2) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
S x - S (x / 2) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have "\<dots> = (\<Sum>n | n > 0 \<and> real n \<in> {x/2<..x}. a n * \<lfloor>x / n\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)
[PROOF STEP]
proof (intro sum.cong)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
 2. \<And>xa. xa \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}} \<Longrightarrow> a xa = a xa * real_of_int \<lfloor>x / real xa\<rfloor>
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
 2. \<And>xa. xa \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}} \<Longrightarrow> a xa = a xa * real_of_int \<lfloor>x / real xa\<rfloor>
[PROOF STEP]
assume "n \<in> {n. n > 0 \<and> real n \<in> {x/2<..x}}"
[PROOF STATE]
proof (state)
this:
n \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}}

goal (2 subgoals):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
 2. \<And>xa. xa \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}} \<Longrightarrow> a xa = a xa * real_of_int \<lfloor>x / real xa\<rfloor>
[PROOF STEP]
hence "x / n \<ge> 1" "x / n < 2"
[PROOF STATE]
proof (prove)
using this:
n \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}}

goal (1 subgoal):
 1. 1 \<le> x / real n &&& x / real n < 2
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
1 \<le> x / real n
x / real n < 2

goal (2 subgoals):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
 2. \<And>xa. xa \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}} \<Longrightarrow> a xa = a xa * real_of_int \<lfloor>x / real xa\<rfloor>
[PROOF STEP]
hence "\<lfloor>x / n\<rfloor> = 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> x / real n
x / real n < 2

goal (1 subgoal):
 1. \<lfloor>x / real n\<rfloor> = 1
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<lfloor>x / real n\<rfloor> = 1

goal (2 subgoals):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
 2. \<And>xa. xa \<in> {n. 0 < n \<and> real n \<in> {x / 2<..x}} \<Longrightarrow> a xa = a xa * real_of_int \<lfloor>x / real xa\<rfloor>
[PROOF STEP]
thus "a n = a n * \<lfloor>x / n\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>x / real n\<rfloor> = 1

goal (1 subgoal):
 1. a n = a n * real_of_int \<lfloor>x / real n\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a n = a n * real_of_int \<lfloor>x / real n\<rfloor>

goal (1 subgoal):
 1. {n. 0 < n \<and> real n \<in> {x / 2<..x}} = {n. 0 < n \<and> real n \<in> {x / 2<..x}}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n) = (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have "\<dots> = 0 + \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = 0 + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = 0 + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = 0 + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have "0 \<le> sum_upto (\<lambda>n. a n * (\<lfloor>x / n\<rfloor> - 2 * \<lfloor>x / (2 * n)\<rfloor>)) (x / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2)
[PROOF STEP]
unfolding sum_upto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (\<Sum>n\<in>{i. 0 < i \<and> real i \<le> x / 2}. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>))
[PROOF STEP]
proof (intro sum_nonneg mult_nonneg_nonneg a_nonneg)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 < xa
 2. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 \<le> real_of_int (\<lfloor>x / real xa\<rfloor> - 2 * \<lfloor>x / real (2 * xa)\<rfloor>)
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 < xa
 2. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 \<le> real_of_int (\<lfloor>x / real xa\<rfloor> - 2 * \<lfloor>x / real (2 * xa)\<rfloor>)
[PROOF STEP]
assume "n \<in> {n. n > 0 \<and> real n \<le> x / 2}"
[PROOF STATE]
proof (state)
this:
n \<in> {n. 0 < n \<and> real n \<le> x / 2}

goal (2 subgoals):
 1. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 < xa
 2. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 \<le> real_of_int (\<lfloor>x / real xa\<rfloor> - 2 * \<lfloor>x / real (2 * xa)\<rfloor>)
[PROOF STEP]
hence "x / real n \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
n \<in> {n. 0 < n \<and> real n \<le> x / 2}

goal (1 subgoal):
 1. 2 \<le> x / real n
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
2 \<le> x / real n

goal (2 subgoals):
 1. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 < xa
 2. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 \<le> real_of_int (\<lfloor>x / real xa\<rfloor> - 2 * \<lfloor>x / real (2 * xa)\<rfloor>)
[PROOF STEP]
thus "real_of_int (\<lfloor>x / n\<rfloor> - 2 * \<lfloor>x / (2 * n)\<rfloor>) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
2 \<le> x / real n

goal (1 subgoal):
 1. 0 \<le> real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)
[PROOF STEP]
using le_mult_floor[of 2 "x / (2 * n)"]
[PROOF STATE]
proof (prove)
using this:
2 \<le> x / real n
\<lbrakk>0 \<le> 2; 0 \<le> x / real (2 * n)\<rbrakk> \<Longrightarrow> \<lfloor>2\<rfloor> * \<lfloor>x / real (2 * n)\<rfloor> \<le> \<lfloor>2 * (x / real (2 * n))\<rfloor>

goal (1 subgoal):
 1. 0 \<le> real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)
[PROOF STEP]
by (simp add: mult_ac)
[PROOF STATE]
proof (state)
this:
0 \<le> real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)

goal (1 subgoal):
 1. \<And>xa. xa \<in> {i. 0 < i \<and> real i \<le> x / 2} \<Longrightarrow> 0 < xa
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
0 \<le> sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
have "\<dots> + (\<Sum>n | n > 0 \<and> real n \<in> {x/2<..x}. a n * \<lfloor>x / n\<rfloor>) = T x - 2 * T (x / 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = T x - 2 * T (x / 2)
[PROOF STEP]
using T_diff_eq
[PROOF STATE]
proof (prove)
using this:
T x - 2 * T (x / 2) = sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)

goal (1 subgoal):
 1. sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = T x - 2 * T (x / 2)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sum_upto (\<lambda>n. a n * real_of_int (\<lfloor>x / real n\<rfloor> - 2 * \<lfloor>x / real (2 * n)\<rfloor>)) (x / 2) + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) = T x - 2 * T (x / 2)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>xa y. xa \<le> y \<Longrightarrow> xa + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) \<le> y + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)) \<Longrightarrow> S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
show "S x - S (x / 2) \<le> T x - 2 * T (x / 2)"
[PROOF STATE]
proof (prove)
using this:
(\<And>xa y. xa \<le> y \<Longrightarrow> xa + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>) \<le> y + (\<Sum>n | 0 < n \<and> real n \<in> {x / 2<..x}. a n * real_of_int \<lfloor>x / real n\<rfloor>)) \<Longrightarrow> S x - S (x / 2) \<le> T x - 2 * T (x / 2)

goal (1 subgoal):
 1. S x - S (x / 2) \<le> T x - 2 * T (x / 2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
S x - S (x / 2) \<le> T x - 2 * T (x / 2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod_mangoldt1_floor_bigo:
  includes prime_counting_notation
  shows "(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln n) floor x - x * ln x) \<in> O(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
proof -
  \<comment> \<open>This is a perhaps somewhat roundabout way of proving this statement. We show this using
      the asymptotics of \<open>\<MM>\<close>: $\mathfrak{M}(x) = \ln x + O(1)$

      We proved this before (which was a bit of work, but not that much).
      Apostol, on the other hand, shows the following statement first and then deduces the
      asymptotics of \<open>\<MM>\<close> with Shapiro's Tauberian theorem instead. This might save a bit of
      work, but it is probably negligible.\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
define R where "R = (\<lambda>x. sum_upto (\<lambda>i. ind prime i * ln i * frac (x / i)) x)"
[PROOF STATE]
proof (state)
this:
R = (\<lambda>x. sum_upto (\<lambda>i. ind prime i * ln (real i) * frac (x / real i)) x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
have *: "R x \<in> {0..ln 4 * x}" if "x \<ge> 1" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
have "R x \<le> \<theta> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R x \<le> \<theta> x
[PROOF STEP]
unfolding R_def prime_sum_upto_altdef1 sum_upto_def \<theta>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i | 0 < i \<and> real i \<le> x. ind prime i * ln (real i) * frac (x / real i)) \<le> (\<Sum>p\<in>{i. 0 < i \<and> real i \<le> x}. ind prime p * ln (real p))
[PROOF STEP]
by (intro sum_mono) (auto simp: ind_def less_imp_le[OF frac_lt_1] dest!: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
R x \<le> \<theta> x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
R x \<le> \<theta> x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
have "\<dots> < ln 4 * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<theta> x < ln 4 * x
[PROOF STEP]
by (rule \<theta>_upper_bound) fact+
[PROOF STATE]
proof (state)
this:
\<theta> x < ln 4 * x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
R x < ln 4 * x
[PROOF STEP]
have "R x \<le> ln 4 * x"
[PROOF STATE]
proof (prove)
using this:
R x < ln 4 * x

goal (1 subgoal):
 1. R x \<le> ln 4 * x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R x \<le> ln 4 * x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R x \<le> ln 4 * x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
have "R x \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> R x
[PROOF STEP]
unfolding R_def sum_upto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> (\<Sum>i | 0 < i \<and> real i \<le> x. ind prime i * ln (real i) * frac (x / real i))
[PROOF STEP]
by (intro sum_nonneg mult_nonneg_nonneg) (auto simp: ind_def)
[PROOF STATE]
proof (state)
this:
0 \<le> R x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
R x \<le> ln 4 * x
0 \<le> R x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
R x \<le> ln 4 * x
0 \<le> R x

goal (1 subgoal):
 1. R x \<in> {0..ln 4 * x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
R x \<in> {0..ln 4 * x}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
1 \<le> ?x \<Longrightarrow> R ?x \<in> {0..ln 4 * ?x}

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
have "eventually (\<lambda>x. \<bar>R x\<bar> \<le> ln 4 * \<bar>x\<bar>) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. \<bar>R x\<bar> \<le> ln 4 * \<bar>x\<bar>
[PROOF STEP]
using eventually_ge_at_top[of 1]
[PROOF STATE]
proof (prove)
using this:
eventually ((\<le>) (1::?'a1)) at_top

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. \<bar>R x\<bar> \<le> ln 4 * \<bar>x\<bar>
[PROOF STEP]
by eventually_elim (use * in auto)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. \<bar>R x\<bar> \<le> ln 4 * \<bar>x\<bar>

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
hence "R \<in> O(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. \<bar>R x\<bar> \<le> ln 4 * \<bar>x\<bar>

goal (1 subgoal):
 1. R \<in> O(\<lambda>x. x)
[PROOF STEP]
by (intro landau_o.bigI[of "ln 4"]) auto
[PROOF STATE]
proof (state)
this:
R \<in> O(\<lambda>x. x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln n) floor x - x * ln x) =
          (\<lambda>x. x * (\<MM> x - ln x) - R x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) = (\<lambda>x. x * (\<MM> x - ln x) - R x)
[PROOF STEP]
by (auto simp: primes_M_def dirichlet_prod'_def prime_sum_upto_altdef1 sum_upto_def
                   frac_def sum_subtractf sum_distrib_left sum_distrib_right algebra_simps R_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) = (\<lambda>x. x * (\<MM> x - ln x) - R x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) = (\<lambda>x. x * (\<MM> x - ln x) - R x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
have "\<dots> \<in> O(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x * (\<MM> x - ln x) - R x) \<in> O(\<lambda>x. x)
[PROOF STEP]
proof (rule sum_in_bigo)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x)
 2. R \<in> O(\<lambda>x. x)
[PROOF STEP]
have "(\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x * 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x * 1)
[PROOF STEP]
by (intro landau_o.big.mult mertens_bounded) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x * 1)

goal (2 subgoals):
 1. (\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x)
 2. R \<in> O(\<lambda>x. x)
[PROOF STEP]
thus "(\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x * 1)

goal (1 subgoal):
 1. (\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x * (\<MM> x - ln x)) \<in> O(\<lambda>x. x)

goal (1 subgoal):
 1. R \<in> O(\<lambda>x. x)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x * (\<MM> x - ln x) - R x) \<in> O(\<lambda>x. x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dirichlet_prod'_mangoldt_floor_asymptotics:
  "(\<lambda>x. dirichlet_prod' mangoldt floor x - x * ln x + x) \<in> O(ln)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
have "dirichlet_prod' mangoldt floor = (\<lambda>x. sum_upto ln x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) = sum_upto (\<lambda>x. ln (real x))
[PROOF STEP]
unfolding sum_upto_ln_conv_sum_upto_mangoldt dirichlet_prod'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sum_upto (\<lambda>m. mangoldt m * real_of_int \<lfloor>x / real m\<rfloor>) x) = (\<lambda>x. sum_upto (\<lambda>xa. mangoldt xa * real (nat \<lfloor>x / real xa\<rfloor>)) x)
[PROOF STEP]
by (intro sum_upto_cong' ext) auto
[PROOF STATE]
proof (state)
this:
dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) = sum_upto (\<lambda>x. ln (real x))

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
hence "(\<lambda>x. dirichlet_prod' mangoldt floor x - x * ln x + x) = (\<lambda>x. sum_upto ln x - x * ln x + x)"
[PROOF STATE]
proof (prove)
using this:
dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) = sum_upto (\<lambda>x. ln (real x))

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) = (\<lambda>x. sum_upto (\<lambda>x. ln (real x)) x - x * ln x + x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) = (\<lambda>x. sum_upto (\<lambda>x. ln (real x)) x - x * ln x + x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) = (\<lambda>x. sum_upto (\<lambda>x. ln (real x)) x - x * ln x + x)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
have "\<dots> \<in> O(ln)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sum_upto (\<lambda>x. ln (real x)) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
by (rule sum_upto_ln_stirling_weak_bigo)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. sum_upto (\<lambda>x. ln (real x)) x - x * ln x + x) \<in> O(ln)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
show "(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)

goal (1 subgoal):
 1. (\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_upto_\<psi>_x_over_n_asymptotics:
        "(\<lambda>x. sum_upto (\<lambda>n. primes_psi (x / n)) x - x * ln x + x) \<in> O(ln)"
  and sum_upto_\<theta>_x_over_n_asymptotics:
        "(\<lambda>x. sum_upto (\<lambda>n. primes_theta (x / n)) x - x * ln x) \<in> O(\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. sum_upto (\<lambda>xa. primes_psi (x / real xa)) x - x * ln x + x) \<in> O(ln) &&& (\<lambda>x. sum_upto (\<lambda>xa. primes_theta (x / real xa)) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
using dirichlet_prod_mangoldt1_floor_bigo dirichlet_prod'_mangoldt_floor_asymptotics
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. dirichlet_prod' (\<lambda>n. ind prime n * ln (real n)) (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x) \<in> O(\<lambda>x. x)
(\<lambda>x. dirichlet_prod' mangoldt (\<lambda>x. real_of_int \<lfloor>x\<rfloor>) x - x * ln x + x) \<in> O(ln)

goal (1 subgoal):
 1. (\<lambda>x. sum_upto (\<lambda>xa. primes_psi (x / real xa)) x - x * ln x + x) \<in> O(ln) &&& (\<lambda>x. sum_upto (\<lambda>xa. primes_theta (x / real xa)) x - x * ln x) \<in> O(\<lambda>x. x)
[PROOF STEP]
by (simp_all add: dirichlet_prod'_floor_conv_sum_upto primes_theta_def
                    primes_psi_def prime_sum_upto_altdef1)


[STATEMENT]
lemma [code]: "Rat.of_int (int_of_integer x) = rat_of_integer x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rat.of_int (int_of_integer x) = rat_of_integer x
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma [code_unfold]: "quotient_of = (\<lambda>x. map_prod int_of_integer int_of_integer (quotient_of' x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of = (\<lambda>x. map_prod int_of_integer int_of_integer (quotient_of' x))
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma tauActTauStepChain:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'"

  shows "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by auto


[STATEMENT]
lemma tauActTauChain:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'"

  shows "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl)


[STATEMENT]
lemma tauStepChainEqvt[eqvt]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"

  shows "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
proof(induct rule: tauStepChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. \<Psi> \<rhd> a \<longmapsto> \<tau> \<prec> b \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b
 2. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
case(TauBase P P')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (2 subgoals):
 1. \<And>a b. \<Psi> \<rhd> a \<longmapsto> \<tau> \<prec> b \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b
 2. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
hence "\<Psi> \<rhd> P \<longmapsto>\<tau> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (2 subgoals):
 1. \<And>a b. \<Psi> \<rhd> a \<longmapsto> \<tau> \<prec> b \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b
 2. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<longmapsto> \<tau> \<prec> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
by(force dest: semantics.eqvt simp add: eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
case(TauStep P P' P'')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
hence "\<Psi> \<rhd> P' \<longmapsto>\<tau> \<prec> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
hence "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P') \<longmapsto>\<tau> \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P' \<longmapsto> \<tau> \<prec> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P' \<longmapsto> \<tau> \<prec> p \<bullet> P''
[PROOF STEP]
by(force dest: semantics.eqvt simp add: eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P' \<longmapsto> \<tau> \<prec> p \<bullet> P''

goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sub>\<tau> b; p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> b; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c\<rbrakk> \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> a \<Longrightarrow>\<^sub>\<tau> p \<bullet> c
[PROOF STEP]
with \<open>(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (p \<bullet> P')\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
p \<bullet> \<Psi> \<rhd> p \<bullet> P' \<longmapsto> \<tau> \<prec> p \<bullet> P''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
p \<bullet> \<Psi> \<rhd> p \<bullet> P' \<longmapsto> \<tau> \<prec> p \<bullet> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P''
[PROOF STEP]
by(subst trancl.trancl_into_trancl) auto
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P''

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tauChainEqvt[eqvt]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"

  shows "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl eqvts)


[STATEMENT]
lemma tauStepChainEqvt'[eqvt]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  shows "(p \<bullet> (\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P')) = (p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P' = p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P' \<Longrightarrow> \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(drule_tac p="rev p" in tauStepChainEqvt) auto


[STATEMENT]
lemma tauChainEqvt'[eqvt]:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  shows "(p \<bullet> (\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P')) = (p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' = p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst] rtrancl_eq_or_trancl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sub>\<tau> p \<bullet> P'; P \<noteq> P'\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(drule_tac p="rev p" in tauStepChainEqvt) auto


[STATEMENT]
lemma tauStepChainFresh:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "x \<sharp> P"

  shows "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by(induct rule: trancl.induct) (auto dest: tauFreshDerivative)


[STATEMENT]
lemma tauChainFresh:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "x \<sharp> P"

  shows "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainFresh)


[STATEMENT]
lemma tauStepChainFreshChain:
  fixes \<Psi>    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   P'    :: "('a, 'b, 'c) psi"
  and   xvec  :: "name list"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "xvec \<sharp>* P"

  shows "xvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
xvec \<sharp>* P

goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
by(induct xvec) (auto intro: tauStepChainFresh)


[STATEMENT]
lemma tauChainFreshChain:
  fixes \<Psi>    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   P'    :: "('a, 'b, 'c) psi"
  and   xvec  :: "name list"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "xvec \<sharp>* P"

  shows "xvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
xvec \<sharp>* P

goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
by(induct xvec) (auto intro: tauChainFresh)


[STATEMENT]
lemma tauStepChainCase:
  fixes \<Psi>  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   \<phi>  :: 'c
  and   Cs :: "('c \<times> ('a, 'b, 'c) psi) list"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "(\<phi>, P) mem Cs"
  and     "\<Psi> \<turnstile> \<phi>"
  and     "guarded P"

  shows "\<Psi> \<rhd> (Cases Cs) \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> Cases Cs \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
(\<phi>, P) mem Cs
\<Psi> \<turnstile> \<phi>
guarded P

goal (1 subgoal):
 1. \<Psi> \<rhd> Cases Cs \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(induct rule: trancl.induct) (auto intro: Case trancl_into_trancl)


[STATEMENT]
lemma tauStepChainResPres:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "x \<sharp> \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
x \<sharp> \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
by(induct rule: trancl.induct) (auto dest: Scope trancl_into_trancl)


[STATEMENT]
lemma tauChainResPres:
  fixes \<Psi> :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "x \<sharp> \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
x \<sharp> \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>x\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>x\<rparr>P'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainResPres)


[STATEMENT]
lemma tauStepChainResChainPres:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "xvec \<sharp>* \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'
[PROOF STEP]
by(induct xvec) (auto intro: tauStepChainResPres)


[STATEMENT]
lemma tauChainResChainPres:
  fixes \<Psi>    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "xvec \<sharp>* \<Psi>"

  shows "\<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
xvec \<sharp>* \<Psi>

goal (1 subgoal):
 1. \<Psi> \<rhd> \<lparr>\<nu>*xvec\<rparr>P \<Longrightarrow>\<^sup>^\<^sub>\<tau> \<lparr>\<nu>*xvec\<rparr>P'
[PROOF STEP]
by(induct xvec) (auto intro: tauChainResPres)


[STATEMENT]
lemma tauStepChainPar1:
  fixes \<Psi>  :: 'b
  and   \<Psi>\<^sub>Q :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   A\<^sub>Q :: "name list"

  assumes "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>"
  and     "A\<^sub>Q \<sharp>* \<Psi>"
  and     "A\<^sub>Q \<sharp>* P"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
by(induct rule: trancl.induct)  (auto dest: Par1 tauStepChainFreshChain trancl_into_trancl)


[STATEMENT]
lemma tauChainPar1:
  fixes \<Psi>  :: 'b
  and   \<Psi>\<^sub>Q :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   A\<^sub>Q :: "name list"

  assumes "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>"
  and     "A\<^sub>Q \<sharp>* \<Psi>"
  and     "A\<^sub>Q \<sharp>* P"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
extractFrame Q = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>
A\<^sub>Q \<sharp>* \<Psi>
A\<^sub>Q \<sharp>* P

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<parallel> Q
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar1)


[STATEMENT]
lemma tauStepChainPar2:
  fixes \<Psi>  :: 'b
  and   \<Psi>\<^sub>P :: 'b
  and   Q   :: "('a, 'b, 'c) psi"
  and   Q'  :: "('a, 'b, 'c) psi"
  and   P   :: "('a, 'b, 'c) psi"
  and   A\<^sub>P :: "name list"

  assumes "\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<Longrightarrow>\<^sub>\<tau> Q'"
  and     "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
  and     "A\<^sub>P \<sharp>* \<Psi>"
  and     "A\<^sub>P \<sharp>* Q"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<Longrightarrow>\<^sub>\<tau> Q'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
A\<^sub>P \<sharp>* Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
by(induct rule: trancl.induct) (auto dest: Par2 trancl_into_trancl tauStepChainFreshChain)


[STATEMENT]
lemma tauChainPar2:
  fixes \<Psi>  :: 'b
  and   \<Psi>\<^sub>P :: 'b
  and   Q   :: "('a, 'b, 'c) psi"
  and   Q'  :: "('a, 'b, 'c) psi"
  and   P   :: "('a, 'b, 'c) psi"
  and   A\<^sub>P :: "name list"

  assumes "\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
  and     "extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>"
  and     "A\<^sub>P \<sharp>* \<Psi>"
  and     "A\<^sub>P \<sharp>* Q"

  shows "\<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P \<parallel> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>\<^sub>P \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
extractFrame P = \<langle>A\<^sub>P, \<Psi>\<^sub>P\<rangle>
A\<^sub>P \<sharp>* \<Psi>
A\<^sub>P \<sharp>* Q

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<parallel> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> P \<parallel> Q'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar2)


[STATEMENT]
lemma tauStepChainBang:
  fixes \<Psi>  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "guarded P"

  shows "\<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<parallel> !P \<Longrightarrow>\<^sub>\<tau> P'
guarded P

goal (1 subgoal):
 1. \<Psi> \<rhd> !P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(induct x1=="P \<parallel> !P" P' rule: trancl.induct) (auto intro: Bang dest: Bang trancl_into_trancl)


[STATEMENT]
lemma tauStepChainStatEq:
  fixes \<Psi>  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   \<Psi>' :: 'b

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
  and     "\<Psi> \<simeq> \<Psi>'"

  shows "\<Psi>' \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sub>\<tau> P'
[PROOF STEP]
by(induct rule: trancl.induct) (auto dest: statEqTransition trancl_into_trancl)


[STATEMENT]
lemma tauChainStatEq:
  fixes \<Psi>  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   \<Psi>' :: 'b

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
  and     "\<Psi> \<simeq> \<Psi>'"

  shows "\<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<simeq> \<Psi>'

goal (1 subgoal):
 1. \<Psi>' \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainStatEq)


[STATEMENT]
lemma weakTransitionI:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   P''  :: "('a, 'b, 'c) psi"
  and   \<alpha>   :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
  and     "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
  and     "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
by(auto simp add: weakTransition_def)


[STATEMENT]
lemma weakTransitionE:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"

  obtains P'' where "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                 and "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: weakTransition_def)


[STATEMENT]
lemma weakOutputAlpha:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'"
  and     S: "set p \<subseteq> set xvec \<times> set(p \<bullet> xvec)"
  and     "distinctPerm p"
  and     "xvec \<sharp>* P"
  and     "xvec \<sharp>* (p \<bullet> xvec)"
  and     "(p \<bullet> xvec) \<sharp>* M"
  and     "distinct xvec"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                           and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
note PChain QeqP''
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
from PChain \<open>xvec \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
xvec \<sharp>* P
[PROOF STEP]
have "xvec \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
xvec \<sharp>* P

goal (1 subgoal):
 1. xvec \<sharp>* P''
[PROOF STEP]
by(rule tauChainFreshChain)
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
with P''Trans \<open>xvec \<sharp>* (p \<bullet> xvec)\<close> \<open>distinct xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* M\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'
xvec \<sharp>* (p \<bullet> xvec)
distinct xvec
(p \<bullet> xvec) \<sharp>* M
xvec \<sharp>* P''
[PROOF STEP]
have "xvec \<sharp>* (p \<bullet> N)" and "xvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'
xvec \<sharp>* (p \<bullet> xvec)
distinct xvec
(p \<bullet> xvec) \<sharp>* M
xvec \<sharp>* P''

goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> N) &&& xvec \<sharp>* P'
[PROOF STEP]
by(force intro: outputFreshChainDerivative)+
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* (p \<bullet> N)
xvec \<sharp>* P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
hence "(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> N)" and "(p \<bullet> xvec) \<sharp>* (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* (p \<bullet> N)
xvec \<sharp>* P'

goal (1 subgoal):
 1. (p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> N) &&& (p \<bullet> xvec) \<sharp>* (p \<bullet> P')
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])+
[PROOF STATE]
proof (state)
this:
(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> N)
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> N)
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')
[PROOF STEP]
have "(p \<bullet> xvec) \<sharp>* N" and "(p \<bullet> xvec) \<sharp>* (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> xvec) \<sharp>* (p \<bullet> p \<bullet> N)
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')

goal (1 subgoal):
 1. (p \<bullet> xvec) \<sharp>* N &&& (p \<bullet> xvec) \<sharp>* (p \<bullet> P')
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
with P''Trans S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* (p \<bullet> P')

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
apply(simp add: residualInject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Psi> \<rhd> P'' \<longmapsto> ROut M (\<lparr>\<nu>*p \<bullet> xvec\<rparr>(p \<bullet> N) \<prec>' P'); set p \<subseteq> set xvec \<times> set (p \<bullet> xvec); distinctPerm p; (p \<bullet> xvec) \<sharp>* N; (p \<bullet> xvec) \<sharp>* (p \<bullet> P')\<rbrakk> \<Longrightarrow> \<Psi> \<rhd> P'' \<longmapsto> ROut M (\<lparr>\<nu>*xvec\<rparr>N \<prec>' (p \<bullet> P'))
[PROOF STEP]
by(subst boundOutputChainAlpha) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakFreshDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   x    :: name

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "x \<sharp> P"
  and     "x \<sharp> \<alpha>"
  and     "bn \<alpha> \<sharp>* subject \<alpha>"
  and     "distinct(bn \<alpha>)"

  shows "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; \<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
from PChain \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P
[PROOF STEP]
have "x \<sharp> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P''
[PROOF STEP]
by(rule tauChainFresh)
[PROOF STATE]
proof (state)
this:
x \<sharp> P''

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
with P''Trans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
x \<sharp> P''
[PROOF STEP]
show "x \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
x \<sharp> P''

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
using \<open>x \<sharp> \<alpha>\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> \<alpha> \<prec> P'
x \<sharp> P''
x \<sharp> \<alpha>
bn \<alpha> \<sharp>* subject \<alpha>
distinct (bn \<alpha>)

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by(force intro: freeFreshDerivative)
[PROOF STATE]
proof (state)
this:
x \<sharp> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakFreshChainDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   \<alpha>    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   yvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     "yvec \<sharp>* P"
  and     "yvec \<sharp>* \<alpha>"
  and     "bn \<alpha> \<sharp>* subject \<alpha>"
  and     "distinct(bn \<alpha>)"

  shows "yvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yvec \<sharp>* P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'
yvec \<sharp>* P
yvec \<sharp>* \<alpha>
bn \<alpha> \<sharp>* subject \<alpha>
distinct (bn \<alpha>)

goal (1 subgoal):
 1. yvec \<sharp>* P'
[PROOF STEP]
by(induct yvec) (auto intro: weakFreshDerivative)


[STATEMENT]
lemma weakInputFreshDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   x    :: name

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'"
  and     "x \<sharp> P"
  and     "x \<sharp> N"

  shows "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>N\<rparr> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
from PChain \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P
[PROOF STEP]
have "x \<sharp> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P''
[PROOF STEP]
by(rule tauChainFresh)
[PROOF STATE]
proof (state)
this:
x \<sharp> P''

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
with P''Trans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
x \<sharp> P''
[PROOF STEP]
show "x \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
x \<sharp> P''

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
using \<open>x \<sharp> N\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
x \<sharp> P''
x \<sharp> N

goal (1 subgoal):
 1. x \<sharp> P'
[PROOF STEP]
by(force intro: inputFreshDerivative)
[PROOF STATE]
proof (state)
this:
x \<sharp> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakInputFreshChainDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'"
  and     "xvec \<sharp>* P"
  and     "xvec \<sharp>* N"

  shows "xvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'
xvec \<sharp>* P
xvec \<sharp>* N

goal (1 subgoal):
 1. xvec \<sharp>* P'
[PROOF STEP]
by(induct xvec) (auto intro: weakInputFreshDerivative)


[STATEMENT]
lemma weakOutputFreshDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   x    :: name

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     "x \<sharp> P"
  and     "x \<sharp> xvec"
  and     "xvec \<sharp>* M"
  and     "distinct xvec"

  shows "x \<sharp> N"
  and   "x \<sharp> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> N &&& x \<sharp> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<sharp> N
 2. x \<sharp> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (2 subgoals):
 1. x \<sharp> N
 2. x \<sharp> P'
[PROOF STEP]
from PChain \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P
[PROOF STEP]
have "x \<sharp> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
x \<sharp> P

goal (1 subgoal):
 1. x \<sharp> P''
[PROOF STEP]
by(rule tauChainFresh)
[PROOF STATE]
proof (state)
this:
x \<sharp> P''

goal (2 subgoals):
 1. x \<sharp> N
 2. x \<sharp> P'
[PROOF STEP]
with P''Trans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
x \<sharp> P''
[PROOF STEP]
show "x \<sharp> N" and "x \<sharp> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
x \<sharp> P''

goal (1 subgoal):
 1. x \<sharp> N &&& x \<sharp> P'
[PROOF STEP]
using \<open>x \<sharp> xvec\<close> \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
x \<sharp> P''
x \<sharp> xvec
xvec \<sharp>* M
distinct xvec

goal (1 subgoal):
 1. x \<sharp> N &&& x \<sharp> P'
[PROOF STEP]
by(force intro: outputFreshDerivative)+
[PROOF STATE]
proof (state)
this:
x \<sharp> N
x \<sharp> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakOutputFreshChainDerivative:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   yvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     "yvec \<sharp>* P"
  and     "xvec \<sharp>* yvec"
  and     "xvec \<sharp>* M"
  and     "distinct xvec"

  shows "yvec \<sharp>* N"
  and   "yvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. yvec \<sharp>* N &&& yvec \<sharp>* P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. yvec \<sharp>* N
 2. yvec \<sharp>* P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (2 subgoals):
 1. yvec \<sharp>* N
 2. yvec \<sharp>* P'
[PROOF STEP]
from PChain \<open>yvec \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P
[PROOF STEP]
have "yvec \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P

goal (1 subgoal):
 1. yvec \<sharp>* P''
[PROOF STEP]
by(rule tauChainFreshChain)
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* P''

goal (2 subgoals):
 1. yvec \<sharp>* N
 2. yvec \<sharp>* P'
[PROOF STEP]
with P''Trans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
yvec \<sharp>* P''
[PROOF STEP]
show "yvec \<sharp>* N" and "yvec \<sharp>* P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
yvec \<sharp>* P''

goal (1 subgoal):
 1. yvec \<sharp>* N &&& yvec \<sharp>* P'
[PROOF STEP]
using \<open>xvec \<sharp>* yvec\<close> \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
yvec \<sharp>* P''
xvec \<sharp>* yvec
xvec \<sharp>* M
distinct xvec

goal (1 subgoal):
 1. yvec \<sharp>* N &&& yvec \<sharp>* P'
[PROOF STEP]
by(force intro: outputFreshChainDerivative)+
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* N
yvec \<sharp>* P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakOutputPermSubject:
  fixes \<Psi>   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"
  and   zvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
  and     S: "set p \<subseteq> set yvec \<times> set zvec"
  and     "yvec \<sharp>* \<Psi>"
  and     "zvec \<sharp>* \<Psi>"
  and     "yvec \<sharp>* P"
  and     "zvec \<sharp>* P"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                            and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from PChain \<open>yvec \<sharp>* P\<close> \<open>zvec \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P
zvec \<sharp>* P
[PROOF STEP]
have "yvec \<sharp>* P''" and "zvec \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P
zvec \<sharp>* P

goal (1 subgoal):
 1. yvec \<sharp>* P'' &&& zvec \<sharp>* P''
[PROOF STEP]
by(force intro: tauChainFreshChain)+
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* P''
zvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
note PChain QeqP''
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
from P''Trans S \<open>yvec \<sharp>* \<Psi>\<close> \<open>zvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P''\<close> \<open>zvec \<sharp>* P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
set p \<subseteq> set yvec \<times> set zvec
yvec \<sharp>* \<Psi>
zvec \<sharp>* \<Psi>
yvec \<sharp>* P''
zvec \<sharp>* P''
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<longmapsto>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
set p \<subseteq> set yvec \<times> set zvec
yvec \<sharp>* \<Psi>
zvec \<sharp>* \<Psi>
yvec \<sharp>* P''
zvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
by(rule_tac outputPermSubject) (assumption | auto)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakInputPermSubject:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"
  and   zvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'"
  and     S: "set p \<subseteq> set yvec \<times> set zvec"
  and     "yvec \<sharp>* \<Psi>"
  and     "zvec \<sharp>* \<Psi>"
  and     "yvec \<sharp>* P"
  and     "zvec \<sharp>* P"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                            and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>N\<rparr> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>; \<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
from PChain \<open>yvec \<sharp>* P\<close> \<open>zvec \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P
zvec \<sharp>* P
[PROOF STEP]
have "yvec \<sharp>* P''" and "zvec \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
yvec \<sharp>* P
zvec \<sharp>* P

goal (1 subgoal):
 1. yvec \<sharp>* P'' &&& zvec \<sharp>* P''
[PROOF STEP]
by(force intro: tauChainFreshChain)+
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* P''
zvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
note PChain QeqP''
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
from P''Trans S \<open>yvec \<sharp>* \<Psi>\<close> \<open>zvec \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P''\<close> \<open>zvec \<sharp>* P''\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
set p \<subseteq> set yvec \<times> set zvec
yvec \<sharp>* \<Psi>
zvec \<sharp>* \<Psi>
yvec \<sharp>* P''
zvec \<sharp>* P''
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<longmapsto>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P'' \<longmapsto> M\<lparr>N\<rparr> \<prec> P'
set p \<subseteq> set yvec \<times> set zvec
yvec \<sharp>* \<Psi>
zvec \<sharp>* \<Psi>
yvec \<sharp>* P''
zvec \<sharp>* P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
by(rule_tac inputPermSubject) auto
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>
\<Psi> \<rhd> P'' \<longmapsto> (p \<bullet> M)\<lparr>N\<rparr> \<prec> P'

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>N\<rparr> \<prec> P'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakInput:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   K    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   Tvec :: "'a list"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "\<Psi> \<turnstile> M \<leftrightarrow> K"
  and     "distinct xvec"
  and     "set xvec \<subseteq> supp N"
  and     "length xvec = length Tvec"
  and     Qeq\<Psi>: "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>"

  shows "\<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>(N[xvec::=Tvec])\<rparr> \<prec> P[xvec::=Tvec]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
have "\<Psi> \<rhd>  M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
from Qeq\<Psi>
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
have "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame(M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<turnstile> M \<leftrightarrow> K
distinct xvec
set xvec \<subseteq> supp N
length xvec = length Tvec
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>
[PROOF STEP]
have "\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto>K\<lparr>(N[xvec::=Tvec])\<rparr> \<prec> P[xvec::=Tvec]"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<turnstile> M \<leftrightarrow> K
distinct xvec
set xvec \<subseteq> supp N
length xvec = length Tvec
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F \<langle>\<epsilon>, \<Psi> \<otimes> \<one>\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
by(rule_tac Input)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>\<^sup>^\<^sub>\<tau> M\<lparr>\<lambda>*xvec N\<rparr>.P
insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame (M\<lparr>\<lambda>*xvec N\<rparr>.P)) \<Psi>
\<Psi> \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<longmapsto> K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> M\<lparr>\<lambda>*xvec N\<rparr>.P \<Longrightarrow>K\<lparr>N[xvec::=Tvec]\<rparr> \<prec> P[xvec::=Tvec]

goal:
No subgoals!
[PROOF STEP]
qed