[STATEMENT]
lemma "\<lbrakk>P \<turnstile> h \<surd>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P\<rbrakk>
  \<Longrightarrow> P \<turnstile> h' \<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> h \<surd>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
[PROOF STEP]
apply (simp add:hconf_def oconf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))) \<and> preallocated h; h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P\<rbrakk> \<Longrightarrow> (\<forall>aa. (aa = a \<longrightarrow> (\<forall>Cs. Subobjs P C Cs \<longrightarrow> (\<exists>!fs'. init_obj P C (Cs, fs'))) \<and> (\<forall>Cs fs'. init_obj P C (Cs, fs') \<longrightarrow> Subobjs P C Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs))) \<and> (aa \<noteq> a \<longrightarrow> (\<forall>ab b. h aa = \<lfloor>(ab, b)\<rfloor> \<longrightarrow> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs))))) \<and> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs\<rbrakk> \<Longrightarrow> \<exists>fs'. init_obj P C (Cs, fs')
 2. \<And>Cs fs' y. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; init_obj P C (Cs, fs'); init_obj P C (Cs, y)\<rbrakk> \<Longrightarrow> fs' = y
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 4. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 6. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (rule_tac x="init_class_fieldmap P (last Cs)" in exI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs\<rbrakk> \<Longrightarrow> init_obj P C (Cs, init_class_fieldmap P (last Cs))
 2. \<And>Cs fs' y. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; init_obj P C (Cs, fs'); init_obj P C (Cs, y)\<rbrakk> \<Longrightarrow> fs' = y
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 4. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 6. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (rule init_obj.intros)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 2. \<And>Cs fs' y. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; init_obj P C (Cs, fs'); init_obj P C (Cs, y)\<rbrakk> \<Longrightarrow> fs' = y
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 4. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 6. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Cs fs' y. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; init_obj P C (Cs, fs'); init_obj P C (Cs, y)\<rbrakk> \<Longrightarrow> fs' = y
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule init_obj.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Cs fs' y Csa. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; init_obj P C (Cs, y); (Cs, fs') = (Csa, init_class_fieldmap P (last Csa)); Subobjs P C Csa\<rbrakk> \<Longrightarrow> fs' = y
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Cs y. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, y); Subobjs P C Cs\<rbrakk> \<Longrightarrow> init_class_fieldmap P (last Cs) = y
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule init_obj.cases)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Cs y Csa. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; Subobjs P C Cs; (Cs, y) = (Csa, init_class_fieldmap P (last Csa)); Subobjs P C Csa\<rbrakk> \<Longrightarrow> init_class_fieldmap P (last Cs) = y
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 3. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 5. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="a" in allE)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; init_obj P C (Cs, fs'); \<forall>aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule init_obj.cases)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs fs' Csa. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; (Cs, fs') = (Csa, init_class_fieldmap P (last Csa)); Subobjs P C Csa\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 2. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="a" in allE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; init_obj P C (Cs, fs'); \<forall>aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule init_obj.cases)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs fs' Csa. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; (Cs, fs') = (Csa, init_class_fieldmap P (last Csa)); Subobjs P C Csa\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; Subobjs P C Cs\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> init_class_fieldmap P (last Cs) (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (drule Subobj_last_isClass)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; preallocated h; Subobjs P C Cs\<rbrakk> \<Longrightarrow> Subobjs P (?C76 Cs) (?Cs76 Cs)
 2. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; preallocated h; Subobjs P C Cs; is_class P (last (?Cs76 Cs))\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> init_class_fieldmap P (last Cs) (:\<le>) map_of fs
 3. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 4. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; preallocated h; Subobjs P C Cs; is_class P (last Cs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> init_class_fieldmap P (last Cs) (:\<le>) map_of fs
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (auto simp:is_class_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs aa aaa b. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; preallocated h; Subobjs P C Cs; class P (last Cs) = \<lfloor>(aa, aaa, b)\<rfloor>\<rbrakk> \<Longrightarrow> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> init_class_fieldmap P (last Cs) (:\<le>) map_of aaa
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (rule fconf_init_fields)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs aa aaa b. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; preallocated h; Subobjs P C Cs; class P (last Cs) = \<lfloor>(aa, aaa, b)\<rfloor>\<rbrakk> \<Longrightarrow> class P (last Cs) = \<lfloor>(?Bs82 Cs aa aaa b, aaa, ?ms82 Cs aa aaa b)\<rfloor>
 2. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 3. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="aa" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>a b. h aa = \<lfloor>(a, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P a Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P a Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="aaa" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>b. h aa = \<lfloor>(aaa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="b" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; h aa = \<lfloor>(aaa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs))\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); \<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (rotate_tac -1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs); h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="Cs" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); \<forall>fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule_tac x="fs'" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs'. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); (Cs, fs') \<in> b \<longrightarrow> Subobjs P aaa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> \<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs' fs Bs ms. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); Subobjs P aaa Cs; P,h \<turnstile> fs' (:\<le>) map_of fs; class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
thm fconf_new
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs' fs Bs ms. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); Subobjs P aaa Cs; P,h \<turnstile> fs' (:\<le>) map_of fs; class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> P,h(a \<mapsto> (C, Collect (init_obj P C))) \<turnstile> fs' (:\<le>) map_of fs
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (erule fconf_new)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>aa aaa b Cs fs' fs Bs ms. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; preallocated h; aa \<noteq> a; h aa = \<lfloor>(aaa, b)\<rfloor>; (Cs, fs') \<in> b; \<forall>Cs. Subobjs P aaa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b); Subobjs P aaa Cs; class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>\<rbrakk> \<Longrightarrow> h a = None
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated (h(a \<mapsto> (C, Collect (init_obj P C))))
[PROOF STEP]
apply (rule preallocated_new)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> preallocated h
 2. \<lbrakk>h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P; \<forall>a aa b. h a = \<lfloor>(aa, b)\<rfloor> \<longrightarrow> (\<forall>Cs. Subobjs P aa Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> b)) \<and> (\<forall>Cs fs'. (Cs, fs') \<in> b \<longrightarrow> Subobjs P aa Cs \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)); preallocated h\<rbrakk> \<Longrightarrow> h a = None
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma eqExcPID_RDD:
"eqExcPID s s1 \<Longrightarrow>
 titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and>
 abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and>
 contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and>
 reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and>
 disPaper (paper s PID) = disPaper (paper s1 PID)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqExcPID s s1 \<Longrightarrow> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)
[PROOF STEP]
using eqExcPID_imp eeqExcPID_RDD
[PROOF STATE]
proof (prove)
using this:
eqExcPID ?s ?s1.0 \<Longrightarrow> confIDs ?s = confIDs ?s1.0 \<and> conf ?s = conf ?s1.0 \<and> userIDs ?s = userIDs ?s1.0 \<and> pass ?s = pass ?s1.0 \<and> user ?s = user ?s1.0 \<and> roles ?s = roles ?s1.0 \<and> paperIDs ?s = paperIDs ?s1.0 \<and> eeqExcPID (paper ?s) (paper ?s1.0) \<and> pref ?s = pref ?s1.0 \<and> voronkov ?s = voronkov ?s1.0 \<and> news ?s = news ?s1.0 \<and> phase ?s = phase ?s1.0 \<and> getAllPaperIDs ?s = getAllPaperIDs ?s1.0 \<and> isRev ?s ?cid ?uid ?pid = isRev ?s1.0 ?cid ?uid ?pid \<and> getReviewIndex ?s ?cid ?uid ?pid = getReviewIndex ?s1.0 ?cid ?uid ?pid \<and> getRevRole ?s ?cid ?uid ?pid = getRevRole ?s1.0 ?cid ?uid ?pid
eeqExcPID ?paps ?paps1.0 \<Longrightarrow> titlePaper (?paps PID) = titlePaper (?paps1.0 PID) \<and> abstractPaper (?paps PID) = abstractPaper (?paps1.0 PID) \<and> contentPaper (?paps PID) = contentPaper (?paps1.0 PID) \<and> reviewsPaper (?paps PID) = reviewsPaper (?paps1.0 PID) \<and> disPaper (?paps PID) = disPaper (?paps1.0 PID)

goal (1 subgoal):
 1. eqExcPID s s1 \<Longrightarrow> titlePaper (paper s PID) = titlePaper (paper s1 PID) \<and> abstractPaper (paper s PID) = abstractPaper (paper s1 PID) \<and> contentPaper (paper s PID) = contentPaper (paper s1 PID) \<and> reviewsPaper (paper s PID) = reviewsPaper (paper s1 PID) \<and> disPaper (paper s PID) = disPaper (paper s1 PID)
[PROOF STEP]
by auto


[STATEMENT]
lemma hadd_succ_right [simp]: "x @+ succ y = succ (x @+ y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x @+ succ y = succ (x @+ y)
[PROOF STEP]
by (metis hadd_hinsert_right succ_def)


[STATEMENT]
lemma diff_hmem_imp_less: assumes "x \<^bold>\<in> y" shows "Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
have  "Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
[PROOF STEP]
by (metis hdiff_iff hsubsetI hsubset_imp_le)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
have "Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<^bold>\<in> y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
by (metis Rep_hf_inject hdiff_iff hinsert_iff)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_hf (y - \<lbrace>x\<rbrace>) \<le> Rep_hf y
Rep_hf (y - \<lbrace>x\<rbrace>) \<noteq> Rep_hf y

goal (1 subgoal):
 1. Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y
[PROOF STEP]
by (metis le_neq_implies_less)
[PROOF STATE]
proof (state)
this:
Rep_hf (y - \<lbrace>x\<rbrace>) < Rep_hf y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]: "(a, 1) \<in> OrdSum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a, 1::'b) \<in> OrdSum
[PROOF STEP]
by (simp add: OrdSum_def)


[STATEMENT]
lemma chain_glb:
  assumes "transp_on (\<sqsubset>) A"
  shows "chain C \<Longrightarrow> glb (\<sqsubset>) C x \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> y \<sqsubset> x \<Longrightarrow> chain ({y} \<union> C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>chain_on (\<sqsubset>) C A; glb (\<sqsubset>) C x; x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> chain_on (\<sqsubset>) ({y} \<union> C) A
[PROOF STEP]
using assms [unfolded transp_on_def]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubset> y \<and> y \<sqsubset> z \<longrightarrow> x \<sqsubset> z

goal (1 subgoal):
 1. \<lbrakk>chain_on (\<sqsubset>) C A; glb (\<sqsubset>) C x; x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> chain_on (\<sqsubset>) ({y} \<union> C) A
[PROOF STEP]
unfolding chain_def glb_def lb_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>A. \<forall>y\<in>A. \<forall>z\<in>A. x \<sqsubset> y \<and> y \<sqsubset> z \<longrightarrow> x \<sqsubset> z

goal (1 subgoal):
 1. \<lbrakk>C \<subseteq> A \<and> (\<forall>x\<in>C. \<forall>y\<in>C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x); Ball C ((\<sqsubseteq>) x) \<and> (\<forall>y. Ball C ((\<sqsubseteq>) y) \<longrightarrow> y \<sqsubseteq> x); x \<in> A; y \<in> A; y \<sqsubset> x\<rbrakk> \<Longrightarrow> {y} \<union> C \<subseteq> A \<and> (\<forall>x\<in>{y} \<union> C. \<forall>y\<in>{y} \<union> C. x \<sqsubseteq> y \<or> y \<sqsubseteq> x)
[PROOF STEP]
by (cases "C = {}") blast+


[STATEMENT]
lemma (in preorder) dc_open_induct [consumes 2, case_names less]:
  assumes "dc_on (\<le>) UNIV"
    and "open_on (\<le>) Q UNIV"
    and "\<And>x. (\<And>y. y < x \<Longrightarrow> Q y) \<Longrightarrow> Q x"
  shows "Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q x
[PROOF STEP]
have "qo_on (\<le>) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qo_on (\<le>) UNIV
[PROOF STEP]
by (auto simp: qo_on_def transp_on_def reflp_on_def dest: order_trans)
[PROOF STATE]
proof (state)
this:
qo_on (\<le>) UNIV

goal (1 subgoal):
 1. Q x
[PROOF STEP]
from open_induct_on [OF this assms(1,2)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
[PROOF STEP]
show "Q x"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
(\<And>y. y < ?x \<Longrightarrow> Q y) \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
unfolding less_le_not_le
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> UNIV; \<And>x. \<lbrakk>x \<in> UNIV; \<And>y. \<lbrakk>y \<in> UNIV; strict (\<le>) y x\<rbrakk> \<Longrightarrow> Q y\<rbrakk> \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> Q ?x
(\<And>y. strict (\<le>) y ?x \<Longrightarrow> Q y) \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. Q x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Q x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parp_sos_cases [elim]:
  assumes "((s, t), a, (s', t')) \<in> parp_sos S T"
      and "\<lbrakk> (s, a, s') \<in> S; \<And>m. a \<noteq> receive m; t' = t \<rbrakk> \<Longrightarrow> P"
      and "\<lbrakk> (t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s \<rbrakk> \<Longrightarrow> P"
      and "\<And>m. \<lbrakk> (s, receive m, s') \<in> S; (t, send m, t') \<in> T \<rbrakk> \<Longrightarrow> P"
    shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
((s, t), a, s', t') \<in> parp_sos S T
\<lbrakk>(s, a, s') \<in> S; \<And>m. a \<noteq> receive m; t' = t\<rbrakk> \<Longrightarrow> P
\<lbrakk>(t, a, t') \<in> T; \<And>m. a \<noteq> send m; s' = s\<rbrakk> \<Longrightarrow> P
\<lbrakk>(s, receive ?m, s') \<in> S; (t, send ?m, t') \<in> T\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by cases auto


[STATEMENT]
lemma delta_unique:
  assumes r: "F (dual r, r) = r"
  shows "r = delta"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta
[PROOF STEP]
unfolding delta_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r = delta_pos
[PROOF STEP]
proof(rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. r \<le> delta_pos
 2. delta_pos \<le> r
[PROOF STEP]
show "delta_pos \<le> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_pos \<le> r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

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

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
have "delta_neg \<le> dual r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
using assms delta_pos_neg_least[where rm=r and rp=r]
[PROOF STATE]
proof (prove)
using this:
F (dual r, r) = r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_neg \<le> dual r
\<lbrakk>r \<le> F (dual r, r); F (dual r, r) \<le> r\<rbrakk> \<Longrightarrow> delta_pos \<le> r

goal (1 subgoal):
 1. delta_neg \<le> dual r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
delta_neg \<le> dual r
[PROOF STEP]
have "r \<le> undual delta_neg"
[PROOF STATE]
proof (prove)
using this:
delta_neg \<le> dual r

goal (1 subgoal):
 1. r \<le> undual delta_neg
[PROOF STEP]
by (simp add: less_eq_dual_def)
[PROOF STATE]
proof (state)
this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<le> undual delta_neg
[PROOF STEP]
show "r \<le> delta_pos"
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg

goal (1 subgoal):
 1. r \<le> delta_pos
[PROOF STEP]
using delta_eq
[PROOF STATE]
proof (prove)
using this:
r \<le> undual delta_neg
undual delta_neg = delta_pos

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma wfLearnLess:
  fixes C::Clause
  shows "wf (learnLess C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf (learnLess C)
[PROOF STEP]
unfolding wf_eq_minimal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> learnLess C \<longrightarrow> y \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> learnLess C \<longrightarrow> y \<notin> Q)
[PROOF STEP]
show "\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
fix F::Formula and Q::"Formula set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
assume "F \<in> Q"
[PROOF STATE]
proof (state)
this:
F \<in> Q

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
have "\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof (cases "\<exists> Fc \<in> Q. C el Fc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>Fc\<in>Q. C el Fc

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>Fc\<in>Q. C el Fc
[PROOF STEP]
obtain Fc where "Fc \<in> Q" "C el Fc"
[PROOF STATE]
proof (prove)
using this:
\<exists>Fc\<in>Q. C el Fc

goal (1 subgoal):
 1. (\<And>Fc. \<lbrakk>Fc \<in> Q; C el Fc\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Fc \<in> Q
C el Fc

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
have "\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
fix F'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show "(F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
assume "(F', Fc) \<in> learnLess C"
[PROOF STATE]
proof (state)
this:
(F', Fc) \<in> learnLess C

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
hence "\<not> C el Fc"
[PROOF STATE]
proof (prove)
using this:
(F', Fc) \<in> learnLess C

goal (1 subgoal):
 1. \<not> C el Fc
[PROOF STEP]
unfolding learnLess_def
[PROOF STATE]
proof (prove)
using this:
(F', Fc) \<in> {(F1, F2). C el F1 \<and> \<not> C el F2}

goal (1 subgoal):
 1. \<not> C el Fc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> C el Fc

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>C el Fc\<close>
[PROOF STATE]
proof (chain)
picking this:
C el Fc
\<not> C el Fc
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
C el Fc
\<not> C el Fc

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

goal (1 subgoal):
 1. (F', Fc) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
thus "F' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. F' \<notin> Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (2 subgoals):
 1. \<exists>Fc\<in>Q. C el Fc \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
 2. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>Fc \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
Fc \<in> Q
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Fc \<in> Q
\<forall>F'. (F', Fc) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (\<exists>Fc\<in>Q. C el Fc)

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
have "\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
fix F'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show "(F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
assume "(F', F) \<in> learnLess C"
[PROOF STATE]
proof (state)
this:
(F', F) \<in> learnLess C

goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
hence "C el F'"
[PROOF STATE]
proof (prove)
using this:
(F', F) \<in> learnLess C

goal (1 subgoal):
 1. C el F'
[PROOF STEP]
unfolding learnLess_def
[PROOF STATE]
proof (prove)
using this:
(F', F) \<in> {(F1, F2). C el F1 \<and> \<not> C el F2}

goal (1 subgoal):
 1. C el F'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
C el F'

goal (1 subgoal):
 1. (F', F) \<in> learnLess C \<Longrightarrow> F' \<notin> Q
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> (\<exists>Fc\<in>Q. C el Fc)
C el F'
[PROOF STEP]
show "F' \<notin> Q"
[PROOF STATE]
proof (prove)
using this:
\<not> (\<exists>Fc\<in>Q. C el Fc)
C el F'

goal (1 subgoal):
 1. F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<not> (\<exists>Fc\<in>Q. C el Fc) \<Longrightarrow> \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
with \<open>F \<in> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> Q
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F \<in> Q
\<forall>F'. (F', F) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?F2 \<in> ?Q2 \<Longrightarrow> \<exists>Fmin\<in>?Q2. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?F2 \<in> ?Q2 \<Longrightarrow> \<exists>Fmin\<in>?Q2. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> ?Q2

goal (1 subgoal):
 1. \<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>Q F. F \<in> Q \<longrightarrow> (\<exists>Fmin\<in>Q. \<forall>F'. (F', Fmin) \<in> learnLess C \<longrightarrow> F' \<notin> Q)

goal:
No subgoals!
[PROOF STEP]
qed