[STATEMENT]
theorem assumes wf:"wwf_prog P"
shows red_preserves_hconf:
  "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow> (\<And>T. \<lbrakk> P,E,h \<turnstile> e : T; P \<turnstile> h \<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>)"
and reds_preserves_hconf:
  "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow> (\<And>Ts. \<lbrakk> P,E,h \<turnstile> es [:] Ts; P \<turnstile> h \<surd> \<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> (\<And>T. \<lbrakk>P,E,h \<turnstile> e : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>)) &&& (P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> (\<And>Ts. \<lbrakk>P,E,h \<turnstile> es [:] Ts; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>))
[PROOF STEP]
proof (induct rule:red_reds_inducts)
[PROOF STATE]
proof (state)
goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 61 subgoals...
[PROOF STEP]
case (RedNew h a h' C E l)
[PROOF STATE]
proof (state)
this:
new_Addr h = \<lfloor>a\<rfloor>
h' = h(a \<mapsto> (C, Collect (init_obj P C)))
P,E,h \<turnstile> new C : T
P \<turnstile> h \<surd>

goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 61 subgoals...
[PROOF STEP]
have new: "new_Addr h = Some a" and h':"h' = h(a \<mapsto> (C, Collect (init_obj P C)))"
    and hconf:"P \<turnstile> h \<surd>" and wt_New:"P,E,h \<turnstile> new C : T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (new_Addr h = \<lfloor>a\<rfloor> &&& h' = h(a \<mapsto> (C, Collect (init_obj P C)))) &&& P \<turnstile> h \<surd> &&& P,E,h \<turnstile> new C : T
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
new_Addr h = \<lfloor>a\<rfloor>
h' = h(a \<mapsto> (C, Collect (init_obj P C)))
P \<turnstile> h \<surd>
P,E,h \<turnstile> new C : T

goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 61 subgoals...
[PROOF STEP]
from new
[PROOF STATE]
proof (chain)
picking this:
new_Addr h = \<lfloor>a\<rfloor>
[PROOF STEP]
have None: "h a = None"
[PROOF STATE]
proof (prove)
using this:
new_Addr h = \<lfloor>a\<rfloor>

goal (1 subgoal):
 1. h a = None
[PROOF STEP]
by(rule new_Addr_SomeD)
[PROOF STATE]
proof (state)
this:
h a = None

goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 61 subgoals...
[PROOF STEP]
with wf
[PROOF STATE]
proof (chain)
picking this:
wwf_prog P
h a = None
[PROOF STEP]
have oconf:"P,h \<turnstile> (C, Collect (init_obj P C)) \<surd>"
[PROOF STATE]
proof (prove)
using this:
wwf_prog P
h a = None

goal (1 subgoal):
 1. P,h \<turnstile> (C, Collect (init_obj P C)) \<surd>
[PROOF STEP]
apply (auto simp:oconf_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs. \<lbrakk>wwf_prog P; h a = None; Subobjs P C Cs\<rbrakk> \<Longrightarrow> \<exists>fs'. init_obj P C (Cs, fs')
 2. \<And>Cs fs' y. \<lbrakk>wwf_prog P; h a = None; 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>wwf_prog P; h a = None; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 4. \<And>Cs fs'. \<lbrakk>wwf_prog P; h a = None; 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 \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (rule_tac x="init_class_fieldmap P (last Cs)" in exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>Cs. \<lbrakk>wwf_prog P; h a = None; Subobjs P C Cs\<rbrakk> \<Longrightarrow> init_obj P C (Cs, init_class_fieldmap P (last Cs))
 2. \<And>Cs fs' y. \<lbrakk>wwf_prog P; h a = None; 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>wwf_prog P; h a = None; init_obj P C (Cs, fs')\<rbrakk> \<Longrightarrow> Subobjs P C Cs
 4. \<And>Cs fs'. \<lbrakk>wwf_prog P; h a = None; 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 \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
by (fastforce intro:init_obj.intros fconf_init_fields
                 elim: init_obj.cases dest!:Subobj_last_isClass simp:is_class_def)+
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> (C, Collect (init_obj P C)) \<surd>

goal (61 subgoals):
 1. \<And>h a h' C E l T. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
 2. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 3. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 4. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 5. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 9. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 10. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 61 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> (C, Collect (init_obj P C)) \<surd>

goal (1 subgoal):
 1. P \<turnstile> h' \<surd>
[PROOF STEP]
using h' None
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> (C, Collect (init_obj P C)) \<surd>
h' = h(a \<mapsto> (C, Collect (init_obj P C)))
h a = None

goal (1 subgoal):
 1. P \<turnstile> h' \<surd>
[PROOF STEP]
by(fast intro: hconf_new[OF hconf])
[PROOF STATE]
proof (state)
this:
P \<turnstile> h' \<surd>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
case (RedFAss h a D S Cs' F T Cs v v' Ds fs' E l T')
[PROOF STATE]
proof (state)
this:
h a = \<lfloor>(D, S)\<rfloor>
P \<turnstile> last Cs' has least F:T via Cs
P \<turnstile> T casts v to v'
Ds = Cs' @\<^sub>p Cs
(Ds, fs') \<in> S
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'
P \<turnstile> h \<surd>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
let ?fs' = "fs'(F \<mapsto> v')"
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
let ?S' = "insert (Ds, ?fs') (S - {(Ds, fs')})"
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
have ha:"h a = Some(D,S)" and hconf:"P \<turnstile> h \<surd>"
    and field:"P \<turnstile> last Cs' has least F:T via Cs"
    and casts:"P \<turnstile> T casts v to v'"
    and Ds:"Ds = Cs' @\<^sub>p Cs" and S:"(Ds,fs') \<in> S"
    and wte:"P,E,h \<turnstile> ref(a,Cs')\<bullet>F{Cs} := Val v : T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h a = \<lfloor>(D, S)\<rfloor> &&& P \<turnstile> h \<surd> &&& P \<turnstile> last Cs' has least F:T via Cs) &&& (P \<turnstile> T casts v to v'  &&& Ds = Cs' @\<^sub>p Cs) &&& (Ds, fs') \<in> S &&& P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
h a = \<lfloor>(D, S)\<rfloor>
P \<turnstile> h \<surd>
P \<turnstile> last Cs' has least F:T via Cs
P \<turnstile> T casts v to v'
Ds = Cs' @\<^sub>p Cs
(Ds, fs') \<in> S
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from wte
[PROOF STATE]
proof (chain)
picking this:
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'
[PROOF STEP]
have "P \<turnstile> last Cs' has least F:T' via Cs"
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'

goal (1 subgoal):
 1. P \<turnstile> last Cs' has least F:T' via Cs
[PROOF STEP]
by (auto split:if_split_asm)
[PROOF STATE]
proof (state)
this:
P \<turnstile> last Cs' has least F:T' via Cs

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with field
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> last Cs' has least F:T via Cs
P \<turnstile> last Cs' has least F:T' via Cs
[PROOF STEP]
have eq:"T = T'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> last Cs' has least F:T via Cs
P \<turnstile> last Cs' has least F:T' via Cs

goal (1 subgoal):
 1. T = T'
[PROOF STEP]
by (rule sees_field_fun)
[PROOF STATE]
proof (state)
this:
T = T'

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with casts wte wf
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> T casts v to v'
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'
wwf_prog P
T = T'
[PROOF STEP]
have conf:"P,h \<turnstile> v' :\<le> T'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> T casts v to v'
P,E,h \<turnstile> ref (a, Cs')\<bullet>F{Cs} := Val v : T'
wwf_prog P
T = T'

goal (1 subgoal):
 1. P,h \<turnstile> v' :\<le> T'
[PROOF STEP]
by(auto intro:casts_conf)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> v' :\<le> T'

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from hconf ha
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> h \<surd>
h a = \<lfloor>(D, S)\<rfloor>
[PROOF STEP]
have oconf:"P,h \<turnstile> (D,S) \<surd>"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> h \<surd>
h a = \<lfloor>(D, S)\<rfloor>

goal (1 subgoal):
 1. P,h \<turnstile> (D, S) \<surd>
[PROOF STEP]
by (fastforce simp:hconf_def)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> (D, S) \<surd>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with S
[PROOF STATE]
proof (chain)
picking this:
(Ds, fs') \<in> S
P,h \<turnstile> (D, S) \<surd>
[PROOF STEP]
have suboD:"Subobjs P D Ds"
[PROOF STATE]
proof (prove)
using this:
(Ds, fs') \<in> S
P,h \<turnstile> (D, S) \<surd>

goal (1 subgoal):
 1. Subobjs P D Ds
[PROOF STEP]
by (fastforce simp:oconf_def)
[PROOF STATE]
proof (state)
this:
Subobjs P D Ds

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from field
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> last Cs' has least F:T via Cs
[PROOF STEP]
obtain Bs fs ms
    where subo:"Subobjs P (last Cs') Cs"
    and "class": "class P (last Cs) = Some(Bs,fs,ms)"
    and map:"map_of fs F = Some T"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> last Cs' has least F:T via Cs

goal (1 subgoal):
 1. (\<And>Bs fs ms. \<lbrakk>Subobjs P (last Cs') Cs; class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>; map_of fs F = \<lfloor>T\<rfloor>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp:LeastFieldDecl_def FieldDecls_def)
[PROOF STATE]
proof (state)
this:
Subobjs P (last Cs') Cs
class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>
map_of fs F = \<lfloor>T\<rfloor>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from Ds subo
[PROOF STATE]
proof (chain)
picking this:
Ds = Cs' @\<^sub>p Cs
Subobjs P (last Cs') Cs
[PROOF STEP]
have last:"last Cs = last Ds"
[PROOF STATE]
proof (prove)
using this:
Ds = Cs' @\<^sub>p Cs
Subobjs P (last Cs') Cs

goal (1 subgoal):
 1. last Cs = last Ds
[PROOF STEP]
by(fastforce dest:Subobjs_nonempty intro:appendPath_last simp:appendPath_last)
[PROOF STATE]
proof (state)
this:
last Cs = last Ds

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with "class"
[PROOF STATE]
proof (chain)
picking this:
class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>
last Cs = last Ds
[PROOF STEP]
have classDs:"class P (last Ds) = Some(Bs,fs,ms)"
[PROOF STATE]
proof (prove)
using this:
class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor>
last Cs = last Ds

goal (1 subgoal):
 1. class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with S suboD oconf
[PROOF STATE]
proof (chain)
picking this:
(Ds, fs') \<in> S
Subobjs P D Ds
P,h \<turnstile> (D, S) \<surd>
class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>
[PROOF STEP]
have "P,h \<turnstile> fs' (:\<le>) map_of fs"
[PROOF STATE]
proof (prove)
using this:
(Ds, fs') \<in> S
Subobjs P D Ds
P,h \<turnstile> (D, S) \<surd>
class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>

goal (1 subgoal):
 1. P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (auto simp:oconf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Ds, fs') \<in> S; class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>; \<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S); \<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D 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> P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Ds, fs') \<in> S; class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>; \<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D 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); Subobjs P D ?Cs12 \<longrightarrow> (\<exists>!fs'. (?Cs12, fs') \<in> S)\<rbrakk> \<Longrightarrow> P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule_tac x="Ds" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Ds, fs') \<in> S; class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>; Subobjs P D ?Cs12 \<longrightarrow> (\<exists>!fs'. (?Cs12, fs') \<in> S); \<forall>fs'. (Ds, fs') \<in> S \<longrightarrow> Subobjs P D Ds \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply (erule_tac x="fs'" in allE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(Ds, fs') \<in> S; class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>; Subobjs P D ?Cs12 \<longrightarrow> (\<exists>!fs'. (?Cs12, fs') \<in> S); (Ds, fs') \<in> S \<longrightarrow> Subobjs P D Ds \<and> (\<exists>fs. (\<exists>Bs ms. class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>) \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)\<rbrakk> \<Longrightarrow> P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> fs' (:\<le>) map_of fs

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with map conf eq
[PROOF STATE]
proof (chain)
picking this:
map_of fs F = \<lfloor>T\<rfloor>
P,h \<turnstile> v' :\<le> T'
T = T'
P,h \<turnstile> fs' (:\<le>) map_of fs
[PROOF STEP]
have fconf:"P,h \<turnstile> fs'(F \<mapsto> v') (:\<le>) map_of fs"
[PROOF STATE]
proof (prove)
using this:
map_of fs F = \<lfloor>T\<rfloor>
P,h \<turnstile> v' :\<le> T'
T = T'
P,h \<turnstile> fs' (:\<le>) map_of fs

goal (1 subgoal):
 1. P,h \<turnstile> fs'(F \<mapsto> v') (:\<le>) map_of fs
[PROOF STEP]
by (simp add:fconf_def)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> fs'(F \<mapsto> v') (:\<le>) map_of fs

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from oconf
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> (D, S) \<surd>
[PROOF STEP]
have "\<forall>Cs fs'. (Cs,fs') \<in> S \<longrightarrow> Subobjs P D Cs \<and>
                    (\<exists>fs Bs ms. class P (last Cs) = Some (Bs,fs,ms) \<and>
                                P,h \<turnstile> fs' (:\<le>) map_of fs)"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> (D, S) \<surd>

goal (1 subgoal):
 1. \<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)
[PROOF STEP]
by(simp add:oconf_def)
[PROOF STATE]
proof (state)
this:
\<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with suboD classDs fconf
[PROOF STATE]
proof (chain)
picking this:
Subobjs P D Ds
class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>
P,h \<turnstile> fs'(F \<mapsto> v') (:\<le>) map_of fs
\<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)
[PROOF STEP]
have oconf':"\<forall>Cs fs'. (Cs,fs') \<in> ?S' \<longrightarrow> Subobjs P D Cs \<and>
                    (\<exists>fs Bs ms. class P (last Cs) = Some (Bs,fs,ms) \<and>
                                P,h \<turnstile> fs' (:\<le>) map_of fs)"
[PROOF STATE]
proof (prove)
using this:
Subobjs P D Ds
class P (last Ds) = \<lfloor>(Bs, fs, ms)\<rfloor>
P,h \<turnstile> fs'(F \<mapsto> v') (:\<le>) map_of fs
\<forall>Cs fs'. (Cs, fs') \<in> S \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs' (:\<le>) map_of fs)

goal (1 subgoal):
 1. \<forall>Cs fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}) \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs'a (:\<le>) map_of fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>Cs fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}) \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs'a (:\<le>) map_of fs)

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
from oconf
[PROOF STATE]
proof (chain)
picking this:
P,h \<turnstile> (D, S) \<surd>
[PROOF STEP]
have all:"\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs,fs') \<in> S)"
[PROOF STATE]
proof (prove)
using this:
P,h \<turnstile> (D, S) \<surd>

goal (1 subgoal):
 1. \<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S)
[PROOF STEP]
by(simp add:oconf_def)
[PROOF STATE]
proof (state)
this:
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S)

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with S
[PROOF STATE]
proof (chain)
picking this:
(Ds, fs') \<in> S
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S)
[PROOF STEP]
have "\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs,fs') \<in> ?S')"
[PROOF STATE]
proof (prove)
using this:
(Ds, fs') \<in> S
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'. (Cs, fs') \<in> S)

goal (1 subgoal):
 1. \<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with oconf'
[PROOF STATE]
proof (chain)
picking this:
\<forall>Cs fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}) \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs'a (:\<le>) map_of fs)
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))
[PROOF STEP]
have oconf':"P,h \<turnstile> (D,?S') \<surd>"
[PROOF STATE]
proof (prove)
using this:
\<forall>Cs fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}) \<longrightarrow> Subobjs P D Cs \<and> (\<exists>fs Bs ms. class P (last Cs) = \<lfloor>(Bs, fs, ms)\<rfloor> \<and> P,h \<turnstile> fs'a (:\<le>) map_of fs)
\<forall>Cs. Subobjs P D Cs \<longrightarrow> (\<exists>!fs'a. (Cs, fs'a) \<in> insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))

goal (1 subgoal):
 1. P,h \<turnstile> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')})) \<surd>
[PROOF STEP]
by (simp add:oconf_def)
[PROOF STATE]
proof (state)
this:
P,h \<turnstile> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')})) \<surd>

goal (60 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 60 subgoals...
[PROOF STEP]
with hconf ha
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> h \<surd>
h a = \<lfloor>(D, S)\<rfloor>
P,h \<turnstile> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')})) \<surd>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> h \<surd>
h a = \<lfloor>(D, S)\<rfloor>
P,h \<turnstile> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')})) \<surd>

goal (1 subgoal):
 1. P \<turnstile> h(a \<mapsto> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))) \<surd>
[PROOF STEP]
by (rule hconf_upd_obj)
[PROOF STATE]
proof (state)
this:
P \<turnstile> h(a \<mapsto> (D, insert (Ds, fs'(F \<mapsto> v')) (S - {(Ds, fs')}))) \<surd>

goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 59 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 59 subgoals...
[PROOF STEP]
case (CallObj E e h l e' h' l' Copt M es)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> e : ?T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
P,E,h \<turnstile> Call e Copt M es : T
P \<turnstile> h \<surd>

goal (59 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 59 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> e : ?T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
P,E,h \<turnstile> Call e Copt M es : T
P \<turnstile> h \<surd>

goal (1 subgoal):
 1. P \<turnstile> h' \<surd>
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> h' \<surd>

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 58 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 58 subgoals...
[PROOF STEP]
case (CallParams E es h l es' h' l' v Copt M)
[PROOF STATE]
proof (state)
this:
P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> es [:] ?Ts; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
P,E,h \<turnstile> Call (Val v) Copt M es : T
P \<turnstile> h \<surd>

goal (58 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 58 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle>
\<lbrakk>P,E,h \<turnstile> es [:] ?Ts; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h' \<surd>
P,E,h \<turnstile> Call (Val v) Copt M es : T
P \<turnstile> h \<surd>

goal (1 subgoal):
 1. P \<turnstile> h' \<surd>
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> h' \<surd>

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 57 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 57 subgoals...
[PROOF STEP]
case (RedCallNull E Copt M vs h l)
[PROOF STATE]
proof (state)
this:
P,E,h \<turnstile> Call null Copt M (map Val vs) : T
P \<turnstile> h \<surd>

goal (57 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 57 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E,h \<turnstile> Call null Copt M (map Val vs) : T
P \<turnstile> h \<surd>

goal (1 subgoal):
 1. P \<turnstile> h \<surd>
[PROOF STEP]
by (cases Copt) auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> h \<surd>

goal (56 subgoals):
 1. \<And>h E C l T. \<lbrakk>new_Addr h = None; P,E,h \<turnstile> new C : T; P \<turnstile> h \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> h \<surd>
 2. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> \<lparr>C\<rparr>e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 3. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> \<lparr>C\<rparr>null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 4. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 5. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs') : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 6. \<And>C Cs E a aa b T. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; P,E,aa \<turnstile> \<lparr>C\<rparr>ref (a, Cs) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 7. \<And>E e a b e' aa ba C T. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<And>T. \<lbrakk>P,E,a \<turnstile> e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>; P,E,a \<turnstile> Cast C e : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 8. \<And>E C a b T. \<lbrakk>P,E,a \<turnstile> Cast C null : T; P \<turnstile> a \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> a \<surd>
 9. \<And>Cs C Cs' Ds E a aa b T. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; P,E,aa \<turnstile> Cast C (ref (a, Cs)) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
 10. \<And>E C a Cs Cs' aa b T. \<lbrakk>P,E,aa \<turnstile> Cast C (ref (a, Cs @ [C] @ Cs')) : T; P \<turnstile> aa \<surd>\<rbrakk> \<Longrightarrow> P \<turnstile> aa \<surd>
A total of 56 subgoals...
[PROOF STEP]
qed auto