[STATEMENT]
lemma aux_lt_implies_mask:
  assumes "a < 2^k"
  shows "\<forall>r\<ge>k. a \<exclamdown> r = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<ge>k. a \<exclamdown> r = 0
[PROOF STEP]
using nth_bit_def assms
[PROOF STATE]
proof (prove)
using this:
?num \<exclamdown> ?k = ?num div 2 ^ ?k mod 2
a < 2 ^ k

goal (1 subgoal):
 1. \<forall>r\<ge>k. a \<exclamdown> r = 0
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
(* found by e *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
fix r :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
assume a1: "a < 2 ^ k"
[PROOF STATE]
proof (state)
this:
a < 2 ^ k

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
assume a2: "k \<le> r"
[PROOF STATE]
proof (state)
this:
k \<le> r

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
have "a div 2 ^ k = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a div 2 ^ k = 0
[PROOF STEP]
using a1 Euclidean_Division.div_eq_0_iff
[PROOF STATE]
proof (prove)
using this:
a < 2 ^ k
(?m div ?n = 0) = (?m < ?n \<or> ?n = 0)

goal (1 subgoal):
 1. a div 2 ^ k = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a div 2 ^ k = 0

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a div 2 ^ k = 0
[PROOF STEP]
have "2 = (0::nat) \<or> a < 2 ^ r"
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ k = 0

goal (1 subgoal):
 1. 2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
a div 2 ^ k = 0
k \<le> r

goal (1 subgoal):
 1. 2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
by (metis (no_types) div_le_mono nat_zero_less_power_iff neq0_conv not_le power_diff)
[PROOF STATE]
proof (state)
this:
2 = 0 \<or> a < 2 ^ r

goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<And>num k. num \<exclamdown> k = num div 2 ^ k mod 2; a < 2 ^ k; k \<le> r\<rbrakk> \<Longrightarrow> a div 2 ^ r mod 2 = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 = 0 \<or> a < 2 ^ r
[PROOF STEP]
show "a div 2 ^ r mod 2 = 0"
[PROOF STATE]
proof (prove)
using this:
2 = 0 \<or> a < 2 ^ r

goal (1 subgoal):
 1. a div 2 ^ r mod 2 = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a div 2 ^ r mod 2 = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma S\<^sub>i: "E(x\<cdot>y) \<^bold>\<rightarrow> (E x \<^bold>\<and> E y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E x \<^bold>\<and> E y \<^bold>\<leftarrow> E (x \<cdot> y)
[PROOF STEP]
using S\<^sub>i\<^sub>i
[PROOF STATE]
proof (prove)
using this:
(E ?x \<^bold>\<and> E ?y \<^bold>\<leftarrow> E (?x \<cdot> ?y)) \<^bold>\<and> (E ?x \<^bold>\<leftarrow> E (dom ?x)) \<^bold>\<and> (E ?y \<^bold>\<leftarrow> E (cod ?y))

goal (1 subgoal):
 1. E x \<^bold>\<and> E y \<^bold>\<leftarrow> E (x \<cdot> y)
[PROOF STEP]
by blast


[STATEMENT]
lemma expectation_add_pair_pmf:
  fixes f :: "'a \<Rightarrow> 'c::{banach, second_countable_topology}"
  assumes "finite (set_pmf p)" and "finite (set_pmf q)"
  shows "measure_pmf.expectation (pair_pmf p q) (\<lambda>(x,y). f x + g y) =
           measure_pmf.expectation p f + measure_pmf.expectation q g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>(x,y). f x + g y) =
          measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))
[PROOF STEP]
by (simp add: case_prod_unfold)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "\<dots> = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) +
                  measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))
[PROOF STEP]
by (intro Bochner_Integration.integral_add integrable_measure_pmf_finite) (auto intro: assms)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z) + g (snd z)) = measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) + measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z))

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) =
               measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. f (fst z)) = measure_pmf.expectation (map_pmf fst (pair_pmf p q)) f

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "map_pmf fst (pair_pmf p q) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf fst (pair_pmf p q) = p
[PROOF STEP]
by (rule map_fst_pair_pmf)
[PROOF STATE]
proof (state)
this:
map_pmf fst (pair_pmf p q) = p

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map_pmf fst (pair_pmf p q) = p

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) =
               measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>z. g (snd z)) = measure_pmf.expectation (map_pmf snd (pair_pmf p q)) g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
have "map_pmf snd (pair_pmf p q) = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf snd (pair_pmf p q) = q
[PROOF STEP]
by (rule map_snd_pair_pmf)
[PROOF STATE]
proof (state)
this:
map_pmf snd (pair_pmf p q) = q

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>a. case a of (x, y) \<Rightarrow> f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>a. case a of (x, y) \<Rightarrow> f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g

goal (1 subgoal):
 1. measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation (pair_pmf p q) (\<lambda>(x, y). f x + g y) = measure_pmf.expectation p f + measure_pmf.expectation q g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cfWriteExtendFileSize:
  "[| ~ index < fileSize cfile1;
      cfWrite cfile1 index value = Some cfile2
   |] ==> fileSize cfile2 = Suc index"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfWrite cfile1 index value = Some cfile2\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (simp add: cfWrite_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; (if index div blockSize < numBlocks then if index < fileSize cfile1 then Some (cfWriteNoExtend cfile1 index value) else Some (cfWriteNoExtend (cfExtendFile cfile1 index) index value) else None) = Some cfile2\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (case_tac "index div blockSize < numBlocks", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfWriteNoExtend (cfExtendFile cfile1 index) index value = cfile2; index div blockSize < numBlocks\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (simp add: cfWriteNoExtend_def cfExtendFile_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfile1\<lparr>fileSize := Suc index, nextFreeBlock := Suc (index div blockSize), data := writeCArray (data cfile1) (index div blockSize) (writeCArray (readCArray (data cfile1) (index div blockSize)) (index mod blockSize) value)\<rparr> = cfile2; index div blockSize < numBlocks\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma min_product_empty_singleton[simp]:
  "A \<otimes>\<^sub>m {{||}} = min_set A"
  "{{||}} \<otimes>\<^sub>m A = min_set A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<otimes>\<^sub>m {{||}} = min_set A &&& {{||}} \<otimes>\<^sub>m A = min_set A
[PROOF STEP]
by (simp_all add: min_product_def)


[STATEMENT]
lemma min_set_min_union[simp]:
  "(min_set A) \<union>\<^sub>m B = A \<union>\<^sub>m B"
  "A \<union>\<^sub>m (min_set B) = A \<union>\<^sub>m B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_set A \<union>\<^sub>m B = A \<union>\<^sub>m B &&& A \<union>\<^sub>m min_set B = A \<union>\<^sub>m B
[PROOF STEP]
proof (unfold min_union_def min_set_def, safe)
[PROOF STATE]
proof (state)
goal (18 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 18 subgoals...
[PROOF STEP]
show "\<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
[PROOF STEP]
by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| ?x \<longrightarrow> xa = ?x; ?x \<in> B; ?xa |\<subseteq>| ?x; ?xb |\<in>| ?x; ?xa \<in> A\<rbrakk> \<Longrightarrow> ?xb |\<in>| ?xa

goal (17 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 17 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 17 subgoals...
[PROOF STEP]
show "\<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
[PROOF STEP]
by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| ?x \<longrightarrow> xa = ?x; ?x \<in> A; ?xa |\<subseteq>| ?x; ?xb |\<in>| ?x; ?xa \<in> B\<rbrakk> \<Longrightarrow> ?xb |\<in>| ?xa

goal (16 subgoals):
 1. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 2. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; \<forall>xa\<in>A. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 3. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>{y \<in> A. \<forall>x\<in>A. x |\<subseteq>| y \<longrightarrow> x = y} \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 4. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; x \<notin> B; xa \<in> A; xa |\<subseteq>| x; xb |\<in>| x\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 5. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 6. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 7. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A; \<forall>x\<in>A. x |\<subseteq>| xa \<longrightarrow> x = xa\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 8. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> B. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> B\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 9. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> A; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
 10. \<And>x xa xb. \<lbrakk>\<forall>xa\<in>A \<union> {y \<in> B. \<forall>x\<in>B. x |\<subseteq>| y \<longrightarrow> x = y}. xa |\<subseteq>| x \<longrightarrow> xa = x; x \<in> B; \<forall>xa\<in>B. xa |\<subseteq>| x \<longrightarrow> xa = x; xa |\<subseteq>| x; xb |\<in>| x; xa \<in> A\<rbrakk> \<Longrightarrow> xb |\<in>| xa
A total of 16 subgoals...
[PROOF STEP]
qed blast+


[STATEMENT]
lemma fold_graph_Or\<^sub>n:
  "finite \<Phi> \<Longrightarrow> fold_graph Or_ltln False_ltln \<Phi> (Or\<^sub>n \<Phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltln false\<^sub>n \<Phi> (Or\<^sub>n \<Phi>)
[PROOF STEP]
unfolding Or\<^sub>n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite \<Phi> \<Longrightarrow> fold_graph Or_ltln false\<^sub>n \<Phi> (SOME \<phi>. fold_graph Or_ltln false\<^sub>n \<Phi> \<phi>)
[PROOF STEP]
by (rule someI2_ex[OF finite_imp_fold_graph])


[STATEMENT]
lemma Gram_Schmidt_column_k_code[code abstract]:
  "vec_nth (Gram_Schmidt_column_k A k) = Gram_Schmidt_column_k_row A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (Gram_Schmidt_column_k A k) = Gram_Schmidt_column_k_row A k
[PROOF STEP]
unfolding Gram_Schmidt_column_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - proj_onto (column b A) {column i A |i. i < b} else column b A) $ a) = Gram_Schmidt_column_k_row A k
[PROOF STEP]
unfolding Gram_Schmidt_column_k_row_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - proj_onto (column b A) {column i A |i. i < b} else column b A) $ a) = (\<lambda>a. \<chi>b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>x\<in>{column i A |i. i < b}. (column b A \<bullet> x / (x \<bullet> x)) *\<^sub>R x) else column b A) $ a)
[PROOF STEP]
unfolding proj_onto_def proj_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>a b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>u\<in>{column i A |i. i < b}. (column b A \<bullet> u / (u \<bullet> u)) *\<^sub>R u) else column b A) $ a) = (\<lambda>a. \<chi>b. (if b = mod_type_class.from_nat k then column b A - (\<Sum>x\<in>{column i A |i. i < b}. (column b A \<bullet> x / (x \<bullet> x)) *\<^sub>R x) else column b A) $ a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pA2: "Fr_2 \<F> \<Longrightarrow> \<forall>A. A \<^bold>\<approx> \<C> A \<^bold>\<leftharpoonup> \<B>(\<^bold>\<midarrow>A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A \<^bold>\<leftharpoonup> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
using pB1 dual_def fp3
[PROOF STATE]
proof (prove)
using this:
\<forall>A w. \<B> A w = (A \<^bold>\<leftharpoonup> \<I> A) w
?\<phi>\<^sup>d \<equiv> \<lambda>X. ?\<phi>\<^sup>c (\<^bold>\<midarrow>X)
Fr_2 \<F> \<Longrightarrow> \<C>\<^sup>f\<^sup>p \<^bold>\<equiv> \<B>\<^sup>d

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A \<^bold>\<leftharpoonup> \<B> (\<^bold>\<midarrow>A)) w
[PROOF STEP]
unfolding equal_op_def conn
[PROOF STATE]
proof (prove)
using this:
\<forall>A w. \<B> A w = (A w \<and> \<not> \<I> A w)
?\<phi>\<^sup>d \<equiv> \<lambda>X w. \<not> ?\<phi> (\<lambda>w. \<not> X w) w
Fr_2 \<F> \<Longrightarrow> \<forall>X w. (\<C> X w = X w) = \<B>\<^sup>d X w

goal (1 subgoal):
 1. Fr_2 \<F> \<Longrightarrow> \<forall>A w. A w = (\<C> A w \<and> \<not> \<B> (\<lambda>w. \<not> A w) w)
[PROOF STEP]
by smt


[STATEMENT]
lemma in_targetsI [intro, simp]:
    assumes "ide b" and "trg t \<frown> b"
    shows "b \<in> targets t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> targets t
[PROOF STEP]
using assms targets_def resid_arr_self
[PROOF STATE]
proof (prove)
using this:
ide b
trg t \<frown> b
targets ?t = {b. ide b \<and> trg ?t \<frown> b}
?t \ ?t = trg ?t

goal (1 subgoal):
 1. b \<in> targets t
[PROOF STEP]
by simp


[STATEMENT]
lemma cong_subst_right:
    assumes "u \<sim> u'" and "t \<frown> u"
    shows "t \<frown> u'" and "t \\ u \<sim> t \\ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u' &&& t \ u \<sim> t \ u'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. t \<frown> u'
 2. t \ u \<sim> t \ u'
[PROOF STEP]
have 1: "t \<frown> u' \<and> t \\ u' \<frown> u \\ u' \<and>
                (t \\ u) \\ (u' \\ u) = (t \\ u') \\ (u \\ u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')
[PROOF STEP]
using assms cube con_sym con_target cong_subst_left(1)
[PROOF STATE]
proof (prove)
using this:
u \<sim> u'
t \<frown> u
(?v \ ?t) \ (?u \ ?t) = (?v \ ?u) \ (?t \ ?u)
?t \<frown> ?u \<Longrightarrow> ?u \<frown> ?t
\<lbrakk>?t \<lesssim> ?u; ?u \<frown> ?v\<rbrakk> \<Longrightarrow> ?t \ ?u \<frown> ?v \ ?u
\<lbrakk>?t \<sim> ?t'; ?t \<frown> ?u\<rbrakk> \<Longrightarrow> ?t' \<frown> ?u

goal (1 subgoal):
 1. t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')

goal (2 subgoals):
 1. t \<frown> u'
 2. t \ u \<sim> t \ u'
[PROOF STEP]
show "t \<frown> u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<frown> u'
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
t \<frown> u' \<and> t \ u' \<frown> u \ u' \<and> (t \ u) \ (u' \ u) = (t \ u') \ (u \ u')

goal (1 subgoal):
 1. t \<frown> u'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
t \<frown> u'

goal (1 subgoal):
 1. t \ u \<sim> t \ u'
[PROOF STEP]
show "t \\ u \<sim> t \\ u'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \ u \<sim> t \ u'
[PROOF STEP]
by (metis 1 arr_resid_iff_con assms(1) cong_reflexive resid_arr_ide)
[PROOF STATE]
proof (state)
this:
t \ u \<sim> t \ u'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma IdeI [intro]:
    assumes "Arr T" and "set T \<subseteq> Collect R.ide"
    shows "Ide T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ide T
[PROOF STEP]
using assms Ide_char
[PROOF STATE]
proof (prove)
using this:
Arr T
set T \<subseteq> Collect R.ide
Ide ?T = (Arr ?T \<and> set ?T \<subseteq> Collect R.ide)

goal (1 subgoal):
 1. Ide T
[PROOF STEP]
by force


[STATEMENT]
lemma prec_frame:
  assumes PREC: "precise P"
  assumes M1: "h\<Turnstile>(R1 \<and>\<^sub>A R2)"
  assumes F1: "R1 \<Longrightarrow>\<^sub>A P x p * F1"
  assumes F2: "R2 \<Longrightarrow>\<^sub>A P y p * F2"
  shows "x=y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
using preciseD[OF PREC] M1 F1 F2
[PROOF STATE]
proof (prove)
using this:
?h \<Turnstile> P ?a ?p * ?F \<and>\<^sub>A P ?a' ?p * ?F' \<Longrightarrow> ?a = ?a'
h \<Turnstile> R1 \<and>\<^sub>A R2
R1 \<Longrightarrow>\<^sub>A P x p * F1
R2 \<Longrightarrow>\<^sub>A P y p * F2

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (metis entailsD mod_and_dist)


[STATEMENT]
lemma upset_set_downset_set_dual: "(`) \<partial> \<circ> \<Up> = \<Down> \<circ> (`) \<partial>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (`) \<partial> \<circ> \<Up> = \<Down> \<circ> (`) \<partial>
[PROOF STEP]
unfolding downset_set_def upset_set_def fun_eq_iff comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<partial> ` {y. \<exists>x\<in>x. x \<le> y} = {y. Bex (\<partial> ` x) ((\<le>) y)}
[PROOF STEP]
apply (safe, force simp: dual_anti)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrakk>xa \<le> \<partial> xc; xc \<in> x\<rbrakk> \<Longrightarrow> xa \<in> \<partial> ` {y. \<exists>x\<in>x. x \<le> y}
[PROOF STEP]
by (metis (mono_tags, lifting) dual.exhaust dual_anti_iff mem_Collect_eq rev_image_eqI)


[STATEMENT]
lemma (in encoding) enc_respects_pred_iff_indRel_respects_pred:
  fixes Pred :: "('procS, 'procT) Proc \<Rightarrow> bool"
  shows "enc_respects_pred Pred = rel_respects_pred indRel Pred"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enc_respects_pred Pred = rel_respects_pred indRel Pred
[PROOF STEP]
using enc_respects_pred_iff_indRelR_respects_pred[where Pred="Pred"]
            indRel_respects_pred_iff_indRelR_respects_pred[where Pred="Pred"]
[PROOF STATE]
proof (prove)
using this:
enc_respects_pred Pred = rel_respects_pred indRelR Pred
rel_respects_pred indRel Pred = rel_respects_pred indRelR Pred

goal (1 subgoal):
 1. enc_respects_pred Pred = rel_respects_pred indRel Pred
[PROOF STEP]
by simp


[STATEMENT]
lemma (in encoding) refl_trans_closure_of_indRelT:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes refl: "refl TRel"
  shows "indRelTEQ TRel = (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. indRelTEQ TRel = (indRelT TRel)\<^sup>*
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (2 subgoals):
 1. \<And>a b. a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b \<Longrightarrow> (a, b) \<in> (indRelT TRel)\<^sup>*
 2. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
thus "(P, Q) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. (P, Q) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
 2. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 3. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 4. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (encR S)
[PROOF STATE]
proof (state)
this:

goal (4 subgoals):
 1. \<And>S. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
 2. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 3. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 4. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
show "(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.encR[of S TRel]
[PROOF STATE]
proof (prove)
using this:
SourceTerm S \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm (\<lbrakk>S\<rbrakk>)

goal (1 subgoal):
 1. (SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(SourceTerm S, TargetTerm (\<lbrakk>S\<rbrakk>)) \<in> (indRelT TRel)\<^sup>*

goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (encL S)
[PROOF STATE]
proof (state)
this:

goal (3 subgoals):
 1. \<And>S. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
 2. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 3. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
show "(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.encL[of S TRel]
[PROOF STATE]
proof (prove)
using this:
TargetTerm (\<lbrakk>S\<rbrakk>) \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> SourceTerm S

goal (1 subgoal):
 1. (TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TargetTerm (\<lbrakk>S\<rbrakk>), SourceTerm S) \<in> (indRelT TRel)\<^sup>*

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (target T1 T2)
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
assume "(T1, T2) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(T1, T2) \<in> TRel

goal (2 subgoals):
 1. \<And>T1 T2. (T1, T2) \<in> TRel \<Longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
 2. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
thus "(TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel

goal (1 subgoal):
 1. (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
using indRelT.target[of T1 T2 TRel]
[PROOF STATE]
proof (prove)
using this:
(T1, T2) \<in> TRel
(T1, T2) \<in> TRel \<Longrightarrow> TargetTerm T1 \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> TargetTerm T2

goal (1 subgoal):
 1. (TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(TargetTerm T1, TargetTerm T2) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
case (trans P Q R)
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
(P, Q) \<in> (indRelT TRel)\<^sup>*
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
assume "(P, Q) \<in> (indRelT TRel)\<^sup>*" and "(Q, R) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>P Q R. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q \<and> (P, Q) \<in> (indRelT TRel)\<^sup>* \<and> Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R \<and> (Q, R) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
thus "(P, R) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
(Q, R) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. (P, R) \<in> (indRelT TRel)\<^sup>*
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(P, R) \<in> (indRelT TRel)\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
assume "(P, Q) \<in> (indRelT TRel)\<^sup>*"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. \<And>a b. (a, b) \<in> (indRelT TRel)\<^sup>* \<Longrightarrow> a \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> b
[PROOF STEP]
thus "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> (indRelT TRel)\<^sup>*

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
 2. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
from refl
[PROOF STATE]
proof (chain)
picking this:
refl TRel
[PROOF STEP]
show "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P"
[PROOF STATE]
proof (prove)
using this:
refl TRel

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
using indRelTEQ_refl[of TRel]
[PROOF STATE]
proof (prove)
using this:
refl TRel
refl TRel \<Longrightarrow> refl (indRelTEQ TRel)

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
unfolding refl_on_def
[PROOF STATE]
proof (prove)
using this:
TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel)
TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. (x, x) \<in> TRel) \<Longrightarrow> indRelTEQ TRel \<subseteq> UNIV \<times> UNIV \<and> (\<forall>x\<in>UNIV. x \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> x)

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> P

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
case (step Q R)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> (indRelT TRel)\<^sup>*
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
assume "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q"
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
assume "Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (state)
this:
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
hence "Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (prove)
using this:
Q \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
by (induct, simp_all add: indRelTEQ.encR indRelTEQ.encL indRelTEQ.target)
[PROOF STATE]
proof (state)
this:
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. \<And>y z. (P, y) \<in> (indRelT TRel)\<^sup>* \<and> y \<R>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z \<and> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> y \<Longrightarrow> P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
show "P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R"
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q
Q \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal (1 subgoal):
 1. P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R
[PROOF STEP]
by (rule indRelTEQ.trans)
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<sim>\<lbrakk>\<cdot>\<rbrakk>T<TRel> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding_wrt_barbs) rel_with_target_impl_TRel_weakly_reflects_barbs:
  fixes TRel :: "('procT \<times> 'procT) set"
    and Rel  :: "(('procS, 'procT) Proc \<times> ('procS, 'procT) Proc) set"
  assumes reflection: "rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)"
      and targetInRel:  "\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel"
  shows "rel_weakly_reflects_barbs TRel TWB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_weakly_reflects_barbs TRel TWB
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
fix TP TQ a TQ'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
assume "(TP, TQ) \<in> TRel"
[PROOF STATE]
proof (state)
this:
(TP, TQ) \<in> TRel

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
with targetInRel
[PROOF STATE]
proof (chain)
picking this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
(TP, TQ) \<in> TRel
[PROOF STEP]
have "(TargetTerm TP, TargetTerm TQ) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>T1 T2. (T1, T2) \<in> TRel \<longrightarrow> (TargetTerm T1, TargetTerm T2) \<in> Rel
(TP, TQ) \<in> TRel

goal (1 subgoal):
 1. (TargetTerm TP, TargetTerm TQ) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
assume "TQ \<longmapsto>(Calculus TWB)* TQ'" and "TQ'\<down><TWB>a"
[PROOF STATE]
proof (state)
this:
TQ \<longmapsto>Calculus TWB* TQ'
TQ'\<down><TWB>a

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
hence "TargetTerm TQ\<Down>.a"
[PROOF STATE]
proof (prove)
using this:
TQ \<longmapsto>Calculus TWB* TQ'
TQ'\<down><TWB>a

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
[PROOF STEP]
have "TargetTerm TP\<Down>.a"
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)
[PROOF STEP]
using reflection weak_reflection_of_barbs_in_barbed_encoding[where Rel="Rel"]
[PROOF STATE]
proof (prove)
using this:
(TargetTerm TP, TargetTerm TQ) \<in> Rel
(\<exists>S. S \<in>S TargetTerm TQ \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TQ \<and> T\<Down><TWB>a)
rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)
rel_weakly_reflects_barbs Rel (STCalWB SWB TWB) \<and> (?P, ?Q) \<in> Rel \<and> ((\<exists>S. S \<in>S ?Q \<and> S\<Down><SWB>?a) \<or> (\<exists>T. T \<in>T ?Q \<and> T\<Down><TWB>?a)) \<Longrightarrow> (\<exists>S. S \<in>S ?P \<and> S\<Down><SWB>?a) \<or> (\<exists>T. T \<in>T ?P \<and> T\<Down><TWB>?a)

goal (1 subgoal):
 1. (\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. \<And>a b x P'. (a, b) \<in> TRel \<and> b \<longmapsto>Calculus TWB* P' \<and> P'\<down><TWB>x \<Longrightarrow> a\<Down><TWB>x
[PROOF STEP]
thus "TP\<Down><TWB>a"
[PROOF STATE]
proof (prove)
using this:
(\<exists>S. S \<in>S TargetTerm TP \<and> S\<Down><SWB>a) \<or> (\<exists>T. T \<in>T TargetTerm TP \<and> T\<Down><TWB>a)

goal (1 subgoal):
 1. TP\<Down><TWB>a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
TP\<Down><TWB>a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding_wrt_barbs) indRelTEQ_impl_TRel_respects_barbs:
  fixes TRel :: "('procT \<times> 'procT) set"
  assumes respection: "rel_respects_barbs (indRelTEQ TRel) (STCalWB SWB TWB)"
  shows "rel_respects_barbs TRel TWB"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_respects_binary_pred TRel (\<lambda>a. hasBarb a TWB)
[PROOF STEP]
using respection indRelTEQ_impl_TRel_preserves_barbs[where TRel="TRel"]
            indRelTEQ_impl_TRel_reflects_barbs[where TRel="TRel"]
[PROOF STATE]
proof (prove)
using this:
rel_respects_binary_pred (indRelTEQ TRel) (\<lambda>a. hasBarb a (STCalWB SWB TWB))
rel_preserves_binary_pred (indRelTEQ TRel) (\<lambda>a. hasBarb a (STCalWB SWB TWB)) \<Longrightarrow> rel_preserves_binary_pred TRel (\<lambda>a. hasBarb a TWB)
rel_reflects_binary_pred (indRelTEQ TRel) (\<lambda>b. hasBarb b (STCalWB SWB TWB)) \<Longrightarrow> rel_reflects_binary_pred TRel (\<lambda>b. hasBarb b TWB)

goal (1 subgoal):
 1. rel_respects_binary_pred TRel (\<lambda>a. hasBarb a TWB)
[PROOF STEP]
by blast


[STATEMENT]
lemma Qp_int_pow_add:
  fixes n::int
  fixes m::int
  assumes "a \<in> nonzero Q\<^sub>p"
  shows "a [^] (n + m) = (a [^] n) \<otimes> (a [^] m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a [^] (n + m) = a [^] n \<otimes> a [^] m
[PROOF STEP]
using monoid.int_pow_add[of Q\<^sub>p a n m] Units_eq_nonzero assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Group.monoid Q\<^sub>p; a \<in> Units Q\<^sub>p\<rbrakk> \<Longrightarrow> a [^] (n + m) = a [^] n \<otimes> a [^] m
Units Q\<^sub>p = nonzero Q\<^sub>p
a \<in> nonzero Q\<^sub>p

goal (1 subgoal):
 1. a [^] (n + m) = a [^] n \<otimes> a [^] m
[PROOF STEP]
by (simp add: Qp.monoid_axioms)


[STATEMENT]
lemma neg_int_pow_val:
  assumes "a \<in> nonzero Q\<^sub>p"
  shows "val (a[^]-(i::int)) = - (val (a[^]i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val (a [^] - i) = - val (a [^] i)
[PROOF STEP]
using int_pow_val[of a i]
[PROOF STATE]
proof (prove)
using this:
a \<in> nonzero Q\<^sub>p \<Longrightarrow> val (a [^] i) = eint i * val a

goal (1 subgoal):
 1. val (a [^] - i) = - val (a [^] i)
[PROOF STEP]
by (metis Qp_int_pow_nonzero assms int_pow_ord mult_minus_left val_ord val_p_int_pow val_p_int_pow_neg)


[STATEMENT]
lemma pgte_antisym:
  assumes "pgte a b"
      and "pgte b a"
    shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis Rep_prat_inverse assms(1) assms(2) leD le_less pgte.rep_eq)


[STATEMENT]
lemma subst_cls_lists_tl[simp]: "length Cs = length \<sigma>s \<Longrightarrow> tl (Cs \<cdot>\<cdot>cl \<sigma>s) = tl Cs \<cdot>\<cdot>cl tl \<sigma>s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length Cs = length \<sigma>s \<Longrightarrow> tl (Cs \<cdot>\<cdot>cl \<sigma>s) = tl Cs \<cdot>\<cdot>cl tl \<sigma>s
[PROOF STEP]
by (cases Cs; cases \<sigma>s) auto


[STATEMENT]
lemma psubst_ty_eqvt[eqvt]:
  fixes pi::"tvar prm"
  and   \<theta>::"Subst"
  and   T::"ty"
  shows "pi\<bullet>(\<theta><T>) = (pi\<bullet>\<theta>)<(pi\<bullet>T)>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pi \<bullet> \<theta><T> = (pi \<bullet> \<theta>)<pi \<bullet> T>
[PROOF STEP]
by (induct T rule: ty.induct) (simp_all add: eqvts)


[STATEMENT]
lemma real_cond_exp_mult:
  assumes [measurable]:"f \<in> borel_measurable F" "g \<in> borel_measurable M" "integrable M (\<lambda>x. f x * g x)"
  shows "AE x in M. real_cond_exp M F (\<lambda>x. f x * g x) x = f x * real_cond_exp M F g x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AE x in M. real_cond_exp M F (\<lambda>x. f x * g x) x = f x * real_cond_exp M F g x
[PROOF STEP]
proof (rule real_cond_exp_charact)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
assume "A \<in> sets F"
[PROOF STATE]
proof (state)
this:
A \<in> sets F

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in> sets F
[PROOF STEP]
have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F"
[PROOF STATE]
proof (prove)
using this:
A \<in> sets F

goal (1 subgoal):
 1. (\<lambda>x. f x * indicat_real A x) \<in> borel_measurable F
[PROOF STEP]
by measurable
[PROOF STATE]
proof (state)
this:
(\<lambda>x. f x * indicat_real A x) \<in> borel_measurable F

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have [measurable]: "A \<in> sets M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in> sets M
[PROOF STEP]
using subalg
[PROOF STATE]
proof (prove)
using this:
subalgebra M F

goal (1 subgoal):
 1. A \<in> sets M
[PROOF STEP]
by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
[PROOF STATE]
proof (state)
this:
A \<in> sets M

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x
[PROOF STEP]
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = LINT x|M. f x * indicat_real A x * g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x
[PROOF STEP]
apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * indicat_real A x * g x)
[PROOF STEP]
using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)]
[PROOF STATE]
proof (prove)
using this:
integrable M (\<lambda>x. indicat_real A x *\<^sub>R (f x * g x))

goal (1 subgoal):
 1. integrable M (\<lambda>x. f x * indicat_real A x * g x)
[PROOF STEP]
by (simp add: mult.commute mult.left_commute)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * g x = LINT x|M. f x * indicat_real A x * real_cond_exp M F g x

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|M. f x * indicat_real A x * real_cond_exp M F g x = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
by (simp add: mult.commute mult.left_commute set_lebesgue_integral_def)
[PROOF STATE]
proof (state)
this:
LINT x|M. f x * indicat_real A x * real_cond_exp M F g x = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (4 subgoals):
 1. \<And>A. A \<in> sets F \<Longrightarrow> \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
 2. integrable M (\<lambda>x. f x * g x)
 3. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 4. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
[PROOF STATE]
proof (prove)
using this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (1 subgoal):
 1. \<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<integral>x\<in>A. (f x * g x)\<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M

goal (3 subgoals):
 1. integrable M (\<lambda>x. f x * g x)
 2. integrable M (\<lambda>x. f x * real_cond_exp M F g x)
 3. (\<lambda>x. f x * real_cond_exp M F g x) \<in> borel_measurable F
[PROOF STEP]
qed (auto simp add: real_cond_exp_intg(1) assms)


[STATEMENT]
lemma degree_reflect_poly_eq [simp]: "coeff p 0 \<noteq> 0 \<Longrightarrow> degree (reflect_poly p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coeff p 0 \<noteq> (0::'a) \<Longrightarrow> degree (reflect_poly p) = degree p
[PROOF STEP]
by (cases p rule: pCons_cases) (simp add: reflect_poly_pCons degree_eq_length_coeffs)


[STATEMENT]
lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
  for f :: "_ \<Rightarrow> 'a::real_normed_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))
[PROOF STEP]
unfolding continuous_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<longlongrightarrow> f (Lim F (\<lambda>x. x))) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p (f (Lim F (\<lambda>x. x)))) F
[PROOF STEP]
by (rule tendsto_poly)


[STATEMENT]
lemma xor_one_eq:
  \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a XOR (1::'a) = a + of_bool (even a) - of_bool (odd a)
[PROOF STEP]
using one_xor_eq [of a]
[PROOF STATE]
proof (prove)
using this:
(1::'a) XOR a = a + of_bool (even a) - of_bool (odd a)

goal (1 subgoal):
 1. a XOR (1::'a) = a + of_bool (even a) - of_bool (odd a)
[PROOF STEP]
by (simp add: ac_simps)


[STATEMENT]
lemma bit_and_int_iff:
  \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close> for k l :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (k AND l) n = (bit k n \<and> bit l n)
[PROOF STEP]
proof (induction n arbitrary: k l)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k l. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
 2. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>k l. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
 2. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bit (k AND l) 0 = (bit k 0 \<and> bit l 0)
[PROOF STEP]
by (simp add: and_int_rec [of k l] bit_0)
[PROOF STATE]
proof (state)
this:
bit (k AND l) 0 = (bit k 0 \<and> bit l 0)

goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)

goal (1 subgoal):
 1. \<And>n k l. (\<And>k l. bit (k AND l) n = (bit k n \<and> bit l n)) \<Longrightarrow> bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
bit (?k AND ?l) n = (bit ?k n \<and> bit ?l n)

goal (1 subgoal):
 1. bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))
[PROOF STEP]
by (simp add: and_int_rec [of k l] bit_Suc)
[PROOF STATE]
proof (state)
this:
bit (k AND l) (Suc n) = (bit k (Suc n) \<and> bit l (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_int_or_eq:
  \<open>of_int (k OR l) = of_int k OR of_int l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (k OR l) = of_int k OR of_int l
[PROOF STEP]
by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)


[STATEMENT]
lemma going_to_mono: "F \<le> G \<Longrightarrow> A \<subseteq> B \<Longrightarrow> f going_to F within A \<le> f going_to G within B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<le> G; A \<subseteq> B\<rbrakk> \<Longrightarrow> f going_to F within A \<le> f going_to G within B
[PROOF STEP]
unfolding going_to_within_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>F \<le> G; A \<subseteq> B\<rbrakk> \<Longrightarrow> inf (filtercomap f F) (principal A) \<le> inf (filtercomap f G) (principal B)
[PROOF STEP]
by (intro inf_mono filtercomap_mono) simp_all


[STATEMENT]
lemma real_arch_simple: "\<exists>n. x \<le> of_nat n"
  for x :: "'a::archimedean_field"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
obtain n where "x < of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. x < of_nat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using reals_Archimedean2
[PROOF STATE]
proof (prove)
using this:
\<exists>n. ?x < of_nat n

goal (1 subgoal):
 1. (\<And>n. x < of_nat n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x < of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < of_nat n
[PROOF STEP]
have "x \<le> of_nat n"
[PROOF STATE]
proof (prove)
using this:
x < of_nat n

goal (1 subgoal):
 1. x \<le> of_nat n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<le> of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<le> of_nat n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> of_nat n

goal (1 subgoal):
 1. \<exists>n. x \<le> of_nat n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<exists>n. x \<le> of_nat n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Spy_analz_shrK [simp]:
     "evs \<in> woolam ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. evs \<in> woolam \<Longrightarrow> (Key (shrK A) \<in> analz (knows Spy evs)) = (A \<in> bad)
[PROOF STEP]
by auto


[STATEMENT]
lemma B_trusts_WL5:
     "[| Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs;
         A \<notin> bad;  B \<notin> bad;  evs \<in> woolam  |]
      ==> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Says S B (Crypt (shrK B) \<lbrace>Agent A, Nonce NB\<rbrace>) \<in> set evs; A \<notin> bad; B \<notin> bad; evs \<in> woolam\<rbrakk> \<Longrightarrow> \<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \<in> set evs
[PROOF STEP]
by (blast dest!: NB_Crypt_imp_Server_msg)


[STATEMENT]
lemma vec_lambda_eq_sum:
     "(\<chi> k. f k (x $ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "?lhs = (\<chi> k. f k (x \<bullet> axis k 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))
[PROOF STEP]
by (simp add: cart_eq_inner_axis)
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<chi>k. f k (x \<bullet> axis k 1))

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "... = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)
[PROOF STEP]
by (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x \<bullet> axis k 1)) = (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
have "... = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
by (simp add: Basis_vec_def UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>UNIV. f u (x \<bullet> axis u 1) *\<^sub>R axis u 1) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal (1 subgoal):
 1. (\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<chi>k. f k (x $ k)) = (\<Sum>k\<in>Basis. f (axis_index k) (x \<bullet> k) *\<^sub>R k)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integrable_by_parts_interior:
  fixes prod :: "_ \<Rightarrow> _ \<Rightarrow> 'b :: banach"
  assumes "bounded_bilinear (prod)" "a \<le> b"
          "continuous_on {a..b} f" "continuous_on {a..b} g"
  assumes "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (f has_vector_derivative f' x) (at x)"
          "\<And>x. x\<in>{a<..<b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
  assumes "(\<lambda>x. prod (f x) (g' x)) integrable_on {a..b}"
  shows   "(\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. prod (f' x) (g x)) integrable_on {a..b}
[PROOF STEP]
by (rule integrable_by_parts_interior_strong[of _ "{}" _ _ f g f' g']) (insert assms, simp_all)


[STATEMENT]
lemma Notes_TTP_imp_Says_A:
     "[|Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace>
           \<in> set evs;
        sub_K = Crypt (priK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>;
        A \<notin> broken; evs \<in> zg|]
     ==> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; A \<notin> broken; evs \<in> zg\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, sub_K\<rbrace> \<in> set evs
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs; A \<notin> broken; evs \<in> zg; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule rev_mp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<notin> broken; evs \<in> zg; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs
[PROOF STEP]
apply (erule zg.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set [] \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set []
 2. \<And>evsf X Ba. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evsf \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evsf \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evsf; X \<in> synth (analz (knows Spy evsf))\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Spy Ba X # evsf) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Spy Ba X # evsf)
 3. \<And>evsr Aa Ba X. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evsr \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evsr \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evsr; Says Aa Ba X \<in> set evsr\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Gets Ba X # evsr) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Gets Ba X # evsr)
 4. \<And>evs1 La C Ka m NRO Aa Ba. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs1 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs1 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs1; Nonce La \<notin> used evs1; C = Crypt Ka (Number m); Ka \<in> symKeys; NRO = Crypt (priEK Aa) \<lbrace>Number f_nro, Agent Ba, Nonce La, C\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> # evs1) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> # evs1)
 5. \<And>evs2 Ba La C NRO Aa NRR. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs2 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs2 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs2; Gets Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> \<in> set evs2; NRO = Crypt (priEK Aa) \<lbrace>Number f_nro, Agent Ba, Nonce La, C\<rbrace>; NRR = Crypt (priEK Ba) \<lbrace>Number f_nrr, Agent Aa, Nonce La, C\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Ba Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> # evs2) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Ba Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> # evs2)
 6. \<And>evs3 C Ka M Aa Ba La NRO NRR sub_Ka. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs3 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs3 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs3; C = Crypt Ka M; Ka \<in> symKeys; Says Aa Ba \<lbrace>Number f_nro, Agent Ba, Nonce La, C, NRO\<rbrace> \<in> set evs3; Gets Aa \<lbrace>Number f_nrr, Agent Aa, Nonce La, NRR\<rbrace> \<in> set evs3; NRR = Crypt (priEK Ba) \<lbrace>Number f_nrr, Agent Aa, Nonce La, C\<rbrace>; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> # evs3) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> # evs3)
 7. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<notin> broken; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, sub_Ka\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set (Says TTP Spy con_Ka # Notes TTP \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka, con_Ka\<rbrace> # evs4) \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set (Says TTP Spy con_Ka # Notes TTP \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka, con_Ka\<rbrace> # evs4)
[PROOF STEP]
apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> L = La \<and> K = Ka \<and> con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace> \<longrightarrow> Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
txt\<open>ZG4\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, con_K\<rbrace> \<in> set evs4 \<longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; Ka \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4; sub_Ka = Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>; con_Ka = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrakk> \<Longrightarrow> A = Aa \<and> B = Ba \<and> L = La \<and> K = Ka \<and> con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent Aa, Agent Ba, Nonce La, Key Ka\<rbrace> \<longrightarrow> Says Aa TTP \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka, Crypt (priEK Aa) \<lbrace>Number f_sub, Agent Ba, Nonce La, Key Ka\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>evs4 Ka Ba La sub_Ka Aa con_Ka. \<lbrakk>A \<in> bad \<longrightarrow> A = Spy; sub_K = Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>; evs4 \<in> zg; K \<in> symKeys; Gets TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4; con_K = Crypt (priEK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>; Notes TTP \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K, Crypt (priEK TTP) \<lbrace>Number f_con, Agent A, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<notin> set evs4\<rbrakk> \<Longrightarrow> Says A TTP \<lbrace>Number f_sub, Agent B, Nonce L, Key K, Crypt (priEK A) \<lbrace>Number f_sub, Agent B, Nonce L, Key K\<rbrace>\<rbrace> \<in> set evs4
[PROOF STEP]
apply (rule sub_K_validity, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_unicity :
  assumes a: "x \<leadsto> a"
  and     b: "x \<leadsto> b"
  shows "a=b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
x \<leadsto> a
x \<leadsto> b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
apply (induct arbitrary: b)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b. App (Lam [x].t\<^sub>1) t\<^sub>2 \<leadsto> b \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (erule whr_inv_auto(3))
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. \<lbrakk>[x].t\<^sub>1 = [xa].t\<^sub>1'; b = t\<^sub>1'[xa::=t\<^sub>2]\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (clarify)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. [x].t\<^sub>1 = [xa].t\<^sub>1' \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = t\<^sub>1'[xa::=t\<^sub>2]
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (rule subst_fun_eq)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b xa t\<^sub>1'. [x].t\<^sub>1 = [xa].t\<^sub>1' \<Longrightarrow> [x].t\<^sub>1 = [xa].t\<^sub>1'
 2. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 3. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x t\<^sub>1 t\<^sub>2 b t\<^sub>1'. \<lbrakk>b = App t\<^sub>1' t\<^sub>2; Lam [x].t\<^sub>1 \<leadsto> t\<^sub>1'\<rbrakk> \<Longrightarrow> t\<^sub>1[x::=t\<^sub>2] = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; App t\<^sub>1 t\<^sub>2 \<leadsto> b\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (erule whr_inv_auto(6))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b x t\<^sub>1''. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; t\<^sub>1 = Lam [x].t\<^sub>1''; b = t\<^sub>1''[x::=t\<^sub>2]\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
 2. \<And>t\<^sub>1 t\<^sub>1' t\<^sub>2 b t\<^sub>1''. \<lbrakk>t\<^sub>1 \<leadsto> t\<^sub>1'; \<And>b. t\<^sub>1 \<leadsto> b \<Longrightarrow> t\<^sub>1' = b; b = App t\<^sub>1'' t\<^sub>2; t\<^sub>1 \<leadsto> t\<^sub>1''\<rbrakk> \<Longrightarrow> App t\<^sub>1' t\<^sub>2 = b
[PROOF STEP]
apply (blast)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma analz_insert_freshK:
     "\<lbrakk>evs \<in> yahalom;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
      (K = KAB | Key K \<in> analz (knows Spy evs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>evs \<in> yahalom; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) = (K = KAB \<or> Key K \<in> analz (knows Spy evs))
[PROOF STEP]
by (simp only: analz_image_freshK analz_image_freshK_simps)