[STATEMENT]
lemma fbox_arden_iff: "\<nabla>x = 0 \<Longrightarrow> (d p = d q \<cdot> |x] p \<longleftrightarrow> d p = |x\<^sup>\<star>] q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nabla>x = (zero_class.zero::'a) \<Longrightarrow> (d p = d q \<cdot>  |x] p) = (d p =  |x\<^sup>\<star>] q)
[PROOF STEP]
by (metis fbox_arden_eq fbox_simp fbox_star_unfold_var)


[STATEMENT]
lemma fbox_arden_while_iff: "\<nabla> (d t \<cdot> x) = 0 \<Longrightarrow> (d p = (d t + d q) \<cdot> |d t \<cdot> x] p \<longleftrightarrow> d p = |while t do x od] q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nabla>(d t \<cdot> x) = (zero_class.zero::'a) \<Longrightarrow> (d p = (d t + d q) \<cdot>  |d t \<cdot> x] p) = (d p =  |while t do x od] q)
[PROOF STEP]
by (metis fbox_arden_iff dka.dom_add_closed fbox_export3 while_def)


[STATEMENT]
lemma fbox_arden_whilei: "\<nabla> (d t \<cdot> x) = 0 \<Longrightarrow> (d i = (d t + d q) \<cdot> |d t \<cdot> x] i \<Longrightarrow> d i = |while t inv i do x od] q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<nabla>(d t \<cdot> x) = (zero_class.zero::'a); d i = (d t + d q) \<cdot>  |d t \<cdot> x] i\<rbrakk> \<Longrightarrow> d i =  |while t inv i do x od] q
[PROOF STEP]
using fbox_arden_while_iff whilei_def
[PROOF STATE]
proof (prove)
using this:
\<nabla>(d ?t \<cdot> ?x) = (zero_class.zero::'a) \<Longrightarrow> (d ?p = (d ?t + d ?q) \<cdot>  |d ?t \<cdot> ?x] ?p) = (d ?p =  |while ?t do ?x od] ?q)
while ?p inv ?i do ?x od = while ?p do ?x od

goal (1 subgoal):
 1. \<lbrakk>\<nabla>(d t \<cdot> x) = (zero_class.zero::'a); d i = (d t + d q) \<cdot>  |d t \<cdot> x] i\<rbrakk> \<Longrightarrow> d i =  |while t inv i do x od] q
[PROOF STEP]
by auto


[STATEMENT]
lemma fbox_arden_whilei_iff: "\<nabla> (d t \<cdot> x) = 0 \<Longrightarrow> (d i = (d t + d q) \<cdot> |d t \<cdot> x] i \<longleftrightarrow> d i = |while t inv i do x od] q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nabla>(d t \<cdot> x) = (zero_class.zero::'a) \<Longrightarrow> (d i = (d t + d q) \<cdot>  |d t \<cdot> x] i) = (d i =  |while t inv i do x od] q)
[PROOF STEP]
using fbox_arden_while_iff whilei_def
[PROOF STATE]
proof (prove)
using this:
\<nabla>(d ?t \<cdot> ?x) = (zero_class.zero::'a) \<Longrightarrow> (d ?p = (d ?t + d ?q) \<cdot>  |d ?t \<cdot> ?x] ?p) = (d ?p =  |while ?t do ?x od] ?q)
while ?p inv ?i do ?x od = while ?p do ?x od

goal (1 subgoal):
 1. \<nabla>(d t \<cdot> x) = (zero_class.zero::'a) \<Longrightarrow> (d i = (d t + d q) \<cdot>  |d t \<cdot> x] i) = (d i =  |while t inv i do x od] q)
[PROOF STEP]
by auto


[STATEMENT]
lemma noether_nabla: "Noetherian x \<Longrightarrow> \<nabla> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Noetherian x \<Longrightarrow> \<nabla>x = (zero_class.zero::'a)
[PROOF STEP]
by (metis nabla_closure nabla_unfold noetherian_alt)


[STATEMENT]
lemma nabla_noether_iff: "Noetherian x \<longleftrightarrow> \<nabla> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Noetherian x = (\<nabla>x = (zero_class.zero::'a))
[PROOF STEP]
using nabla_noether noether_nabla
[PROOF STATE]
proof (prove)
using this:
\<nabla>?x = (zero_class.zero::'a) \<Longrightarrow> Noetherian ?x
Noetherian ?x \<Longrightarrow> \<nabla>?x = (zero_class.zero::'a)

goal (1 subgoal):
 1. Noetherian x = (\<nabla>x = (zero_class.zero::'a))
[PROOF STEP]
by blast


[STATEMENT]
lemma nabla_preloeb_iff: "\<nabla> x = 0 \<longleftrightarrow> PreLoebian x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nabla>x = (zero_class.zero::'a)) = PreLoebian x
[PROOF STEP]
using Noetherian_iff_PreLoebian nabla_noether noether_nabla
[PROOF STATE]
proof (prove)
using this:
Noetherian ?x = PreLoebian ?x
\<nabla>?x = (zero_class.zero::'a) \<Longrightarrow> Noetherian ?x
Noetherian ?x \<Longrightarrow> \<nabla>?x = (zero_class.zero::'a)

goal (1 subgoal):
 1. (\<nabla>x = (zero_class.zero::'a)) = PreLoebian x
[PROOF STEP]
by blast


[STATEMENT]
lemma rel_nabla_prop: "rel_nabla R = {} \<longleftrightarrow> (\<forall>P. P \<subseteq> relfdia R P \<longrightarrow> P = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_nabla R = {}) = (\<forall>P. P \<subseteq> relfdia R P \<longrightarrow> P = {})
[PROOF STEP]
by (metis bot.extremum_uniqueI rel_nabla_coinduct_var rel_nabla_unfold)


[STATEMENT]
lemma fdia_rel_im1: "s2r ((converse R) `` P) = relfdia R (s2r P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2r (R\<inverse> `` P) = relfdia R (s2r P)
[PROOF STEP]
by (auto simp: Id_on_def rel_antidomain_kleene_algebra.ads_d_def rel_ad_def rel_antidomain_kleene_algebra.fdia_def Image_def converse_def)


[STATEMENT]
lemma fdia_rel_im2: "s2r ((converse R) `` (r2s (rdom P))) = relfdia R P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2r (R\<inverse> `` r2s (rdom P)) = relfdia R P
[PROOF STEP]
by (simp add: fdia_rel_im1 rsr)


[STATEMENT]
lemma wf_nabla_aux: "(P \<subseteq> (converse R) `` P \<longrightarrow> P = {}) \<longleftrightarrow> (s2r P \<subseteq> relfdia R (s2r P) \<longrightarrow> s2r P = {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P \<subseteq> R\<inverse> `` P \<longrightarrow> P = {}) = (s2r P \<subseteq> relfdia R (s2r P) \<longrightarrow> s2r P = {})
[PROOF STEP]
apply (standard, metis Domain_Id_on Domain_mono Id_on_empty fdia_rel_im1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s2r P \<subseteq> relfdia R (s2r P) \<longrightarrow> s2r P = {} \<Longrightarrow> P \<subseteq> R\<inverse> `` P \<longrightarrow> P = {}
[PROOF STEP]
using fdia_rel_im1
[PROOF STATE]
proof (prove)
using this:
s2r (?R\<inverse> `` ?P) = relfdia ?R (s2r ?P)

goal (1 subgoal):
 1. s2r P \<subseteq> relfdia R (s2r P) \<longrightarrow> s2r P = {} \<Longrightarrow> P \<subseteq> R\<inverse> `` P \<longrightarrow> P = {}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma wf_nabla: "wf (converse R) \<longleftrightarrow> rel_nabla R = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (R\<inverse>) = (rel_nabla R = {})
[PROOF STEP]
by (metis (no_types, lifting) fdia_rel_im2 rel_fdivka.nabla_unfold_eq rel_nabla_prop rel_nabla_unfold wfE_pf wfI_pf wf_nabla_aux)


[STATEMENT]
lemma HT'_eq_HT: "HT' \<pi> P (\<lambda>_. c) Q = HT \<pi> P c Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT' \<pi> P (\<lambda>_. c) Q = HT \<pi> P c Q
[PROOF STEP]
unfolding HT_def HT'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<^sub>0. P s\<^sub>0 \<longrightarrow> wp \<pi> c (Q s\<^sub>0) s\<^sub>0) = (\<forall>s\<^sub>0. P s\<^sub>0 \<longrightarrow> wp \<pi> c (Q s\<^sub>0) s\<^sub>0)
[PROOF STEP]
..


[STATEMENT]
lemma HT'_partial_eq_HT: "HT'_partial \<pi> P (\<lambda>_. c) Q = HT_partial \<pi> P c Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT'_partial \<pi> P (\<lambda>_. c) Q = HT_partial \<pi> P c Q
[PROOF STEP]
unfolding HT_partial_def HT'_partial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>s\<^sub>0. P s\<^sub>0 \<longrightarrow> wlp \<pi> c (Q s\<^sub>0) s\<^sub>0) = (\<forall>s\<^sub>0. P s\<^sub>0 \<longrightarrow> wlp \<pi> c (Q s\<^sub>0) s\<^sub>0)
[PROOF STEP]
..


[STATEMENT]
lemma HT'setI:
    assumes "wf R"
    assumes RL: "\<And>f P c Q s\<^sub>0. \<lbrakk> HT'set_r (\<lambda>f' s'. ((f' s'),(f s\<^sub>0))\<in>R ) \<pi> \<Theta>; (f,(P,c,Q))\<in>\<Theta>; P s\<^sub>0 \<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0"
    shows "HT'set \<pi> \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT'set \<pi> \<Theta>
[PROOF STEP]
unfolding HT'set_def HT'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(n, P, c, Q)\<in>\<Theta>. \<forall>s\<^sub>0. P s\<^sub>0 \<longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
proof clarsimp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa ab b s\<^sub>0. \<lbrakk>(a, aa, ab, b) \<in> \<Theta>; aa s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (ab s\<^sub>0) (b s\<^sub>0) s\<^sub>0
[PROOF STEP]
fix f\<^sub>0 P c Q s\<^sub>0
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a aa ab b s\<^sub>0. \<lbrakk>(a, aa, ab, b) \<in> \<Theta>; aa s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (ab s\<^sub>0) (b s\<^sub>0) s\<^sub>0
[PROOF STEP]
assume "(f\<^sub>0,(P,c,Q))\<in>\<Theta>" "P s\<^sub>0"
[PROOF STATE]
proof (state)
this:
(f\<^sub>0, P, c, Q) \<in> \<Theta>
P s\<^sub>0

goal (1 subgoal):
 1. \<And>a aa ab b s\<^sub>0. \<lbrakk>(a, aa, ab, b) \<in> \<Theta>; aa s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (ab s\<^sub>0) (b s\<^sub>0) s\<^sub>0
[PROOF STEP]
with \<open>wf R\<close>
[PROOF STATE]
proof (chain)
picking this:
wf R
(f\<^sub>0, P, c, Q) \<in> \<Theta>
P s\<^sub>0
[PROOF STEP]
show "wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0"
[PROOF STATE]
proof (prove)
using this:
wf R
(f\<^sub>0, P, c, Q) \<in> \<Theta>
P s\<^sub>0

goal (1 subgoal):
 1. wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
proof (induction "f\<^sub>0 s\<^sub>0" arbitrary: f\<^sub>0 c s\<^sub>0 P Q)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f\<^sub>0 s\<^sub>0 c P Q. \<lbrakk>\<And>f\<^sub>0' s\<^sub>0' c P Q. \<lbrakk>(f\<^sub>0' s\<^sub>0', f\<^sub>0 s\<^sub>0) \<in> R; (f\<^sub>0', P, c, Q) \<in> \<Theta>; P s\<^sub>0'\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0') (Q s\<^sub>0') s\<^sub>0'; (f\<^sub>0, P, c, Q) \<in> \<Theta>; P s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?f\<^sub>0 ?s\<^sub>0, f\<^sub>0 s\<^sub>0) \<in> R; (?f\<^sub>0, ?P, ?c, ?Q) \<in> \<Theta>; ?P ?s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (?c ?s\<^sub>0) (?Q ?s\<^sub>0) ?s\<^sub>0
(f\<^sub>0, P, c, Q) \<in> \<Theta>
P s\<^sub>0

goal (1 subgoal):
 1. \<And>f\<^sub>0 s\<^sub>0 c P Q. \<lbrakk>\<And>f\<^sub>0' s\<^sub>0' c P Q. \<lbrakk>(f\<^sub>0' s\<^sub>0', f\<^sub>0 s\<^sub>0) \<in> R; (f\<^sub>0', P, c, Q) \<in> \<Theta>; P s\<^sub>0'\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0') (Q s\<^sub>0') s\<^sub>0'; (f\<^sub>0, P, c, Q) \<in> \<Theta>; P s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
note RL' = RL[of f\<^sub>0 s\<^sub>0 P, OF _ less.prems]
[PROOF STATE]
proof (state)
this:
HT'set_r (\<lambda>f' s'. (f' s', f\<^sub>0 s\<^sub>0) \<in> R) \<pi> \<Theta> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0

goal (1 subgoal):
 1. \<And>f\<^sub>0 s\<^sub>0 c P Q. \<lbrakk>\<And>f\<^sub>0' s\<^sub>0' c P Q. \<lbrakk>(f\<^sub>0' s\<^sub>0', f\<^sub>0 s\<^sub>0) \<in> R; (f\<^sub>0', P, c, Q) \<in> \<Theta>; P s\<^sub>0'\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0') (Q s\<^sub>0') s\<^sub>0'; (f\<^sub>0, P, c, Q) \<in> \<Theta>; P s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
apply (rule RL')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT'set_r (\<lambda>f' s'. (f' s', f\<^sub>0 s\<^sub>0) \<in> R) \<pi> \<Theta>
[PROOF STEP]
unfolding HT'set_r_def HT'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>(n, P, c, Q)\<in>\<Theta>. \<forall>s\<^sub>0. (n s\<^sub>0, f\<^sub>0 s\<^sub>0) \<in> R \<and> P s\<^sub>0 \<longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
using less.hyps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>(?f\<^sub>0 ?s\<^sub>0, f\<^sub>0 s\<^sub>0) \<in> R; (?f\<^sub>0, ?P, ?c, ?Q) \<in> \<Theta>; ?P ?s\<^sub>0\<rbrakk> \<Longrightarrow> wp \<pi> (?c ?s\<^sub>0) (?Q ?s\<^sub>0) ?s\<^sub>0

goal (1 subgoal):
 1. \<forall>(n, P, c, Q)\<in>\<Theta>. \<forall>s\<^sub>0. (n s\<^sub>0, f\<^sub>0 s\<^sub>0) \<in> R \<and> P s\<^sub>0 \<longrightarrow> wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wp \<pi> (c s\<^sub>0) (Q s\<^sub>0) s\<^sub>0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HT'setD:
    assumes "HT'set \<pi> (insert (f,(P,c,Q)) \<Theta>)"
    shows "HT' \<pi> P c Q" and "HT'set \<pi> \<Theta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HT' \<pi> P c Q &&& HT'set \<pi> \<Theta>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
HT'set \<pi> (insert (f, P, c, Q) \<Theta>)

goal (1 subgoal):
 1. HT' \<pi> P c Q &&& HT'set \<pi> \<Theta>
[PROOF STEP]
unfolding HT'set_def
[PROOF STATE]
proof (prove)
using this:
\<forall>(n, P, c, Q)\<in>insert (f, P, c, Q) \<Theta>. HT' \<pi> P c Q

goal (1 subgoal):
 1. HT' \<pi> P c Q &&& \<forall>(n, P, c, Q)\<in>\<Theta>. HT' \<pi> P c Q
[PROOF STEP]
by auto


[STATEMENT]
lemma cxt_inv:
  "\<lbrakk> cxt_to_stmt E c = c' ; \<And> p q. c' \<noteq> Seq p q \<rbrakk> \<Longrightarrow> E = [] \<and> c' = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cxt_to_stmt E c = c'; \<And>p q. c' \<noteq> p ;; q\<rbrakk> \<Longrightarrow> E = [] \<and> c' = c
[PROOF STEP]
by (metis cxt_to_stmt.simps(1) cxt_to_stmt.simps(2) neq_Nil_conv)


[STATEMENT]
lemma cxt_inv_assign:
  "\<lbrakk> cxt_to_stmt E c = x \<leftarrow> e \<rbrakk> \<Longrightarrow> c = x \<leftarrow> e \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = x \<leftarrow> e \<Longrightarrow> c = x \<leftarrow> e \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(11) cxt_inv)


[STATEMENT]
lemma cxt_inv_skip:
  "\<lbrakk> cxt_to_stmt E c = Skip \<rbrakk> \<Longrightarrow> c = Skip \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = Skip \<Longrightarrow> c = Skip \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(21) cxt_inv)


[STATEMENT]
lemma cxt_inv_stop:
  "cxt_to_stmt E c = Stop \<Longrightarrow> c = Stop \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = Stop \<Longrightarrow> c = Stop \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(40) cxt_inv)


[STATEMENT]
lemma cxt_inv_if:
  "cxt_to_stmt E c = If e p q \<Longrightarrow> c = If e p q \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = Stmt.If e p q \<Longrightarrow> c = Stmt.If e p q \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(37) cxt_inv)


[STATEMENT]
lemma cxt_inv_while:
  "cxt_to_stmt E c = While e p \<Longrightarrow> c = While e p \<and> E = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cxt_to_stmt E c = While e p \<Longrightarrow> c = While e p \<and> E = []
[PROOF STEP]
by (metis Stmt.simps(39) cxt_inv)


[STATEMENT]
lemma skip_elim [elim]:
  "\<langle>Skip, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Skip, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>Skip = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Skip = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
 3. \<And>c mu c'a E. \<lbrakk>Skip = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
[PROOF STEP]
apply (metis (lifting) cxt_inv_skip cxt_to_stmt.simps(1) skip_elim')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Skip = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
 2. \<And>c mu c'a E. \<lbrakk>Skip = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
[PROOF STEP]
apply (metis Stmt.simps(20))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c mu c'a E. \<lbrakk>Skip = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem = mem'
[PROOF STEP]
by (metis Stmt.simps(18) cxt_inv_skip)


[STATEMENT]
lemma assign_elim [elim]:
  "\<langle>x \<leftarrow> e, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem (x := eval\<^sub>A mem e)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>x \<leftarrow> e, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>x \<leftarrow> e = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 3. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (rename_tac c c'a E)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>x \<leftarrow> e = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 3. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (subgoal_tac "c = x \<leftarrow> e \<and> E = []")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c = x \<leftarrow> e \<and> E = []\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 2. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c = x \<leftarrow> e \<and> E = []
 3. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>x \<leftarrow> e = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
 4. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stop \<and> mds = mds' \<and> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c = cxt_to_stmt E c
 2. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> E = []
 3. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> cxt_to_stmt E c'a = Stop
 4. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mds = mds'
 5. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (metis cxt_inv_assign)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> E = []
 2. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> cxt_to_stmt E c'a = Stop
 3. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mds = mds'
 4. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (metis cxt_inv_assign)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> cxt_to_stmt E c'a = Stop
 2. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mds = mds'
 3. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (metis Stmt.simps(8) cxt_inv_assign)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mds = mds'
 2. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
apply (metis Stmt.simps(8) cxt_inv_assign)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c mu c'a E. \<lbrakk>x \<leftarrow> e = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> mem' = mem(x := eval\<^sub>A mem e)
[PROOF STEP]
by (metis Stmt.simps(8) cxt_inv_assign)


[STATEMENT]
lemma if_elim [elim]:
  "\<And> P.
    \<lbrakk> \<langle>If b p q, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w ;
     \<lbrakk> c' = p; mem' = mem ; mds' = mds ; eval\<^sub>B mem b \<rbrakk> \<Longrightarrow> P ;
     \<lbrakk> c' = q; mem' = mem ; mds' = mds ; \<not> eval\<^sub>B mem b \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>\<langle>Stmt.If b p q, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w; \<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>P c c'a E. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> P
 2. \<And>P c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> P
 3. \<And>P c mu c'a E. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (metis (no_types) cxt_inv_if cxt_to_stmt.simps(1) if_elim')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> P
 2. \<And>P c mu c'a E. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
apply (metis Stmt.simps(36))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P c mu c'a E. \<lbrakk>\<lbrakk>c' = p; mem' = mem; mds' = mds; eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; \<lbrakk>c' = q; mem' = mem; mds' = mds; \<not> eval\<^sub>B mem b\<rbrakk> \<Longrightarrow> P; Stmt.If b p q = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> P
[PROOF STEP]
by (metis Stmt.simps(30) cxt_inv_if)


[STATEMENT]
lemma while_elim [elim]:
  "\<lbrakk> \<langle>While e c, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<rbrakk> \<Longrightarrow> c' = If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>While e c, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ca c'a E. \<lbrakk>While e c = cxt_to_stmt E ca; c' = cxt_to_stmt E c'a; mds' = mds; (ca, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>While e c = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
 3. \<And>ca mu c'a E. \<lbrakk>While e c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (metis (no_types) cxt_inv_while cxt_to_stmt.simps(1) while_elim')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>While e c = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
 2. \<And>ca mu c'a E. \<lbrakk>While e c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (metis Stmt.simps(38))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca mu c'a E. \<lbrakk>While e c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = Stmt.If e (c ;; While e c) Stop \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
by (metis (lifting) Stmt.simps(33) cxt_inv_while)


[STATEMENT]
lemma upd_elim [elim]:
  "\<langle>c@[upd], mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>c@[upd], mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ca c'a E. \<lbrakk>c@[upd] = cxt_to_stmt E ca; c' = cxt_to_stmt E c'a; mds' = mds; (ca, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>c@[upd] = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
 3. \<And>ca mu c'a E. \<lbrakk>c@[upd] = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
[PROOF STEP]
apply (metis (lifting) Stmt.simps(28) cxt_inv upd_elim')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>c@[upd] = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
 2. \<And>ca mu c'a E. \<lbrakk>c@[upd] = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
[PROOF STEP]
apply (metis Stmt.simps(29))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca mu c'a E. \<lbrakk>c@[upd] = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<langle>c, update_modes upd mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w
[PROOF STEP]
by (metis (lifting) Stmt.simps(2) Stmt.simps(29) cxt_inv cxt_to_stmt.simps(1))


[STATEMENT]
lemma cxt_seq_elim [elim]:
  "c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c \<Longrightarrow> (E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2) \<or> (\<exists> c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c \<Longrightarrow> E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')
[PROOF STEP]
apply (cases E)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c; E = []\<rbrakk> \<Longrightarrow> E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')
 2. \<And>a list. \<lbrakk>c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c; E = a # list\<rbrakk> \<Longrightarrow> E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')
[PROOF STEP]
apply (metis cxt_to_stmt.simps(1))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c; E = a # list\<rbrakk> \<Longrightarrow> E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')
[PROOF STEP]
by (metis Stmt.simps(3) cxt_to_stmt.simps(2))


[STATEMENT]
lemma stop_no_eval: "\<not> (\<langle>Stop, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<langle>Stop, mds, mem\<rangle>\<^sub>w, \<langle>c', mds', mem'\<rangle>\<^sub>w) \<notin> eval\<^sub>w
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Stop, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> False
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>Stop = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> False
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Stop = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> False
 3. \<And>c mu c'a E. \<lbrakk>Stop = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis cxt_inv_stop stop_no_eval')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Stop = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> False
 2. \<And>c mu c'a E. \<lbrakk>Stop = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply (metis Stmt.simps(41))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c mu c'a E. \<lbrakk>Stop = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (metis Stmt.simps(35) cxt_inv_stop)


[STATEMENT]
lemma seq_stop_elim [elim]:
  "\<langle>Stop ;; c, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Stop ;; c, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ca c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E ca; c' = cxt_to_stmt E c'a; mds' = mds; (ca, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Stop ;; c = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
 3. \<And>ca mu c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>ca c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E ca; mds' = mds; (ca, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a\<rbrakk> \<Longrightarrow> cxt_to_stmt E c'a = c \<and> mds = mds \<and> mem' = mem
 2. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Stop ;; c = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
 3. \<And>ca mu c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (metis (no_types) cxt_seq_elim cxt_to_stmt.simps(1) seq_elim' stop_no_eval')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c\<^sub>1 c\<^sub>1' c\<^sub>2. \<lbrakk>Stop ;; c = c\<^sub>1 ;; c\<^sub>2; c' = c\<^sub>1' ;; c\<^sub>2; \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
 2. \<And>ca mu c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
apply (metis Stmt.inject(3) stop_no_eval)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca mu c'a E. \<lbrakk>Stop ;; c = cxt_to_stmt E (ca@[mu]); c' = cxt_to_stmt E c'a; \<langle>ca, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c' = c \<and> mds' = mds \<and> mem' = mem
[PROOF STEP]
by (metis Stmt.distinct(23) Stmt.distinct(29) cxt_seq_elim)


[STATEMENT]
lemma cxt_stmt_seq:
  "c ;; cxt_to_stmt E c' = cxt_to_stmt (c' # E) c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c ;; cxt_to_stmt E c' = cxt_to_stmt (c' # E) c
[PROOF STEP]
by (metis cxt_to_stmt.simps(2))


[STATEMENT]
lemma seq_elim [elim]:
  "\<lbrakk> \<langle>c\<^sub>1 ;; c\<^sub>2, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w ; c\<^sub>1 \<noteq> Stop \<rbrakk> \<Longrightarrow>
  (\<exists> c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<langle>c\<^sub>1 ;; c\<^sub>2, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c', mds', mem'\<rangle>\<^sub>w; c\<^sub>1 \<noteq> Stop\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (erule eval_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c; c' = cxt_to_stmt E c'a; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem')\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c\<^sub>1' c\<^sub>1'' c\<^sub>2'. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = c\<^sub>1' ;; c\<^sub>2'; c' = c\<^sub>1'' ;; c\<^sub>2'; \<langle>c\<^sub>1', mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1'', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 3. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E c; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds, mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c\<^sub>1' c\<^sub>1'' c\<^sub>2'. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = c\<^sub>1' ;; c\<^sub>2'; c' = c\<^sub>1'' ;; c\<^sub>2'; \<langle>c\<^sub>1', mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1'', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 3. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (drule cxt_seq_elim)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a; E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c')\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds, mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c\<^sub>1' c\<^sub>1'' c\<^sub>2'. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = c\<^sub>1' ;; c\<^sub>2'; c' = c\<^sub>1'' ;; c\<^sub>2'; \<langle>c\<^sub>1', mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1'', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 3. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (erule disjE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a; E = [] \<and> c = c\<^sub>1 ;; c\<^sub>2\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds, mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a; \<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c'\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds, mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 3. \<And>c\<^sub>1' c\<^sub>1'' c\<^sub>2'. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = c\<^sub>1' ;; c\<^sub>2'; c' = c\<^sub>1'' ;; c\<^sub>2'; \<langle>c\<^sub>1', mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1'', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 4. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (metis seq_elim')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; mds' = mds; (c, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = cxt_to_stmt E c'a; \<exists>c' cs. E = c' # cs \<and> c = c\<^sub>1 \<and> c\<^sub>2 = cxt_to_stmt cs c'\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds, mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c\<^sub>1' c\<^sub>1'' c\<^sub>2'. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = c\<^sub>1' ;; c\<^sub>2'; c' = c\<^sub>1'' ;; c\<^sub>2'; \<langle>c\<^sub>1', mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1'', mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
 3. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> c' = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c'a c'aa cs. \<lbrakk>c\<^sub>1 \<noteq> Stop; mds' = mds; (c\<^sub>1, mem) \<leadsto>\<^sub>s (c'a, mem'); c' = c'a ;; cxt_to_stmt cs c'aa; c\<^sub>2 = cxt_to_stmt cs c'aa\<rbrakk> \<Longrightarrow> \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds, mem'\<rangle>\<^sub>w
 2. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (metis cxt_to_stmt.simps(1) eval\<^sub>w.unannotated)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
[PROOF STEP]
apply (subgoal_tac "c\<^sub>1 = (c@[mu])")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w; c\<^sub>1 = c@[mu]\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c\<^sub>1, mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c\<^sub>1 = c@[mu]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c mu c'a E. \<lbrakk>(c@[mu]) ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w; c\<^sub>1 = c@[mu]\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c@[mu], mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c\<^sub>1 = c@[mu]
[PROOF STEP]
apply (drule cxt_seq_elim)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c mu c'a E. \<lbrakk>c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w; c\<^sub>1 = c@[mu]; E = [] \<and> c@[mu] = (c@[mu]) ;; c\<^sub>2 \<or> (\<exists>c' cs. E = c' # cs \<and> c@[mu] = c@[mu] \<and> c\<^sub>2 = cxt_to_stmt cs c')\<rbrakk> \<Longrightarrow> \<exists>c\<^sub>1'. \<langle>c@[mu], mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c\<^sub>1', mds', mem'\<rangle>\<^sub>w \<and> cxt_to_stmt E c'a = c\<^sub>1' ;; c\<^sub>2
 2. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c\<^sub>1 = c@[mu]
[PROOF STEP]
apply (metis Stmt.distinct(23) cxt_stmt_seq cxt_to_stmt.simps(1) eval\<^sub>w.decl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c mu c'a E. \<lbrakk>c\<^sub>1 \<noteq> Stop; c\<^sub>1 ;; c\<^sub>2 = cxt_to_stmt E (c@[mu]); c' = cxt_to_stmt E c'a; \<langle>c, update_modes mu mds, mem\<rangle>\<^sub>w \<leadsto>\<^sub>w \<langle>c'a, mds', mem'\<rangle>\<^sub>w\<rbrakk> \<Longrightarrow> c\<^sub>1 = c@[mu]
[PROOF STEP]
by (metis Stmt.distinct(23) cxt_seq_elim)


[STATEMENT]
lemma stop_cxt: "Stop = cxt_to_stmt E c \<Longrightarrow> c = Stop"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Stop = cxt_to_stmt E c \<Longrightarrow> c = Stop
[PROOF STEP]
by (metis Stmt.simps(41) cxt_to_stmt.simps(1) cxt_to_stmt.simps(2) neq_Nil_conv)


[STATEMENT]
lemma to_vec_eq_ith: "(to_vec A) $ i = A $$ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_vec A $ i = A $$ i
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma to_mtx_ith[simp]:
  "(to_mtx A) $$ i1 = A $ i1"
  "(to_mtx A) $$ i1 $ i2 = A $ i1 $ i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx A $$ i1 = A $ i1 &&& to_mtx A $$ i1 $ i2 = A $ i1 $ i2
[PROOF STEP]
by (transfer, simp)+


[STATEMENT]
lemma to_mtx_vec_lambda_ith[simp]: "to_mtx (\<chi> i j. x i j) $$ i1 $ i2 = x i1 i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. x i j) $$ i1 $ i2 = x i1 i2
[PROOF STEP]
by (simp add: sq_mtx_ith_def)


[STATEMENT]
lemma sq_mtx_eq_iff:
  shows "A = B = (\<forall>i j. A $$ i $ j = B $$ i $ j)"
    and "A = B = (\<forall>i. A $$ i = B $$ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A = B) = (\<forall>i j. A $$ i $ j = B $$ i $ j) &&& (A = B) = (\<forall>i. A $$ i = B $$ i)
[PROOF STEP]
by (transfer, simp add: vec_eq_iff)+


[STATEMENT]
lemma sq_mtx_diag_simps[simp]:
  "i = j \<Longrightarrow> sq_mtx_diag f $$ i $ j = f i"
  "i \<noteq> j \<Longrightarrow> sq_mtx_diag f $$ i $ j = 0"
  "sq_mtx_diag f $$ i = axis i (f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i = j \<Longrightarrow> sq_mtx_diag f $$ i $ j = f i) &&& (i \<noteq> j \<Longrightarrow> sq_mtx_diag f $$ i $ j = 0) &&& sq_mtx_diag f $$ i = axis i (f i)
[PROOF STEP]
unfolding sq_mtx_diag_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i = j \<Longrightarrow> map_fun id to_mtx diag_mat f $$ i $ j = f i) &&& (i \<noteq> j \<Longrightarrow> map_fun id to_mtx diag_mat f $$ i $ j = 0) &&& map_fun id to_mtx diag_mat f $$ i = axis i (f i)
[PROOF STEP]
by (simp_all add: axis_def vec_eq_iff)


[STATEMENT]
lemma sq_mtx_vec_mult_diag_axis: "(\<d>\<i>\<a>\<g> i. f i) *\<^sub>V (axis i k) = axis i (f i * k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<d>\<i>\<a>\<g> i. f i) *\<^sub>V axis i k = axis i (f i * k)
[PROOF STEP]
unfolding sq_mtx_diag_vec_mult axis_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>ia. f ia * (\<chi>ia. if ia = i then k else 0) $ ia) = (\<chi>ia. if ia = i then f i * k else 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma sq_mtx_vec_mult_eq: "m *\<^sub>V x = (\<chi> i. sum (\<lambda>j. (m $$ i $ j) * (x $ j)) UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m *\<^sub>V x = (\<chi>i. \<Sum>j\<in>UNIV. m $$ i $ j * x $ j)
[PROOF STEP]
by (transfer, simp add: matrix_vector_mult_def)


[STATEMENT]
lemma sq_mtx_transpose_transpose[simp]: "(A\<^sup>\<dagger>)\<^sup>\<dagger> = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>\<dagger>\<^sup>\<dagger> = A
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma transpose_mult_vec_canon_row[simp]: "(A\<^sup>\<dagger>) *\<^sub>V (\<e> i) = \<r>\<o>\<w> i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>\<dagger> *\<^sub>V \<e> i = \<r>\<o>\<w> i A
[PROOF STEP]
by transfer (simp add: row_def transpose_def axis_def matrix_vector_mult_def)


[STATEMENT]
lemma row_ith[simp]: "\<r>\<o>\<w> i A = A $$ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<r>\<o>\<w> i A = A $$ i
[PROOF STEP]
by transfer (simp add: row_def)


[STATEMENT]
lemma mtx_vec_mult_canon: "A *\<^sub>V (\<e> i) = \<c>\<o>\<l> i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V \<e> i = \<c>\<o>\<l> i A
[PROOF STEP]
by (transfer, simp add: matrix_vector_mult_basis)


[STATEMENT]
lemma sq_mtx_zero_ith[simp]: "0 $$ i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 $$ i = 0
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma sq_mtx_zero_nth[simp]: "0 $$ i $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 $$ i $ j = 0
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma sq_mtx_plus_eq: "A + B = to_mtx (\<chi> i j. A$$i$j + B$$i$j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A + B = to_mtx (\<chi>i j. A $$ i $ j + B $$ i $ j)
[PROOF STEP]
by transfer (simp add: vec_eq_iff)


[STATEMENT]
lemma sq_mtx_plus_ith[simp]:"(A + B) $$ i = A $$ i + B $$ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A + B) $$ i = A $$ i + B $$ i
[PROOF STEP]
unfolding sq_mtx_plus_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. A $$ i $ j + B $$ i $ j) $$ i = A $$ i + B $$ i
[PROOF STEP]
by (simp add: vec_eq_iff)


[STATEMENT]
lemma sq_mtx_minus_eq: "A - B = to_mtx (\<chi> i j. A$$i$j - B$$i$j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B = to_mtx (\<chi>i j. A $$ i $ j - B $$ i $ j)
[PROOF STEP]
by transfer (simp add: vec_eq_iff)


[STATEMENT]
lemma sq_mtx_minus_ith[simp]:"(A - B) $$ i = A $$ i - B $$ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A - B) $$ i = A $$ i - B $$ i
[PROOF STEP]
unfolding sq_mtx_minus_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. A $$ i $ j - B $$ i $ j) $$ i = A $$ i - B $$ i
[PROOF STEP]
by (simp add: vec_eq_iff)


[STATEMENT]
lemma sq_mtx_times_eq: "A * B = to_mtx (\<chi> i j. sum (\<lambda>k. A$$i$k * B$$k$j) UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * B = to_mtx (\<chi>i j. \<Sum>k\<in>UNIV. A $$ i $ k * B $$ k $ j)
[PROOF STEP]
by transfer (simp add: matrix_matrix_mult_def)


[STATEMENT]
lemma sq_mtx_plus_diag_diag[simp]: "sq_mtx_diag f + sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i + g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sq_mtx_diag f + sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i + g i)
[PROOF STEP]
by (subst sq_mtx_eq_iff) (simp add: axis_def)


[STATEMENT]
lemma sq_mtx_minus_diag_diag[simp]: "sq_mtx_diag f - sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i - g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sq_mtx_diag f - sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i - g i)
[PROOF STEP]
by (subst sq_mtx_eq_iff) (simp add: axis_def)


[STATEMENT]
lemma sum_sq_mtx_diag[simp]: "(\<Sum>n<m. sq_mtx_diag (g n)) = (\<d>\<i>\<a>\<g> i. \<Sum>n<m. (g n i))" for m::nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<m. sq_mtx_diag (g n)) = (\<d>\<i>\<a>\<g> i. \<Sum>n<m. g n i)
[PROOF STEP]
by (induct m, simp, subst sq_mtx_eq_iff, simp_all)


[STATEMENT]
lemma sq_mtx_mult_diag_diag[simp]: "sq_mtx_diag f * sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i * g i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sq_mtx_diag f * sq_mtx_diag g = (\<d>\<i>\<a>\<g> i. f i * g i)
[PROOF STEP]
by (simp add: matrix_mul_diag_diag sq_mtx_diag.abs_eq times_sq_mtx.abs_eq)


[STATEMENT]
lemma sq_mtx_mult_diagl: "(\<d>\<i>\<a>\<g> i. f i) * A = to_mtx (\<chi> i j. f i * A $$ i $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<d>\<i>\<a>\<g> i. f i) * A = to_mtx (\<chi>i j. f i * A $$ i $ j)
[PROOF STEP]
by transfer (simp add: matrix_mul_diag_matl)


[STATEMENT]
lemma sq_mtx_mult_diagr: "A * (\<d>\<i>\<a>\<g> i. f i) = to_mtx (\<chi> i j. A $$ i $ j * f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * (\<d>\<i>\<a>\<g> i. f i) = to_mtx (\<chi>i j. A $$ i $ j * f j)
[PROOF STEP]
by transfer (simp add: matrix_matrix_mul_diag_matr)


[STATEMENT]
lemma mtx_vec_mult_0l[simp]: "0 *\<^sub>V x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 *\<^sub>V x = 0
[PROOF STEP]
by (simp add: sq_mtx_vec_mult.abs_eq zero_sq_mtx_def)


[STATEMENT]
lemma mtx_vec_mult_0r[simp]: "A *\<^sub>V 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V 0 = 0
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma mtx_vec_mult_add_rdistr: "(A + B) *\<^sub>V x = A *\<^sub>V x + B *\<^sub>V x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A + B) *\<^sub>V x = A *\<^sub>V x + B *\<^sub>V x
[PROOF STEP]
unfolding plus_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun to_vec (map_fun to_vec to_mtx) (+) A B *\<^sub>V x = A *\<^sub>V x + B *\<^sub>V x
[PROOF STEP]
apply(transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B x. map_fun (\<lambda>x. x) (map_fun (\<lambda>x. x) (\<lambda>x. x)) (+) A B *v x = A *v x + B *v x
[PROOF STEP]
by (simp add: matrix_vector_mult_add_rdistrib)


[STATEMENT]
lemma mtx_vec_mult_add_rdistl: "A *\<^sub>V (x + y) = A *\<^sub>V x + A *\<^sub>V y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V (x + y) = A *\<^sub>V x + A *\<^sub>V y
[PROOF STEP]
unfolding plus_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V (x + y) = A *\<^sub>V x + A *\<^sub>V y
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A x y. A *v (x + y) = A *v x + A *v y
[PROOF STEP]
by (simp add: matrix_vector_right_distrib)


[STATEMENT]
lemma mtx_vec_mult_minus_ldistrib: "A *\<^sub>V (x - y) =  A *\<^sub>V x -  A *\<^sub>V y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V (x - y) = A *\<^sub>V x - A *\<^sub>V y
[PROOF STEP]
by (metis (no_types, lifting) add_diff_cancel diff_add_cancel
      matrix_vector_right_distrib sq_mtx_vec_mult.rep_eq)


[STATEMENT]
lemma sq_mtx_times_vec_assoc: "(A * B) *\<^sub>V x = A *\<^sub>V (B *\<^sub>V x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A * B) *\<^sub>V x = A *\<^sub>V (B *\<^sub>V x)
[PROOF STEP]
by (transfer, simp add: matrix_vector_mul_assoc)


[STATEMENT]
lemma sq_mtx_vec_mult_sum_cols: "A *\<^sub>V x = sum (\<lambda>i. x $ i *\<^sub>R \<c>\<o>\<l> i A) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V x = (\<Sum>i\<in>UNIV. x $ i *\<^sub>R \<c>\<o>\<l> i A)
[PROOF STEP]
by(transfer) (simp add: matrix_mult_sum scalar_mult_eq_scaleR)


[STATEMENT]
lemma sq_mtx_scaleR_eq: "c *\<^sub>R A = to_mtx (\<chi> i j. c *\<^sub>R A $$ i $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R A = to_mtx (\<chi>i j. c *\<^sub>R A $$ i $ j)
[PROOF STEP]
by transfer (simp add: vec_eq_iff)


[STATEMENT]
lemma scaleR_to_mtx_ith[simp]: "c *\<^sub>R (to_mtx A) $$ i1 $ i2 = c * A $ i1 $ i2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R to_mtx A $$ i1 $ i2 = c * A $ i1 $ i2
[PROOF STEP]
by transfer (simp add: scaleR_vec_def)


[STATEMENT]
lemma sq_mtx_scaleR_ith[simp]: "(c *\<^sub>R A) $$ i = (c  *\<^sub>R (A $$ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c *\<^sub>R A) $$ i = c *\<^sub>R A $$ i
[PROOF STEP]
by (unfold scaleR_sq_mtx_def, transfer, simp)


[STATEMENT]
lemma scaleR_sq_mtx_diag: "c *\<^sub>R sq_mtx_diag f = (\<d>\<i>\<a>\<g> i. c * f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R sq_mtx_diag f = (\<d>\<i>\<a>\<g> i. c * f i)
[PROOF STEP]
by (subst sq_mtx_eq_iff, simp add: axis_def)


[STATEMENT]
lemma scaleR_mtx_vec_assoc: "(c *\<^sub>R A) *\<^sub>V x = c *\<^sub>R (A *\<^sub>V x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c *\<^sub>R A) *\<^sub>V x = c *\<^sub>R A *\<^sub>V x
[PROOF STEP]
unfolding scaleR_sq_mtx_def sq_mtx_vec_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun to_vec id (*v) (map_fun id (map_fun to_vec to_mtx) (*\<^sub>R) c A) x = c *\<^sub>R map_fun to_vec id (*v) A x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c *\<^sub>R to_vec A *v x = c *\<^sub>R (to_vec A *v x)
[PROOF STEP]
by (simp add: scaleR_matrix_vector_assoc)


[STATEMENT]
lemma mtx_vec_scaleR_commute: "A *\<^sub>V (c *\<^sub>R x) = c *\<^sub>R (A *\<^sub>V x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A *\<^sub>V (c *\<^sub>R x) = c *\<^sub>R A *\<^sub>V x
[PROOF STEP]
unfolding scaleR_sq_mtx_def sq_mtx_vec_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun to_vec id (*v) A (c *\<^sub>R x) = c *\<^sub>R map_fun to_vec id (*v) A x
[PROOF STEP]
apply(simp, transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A c x. A *v c *\<^sub>R x = c *\<^sub>R (A *v x)
[PROOF STEP]
by (simp add: vector_scaleR_commute)


[STATEMENT]
lemma mtx_times_scaleR_commute: "A * (c *\<^sub>R B) = c *\<^sub>R (A * B)" for A::"('n::finite) sq_mtx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A * c *\<^sub>R B = c *\<^sub>R (A * B)
[PROOF STEP]
unfolding sq_mtx_scaleR_eq sq_mtx_times_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_mtx (\<chi>i j. \<Sum>k\<in>UNIV. A $$ i $ k * to_mtx (\<chi>i j. c *\<^sub>R B $$ i $ j) $$ k $ j) = to_mtx (\<chi>i j. c *\<^sub>R to_mtx (\<chi>i j. \<Sum>k\<in>UNIV. A $$ i $ k * B $$ k $ j) $$ i $ j)
[PROOF STEP]
apply(simp add: to_mtx_inject)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i. \<chi>j. \<Sum>k\<in>UNIV. A $$ i $ k * (c * B $$ k $ j)) = (\<lambda>i. \<chi>j. c * (\<Sum>k\<in>UNIV. A $$ i $ k * B $$ k $ j))
[PROOF STEP]
apply(simp add: vec_eq_iff fun_eq_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x i. (\<Sum>k\<in>UNIV. A $$ x $ k * (c * B $$ k $ i)) = c * (\<Sum>k\<in>UNIV. A $$ x $ k * B $$ k $ i)
[PROOF STEP]
by (simp add: semiring_normalization_rules(19) vector_space_over_itself.scale_sum_right)


[STATEMENT]
lemma le_mtx_norm: "m \<in> {\<parallel>A *\<^sub>V x\<parallel> |x. \<parallel>x\<parallel> = 1} \<Longrightarrow> m \<le> \<parallel>A\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> {\<parallel>A *\<^sub>V x\<parallel> |x. \<parallel>x\<parallel> = 1} \<Longrightarrow> m \<le> \<parallel>A\<parallel>
[PROOF STEP]
using cSup_upper[of _ "{\<parallel>(to_vec A) *v x\<parallel> | x. \<parallel>x\<parallel> = 1}"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> {\<parallel>to_vec A *v x\<parallel> |x. \<parallel>x\<parallel> = 1}; bdd_above {\<parallel>to_vec A *v x\<parallel> |x. \<parallel>x\<parallel> = 1}\<rbrakk> \<Longrightarrow> ?x \<le> Sup {\<parallel>to_vec A *v x\<parallel> |x. \<parallel>x\<parallel> = 1}

goal (1 subgoal):
 1. m \<in> {\<parallel>A *\<^sub>V x\<parallel> |x. \<parallel>x\<parallel> = 1} \<Longrightarrow> m \<le> \<parallel>A\<parallel>
[PROOF STEP]
by (simp add: op_norm_set_proptys(2) op_norm_def norm_sq_mtx_def sq_mtx_vec_mult.rep_eq)


[STATEMENT]
lemma norm_vec_mult_le: "\<parallel>A *\<^sub>V x\<parallel> \<le> (\<parallel>A\<parallel>) * (\<parallel>x\<parallel>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A *\<^sub>V x\<parallel> \<le> \<parallel>A\<parallel> * \<parallel>x\<parallel>
[PROOF STEP]
by (simp add: norm_matrix_le_mult_op_norm norm_sq_mtx_def sq_mtx_vec_mult.rep_eq)


[STATEMENT]
lemma bounded_bilinear_sq_mtx_vec_mult: "bounded_bilinear (\<lambda>A s. A *\<^sub>V s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_bilinear (*\<^sub>V)
[PROOF STEP]
apply (rule bounded_bilinear.intro, simp_all add: mtx_vec_mult_add_rdistr
      mtx_vec_mult_add_rdistl scaleR_mtx_vec_assoc mtx_vec_scaleR_commute)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>K. \<forall>a b. \<parallel>a *\<^sub>V b\<parallel> \<le> \<parallel>a\<parallel> * \<parallel>b\<parallel> * K
[PROOF STEP]
by (rule_tac x=1 in exI, auto intro!: norm_vec_mult_le)


[STATEMENT]
lemma norm_sq_mtx_def2: "\<parallel>A\<parallel> = Sup {\<parallel>A *\<^sub>V x\<parallel> |x. \<parallel>x\<parallel> = 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A\<parallel> = Sup {\<parallel>A *\<^sub>V x\<parallel> |x. \<parallel>x\<parallel> = 1}
[PROOF STEP]
unfolding norm_sq_mtx_def op_norm_def sq_mtx_vec_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {\<parallel>to_vec A *v x\<parallel> |x. \<parallel>x\<parallel> = 1} = Sup {\<parallel>map_fun to_vec id (*v) A x\<parallel> |x. \<parallel>x\<parallel> = 1}
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_sq_mtx_def3: "\<parallel>A\<parallel> = (SUP x. (\<parallel>A *\<^sub>V x\<parallel>) / (\<parallel>x\<parallel>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A\<parallel> = (SUP x. \<parallel>A *\<^sub>V x\<parallel> / \<parallel>x\<parallel>)
[PROOF STEP]
unfolding norm_sq_mtx_def onorm_def sq_mtx_vec_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP x. \<parallel>to_vec A *v x\<parallel> / \<parallel>x\<parallel>) = (SUP x. \<parallel>map_fun to_vec id (*v) A x\<parallel> / \<parallel>x\<parallel>)
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_sq_mtx_diag: "\<parallel>sq_mtx_diag f\<parallel> = Max {\<bar>f i\<bar> |i. i \<in> UNIV}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>sq_mtx_diag f\<parallel> = Max {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
unfolding norm_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>to_vec (sq_mtx_diag f)\<parallel>\<^sub>o\<^sub>p = Max {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. \<parallel>diag_mat f\<parallel>\<^sub>o\<^sub>p = Max {\<bar>f i\<bar> |i. i \<in> UNIV}
[PROOF STEP]
by (rule op_norm_diag_mat_eq)


[STATEMENT]
lemma sq_mtx_norm_le_sum_col: "\<parallel>A\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i A\<parallel>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i A\<parallel>)
[PROOF STEP]
using op_norm_le_sum_column[of "to_vec A"]
[PROOF STATE]
proof (prove)
using this:
\<parallel>to_vec A\<parallel>\<^sub>o\<^sub>p \<le> (\<Sum>i\<in>UNIV. \<parallel>column i (to_vec A)\<parallel>)

goal (1 subgoal):
 1. \<parallel>A\<parallel> \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i A\<parallel>)
[PROOF STEP]
apply(simp add: norm_sq_mtx_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>to_vec A\<parallel>\<^sub>o\<^sub>p \<le> (\<Sum>i\<in>UNIV. \<parallel>column i (to_vec A)\<parallel>) \<Longrightarrow> \<parallel>to_vec A\<parallel>\<^sub>o\<^sub>p \<le> (\<Sum>i\<in>UNIV. \<parallel>\<c>\<o>\<l> i A\<parallel>)
[PROOF STEP]
by(transfer, simp add: op_norm_le_sum_column)


[STATEMENT]
lemma norm_le_transpose: "\<parallel>A\<parallel> \<le> \<parallel>A\<^sup>\<dagger>\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A\<parallel> \<le> \<parallel>A\<^sup>\<dagger>\<parallel>
[PROOF STEP]
unfolding norm_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>to_vec A\<parallel>\<^sub>o\<^sub>p \<le> \<parallel>to_vec A\<^sup>\<dagger>\<parallel>\<^sub>o\<^sub>p
[PROOF STEP]
by transfer (rule op_norm_le_transpose)


[STATEMENT]
lemma norm_eq_norm_transpose[simp]: "\<parallel>A\<^sup>\<dagger>\<parallel> = \<parallel>A\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A\<^sup>\<dagger>\<parallel> = \<parallel>A\<parallel>
[PROOF STEP]
using norm_le_transpose[of A] and norm_le_transpose[of "A\<^sup>\<dagger>"]
[PROOF STATE]
proof (prove)
using this:
\<parallel>A\<parallel> \<le> \<parallel>A\<^sup>\<dagger>\<parallel>
\<parallel>A\<^sup>\<dagger>\<parallel> \<le> \<parallel>A\<^sup>\<dagger>\<^sup>\<dagger>\<parallel>

goal (1 subgoal):
 1. \<parallel>A\<^sup>\<dagger>\<parallel> = \<parallel>A\<parallel>
[PROOF STEP]
by simp


[STATEMENT]
lemma norm_column_le_norm: "\<parallel>A $$ i\<parallel> \<le> \<parallel>A\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A $$ i\<parallel> \<le> \<parallel>A\<parallel>
[PROOF STEP]
using norm_vec_mult_le[of "A\<^sup>\<dagger>" "\<e> i"]
[PROOF STATE]
proof (prove)
using this:
\<parallel>A\<^sup>\<dagger> *\<^sub>V \<e> i\<parallel> \<le> \<parallel>A\<^sup>\<dagger>\<parallel> * \<parallel>\<e> i\<parallel>

goal (1 subgoal):
 1. \<parallel>A $$ i\<parallel> \<le> \<parallel>A\<parallel>
[PROOF STEP]
by simp


[STATEMENT]
lemma sq_mtx_one_idty: "1 * A = A" "A * 1 = A" for A :: "'a sq_mtx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * A = A &&& A * 1 = A
[PROOF STEP]
by(transfer, transfer, unfold mat_def matrix_matrix_mult_def, simp add: vec_eq_iff)+


[STATEMENT]
lemma sq_mtx_norm_1: "\<parallel>(1::'a sq_mtx)\<parallel> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>1\<parallel> = 1
[PROOF STEP]
unfolding one_sq_mtx_def norm_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>to_vec (id (to_mtx (mat 1)))\<parallel>\<^sub>o\<^sub>p = 1
[PROOF STEP]
apply(simp add: op_norm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup {\<parallel>x\<parallel> |x. \<parallel>x\<parallel> = 1} = 1
[PROOF STEP]
apply(subst cSup_eq[of _ 1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<forall>x\<in>{\<parallel>x\<parallel> |x. \<parallel>x\<parallel> = 1}. x \<le> 1
 2. Bex {\<parallel>x\<parallel> |x. \<parallel>x\<parallel> = 1} ((\<le>) 1)
 3. 1 = 1
[PROOF STEP]
using ex_norm_eq_1
[PROOF STATE]
proof (prove)
using this:
\<exists>x. \<parallel>x\<parallel> = 1

goal (3 subgoals):
 1. \<forall>x\<in>{\<parallel>x\<parallel> |x. \<parallel>x\<parallel> = 1}. x \<le> 1
 2. Bex {\<parallel>x\<parallel> |x. \<parallel>x\<parallel> = 1} ((\<le>) 1)
 3. 1 = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma sq_mtx_norm_times: "\<parallel>A * B\<parallel> \<le> (\<parallel>A\<parallel>) * (\<parallel>B\<parallel>)" for A :: "'a sq_mtx"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>A * B\<parallel> \<le> \<parallel>A\<parallel> * \<parallel>B\<parallel>
[PROOF STEP]
unfolding norm_sq_mtx_def times_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>to_vec (map_fun to_vec (map_fun to_vec to_mtx) (**) A B)\<parallel>\<^sub>o\<^sub>p \<le> (\<parallel>to_vec A\<parallel>\<^sub>o\<^sub>p) * (\<parallel>to_vec B\<parallel>\<^sub>o\<^sub>p)
[PROOF STEP]
by(simp add: op_norm_matrix_matrix_mult_le)


[STATEMENT]
lemma sq_mtx_one_ith_simps[simp]: "1 $$ i $ i = 1" "i \<noteq> j \<Longrightarrow> 1 $$ i $ j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 $$ i $ i = 1 &&& (i \<noteq> j \<Longrightarrow> 1 $$ i $ j = 0)
[PROOF STEP]
unfolding one_sq_mtx_def mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. id (to_mtx (\<chi>i j. if i = j then 1 else 0)) $$ i $ i = 1 &&& (i \<noteq> j \<Longrightarrow> id (to_mtx (\<chi>i j. if i = j then 1 else 0)) $$ i $ j = 0)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma of_nat_eq_sq_mtx_diag[simp]: "of_nat m = (\<d>\<i>\<a>\<g> i. m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat m = (\<d>\<i>\<a>\<g> x. real m)
[PROOF STEP]
by (induct m) (simp, subst sq_mtx_eq_iff, simp add: axis_def)+


[STATEMENT]
lemma mtx_vec_mult_1[simp]: "1 *\<^sub>V s = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 *\<^sub>V s = s
[PROOF STEP]
by (auto simp: sq_mtx_vec_mult_def one_sq_mtx_def
      mat_def vec_eq_iff matrix_vector_mult_def)


[STATEMENT]
lemma sq_mtx_diag_one[simp]: "(\<d>\<i>\<a>\<g> i. 1) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<d>\<i>\<a>\<g> i. 1) = 1
[PROOF STEP]
by (subst sq_mtx_eq_iff, simp add: one_sq_mtx_def mat_def axis_def)


[STATEMENT]
lemma mtx_invertible_def: "mtx_invertible A \<longleftrightarrow> (\<exists>A'. A' * A = 1 \<and> A * A' = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx_invertible A = (\<exists>A'. A' * A = 1 \<and> A * A' = 1)
[PROOF STEP]
apply (unfold sq_mtx_inv_def times_sq_mtx_def one_sq_mtx_def invertible_def, clarsimp, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A'. \<lbrakk>to_vec A ** A' = mat 1; A' ** to_vec A = mat 1\<rbrakk> \<Longrightarrow> \<exists>A'. to_mtx (to_vec A' ** to_vec A) = to_mtx (mat 1) \<and> to_mtx (to_vec A ** to_vec A') = to_mtx (mat 1)
 2. \<And>A'. \<lbrakk>to_mtx (to_vec A' ** to_vec A) = to_mtx (mat 1); to_mtx (to_vec A ** to_vec A') = to_mtx (mat 1)\<rbrakk> \<Longrightarrow> \<exists>A'. to_vec A ** A' = mat 1 \<and> A' ** to_vec A = mat 1
[PROOF STEP]
apply(rule_tac x="to_mtx A'" in exI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A'. \<lbrakk>to_mtx (to_vec A' ** to_vec A) = to_mtx (mat 1); to_mtx (to_vec A ** to_vec A') = to_mtx (mat 1)\<rbrakk> \<Longrightarrow> \<exists>A'. to_vec A ** A' = mat 1 \<and> A' ** to_vec A = mat 1
[PROOF STEP]
by (rule_tac x="to_vec A'" in exI, simp add: to_mtx_inject)


[STATEMENT]
lemma mtx_invertibleI:
  assumes "A * B = 1" and "B * A = 1"
  shows "mtx_invertible A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx_invertible A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A * B = 1
B * A = 1

goal (1 subgoal):
 1. mtx_invertible A
[PROOF STEP]
unfolding mtx_invertible_def
[PROOF STATE]
proof (prove)
using this:
A * B = 1
B * A = 1

goal (1 subgoal):
 1. \<exists>A'. A' * A = 1 \<and> A * A' = 1
[PROOF STEP]
by auto


[STATEMENT]
lemma mtx_invertibleD[simp]:
  assumes "mtx_invertible A"
  shows "A\<^sup>-\<^sup>1 * A = 1" and "A * A\<^sup>-\<^sup>1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>-\<^sup>1 * A = 1 &&& A * A\<^sup>-\<^sup>1 = 1
[PROOF STEP]
apply (unfold sq_mtx_inv_def times_sq_mtx_def one_sq_mtx_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. map_fun to_vec (map_fun to_vec to_mtx) (**) (map_fun to_vec to_mtx matrix_inv A) A = id (to_mtx (mat 1))
 2. map_fun to_vec (map_fun to_vec to_mtx) (**) A (map_fun to_vec to_mtx matrix_inv A) = id (to_mtx (mat 1))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mtx_invertible A

goal (2 subgoals):
 1. map_fun to_vec (map_fun to_vec to_mtx) (**) (map_fun to_vec to_mtx matrix_inv A) A = id (to_mtx (mat 1))
 2. map_fun to_vec (map_fun to_vec to_mtx) (**) A (map_fun to_vec to_mtx matrix_inv A) = id (to_mtx (mat 1))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma mtx_invertible_inv[simp]: "mtx_invertible A \<Longrightarrow> mtx_invertible (A\<^sup>-\<^sup>1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx_invertible A \<Longrightarrow> mtx_invertible A\<^sup>-\<^sup>1
[PROOF STEP]
using mtx_invertibleD mtx_invertibleI
[PROOF STATE]
proof (prove)
using this:
mtx_invertible ?A \<Longrightarrow> ?A\<^sup>-\<^sup>1 * ?A = 1
mtx_invertible ?A \<Longrightarrow> ?A * ?A\<^sup>-\<^sup>1 = 1
\<lbrakk>?A * ?B = 1; ?B * ?A = 1\<rbrakk> \<Longrightarrow> mtx_invertible ?A

goal (1 subgoal):
 1. mtx_invertible A \<Longrightarrow> mtx_invertible A\<^sup>-\<^sup>1
[PROOF STEP]
by blast


[STATEMENT]
lemma mtx_invertible_one[simp]: "mtx_invertible 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx_invertible 1
[PROOF STEP]
by (simp add: one_sq_mtx.rep_eq)


[STATEMENT]
lemma sq_mtx_inv_unique:
  assumes "A * B = 1" and "B * A = 1"
  shows "A\<^sup>-\<^sup>1 = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A\<^sup>-\<^sup>1 = B
[PROOF STEP]
by (metis (no_types, lifting) assms mtx_invertibleD(2)
      mtx_invertibleI mult.assoc sq_mtx_one_idty(1))


[STATEMENT]
lemma sq_mtx_inv_idempotent[simp]: "mtx_invertible A \<Longrightarrow> A\<^sup>-\<^sup>1\<^sup>-\<^sup>1 = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mtx_invertible A \<Longrightarrow> A\<^sup>-\<^sup>1\<^sup>-\<^sup>1 = A
[PROOF STEP]
using mtx_invertibleD sq_mtx_inv_unique
[PROOF STATE]
proof (prove)
using this:
mtx_invertible ?A \<Longrightarrow> ?A\<^sup>-\<^sup>1 * ?A = 1
mtx_invertible ?A \<Longrightarrow> ?A * ?A\<^sup>-\<^sup>1 = 1
\<lbrakk>?A * ?B = 1; ?B * ?A = 1\<rbrakk> \<Longrightarrow> ?A\<^sup>-\<^sup>1 = ?B

goal (1 subgoal):
 1. mtx_invertible A \<Longrightarrow> A\<^sup>-\<^sup>1\<^sup>-\<^sup>1 = A
[PROOF STEP]
by blast


[STATEMENT]
lemma sq_mtx_inv_mult:
  assumes "mtx_invertible A" and "mtx_invertible B"
  shows "(A * B)\<^sup>-\<^sup>1 = B\<^sup>-\<^sup>1 * A\<^sup>-\<^sup>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A * B)\<^sup>-\<^sup>1 = B\<^sup>-\<^sup>1 * A\<^sup>-\<^sup>1
[PROOF STEP]
by (simp add: assms matrix_inv_matrix_mul sq_mtx_inv_def times_sq_mtx_def)


[STATEMENT]
lemma sq_mtx_inv_one[simp]: "1\<^sup>-\<^sup>1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1\<^sup>-\<^sup>1 = 1
[PROOF STEP]
by (simp add: sq_mtx_inv_unique)


[STATEMENT]
lemma similar_sq_mtx_matrix: "(A \<sim> B) = similar_matrix (to_vec A) (to_vec B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<sim> B) = similar_matrix (to_vec A) (to_vec B)
[PROOF STEP]
apply(unfold similar_matrix_def similar_sq_mtx_def, safe)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrakk>mtx_invertible P; A = P\<^sup>-\<^sup>1 * B * P\<rbrakk> \<Longrightarrow> \<exists>Pa. invertible Pa \<and> to_vec (P\<^sup>-\<^sup>1 * B * P) = matrix_inv Pa ** to_vec B ** Pa
 2. \<And>P. \<lbrakk>invertible P; to_vec A = matrix_inv P ** to_vec B ** P\<rbrakk> \<Longrightarrow> \<exists>P. mtx_invertible P \<and> A = P\<^sup>-\<^sup>1 * B * P
[PROOF STEP]
apply (metis sq_mtx_inv.rep_eq times_sq_mtx.rep_eq)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>invertible P; to_vec A = matrix_inv P ** to_vec B ** P\<rbrakk> \<Longrightarrow> \<exists>P. mtx_invertible P \<and> A = P\<^sup>-\<^sup>1 * B * P
[PROOF STEP]
by (metis UNIV_I sq_mtx_inv.abs_eq times_sq_mtx.abs_eq to_mtx_inverse to_vec_inverse)


[STATEMENT]
lemma similar_sq_mtx_refl[simp]: "A \<sim> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sim> A
[PROOF STEP]
by (unfold similar_sq_mtx_def, rule_tac x="1" in exI, simp)


[STATEMENT]
lemma similar_sq_mtx_simm: "A \<sim> B \<Longrightarrow> B \<sim> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<sim> B \<Longrightarrow> B \<sim> A
[PROOF STEP]
apply(unfold similar_sq_mtx_def, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>mtx_invertible P; A = P\<^sup>-\<^sup>1 * B * P\<rbrakk> \<Longrightarrow> \<exists>Pa. mtx_invertible Pa \<and> B = Pa\<^sup>-\<^sup>1 * (P\<^sup>-\<^sup>1 * B * P) * Pa
[PROOF STEP]
apply(rule_tac x="P\<^sup>-\<^sup>1" in exI, simp add: mult.assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrakk>mtx_invertible P; A = P\<^sup>-\<^sup>1 * (B * P)\<rbrakk> \<Longrightarrow> B = P * (P\<^sup>-\<^sup>1 * B)
[PROOF STEP]
by (metis mtx_invertibleD(2) mult.assoc mult.left_neutral)


[STATEMENT]
lemma similar_sq_mtx_trans: "A \<sim> B \<Longrightarrow> B \<sim> C \<Longrightarrow> A \<sim> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sim> B; B \<sim> C\<rbrakk> \<Longrightarrow> A \<sim> C
[PROOF STEP]
unfolding similar_sq_mtx_matrix
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>similar_matrix (to_vec A) (to_vec B); similar_matrix (to_vec B) (to_vec C)\<rbrakk> \<Longrightarrow> similar_matrix (to_vec A) (to_vec C)
[PROOF STEP]
using similar_matrix_trans
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>similar_matrix ?A ?B; similar_matrix ?B ?C\<rbrakk> \<Longrightarrow> similar_matrix ?A ?C

goal (1 subgoal):
 1. \<lbrakk>similar_matrix (to_vec A) (to_vec B); similar_matrix (to_vec B) (to_vec C)\<rbrakk> \<Longrightarrow> similar_matrix (to_vec A) (to_vec C)
[PROOF STEP]
by blast


[STATEMENT]
lemma power_similiar_sq_mtx_diag_eq:
  assumes "mtx_invertible P"
      and "A = P\<^sup>-\<^sup>1 * (sq_mtx_diag f) * P"
    shows "A^n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i^n) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P
[PROOF STEP]
proof(induct n, simp_all add: assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (P\<^sup>-\<^sup>1 * sq_mtx_diag f * P) ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P \<Longrightarrow> P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
fix n::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. (P\<^sup>-\<^sup>1 * sq_mtx_diag f * P) ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P \<Longrightarrow> P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
have "P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) =
  P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P
[PROOF STEP]
by (metis (no_types, lifting) assms(1) mtx_invertibleD(2) mult.assoc mult.right_neutral)
[PROOF STATE]
proof (state)
this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P

goal (1 subgoal):
 1. \<And>n. (P\<^sup>-\<^sup>1 * sq_mtx_diag f * P) ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P \<Longrightarrow> P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P

goal (1 subgoal):
 1. \<And>n. (P\<^sup>-\<^sup>1 * sq_mtx_diag f * P) ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P \<Longrightarrow> P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
have "... = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * (\<d>\<i>\<a>\<g> i. f i ^ n) * P = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P

goal (1 subgoal):
 1. \<And>n. (P\<^sup>-\<^sup>1 * sq_mtx_diag f * P) ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P \<Longrightarrow> P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
show "P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) =
  P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P"
[PROOF STATE]
proof (prove)
using this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P

goal (1 subgoal):
 1. P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
P\<^sup>-\<^sup>1 * sq_mtx_diag f * P * (P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P) = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i * f i ^ n) * P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma power_similar_sq_mtx_diag:
  assumes "A \<sim> (sq_mtx_diag f)"
  shows "A^n \<sim> (\<d>\<i>\<a>\<g> i. f i^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ^ n \<sim> (\<d>\<i>\<a>\<g> i. f i ^ n)
[PROOF STEP]
using assms power_similiar_sq_mtx_diag_eq
[PROOF STATE]
proof (prove)
using this:
A \<sim> sq_mtx_diag f
\<lbrakk>mtx_invertible ?P; ?A = ?P\<^sup>-\<^sup>1 * sq_mtx_diag ?f * ?P\<rbrakk> \<Longrightarrow> ?A ^ ?n = ?P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. ?f i ^ ?n) * ?P

goal (1 subgoal):
 1. A ^ n \<sim> (\<d>\<i>\<a>\<g> i. f i ^ n)
[PROOF STEP]
unfolding similar_sq_mtx_def
[PROOF STATE]
proof (prove)
using this:
\<exists>P. mtx_invertible P \<and> A = P\<^sup>-\<^sup>1 * sq_mtx_diag f * P
\<lbrakk>mtx_invertible ?P; ?A = ?P\<^sup>-\<^sup>1 * sq_mtx_diag ?f * ?P\<rbrakk> \<Longrightarrow> ?A ^ ?n = ?P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. ?f i ^ ?n) * ?P

goal (1 subgoal):
 1. \<exists>P. mtx_invertible P \<and> A ^ n = P\<^sup>-\<^sup>1 * (\<d>\<i>\<a>\<g> i. f i ^ n) * P
[PROOF STEP]
by blast


[STATEMENT]
lemma Cauchy_cols:
  fixes X :: "nat \<Rightarrow> ('a::finite) sq_mtx"
  assumes "Cauchy X"
  shows "Cauchy (\<lambda>n. \<c>\<o>\<l> i (X n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Cauchy (\<lambda>n. \<c>\<o>\<l> i (X n))
[PROOF STEP]
proof(unfold Cauchy_def dist_norm, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
fix \<epsilon>::real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
assume "\<epsilon> > 0"
[PROOF STATE]
proof (state)
this:
0 < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < \<epsilon>
[PROOF STEP]
obtain M where M_def:"\<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>

goal (1 subgoal):
 1. (\<And>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>Cauchy X\<close>
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>
Cauchy X

goal (1 subgoal):
 1. (\<And>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Cauchy_def
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>
\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e

goal (1 subgoal):
 1. (\<And>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(simp add: dist_sq_mtx_def) metis
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
fix m n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
assume "m \<ge> M" and "n \<ge> M"
[PROOF STATE]
proof (state)
this:
M \<le> m
M \<le> n

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
hence "\<epsilon> > \<parallel>X m - X n\<parallel>"
[PROOF STATE]
proof (prove)
using this:
M \<le> m
M \<le> n

goal (1 subgoal):
 1. \<parallel>X m - X n\<parallel> < \<epsilon>
[PROOF STEP]
using M_def
[PROOF STATE]
proof (prove)
using this:
M \<le> m
M \<le> n
\<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>X m - X n\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<parallel>X m - X n\<parallel> < \<epsilon>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<parallel>X m - X n\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>X m - X n\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
have "\<parallel>X m - X n\<parallel> \<ge> \<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> \<le> \<parallel>X m - X n\<parallel>
[PROOF STEP]
by(rule le_mtx_norm[of _ "X m - X n"], force)
[PROOF STATE]
proof (state)
this:
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> \<le> \<parallel>X m - X n\<parallel>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> \<le> \<parallel>X m - X n\<parallel>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
have "\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>
[PROOF STEP]
by (simp add: mtx_vec_mult_minus_rdistrib)
[PROOF STATE]
proof (state)
this:
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
have "... = \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel> = \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel>
[PROOF STEP]
by (simp add: mtx_vec_mult_minus_rdistrib mtx_vec_mult_canon)
[PROOF STATE]
proof (state)
this:
\<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel> = \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>X m - X n\<parallel> < \<epsilon>
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> \<le> \<parallel>X m - X n\<parallel>
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>
\<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel> = \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel>
[PROOF STEP]
have "\<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
\<parallel>X m - X n\<parallel> < \<epsilon>
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> \<le> \<parallel>X m - X n\<parallel>
\<parallel>(X m - X n) *\<^sub>V \<e> i\<parallel> = \<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel>
\<parallel>X m *\<^sub>V \<e> i - X n *\<^sub>V \<e> i\<parallel> = \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel>

goal (1 subgoal):
 1. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>M \<le> ?m2; M \<le> ?n2\<rbrakk> \<Longrightarrow> \<parallel>\<c>\<o>\<l> i (X ?m2) - \<c>\<o>\<l> i (X ?n2)\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < e
[PROOF STEP]
thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>M \<le> ?m2; M \<le> ?n2\<rbrakk> \<Longrightarrow> \<parallel>\<c>\<o>\<l> i (X ?m2) - \<c>\<o>\<l> i (X ?n2)\<parallel> < \<epsilon>

goal (1 subgoal):
 1. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. \<parallel>\<c>\<o>\<l> i (X m) - \<c>\<o>\<l> i (X n)\<parallel> < \<epsilon>

goal:
No subgoals!
[PROOF STEP]
qed