[STATEMENT]
lemma eventually_nat_real:
  assumes "eventually P (at_top :: real filter)"
  shows   "eventually (\<lambda>x. P (real x)) (at_top :: nat filter)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. P (real x)
[PROOF STEP]
using assms filterlim_real_sequentially
[PROOF STATE]
proof (prove)
using this:
eventually P at_top
filterlim real at_top sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. P (real x)
[PROOF STEP]
unfolding filterlim_def le_filter_def eventually_filtermap
[PROOF STATE]
proof (prove)
using this:
eventually P at_top
\<forall>P. eventually P at_top \<longrightarrow> (\<forall>\<^sub>F x in sequentially. P (real x))

goal (1 subgoal):
 1. \<forall>\<^sub>F x in sequentially. P (real x)
[PROOF STEP]
by auto


[STATEMENT]
lemma le_finfun_code [code]:
  "f \<le> g \<longleftrightarrow> finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f \<le> g) = finfun_All ((\<lambda>(x, y). x \<le> y) \<circ>$ ($f, g$))
[PROOF STEP]
by(simp add: le_finfun_def finfun_All_All o_def)


[STATEMENT]
lemma bot_finfun_apply [simp]: "($) bot = (\<lambda>_. bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) bot = (\<lambda>_. bot)
[PROOF STEP]
by(auto simp add: bot_finfun_def)


[STATEMENT]
lemma top_finfun_apply [simp]: "($) top = (\<lambda>_. top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) top = (\<lambda>_. top)
[PROOF STEP]
by(auto simp add: top_finfun_def)


[STATEMENT]
lemma inf_finfun_apply [simp]: "($) (inf f g) = inf (($) f) (($) g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (inf f g) = inf (($) f) (($) g)
[PROOF STEP]
by(auto simp add: inf_finfun_def o_def inf_fun_def)


[STATEMENT]
lemma sup_finfun_apply [simp]: "($) (sup f g) = sup (($) f) (($) g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (sup f g) = sup (($) f) (($) g)
[PROOF STEP]
by(auto simp add: sup_finfun_def o_def sup_fun_def)


[STATEMENT]
lemma minus_finfun_apply [simp]: "($) (f - g) = ($) f - ($) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (f - g) = ($) f - ($) g
[PROOF STEP]
by(simp add: minus_finfun_def o_def fun_diff_def)


[STATEMENT]
lemma uminus_finfun_apply [simp]: "($) (- g) = - ($) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (- g) = - ($) g
[PROOF STEP]
by(simp add: uminus_finfun_def o_def fun_Compl_def)


[STATEMENT]
lemma finfun_single_apply [simp]:
  "finfun_single x $ y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_single x $ y = (x = y)
[PROOF STEP]
by(simp add: finfun_single_def finfun_upd_apply)


[STATEMENT]
lemma [iff]:
  shows finfun_single_neq_bot: "finfun_single x \<noteq> bot"
  and bot_neq_finfun_single: "bot \<noteq> finfun_single x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_single x \<noteq> {}\<^sub>f &&& {}\<^sub>f \<noteq> finfun_single x
[PROOF STEP]
by(simp_all add: expand_finfun_eq fun_eq_iff)


[STATEMENT]
lemma finfun_leI [intro!]: "(!!x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. A $ x \<Longrightarrow> B $ x) \<Longrightarrow> A \<le> B
[PROOF STEP]
by(simp add: le_finfun_def)


[STATEMENT]
lemma finfun_leD [elim]: "\<lbrakk> A \<le> B; A $ x \<rbrakk> \<Longrightarrow> B $ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<le> B; A $ x\<rbrakk> \<Longrightarrow> B $ x
[PROOF STEP]
by(simp add: le_finfun_def)


[STATEMENT]
lemma finfun_Ball_except_const:
  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> set xs = UNIV \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Ball_except xs (K$ b) P = (\<not> b \<or> set xs = UNIV \<or> Code.abort STR ''finfun_ball_except'' (\<lambda>u. finfun_Ball_except xs (K$ b) P))
[PROOF STEP]
by(auto simp add: finfun_Ball_except_def)


[STATEMENT]
lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
  "finfun_Ball_except xs (K$ b) P \<longleftrightarrow> \<not> b \<or> is_list_UNIV xs \<or> Code.abort (STR ''finfun_ball_except'') (\<lambda>u. finfun_Ball_except xs (K$ b) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Ball_except xs (K$ b) P = (\<not> b \<or> is_list_UNIV xs \<or> Code.abort STR ''finfun_ball_except'' (\<lambda>u. finfun_Ball_except xs (K$ b) P))
[PROOF STEP]
by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff)


[STATEMENT]
lemma finfun_Ball_except_update:
  "finfun_Ball_except xs (A(a $:= b)) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Ball_except xs A(a $:= b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) A P)
[PROOF STEP]
by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm)


[STATEMENT]
lemma finfun_Ball_except_update_code [code]:
  fixes a :: "'a :: card_UNIV"
  shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Ball_except xs (finfun_update_code f a b) P = ((a \<in> set xs \<or> (b \<longrightarrow> P a)) \<and> finfun_Ball_except (a # xs) f P)
[PROOF STEP]
by(simp add: finfun_Ball_except_update)


[STATEMENT]
lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Ball = finfun_Ball_except []
[PROOF STEP]
by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)


[STATEMENT]
lemma finfun_Bex_except_const:
  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> set xs \<noteq> UNIV \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Bex_except xs (K$ b) P = (b \<and> set xs \<noteq> UNIV \<and> Code.abort STR ''finfun_Bex_except'' (\<lambda>u. finfun_Bex_except xs (K$ b) P))
[PROOF STEP]
by(auto simp add: finfun_Bex_except_def)


[STATEMENT]
lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
  "finfun_Bex_except xs (K$ b) P \<longleftrightarrow> b \<and> \<not> is_list_UNIV xs \<and> Code.abort (STR ''finfun_Bex_except'') (\<lambda>u. finfun_Bex_except xs (K$ b) P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Bex_except xs (K$ b) P = (b \<and> \<not> is_list_UNIV xs \<and> Code.abort STR ''finfun_Bex_except'' (\<lambda>u. finfun_Bex_except xs (K$ b) P))
[PROOF STEP]
by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff)


[STATEMENT]
lemma finfun_Bex_except_update:
  "finfun_Bex_except xs (A(a $:= b)) P \<longleftrightarrow> (a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Bex_except xs A(a $:= b) P = (a \<notin> set xs \<and> b \<and> P a \<or> finfun_Bex_except (a # xs) A P)
[PROOF STEP]
by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm)


[STATEMENT]
lemma finfun_Bex_except_update_code [code]:
  fixes a :: "'a :: card_UNIV"
  shows "finfun_Bex_except xs (finfun_update_code f a b) P \<longleftrightarrow> ((a \<notin> set xs \<and> b \<and> P a) \<or> finfun_Bex_except (a # xs) f P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Bex_except xs (finfun_update_code f a b) P = (a \<notin> set xs \<and> b \<and> P a \<or> finfun_Bex_except (a # xs) f P)
[PROOF STEP]
by(simp add: finfun_Bex_except_update)


[STATEMENT]
lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finfun_Bex = finfun_Bex_except []
[PROOF STEP]
by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)


[STATEMENT]
lemma iso_finfun_le [code_unfold]:
  "($) A \<le> ($) B \<longleftrightarrow> A \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (($) A \<le> ($) B) = (A \<le> B)
[PROOF STEP]
by (metis le_finfun_def le_funD le_funI)


[STATEMENT]
lemma iso_finfun_less [code_unfold]:
  "($) A < ($) B \<longleftrightarrow> A < B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (($) A < ($) B) = (A < B)
[PROOF STEP]
by (metis iso_finfun_le less_finfun_def less_fun_def)


[STATEMENT]
lemma iso_finfun_eq [code_unfold]:
  "($) A = ($) B \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (($) A = ($) B) = (A = B)
[PROOF STEP]
by(simp only: expand_finfun_eq)


[STATEMENT]
lemma iso_finfun_sup [code_unfold]:
  "sup (($) A) (($) B) = ($) (sup A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup (($) A) (($) B) = ($) (sup A B)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma iso_finfun_disj [code_unfold]:
  "A $ x \<or> B $ x \<longleftrightarrow> sup A B $ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A $ x \<or> B $ x) = sup A B $ x
[PROOF STEP]
by(simp add: sup_fun_def)


[STATEMENT]
lemma iso_finfun_conj [code_unfold]:
  "A $ x \<and> B $ x \<longleftrightarrow> inf A B $ x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A $ x \<and> B $ x) = inf A B $ x
[PROOF STEP]
by(simp add: inf_fun_def)


[STATEMENT]
lemma iso_finfun_empty_conv [code_unfold]:
  "(\<lambda>_. False) = ($) {}\<^sub>f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. False) = ($) {}\<^sub>f
[PROOF STEP]
by simp


[STATEMENT]
lemma iso_finfun_UNIV_conv [code_unfold]:
  "(\<lambda>_. True) = ($) finfun_UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. True) = ($) finfun_UNIV
[PROOF STEP]
by simp


[STATEMENT]
lemma iso_finfun_upd [code_unfold]:
  fixes A :: "'a pred\<^sub>f"
  shows "(($) A)(x := b) = ($) (A(x $:= b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (($) A)(x := b) = ($) A(x $:= b)
[PROOF STEP]
by(simp add: fun_eq_iff)


[STATEMENT]
lemma iso_finfun_uminus [code_unfold]:
  fixes A :: "'a pred\<^sub>f"
  shows "- ($) A = ($) (- A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - ($) A = ($) (- A)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma iso_finfun_minus [code_unfold]:
  fixes A :: "'a pred\<^sub>f"
  shows "($) A - ($) B = ($) (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) A - ($) B = ($) (A - B)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma iso_finfun_Ball_Ball:
  "(\<forall>x. A $ x \<longrightarrow> P x) \<longleftrightarrow> finfun_Ball A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. A $ x \<longrightarrow> P x) = finfun_Ball A P
[PROOF STEP]
by(simp add: finfun_Ball_def)


[STATEMENT]
lemma iso_finfun_Bex_Bex:
  "(\<exists>x. A $ x \<and> P x) \<longleftrightarrow> finfun_Bex A P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. A $ x \<and> P x) = finfun_Bex A P
[PROOF STEP]
by(simp add: finfun_Bex_def)


[STATEMENT]
lemma [iff]: "(s -Do f\<rightarrow> t) = (t \<in> f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -Do f\<rightarrow> t) = (t \<in> f s)
[PROOF STEP]
by(auto elim: exec.cases intro:exec.intros)


[STATEMENT]
lemma [iff]: "(s -c;d\<rightarrow> u) = (\<exists>t. s -c\<rightarrow> t \<and> t -d\<rightarrow> u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -c; d\<rightarrow> u) = (\<exists>t. s -c\<rightarrow> t \<and> t -d\<rightarrow> u)
[PROOF STEP]
by(auto elim: exec.cases intro:exec.intros)


[STATEMENT]
lemma [iff]: "(s -IF b THEN c ELSE d\<rightarrow> t) =
              (s -if b s then c else d\<rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -IF b THEN c ELSE d\<rightarrow> t) = (s -if b s then c else d\<rightarrow> t)
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s -IF b THEN c ELSE d\<rightarrow> t \<Longrightarrow> s -if b s then c else d\<rightarrow> t
 2. s -if b s then c else d\<rightarrow> t \<Longrightarrow> s -IF b THEN c ELSE d\<rightarrow> t
[PROOF STEP]
apply(auto elim: exec.cases intro:exec.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s -if b s then c else d\<rightarrow> t \<Longrightarrow> s -IF b THEN c ELSE d\<rightarrow> t
[PROOF STEP]
apply(auto intro:exec.intros split:if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma unfold_while:
 "(s -WHILE b DO c\<rightarrow> u) =
  (s -IF b THEN c;WHILE b DO c ELSE Do(\<lambda>s. {s})\<rightarrow> u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -WHILE b DO c\<rightarrow> u) = (s -IF b THEN c; WHILE b DO c ELSE Do (\<lambda>s. {s})\<rightarrow> u)
[PROOF STEP]
by(auto elim: exec.cases intro:exec.intros split:if_split_asm)


[STATEMENT]
lemma [iff]: "(s -CALL\<rightarrow> t) = (s -body\<rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -CALL\<rightarrow> t) = (s -body\<rightarrow> t)
[PROOF STEP]
by(blast elim: exec.cases intro:exec.intros)


[STATEMENT]
lemma [iff]: "(s -LOCAL f; c; g\<rightarrow> u) = (\<exists>t. f s -c\<rightarrow> t \<and> u = g s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -LOCAL f; c; g\<rightarrow> u) = (\<exists>t. f s -c\<rightarrow> t \<and> u = g s t)
[PROOF STEP]
by(fastforce elim: exec.cases intro:exec.intros)


[STATEMENT]
lemma [simp]: "\<not>b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
[PROOF STEP]
by(fast intro:exec.intros)


[STATEMENT]
lemma WhileI: "\<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
[PROOF STEP]
by(fastforce elim:exec.WhileTrue)


[STATEMENT]
lemma [iff]: "(s -Do f-n\<rightarrow> t) = (t \<in> f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -Do f-n\<rightarrow> t) = (t \<in> f s)
[PROOF STEP]
by(auto elim: execn.cases intro:execn.intros)


[STATEMENT]
lemma [iff]: "(s -c1;c2-n\<rightarrow> u) = (\<exists>t. s -c1-n\<rightarrow> t \<and> t -c2-n\<rightarrow> u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -c1; c2-n\<rightarrow> u) = (\<exists>t. s -c1-n\<rightarrow> t \<and> t -c2-n\<rightarrow> u)
[PROOF STEP]
by(best elim: execn.cases intro:execn.intros)


[STATEMENT]
lemma [iff]: "(s -IF b THEN c ELSE d-n\<rightarrow> t) =
              (s -if b s then c else d-n\<rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -IF b THEN c ELSE d-n\<rightarrow> t) = (s -if b s then c else d-n\<rightarrow> t)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>b s; s -IF b THEN c ELSE d-n\<rightarrow> t\<rbrakk> \<Longrightarrow> s -c-n\<rightarrow> t
 2. \<lbrakk>b s; s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c ELSE d-n\<rightarrow> t
 3. \<lbrakk>\<not> b s; s -IF b THEN c ELSE d-n\<rightarrow> t\<rbrakk> \<Longrightarrow> s -d-n\<rightarrow> t
 4. \<lbrakk>\<not> b s; s -d-n\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c ELSE d-n\<rightarrow> t
[PROOF STEP]
apply(blast elim: execn.cases intro:execn.intros)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [iff]: "(s -CALL- 0\<rightarrow> t) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -CALL-0\<rightarrow> t) = False
[PROOF STEP]
by(blast elim: execn.cases intro:execn.intros)


[STATEMENT]
lemma [iff]: "(s -CALL-Suc n\<rightarrow> t) = (s -body-n\<rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -CALL-Suc n\<rightarrow> t) = (s -body-n\<rightarrow> t)
[PROOF STEP]
by(blast elim: execn.cases intro:execn.intros)


[STATEMENT]
lemma [iff]: "(s -LOCAL f; c; g-n\<rightarrow> u) = (\<exists>t. f s -c-n\<rightarrow> t \<and> u = g s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -LOCAL f; c; g-n\<rightarrow> u) = (\<exists>t. f s -c-n\<rightarrow> t \<and> u = g s t)
[PROOF STEP]
by(auto elim: execn.cases intro:execn.intros)


[STATEMENT]
lemma exec_mono[rule_format]: "s -c-m\<rightarrow> t \<Longrightarrow> \<forall>n. m \<le> n \<longrightarrow> s -c-n\<rightarrow> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s -c-m\<rightarrow> t \<Longrightarrow> \<forall>n\<ge>m. s -c-n\<rightarrow> t
[PROOF STEP]
apply(erule execn.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>t f s n. t \<in> f s \<Longrightarrow> \<forall>na\<ge>n. s -Do f-na\<rightarrow> t
 2. \<And>s0 c1 n s1 c2 s2. \<lbrakk>s0 -c1-n\<rightarrow> s1; \<forall>na\<ge>n. s0 -c1-na\<rightarrow> s1; s1 -c2-n\<rightarrow> s2; \<forall>na\<ge>n. s1 -c2-na\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s0 -c1; c2-na\<rightarrow> s2
 3. \<And>b s c1 n t c2. \<lbrakk>b s; s -c1-n\<rightarrow> t; \<forall>na\<ge>n. s -c1-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 4. \<And>b s c2 n t c1. \<lbrakk>\<not> b s; s -c2-n\<rightarrow> t; \<forall>na\<ge>n. s -c2-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 5. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> s
 6. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 7. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 8. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>s0 c1 n s1 c2 s2. \<lbrakk>s0 -c1-n\<rightarrow> s1; \<forall>na\<ge>n. s0 -c1-na\<rightarrow> s1; s1 -c2-n\<rightarrow> s2; \<forall>na\<ge>n. s1 -c2-na\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s0 -c1; c2-na\<rightarrow> s2
 2. \<And>b s c1 n t c2. \<lbrakk>b s; s -c1-n\<rightarrow> t; \<forall>na\<ge>n. s -c1-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 3. \<And>b s c2 n t c1. \<lbrakk>\<not> b s; s -c2-n\<rightarrow> t; \<forall>na\<ge>n. s -c2-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 4. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> s
 5. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 6. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 7. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>b s c1 n t c2. \<lbrakk>b s; s -c1-n\<rightarrow> t; \<forall>na\<ge>n. s -c1-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 2. \<And>b s c2 n t c1. \<lbrakk>\<not> b s; s -c2-n\<rightarrow> t; \<forall>na\<ge>n. s -c2-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 3. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> s
 4. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 5. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 6. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b s c2 n t c1. \<lbrakk>\<not> b s; s -c2-n\<rightarrow> t; \<forall>na\<ge>n. s -c2-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -IF b THEN c1 ELSE c2-na\<rightarrow> t
 2. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> s
 3. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 4. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 5. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> s
 2. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 3. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 4. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(simp add:execn.intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>na\<ge>n. s -c-na\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u; \<forall>na\<ge>n. t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -WHILE b DO c-na\<rightarrow> u
 2. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 3. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(blast intro:execn.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>Suc n. s -CALL-na\<rightarrow> t
 2. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n t na. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t; Suc n \<le> na\<rbrakk> \<Longrightarrow> s -CALL-na\<rightarrow> t
 2. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(rename_tac m)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n t m. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t; Suc n \<le> m\<rbrakk> \<Longrightarrow> s -CALL-m\<rightarrow> t
 2. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply(case_tac m)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s n t m. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t; Suc n \<le> m; m = 0\<rbrakk> \<Longrightarrow> s -CALL-m\<rightarrow> t
 2. \<And>s n t m nat. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t; Suc n \<le> m; m = Suc nat\<rbrakk> \<Longrightarrow> s -CALL-m\<rightarrow> t
 3. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s n t m nat. \<lbrakk>s -body-n\<rightarrow> t; \<forall>na\<ge>n. s -body-na\<rightarrow> t; Suc n \<le> m; m = Suc nat\<rbrakk> \<Longrightarrow> s -CALL-m\<rightarrow> t
 2. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>na\<ge>n. f s -c-na\<rightarrow> t\<rbrakk> \<Longrightarrow> \<forall>na\<ge>n. s -LOCAL f; c; g-na\<rightarrow> g s t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exec_iff_execn: "(s -c\<rightarrow> t) = (\<exists>n. s -c-n\<rightarrow> t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s -c\<rightarrow> t) = (\<exists>n. s -c-n\<rightarrow> t)
[PROOF STEP]
apply(rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. s -c\<rightarrow> t \<Longrightarrow> \<exists>n. s -c-n\<rightarrow> t
 2. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(erule exec.induct)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>t f s. t \<in> f s \<Longrightarrow> \<exists>n. s -Do f-n\<rightarrow> t
 2. \<And>s0 c1 s1 c2 s2. \<lbrakk>s0 -c1\<rightarrow> s1; \<exists>n. s0 -c1-n\<rightarrow> s1; s1 -c2\<rightarrow> s2; \<exists>n. s1 -c2-n\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<exists>n. s0 -c1; c2-n\<rightarrow> s2
 3. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 4. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 5. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 6. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 7. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 8. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 9. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s0 c1 s1 c2 s2. \<lbrakk>s0 -c1\<rightarrow> s1; \<exists>n. s0 -c1-n\<rightarrow> s1; s1 -c2\<rightarrow> s2; \<exists>n. s1 -c2-n\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<exists>n. s0 -c1; c2-n\<rightarrow> s2
 2. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 3. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 4. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 5. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 6. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 7. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 8. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s0 c1 s1 c2 s2 n na. \<lbrakk>s0 -c1\<rightarrow> s1; s1 -c2\<rightarrow> s2; s0 -c1-n\<rightarrow> s1; s1 -c2-na\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<exists>n. s0 -c1; c2-n\<rightarrow> s2
 2. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 3. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 4. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 5. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 6. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 7. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 8. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(rename_tac m n)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s0 c1 s1 c2 s2 m n. \<lbrakk>s0 -c1\<rightarrow> s1; s1 -c2\<rightarrow> s2; s0 -c1-m\<rightarrow> s1; s1 -c2-n\<rightarrow> s2\<rbrakk> \<Longrightarrow> \<exists>n. s0 -c1; c2-n\<rightarrow> s2
 2. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 3. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 4. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 5. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 6. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 7. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 8. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(rule_tac x = "max m n" in exI)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>s0 c1 s1 c2 s2 m n. \<lbrakk>s0 -c1\<rightarrow> s1; s1 -c2\<rightarrow> s2; s0 -c1-m\<rightarrow> s1; s1 -c2-n\<rightarrow> s2\<rbrakk> \<Longrightarrow> s0 -c1; c2-max m n\<rightarrow> s2
 2. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 3. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 4. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 5. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 6. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 7. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 8. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(fastforce intro:exec.intros exec_mono simp add:max_def)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>b s c1 t c2. \<lbrakk>b s; s -c1\<rightarrow> t; \<exists>n. s -c1-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 2. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 3. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 4. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 5. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 6. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 7. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>b s c2 t c1. \<lbrakk>\<not> b s; s -c2\<rightarrow> t; \<exists>n. s -c2-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -IF b THEN c1 ELSE c2-n\<rightarrow> t
 2. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 3. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 4. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 5. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 6. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>b s c. \<not> b s \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> s
 2. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 3. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 4. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 5. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(blast intro:execn.intros)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c t u. \<lbrakk>b s; s -c\<rightarrow> t; \<exists>n. s -c-n\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; \<exists>n. t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 2. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 3. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 4. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c t u n na. \<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; s -c-n\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 2. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 3. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 4. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(rename_tac m n)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c t u m n. \<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; s -c-m\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> \<exists>n. s -WHILE b DO c-n\<rightarrow> u
 2. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 3. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 4. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(rule_tac x = "max m n" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>b s c t u m n. \<lbrakk>b s; s -c\<rightarrow> t; t -WHILE b DO c\<rightarrow> u; s -c-m\<rightarrow> t; t -WHILE b DO c-n\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c-max m n\<rightarrow> u
 2. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 3. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 4. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(fastforce elim:execn.WhileTrue exec_mono simp add:max_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s t. \<lbrakk>s -body\<rightarrow> t; \<exists>n. s -body-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -CALL-n\<rightarrow> t
 2. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 3. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f s c t g. \<lbrakk>f s -c\<rightarrow> t; \<exists>n. f s -c-n\<rightarrow> t\<rbrakk> \<Longrightarrow> \<exists>n. s -LOCAL f; c; g-n\<rightarrow> g s t
 2. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>n. s -c-n\<rightarrow> t \<Longrightarrow> s -c\<rightarrow> t
[PROOF STEP]
apply(erule exE, erule execn.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>n t f s na. t \<in> f s \<Longrightarrow> s -Do f\<rightarrow> t
 2. \<And>n s0 c1 na s1 c2 s2. \<lbrakk>s0 -c1-na\<rightarrow> s1; s0 -c1\<rightarrow> s1; s1 -c2-na\<rightarrow> s2; s1 -c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> s0 -c1; c2\<rightarrow> s2
 3. \<And>n b s c1 na t c2. \<lbrakk>b s; s -c1-na\<rightarrow> t; s -c1\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 4. \<And>n b s c2 na t c1. \<lbrakk>\<not> b s; s -c2-na\<rightarrow> t; s -c2\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 5. \<And>n b s c na. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
 6. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 7. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 8. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>n s0 c1 na s1 c2 s2. \<lbrakk>s0 -c1-na\<rightarrow> s1; s0 -c1\<rightarrow> s1; s1 -c2-na\<rightarrow> s2; s1 -c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> s0 -c1; c2\<rightarrow> s2
 2. \<And>n b s c1 na t c2. \<lbrakk>b s; s -c1-na\<rightarrow> t; s -c1\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 3. \<And>n b s c2 na t c1. \<lbrakk>\<not> b s; s -c2-na\<rightarrow> t; s -c2\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 4. \<And>n b s c na. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
 5. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 6. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 7. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>n b s c1 na t c2. \<lbrakk>b s; s -c1-na\<rightarrow> t; s -c1\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 2. \<And>n b s c2 na t c1. \<lbrakk>\<not> b s; s -c2-na\<rightarrow> t; s -c2\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 3. \<And>n b s c na. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
 4. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 5. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 6. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n b s c2 na t c1. \<lbrakk>\<not> b s; s -c2-na\<rightarrow> t; s -c2\<rightarrow> t\<rbrakk> \<Longrightarrow> s -IF b THEN c1 ELSE c2\<rightarrow> t
 2. \<And>n b s c na. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
 3. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 4. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 5. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n b s c na. \<not> b s \<Longrightarrow> s -WHILE b DO c\<rightarrow> s
 2. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 3. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 4. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply(erule exec.WhileFalse)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n b s c na t u. \<lbrakk>b s; s -c-na\<rightarrow> t; s -c\<rightarrow> t; t -WHILE b DO c-na\<rightarrow> u; t -WHILE b DO c\<rightarrow> u\<rbrakk> \<Longrightarrow> s -WHILE b DO c\<rightarrow> u
 2. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 3. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply(blast intro: exec.intros)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n s na t. \<lbrakk>s -body-na\<rightarrow> t; s -body\<rightarrow> t\<rbrakk> \<Longrightarrow> s -CALL\<rightarrow> t
 2. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n f s c na t g. \<lbrakk>f s -c-na\<rightarrow> t; f s -c\<rightarrow> t\<rbrakk> \<Longrightarrow> s -LOCAL f; c; g\<rightarrow> g s t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma while_lemma[rule_format]:
"s -w-n\<rightarrow> t \<Longrightarrow> \<forall>b c. w = WHILE b DO c \<and> P s \<and>
                    (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not>b t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s -w-n\<rightarrow> t \<Longrightarrow> \<forall>b c. w = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t
[PROOF STEP]
apply(erule execn.induct)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>t f s n. t \<in> f s \<Longrightarrow> \<forall>b c. Do f = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t
 2. \<And>s0 c1 n s1 c2 s2. \<lbrakk>s0 -c1-n\<rightarrow> s1; \<forall>b c. c1 = WHILE b DO c \<and> P s0 \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P s1 \<and> \<not> b s1; s1 -c2-n\<rightarrow> s2; \<forall>b c. c2 = WHILE b DO c \<and> P s1 \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P s2 \<and> \<not> b s2\<rbrakk> \<Longrightarrow> \<forall>b c. (c1; c2) = WHILE b DO c \<and> P s0 \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P s2 \<and> \<not> b s2
 3. \<And>b s c1 n t c2. \<lbrakk>b s; s -c1-n\<rightarrow> t; \<forall>b c. c1 = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>ba c. IF b THEN c1 ELSE c2 = WHILE ba DO c \<and> P s \<and> (\<forall>s s'. P s \<and> ba s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> ba t
 4. \<And>b s c2 n t c1. \<lbrakk>\<not> b s; s -c2-n\<rightarrow> t; \<forall>b c. c2 = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>ba c. IF b THEN c1 ELSE c2 = WHILE ba DO c \<and> P s \<and> (\<forall>s s'. P s \<and> ba s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> ba t
 5. \<And>b s c n. \<not> b s \<Longrightarrow> \<forall>ba ca. WHILE b DO c = WHILE ba DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P s \<and> \<not> ba s
 6. \<And>b s c n t u. \<lbrakk>b s; s -c-n\<rightarrow> t; \<forall>b ca. c = WHILE b DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE b DO c-n\<rightarrow> u; \<forall>ba ca. WHILE b DO c = WHILE ba DO ca \<and> P t \<and> (\<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> ba u\<rbrakk> \<Longrightarrow> \<forall>ba ca. WHILE b DO c = WHILE ba DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> ba u
 7. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>b c. body = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b c. CALL = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-Suc n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t
 8. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>b ca. c = WHILE b DO ca \<and> P (f s) \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b ca. LOCAL f; c; g = WHILE b DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P (g s t) \<and> \<not> b (g s t)
[PROOF STEP]
apply clarify+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'\<rbrakk> \<Longrightarrow> P u \<and> \<not> ba u
 2. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>b c. body = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b c. CALL = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-Suc n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t
 3. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>b ca. c = WHILE b DO ca \<and> P (f s) \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b ca. LOCAL f; c; g = WHILE b DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P (g s t) \<and> \<not> b (g s t)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s n t. \<lbrakk>s -body-n\<rightarrow> t; \<forall>b c. body = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b c. CALL = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-Suc n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t
 2. \<And>f s c n t g. \<lbrakk>f s -c-n\<rightarrow> t; \<forall>b ca. c = WHILE b DO ca \<and> P (f s) \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t\<rbrakk> \<Longrightarrow> \<forall>b ca. LOCAL f; c; g = WHILE b DO ca \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P (g s t) \<and> \<not> b (g s t)
 3. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'\<rbrakk> \<Longrightarrow> P u \<and> \<not> ba u
[PROOF STEP]
apply clarify+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'\<rbrakk> \<Longrightarrow> P u \<and> \<not> ba u
[PROOF STEP]
apply(subgoal_tac "P t")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'; P t\<rbrakk> \<Longrightarrow> P u \<and> \<not> ba u
 2. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b s c n t u ba ca. \<lbrakk>ba s; s -ca-n\<rightarrow> t; \<forall>b c. ca = WHILE b DO c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P t \<and> \<not> b t; t -WHILE ba DO ca-n\<rightarrow> u; \<forall>b c. WHILE ba DO ca = WHILE b DO c \<and> P t \<and> (\<forall>s s'. P s \<and> b s \<and> s -c-n\<rightarrow> s' \<longrightarrow> P s') \<longrightarrow> P u \<and> \<not> b u; P s; \<forall>s s'. P s \<and> ba s \<and> s -ca-n\<rightarrow> s' \<longrightarrow> P s'\<rbrakk> \<Longrightarrow> P t
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma while_rule:
 "\<lbrakk>s -WHILE b DO c-n\<rightarrow> t; P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s' \<rbrakk> \<Longrightarrow> P s'\<rbrakk>
  \<Longrightarrow> P t \<and> \<not>b t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s -WHILE b DO c-n\<rightarrow> t; P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'\<rbrakk> \<Longrightarrow> P t \<and> \<not> b t
[PROOF STEP]
apply(drule while_lemma)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'\<rbrakk> \<Longrightarrow> WHILE b DO c = WHILE ?b DO ?c \<and> ?P s \<and> (\<forall>s s'. ?P s \<and> ?b s \<and> s -?c-n\<rightarrow> s' \<longrightarrow> ?P s')
 2. \<lbrakk>P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'; ?P t \<and> \<not> ?b t\<rbrakk> \<Longrightarrow> P t \<and> \<not> b t
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'; ?P t \<and> \<not> ?b t\<rbrakk> \<Longrightarrow> P t \<and> \<not> b t
 2. \<lbrakk>P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'\<rbrakk> \<Longrightarrow> WHILE b DO c = WHILE ?b DO ?c \<and> ?P s \<and> (\<forall>s s'. ?P s \<and> ?b s \<and> s -?c-n\<rightarrow> s' \<longrightarrow> ?P s')
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; \<And>s s'. \<lbrakk>P s; b s; s -c-n\<rightarrow> s'\<rbrakk> \<Longrightarrow> P s'\<rbrakk> \<Longrightarrow> WHILE b DO c = WHILE b DO ?c \<and> P s \<and> (\<forall>s s'. P s \<and> b s \<and> s -?c-n\<rightarrow> s' \<longrightarrow> P s')
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma d_restrict_equals:
  "x = d(x) * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = d x * x
[PROOF STEP]
by (metis sup_commute d_plus_one d_restrict mult_left_one mult_right_dist_sup)


[STATEMENT]
lemma d_involutive:
  "d(d(x)) = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (d x) = d x
[PROOF STEP]
by (metis d_mult_d mult_left_one)


[STATEMENT]
lemma d_fixpoint:
  "(\<exists>y . x = d(y)) \<longleftrightarrow> x = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>y. x = d y) = (x = d x)
[PROOF STEP]
using d_involutive
[PROOF STATE]
proof (prove)
using this:
d (d ?x) = d ?x

goal (1 subgoal):
 1. (\<exists>y. x = d y) = (x = d x)
[PROOF STEP]
by auto


[STATEMENT]
lemma d_type:
  "\<forall>P . (\<forall>x . x = d(x) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x . P(d(x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>P. (\<forall>x. x = d x \<longrightarrow> P x) = (\<forall>x. P (d x))
[PROOF STEP]
by (metis d_involutive)


[STATEMENT]
lemma d_mult_sub:
  "d(x * y) \<le> d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (x * y) \<le> d x
[PROOF STEP]
by (metis d_dist_sup d_mult_d d_plus_one le_iff_sup mult_left_sub_dist_sup_left mult_1_right)


[STATEMENT]
lemma d_sub_one:
  "x \<le> 1 \<Longrightarrow> x \<le> d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> x \<le> d x
[PROOF STEP]
by (metis d_restrict_equals mult_right_isotone mult_1_right)


[STATEMENT]
lemma d_strict:
  "d(x) = bot \<longleftrightarrow> x = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x = bot) = (x = bot)
[PROOF STEP]
by (metis d_restrict_equals d_zero mult_left_zero)


[STATEMENT]
lemma d_one:
  "d(1) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (1::'a) = (1::'a)
[PROOF STEP]
by (metis d_restrict_equals mult_1_right)


[STATEMENT]
lemma d_below_one:
  "d(x) \<le> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (d x)
[PROOF STEP]
by (simp add: d_plus_one le_iff_sup)


[STATEMENT]
lemma d_isotone:
  "x \<le> y \<Longrightarrow> d(x) \<le> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> d x \<le> d y
[PROOF STEP]
by (metis d_dist_sup le_iff_sup)


[STATEMENT]
lemma d_plus_left_upper_bound:
  "d(x) \<le> d(x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<le> d (x \<squnion> y)
[PROOF STEP]
by (simp add: d_isotone)


[STATEMENT]
lemma d_export:
  "d(d(x) * y) = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (d x * y) = d x * d y
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d (d x * y) \<le> d x * d y
 2. d x * d y \<le> d (d x * y)
[PROOF STEP]
apply (metis d_below_one d_involutive d_mult_sub d_restrict_equals d_isotone d_mult_d mult_isotone mult_left_one)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * d y \<le> d (d x * y)
[PROOF STEP]
by (metis d_below_one d_sub_one coreflexive_mult_closed d_mult_d)


[STATEMENT]
lemma d_idempotent:
  "d(x) * d(x) = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent (d x)
[PROOF STEP]
by (metis d_export d_restrict_equals)


[STATEMENT]
lemma d_commutative:
  "d(x) * d(y) = d(y) * d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * d y = d y * d x
[PROOF STEP]
by (metis ils.il_inf_associative order.antisym d_export d_mult_d d_mult_sub d_one d_restrict_equals mult_isotone mult_left_one)


[STATEMENT]
lemma d_least_left_preserver:
  "x \<le> d(y) * x \<longleftrightarrow> d(x) \<le> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> d y * x) = (d x \<le> d y)
[PROOF STEP]
by (metis d_below_one d_involutive d_mult_sub d_restrict_equals order.eq_iff mult_left_isotone mult_left_one)


[STATEMENT]
lemma d_weak_locality:
  "x * y = bot \<longleftrightarrow> x * d(y) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x * y = bot) = (x * d y = bot)
[PROOF STEP]
by (metis d_mult_d d_strict)


[STATEMENT]
lemma d_sup_closed:
  "d(d(x) \<squnion> d(y)) = d(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (d x \<squnion> d y) = d x \<squnion> d y
[PROOF STEP]
by (simp add: d_involutive d_dist_sup)


[STATEMENT]
lemma d_mult_closed:
  "d(d(x) * d(y)) = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (d x * d y) = d x * d y
[PROOF STEP]
using d_export d_mult_d
[PROOF STATE]
proof (prove)
using this:
d (d ?x * ?y) = d ?x * d ?y
d (?x * ?y) = d (?x * d ?y)

goal (1 subgoal):
 1. d (d x * d y) = d x * d y
[PROOF STEP]
by auto


[STATEMENT]
lemma d_mult_left_lower_bound:
  "d(x) * d(y) \<le> d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * d y \<le> d x
[PROOF STEP]
by (metis d_export d_involutive d_mult_sub)


[STATEMENT]
lemma d_mult_greatest_lower_bound:
  "d(x) \<le> d(y) * d(z) \<longleftrightarrow> d(x) \<le> d(y) \<and> d(x) \<le> d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<le> d y * d z) = (d x \<le> d y \<and> d x \<le> d z)
[PROOF STEP]
by (metis d_commutative d_idempotent d_mult_left_lower_bound mult_isotone order_trans)


[STATEMENT]
lemma d_mult_left_absorb_sup:
  "d(x) * (d(x) \<squnion> d(y)) = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * (d x \<squnion> d y) = d x
[PROOF STEP]
by (metis sup_commute d_idempotent d_plus_one mult_left_dist_sup mult_1_right)


[STATEMENT]
lemma d_sup_left_absorb_mult:
  "d(x) \<squnion> d(x) * d(y) = d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<squnion> d x * d y = d x
[PROOF STEP]
using d_mult_left_lower_bound sup.absorb_iff1
[PROOF STATE]
proof (prove)
using this:
d ?x * d ?y \<le> d ?x
(?b \<le> ?a) = (?a \<squnion> ?b = ?a)

goal (1 subgoal):
 1. d x \<squnion> d x * d y = d x
[PROOF STEP]
by auto


[STATEMENT]
lemma d_sup_left_dist_mult:
  "d(x) \<squnion> d(y) * d(z) = (d(x) \<squnion> d(y)) * (d(x) \<squnion> d(z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<squnion> d y * d z = (d x \<squnion> d y) * (d x \<squnion> d z)
[PROOF STEP]
by (smt sup_assoc d_commutative d_idempotent d_mult_left_absorb_sup mult_left_dist_sup mult_right_dist_sup)


[STATEMENT]
lemma d_order:
  "d(x) \<le> d(y) \<longleftrightarrow> d(x) = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x \<le> d y) = (d x = d x * d y)
[PROOF STEP]
by (metis d_mult_greatest_lower_bound d_mult_left_absorb_sup le_iff_sup order_refl)


[STATEMENT]
lemma d_mult_below:
  "d(x) * y \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y \<le> y
[PROOF STEP]
by (metis sup_left_divisibility d_plus_one mult_left_one mult_right_dist_sup)


[STATEMENT]
lemma d_preserves_equation:
  "d(y) * x \<le> x * d(y) \<longleftrightarrow> d(y) * x = d(y) * x * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d y * x \<le> x * d y) = (d y * x = d y * x * d y)
[PROOF STEP]
by (simp add: d_below_one d_idempotent test_preserves_equation)


[STATEMENT]
lemma a_greatest_left_absorber:
  "a(x) * y = bot \<longleftrightarrow> a(x) \<le> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a x * y = bot) = (a x \<le> a y)
[PROOF STEP]
by (simp add: aa.l10_iff)


[STATEMENT]
lemma a_mult_d:
  "a(x * y) = a(x * d(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (x * y) = a (x * d y)
[PROOF STEP]
by (simp add: d_def aa.sba3_complement_inf_double_complement)


[STATEMENT]
lemma a_d_closed:
  "d(a(x)) = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (a x) = a x
[PROOF STEP]
by (simp add: d_def)


[STATEMENT]
lemma a_plus_left_lower_bound:
  "a(x \<squnion> y) \<le> a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (x \<squnion> y) \<le> a x
[PROOF STEP]
by (simp add: aa.l9)


[STATEMENT]
lemma a_mult_sup:
  "a(x) * (y \<squnion> x) = a(x) * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a x * (y \<squnion> x) = a x * y
[PROOF STEP]
by (simp add: aa.sba3_inf_complement_bot semiring.distrib_left)


[STATEMENT]
lemma a_3:
  "a(x) * a(y) * d(x \<squnion> y) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a x * a y * d (x \<squnion> y) = bot
[PROOF STEP]
using d_weak_locality aa.l12 aa.sba3_inf_complement_bot
[PROOF STATE]
proof (prove)
using this:
(?x * ?y = bot) = (?x * d ?y = bot)
a ?x * a ?y = a (?x \<squnion> ?y)
a ?x * ?x = bot

goal (1 subgoal):
 1. a x * a y * d (x \<squnion> y) = bot
[PROOF STEP]
by force


[STATEMENT]
lemma a_export:
  "a(a(x) * y) = d(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (a x * y) = d x \<squnion> a y
[PROOF STEP]
using a_mult_d d_def aa.sba_dual.sub_inf_def
[PROOF STATE]
proof (prove)
using this:
a (?x * ?y) = a (?x * d ?y)
d ?x = a (a ?x)
a ?x \<squnion> a ?y = a (a (a ?x) * a (a ?y))

goal (1 subgoal):
 1. a (a x * y) = d x \<squnion> a y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_fixpoint:
  "\<forall>x . (a(x) = x \<longrightarrow> (\<forall>y . y = bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. a x = x \<longrightarrow> (\<forall>y. y = bot)
[PROOF STEP]
by (metis aa.a_d.d_fully_strict aa.sba2_bot_unit aa.sup_idempotent aa.sup_right_zero_var)


[STATEMENT]
lemma a_strict:
  "a(x) = 1 \<longleftrightarrow> x = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a x = (1::'a)) = (x = bot)
[PROOF STEP]
using aa.a_d.d_fully_strict one_def
[PROOF STATE]
proof (prove)
using this:
(a (a ?x) = bot) = (?x = bot)
(1::'a) = a bot

goal (1 subgoal):
 1. (a x = (1::'a)) = (x = bot)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma d_complement_zero:
  "d(x) * a(x) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * a x = bot
[PROOF STEP]
by (simp add: aa.sba3_inf_complement_bot d_def)


[STATEMENT]
lemma a_complement_zero:
  "a(x) * d(x) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a x * d x = bot
[PROOF STEP]
by (simp add: d_def)


[STATEMENT]
lemma a_shunting_zero:
  "a(x) * d(y) = bot \<longleftrightarrow> a(x) \<le> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a x * d y = bot) = (a x \<le> a y)
[PROOF STEP]
by (simp add: aa.less_eq_inf_bot d_def)


[STATEMENT]
lemma a_antitone:
  "x \<le> y \<Longrightarrow> a(y) \<le> a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> a y \<le> a x
[PROOF STEP]
by (simp add: aa.l9)


[STATEMENT]
lemma a_mult_deMorgan:
  "a(a(x) * a(y)) = d(x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (a x * a y) = d (x \<squnion> y)
[PROOF STEP]
by (simp add: aa.sup_demorgan d_def)


[STATEMENT]
lemma a_mult_deMorgan_1:
  "a(a(x) * a(y)) = d(x) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (a x * a y) = d x \<squnion> d y
[PROOF STEP]
by (simp add: a_export d_def)


[STATEMENT]
lemma a_mult_deMorgan_2:
  "a(d(x) * d(y)) = a(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (d x * d y) = a x \<squnion> a y
[PROOF STEP]
by (simp add: d_def sup_def)


[STATEMENT]
lemma a_plus_deMorgan:
  "a(a(x) \<squnion> a(y)) = d(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (a x \<squnion> a y) = d x * d y
[PROOF STEP]
by (simp add: aa.sub_sup_demorgan d_def)


[STATEMENT]
lemma a_plus_deMorgan_1:
  "a(d(x) \<squnion> d(y)) = a(x) * a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (d x \<squnion> d y) = a x * a y
[PROOF STEP]
by (simp add: aa.sup_demorgan d_def)


[STATEMENT]
lemma a_mult_left_upper_bound:
  "a(x) \<le> a(x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a x \<le> a (x * y)
[PROOF STEP]
using aa.l5 d_def d_mult_sub
[PROOF STATE]
proof (prove)
using this:
a (a ?x) \<le> a (a ?y) \<Longrightarrow> a ?y \<le> a ?x
d ?x = a (a ?x)
d (?x * ?y) \<le> d ?x

goal (1 subgoal):
 1. a x \<le> a (x * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma d_a_closed:
  "a(d(x)) = a(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (d x) = a x
[PROOF STEP]
by (simp add: d_def)


[STATEMENT]
lemma a_export_d:
  "a(d(x) * y) = a(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (d x * y) = a x \<squnion> a y
[PROOF STEP]
using a_mult_d a_mult_deMorgan_2
[PROOF STATE]
proof (prove)
using this:
a (?x * ?y) = a (?x * d ?y)
a (d ?x * d ?y) = a ?x \<squnion> a ?y

goal (1 subgoal):
 1. a (d x * y) = a x \<squnion> a y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_7:
  "d(x) * a(d(y) \<squnion> d(z)) = d(x) * a(y) * a(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * a (d y \<squnion> d z) = d x * a y * a z
[PROOF STEP]
by (simp add: a_plus_deMorgan_1 mult_assoc)


[STATEMENT]
lemma d_a_shunting:
  "d(x) * a(y) \<le> d(z) \<longleftrightarrow> d(x) \<le> d(z) \<squnion> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * a y \<le> d z) = (d x \<le> d z \<squnion> d y)
[PROOF STEP]
using aa.sba_dual.shunting_right d_def
[PROOF STATE]
proof (prove)
using this:
(a ?z \<le> a ?x \<squnion> a ?y) = (a ?z * a (a ?y) \<le> a ?x)
d ?x = a (a ?x)

goal (1 subgoal):
 1. (d x * a y \<le> d z) = (d x \<le> d z \<squnion> d y)
[PROOF STEP]
by auto


[STATEMENT]
lemma d_d_shunting:
  "d(x) * d(y) \<le> d(z) \<longleftrightarrow> d(x) \<le> d(z) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * d y \<le> d z) = (d x \<le> d z \<squnion> a y)
[PROOF STEP]
using d_a_shunting d_def
[PROOF STATE]
proof (prove)
using this:
(d ?x * a ?y \<le> d ?z) = (d ?x \<le> d ?z \<squnion> d ?y)
d ?x = a (a ?x)

goal (1 subgoal):
 1. (d x * d y \<le> d z) = (d x \<le> d z \<squnion> a y)
[PROOF STEP]
by auto


[STATEMENT]
lemma d_cancellation_1:
  "d(x) \<le> d(y) \<squnion> (d(x) * a(y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<le> d y \<squnion> d x * a y
[PROOF STEP]
by (metis a_d_closed aa.sba2_export aa.sup_demorgan d_def eq_refl le_supE sup_commute)


[STATEMENT]
lemma d_cancellation_2:
  "(d(z) \<squnion> d(y)) * a(y) \<le> d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d z \<squnion> d y) * a y \<le> d z
[PROOF STEP]
by (metis d_a_shunting d_dist_sup eq_refl)


[STATEMENT]
lemma a_sup_closed:
  "d(a(x) \<squnion> a(y)) = a(x) \<squnion> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (a x \<squnion> a y) = a x \<squnion> a y
[PROOF STEP]
using aa.sub_sup_closed d_def
[PROOF STATE]
proof (prove)
using this:
a ?x \<squnion> a ?y = a (a (a ?x \<squnion> a ?y))
d ?x = a (a ?x)

goal (1 subgoal):
 1. d (a x \<squnion> a y) = a x \<squnion> a y
[PROOF STEP]
by auto


[STATEMENT]
lemma a_mult_closed:
  "d(a(x) * a(y)) = a(x) * a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d (a x * a y) = a x * a y
[PROOF STEP]
using a_d_closed aa.l12
[PROOF STATE]
proof (prove)
using this:
d (a ?x) = a ?x
a ?x * a ?y = a (?x \<squnion> ?y)

goal (1 subgoal):
 1. d (a x * a y) = a x * a y
[PROOF STEP]
by auto


[STATEMENT]
lemma d_a_shunting_zero:
  "d(x) * a(y) = bot \<longleftrightarrow> d(x) \<le> d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * a y = bot) = (d x \<le> d y)
[PROOF STEP]
by (simp add: aa.l10_iff d_def)


[STATEMENT]
lemma d_d_shunting_zero:
  "d(x) * d(y) = bot \<longleftrightarrow> d(x) \<le> a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * d y = bot) = (d x \<le> a y)
[PROOF STEP]
by (simp add: aa.l10_iff d_def)


[STATEMENT]
lemma d_compl_intro:
  "d(x) \<squnion> d(y) = d(x) \<squnion> a(x) * d(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<squnion> d y = d x \<squnion> a x * d y
[PROOF STEP]
by (simp add: aa.sup_complement_intro d_def)


[STATEMENT]
lemma a_compl_intro:
  "a(x) \<squnion> a(y) = a(x) \<squnion> d(x) * a(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a x \<squnion> a y = a x \<squnion> d x * a y
[PROOF STEP]
by (simp add: aa.sup_complement_intro d_def)


[STATEMENT]
lemma kat_2:
  "y * a(z) \<le> a(x) * y \<Longrightarrow> d(x) * y * a(z) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * a z \<le> a x * y \<Longrightarrow> d x * y * a z = bot
[PROOF STEP]
by (smt a_export a_plus_left_lower_bound le_sup_iff d_d_shunting_zero d_export d_strict le_iff_sup mult_assoc)


[STATEMENT]
lemma kat_3:
  "d(x) * y * a(z) = bot \<Longrightarrow> d(x) * y = d(x) * y * d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y * a z = bot \<Longrightarrow> d x * y = d x * y * d z
[PROOF STEP]
by (metis a_export_d aa.complement_bot d_complement_zero d_def mult_1_right mult_left_dist_sup sup_bot_left)


[STATEMENT]
lemma kat_4:
  "d(x) * y = d(x) * y * d(z) \<Longrightarrow> d(x) * y \<le> y * d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y = d x * y * d z \<Longrightarrow> d x * y \<le> y * d z
[PROOF STEP]
using d_mult_below mult_assoc
[PROOF STATE]
proof (prove)
using this:
d ?x * ?y \<le> ?y
?a * ?b * ?c = ?a * (?b * ?c)

goal (1 subgoal):
 1. d x * y = d x * y * d z \<Longrightarrow> d x * y \<le> y * d z
[PROOF STEP]
by auto


[STATEMENT]
lemma kat_2_equiv:
  "y * a(z) \<le> a(x) * y \<longleftrightarrow> d(x) * y * a(z) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y * a z \<le> a x * y) = (d x * y * a z = bot)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y * a z \<le> a x * y \<Longrightarrow> d x * y * a z = bot
 2. d x * y * a z = bot \<Longrightarrow> y * a z \<le> a x * y
[PROOF STEP]
apply (simp add: kat_2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y * a z = bot \<Longrightarrow> y * a z \<le> a x * y
[PROOF STEP]
by (metis aa.top_greatest a_complement sup_bot_left d_def mult_left_one mult_right_dist_sup mult_right_isotone mult_1_right)


[STATEMENT]
lemma kat_4_equiv:
  "d(x) * y = d(x) * y * d(z) \<longleftrightarrow> d(x) * y \<le> y * d(z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * y = d x * y * d z) = (d x * y \<le> y * d z)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d x * y = d x * y * d z \<Longrightarrow> d x * y \<le> y * d z
 2. d x * y \<le> y * d z \<Longrightarrow> d x * y = d x * y * d z
[PROOF STEP]
apply (simp add: kat_4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y \<le> y * d z \<Longrightarrow> d x * y = d x * y * d z
[PROOF STEP]
apply (rule order.antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. d x * y \<le> y * d z \<Longrightarrow> d x * y \<le> d x * y * d z
 2. d x * y \<le> y * d z \<Longrightarrow> d x * y * d z \<le> d x * y
[PROOF STEP]
apply (metis d_idempotent le_iff_sup mult_assoc mult_left_dist_sup)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x * y \<le> y * d z \<Longrightarrow> d x * y * d z \<le> d x * y
[PROOF STEP]
by (metis d_plus_one le_iff_sup mult_left_dist_sup mult_1_right)


[STATEMENT]
lemma kat_3_equiv_opp:
  "a(z) * y * d(x) = bot \<longleftrightarrow> y * d(x) = d(z) * y * d(x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a z * y * d x = bot) = (y * d x = d z * y * d x)
[PROOF STEP]
by (metis a_complement a_restrict sup_bot_left d_a_closed d_def mult_assoc mult_left_one mult_left_zero mult_right_dist_sup)


[STATEMENT]
lemma kat_4_equiv_opp:
  "y * d(x) = d(z) * y * d(x) \<longleftrightarrow> y * d(x) \<le> d(z) * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y * d x = d z * y * d x) = (y * d x \<le> d z * y)
[PROOF STEP]
using kat_2_equiv kat_3_equiv_opp d_def
[PROOF STATE]
proof (prove)
using this:
(?y * a ?z \<le> a ?x * ?y) = (d ?x * ?y * a ?z = bot)
(a ?z * ?y * d ?x = bot) = (?y * d ?x = d ?z * ?y * d ?x)
d ?x = a (a ?x)

goal (1 subgoal):
 1. (y * d x = d z * y * d x) = (y * d x \<le> d z * y)
[PROOF STEP]
by auto


[STATEMENT]
lemma d_restrict_iff:
  "(x \<le> y) \<longleftrightarrow> (x \<le> d(x) * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = (x \<le> d x * y)
[PROOF STEP]
by (metis d_mult_below d_restrict_equals mult_isotone order_lesseq_imp)


[STATEMENT]
lemma d_restrict_iff_1:
  "(d(x) * y \<le> z) \<longleftrightarrow> (d(x) * y \<le> d(x) * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (d x * y \<le> z) = (d x * y \<le> d x * z)
[PROOF STEP]
by (metis sup_commute d_export d_mult_left_lower_bound d_plus_one d_restrict_iff mult_left_isotone mult_left_one mult_right_sub_dist_sup_right order_trans)


[STATEMENT]
lemma show_law_real_alg [show_law_intros]:
  "show_law showsp_real_alg r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. show_law showsp_real_alg r
[PROOF STEP]
by (rule show_lawI) (simp add: showsp_real_alg_def show_law_simps)


[STATEMENT]
lemma showsp_real_alg_append [show_law_simps]:
  "showsp_real_alg p r (x @ y) = showsp_real_alg p r x @ y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. showsp_real_alg p r (x @ y) = showsp_real_alg p r x @ y
[PROOF STEP]
by (intro show_lawD show_law_intros)


[STATEMENT]
lemma is_process_REP_Skip:
" is_process ({(s, X). s = [] \<and> tick \<notin> X} \<union> {(s, X). s = [tick]}, {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_process ({(s, X). s = [] \<and> tick \<notin> X} \<union> {(s, X). s = [tick]}, {})
[PROOF STEP]
apply(auto simp: FAILURES_def DIVERGENCES_def front_tickFree_def is_process_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>s @ t = [tick]; s \<noteq> [tick]\<rbrakk> \<Longrightarrow> s = []
[PROOF STEP]
apply(erule contrapos_np,drule neq_Nil_conv[THEN iffD1], auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_process_REP_Skip2:
"is_process ({[]} \<times> {X. tick \<notin> X} \<union> {(s, X). s = [tick]}, {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_process ({[]} \<times> {X. tick \<notin> X} \<union> {(s, X). s = [tick]}, {})
[PROOF STEP]
using is_process_REP_Skip
[PROOF STATE]
proof (prove)
using this:
is_process ({(s, X). s = [] \<and> tick \<notin> X} \<union> {(s, X). s = [tick]}, {})

goal (1 subgoal):
 1. is_process ({[]} \<times> {X. tick \<notin> X} \<union> {(s, X). s = [tick]}, {})
[PROOF STEP]
by auto


[STATEMENT]
lemma F_SKIP:
"F SKIP = {(s, X). s = [] \<and> tick \<notin> X} \<union> {(s, X). s = [tick]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F SKIP = {(s, X). s = [] \<and> tick \<notin> X} \<union> {(s, X). s = [tick]}
[PROOF STEP]
by(simp add:  process_prover SKIP_def F_def is_process_REP_Skip2)


[STATEMENT]
lemma D_SKIP: "D SKIP = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D SKIP = {}
[PROOF STEP]
by(simp add:  process_prover SKIP_def D_def is_process_REP_Skip2)


[STATEMENT]
lemma T_SKIP: "T SKIP ={[],[tick]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T SKIP = {[], [tick]}
[PROOF STEP]
by(auto simp:  process_prover SKIP_def T_def is_process_REP_Skip2)


[STATEMENT]
lemma card_bit[simp]: "CARD(bit) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD(bit) = 2
[PROOF STEP]
using card_2_iff'
[PROOF STATE]
proof (prove)
using this:
(card ?S = 2) = (\<exists>x\<in>?S. \<exists>y\<in>?S. x \<noteq> y \<and> (\<forall>z\<in>?S. z = x \<or> z = y))

goal (1 subgoal):
 1. CARD(bit) = 2
[PROOF STEP]
by force


[STATEMENT]
lemma mat_of_rows_list_carrier[simp]:
  "mat_of_rows_list n vs \<in> carrier_mat (length vs) n"
  "dim_row (mat_of_rows_list n vs) = length vs"
  "dim_col (mat_of_rows_list n vs) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows_list n vs \<in> carrier_mat (length vs) n &&& dim_row (mat_of_rows_list n vs) = length vs &&& dim_col (mat_of_rows_list n vs) = n
[PROOF STEP]
unfolding mat_of_rows_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (length vs) n (\<lambda>(i, y). vs ! i ! y) \<in> carrier_mat (length vs) n &&& dim_row (mat (length vs) n (\<lambda>(i, y). vs ! i ! y)) = length vs &&& dim_col (mat (length vs) n (\<lambda>(i, y). vs ! i ! y)) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma apply_id_cblinfun[simp]: \<open>(*\<^sub>V) id_cblinfun = id\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (*\<^sub>V) id_cblinfun = id
[PROOF STEP]
by auto


[STATEMENT]
lemma clinear_sandwich[simp]: \<open>clinear (sandwich a)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. clinear (Misc.sandwich a)
[PROOF STEP]
apply (rule clinearI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>b1 b2. Misc.sandwich a (b1 + b2) = Misc.sandwich a b1 + Misc.sandwich a b2
 2. \<And>r b. Misc.sandwich a (r *\<^sub>C b) = r *\<^sub>C Misc.sandwich a b
[PROOF STEP]
apply (simp add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right sandwich_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r b. Misc.sandwich a (r *\<^sub>C b) = r *\<^sub>C Misc.sandwich a b
[PROOF STEP]
by (simp add: sandwich_def)


[STATEMENT]
lemma sandwich_id[simp]: \<open>sandwich id_cblinfun = id\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Misc.sandwich id_cblinfun = id
[PROOF STEP]
by (auto simp: sandwich_def)


[STATEMENT]
lemma mat_of_cblinfun_sandwich:
  fixes a :: "(_::onb_enum, _::onb_enum) cblinfun"
  shows \<open>mat_of_cblinfun (sandwich a b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_cblinfun (Misc.sandwich a b) = (let a' = mat_of_cblinfun a in a' * mat_of_cblinfun b * mat_adjoint a')
[PROOF STEP]
by (simp add: mat_of_cblinfun_compose sandwich_def Let_def mat_of_cblinfun_adj)


[STATEMENT]
lemma prod_cases3' [cases type]:
  obtains (fields) a b c where "y = ((a, b), c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c. y = ((a, b), c) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases y, case_tac a) blast


[STATEMENT]
lemma lift_cblinfun_comp:
  assumes \<open>a o\<^sub>C\<^sub>L b = c\<close>
  shows \<open>a o\<^sub>C\<^sub>L b = c\<close>
    and \<open>a o\<^sub>C\<^sub>L (b o\<^sub>C\<^sub>L d) = c o\<^sub>C\<^sub>L d\<close>
    and \<open>a *\<^sub>S (b *\<^sub>S S) = c *\<^sub>S S\<close>
    and \<open>a *\<^sub>V (b *\<^sub>V x) = c *\<^sub>V x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a o\<^sub>C\<^sub>L b = c &&& a o\<^sub>C\<^sub>L (b o\<^sub>C\<^sub>L d) = c o\<^sub>C\<^sub>L d) &&& a *\<^sub>S b *\<^sub>S S = c *\<^sub>S S &&& a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
apply (fact assms)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a o\<^sub>C\<^sub>L (b o\<^sub>C\<^sub>L d) = c o\<^sub>C\<^sub>L d
 2. a *\<^sub>S b *\<^sub>S S = c *\<^sub>S S
 3. a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
apply (simp add: assms cblinfun_assoc_left(1))
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a *\<^sub>S b *\<^sub>S S = c *\<^sub>S S
 2. a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
using assms cblinfun_assoc_left(2)
[PROOF STATE]
proof (prove)
using this:
a o\<^sub>C\<^sub>L b = c
?A *\<^sub>S ?B *\<^sub>S ?S = (?A o\<^sub>C\<^sub>L ?B) *\<^sub>S ?S

goal (2 subgoals):
 1. a *\<^sub>S b *\<^sub>S S = c *\<^sub>S S
 2. a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a o\<^sub>C\<^sub>L b = c

goal (1 subgoal):
 1. a *\<^sub>V b *\<^sub>V x = c *\<^sub>V x
[PROOF STEP]
by force


[STATEMENT]
lemma enum_inj:
  assumes "i < CARD('a)" and "j < CARD('a)"
  shows "(Enum.enum ! i :: 'a::enum) = Enum.enum ! j \<longleftrightarrow> i = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (enum_class.enum ! i = enum_class.enum ! j) = (i = j)
[PROOF STEP]
using inj_on_nth[OF enum_distinct, where I=\<open>{..<CARD('a)}\<close>]
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{..<CARD('a)}. i < length enum_class.enum \<Longrightarrow> inj_on ((!) enum_class.enum) {..<CARD('a)}

goal (1 subgoal):
 1. (enum_class.enum ! i = enum_class.enum ! j) = (i = j)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{..<CARD('a)}. i < length enum_class.enum \<Longrightarrow> inj_on ((!) enum_class.enum) {..<CARD('a)}
i < CARD('a)
j < CARD('a)

goal (1 subgoal):
 1. (enum_class.enum ! i = enum_class.enum ! j) = (i = j)
[PROOF STEP]
by (auto dest: inj_onD simp flip: card_UNIV_length_enum)


[STATEMENT]
lemma [simp]: "dim_col (mat_adjoint m) = dim_row m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat_adjoint m) = dim_row m
[PROOF STEP]
unfolding mat_adjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (mat_of_rows (dim_row m) (map conjugate (cols m))) = dim_row m
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "dim_row (mat_adjoint m) = dim_col m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_adjoint m) = dim_col m
[PROOF STEP]
unfolding mat_adjoint_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_rows (dim_row m) (map conjugate (cols m))) = dim_col m
[PROOF STEP]
by simp


[STATEMENT]
lemma invI:
  assumes \<open>inj f\<close>
  assumes \<open>x = f y\<close>
  shows \<open>inv f x = y\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv f x = y
[PROOF STEP]
by (simp add: assms(1) assms(2))


[STATEMENT]
lemma surj_from_comp:
  assumes \<open>surj (g o f)\<close>
  assumes \<open>inj g\<close>
  shows \<open>surj f\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surj f
[PROOF STEP]
by (metis assms(1) assms(2) f_inv_into_f fun.set_map inj_image_mem_iff iso_tuple_UNIV_I surj_iff_all)


[STATEMENT]
lemma double_exists: \<open>(\<exists>x y. Q x y) \<longleftrightarrow> (\<exists>z. Q (fst z) (snd z))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x y. Q x y) = (\<exists>z. Q (fst z) (snd z))
[PROOF STEP]
by simp


[STATEMENT]
lemma x_leq_triple_x:
  "x \<le> x;x\<^sup>T;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
have "x = x;1' \<cdot> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x ; 1' \<cdot> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = x ; 1' \<cdot> 1

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x = x ; 1' \<cdot> 1

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
have "... \<le> (x \<cdot> 1;1'\<^sup>T);(1' \<cdot> x\<^sup>T;1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; 1' \<cdot> 1 \<le> (x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1)
[PROOF STEP]
by (rule dedekind)
[PROOF STATE]
proof (state)
this:
x ; 1' \<cdot> 1 \<le> (x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1)

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x ; 1' \<cdot> 1 \<le> (x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1)

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
have "... = x;(x\<^sup>T;1 \<cdot> 1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1) = x ; (x\<^sup>T ; 1 \<cdot> 1')
[PROOF STEP]
by (simp add: inf.commute)
[PROOF STATE]
proof (state)
this:
(x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1) = x ; (x\<^sup>T ; 1 \<cdot> 1')

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<cdot> 1 ; 1'\<^sup>T) ; (1' \<cdot> x\<^sup>T ; 1) = x ; (x\<^sup>T ; 1 \<cdot> 1')

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
have "... \<le> x;(x\<^sup>T \<cdot> 1';1\<^sup>T);(1 \<cdot> (x\<^sup>T)\<^sup>T;1')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; (x\<^sup>T ; 1 \<cdot> 1') \<le> x ; (x\<^sup>T \<cdot> 1' ; 1\<^sup>T) ; (1 \<cdot> (x\<^sup>T)\<^sup>T ; 1')
[PROOF STEP]
by (metis comp_assoc dedekind mult_isol)
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>T ; 1 \<cdot> 1') \<le> x ; (x\<^sup>T \<cdot> 1' ; 1\<^sup>T) ; (1 \<cdot> (x\<^sup>T)\<^sup>T ; 1')

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>T ; 1 \<cdot> 1') \<le> x ; (x\<^sup>T \<cdot> 1' ; 1\<^sup>T) ; (1 \<cdot> (x\<^sup>T)\<^sup>T ; 1')

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
have "... \<le> x;x\<^sup>T;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x ; (x\<^sup>T \<cdot> 1' ; 1\<^sup>T) ; (1 \<cdot> (x\<^sup>T)\<^sup>T ; 1') \<le> x ; x\<^sup>T ; x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x ; (x\<^sup>T \<cdot> 1' ; 1\<^sup>T) ; (1 \<cdot> (x\<^sup>T)\<^sup>T ; 1') \<le> x ; x\<^sup>T ; x

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<le> x ; x\<^sup>T ; x

goal (1 subgoal):
 1. x \<le> x ; x\<^sup>T ; x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<le> x ; x\<^sup>T ; x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_triple:
  assumes "is_inj x"
    shows "x = x;x\<^sup>T;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x ; x\<^sup>T ; x
[PROOF STEP]
by (metis assms order.eq_iff inf_absorb2 is_inj_def mult_1_left mult_subdistr x_leq_triple_x)


[STATEMENT]
lemma p_fun_triple:
  assumes "is_p_fun x"
    shows "x = x;x\<^sup>T;x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = x ; x\<^sup>T ; x
[PROOF STEP]
by (metis assms comp_assoc order.eq_iff is_p_fun_def mult_isol mult_oner x_leq_triple_x)


[STATEMENT]
lemma loop_backward_forward:
  "x\<^sup>T \<le> -(1') + x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>T \<le> - 1' + x
[PROOF STEP]
by (metis conv_e conv_times inf.cobounded2 test_dom test_domain test_eq_conv galois_2 inf.commute
           sup.commute)


[STATEMENT]
lemma inj_sur_semi_swap:
  assumes "is_sur z"
      and "is_inj x"
    shows "z \<le> y;x \<Longrightarrow> x \<le> y\<^sup>T;z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
assume "z \<le> y;x"
[PROOF STATE]
proof (state)
this:
z \<le> y ; x

goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
hence "z;x\<^sup>T \<le> y;(x;x\<^sup>T)"
[PROOF STATE]
proof (prove)
using this:
z \<le> y ; x

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y ; (x ; x\<^sup>T)
[PROOF STEP]
by (metis mult_isor mult_assoc)
[PROOF STATE]
proof (state)
this:
z ; x\<^sup>T \<le> y ; (x ; x\<^sup>T)

goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
hence "z;x\<^sup>T \<le> y"
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y ; (x ; x\<^sup>T)

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y
[PROOF STEP]
using \<open>is_inj x\<close>
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y ; (x ; x\<^sup>T)
is_inj x

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y
[PROOF STEP]
unfolding is_inj_def
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y ; (x ; x\<^sup>T)
x ; x\<^sup>T \<le> 1'

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y
[PROOF STEP]
by (metis mult_isol order.trans mult_1_right)
[PROOF STATE]
proof (state)
this:
z ; x\<^sup>T \<le> y

goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
hence "(z\<^sup>T;z);x\<^sup>T \<le> z\<^sup>T;y"
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y

goal (1 subgoal):
 1. z\<^sup>T ; z ; x\<^sup>T \<le> z\<^sup>T ; y
[PROOF STEP]
by (metis mult_isol mult_assoc)
[PROOF STATE]
proof (state)
this:
z\<^sup>T ; z ; x\<^sup>T \<le> z\<^sup>T ; y

goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
hence "x\<^sup>T \<le> z\<^sup>T;y"
[PROOF STATE]
proof (prove)
using this:
z\<^sup>T ; z ; x\<^sup>T \<le> z\<^sup>T ; y

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y
[PROOF STEP]
using \<open>is_sur z\<close>
[PROOF STATE]
proof (prove)
using this:
z\<^sup>T ; z ; x\<^sup>T \<le> z\<^sup>T ; y
is_sur z

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y
[PROOF STEP]
unfolding is_sur_def
[PROOF STATE]
proof (prove)
using this:
z\<^sup>T ; z ; x\<^sup>T \<le> z\<^sup>T ; y
reflexive (z\<^sup>T ; z)

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y
[PROOF STEP]
by (metis mult_isor order.trans mult_1_left)
[PROOF STATE]
proof (state)
this:
x\<^sup>T \<le> z\<^sup>T ; y

goal (1 subgoal):
 1. z \<le> y ; x \<Longrightarrow> x \<le> y\<^sup>T ; z
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T \<le> z\<^sup>T ; y

goal (1 subgoal):
 1. x \<le> y\<^sup>T ; z
[PROOF STEP]
using conv_iso
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T \<le> z\<^sup>T ; y
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

goal (1 subgoal):
 1. x \<le> y\<^sup>T ; z
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<le> y\<^sup>T ; z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_sur_semi_swap_short:
  assumes "is_sur z"
      and "is_inj x"
    shows "z \<le> y\<^sup>T;x \<Longrightarrow> x \<le> y;z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. z \<le> y\<^sup>T ; x \<Longrightarrow> x \<le> y ; z
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<le> y\<^sup>T ; x \<Longrightarrow> x \<le> y ; z
[PROOF STEP]
assume as: "z \<le> y\<^sup>T;x"
[PROOF STATE]
proof (state)
this:
z \<le> y\<^sup>T ; x

goal (1 subgoal):
 1. z \<le> y\<^sup>T ; x \<Longrightarrow> x \<le> y ; z
[PROOF STEP]
hence "z;x\<^sup>T \<le> y\<^sup>T"
[PROOF STATE]
proof (prove)
using this:
z \<le> y\<^sup>T ; x

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y\<^sup>T
[PROOF STEP]
using \<open>z \<le> y\<^sup>T;x\<close> \<open>is_inj x\<close>
[PROOF STATE]
proof (prove)
using this:
z \<le> y\<^sup>T ; x
z \<le> y\<^sup>T ; x
is_inj x

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y\<^sup>T
[PROOF STEP]
unfolding is_inj_def
[PROOF STATE]
proof (prove)
using this:
z \<le> y\<^sup>T ; x
z \<le> y\<^sup>T ; x
x ; x\<^sup>T \<le> 1'

goal (1 subgoal):
 1. z ; x\<^sup>T \<le> y\<^sup>T
[PROOF STEP]
by (metis assms(2) conv_invol inf.orderI inf_absorb1 inj_p_fun ss_422iii)
[PROOF STATE]
proof (state)
this:
z ; x\<^sup>T \<le> y\<^sup>T

goal (1 subgoal):
 1. z \<le> y\<^sup>T ; x \<Longrightarrow> x \<le> y ; z
[PROOF STEP]
hence "x\<^sup>T \<le> z\<^sup>T;y\<^sup>T"
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y\<^sup>T

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T
[PROOF STEP]
using \<open>is_sur z\<close>
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y\<^sup>T
is_sur z

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T
[PROOF STEP]
unfolding is_sur_def
[PROOF STATE]
proof (prove)
using this:
z ; x\<^sup>T \<le> y\<^sup>T
reflexive (z\<^sup>T ; z)

goal (1 subgoal):
 1. x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T
[PROOF STEP]
by (metis as assms inj_sur_semi_swap conv_contrav conv_invol conv_iso)
[PROOF STATE]
proof (state)
this:
x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T

goal (1 subgoal):
 1. z \<le> y\<^sup>T ; x \<Longrightarrow> x \<le> y ; z
[PROOF STEP]
thus "x \<le> y;z"
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T

goal (1 subgoal):
 1. x \<le> y ; z
[PROOF STEP]
using conv_iso
[PROOF STATE]
proof (prove)
using this:
x\<^sup>T \<le> z\<^sup>T ; y\<^sup>T
(?x \<le> ?y) = (?x\<^sup>T \<le> ?y\<^sup>T)

goal (1 subgoal):
 1. x \<le> y ; z
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x \<le> y ; z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bij_swap:
  assumes "bijective z"
      and "bijective x"
    shows "z \<le> y\<^sup>T;x \<longleftrightarrow> x \<le> y;z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (z \<le> y\<^sup>T ; x) = (x \<le> y ; z)
[PROOF STEP]
by (metis assms inj_sur_semi_swap conv_invol)