[STATEMENT]
lemma s_sub_all_clauses: "S \<subseteq> all_clauses S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> all_clauses S
[PROOF STEP]
unfolding all_clauses_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}}
[PROOF STEP]
apply(rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<in> {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}}
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> S \<Longrightarrow> x \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}
[PROOF STEP]
apply(rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> S; xa \<in> x\<rbrakk> \<Longrightarrow> xa \<in> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}
[PROOF STEP]
apply(simp add: atoms_of_cnf_alt lit_atoms_cases[abs_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> S; xa \<in> x\<rbrakk> \<Longrightarrow> (\<exists>k. xa = k\<^sup>+ \<and> (\<exists>x\<in>S. k \<in> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x)) \<or> (\<exists>k. xa = k\<inverse> \<and> (\<exists>x\<in>S. k \<in> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x))
[PROOF STEP]
by (metis imageI literal.exhaust literal.simps(5) literal.simps(6))


[STATEMENT]
lemma atoms_res: "atoms_of_cnf (res S) \<subseteq>  atoms_of_cnf S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atoms_of_cnf (res S) \<subseteq> atoms_of_cnf S
[PROOF STEP]
unfolding res_def atoms_of_cnf_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> ((`) atoms_of_lit ` (\<Union>C1\<in>S. \<Union>C2\<in>S. \<Union>L1\<in>C1. \<Union>L2\<in>C2. case (L1, L2) of (i\<^sup>+, a\<^sup>+) \<Rightarrow> {} | (i\<^sup>+, j\<inverse>) \<Rightarrow> if i = j then {C1 - {i\<^sup>+} \<union> (C2 - {j\<inverse>})} else {} | (aa\<inverse>, b) \<Rightarrow> {})) \<subseteq> \<Union> ((`) atoms_of_lit ` S)
[PROOF STEP]
apply (clarsimp simp: lit_atoms_cases [abs_def] split: literal.splits if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xf x2. \<lbrakk>xf \<in> xa \<and> xf \<noteq> x2\<^sup>+ \<or> xf \<in> xb \<and> xf \<noteq> x2\<inverse>; xa \<in> S; xb \<in> S; x2\<^sup>+ \<in> xa; x2\<inverse> \<in> xb\<rbrakk> \<Longrightarrow> (\<forall>x1. xf = x1\<^sup>+ \<longrightarrow> (\<exists>x\<in>S. x1 \<in> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x)) \<and> (\<forall>x2. xf = x2\<inverse> \<longrightarrow> (\<exists>x\<in>S. x2 \<in> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x))
[PROOF STEP]
apply (clarsimp simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xf x2. \<lbrakk>xf \<in> xa \<and> xf \<noteq> x2\<^sup>+ \<or> xf \<in> xb \<and> xf \<noteq> x2\<inverse>; xa \<in> S; xb \<in> S; x2\<^sup>+ \<in> xa; x2\<inverse> \<in> xb\<rbrakk> \<Longrightarrow> (\<forall>x1. xf = x1\<^sup>+ \<longrightarrow> (\<exists>x\<in>S. \<exists>x\<in>x. x1 = (case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea))) \<and> (\<forall>x2. xf = x2\<inverse> \<longrightarrow> (\<exists>x\<in>S. \<exists>x\<in>x. x2 = (case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea)))
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma exlitE: "(\<And>x. xe = Pos x \<Longrightarrow> P x) \<Longrightarrow> (\<And>x. xe = Neg x \<Longrightarrow> False) \<Longrightarrow> \<exists>x. xe = Pos x \<and> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. xe = x\<^sup>+ \<Longrightarrow> P x; \<And>x. xe = x\<inverse> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> \<exists>x. xe = x\<^sup>+ \<and> P x
[PROOF STEP]
by(cases xe) auto


[STATEMENT]
lemma res_in_all_clauses: "res S \<subseteq> all_clauses S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res S \<subseteq> all_clauses S
[PROOF STEP]
apply (clarsimp simp: res_def all_clauses_def atoms_of_cnf_alt lit_atoms_cases
    split: literal.splits if_splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xe x2. \<lbrakk>\<forall>k. xe = k\<inverse> \<longrightarrow> (\<forall>x\<in>S. k \<notin> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x); xa \<in> S; xb \<in> S; x2\<^sup>+ \<in> xa; x2\<inverse> \<in> xb; xe \<in> xa \<and> xe \<noteq> x2\<^sup>+ \<or> xe \<in> xb \<and> xe \<noteq> x2\<inverse>\<rbrakk> \<Longrightarrow> \<exists>k. xe = k\<^sup>+ \<and> (\<exists>x\<in>S. k \<in> (\<lambda>x. case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea) ` x)
[PROOF STEP]
apply (clarsimp simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa xb xe x2. \<lbrakk>\<forall>k. xe = k\<inverse> \<longrightarrow> (\<forall>x\<in>S. \<forall>x\<in>x. k \<noteq> (case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea)); xa \<in> S; xb \<in> S; x2\<^sup>+ \<in> xa; x2\<inverse> \<in> xb; xe \<in> xa \<and> xe \<noteq> x2\<^sup>+ \<or> xe \<in> xb \<and> xe \<noteq> x2\<inverse>\<rbrakk> \<Longrightarrow> \<exists>k. xe = k\<^sup>+ \<and> (\<exists>x\<in>S. \<exists>x\<in>x. k = (case x of xda\<^sup>+ \<Rightarrow> xda | xea\<inverse> \<Rightarrow> xea))
[PROOF STEP]
apply (metis atoms_of_lit.simps(1) atoms_of_lit.simps(2) lit_atoms_cases literal.exhaust)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Res_in_all_clauses: "res S \<union> S \<subseteq> all_clauses S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. res S \<union> S \<subseteq> all_clauses S
[PROOF STEP]
by (simp add: res_in_all_clauses s_sub_all_clauses)


[STATEMENT]
lemma all_clauses_Res_inv: "all_clauses (res S \<union> S) = all_clauses S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_clauses (res S \<union> S) = all_clauses S
[PROOF STEP]
unfolding all_clauses_def atoms_of_cnf_Un
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf (res S) \<union> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf (res S) \<union> atoms_of_cnf S}} = {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}}
[PROOF STEP]
using atoms_res
[PROOF STATE]
proof (prove)
using this:
atoms_of_cnf (res ?S) \<subseteq> atoms_of_cnf ?S

goal (1 subgoal):
 1. {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf (res S) \<union> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf (res S) \<union> atoms_of_cnf S}} = {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_cnf S} \<union> {k\<inverse> |k. k \<in> atoms_of_cnf S}}
[PROOF STEP]
by fast


[STATEMENT]
lemma all_clauses_finite: "finite S \<and> (\<forall>C \<in> S. finite C) \<Longrightarrow> finite (all_clauses S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<and> (\<forall>C\<in>S. finite C) \<Longrightarrow> finite (all_clauses S)
[PROOF STEP]
unfolding all_clauses_def atoms_of_cnf_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<and> (\<forall>C\<in>S. finite C) \<Longrightarrow> finite {s. s \<subseteq> {k\<^sup>+ |k. k \<in> atoms_of_lit ` \<Union> S} \<union> {k\<inverse> |k. k \<in> atoms_of_lit ` \<Union> S}}
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_res: "\<forall>C \<in> S. finite C \<Longrightarrow> \<forall>C \<in> res S. finite C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>S. finite C \<Longrightarrow> \<forall>C\<in>res S. finite C
[PROOF STEP]
unfolding res_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>C\<in>S. finite C \<Longrightarrow> \<forall>C\<in>\<Union>C1\<in>S. \<Union>C2\<in>S. \<Union>L1\<in>C1. \<Union>L2\<in>C2. case (L1, L2) of (i\<^sup>+, a\<^sup>+) \<Rightarrow> {} | (i\<^sup>+, j\<inverse>) \<Rightarrow> if i = j then {C1 - {i\<^sup>+} \<union> (C2 - {j\<inverse>})} else {} | (aa\<inverse>, b) \<Rightarrow> {}. finite C
[PROOF STEP]
by(clarsimp split: literal.splits)


[STATEMENT]
lemma "finite T \<Longrightarrow> S \<subseteq> T \<Longrightarrow> card S < Suc (card T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite T; S \<subseteq> T\<rbrakk> \<Longrightarrow> card S < Suc (card T)
[PROOF STEP]
by (simp add: card_mono le_imp_less_Suc)


[STATEMENT]
lemma "finite S \<and> (\<forall>C \<in> S. finite C) \<Longrightarrow> \<exists>T. Rwhile S = Some T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<and> (\<forall>C\<in>S. finite C) \<Longrightarrow> \<exists>T. Rwhile S = Some T
[PROOF STEP]
apply(unfold Rwhile_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<and> (\<forall>C\<in>S. finite C) \<Longrightarrow> \<exists>T. while_option (\<lambda>S. \<box> \<notin> S \<and> \<not> res S \<subseteq> S) (\<lambda>S. res S \<union> S) S = Some T
[PROOF STEP]
apply(rule measure_while_option_Some[rotated, where f="\<lambda>T. Suc (card (all_clauses S)) - card T"
        and P="\<lambda>T. finite T \<and> (\<forall>C \<in> T. finite C) \<and> all_clauses T = all_clauses S"])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite S \<and> (\<forall>C\<in>S. finite C) \<Longrightarrow> finite S \<and> (\<forall>C\<in>S. finite C) \<and> all_clauses S = all_clauses S
 2. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> (finite (res s \<union> s) \<and> (\<forall>C\<in>res s \<union> s. finite C) \<and> all_clauses (res s \<union> s) = all_clauses S) \<and> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
apply(simp;fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> (finite (res s \<union> s) \<and> (\<forall>C\<in>res s \<union> s. finite C) \<and> all_clauses (res s \<union> s) = all_clauses S) \<and> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> finite (res s \<union> s)
 2. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> \<forall>C\<in>res s \<union> s. finite C
 3. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> all_clauses (res s \<union> s) = all_clauses S
 4. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> finite (res s_ \<union> s_)
[PROOF STEP]
by (meson all_clauses_finite finite_UnI finite_subset res_in_all_clauses)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> \<forall>C\<in>res s \<union> s. finite C
 2. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> all_clauses (res s \<union> s) = all_clauses S
 3. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> \<forall>C\<in>res s_ \<union> s_. finite C
[PROOF STEP]
using finite_res
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>?S. finite C \<Longrightarrow> \<forall>C\<in>res ?S. finite C

goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> \<forall>C\<in>res s_ \<union> s_. finite C
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> all_clauses (res s \<union> s) = all_clauses S
 2. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> all_clauses (res s_ \<union> s_) = all_clauses S
[PROOF STEP]
using all_clauses_Res_inv
[PROOF STATE]
proof (prove)
using this:
all_clauses (res ?S \<union> ?S) = all_clauses ?S

goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> all_clauses (res s_ \<union> s_) = all_clauses S
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s \<and> (\<forall>C\<in>s. finite C) \<and> all_clauses s = all_clauses S; \<box> \<notin> s \<and> \<not> res s \<subseteq> s\<rbrakk> \<Longrightarrow> Suc (card (all_clauses S)) - card (res s \<union> s) < Suc (card (all_clauses S)) - card s
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> Suc (card (all_clauses S)) - card (res s_ \<union> s_) < Suc (card (all_clauses S)) - card s_
[PROOF STEP]
apply(rule diff_less_mono2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> card s_ < card (res s_ \<union> s_)
 2. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> card s_ < Suc (card (all_clauses S))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> card s_ < card (res s_ \<union> s_)
[PROOF STEP]
by (metis Res_in_all_clauses all_clauses_finite card_seteq finite_subset not_le sup_commute sup_ge2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> card s_ < Suc (card (all_clauses S))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> card s_ < Suc (card (all_clauses S))
[PROOF STEP]
apply(intro card_mono le_imp_less_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> finite (all_clauses S)
 2. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> s_ \<subseteq> all_clauses S
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> finite (all_clauses S)
[PROOF STEP]
using all_clauses_finite
[PROOF STATE]
proof (prove)
using this:
finite ?S \<and> (\<forall>C\<in>?S. finite C) \<Longrightarrow> finite (all_clauses ?S)

goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> finite (all_clauses S)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> s_ \<subseteq> all_clauses S
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> s_ \<subseteq> all_clauses S
[PROOF STEP]
using s_sub_all_clauses
[PROOF STATE]
proof (prove)
using this:
?S \<subseteq> all_clauses ?S

goal (1 subgoal):
 1. \<lbrakk>finite S \<and> (\<forall>C\<in>S. finite C); finite s_ \<and> (\<forall>C\<in>s_. finite C) \<and> all_clauses s_ = all_clauses S; \<box> \<notin> s_ \<and> \<not> res s_ \<subseteq> s_\<rbrakk> \<Longrightarrow> s_ \<subseteq> all_clauses S
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "\<box> \<in> the (Res ex1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<box> \<in> the (Res ex1)
[PROOF STEP]
by code_simp


[STATEMENT]
lemma res: "C \<in> res S \<Longrightarrow> S \<turnstile> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<in> res S \<Longrightarrow> S \<turnstile> C
[PROOF STEP]
unfolding res_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<in> (\<Union>C1\<in>S. \<Union>C2\<in>S. \<Union>L1\<in>C1. \<Union>L2\<in>C2. case (L1, L2) of (i\<^sup>+, a\<^sup>+) \<Rightarrow> {} | (i\<^sup>+, j\<inverse>) \<Rightarrow> if i = j then {C1 - {i\<^sup>+} \<union> (C2 - {j\<inverse>})} else {} | (aa\<inverse>, b) \<Rightarrow> {}) \<Longrightarrow> S \<turnstile> C
[PROOF STEP]
by(auto split: literal.splits if_splits) (metis Resolution.simps literal.exhaust)


[STATEMENT]
lemma Res_sound: "Res S = Some S' \<Longrightarrow> (\<forall>C \<in> S'. S \<turnstile> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Res S = Some S' \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
proof (induction arbitrary: S S' rule: Res.fixp_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. option.admissible (\<lambda>Res. \<forall>x xa. Res x = Some xa \<longrightarrow> Ball xa (Resolution x))
 2. \<And>S S'. None = Some S' \<Longrightarrow> Ball S' (Resolution S)
 3. \<And>S Sa S'. \<lbrakk>\<And>Sa S'. S Sa = Some S' \<Longrightarrow> Ball S' (Resolution Sa); (let R = res Sa \<union> Sa in if R = Sa then Some Sa else S R) = Some S'\<rbrakk> \<Longrightarrow> Ball S' (Resolution Sa)
[PROOF STEP]
fix X S S'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. option.admissible (\<lambda>Res. \<forall>x xa. Res x = Some xa \<longrightarrow> Ball xa (Resolution x))
 2. \<And>S S'. None = Some S' \<Longrightarrow> Ball S' (Resolution S)
 3. \<And>S Sa S'. \<lbrakk>\<And>Sa S'. S Sa = Some S' \<Longrightarrow> Ball S' (Resolution Sa); (let R = res Sa \<union> Sa in if R = Sa then Some Sa else S R) = Some S'\<rbrakk> \<Longrightarrow> Ball S' (Resolution Sa)
[PROOF STEP]
assume IH: "\<And>S S'. X S = Some S' \<Longrightarrow> (\<forall>C\<in>S'. S \<turnstile> C)"
[PROOF STATE]
proof (state)
this:
X ?S = Some ?S' \<Longrightarrow> \<forall>C\<in>?S'. ?S \<turnstile> C

goal (3 subgoals):
 1. option.admissible (\<lambda>Res. \<forall>x xa. Res x = Some xa \<longrightarrow> Ball xa (Resolution x))
 2. \<And>S S'. None = Some S' \<Longrightarrow> Ball S' (Resolution S)
 3. \<And>S Sa S'. \<lbrakk>\<And>Sa S'. S Sa = Some S' \<Longrightarrow> Ball S' (Resolution Sa); (let R = res Sa \<union> Sa in if R = Sa then Some Sa else S R) = Some S'\<rbrakk> \<Longrightarrow> Ball S' (Resolution Sa)
[PROOF STEP]
assume prem: "(let R = res S \<union> S in if R = S then Some S else X R) = Some S'"
[PROOF STATE]
proof (state)
this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'

goal (3 subgoals):
 1. option.admissible (\<lambda>Res. \<forall>x xa. Res x = Some xa \<longrightarrow> Ball xa (Resolution x))
 2. \<And>S S'. None = Some S' \<Longrightarrow> Ball S' (Resolution S)
 3. \<And>S Sa S'. \<lbrakk>\<And>Sa S'. S Sa = Some S' \<Longrightarrow> Ball S' (Resolution Sa); (let R = res Sa \<union> Sa in if R = Sa then Some Sa else S R) = Some S'\<rbrakk> \<Longrightarrow> Ball S' (Resolution Sa)
[PROOF STEP]
thus "(\<forall>C\<in>S'. S \<turnstile> C)"
[PROOF STATE]
proof (prove)
using this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'

goal (1 subgoal):
 1. \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; ?P1\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
 2. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; \<not> ?P1\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
assume "res S \<union> S = S"
[PROOF STATE]
proof (state)
this:
res S \<union> S = S

goal (2 subgoals):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; ?P1\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
 2. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; \<not> ?P1\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
with prem
[PROOF STATE]
proof (chain)
picking this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'
res S \<union> S = S
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'
res S \<union> S = S

goal (1 subgoal):
 1. \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
by (simp add: Resolution.Ass)
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S'. S \<turnstile> C

goal (1 subgoal):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; res S \<union> S \<noteq> S\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; res S \<union> S \<noteq> S\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
assume 1: "res S \<union> S \<noteq> S"
[PROOF STATE]
proof (state)
this:
res S \<union> S \<noteq> S

goal (1 subgoal):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; res S \<union> S \<noteq> S\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
with prem
[PROOF STATE]
proof (chain)
picking this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'
res S \<union> S \<noteq> S
[PROOF STEP]
have "X (res S \<union> S) = Some S'"
[PROOF STATE]
proof (prove)
using this:
(let R = res S \<union> S in if R = S then Some S else X R) = Some S'
res S \<union> S \<noteq> S

goal (1 subgoal):
 1. X (res S \<union> S) = Some S'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
X (res S \<union> S) = Some S'

goal (1 subgoal):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; res S \<union> S \<noteq> S\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
with IH
[PROOF STATE]
proof (chain)
picking this:
X ?S = Some ?S' \<Longrightarrow> \<forall>C\<in>?S'. ?S \<turnstile> C
X (res S \<union> S) = Some S'
[PROOF STEP]
have "\<forall>C\<in>S'. res S \<union> S \<turnstile> C"
[PROOF STATE]
proof (prove)
using this:
X ?S = Some ?S' \<Longrightarrow> \<forall>C\<in>?S'. ?S \<turnstile> C
X (res S \<union> S) = Some S'

goal (1 subgoal):
 1. \<forall>C\<in>S'. res S \<union> S \<turnstile> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S'. res S \<union> S \<turnstile> C

goal (1 subgoal):
 1. \<lbrakk>(let R = res S \<union> S in if R = S then Some S else X R) = Some S'; res S \<union> S \<noteq> S\<rbrakk> \<Longrightarrow> \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>S'. res S \<union> S \<turnstile> C

goal (1 subgoal):
 1. \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
using Resolution_unnecessary res
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>S'. res S \<union> S \<turnstile> C
\<forall>C\<in>?T. ?S \<turnstile> C \<Longrightarrow> (?T \<union> ?S \<turnstile> ?D) = (?S \<turnstile> ?D)
?C \<in> res ?S \<Longrightarrow> ?S \<turnstile> ?C

goal (1 subgoal):
 1. \<forall>C\<in>S'. S \<turnstile> C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S'. S \<turnstile> C

goal:
No subgoals!
[PROOF STEP]
(* this needs the generalized Resolution_unnecessary lemma. And I don't get why the option-variant didn't. *)
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S'. S \<turnstile> C

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>C\<in>S'. S \<turnstile> C

goal (2 subgoals):
 1. option.admissible (\<lambda>Res. \<forall>x xa. Res x = Some xa \<longrightarrow> Ball xa (Resolution x))
 2. \<And>S S'. None = Some S' \<Longrightarrow> Ball S' (Resolution S)
[PROOF STEP]
qed (fast intro!: option_admissible)+


[STATEMENT]
lemma Res_terminates: "finite S \<Longrightarrow> \<forall>C \<in> S. finite C \<Longrightarrow> \<exists>T. Res S = Some T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; \<forall>C\<in>S. finite C\<rbrakk> \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
proof(induction "card (all_clauses S) - card S" arbitrary: S rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>Sa. \<lbrakk>card (all_clauses Sa) - card Sa < card (all_clauses S) - card S; finite Sa; Ball Sa finite\<rbrakk> \<Longrightarrow> \<exists>T. Res Sa = Some T; finite S; Ball S finite\<rbrakk> \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
(* can be done by induction on "card (all_clauses S - S)", but I found that to be more annoying. *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>Sa. \<lbrakk>card (all_clauses Sa) - card Sa < card (all_clauses S) - card S; finite Sa; Ball Sa finite\<rbrakk> \<Longrightarrow> \<exists>T. Res Sa = Some T; finite S; Ball S finite\<rbrakk> \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
case less
[PROOF STATE]
proof (state)
this:
\<lbrakk>card (all_clauses ?S) - card ?S < card (all_clauses S) - card S; finite ?S; Ball ?S finite\<rbrakk> \<Longrightarrow> \<exists>T. Res ?S = Some T
finite S
Ball S finite

goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>Sa. \<lbrakk>card (all_clauses Sa) - card Sa < card (all_clauses S) - card S; finite Sa; Ball Sa finite\<rbrakk> \<Longrightarrow> \<exists>T. Res Sa = Some T; finite S; Ball S finite\<rbrakk> \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
let ?r = "res S \<union> S"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>S. \<lbrakk>\<And>Sa. \<lbrakk>card (all_clauses Sa) - card Sa < card (all_clauses S) - card S; finite Sa; Ball Sa finite\<rbrakk> \<Longrightarrow> \<exists>T. Res Sa = Some T; finite S; Ball S finite\<rbrakk> \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T. Res S = Some T
[PROOF STEP]
proof(cases "?r = S")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
res S \<union> S \<noteq> S

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
have b: "finite (res S \<union> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (res S \<union> S)
[PROOF STEP]
by (meson less Res_in_all_clauses all_clauses_finite infinite_super)
[PROOF STATE]
proof (state)
this:
finite (res S \<union> S)

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
have c: "Ball (res S \<union> S) finite"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ball (res S \<union> S) finite
[PROOF STEP]
using less.prems(2) finite_res
[PROOF STATE]
proof (prove)
using this:
Ball S finite
\<forall>C\<in>?S. finite C \<Longrightarrow> \<forall>C\<in>res ?S. finite C

goal (1 subgoal):
 1. Ball (res S \<union> S) finite
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (res S \<union> S) finite

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
have "card S < card ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card S < card (res S \<union> S)
[PROOF STEP]
by (metis False b psubsetI psubset_card_mono sup_ge2)
[PROOF STATE]
proof (state)
this:
card S < card (res S \<union> S)

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card S < card (res S \<union> S)

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
have "card ?r \<le> (card (all_clauses S))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (res S \<union> S) \<le> card (all_clauses S)
[PROOF STEP]
by (meson less Res_in_all_clauses all_clauses_finite card_mono le_imp_less_Suc)
[PROOF STATE]
proof (state)
this:
card (res S \<union> S) \<le> card (all_clauses S)

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card S < card (res S \<union> S)
card (res S \<union> S) \<le> card (all_clauses S)
[PROOF STEP]
have a: "(card (all_clauses ?r)) - card ?r < (card (all_clauses S)) - card S"
[PROOF STATE]
proof (prove)
using this:
card S < card (res S \<union> S)
card (res S \<union> S) \<le> card (all_clauses S)

goal (1 subgoal):
 1. card (all_clauses (res S \<union> S)) - card (res S \<union> S) < card (all_clauses S) - card S
[PROOF STEP]
using all_clauses_Res_inv[of S]
[PROOF STATE]
proof (prove)
using this:
card S < card (res S \<union> S)
card (res S \<union> S) \<le> card (all_clauses S)
all_clauses (res S \<union> S) = all_clauses S

goal (1 subgoal):
 1. card (all_clauses (res S \<union> S)) - card (res S \<union> S) < card (all_clauses S) - card S
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (all_clauses (res S \<union> S)) - card (res S \<union> S) < card (all_clauses S) - card S

goal (2 subgoals):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
 2. res S \<union> S \<noteq> S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
from less(1)[OF a b c]
[PROOF STATE]
proof (chain)
picking this:
\<exists>T. Res (res S \<union> S) = Some T
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>T. Res (res S \<union> S) = Some T

goal (1 subgoal):
 1. \<exists>T. Res S = Some T
[PROOF STEP]
by (subst Res.simps) (simp add: Let_def)
[PROOF STATE]
proof (state)
this:
\<exists>T. Res S = Some T

goal (1 subgoal):
 1. res S \<union> S = S \<Longrightarrow> \<exists>T. Res S = Some T
[PROOF STEP]
qed (simp add: Res.simps)
[PROOF STATE]
proof (state)
this:
\<exists>T. Res S = Some T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lambda_eq_eq[simp]: "(\<lambda>x y. y = x) = (=)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. y = x) = (=)
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. (y = x) = (x = y)
[PROOF STEP]
by blast


[STATEMENT]
lemma norm_compile_instr:
  "norm_instr (compile_instr instr) = instr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm_eq instr (compile_instr instr)
[PROOF STEP]
by (cases instr) auto


[STATEMENT]
lemma rel_compile_fundef:
  assumes "compile_fundef fd1 = Some fd2"
  shows "rel_fundef (=) norm_eq fd1 fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
compile_fundef fd1 = Some fd2

goal (1 subgoal):
 1. rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
proof (cases rule: compile_fundef.elims)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd1 = Fundef [] uu_ uv_ uw_; Some fd2 = None\<rbrakk> \<Longrightarrow> rel_fundef (=) norm_eq fd1 fd2
 2. \<And>v va ar ret locals. \<lbrakk>fd1 = Fundef (v # va) ar ret locals; Some fd2 = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (v # va)) ar ret locals)\<rbrakk> \<Longrightarrow> rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
case (2 x xs ar)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef (x # xs) ar ret_ locals_
Some fd2 = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)

goal (2 subgoals):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd1 = Fundef [] uu_ uv_ uw_; Some fd2 = None\<rbrakk> \<Longrightarrow> rel_fundef (=) norm_eq fd1 fd2
 2. \<And>v va ar ret locals. \<lbrakk>fd1 = Fundef (v # va) ar ret locals; Some fd2 = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (v # va)) ar ret locals)\<rbrakk> \<Longrightarrow> rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef (x # xs) ar ret_ locals_
Some fd2 = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef (x # xs) ar ret_ locals_
Some fd2 = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)

goal (1 subgoal):
 1. rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
by (auto intro: list.rel_refl
        simp: const_eq_if_conv list.rel_map norm_compile_instr map_ran_def case_prod_beta
          rel_prod_sel)
[PROOF STATE]
proof (state)
this:
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd1 = Fundef [] uu_ uv_ uw_; Some fd2 = None\<rbrakk> \<Longrightarrow> rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma rel_fundef_imp_fundef_ok_iff:
  assumes "rel_fundef (=) norm_eq fd1 fd2"
  shows "wf_fundef fd1 \<longleftrightarrow> wf_fundef fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundef fd1 = wf_fundef fd2
[PROOF STEP]
unfolding wf_fundef_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body fd1 \<noteq> []) = (body fd2 \<noteq> [])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. (body fd1 \<noteq> []) = (body fd2 \<noteq> [])
[PROOF STEP]
by (auto simp: list_all2_rel_prod_conv list.rel_eq elim: fundef.rel_cases)


[STATEMENT]
lemma rel_fundefs_imp_wf_fundefs_iff:
  assumes rel_f_g: "rel_fundefs f g"
  shows "wf_fundefs f \<longleftrightarrow> wf_fundefs g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs f = wf_fundefs g
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wf_fundefs f \<Longrightarrow> wf_fundefs g
 2. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
assume "wf_fundefs f"
[PROOF STATE]
proof (state)
this:
wf_fundefs f

goal (2 subgoals):
 1. wf_fundefs f \<Longrightarrow> wf_fundefs g
 2. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
show "wf_fundefs g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs g
[PROOF STEP]
proof (rule wf_fundefsI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fd. g f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
fix x fd
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fd. g f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
assume "g x = Some fd"
[PROOF STATE]
proof (state)
this:
g x = Some fd

goal (1 subgoal):
 1. \<And>f fd. g f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
thus "wf_fundef fd"
[PROOF STATE]
proof (prove)
using this:
g x = Some fd

goal (1 subgoal):
 1. wf_fundef fd
[PROOF STEP]
using \<open>wf_fundefs f\<close>
[PROOF STATE]
proof (prove)
using this:
g x = Some fd
wf_fundefs f

goal (1 subgoal):
 1. wf_fundef fd
[PROOF STEP]
by (meson rel_f_g rel_fundef_imp_fundef_ok_iff rel_fundefs_Some2 wf_fundefs_imp_wf_fundef)
[PROOF STATE]
proof (state)
this:
wf_fundef fd

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

goal (1 subgoal):
 1. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
show "wf_fundefs g \<Longrightarrow> wf_fundefs f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
using rel_f_g
[PROOF STATE]
proof (prove)
using this:
rel_fundefs f g

goal (1 subgoal):
 1. wf_fundefs g \<Longrightarrow> wf_fundefs f
[PROOF STEP]
by (meson rel_fundef_imp_fundef_ok_iff rel_fundefs_Some1 wf_fundefs_imp_wf_fundef wf_fundefsI)
[PROOF STATE]
proof (state)
this:
wf_fundefs g \<Longrightarrow> wf_fundefs f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compile_fundef_wf:
  assumes "compile_fundef fd = Some fd'"
  shows "wf_fundef fd'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundef fd'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
compile_fundef fd = Some fd'

goal (1 subgoal):
 1. wf_fundef fd'
[PROOF STEP]
proof (cases rule: compile_fundef.elims)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd = Fundef [] uu_ uv_ uw_; Some fd' = None\<rbrakk> \<Longrightarrow> wf_fundef fd'
 2. \<And>v va ar ret locals. \<lbrakk>fd = Fundef (v # va) ar ret locals; Some fd' = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (v # va)) ar ret locals)\<rbrakk> \<Longrightarrow> wf_fundef fd'
[PROOF STEP]
case (2 x xs ar)
[PROOF STATE]
proof (state)
this:
fd = Fundef (x # xs) ar ret_ locals_
Some fd' = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)

goal (2 subgoals):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd = Fundef [] uu_ uv_ uw_; Some fd' = None\<rbrakk> \<Longrightarrow> wf_fundef fd'
 2. \<And>v va ar ret locals. \<lbrakk>fd = Fundef (v # va) ar ret locals; Some fd' = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (v # va)) ar ret locals)\<rbrakk> \<Longrightarrow> wf_fundef fd'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd = Fundef (x # xs) ar ret_ locals_
Some fd' = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fd = Fundef (x # xs) ar ret_ locals_
Some fd' = Some (Fundef (map_ran (\<lambda>_. map compile_instr) (x # xs)) ar ret_ locals_)

goal (1 subgoal):
 1. wf_fundef fd'
[PROOF STEP]
by (simp add: const_eq_if_conv wf_fundef_def map_ran_Cons_sel)
[PROOF STATE]
proof (state)
this:
wf_fundef fd'

goal (1 subgoal):
 1. \<And>uu_ uv_ uw_. \<lbrakk>fd = Fundef [] uu_ uv_ uw_; Some fd' = None\<rbrakk> \<Longrightarrow> wf_fundef fd'
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma Finca_get_compile:
  assumes compile_F1: "compile_env F1 = Some F2"
  shows "Finca_get F2 f = Fstd_get F1 f \<bind> compile_fundef"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Finca_get F2 f = Fstd_get F1 f \<bind> compile_fundef
[PROOF STEP]
using compile_env_imp_rel_option[OF assms(1), of f]
[PROOF STATE]
proof (prove)
using this:
rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)

goal (1 subgoal):
 1. Finca_get F2 f = Fstd_get F1 f \<bind> compile_fundef
[PROOF STEP]
by (auto elim!: option.rel_cases)


[STATEMENT]
lemma compile_env_rel_fundefs:
  assumes "compile_env F1 = Some F2"
  shows "rel_fundefs (Fstd_get F1) (Finca_get F2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fundefs (Fstd_get F1) (Finca_get F2)
[PROOF STEP]
unfolding rel_fundefs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 x) (Finca_get F2 x)
[PROOF STEP]
proof (rule allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 x) (Finca_get F2 x)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 x) (Finca_get F2 x)
[PROOF STEP]
show "rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 f) (Finca_get F2 f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
using compile_env_imp_rel_option[OF assms(1), of f]
[PROOF STATE]
proof (prove)
using this:
rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 f) (Finca_get F2 f)

goal (1 subgoal):
 1. rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 f) (Finca_get F2 f)
[PROOF STEP]
by (auto elim!: option.rel_cases intro: rel_compile_fundef)
[PROOF STATE]
proof (state)
this:
rel_option (rel_fundef (=) norm_eq) (Fstd_get F1 f) (Finca_get F2 f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compile_env_imp_wf_fundefs2:
  assumes "compile_env F1 = Some F2"
  shows "wf_fundefs (Finca_get F2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs (Finca_get F2)
[PROOF STEP]
unfolding Finca_get_compile[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs (\<lambda>f. Fstd_get F1 f \<bind> compile_fundef)
[PROOF STEP]
by (auto simp: bind_eq_Some_conv intro!: wf_fundefsI intro: compile_fundef_wf)


[STATEMENT]
theorem compile_load:
  assumes
    compile_p1: "compile p1 = Some p2" and
    load: "Sinca.load p2 s2"
  shows "\<exists>s1. Sstd.load p1 s1 \<and> match s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
proof (cases p1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3. p1 = Prog x1 x2 x3 \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
case (Prog F1 H main)
[PROOF STATE]
proof (state)
this:
p1 = Prog F1 H main

goal (1 subgoal):
 1. \<And>x1 x2 x3. p1 = Prog x1 x2 x3 \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
with assms(1)
[PROOF STATE]
proof (chain)
picking this:
compile p1 = Some p2
p1 = Prog F1 H main
[PROOF STEP]
obtain F2 where
    compile_F1: "compile_env F1 = Some F2" and
    p2_def: "p2 = Prog F2 H main"
[PROOF STATE]
proof (prove)
using this:
compile p1 = Some p2
p1 = Prog F1 H main

goal (1 subgoal):
 1. (\<And>F2. \<lbrakk>compile_env F1 = Some F2; p2 = Prog F2 H main\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: ap_option_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
compile_env F1 = Some F2
p2 = Prog F2 H main

goal (1 subgoal):
 1. \<And>x1 x2 x3. p1 = Prog x1 x2 x3 \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
Sinca.load p2 s2

goal (1 subgoal):
 1. \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
unfolding p2_def Sinca.load_def
[PROOF STATE]
proof (prove)
using this:
load Finca_get uninitialized (Prog F2 H main) s2

goal (1 subgoal):
 1. \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
proof (cases _ _ _ s2 rule: load.cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
case (1 fd2)
[PROOF STATE]
proof (state)
this:
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []

goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []
[PROOF STEP]
obtain fd1 where
      F1_main: "Fstd_get F1 main = Some fd1" and compile_fd1: "compile_fundef fd1 = Some fd2"
[PROOF STATE]
proof (prove)
using this:
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []

goal (1 subgoal):
 1. (\<And>fd1. \<lbrakk>Fstd_get F1 main = Some fd1; compile_fundef fd1 = Some fd2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Finca_get_compile[OF compile_F1]
[PROOF STATE]
proof (prove)
using this:
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []
Finca_get F2 ?f = Fstd_get F1 ?f \<bind> compile_fundef

goal (1 subgoal):
 1. (\<And>fd1. \<lbrakk>Fstd_get F1 main = Some fd1; compile_fundef fd1 = Some fd2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: bind_eq_Some_conv)
[PROOF STATE]
proof (state)
this:
Fstd_get F1 main = Some fd1
compile_fundef fd1 = Some fd2

goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
note rel_fd1_fd2 = rel_compile_fundef[OF compile_fd1]
[PROOF STATE]
proof (state)
this:
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
hence first_label_fd1_fd2: "fst (hd (body fd1)) = fst (hd (body fd2))"
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. fst (hd (body fd1)) = fst (hd (body fd2))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) norm_eq fd1 fd2
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []

goal (1 subgoal):
 1. fst (hd (body fd1)) = fst (hd (body fd2))
[PROOF STEP]
by (auto elim!: fundef.rel_cases dest: list_all2_rel_prod_fst_hd)
[PROOF STATE]
proof (state)
this:
fst (hd (body fd1)) = fst (hd (body fd2))

goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
have bodies_fd1_fd2: "body fd1 = [] \<longleftrightarrow> body fd2 = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (body fd1 = []) = (body fd2 = [])
[PROOF STEP]
using rel_fundef_body_length[OF rel_fd1_fd2]
[PROOF STATE]
proof (prove)
using this:
length (body fd1) = length (body fd2)

goal (1 subgoal):
 1. (body fd1 = []) = (body fd2 = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(body fd1 = []) = (body fd2 = [])

goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
let ?s1 = "State F1 H [allocate_frame main fd1 [] uninitialized]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>fd. \<lbrakk>s2 = Global.state.State F2 H [allocate_frame main fd [] uninitialized]; Finca_get F2 main = Some fd; arity fd = 0; body fd \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Sstd.load p1 ?s1.0
 2. ?s1.0 \<sim> s2
[PROOF STEP]
show "Sstd.load p1 ?s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sstd.load p1 (Global.state.State F1 H [allocate_frame main fd1 [] uninitialized])
[PROOF STEP]
unfolding Prog
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sstd.load (Prog F1 H main) (Global.state.State F1 H [allocate_frame main fd1 [] uninitialized])
[PROOF STEP]
using 1 F1_main rel_fd1_fd2 bodies_fd1_fd2
[PROOF STATE]
proof (prove)
using this:
s2 = Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
Finca_get F2 main = Some fd2
arity fd2 = 0
body fd2 \<noteq> []
Fstd_get F1 main = Some fd1
rel_fundef (=) norm_eq fd1 fd2
(body fd1 = []) = (body fd2 = [])

goal (1 subgoal):
 1. Sstd.load (Prog F1 H main) (Global.state.State F1 H [allocate_frame main fd1 [] uninitialized])
[PROOF STEP]
by (auto simp: rel_fundef_arities Sstd.load_def intro!: load.intros)
[PROOF STATE]
proof (state)
this:
Sstd.load p1 (Global.state.State F1 H [allocate_frame main fd1 [] uninitialized])

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
note rel_F1_F2 = compile_env_rel_fundefs[OF compile_F1]
[PROOF STATE]
proof (state)
this:
rel_fundefs (Fstd_get F1) (Finca_get F2)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
rel_fundefs (Fstd_get F1) (Finca_get F2)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
have "wf_fundefs (Fstd_get F1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs (Fstd_get F1)
[PROOF STEP]
proof (rule wf_fundefsI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fd. Fstd_get F1 f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
fix f fd1
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f fd. Fstd_get F1 f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
assume "Fstd_get F1 f = Some fd1"
[PROOF STATE]
proof (state)
this:
Fstd_get F1 f = Some fd1

goal (1 subgoal):
 1. \<And>f fd. Fstd_get F1 f = Some fd \<Longrightarrow> wf_fundef fd
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Fstd_get F1 f = Some fd1
[PROOF STEP]
show "wf_fundef fd1"
[PROOF STATE]
proof (prove)
using this:
Fstd_get F1 f = Some fd1

goal (1 subgoal):
 1. wf_fundef fd1
[PROOF STEP]
by (metis (mono_tags, lifting) Finca_get_compile bind.bind_lunit compile_F1
              rel_F1_F2 compile_fundef_wf rel_fundef_imp_fundef_ok_iff
              rel_fundefs_Some1)
[PROOF STATE]
proof (state)
this:
wf_fundef fd1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
rel_fundefs (Fstd_get F1) (Finca_get F2)
wf_fundefs (Fstd_get F1)
[PROOF STEP]
show "match ?s1 s2"
[PROOF STATE]
proof (prove)
using this:
rel_fundefs (Fstd_get F1) (Finca_get F2)
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2
[PROOF STEP]
unfolding 1
[PROOF STATE]
proof (prove)
using this:
rel_fundefs (Fstd_get F1) (Finca_get F2)
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
using rel_fd1_fd2
[PROOF STATE]
proof (prove)
using this:
rel_fundefs (Fstd_get F1) (Finca_get F2)
wf_fundefs (Fstd_get F1)
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
by (auto simp: allocate_frame_def first_label_fd1_fd2 rel_fundef_locals
            intro: match.intros)
[PROOF STATE]
proof (state)
this:
Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> s2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>s1. Sstd.load p1 s1 \<and> s1 \<sim> s2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compile_fundef_complete:
  assumes "wf_fundef fd1"
  shows "\<exists>fd2. compile_fundef fd1 = Some fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
proof (cases fd1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. fd1 = Fundef x1 x2 x3 x4 \<Longrightarrow> \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
case (Fundef bbs ar)
[PROOF STATE]
proof (state)
this:
fd1 = Fundef bbs ar x3_ x4_

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. fd1 = Fundef x1 x2 x3 x4 \<Longrightarrow> \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fd1 = Fundef bbs ar x3_ x4_
[PROOF STEP]
obtain bb bbs' where bbs_def: "bbs = bb # bbs'"
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bbs ar x3_ x4_

goal (1 subgoal):
 1. (\<And>bb bbs'. bbs = bb # bbs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
fd1 = Fundef bbs ar x3_ x4_
wf_fundef fd1

goal (1 subgoal):
 1. (\<And>bb bbs'. bbs = bb # bbs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases bbs; auto)
[PROOF STATE]
proof (state)
this:
bbs = bb # bbs'

goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. fd1 = Fundef x1 x2 x3 x4 \<Longrightarrow> \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_fundef fd1

goal (1 subgoal):
 1. \<exists>fd2. compile_fundef fd1 = Some fd2
[PROOF STEP]
unfolding Fundef bbs_def
[PROOF STATE]
proof (prove)
using this:
wf_fundef (Fundef (bb # bbs') ar x3_ x4_)

goal (1 subgoal):
 1. \<exists>fd2. compile_fundef (Fundef (bb # bbs') ar x3_ x4_) = Some fd2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>fd2. compile_fundef fd1 = Some fd2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma compile_env_complete:
  assumes wf_F1: "wf_fundefs (Fstd_get F1)"
  shows "\<exists>F2. compile_env F1 = Some F2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F2. compile_env F1 = Some F2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>F2. compile_env F1 = Some F2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>F2. compile_env F1 = Some F2
[PROOF STEP]
using wf_F1
[PROOF STATE]
proof (prove)
using this:
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. \<exists>F2. compile_env F1 = Some F2
[PROOF STEP]
by (auto simp: compile_env_def ap_option_eq_Some_conv ap_map_prod_eq_Some_conv
        intro!: ex_ap_map_list_eq_SomeI Sstd.Fenv.to_list_list_allI compile_fundef_complete
        intro: wf_fundefs_imp_wf_fundef)
[PROOF STATE]
proof (state)
this:
\<exists>F2. compile_env F1 = Some F2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem compile_complete:
  assumes wf_p1: "wf_prog Fstd_get p1"
  shows "\<exists>p2. compile p1 = Some p2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p2. compile p1 = Some p2
[PROOF STEP]
proof (cases p1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 x3. p1 = Prog x1 x2 x3 \<Longrightarrow> \<exists>p2. compile p1 = Some p2
[PROOF STEP]
case (Prog x1 x2 x3)
[PROOF STATE]
proof (state)
this:
p1 = Prog x1 x2 x3

goal (1 subgoal):
 1. \<And>x1 x2 x3. p1 = Prog x1 x2 x3 \<Longrightarrow> \<exists>p2. compile p1 = Some p2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p1 = Prog x1 x2 x3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p1 = Prog x1 x2 x3

goal (1 subgoal):
 1. \<exists>p2. compile p1 = Some p2
[PROOF STEP]
using wf_p1
[PROOF STATE]
proof (prove)
using this:
p1 = Prog x1 x2 x3
wf_prog Fstd_get p1

goal (1 subgoal):
 1. \<exists>p2. compile p1 = Some p2
[PROOF STEP]
unfolding wf_prog_def
[PROOF STATE]
proof (prove)
using this:
p1 = Prog x1 x2 x3
wf_fundefs (Fstd_get (prog_fundefs p1))

goal (1 subgoal):
 1. \<exists>p2. compile p1 = Some p2
[PROOF STEP]
by (auto dest: compile_env_complete)
[PROOF STATE]
proof (state)
this:
\<exists>p2. compile p1 = Some p2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem compile_load_forward:
  assumes
    wf_p1: "wf_prog Fstd_get p1" and load_p1: "Sstd.load p1 s1"
  shows "\<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> match s1 s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
from load_p1
[PROOF STATE]
proof (chain)
picking this:
Sstd.load p1 s1
[PROOF STEP]
obtain F1 H main fd1 where
    p1_def: "p1 = Prog F1 H main" and
    s1_def: "s1 = Global.state.State F1 H [allocate_frame main fd1 [] uninitialized]" and
    F1_main: "Fstd_get F1 main = Some fd1" and
    arity_fd1: "arity fd1 = 0"
[PROOF STATE]
proof (prove)
using this:
Sstd.load p1 s1

goal (1 subgoal):
 1. (\<And>F1 H main fd1. \<lbrakk>p1 = Prog F1 H main; s1 = Global.state.State F1 H [allocate_frame main fd1 [] uninitialized]; Fstd_get F1 main = Some fd1; arity fd1 = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: Sstd.load_def elim: load.cases)
[PROOF STATE]
proof (state)
this:
p1 = Prog F1 H main
s1 = Global.state.State F1 H [allocate_frame main fd1 [] uninitialized]
Fstd_get F1 main = Some fd1
arity fd1 = 0

goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
obtain F2 where compile_F1: "compile_env F1 = Some F2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>F2. compile_env F1 = Some F2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using wf_p1[unfolded p1_def wf_prog_def, simplified]
[PROOF STATE]
proof (prove)
using this:
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. (\<And>F2. compile_env F1 = Some F2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using compile_env_complete[of F1]
[PROOF STATE]
proof (prove)
using this:
wf_fundefs (Fstd_get F1)
wf_fundefs (Fstd_get F1) \<Longrightarrow> \<exists>F2. compile_env F1 = Some F2

goal (1 subgoal):
 1. (\<And>F2. compile_env F1 = Some F2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
compile_env F1 = Some F2

goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
obtain fd2 where
    F2_main: "Finca_get F2 main = Some fd2" and compile_fd1: "compile_fundef fd1 = Some fd2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>fd2. \<lbrakk>Finca_get F2 main = Some fd2; compile_fundef fd1 = Some fd2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using compile_env_imp_rel_option[OF compile_F1, of main]
[PROOF STATE]
proof (prove)
using this:
rel_option (\<lambda>fd1 fd2. compile_fundef fd1 = Some fd2) (Fstd_get F1 main) (Finca_get F2 main)

goal (1 subgoal):
 1. (\<And>fd2. \<lbrakk>Finca_get F2 main = Some fd2; compile_fundef fd1 = Some fd2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding F1_main option_rel_Some1
[PROOF STATE]
proof (prove)
using this:
\<exists>y'. Finca_get F2 main = Some y' \<and> compile_fundef fd1 = Some y'

goal (1 subgoal):
 1. (\<And>fd2. \<lbrakk>Finca_get F2 main = Some fd2; compile_fundef fd1 = Some fd2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Finca_get F2 main = Some fd2
compile_fundef fd1 = Some fd2

goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
hence rel_fd1_fd2: "rel_fundef (=) norm_eq fd1 fd2"
[PROOF STATE]
proof (prove)
using this:
Finca_get F2 main = Some fd2
compile_fundef fd1 = Some fd2

goal (1 subgoal):
 1. rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
using rel_compile_fundef
[PROOF STATE]
proof (prove)
using this:
Finca_get F2 main = Some fd2
compile_fundef fd1 = Some fd2
compile_fundef ?fd1.0 = Some ?fd2.0 \<Longrightarrow> rel_fundef (=) norm_eq ?fd1.0 ?fd2.0

goal (1 subgoal):
 1. rel_fundef (=) norm_eq fd1 fd2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_fundef (=) norm_eq fd1 fd2

goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
note wf_fd2 = compile_fundef_wf[OF compile_fd1]
[PROOF STATE]
proof (state)
this:
wf_fundef fd2

goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
let ?s2 = "State F2 H [allocate_frame main fd2 [] uninitialized]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. compile p1 = Some ?p2.0
 2. Sinca.load ?p2.0 ?s2.1
 3. s1 \<sim> ?s2.1
[PROOF STEP]
show "compile p1 = Some (Prog F2 H main)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compile p1 = Some (Prog F2 H main)
[PROOF STEP]
by (simp add: p1_def compile_F1)
[PROOF STATE]
proof (state)
this:
compile p1 = Some (Prog F2 H main)

goal (2 subgoals):
 1. Sinca.load (Prog F2 H main) ?s2.1
 2. s1 \<sim> ?s2.1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Sinca.load (Prog F2 H main) ?s2.1
 2. s1 \<sim> ?s2.1
[PROOF STEP]
show "Sinca.load (Prog F2 H main) ?s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sinca.load (Prog F2 H main) (Global.state.State F2 H [allocate_frame main fd2 [] uninitialized])
[PROOF STEP]
using F2_main arity_fd1
[PROOF STATE]
proof (prove)
using this:
Finca_get F2 main = Some fd2
arity fd1 = 0

goal (1 subgoal):
 1. Sinca.load (Prog F2 H main) (Global.state.State F2 H [allocate_frame main fd2 [] uninitialized])
[PROOF STEP]
using rel_fundef_arities[OF rel_fd1_fd2]
[PROOF STATE]
proof (prove)
using this:
Finca_get F2 main = Some fd2
arity fd1 = 0
arity fd1 = arity fd2

goal (1 subgoal):
 1. Sinca.load (Prog F2 H main) (Global.state.State F2 H [allocate_frame main fd2 [] uninitialized])
[PROOF STEP]
using compile_fundef_wf[OF compile_fd1]
[PROOF STATE]
proof (prove)
using this:
Finca_get F2 main = Some fd2
arity fd1 = 0
arity fd1 = arity fd2
wf_fundef fd2

goal (1 subgoal):
 1. Sinca.load (Prog F2 H main) (Global.state.State F2 H [allocate_frame main fd2 [] uninitialized])
[PROOF STEP]
by (auto simp: wf_fundef_def Sinca.load_def intro: load.intros)
[PROOF STATE]
proof (state)
this:
Sinca.load (Prog F2 H main) (Global.state.State F2 H [allocate_frame main fd2 [] uninitialized])

goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
have "fst (hd (body fd1)) = fst (hd (body fd2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (hd (body fd1)) = fst (hd (body fd2))
[PROOF STEP]
using rel_fd1_fd2 wf_fd2
[PROOF STATE]
proof (prove)
using this:
rel_fundef (=) norm_eq fd1 fd2
wf_fundef fd2

goal (1 subgoal):
 1. fst (hd (body fd1)) = fst (hd (body fd2))
[PROOF STEP]
by (auto simp add: fundef.rel_sel wf_fundef_def list_all2_rel_prod_fst_hd)
[PROOF STATE]
proof (state)
this:
fst (hd (body fd1)) = fst (hd (body fd2))

goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
fst (hd (body fd1)) = fst (hd (body fd2))

goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
have "wf_fundefs (Fstd_get F1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fundefs (Fstd_get F1)
[PROOF STEP]
using compile_env_imp_wf_fundefs2[OF compile_F1]
[PROOF STATE]
proof (prove)
using this:
wf_fundefs (Finca_get F2)

goal (1 subgoal):
 1. wf_fundefs (Fstd_get F1)
[PROOF STEP]
using compile_env_rel_fundefs[OF compile_F1, THEN rel_fundefs_imp_wf_fundefs_iff]
[PROOF STATE]
proof (prove)
using this:
wf_fundefs (Finca_get F2)
wf_fundefs (Fstd_get F1) = wf_fundefs (Finca_get F2)

goal (1 subgoal):
 1. wf_fundefs (Fstd_get F1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
fst (hd (body fd1)) = fst (hd (body fd2))
wf_fundefs (Fstd_get F1)
[PROOF STEP]
show "match s1 ?s2"
[PROOF STATE]
proof (prove)
using this:
fst (hd (body fd1)) = fst (hd (body fd2))
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
unfolding s1_def
[PROOF STATE]
proof (prove)
using this:
fst (hd (body fd1)) = fst (hd (body fd2))
wf_fundefs (Fstd_get F1)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
using rel_fd1_fd2 compile_env_rel_fundefs[OF compile_F1]
[PROOF STATE]
proof (prove)
using this:
fst (hd (body fd1)) = fst (hd (body fd2))
wf_fundefs (Fstd_get F1)
rel_fundef (=) norm_eq fd1 fd2
rel_fundefs (Fstd_get F1) (Finca_get F2)

goal (1 subgoal):
 1. Global.state.State F1 H [allocate_frame main fd1 [] uninitialized] \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]
[PROOF STEP]
by (auto simp: allocate_frame_def rel_fundef_locals intro!: match.intros)
[PROOF STATE]
proof (state)
this:
s1 \<sim> Global.state.State F2 H [allocate_frame main fd2 [] uninitialized]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>p2 s2. compile p1 = Some p2 \<and> Sinca.load p2 s2 \<and> s1 \<sim> s2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma language_entails[iff]: "w \<in> language \<longleftrightarrow> snth w \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<in> language) = (!!) w \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
unfolding language_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (w \<in> {w. (!!) w \<Turnstile>\<^sub>p \<phi>}) = (!!) w \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by simp


[STATEMENT]
lemma stutter_equivalent_entails[dest]: "u \<approx> v \<Longrightarrow> u \<Turnstile>\<^sub>p \<phi> \<longleftrightarrow> v \<Turnstile>\<^sub>p \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<approx> v \<Longrightarrow> u \<Turnstile>\<^sub>p \<phi> = v \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
using next_free_stutter_invariant next_free
[PROOF STATE]
proof (prove)
using this:
next_free ?\<phi> \<Longrightarrow> stutter_invariant ?\<phi>
next_free \<phi>

goal (1 subgoal):
 1. u \<approx> v \<Longrightarrow> u \<Turnstile>\<^sub>p \<phi> = v \<Turnstile>\<^sub>p \<phi>
[PROOF STEP]
by blast


[STATEMENT]
lemma rtrancl_rbt_impl:
  "rs.\<alpha> (rtrancl_rbt_impl r as) = {b. \<exists> a \<in> set as. (a,b) \<in> (set r)\<^sup>*}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (rtrancl_rbt_impl r as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
unfolding rtrancl_rbt_impl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (rtrancl_impl rm_succ (\<lambda>as bs. rs.union bs (rs.from_list as)) rs.memb (rs.empty ()) r as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
by (rule set_access_gen.rtrancl_impl, unfold_locales, unfold Let_def, simp add: rs.correct elem_list_to_rm.rm_set_lookup, force)


[STATEMENT]
lemma trancl_rbt_impl:
  "rs.\<alpha> (trancl_rbt_impl r as) = {b. \<exists> a \<in> set as. (a,b) \<in> (set r)\<^sup>+}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (trancl_rbt_impl r as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
unfolding trancl_rbt_impl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (trancl_impl rm_succ (\<lambda>as bs. rs.union bs (rs.from_list as)) rs.memb (rs.empty ()) r as) = {b. \<exists>a\<in>set as. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
by (rule set_access_gen.trancl_impl, unfold_locales, unfold Let_def, simp add: rs.correct elem_list_to_rm.rm_set_lookup, force)


[STATEMENT]
lemma memo_rbt_rtrancl:
  "rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
let ?rm = "rm.to_map
    (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) ((rs.to_list \<circ> rs.from_list \<circ> map fst) r))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
proof (cases "rm.lookup a ?rm")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
have one: "?l = {a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {a}
[PROOF STEP]
unfolding memo_rbt_rtrancl_def Let_def None
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (case None of None \<Rightarrow> rs.from_list [a] | Some as \<Rightarrow> as) = {a}
[PROOF STEP]
by (simp add: rs.correct)
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_rtrancl r a) = {a}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
from None [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct map_of_eq_None_iff]
[PROOF STATE]
proof (chain)
picking this:
a \<notin> fst ` set (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))
[PROOF STEP]
have a: "a \<notin> fst ` set r"
[PROOF STATE]
proof (prove)
using this:
a \<notin> fst ` set (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))

goal (1 subgoal):
 1. a \<notin> fst ` set r
[PROOF STEP]
by (simp add: rs.correct, force)
[PROOF STATE]
proof (state)
this:
a \<notin> fst ` set r

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<notin> fst ` set r

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
assume "b \<in> ?r"
[PROOF STATE]
proof (state)
this:
b \<in> {b. (a, b) \<in> (set r)\<^sup>*}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
from this [unfolded rtrancl_power relpow_fun_conv]
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. \<exists>n f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> set r)}
[PROOF STEP]
obtain n f where
        ab: "f 0 = a \<and> f n = b" and steps: "\<And> i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> set r"
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. \<exists>n f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> set r)}

goal (1 subgoal):
 1. (\<And>f n. \<lbrakk>f 0 = a \<and> f n = b; \<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> set r\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f 0 = a \<and> f n = b
?i < n \<Longrightarrow> (f ?i, f (Suc ?i)) \<in> set r

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
from ab steps [of 0] a
[PROOF STATE]
proof (chain)
picking this:
f 0 = a \<and> f n = b
0 < n \<Longrightarrow> (f 0, f (Suc 0)) \<in> set r
a \<notin> fst ` set r
[PROOF STEP]
have "b = a"
[PROOF STATE]
proof (prove)
using this:
f 0 = a \<and> f n = b
0 < n \<Longrightarrow> (f 0, f (Suc 0)) \<in> set r
a \<notin> fst ` set r

goal (1 subgoal):
 1. b = a
[PROOF STEP]
by (cases n, force+)
[PROOF STATE]
proof (state)
this:
b = a

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>*} \<Longrightarrow> ?b2 = a

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>*} \<Longrightarrow> ?b2 = a
[PROOF STEP]
have "?r = {a}"
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>*} \<Longrightarrow> ?b2 = a

goal (1 subgoal):
 1. {b. (a, b) \<in> (set r)\<^sup>*} = {a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{b. (a, b) \<in> (set r)\<^sup>*} = {a}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{b. (a, b) \<in> (set r)\<^sup>*} = {a}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{b. (a, b) \<in> (set r)\<^sup>*} = {a}

goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
unfolding one
[PROOF STATE]
proof (prove)
using this:
{b. (a, b) \<in> (set r)\<^sup>*} = {a}

goal (1 subgoal):
 1. {a} = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
case (Some as)
[PROOF STATE]
proof (state)
this:
rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some as

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
have as: "rs.\<alpha> as = {b. (a,b) \<in> (set r)\<^sup>*}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
using map_of_SomeD [OF Some [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct]]
        rtrancl_rbt_impl [of r "[a]"]
[PROOF STATE]
proof (prove)
using this:
(a, as) \<in> set (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))
rs.\<alpha> (rtrancl_rbt_impl r [a]) = {b. \<exists>a\<in>set [a]. (a, b) \<in> (set r)\<^sup>*}

goal (1 subgoal):
 1. rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, rtrancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}

goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
unfolding memo_rbt_rtrancl_def Let_def Some
[PROOF STATE]
proof (prove)
using this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>*}

goal (1 subgoal):
 1. rs.\<alpha> (case Some as of None \<Rightarrow> rs.from_list [a] | Some as \<Rightarrow> as) = {b. (a, b) \<in> (set r)\<^sup>*}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_rtrancl r a) = {b. (a, b) \<in> (set r)\<^sup>*}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma memo_rbt_trancl:
  "rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}" (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
let ?rm = "rm.to_map
    (map (\<lambda> a. (a, trancl_rbt_impl r [a])) ((rs.to_list \<circ> rs.from_list \<circ> map fst) r))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
proof (cases "rm.lookup a ?rm")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
have one: "?l = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {}
[PROOF STEP]
unfolding memo_rbt_trancl_def Let_def None
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> (case None of None \<Rightarrow> rs.empty () | Some as \<Rightarrow> as) = {}
[PROOF STEP]
by (simp add: rs.correct)
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_trancl r a) = {}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
from None [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct map_of_eq_None_iff]
[PROOF STATE]
proof (chain)
picking this:
a \<notin> fst ` set (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))
[PROOF STEP]
have a: "a \<notin> fst ` set r"
[PROOF STATE]
proof (prove)
using this:
a \<notin> fst ` set (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))

goal (1 subgoal):
 1. a \<notin> fst ` set r
[PROOF STEP]
by (simp add: rs.correct, force)
[PROOF STATE]
proof (state)
this:
a \<notin> fst ` set r

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
a \<notin> fst ` set r

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
assume "b \<in> ?r"
[PROOF STATE]
proof (state)
this:
b \<in> {b. (a, b) \<in> (set r)\<^sup>+}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
from this [unfolded trancl_unfold_left] a
[PROOF STATE]
proof (chain)
picking this:
b \<in> {b. (a, b) \<in> set r O (set r)\<^sup>*}
a \<notin> fst ` set r
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
b \<in> {b. (a, b) \<in> set r O (set r)\<^sup>*}
a \<notin> fst ` set r

goal (1 subgoal):
 1. False
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>+} \<Longrightarrow> False

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>+} \<Longrightarrow> False
[PROOF STEP]
have "?r = {}"
[PROOF STATE]
proof (prove)
using this:
?b2 \<in> {b. (a, b) \<in> (set r)\<^sup>+} \<Longrightarrow> False

goal (1 subgoal):
 1. {b. (a, b) \<in> (set r)\<^sup>+} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{b. (a, b) \<in> (set r)\<^sup>+} = {}

goal (2 subgoals):
 1. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = None \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
 2. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{b. (a, b) \<in> (set r)\<^sup>+} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{b. (a, b) \<in> (set r)\<^sup>+} = {}

goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
unfolding one
[PROOF STATE]
proof (prove)
using this:
{b. (a, b) \<in> (set r)\<^sup>+} = {}

goal (1 subgoal):
 1. {} = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
case (Some as)
[PROOF STATE]
proof (state)
this:
rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some as

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
have as: "rs.\<alpha> as = {b. (a,b) \<in> (set r)\<^sup>+}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
using map_of_SomeD [OF Some [unfolded rm.lookup_correct [OF rm.invar], simplified rm.correct]]
        trancl_rbt_impl [of r "[a]"]
[PROOF STATE]
proof (prove)
using this:
(a, as) \<in> set (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))
rs.\<alpha> (trancl_rbt_impl r [a]) = {b. \<exists>a\<in>set [a]. (a, b) \<in> (set r)\<^sup>+}

goal (1 subgoal):
 1. rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}

goal (1 subgoal):
 1. \<And>aa. rm.lookup a (rm.to_map (map (\<lambda>a. (a, trancl_rbt_impl r [a])) (((rs.to_list \<circ>\<circ> set_op_from_list) rs_ops \<circ>\<circ> map) fst r))) = Some aa \<Longrightarrow> rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}

goal (1 subgoal):
 1. rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
unfolding memo_rbt_trancl_def Let_def Some
[PROOF STATE]
proof (prove)
using this:
rs.\<alpha> as = {b. (a, b) \<in> (set r)\<^sup>+}

goal (1 subgoal):
 1. rs.\<alpha> (case Some as of None \<Rightarrow> rs.empty () | Some as \<Rightarrow> as) = {b. (a, b) \<in> (set r)\<^sup>+}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
rs.\<alpha> (memo_rbt_trancl r a) = {b. (a, b) \<in> (set r)\<^sup>+}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_Image: fixes R shows "\<lbrakk> finite R \<rbrakk> \<Longrightarrow> finite (R `` A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite R \<Longrightarrow> finite (R `` A)
[PROOF STEP]
by (meson Image_iff finite_Range Range.intros finite_subset subsetI)