[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