[STATEMENT]
lemma inverse_le_iff_sgn: assumes sgn: "sgn x = sgn y"
  shows "(inverse (x :: real) \<le> inverse y) = (y \<le> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
with sgn
[PROOF STATE]
proof (chain)
picking this:
sgn x = sgn y
x = 0
[PROOF STEP]
have "sgn y = 0"
[PROOF STATE]
proof (prove)
using this:
sgn x = sgn y
x = 0

goal (1 subgoal):
 1. sgn y = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn y = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
hence "y = 0"
[PROOF STATE]
proof (prove)
using this:
sgn y = 0

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
unfolding sgn_real_def
[PROOF STATE]
proof (prove)
using this:
(if y = 0 then 0 else if 0 < y then 1 else - 1) = 0

goal (1 subgoal):
 1. y = 0
[PROOF STEP]
by (cases "y = 0"; cases "y < 0"; auto)
[PROOF STATE]
proof (state)
this:
y = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
y = 0

goal (1 subgoal):
 1. (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
y = 0
x = 0

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

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
note x = this
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
proof (cases "x < 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
with x sgn
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
sgn x = sgn y
x < 0
[PROOF STEP]
have "sgn y = -1"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
sgn x = sgn y
x < 0

goal (1 subgoal):
 1. sgn y = - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn y = - 1

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
hence "y < 0"
[PROOF STATE]
proof (prove)
using this:
sgn y = - 1

goal (1 subgoal):
 1. y < 0
[PROOF STEP]
unfolding sgn_real_def
[PROOF STATE]
proof (prove)
using this:
(if y = 0 then 0 else if 0 < y then 1 else - 1) = - 1

goal (1 subgoal):
 1. y < 0
[PROOF STEP]
by (cases "y = 0"; cases "y < 0", auto)
[PROOF STATE]
proof (state)
this:
y < 0

goal (2 subgoals):
 1. x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
 2. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
by (rule inverse_le_iff_le_neg[OF True \<open>y < 0\<close>])
[PROOF STATE]
proof (state)
this:
(inverse x \<le> inverse y) = (y \<le> x)

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < 0

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
\<not> x < 0
[PROOF STEP]
have x: "x > 0"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
\<not> x < 0

goal (1 subgoal):
 1. 0 < x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < x

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
with sgn
[PROOF STATE]
proof (chain)
picking this:
sgn x = sgn y
0 < x
[PROOF STEP]
have "sgn y = 1"
[PROOF STATE]
proof (prove)
using this:
sgn x = sgn y
0 < x

goal (1 subgoal):
 1. sgn y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sgn y = 1

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
hence "y > 0"
[PROOF STATE]
proof (prove)
using this:
sgn y = 1

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
unfolding sgn_real_def
[PROOF STATE]
proof (prove)
using this:
(if y = 0 then 0 else if 0 < y then 1 else - 1) = 1

goal (1 subgoal):
 1. 0 < y
[PROOF STEP]
by (cases "y = 0"; cases "y < 0", auto)
[PROOF STATE]
proof (state)
this:
0 < y

goal (1 subgoal):
 1. \<not> x < 0 \<Longrightarrow> (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse x \<le> inverse y) = (y \<le> x)
[PROOF STEP]
by (rule inverse_le_iff_le[OF x \<open>y > 0\<close>])
[PROOF STATE]
proof (state)
this:
(inverse x \<le> inverse y) = (y \<le> x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(inverse x \<le> inverse y) = (y \<le> x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma allAllocationsEquivalenceExtended:
  "soldAllocations =  soldAllocations' &
   soldAllocations' = soldAllocations'' &
   soldAllocations'' = soldAllocations'''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. soldAllocations = soldAllocations' \<and> soldAllocations' = soldAllocations'' \<and> soldAllocations'' = soldAllocations'''
[PROOF STEP]
using soldAllocationVariantEquivalence soldAllocationsEquivalenceVariant
[PROOF STATE]
proof (prove)
using this:
soldAllocations'' ?N ?\<Omega> = soldAllocations''' ?N ?\<Omega>
soldAllocations = soldAllocations' \<and> soldAllocations' = soldAllocations'' \<and> soldAllocations = soldAllocations''

goal (1 subgoal):
 1. soldAllocations = soldAllocations' \<and> soldAllocations' = soldAllocations'' \<and> soldAllocations'' = soldAllocations'''
[PROOF STEP]
by metis


[STATEMENT]
lemma bv_prepend_equal: "bv_prepend (Suc n) b l = b#bv_prepend n b l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bv_prepend (Suc n) b l = b # bv_prepend n b l
[PROOF STEP]
by (simp add: bv_prepend)


[STATEMENT]
lemma has_field_compP [simp]: "(compP f P \<turnstile> C has F,b:T in D) = (P \<turnstile> C has F,b:T in D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compP f P \<turnstile> C has F,b:T in D) = (P \<turnstile> C has F,b:T in D)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compP f P \<turnstile> C has F,b:T in D) = (P \<turnstile> C has F,b:T in D)
[PROOF STEP]
by(simp add:has_field_def)


[STATEMENT]
lemma test_comp_mult2 [simp]: "test p \<Longrightarrow> p \<cdot> !p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test p \<Longrightarrow> p \<cdot> !p = (0::'a)
[PROOF STEP]
using local.test_mult_comp
[PROOF STATE]
proof (prove)
using this:
!?x \<cdot> t ?x = (0::'a)

goal (1 subgoal):
 1. test p \<Longrightarrow> p \<cdot> !p = (0::'a)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma test_add_distr: "test p \<Longrightarrow> test q \<Longrightarrow> test r \<Longrightarrow> p + q \<cdot> r = (p + q) \<cdot> (p + r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test p; test q; test r\<rbrakk> \<Longrightarrow> p + q \<cdot> r = (p + q) \<cdot> (p + r)
[PROOF STEP]
using n_add_distr
[PROOF STATE]
proof (prove)
using this:
!?x + !?y \<cdot> !?z = (!?x + !?y) \<cdot> (!?x + !?z)

goal (1 subgoal):
 1. \<lbrakk>test p; test q; test r\<rbrakk> \<Longrightarrow> p + q \<cdot> r = (p + q) \<cdot> (p + r)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma sorted_list_subset_correct:
  "\<lbrakk> sorted xs; distinct xs; sorted ys; distinct ys \<rbrakk>
  \<Longrightarrow> sorted_list_subset (=) xs ys \<longleftrightarrow> set xs \<subseteq> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> sorted_list_subset (=) xs ys = (set xs \<subseteq> set ys)
[PROOF STEP]
apply(induct "(=) :: 'a \<Rightarrow> 'a \<Rightarrow> bool" xs ys rule: sorted_list_subset.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ys. \<lbrakk>sorted []; distinct []; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> sorted_list_subset (=) [] ys = (set [] \<subseteq> set ys)
 2. \<And>x xs. \<lbrakk>sorted (x # xs); distinct (x # xs); sorted []; distinct []\<rbrakk> \<Longrightarrow> sorted_list_subset (=) (x # xs) [] = (set (x # xs) \<subseteq> set [])
 3. \<And>x xs y ys. \<lbrakk>\<lbrakk>x = y; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> sorted_list_subset (=) xs ys = (set xs \<subseteq> set ys); \<lbrakk>x \<noteq> y; sorted (x # xs); distinct (x # xs); sorted ys; distinct ys\<rbrakk> \<Longrightarrow> sorted_list_subset (=) (x # xs) ys = (set (x # xs) \<subseteq> set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> sorted_list_subset (=) (x # xs) (y # ys) = (set (x # xs) \<subseteq> set (y # ys))
[PROOF STEP]
apply(auto 6 2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x xs y ys xa. \<lbrakk>\<forall>xa\<in>set xs. x \<le> xa; sorted xs; x \<notin> set xs; distinct xs; \<forall>x\<in>set ys. y \<le> x; sorted ys; y \<notin> set ys; distinct ys; x \<noteq> y; x \<in> set ys; set xs \<subseteq> insert y (set ys); xa \<in> set xs; sorted_list_subset (=) (x # xs) ys; set xs \<subseteq> set ys\<rbrakk> \<Longrightarrow> xa \<in> set ys
 2. \<And>x xs y ys xa xb. \<lbrakk>\<forall>xa\<in>set xs. x \<le> xa; sorted xs; x \<notin> set xs; distinct xs; \<forall>x\<in>set ys. y \<le> x; sorted ys; y \<notin> set ys; distinct ys; x \<noteq> y; x \<in> set ys; set xs \<subseteq> insert y (set ys); xa \<in> set xs; \<not> sorted_list_subset (=) (x # xs) ys; xa \<notin> set ys; xb \<in> set xs\<rbrakk> \<Longrightarrow> xb \<in> set ys
[PROOF STEP]
using order_antisym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?x\<rbrakk> \<Longrightarrow> ?x = ?y

goal (2 subgoals):
 1. \<And>x xs y ys xa. \<lbrakk>\<forall>xa\<in>set xs. x \<le> xa; sorted xs; x \<notin> set xs; distinct xs; \<forall>x\<in>set ys. y \<le> x; sorted ys; y \<notin> set ys; distinct ys; x \<noteq> y; x \<in> set ys; set xs \<subseteq> insert y (set ys); xa \<in> set xs; sorted_list_subset (=) (x # xs) ys; set xs \<subseteq> set ys\<rbrakk> \<Longrightarrow> xa \<in> set ys
 2. \<And>x xs y ys xa xb. \<lbrakk>\<forall>xa\<in>set xs. x \<le> xa; sorted xs; x \<notin> set xs; distinct xs; \<forall>x\<in>set ys. y \<le> x; sorted ys; y \<notin> set ys; distinct ys; x \<noteq> y; x \<in> set ys; set xs \<subseteq> insert y (set ys); xa \<in> set xs; \<not> sorted_list_subset (=) (x # xs) ys; xa \<notin> set ys; xb \<in> set xs\<rbrakk> \<Longrightarrow> xb \<in> set ys
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma econc_fun_ESPEC: "\<Down>\<^sub>E E R (ESPEC \<Phi> \<Psi>) = ESPEC (\<lambda>ei. \<exists>e. (ei,e)\<in>E \<and> \<Phi> e) (\<lambda>ri. \<exists>r. (ri,r)\<in>R \<and> \<Psi> r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Down>\<^sub>E E R (ESPEC \<Phi> \<Psi>) = ESPEC (\<lambda>ei. \<exists>e. (ei, e) \<in> E \<and> \<Phi> e) (\<lambda>ri. \<exists>r. (ri, r) \<in> R \<and> \<Psi> r)
[PROOF STEP]
by (auto simp: pw_eeq_iff refine_pw_simps)


[STATEMENT]
lemma dot\<^sub>O\<^sub>c\<^sub>l\<^sub>A\<^sub>n\<^sub>y\<A>\<N>\<Y>_strict [simp] : "(invalid).any = invalid"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (invalid.any) = invalid
[PROOF STEP]
by(rule ext, simp add: dot_accessor null_fun_def null_option_def bot_option_def null_def invalid_def)


[STATEMENT]
lemma is_volatile_Write\<^sub>s\<^sub>b_simps [simp]:
"is_volatile_Write\<^sub>s\<^sub>b (Write\<^sub>s\<^sub>b volatile a sop v A L R W) = volatile"
"is_volatile_Write\<^sub>s\<^sub>b (Read\<^sub>s\<^sub>b volatile a t v) = False"
"is_volatile_Write\<^sub>s\<^sub>b (Prog\<^sub>s\<^sub>b p p' is) = False"
"is_volatile_Write\<^sub>s\<^sub>b (Ghost\<^sub>s\<^sub>b A L R W) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_volatile_Write\<^sub>s\<^sub>b (Write\<^sub>s\<^sub>b volatile a sop v A L R W) = volatile &&& is_volatile_Write\<^sub>s\<^sub>b (Read\<^sub>s\<^sub>b volatile a t v) = False) &&& is_volatile_Write\<^sub>s\<^sub>b (Prog\<^sub>s\<^sub>b p p' is) = False &&& is_volatile_Write\<^sub>s\<^sub>b (Ghost\<^sub>s\<^sub>b A L R W) = False
[PROOF STEP]
by (auto simp add: is_volatile_Write\<^sub>s\<^sub>b_def)


[STATEMENT]
lemma share_read_only_mono: "\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow>
        read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>')
[PROOF STEP]
proof (induct sb)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share [] \<S>) \<subseteq> read_only (share [] \<S>')
 2. \<And>a sb \<S> \<S>'. \<lbrakk>\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>'); read_only \<S> \<subseteq> read_only \<S>'\<rbrakk> \<Longrightarrow> read_only (share (a # sb) \<S>) \<subseteq> read_only (share (a # sb) \<S>')
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
read_only \<S> \<subseteq> read_only \<S>'

goal (2 subgoals):
 1. \<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share [] \<S>) \<subseteq> read_only (share [] \<S>')
 2. \<And>a sb \<S> \<S>'. \<lbrakk>\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>'); read_only \<S> \<subseteq> read_only \<S>'\<rbrakk> \<Longrightarrow> read_only (share (a # sb) \<S>) \<subseteq> read_only (share (a # sb) \<S>')
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
read_only \<S> \<subseteq> read_only \<S>'

goal (1 subgoal):
 1. read_only (share [] \<S>) \<subseteq> read_only (share [] \<S>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
read_only (share [] \<S>) \<subseteq> read_only (share [] \<S>')

goal (1 subgoal):
 1. \<And>a sb \<S> \<S>'. \<lbrakk>\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>'); read_only \<S> \<subseteq> read_only \<S>'\<rbrakk> \<Longrightarrow> read_only (share (a # sb) \<S>) \<subseteq> read_only (share (a # sb) \<S>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a sb \<S> \<S>'. \<lbrakk>\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>'); read_only \<S> \<subseteq> read_only \<S>'\<rbrakk> \<Longrightarrow> read_only (share (a # sb) \<S>) \<subseteq> read_only (share (a # sb) \<S>')
[PROOF STEP]
case (Cons x sb)
[PROOF STATE]
proof (state)
this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'

goal (1 subgoal):
 1. \<And>a sb \<S> \<S>'. \<lbrakk>\<And>\<S> \<S>'. read_only \<S> \<subseteq> read_only \<S>' \<Longrightarrow> read_only (share sb \<S>) \<subseteq> read_only (share sb \<S>'); read_only \<S> \<subseteq> read_only \<S>'\<rbrakk> \<Longrightarrow> read_only (share (a # sb) \<S>) \<subseteq> read_only (share (a # sb) \<S>')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
proof (cases x)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18. x = Write\<^sub>s\<^sub>b x11 x12 x13 x14 x15 x16 x17 x18 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x21 x22 x23 x24. x = Read\<^sub>s\<^sub>b x21 x22 x23 x24 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 3. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 4. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case (Write\<^sub>s\<^sub>b volatile a sop v A L R W)
[PROOF STATE]
proof (state)
this:
x = Write\<^sub>s\<^sub>b volatile a sop v A L R W

goal (4 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18. x = Write\<^sub>s\<^sub>b x11 x12 x13 x14 x15 x16 x17 x18 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x21 x22 x23 x24. x = Read\<^sub>s\<^sub>b x21 x22 x23 x24 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 3. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 4. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
proof (cases volatile)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<not> volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> volatile

goal (2 subgoals):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<not> volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
with Cons Write\<^sub>s\<^sub>b
[PROOF STATE]
proof (chain)
picking this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Write\<^sub>s\<^sub>b volatile a sop v A L R W
\<not> volatile
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Write\<^sub>s\<^sub>b volatile a sop v A L R W
\<not> volatile

goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
volatile

goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
note \<open>read_only \<S> \<subseteq> read_only \<S>'\<close>
[PROOF STATE]
proof (state)
this:
read_only \<S> \<subseteq> read_only \<S>'

goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from augment_read_only_mono [OF this]
[PROOF STATE]
proof (chain)
picking this:
read_only (\<S> \<oplus>\<^bsub>?W\<^esub> ?R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>?W\<^esub> ?R)
[PROOF STEP]
have "read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)"
[PROOF STATE]
proof (prove)
using this:
read_only (\<S> \<oplus>\<^bsub>?W\<^esub> ?R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>?W\<^esub> ?R)

goal (1 subgoal):
 1. read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)

goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from restrict_read_only_mono [OF this, of A L]
[PROOF STATE]
proof (chain)
picking this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)
[PROOF STEP]
have "read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)"
[PROOF STATE]
proof (prove)
using this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)

goal (1 subgoal):
 1. read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)

goal (1 subgoal):
 1. volatile \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from Cons.hyps [OF this]
[PROOF STATE]
proof (chain)
picking this:
read_only (share sb (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)) \<subseteq> read_only (share sb (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
read_only (share sb (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)) \<subseteq> read_only (share sb (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L))

goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
by (clarsimp simp add: Write\<^sub>s\<^sub>b True)
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal (3 subgoals):
 1. \<And>x21 x22 x23 x24. x = Read\<^sub>s\<^sub>b x21 x22 x23 x24 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 3. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x21 x22 x23 x24. x = Read\<^sub>s\<^sub>b x21 x22 x23 x24 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 3. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case Read\<^sub>s\<^sub>b
[PROOF STATE]
proof (state)
this:
x = Read\<^sub>s\<^sub>b x21_ x22_ x23_ x24_

goal (3 subgoals):
 1. \<And>x21 x22 x23 x24. x = Read\<^sub>s\<^sub>b x21 x22 x23 x24 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 3. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Read\<^sub>s\<^sub>b x21_ x22_ x23_ x24_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Read\<^sub>s\<^sub>b x21_ x22_ x23_ x24_

goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal (2 subgoals):
 1. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case Prog\<^sub>s\<^sub>b
[PROOF STATE]
proof (state)
this:
x = Prog\<^sub>s\<^sub>b x31_ x32_ x33_

goal (2 subgoals):
 1. \<And>x31 x32 x33. x = Prog\<^sub>s\<^sub>b x31 x32 x33 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
 2. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Prog\<^sub>s\<^sub>b x31_ x32_ x33_
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
read_only ?\<S> \<subseteq> read_only ?\<S>' \<Longrightarrow> read_only (share sb ?\<S>) \<subseteq> read_only (share sb ?\<S>')
read_only \<S> \<subseteq> read_only \<S>'
x = Prog\<^sub>s\<^sub>b x31_ x32_ x33_

goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
case (Ghost\<^sub>s\<^sub>b A L R W)
[PROOF STATE]
proof (state)
this:
x = Ghost\<^sub>s\<^sub>b A L R W

goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
note \<open>read_only \<S> \<subseteq> read_only \<S>'\<close>
[PROOF STATE]
proof (state)
this:
read_only \<S> \<subseteq> read_only \<S>'

goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from augment_read_only_mono [OF this]
[PROOF STATE]
proof (chain)
picking this:
read_only (\<S> \<oplus>\<^bsub>?W\<^esub> ?R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>?W\<^esub> ?R)
[PROOF STEP]
have "read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)"
[PROOF STATE]
proof (prove)
using this:
read_only (\<S> \<oplus>\<^bsub>?W\<^esub> ?R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>?W\<^esub> ?R)

goal (1 subgoal):
 1. read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R)

goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from restrict_read_only_mono [OF this, of A L]
[PROOF STATE]
proof (chain)
picking this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)
[PROOF STEP]
have "read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)"
[PROOF STATE]
proof (prove)
using this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)

goal (1 subgoal):
 1. read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
read_only (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L) \<subseteq> read_only (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)

goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. x = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44 \<Longrightarrow> read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
from Cons.hyps [OF this]
[PROOF STATE]
proof (chain)
picking this:
read_only (share sb (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)) \<subseteq> read_only (share sb (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
read_only (share sb (\<S> \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L)) \<subseteq> read_only (share sb (\<S>' \<oplus>\<^bsub>W\<^esub> R \<ominus>\<^bsub>A\<^esub> L))

goal (1 subgoal):
 1. read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')
[PROOF STEP]
by (clarsimp simp add: Ghost\<^sub>s\<^sub>b)
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
read_only (share (x # sb) \<S>) \<subseteq> read_only (share (x # sb) \<S>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_shared_acquired_or_owned:
  "\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb \<Longrightarrow> all_shared sb \<subseteq> all_acquired sb \<union> \<O>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<S> \<O>. sharing_consistent \<S> \<O> sb \<Longrightarrow> all_shared sb \<subseteq> all_acquired sb \<union> \<O>
[PROOF STEP]
apply (induct sb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<S> \<O>. sharing_consistent \<S> \<O> [] \<Longrightarrow> all_shared [] \<subseteq> all_acquired [] \<union> \<O>
 2. \<And>a sb \<S> \<O>. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb \<Longrightarrow> all_shared sb \<subseteq> all_acquired sb \<union> \<O>; sharing_consistent \<S> \<O> (a # sb)\<rbrakk> \<Longrightarrow> all_shared (a # sb) \<subseteq> all_acquired (a # sb) \<union> \<O>
[PROOF STEP]
apply  simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a sb \<S> \<O>. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb \<Longrightarrow> all_shared sb \<subseteq> all_acquired sb \<union> \<O>; sharing_consistent \<S> \<O> (a # sb)\<rbrakk> \<Longrightarrow> all_shared (a # sb) \<subseteq> all_acquired (a # sb) \<union> \<O>
[PROOF STEP]
subgoal for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb_ \<Longrightarrow> all_shared sb_ \<subseteq> all_acquired sb_ \<union> \<O>; sharing_consistent \<S>_ \<O>_ (a # sb_)\<rbrakk> \<Longrightarrow> all_shared (a # sb_) \<subseteq> all_acquired (a # sb_) \<union> \<O>_
[PROOF STEP]
apply (case_tac a)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x17 x18. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb_ \<Longrightarrow> all_shared sb_ \<subseteq> all_acquired sb_ \<union> \<O>; sharing_consistent \<S>_ \<O>_ (a # sb_); a = Write\<^sub>s\<^sub>b x11 x12 x13 x14 x15 x16 x17 x18\<rbrakk> \<Longrightarrow> all_shared (a # sb_) \<subseteq> all_acquired (a # sb_) \<union> \<O>_
 2. \<And>x21 x22 x23 x24. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb_ \<Longrightarrow> all_shared sb_ \<subseteq> all_acquired sb_ \<union> \<O>; sharing_consistent \<S>_ \<O>_ (a # sb_); a = Read\<^sub>s\<^sub>b x21 x22 x23 x24\<rbrakk> \<Longrightarrow> all_shared (a # sb_) \<subseteq> all_acquired (a # sb_) \<union> \<O>_
 3. \<And>x31 x32 x33. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb_ \<Longrightarrow> all_shared sb_ \<subseteq> all_acquired sb_ \<union> \<O>; sharing_consistent \<S>_ \<O>_ (a # sb_); a = Prog\<^sub>s\<^sub>b x31 x32 x33\<rbrakk> \<Longrightarrow> all_shared (a # sb_) \<subseteq> all_acquired (a # sb_) \<union> \<O>_
 4. \<And>x41 x42 x43 x44. \<lbrakk>\<And>\<S> \<O>. sharing_consistent \<S> \<O> sb_ \<Longrightarrow> all_shared sb_ \<subseteq> all_acquired sb_ \<union> \<O>; sharing_consistent \<S>_ \<O>_ (a # sb_); a = Ghost\<^sub>s\<^sub>b x41 x42 x43 x44\<rbrakk> \<Longrightarrow> all_shared (a # sb_) \<subseteq> all_acquired (a # sb_) \<union> \<O>_
[PROOF STEP]
apply auto+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma epath_decompose:
  assumes e: "epath G v p v'"
    and elem :"Upair a b \<in> set p"
  shows  "\<exists> u u' p' p'' . u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and>
          length p' < length p \<and> length p'' < length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
from elem
[PROOF STATE]
proof (chain)
picking this:
Upair a b \<in> set p
[PROOF STEP]
obtain p' p'' where p: "p = p' @ (Upair a b) # p''"
[PROOF STATE]
proof (prove)
using this:
Upair a b \<in> set p

goal (1 subgoal):
 1. (\<And>p' p''. p = p' @ Upair a b # p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_decomp
[PROOF STATE]
proof (prove)
using this:
Upair a b \<in> set p
(?x \<in> set ?xs) = (\<exists>ys zs. ?xs = ys @ ?x # zs)

goal (1 subgoal):
 1. (\<And>p' p''. p = p' @ Upair a b # p'' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
p = p' @ Upair a b # p''

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p = p' @ Upair a b # p''
[PROOF STEP]
have "epath G v (p' @ (Upair a b) # p'') v'"
[PROOF STATE]
proof (prove)
using this:
p = p' @ Upair a b # p''

goal (1 subgoal):
 1. epath G v (p' @ Upair a b # p'') v'
[PROOF STEP]
using e
[PROOF STATE]
proof (prove)
using this:
p = p' @ Upair a b # p''
epath G v p v'

goal (1 subgoal):
 1. epath G v (p' @ Upair a b # p'') v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
epath G v (p' @ Upair a b # p'') v'

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
epath G v (p' @ Upair a b # p'') v'
[PROOF STEP]
obtain z z' where pr: "epath G v p' z"  "epath G z' p'' v'" and u: "Upair z z'=Upair a b"
[PROOF STATE]
proof (prove)
using this:
epath G v (p' @ Upair a b # p'') v'

goal (1 subgoal):
 1. (\<And>z z'. \<lbrakk>epath G v p' z; epath G z' p'' v'; Upair z z' = Upair a b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
epath G v p' z
epath G z' p'' v'
Upair z z' = Upair a b

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
from u
[PROOF STATE]
proof (chain)
picking this:
Upair z z' = Upair a b
[PROOF STEP]
have u': "z \<in> {a, b} \<and> z' \<in> {a, b}"
[PROOF STATE]
proof (prove)
using this:
Upair z z' = Upair a b

goal (1 subgoal):
 1. z \<in> {a, b} \<and> z' \<in> {a, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> {a, b} \<and> z' \<in> {a, b}

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
have len: "length p' < length p"  "length p'' < length p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length p' < length p &&& length p'' < length p
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
p = p' @ Upair a b # p''

goal (1 subgoal):
 1. length p' < length p &&& length p'' < length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length p' < length p
length p'' < length p

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
from len pr u'
[PROOF STATE]
proof (chain)
picking this:
length p' < length p
length p'' < length p
epath G v p' z
epath G z' p'' v'
z \<in> {a, b} \<and> z' \<in> {a, b}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
length p' < length p
length p'' < length p
epath G v p' z
epath G z' p'' v'
z \<in> {a, b} \<and> z' \<in> {a, b}

goal (1 subgoal):
 1. \<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>u u' p' p''. u \<in> {a, b} \<and> u' \<in> {a, b} \<and> epath G v p' u \<and> epath G u' p'' v' \<and> length p' < length p \<and> length p'' < length p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma polynate_norm[simp]:
  fixes p :: "'a::field poly"
  shows "isnpoly (polynate p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isnpoly (polynate p)
[PROOF STEP]
by (induct p rule: polynate.induct)
     (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm,
      simp_all add: isnpoly_def)


[STATEMENT]
lemma behead:
  assumes "isnpolyh p n"
  shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) =
    (Ipoly bs p :: 'a :: comm_ring_1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
isnpolyh p n

goal (1 subgoal):
 1. Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
[PROOF STEP]
proof (induct p arbitrary: n rule: behead.induct)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>c p n. \<lbrakk>\<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; isnpolyh (CN c 0 p) n\<rbrakk> \<Longrightarrow> Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
 2. \<And>v n. isnpolyh (v)\<^sub>p n \<Longrightarrow> Ipoly bs (Add (Mul (head (v)\<^sub>p) (Pw (Bound 0) (Polynomial_Expression.degree (v)\<^sub>p))) (behead (v)\<^sub>p)) = Ipoly bs (v)\<^sub>p
 3. \<And>v n. isnpolyh (Bound v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Bound v)) (Pw (Bound 0) (Polynomial_Expression.degree (Bound v)))) (behead (Bound v))) = Ipoly bs (Bound v)
 4. \<And>v va n. isnpolyh (Add v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Add v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Add v va)))) (behead (Add v va))) = Ipoly bs (Add v va)
 5. \<And>v va n. isnpolyh (Sub v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Sub v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Sub v va)))) (behead (Sub v va))) = Ipoly bs (Sub v va)
 6. \<And>v va n. isnpolyh (Mul v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Mul v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Mul v va)))) (behead (Mul v va))) = Ipoly bs (Mul v va)
 7. \<And>v n. isnpolyh (Neg v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Neg v)) (Pw (Bound 0) (Polynomial_Expression.degree (Neg v)))) (behead (Neg v))) = Ipoly bs (Neg v)
 8. \<And>v va n. isnpolyh (Pw v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Pw v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Pw v va)))) (behead (Pw v va))) = Ipoly bs (Pw v va)
 9. \<And>v vc vb n. isnpolyh (CN v (Suc vc) vb) n \<Longrightarrow> Ipoly bs (Add (Mul (head (CN v (Suc vc) vb)) (Pw (Bound 0) (Polynomial_Expression.degree (CN v (Suc vc) vb)))) (behead (CN v (Suc vc) vb))) = Ipoly bs (CN v (Suc vc) vb)
[PROOF STEP]
case (1 c p n)
[PROOF STATE]
proof (state)
this:
isnpolyh p ?n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
isnpolyh (CN c 0 p) n

goal (9 subgoals):
 1. \<And>c p n. \<lbrakk>\<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; isnpolyh (CN c 0 p) n\<rbrakk> \<Longrightarrow> Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
 2. \<And>v n. isnpolyh (v)\<^sub>p n \<Longrightarrow> Ipoly bs (Add (Mul (head (v)\<^sub>p) (Pw (Bound 0) (Polynomial_Expression.degree (v)\<^sub>p))) (behead (v)\<^sub>p)) = Ipoly bs (v)\<^sub>p
 3. \<And>v n. isnpolyh (Bound v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Bound v)) (Pw (Bound 0) (Polynomial_Expression.degree (Bound v)))) (behead (Bound v))) = Ipoly bs (Bound v)
 4. \<And>v va n. isnpolyh (Add v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Add v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Add v va)))) (behead (Add v va))) = Ipoly bs (Add v va)
 5. \<And>v va n. isnpolyh (Sub v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Sub v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Sub v va)))) (behead (Sub v va))) = Ipoly bs (Sub v va)
 6. \<And>v va n. isnpolyh (Mul v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Mul v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Mul v va)))) (behead (Mul v va))) = Ipoly bs (Mul v va)
 7. \<And>v n. isnpolyh (Neg v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Neg v)) (Pw (Bound 0) (Polynomial_Expression.degree (Neg v)))) (behead (Neg v))) = Ipoly bs (Neg v)
 8. \<And>v va n. isnpolyh (Pw v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Pw v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Pw v va)))) (behead (Pw v va))) = Ipoly bs (Pw v va)
 9. \<And>v vc vb n. isnpolyh (CN v (Suc vc) vb) n \<Longrightarrow> Ipoly bs (Add (Mul (head (CN v (Suc vc) vb)) (Pw (Bound 0) (Polynomial_Expression.degree (CN v (Suc vc) vb)))) (behead (CN v (Suc vc) vb))) = Ipoly bs (CN v (Suc vc) vb)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
isnpolyh p ?n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
isnpolyh (CN c 0 p) n
[PROOF STEP]
have pn: "isnpolyh p n"
[PROOF STATE]
proof (prove)
using this:
isnpolyh p ?n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
isnpolyh (CN c 0 p) n

goal (1 subgoal):
 1. isnpolyh p n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
isnpolyh p n

goal (9 subgoals):
 1. \<And>c p n. \<lbrakk>\<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; isnpolyh (CN c 0 p) n\<rbrakk> \<Longrightarrow> Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
 2. \<And>v n. isnpolyh (v)\<^sub>p n \<Longrightarrow> Ipoly bs (Add (Mul (head (v)\<^sub>p) (Pw (Bound 0) (Polynomial_Expression.degree (v)\<^sub>p))) (behead (v)\<^sub>p)) = Ipoly bs (v)\<^sub>p
 3. \<And>v n. isnpolyh (Bound v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Bound v)) (Pw (Bound 0) (Polynomial_Expression.degree (Bound v)))) (behead (Bound v))) = Ipoly bs (Bound v)
 4. \<And>v va n. isnpolyh (Add v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Add v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Add v va)))) (behead (Add v va))) = Ipoly bs (Add v va)
 5. \<And>v va n. isnpolyh (Sub v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Sub v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Sub v va)))) (behead (Sub v va))) = Ipoly bs (Sub v va)
 6. \<And>v va n. isnpolyh (Mul v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Mul v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Mul v va)))) (behead (Mul v va))) = Ipoly bs (Mul v va)
 7. \<And>v n. isnpolyh (Neg v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Neg v)) (Pw (Bound 0) (Polynomial_Expression.degree (Neg v)))) (behead (Neg v))) = Ipoly bs (Neg v)
 8. \<And>v va n. isnpolyh (Pw v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Pw v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Pw v va)))) (behead (Pw v va))) = Ipoly bs (Pw v va)
 9. \<And>v vc vb n. isnpolyh (CN v (Suc vc) vb) n \<Longrightarrow> Ipoly bs (Add (Mul (head (CN v (Suc vc) vb)) (Pw (Bound 0) (Polynomial_Expression.degree (CN v (Suc vc) vb)))) (behead (CN v (Suc vc) vb))) = Ipoly bs (CN v (Suc vc) vb)
[PROOF STEP]
from 1(1)[OF pn]
[PROOF STATE]
proof (chain)
picking this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
[PROOF STEP]
have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p"
[PROOF STATE]
proof (prove)
using this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p

goal (1 subgoal):
 1. Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p

goal (9 subgoals):
 1. \<And>c p n. \<lbrakk>\<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; isnpolyh (CN c 0 p) n\<rbrakk> \<Longrightarrow> Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
 2. \<And>v n. isnpolyh (v)\<^sub>p n \<Longrightarrow> Ipoly bs (Add (Mul (head (v)\<^sub>p) (Pw (Bound 0) (Polynomial_Expression.degree (v)\<^sub>p))) (behead (v)\<^sub>p)) = Ipoly bs (v)\<^sub>p
 3. \<And>v n. isnpolyh (Bound v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Bound v)) (Pw (Bound 0) (Polynomial_Expression.degree (Bound v)))) (behead (Bound v))) = Ipoly bs (Bound v)
 4. \<And>v va n. isnpolyh (Add v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Add v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Add v va)))) (behead (Add v va))) = Ipoly bs (Add v va)
 5. \<And>v va n. isnpolyh (Sub v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Sub v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Sub v va)))) (behead (Sub v va))) = Ipoly bs (Sub v va)
 6. \<And>v va n. isnpolyh (Mul v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Mul v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Mul v va)))) (behead (Mul v va))) = Ipoly bs (Mul v va)
 7. \<And>v n. isnpolyh (Neg v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Neg v)) (Pw (Bound 0) (Polynomial_Expression.degree (Neg v)))) (behead (Neg v))) = Ipoly bs (Neg v)
 8. \<And>v va n. isnpolyh (Pw v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Pw v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Pw v va)))) (behead (Pw v va))) = Ipoly bs (Pw v va)
 9. \<And>v vc vb n. isnpolyh (CN v (Suc vc) vb) n \<Longrightarrow> Ipoly bs (Add (Mul (head (CN v (Suc vc) vb)) (Pw (Bound 0) (Polynomial_Expression.degree (CN v (Suc vc) vb)))) (behead (CN v (Suc vc) vb))) = Ipoly bs (CN v (Suc vc) vb)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p

goal (1 subgoal):
 1. Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
[PROOF STEP]
using "1.hyps"
[PROOF STATE]
proof (prove)
using this:
Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p
isnpolyh p ?n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p

goal (1 subgoal):
 1. Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)
[PROOF STEP]
apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Ipoly bs (head p) * bs ! 0 ^ Polynomial_Expression.degree p + Ipoly bs (behead p) = Ipoly bs p; Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; \<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; behead p = 0\<^sub>p\<rbrakk> \<Longrightarrow> (behead p = 0\<^sub>p \<longrightarrow> Ipoly bs (head p) * (bs ! 0 * bs ! 0 ^ Polynomial_Expression.degree p) = bs ! 0 * Ipoly bs p) \<and> (behead p \<noteq> 0\<^sub>p \<longrightarrow> Ipoly bs (head p) * (bs ! 0 * bs ! 0 ^ Polynomial_Expression.degree p) + bs ! 0 * Ipoly bs (behead p) = bs ! 0 * Ipoly bs p)
 2. \<lbrakk>Ipoly bs (head p) * bs ! 0 ^ Polynomial_Expression.degree p + Ipoly bs (behead p) = Ipoly bs p; Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; \<And>n. isnpolyh p n \<Longrightarrow> Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (Polynomial_Expression.degree p))) (behead p)) = Ipoly bs p; behead p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> (behead p = 0\<^sub>p \<longrightarrow> Ipoly bs (head p) * (bs ! 0 * bs ! 0 ^ Polynomial_Expression.degree p) = bs ! 0 * Ipoly bs p) \<and> (behead p \<noteq> 0\<^sub>p \<longrightarrow> Ipoly bs (head p) * (bs ! 0 * bs ! 0 ^ Polynomial_Expression.degree p) + bs ! 0 * Ipoly bs (behead p) = bs ! 0 * Ipoly bs p)
[PROOF STEP]
apply (simp_all add: th[symmetric] field_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
Ipoly bs (Add (Mul (head (CN c 0 p)) (Pw (Bound 0) (Polynomial_Expression.degree (CN c 0 p)))) (behead (CN c 0 p))) = Ipoly bs (CN c 0 p)

goal (8 subgoals):
 1. \<And>v n. isnpolyh (v)\<^sub>p n \<Longrightarrow> Ipoly bs (Add (Mul (head (v)\<^sub>p) (Pw (Bound 0) (Polynomial_Expression.degree (v)\<^sub>p))) (behead (v)\<^sub>p)) = Ipoly bs (v)\<^sub>p
 2. \<And>v n. isnpolyh (Bound v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Bound v)) (Pw (Bound 0) (Polynomial_Expression.degree (Bound v)))) (behead (Bound v))) = Ipoly bs (Bound v)
 3. \<And>v va n. isnpolyh (Add v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Add v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Add v va)))) (behead (Add v va))) = Ipoly bs (Add v va)
 4. \<And>v va n. isnpolyh (Sub v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Sub v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Sub v va)))) (behead (Sub v va))) = Ipoly bs (Sub v va)
 5. \<And>v va n. isnpolyh (Mul v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Mul v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Mul v va)))) (behead (Mul v va))) = Ipoly bs (Mul v va)
 6. \<And>v n. isnpolyh (Neg v) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Neg v)) (Pw (Bound 0) (Polynomial_Expression.degree (Neg v)))) (behead (Neg v))) = Ipoly bs (Neg v)
 7. \<And>v va n. isnpolyh (Pw v va) n \<Longrightarrow> Ipoly bs (Add (Mul (head (Pw v va)) (Pw (Bound 0) (Polynomial_Expression.degree (Pw v va)))) (behead (Pw v va))) = Ipoly bs (Pw v va)
 8. \<And>v vc vb n. isnpolyh (CN v (Suc vc) vb) n \<Longrightarrow> Ipoly bs (Add (Mul (head (CN v (Suc vc) vb)) (Pw (Bound 0) (Polynomial_Expression.degree (CN v (Suc vc) vb)))) (behead (CN v (Suc vc) vb))) = Ipoly bs (CN v (Suc vc) vb)
[PROOF STEP]
qed (auto simp add: Let_def)


[STATEMENT]
lemma A2_DAcc_level0: "DAcc level0 sA2 = { sA3 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DAcc level0 sA2 = {sA3}
[PROOF STEP]
by (simp add: DAcc_def  AbstrLevel0, force)


[STATEMENT]
lemma l2_commutative: "l2_\<phi> p q = l2_\<phi> q p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l2_\<phi> p q = l2_\<phi> q p
[PROOF STEP]
by (simp add: l2_\<phi>_def mult.commute)


[STATEMENT]
lemma echelon_form_upt_k_condition2:
  assumes "echelon_form_upt_k A k" "i<j"
  and  "\<not> (is_zero_row_upt_k i k A)" "\<not> (is_zero_row_upt_k j k A)"
  shows "(LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ j $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
echelon_form_upt_k A k
i < j
\<not> is_zero_row_upt_k i k A
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
unfolding echelon_form_upt_k_def
[PROOF STATE]
proof (prove)
using this:
(\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)) \<and> (\<forall>i j. i < j \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k j k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a)))
i < j
\<not> is_zero_row_upt_k i k A
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma bezout_iterate_not_zero:
  assumes Aik_0: "A $ i $ from_nat k \<noteq> 0"
  and n: "n<nrows A"
  and a: "to_nat i \<le> n"
  and ib: "is_bezout_ext bezout"
  shows "bezout_iterate A n i (from_nat k) bezout $ i $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using Aik_0 n a
[PROOF STATE]
proof (prove)
using this:
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
n < nrows A
mod_type_class.to_nat i \<le> n

goal (1 subgoal):
 1. bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
proof (induct n arbitrary: A)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); 0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
0 < nrows A
mod_type_class.to_nat i \<le> 0

goal (2 subgoals):
 1. \<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); 0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
have "to_nat i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i = 0
[PROOF STEP]
by (metis "0.prems"(3) le_0_eq)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i = 0

goal (2 subgoals):
 1. \<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); 0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
hence i0: "i=0"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i = 0

goal (1 subgoal):
 1. i = (0::'c)
[PROOF STEP]
by (metis to_nat_eq_0)
[PROOF STATE]
proof (state)
this:
i = (0::'c)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); 0 < nrows A; mod_type_class.to_nat i \<le> 0\<rbrakk> \<Longrightarrow> bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using "0.prems"(1)
[PROOF STATE]
proof (prove)
using this:
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
unfolding i0
[PROOF STATE]
proof (prove)
using this:
A $ (0::'c) $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. bezout_iterate A 0 (0::'c) (mod_type_class.from_nat k) bezout $ (0::'c) $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bezout_iterate A 0 i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows ?A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate ?A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
Suc n < nrows A
mod_type_class.to_nat i \<le> Suc n

goal (1 subgoal):
 1. \<And>n A. \<lbrakk>\<And>A. \<lbrakk>A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); n < nrows A; mod_type_class.to_nat i \<le> n\<rbrakk> \<Longrightarrow> bezout_iterate A n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a); A $ i $ mod_type_class.from_nat k \<noteq> (0::'a); Suc n < nrows A; mod_type_class.to_nat i \<le> Suc n\<rbrakk> \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
proof (cases "Suc n = to_nat i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc n = mod_type_class.to_nat i

goal (2 subgoals):
 1. Suc n = mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
unfolding bezout_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
using True Suc.prems(1)
[PROOF STATE]
proof (prove)
using this:
Suc n = mod_type_class.to_nat i
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout) $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
let ?B="(bezout_matrix A i (from_nat (Suc n)) (from_nat k) bezout ** A)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
have i_le_n: "to_nat i < Suc n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i < Suc n
[PROOF STEP]
using Suc.prems(3) False
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i \<le> Suc n
Suc n \<noteq> mod_type_class.to_nat i

goal (1 subgoal):
 1. mod_type_class.to_nat i < Suc n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i < Suc n

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
have "bezout_iterate A (Suc n) i (from_nat k) bezout $ i $ from_nat k
      = bezout_iterate ?B n i (from_nat k) bezout $ i $ from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k = bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k
[PROOF STEP]
unfolding bezout_iterate.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout) $ i $ mod_type_class.from_nat k = bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k
[PROOF STEP]
using i_le_n
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < Suc n

goal (1 subgoal):
 1. (if Suc n \<le> mod_type_class.to_nat i then A else bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout) $ i $ mod_type_class.from_nat k = bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k = bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k = bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
have "... \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
proof (rule Suc.hyps, rule bezout_matrix_not_zero[OF ib])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. i \<noteq> mod_type_class.from_nat (Suc n)
 2. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 3. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A)
 4. mod_type_class.to_nat i \<le> n
[PROOF STEP]
show "i \<noteq> from_nat (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> mod_type_class.from_nat (Suc n)
[PROOF STEP]
by (metis False Suc.prems(2) nrows_def to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
i \<noteq> mod_type_class.from_nat (Suc n)

goal (3 subgoals):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
 2. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A)
 3. mod_type_class.to_nat i \<le> n
[PROOF STEP]
show "A $ i $ from_nat k \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
by (rule Suc.prems(1))
[PROOF STATE]
proof (state)
this:
A $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (2 subgoals):
 1. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A)
 2. mod_type_class.to_nat i \<le> n
[PROOF STEP]
show "n < nrows ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A)
[PROOF STEP]
by (metis Suc.prems(2) Suc_lessD nrows_def)
[PROOF STATE]
proof (state)
this:
n < nrows (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A)

goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> n
[PROOF STEP]
show "to_nat i \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> n
[PROOF STEP]
using i_le_n
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat i < Suc n

goal (1 subgoal):
 1. mod_type_class.to_nat i \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat i \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bezout_iterate (bezout_matrix A i (mod_type_class.from_nat (Suc n)) (mod_type_class.from_nat k) bezout ** A) n i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. Suc n \<noteq> mod_type_class.to_nat i \<Longrightarrow> bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal (1 subgoal):
 1. bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
bezout_iterate A (Suc n) i (mod_type_class.from_nat k) bezout $ i $ mod_type_class.from_nat k \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  wf_nodes_le: "wf {(y, x). nodes_le x y \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
have eq_set: "{(y, x). (sorted (rev y) \<and> sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y} =
                {(y, x). nodes_le x y \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y} = {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
by (unfold nodes_le_def) auto
[PROOF STATE]
proof (state)
this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y} = {(y, x). nodes_le x y \<and> x \<noteq> y}

goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
have "{(y, x). (sorted (rev y) \<and> sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y} =
        {(y, x). (sorted (rev y) \<and> sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y} = {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}
[PROOF STEP]
by (auto simp add:sorted_less_rev_set_unique)
[PROOF STATE]
proof (state)
this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y} = {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}

goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
from this wf_nodes_le_auxi
[PROOF STATE]
proof (chain)
picking this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y} = {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}
wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y}
[PROOF STEP]
have "wf {(y, x). (sorted (rev y) \<and> sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}"
[PROOF STATE]
proof (prove)
using this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y} = {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}
wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subset> set x) \<and> x \<noteq> y}

goal (1 subgoal):
 1. wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}
[PROOF STEP]
by (rule subst)
[PROOF STATE]
proof (state)
this:
wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}

goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
with eq_set
[PROOF STATE]
proof (chain)
picking this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y} = {(y, x). nodes_le x y \<and> x \<noteq> y}
wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y} = {(y, x). nodes_le x y \<and> x \<noteq> y}
wf {(y, x). (Sorted_Less.sorted (rev y) \<and> Sorted_Less.sorted (rev x) \<and> set y \<subseteq> set x) \<and> x \<noteq> y}

goal (1 subgoal):
 1. wf {(y, x). nodes_le x y \<and> x \<noteq> y}
[PROOF STEP]
by (rule subst)
[PROOF STATE]
proof (state)
this:
wf {(y, x). nodes_le x y \<and> x \<noteq> y}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_1_size[simp]:
  "1 = size_kdt kdt \<longleftrightarrow> (\<exists>p. kdt = Leaf p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1 = KD_Tree.size_kdt kdt) = (\<exists>p. kdt = Leaf p)
[PROOF STEP]
using eq_size_1
[PROOF STATE]
proof (prove)
using this:
(KD_Tree.size_kdt ?kdt = 1) = (\<exists>p. ?kdt = Leaf p)

goal (1 subgoal):
 1. (1 = KD_Tree.size_kdt kdt) = (\<exists>p. kdt = Leaf p)
[PROOF STEP]
by metis


[STATEMENT]
lemma A\<^sub>i\<^sub>v: "x\<cdot>(y\<cdot>z) \<cong> (x\<cdot>y)\<cdot>z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> (y \<cdot> z) \<cong> (x \<cdot> y) \<cdot> z
[PROOF STEP]
using A\<^sub>i\<^sub>i\<^sub>i
[PROOF STATE]
proof (prove)
using this:
?x \<cdot> (?y \<cdot> ?z) \<cong> (?x \<cdot> ?y) \<cdot> ?z

goal (1 subgoal):
 1. x \<cdot> (y \<cdot> z) \<cong> (x \<cdot> y) \<cdot> z
[PROOF STEP]
by blast


[STATEMENT]
lemma hextI: "\<forall>a C fs. h a = Some(C,fs) \<longrightarrow> (\<exists>fs'. h' a = Some(C,fs')) \<Longrightarrow> h \<unlhd> h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a C fs. h a = \<lfloor>(C, fs)\<rfloor> \<longrightarrow> (\<exists>fs'. h' a = \<lfloor>(C, fs')\<rfloor>) \<Longrightarrow> h \<unlhd> h'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a C fs. h a = \<lfloor>(C, fs)\<rfloor> \<longrightarrow> (\<exists>fs'. h' a = \<lfloor>(C, fs')\<rfloor>) \<Longrightarrow> h \<unlhd> h'
[PROOF STEP]
by(auto simp: hext_def)


[STATEMENT]
lemma bounded_clinear_inv:
  assumes [simp]: \<open>bounded_clinear f\<close>
  assumes b: \<open>b > 0\<close>
  assumes bound: \<open>\<And>x. norm (f x) \<ge> b * norm x\<close>
  assumes \<open>surj f\<close>
  shows \<open>bounded_clinear (inv f)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_clinear (inv f)
[PROOF STEP]
proof (rule bounded_clinear_intro)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
fix x y :: 'b and r :: complex
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
define x' y' where \<open>x' = inv f x\<close> and \<open>y' = inv f y\<close>
[PROOF STATE]
proof (state)
this:
x' = inv f x
y' = inv f y

goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
have [simp]: \<open>clinear f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear f
[PROOF STEP]
by (simp add: bounded_clinear.clinear)
[PROOF STATE]
proof (state)
this:
clinear f

goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
have [simp]: \<open>inj f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj f
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
assume \<open>f x = f y\<close>
[PROOF STATE]
proof (state)
this:
f x = f y

goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f x = f y
[PROOF STEP]
have \<open>norm (f (x - y)) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
f x = f y

goal (1 subgoal):
 1. norm (f (x - y)) = 0
[PROOF STEP]
by (simp add: complex_vector.linear_diff)
[PROOF STATE]
proof (state)
this:
norm (f (x - y)) = 0

goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
with bound b
[PROOF STATE]
proof (chain)
picking this:
b * norm ?x \<le> norm (f ?x)
0 < b
norm (f (x - y)) = 0
[PROOF STEP]
have \<open>norm (x - y) = 0\<close>
[PROOF STATE]
proof (prove)
using this:
b * norm ?x \<le> norm (f ?x)
0 < b
norm (f (x - y)) = 0

goal (1 subgoal):
 1. norm (x - y) = 0
[PROOF STEP]
by (metis linorder_not_le mult_le_0_iff nle_le norm_ge_zero)
[PROOF STATE]
proof (state)
this:
norm (x - y) = 0

goal (1 subgoal):
 1. \<And>x y. f x = f y \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
norm (x - y) = 0
[PROOF STEP]
show \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
norm (x - y) = 0

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inj f

goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
from \<open>surj f\<close>
[PROOF STATE]
proof (chain)
picking this:
surj f
[PROOF STEP]
have [simp]: \<open>x = f x'\<close> \<open>y = f y'\<close>
[PROOF STATE]
proof (prove)
using this:
surj f

goal (1 subgoal):
 1. x = f x' &&& y = f y'
[PROOF STEP]
by (simp_all add: surj_f_inv_f x'_def y'_def)
[PROOF STATE]
proof (state)
this:
x = f x'
y = f y'

goal (3 subgoals):
 1. \<And>x y. inv f (x + y) = inv f x + inv f y
 2. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 3. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
show "inv f (x + y) = inv f x + inv f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f (x + y) = inv f x + inv f y
[PROOF STEP]
by (simp flip: complex_vector.linear_add)
[PROOF STATE]
proof (state)
this:
inv f (x + y) = inv f x + inv f y

goal (2 subgoals):
 1. \<And>r x. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
 2. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
show "inv f (r *\<^sub>C x) = r *\<^sub>C inv f x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f (r *\<^sub>C x) = r *\<^sub>C inv f x
[PROOF STEP]
by (simp flip: clinear.scaleC)
[PROOF STATE]
proof (state)
this:
inv f (r *\<^sub>C x) = r *\<^sub>C inv f x

goal (1 subgoal):
 1. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
from bound
[PROOF STATE]
proof (chain)
picking this:
b * norm ?x \<le> norm (f ?x)
[PROOF STEP]
have "b * norm (inv f x) \<le> norm x"
[PROOF STATE]
proof (prove)
using this:
b * norm ?x \<le> norm (f ?x)

goal (1 subgoal):
 1. b * norm (inv f x) \<le> norm x
[PROOF STEP]
by (simp flip: clinear.scaleC)
[PROOF STATE]
proof (state)
this:
b * norm (inv f x) \<le> norm x

goal (1 subgoal):
 1. \<And>x. norm (inv f x) \<le> norm x * ?K
[PROOF STEP]
with b
[PROOF STATE]
proof (chain)
picking this:
0 < b
b * norm (inv f x) \<le> norm x
[PROOF STEP]
show "norm (inv f x) \<le> norm x * inverse b"
[PROOF STATE]
proof (prove)
using this:
0 < b
b * norm (inv f x) \<le> norm x

goal (1 subgoal):
 1. norm (inv f x) \<le> norm x * inverse b
[PROOF STEP]
by (smt (verit, ccfv_threshold) left_inverse mult.commute mult_cancel_right1 mult_le_cancel_left_pos vector_space_over_itself.scale_scale)
[PROOF STATE]
proof (state)
this:
norm (inv f x) \<le> norm x * inverse b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma read'_correct_alt: "(read' el s t, read el s t) \<in> \<langle>pnet_rel\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (read' el s t, read el s t) \<in> \<langle>pnet_rel\<rangle>option_rel
[PROOF STEP]
unfolding pnet_rel_def br_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (read' el s t, read el s t) \<in> \<langle>{(c, a). a = pnet_\<alpha> c \<and> True}\<rangle>option_rel
[PROOF STEP]
apply (simp add: option_rel_def read'_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. read' el s t = None \<or> (\<exists>a. read' el s t = Some a \<and> (\<exists>z. read' el s t = Some z \<and> pnet_\<alpha> z = pnet_\<alpha> a))
[PROOF STEP]
using domIff
[PROOF STATE]
proof (prove)
using this:
(?a \<in> dom ?m) = (?m ?a \<noteq> None)

goal (1 subgoal):
 1. read' el s t = None \<or> (\<exists>a. read' el s t = Some a \<and> (\<exists>z. read' el s t = Some z \<and> pnet_\<alpha> z = pnet_\<alpha> a))
[PROOF STEP]
by force