[STATEMENT]
lemma assumes wf: "wf_C_prog P"
shows red_preserves_defass:
  "P,E \<turnstile> \<langle>e,(h,l)\<rangle> \<rightarrow> \<langle>e',(h',l')\<rangle> \<Longrightarrow> \<D> e \<lfloor>dom l\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom l'\<rfloor>"
and "P,E \<turnstile> \<langle>es,(h,l)\<rangle> [\<rightarrow>] \<langle>es',(h',l')\<rangle> \<Longrightarrow> \<D>s es \<lfloor>dom l\<rfloor> \<Longrightarrow> \<D>s es' \<lfloor>dom l'\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P,E \<turnstile> \<langle>e,(h, l)\<rangle> \<rightarrow> \<langle>e',(h', l')\<rangle>; \<D> e \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom l'\<rfloor>) &&& (\<lbrakk>P,E \<turnstile> \<langle>es,(h, l)\<rangle> [\<rightarrow>] \<langle>es',(h', l')\<rangle>; \<D>s es \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D>s es' \<lfloor>dom l'\<rfloor>)
[PROOF STEP]
proof (induct rule:red_reds_inducts)
[PROOF STATE]
proof (state)
goal (61 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 61 subgoals...
[PROOF STEP]
case BinOpRed1
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (e_ \<guillemotleft>bop_\<guillemotright> e\<^sub>2_) \<lfloor>dom b___\<rfloor>

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

goal (1 subgoal):
 1. \<D> (e'_ \<guillemotleft>bop_\<guillemotright> e\<^sub>2_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (e'_ \<guillemotleft>bop_\<guillemotright> e\<^sub>2_) \<lfloor>dom b_\<rfloor>

goal (60 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 60 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (60 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 60 subgoals...
[PROOF STEP]
case FAssRed1
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (e_\<bullet>F_{Cs_} := e\<^sub>2_) \<lfloor>dom b___\<rfloor>

goal (60 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 60 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (e_\<bullet>F_{Cs_} := e\<^sub>2_) \<lfloor>dom b___\<rfloor>

goal (1 subgoal):
 1. \<D> (e'_\<bullet>F_{Cs_} := e\<^sub>2_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (e'_\<bullet>F_{Cs_} := e\<^sub>2_) \<lfloor>dom b_\<rfloor>

goal (59 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 59 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (59 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 59 subgoals...
[PROOF STEP]
case CallObj
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (Call e_ Copt_ M_ es_) \<lfloor>dom b___\<rfloor>

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

goal (1 subgoal):
 1. \<D> (Call e'_ Copt_ M_ es_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: Ds_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (Call e'_ Copt_ M_ es_) \<lfloor>dom b_\<rfloor>

goal (58 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 58 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (58 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 58 subgoals...
[PROOF STEP]
case (RedCall h l a C S Cs M Ts' T' pns' body' Ds Ts T pns body Cs'
                vs bs new_body E)
[PROOF STATE]
proof (state)
this:
hp (h, l) a = \<lfloor>(C, S)\<rfloor>
P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds
P \<turnstile> (C,Cs @\<^sub>p Ds) selects M = (Ts, T, pns, body) via Cs'
length vs = length pns
length Ts = length pns
bs = blocks (this # pns, Class (last Cs') # Ts, Ref (a, Cs') # vs, body)
new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>bs | _ \<Rightarrow> bs)
\<D> (Call (ref (a, Cs)) None M (map Val vs)) \<lfloor>dom l\<rfloor>

goal (58 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 58 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
hp (h, l) a = \<lfloor>(C, S)\<rfloor>
P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds
P \<turnstile> (C,Cs @\<^sub>p Ds) selects M = (Ts, T, pns, body) via Cs'
length vs = length pns
length Ts = length pns
bs = blocks (this # pns, Class (last Cs') # Ts, Ref (a, Cs') # vs, body)
new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>bs | _ \<Rightarrow> bs)
\<D> (Call (ref (a, Cs)) None M (map Val vs)) \<lfloor>dom l\<rfloor>

goal (1 subgoal):
 1. \<D> new_body \<lfloor>dom l\<rfloor>
[PROOF STEP]
apply (auto dest!:select_method_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
[PROOF STEP]
apply(cases T')
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Void\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
 2. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Boolean\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
 3. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Integer\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
 4. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = NT\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
 5. \<And>x5. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', T', pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}); \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Class x5\<rbrakk> \<Longrightarrow> \<D> (case T' of Class D \<Rightarrow> \<lparr>D\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)} | _ \<Rightarrow> {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}) \<lfloor>dom l\<rfloor>
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', Void, pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Void\<rbrakk> \<Longrightarrow> \<D> body \<lfloor>insert this (dom l \<union> set pns)\<rfloor>
 2. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', Boolean, pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Boolean\<rbrakk> \<Longrightarrow> \<D> body \<lfloor>insert this (dom l \<union> set pns)\<rfloor>
 3. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', Integer, pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Integer\<rbrakk> \<Longrightarrow> \<D> body \<lfloor>insert this (dom l \<union> set pns)\<rfloor>
 4. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', NT, pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = NT\<rbrakk> \<Longrightarrow> \<D> body \<lfloor>insert this (dom l \<union> set pns)\<rfloor>
 5. \<And>x5. \<lbrakk>h a = \<lfloor>(C, S)\<rfloor>; P \<turnstile> last Cs has least M = (Ts', Class x5, pns', body') via Ds; length vs = length pns; length Ts = length pns; new_body = \<lparr>x5\<rparr>{this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<D>s (map Val vs) \<lfloor>dom l\<rfloor>; bs = {this:Class (last Cs'); this:=ref (a, Cs');; blocks (pns, Ts, vs, body)}; \<forall>x\<in>set Ts. is_type P x; is_type P T; T \<noteq> NT; distinct pns; this \<notin> set pns; P,[pns [\<mapsto>] Ts, this \<mapsto> Class (last Cs')] \<turnstile> body :: T; \<D> body \<lfloor>insert this (set pns)\<rfloor>; T' = Class x5\<rbrakk> \<Longrightarrow> \<D> body \<lfloor>insert this (dom l \<union> set pns)\<rfloor>
[PROOF STEP]
by(rule_tac A="\<lfloor>insert this (set pns)\<rfloor>" in D_mono,clarsimp simp:hyperset_defs,
          assumption)+
[PROOF STATE]
proof (state)
this:
\<D> new_body \<lfloor>dom l\<rfloor>

goal (57 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 57 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (57 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 57 subgoals...
[PROOF STEP]
case RedStaticCall
[PROOF STATE]
proof (state)
this:
P \<turnstile> Path last Cs_ to C_ unique
P \<turnstile> Path last Cs_ to C_ via Cs''_
P \<turnstile> C_ has least M_ = (Ts_, T_, pns_, body_) via Cs'_
Ds_ = (Cs_ @\<^sub>p Cs''_) @\<^sub>p Cs'_
length vs_ = length pns_
length Ts_ = length pns_
\<D> (Call (ref (a___, Cs_)) \<lfloor>C_\<rfloor> M_ (map Val vs_)) \<lfloor>dom b_\<rfloor>

goal (57 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 57 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> Path last Cs_ to C_ unique
P \<turnstile> Path last Cs_ to C_ via Cs''_
P \<turnstile> C_ has least M_ = (Ts_, T_, pns_, body_) via Cs'_
Ds_ = (Cs_ @\<^sub>p Cs''_) @\<^sub>p Cs'_
length vs_ = length pns_
length Ts_ = length pns_
\<D> (Call (ref (a___, Cs_)) \<lfloor>C_\<rfloor> M_ (map Val vs_)) \<lfloor>dom b_\<rfloor>

goal (1 subgoal):
 1. \<D> (blocks (this # pns_, Class (last Ds_) # Ts_, Ref (a___, Ds_) # vs_, body_)) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
apply (auto dest!:has_least_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<turnstile> Path last Cs_ to C_ unique; P \<turnstile> Path last Cs_ to C_ via Cs''_ ; Ds_ = (Cs_ @\<^sub>p Cs''_) @\<^sub>p Cs'_; length vs_ = length pns_; length Ts_ = length pns_; \<D>s (map Val vs_) \<lfloor>dom b_\<rfloor>; \<forall>x\<in>set Ts_. is_type P x; is_type P T_; T_ \<noteq> NT; distinct pns_; this \<notin> set pns_; P,[pns_ [\<mapsto>] Ts_, this \<mapsto> Class (last Cs'_)] \<turnstile> body_ :: T_\<rbrakk> \<Longrightarrow> \<lfloor>insert this (set pns_)\<rfloor> \<sqsubseteq> \<lfloor>insert this (dom b_ \<union> set pns_)\<rfloor>
[PROOF STEP]
by(auto simp:hyperset_defs)
[PROOF STATE]
proof (state)
this:
\<D> (blocks (this # pns_, Class (last Ds_) # Ts_, Ref (a___, Ds_) # vs_, body_)) \<lfloor>dom b_\<rfloor>

goal (56 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 56 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (56 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 56 subgoals...
[PROOF STEP]
case InitBlockRed
[PROOF STATE]
proof (state)
this:
P,E_(V_ \<mapsto> T_) \<turnstile> \<langle>e_,(h_, l_(V_ \<mapsto> v'_))\<rangle> \<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (l_(V_ \<mapsto> v'_))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom l'_\<rfloor>
l'_ V_ = \<lfloor>v''_\<rfloor>
P \<turnstile> T_ casts v_ to v'_
\<D> {V_:T_; V_:=Val v_;; e_} \<lfloor>dom l_\<rfloor>

goal (56 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 56 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E_(V_ \<mapsto> T_) \<turnstile> \<langle>e_,(h_, l_(V_ \<mapsto> v'_))\<rangle> \<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (l_(V_ \<mapsto> v'_))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom l'_\<rfloor>
l'_ V_ = \<lfloor>v''_\<rfloor>
P \<turnstile> T_ casts v_ to v'_
\<D> {V_:T_; V_:=Val v_;; e_} \<lfloor>dom l_\<rfloor>

goal (1 subgoal):
 1. \<D> {V_:T_; V_:=Val v''_;; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>
[PROOF STEP]
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
[PROOF STATE]
proof (state)
this:
\<D> {V_:T_; V_:=Val v''_;; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>

goal (55 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 55 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (55 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 55 subgoals...
[PROOF STEP]
case BlockRedNone
[PROOF STATE]
proof (state)
this:
P,E_(V_ \<mapsto> T_) \<turnstile> \<langle>e_,(h_, l_(V_ := None))\<rangle> \<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (l_(V_ := None))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom l'_\<rfloor>
l'_ V_ = None
\<not> assigned V_ e_
\<D> {V_:T_; e_} \<lfloor>dom l_\<rfloor>

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

goal (1 subgoal):
 1. \<D> {V_:T_; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>
[PROOF STEP]
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
[PROOF STATE]
proof (state)
this:
\<D> {V_:T_; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>

goal (54 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 54 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (54 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 54 subgoals...
[PROOF STEP]
case BlockRedSome
[PROOF STATE]
proof (state)
this:
P,E_(V_ \<mapsto> T_) \<turnstile> \<langle>e_,(h_, l_(V_ := None))\<rangle> \<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (l_(V_ := None))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom l'_\<rfloor>
l'_ V_ = \<lfloor>v_\<rfloor>
\<not> assigned V_ e_
\<D> {V_:T_; e_} \<lfloor>dom l_\<rfloor>

goal (54 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 54 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P,E_(V_ \<mapsto> T_) \<turnstile> \<langle>e_,(h_, l_(V_ := None))\<rangle> \<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (l_(V_ := None))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom l'_\<rfloor>
l'_ V_ = \<lfloor>v_\<rfloor>
\<not> assigned V_ e_
\<D> {V_:T_; e_} \<lfloor>dom l_\<rfloor>

goal (1 subgoal):
 1. \<D> {V_:T_; V_:=Val v_;; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>
[PROOF STEP]
by(auto simp:hyperset_defs elim!:D_mono' simp del:fun_upd_apply)
[PROOF STATE]
proof (state)
this:
\<D> {V_:T_; V_:=Val v_;; e'_} \<lfloor>dom (l'_(V_ := l_ V_))\<rfloor>

goal (53 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 53 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (53 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 53 subgoals...
[PROOF STEP]
case SeqRed
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (e_;; e\<^sub>2_) \<lfloor>dom b___\<rfloor>

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

goal (1 subgoal):
 1. \<D> (e'_;; e\<^sub>2_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (e'_;; e\<^sub>2_) \<lfloor>dom b_\<rfloor>

goal (52 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 52 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (52 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 52 subgoals...
[PROOF STEP]
case CondRed
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D> (if (e_) e\<^sub>1_ else e\<^sub>2_) \<lfloor>dom b___\<rfloor>

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

goal (1 subgoal):
 1. \<D> (if (e'_) e\<^sub>1_ else e\<^sub>2_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (if (e'_) e\<^sub>1_ else e\<^sub>2_) \<lfloor>dom b_\<rfloor>

goal (51 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 51 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (51 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 51 subgoals...
[PROOF STEP]
case RedWhile
[PROOF STATE]
proof (state)
this:
\<D> (while (b___) c_) \<lfloor>dom b_\<rfloor>

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

goal (1 subgoal):
 1. \<D> (if (b___) (c_;; while (b___) c_) else unit) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by(auto simp:hyperset_defs elim!:D_mono')
[PROOF STATE]
proof (state)
this:
\<D> (if (b___) (c_;; while (b___) c_) else unit) \<lfloor>dom b_\<rfloor>

goal (50 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 50 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (50 subgoals):
 1. \<And>h a h' C E l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, [C])) \<lfloor>dom l\<rfloor>
 2. \<And>h E C l. \<lbrakk>new_Addr h = None; \<D> (new C) \<lfloor>dom l\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory, [OutOfMemory])) \<lfloor>dom l\<rfloor>
 3. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (\<lparr>C\<rparr>e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (\<lparr>C\<rparr>e') \<lfloor>dom ba\<rfloor>
 4. \<And>E C a b. \<D> (\<lparr>C\<rparr>null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 5. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
 6. \<And>E C a Cs Cs' aa b. \<D> (\<lparr>C\<rparr>ref (a, Cs @ [C] @ Cs')) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> (ref (a, Cs @ [C])) \<lfloor>dom b\<rfloor>
 7. \<And>C Cs E a aa b. \<lbrakk>C \<notin> set Cs; (last Cs, C) \<notin> (subcls1 P)\<^sup>*; \<D> (\<lparr>C\<rparr>ref (a, Cs)) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast, [ClassCast])) \<lfloor>dom b\<rfloor>
 8. \<And>E e a b e' aa ba C. \<lbrakk>P,E \<turnstile> \<langle>e,(a, b)\<rangle> \<rightarrow> \<langle>e',(aa, ba)\<rangle>; \<D> e \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom ba\<rfloor>; \<D> (Cast C e) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom ba\<rfloor>
 9. \<And>E C a b. \<D> (Cast C null) \<lfloor>dom b\<rfloor> \<Longrightarrow> \<D> null \<lfloor>dom b\<rfloor>
 10. \<And>Cs C Cs' Ds E a aa b. \<lbrakk>P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs' ; Ds = Cs @\<^sub>p Cs'; \<D> (Cast C (ref (a, Cs))) \<lfloor>dom b\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (ref (a, Ds)) \<lfloor>dom b\<rfloor>
A total of 50 subgoals...
[PROOF STEP]
case ListRed1
[PROOF STATE]
proof (state)
this:
P,E_ \<turnstile> \<langle>e_,(a___, b___)\<rangle> \<rightarrow> \<langle>e'_,(a_, b_)\<rangle>
\<D> e_ \<lfloor>dom b___\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom b_\<rfloor>
\<D>s (e_ # es_) \<lfloor>dom b___\<rfloor>

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

goal (1 subgoal):
 1. \<D>s (e'_ # es_) \<lfloor>dom b_\<rfloor>
[PROOF STEP]
by (auto elim!: Ds_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D>s (e'_ # es_) \<lfloor>dom b_\<rfloor>

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