[STATEMENT]
lemma assumes wf: "wf_J_prog P"
  shows red_preserves_defass: "extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>"
  and reds_preserves_defass: "extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> \<D>s es \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D>s es' \<lfloor>dom (lcl s')\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>) &&& (\<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; \<D>s es \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D>s es' \<lfloor>dom (lcl s')\<rfloor>)
[PROOF STEP]
proof (induction rule:red_reds.inducts)
[PROOF STATE]
proof (state)
goal (98 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 98 subgoals...
[PROOF STEP]
case BinOpRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_ \<guillemotleft>bop_\<guillemotright> e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (98 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 98 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_ \<guillemotleft>bop_\<guillemotright> e2_) \<lfloor>dom (lcl s_)\<rfloor>

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

goal (97 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 97 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (97 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 97 subgoals...
[PROOF STEP]
case AAccRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>a_,s_\<rangle> -ta_\<rightarrow> \<langle>a'_,s'_\<rangle>
\<D> a_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> a'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (a_\<lfloor>i_\<rceil>) \<lfloor>dom (lcl s_)\<rfloor>

goal (97 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 97 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>a_,s_\<rangle> -ta_\<rightarrow> \<langle>a'_,s'_\<rangle>
\<D> a_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> a'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (a_\<lfloor>i_\<rceil>) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (a'_\<lfloor>i_\<rceil>) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (a'_\<lfloor>i_\<rceil>) \<lfloor>dom (lcl s'_)\<rfloor>

goal (96 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 96 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (96 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 96 subgoals...
[PROOF STEP]
case AAssRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>a_,s_\<rangle> -ta_\<rightarrow> \<langle>a'_,s'_\<rangle>
\<D> a_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> a'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (a_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (96 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 96 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>a_,s_\<rangle> -ta_\<rightarrow> \<langle>a'_,s'_\<rangle>
\<D> a_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> a'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (a_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (a'_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by(auto intro: red_lA_incr sqUn_lem D_mono)
[PROOF STATE]
proof (state)
this:
\<D> (a'_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s'_)\<rfloor>

goal (95 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 95 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (95 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 95 subgoals...
[PROOF STEP]
case AAssRed2
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>i_,s_\<rangle> -ta_\<rightarrow> \<langle>i'_,s'_\<rangle>
\<D> i_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> i'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val a_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (95 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 95 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>i_,s_\<rangle> -ta_\<rightarrow> \<langle>i'_,s'_\<rangle>
\<D> i_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> i'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val a_\<lfloor>i_\<rceil> := e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (Val a_\<lfloor>i'_\<rceil> := e_) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (Val a_\<lfloor>i'_\<rceil> := e_) \<lfloor>dom (lcl s'_)\<rfloor>

goal (94 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 94 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (94 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 94 subgoals...
[PROOF STEP]
case FAssRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>F_{D_} := e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (94 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 94 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>F_{D_} := e2_) \<lfloor>dom (lcl s_)\<rfloor>

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

goal (93 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 93 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (93 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 93 subgoals...
[PROOF STEP]
case CASRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>compareAndSwap(D_\<bullet>F_, e2_, e3_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (93 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 93 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>compareAndSwap(D_\<bullet>F_, e2_, e3_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (e'_\<bullet>compareAndSwap(D_\<bullet>F_, e2_, e3_)) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by(auto intro: red_lA_incr sqUn_lem D_mono)
[PROOF STATE]
proof (state)
this:
\<D> (e'_\<bullet>compareAndSwap(D_\<bullet>F_, e2_, e3_)) \<lfloor>dom (lcl s'_)\<rfloor>

goal (92 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 92 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (92 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 92 subgoals...
[PROOF STEP]
case CASRed2
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val v_\<bullet>compareAndSwap(D_\<bullet>F_, e_, e3_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (92 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 92 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val v_\<bullet>compareAndSwap(D_\<bullet>F_, e_, e3_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (Val v_\<bullet>compareAndSwap(D_\<bullet>F_, e'_, e3_)) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (Val v_\<bullet>compareAndSwap(D_\<bullet>F_, e'_, e3_)) \<lfloor>dom (lcl s'_)\<rfloor>

goal (91 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 91 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (91 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 91 subgoals...
[PROOF STEP]
case CallObj
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>M_(es_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (91 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 91 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_\<bullet>M_(es_)) \<lfloor>dom (lcl s_)\<rfloor>

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

goal (90 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 90 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (90 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 90 subgoals...
[PROOF STEP]
case CallParams
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>es_,s_\<rangle> [-ta_\<rightarrow>] \<langle>es'_,s'_\<rangle>
\<D>s es_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D>s es'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val v_\<bullet>M_(es_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (90 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 90 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>es_,s_\<rangle> [-ta_\<rightarrow>] \<langle>es'_,s'_\<rangle>
\<D>s es_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D>s es'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (Val v_\<bullet>M_(es_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (Val v_\<bullet>M_(es'_)) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by(auto elim!: Ds_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (Val v_\<bullet>M_(es'_)) \<lfloor>dom (lcl s'_)\<rfloor>

goal (89 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 89 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (89 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 89 subgoals...
[PROOF STEP]
case RedCall
[PROOF STATE]
proof (state)
this:
typeof_addr (hp s_) a_ = \<lfloor>hU_\<rfloor>
P \<turnstile> class_type_of hU_ sees M_: Ts_\<rightarrow>T_ = \<lfloor>(pns_, body_)\<rfloor> in D_
length vs_ = length pns_
length Ts_ = length pns_
\<D> (addr a_\<bullet>M_(map Val vs_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (89 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 89 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
typeof_addr (hp s_) a_ = \<lfloor>hU_\<rfloor>
P \<turnstile> class_type_of hU_ sees M_: Ts_\<rightarrow>T_ = \<lfloor>(pns_, body_)\<rfloor> in D_
length vs_ = length pns_
length Ts_ = length pns_
\<D> (addr a_\<bullet>M_(map Val vs_)) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (blocks (this # pns_) (Class D_ # Ts_) (Addr a_ # vs_) body_) \<lfloor>dom (lcl s_)\<rfloor>
[PROOF STEP]
by(auto dest!:sees_wf_mdecl[OF wf] simp:wf_mdecl_def elim!:D_mono')
[PROOF STATE]
proof (state)
this:
\<D> (blocks (this # pns_) (Class D_ # Ts_) (Addr a_ # vs_) body_) \<lfloor>dom (lcl s_)\<rfloor>

goal (88 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 88 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (88 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 88 subgoals...
[PROOF STEP]
case BlockRed
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,(h_, l_(V_ := vo_))\<rangle> -ta_\<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (lcl (h_, l_(V_ := vo_)))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl (h'_, l'_))\<rfloor>
\<D> {V_:T_=vo_; e_} \<lfloor>dom (lcl (h_, l_))\<rfloor>

goal (88 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 88 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,(h_, l_(V_ := vo_))\<rangle> -ta_\<rightarrow> \<langle>e'_,(h'_, l'_)\<rangle>
\<D> e_ \<lfloor>dom (lcl (h_, l_(V_ := vo_)))\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl (h'_, l'_))\<rfloor>
\<D> {V_:T_=vo_; e_} \<lfloor>dom (lcl (h_, l_))\<rfloor>

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

goal (87 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 87 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (87 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 87 subgoals...
[PROOF STEP]
case SynchronizedRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>o'_,s_\<rangle> -ta_\<rightarrow> \<langle>o''_,s'_\<rangle>
\<D> o'_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> o''_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (sync(o'_) e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (87 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 87 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>o'_,s_\<rangle> -ta_\<rightarrow> \<langle>o''_,s'_\<rangle>
\<D> o'_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> o''_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (sync(o'_) e_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (sync(o''_) e_) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by(auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (sync(o''_) e_) \<lfloor>dom (lcl s'_)\<rfloor>

goal (86 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 86 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (86 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 86 subgoals...
[PROOF STEP]
case SeqRed
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_;; e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (86 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 86 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (e_;; e2_) \<lfloor>dom (lcl s_)\<rfloor>

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

goal (85 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 85 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (85 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 85 subgoals...
[PROOF STEP]
case CondRed
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>b_,s_\<rangle> -ta_\<rightarrow> \<langle>b'_,s'_\<rangle>
\<D> b_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> b'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (if (b_) e1_ else e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (85 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 85 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>b_,s_\<rangle> -ta_\<rightarrow> \<langle>b'_,s'_\<rangle>
\<D> b_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> b'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (if (b_) e1_ else e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (if (b'_) e1_ else e2_) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by (auto elim!: D_mono[OF red_lA_incr])
[PROOF STATE]
proof (state)
this:
\<D> (if (b'_) e1_ else e2_) \<lfloor>dom (lcl s'_)\<rfloor>

goal (84 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 84 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (84 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 84 subgoals...
[PROOF STEP]
case TryRed
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (try e_ catch(C_ V_) e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (84 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 84 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D> (try e_ catch(C_ V_) e2_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (try e'_ catch(C_ V_) e2_) \<lfloor>dom (lcl s'_)\<rfloor>
[PROOF STEP]
by (fastforce dest:red_lcl_incr intro:D_mono' simp:hyperset_defs)
[PROOF STATE]
proof (state)
this:
\<D> (try e'_ catch(C_ V_) e2_) \<lfloor>dom (lcl s'_)\<rfloor>

goal (83 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 83 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (83 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 83 subgoals...
[PROOF STEP]
case RedWhile
[PROOF STATE]
proof (state)
this:
\<D> (while (b_) c_) \<lfloor>dom (lcl s_)\<rfloor>

goal (83 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 83 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<D> (while (b_) c_) \<lfloor>dom (lcl s_)\<rfloor>

goal (1 subgoal):
 1. \<D> (if (b_) (c_;; while (b_) c_) else unit) \<lfloor>dom (lcl s_)\<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 (lcl s_)\<rfloor>

goal (82 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 82 subgoals...
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (82 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 82 subgoals...
[PROOF STEP]
case ListRed1
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D>s (e_ # es_) \<lfloor>dom (lcl s_)\<rfloor>

goal (82 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 82 subgoals...
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e_,s_\<rangle> -ta_\<rightarrow> \<langle>e'_,s'_\<rangle>
\<D> e_ \<lfloor>dom (lcl s_)\<rfloor> \<Longrightarrow> \<D> e'_ \<lfloor>dom (lcl s'_)\<rfloor>
\<D>s (e_ # es_) \<lfloor>dom (lcl s_)\<rfloor>

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

goal (81 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; \<D> (new C) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (newA T\<lfloor>e\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (newA T\<lfloor>e'\<rceil>) \<lfloor>dom (lcl s')\<rfloor>
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (addr a) \<lfloor>dom (lcl (h', l))\<rfloor>
 5. \<And>i T s. \<lbrakk>i <s 0; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt NegativeArraySize)) \<lfloor>dom (lcl s)\<rfloor>
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; \<D> (newA T\<lfloor>Val (Intg i)\<rceil>) \<lfloor>dom (lcl (h, l))\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt OutOfMemory)) \<lfloor>dom (lcl (h, l))\<rfloor>
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (Cast C e) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Cast C e') \<lfloor>dom (lcl s')\<rfloor>
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Val v) \<lfloor>dom (lcl s)\<rfloor>
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; \<D> (Cast T (Val v)) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (Throw (addr_of_sys_xcpt ClassCast)) \<lfloor>dom (lcl s)\<rfloor>
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<D> e \<lfloor>dom (lcl s)\<rfloor> \<Longrightarrow> \<D> e' \<lfloor>dom (lcl s')\<rfloor>; \<D> (e instanceof T) \<lfloor>dom (lcl s)\<rfloor>\<rbrakk> \<Longrightarrow> \<D> (e' instanceof T) \<lfloor>dom (lcl s')\<rfloor>
A total of 81 subgoals...
[PROOF STEP]
qed (auto simp:hyperset_defs)