[STATEMENT]
lemma red_lcl_sub:
  "\<lbrakk> extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>; fv e \<subseteq> W \<rbrakk>
  \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e, (hp s, (lcl s)|`W)\<rangle> -ta\<rightarrow> \<langle>e', (hp s', (lcl s')|`W)\<rangle>"

  and reds_lcl_sub:
  "\<lbrakk> extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle>; fvs es \<subseteq> W \<rbrakk>
  \<Longrightarrow> extTA,P,t \<turnstile> \<langle>es, (hp s, (lcl s)|`W)\<rangle> [-ta\<rightarrow>] \<langle>es', (hp s', (lcl s')|`W)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; fv e \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>) &&& (\<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; fvs es \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>es,(hp s, lcl s |` W)\<rangle> [-ta\<rightarrow>] \<langle>es',(hp s', lcl s' |` W)\<rangle>)
[PROOF STEP]
proof(induct arbitrary: W and W rule: red_reds.inducts)
[PROOF STATE]
proof (state)
goal (98 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 98 subgoals...
[PROOF STEP]
case (RedLAss V v h l W)
[PROOF STATE]
proof (state)
this:
fv (V:=Val v) \<subseteq> W

goal (98 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 98 subgoals...
[PROOF STEP]
have "extTA,P,t \<turnstile> \<langle>V:=Val v,(h, l |` W)\<rangle> -\<epsilon>\<rightarrow> \<langle>unit,(h, (l |`W)(V \<mapsto> v))\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>V:=Val v,(h, l |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(h, (l |` W)(V \<mapsto> v))\<rangle>
[PROOF STEP]
by(rule red_reds.RedLAss)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>V:=Val v,(h, l |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(h, (l |` W)(V \<mapsto> v))\<rangle>

goal (98 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 98 subgoals...
[PROOF STEP]
with RedLAss
[PROOF STATE]
proof (chain)
picking this:
fv (V:=Val v) \<subseteq> W
extTA,P,t \<turnstile> \<langle>V:=Val v,(h, l |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(h, (l |` W)(V \<mapsto> v))\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fv (V:=Val v) \<subseteq> W
extTA,P,t \<turnstile> \<langle>V:=Val v,(h, l |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(h, (l |` W)(V \<mapsto> v))\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>V:=Val v,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(hp (h, l(V \<mapsto> v)), lcl (h, l(V \<mapsto> v)) |` W)\<rangle>
[PROOF STEP]
by(simp del: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>V:=Val v,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>unit,(hp (h, l(V \<mapsto> v)), lcl (h, l(V \<mapsto> v)) |` W)\<rangle>

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

goal (97 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 97 subgoals...
[PROOF STEP]
have IH: "\<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` W)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` W)\<rangle>
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
fv e \<subseteq> ?W18 \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` ?W18)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` ?W18)\<rangle>

goal (97 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 97 subgoals...
[PROOF STEP]
from \<open>fv {V:T=vo; e} \<subseteq> W\<close>
[PROOF STATE]
proof (chain)
picking this:
fv {V:T=vo; e} \<subseteq> W
[PROOF STEP]
have fve: "fv e \<subseteq> insert V W"
[PROOF STATE]
proof (prove)
using this:
fv {V:T=vo; e} \<subseteq> W

goal (1 subgoal):
 1. fv e \<subseteq> insert V W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv e \<subseteq> insert V W

goal (97 subgoals):
 1. \<And>h' a h C l W. \<lbrakk>(h', a) \<in> allocate h (Class_type C); fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 2. \<And>h C l W. \<lbrakk>allocate h (Class_type C) = {}; fv (new C) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>new C,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 3. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (newA T\<lfloor>e\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(hp s', lcl s' |` W)\<rangle>
 4. \<And>i h' a h T l W. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(hp (h', l), lcl (h', l) |` W)\<rangle>
 5. \<And>i T s W. \<lbrakk>i <s 0; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(hp s, lcl s |` W)\<rangle>
 6. \<And>i h T l W. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; fv (newA T\<lfloor>Val (Intg i)\<rceil>) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>newA T\<lfloor>Val (Intg i)\<rceil>,(hp (h, l), lcl (h, l) |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(hp (h, l), lcl (h, l) |` W)\<rangle>
 7. \<And>e s ta e' s' C W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (Cast C e) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast C e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>Cast C e',(hp s', lcl s' |` W)\<rangle>
 8. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Val v,(hp s, lcl s |` W)\<rangle>
 9. \<And>s v U T W. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; fv (Cast T (Val v)) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Cast T (Val v),(hp s, lcl s |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt ClassCast),(hp s, lcl s |` W)\<rangle>
 10. \<And>e s ta e' s' T W. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; \<And>W. fv e \<subseteq> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp s', lcl s' |` W)\<rangle>; fv (e instanceof T) \<subseteq> W\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e instanceof T,(hp s, lcl s |` W)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(hp s', lcl s' |` W)\<rangle>
A total of 97 subgoals...
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
proof(cases "V \<in> W")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. V \<in> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
 2. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
V \<in> W

goal (2 subgoals):
 1. V \<in> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
 2. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with fve
[PROOF STATE]
proof (chain)
picking this:
fv e \<subseteq> insert V W
V \<in> W
[PROOF STEP]
have "fv e \<subseteq> W"
[PROOF STATE]
proof (prove)
using this:
fv e \<subseteq> insert V W
V \<in> W

goal (1 subgoal):
 1. fv e \<subseteq> W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv e \<subseteq> W

goal (2 subgoals):
 1. V \<in> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
 2. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
from True IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
V \<in> W
extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` W)\<rangle>
[PROOF STEP]
have "extTA,P,t \<turnstile> \<langle>e,(h, (x |` W )(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` W)\<rangle>"
[PROOF STATE]
proof (prove)
using this:
V \<in> W
extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` W)\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` W)\<rangle>
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` W)\<rangle>

goal (2 subgoals):
 1. V \<in> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
 2. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
V \<in> W
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` W)\<rangle>
[PROOF STEP]
have "extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W)(V := x V))\<rangle>"
[PROOF STATE]
proof (prove)
using this:
V \<in> W
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` W)\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W)(V := x V))\<rangle>
[PROOF STEP]
by -(drule red_reds.BlockRed[where T=T], simp)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W)(V := x V))\<rangle>

goal (2 subgoals):
 1. V \<in> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
 2. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with True
[PROOF STATE]
proof (chain)
picking this:
V \<in> W
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W)(V := x V))\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V \<in> W
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W)(V := x V))\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
by(simp del: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>

goal (1 subgoal):
 1. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
V \<notin> W

goal (1 subgoal):
 1. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with IH[OF fve]
[PROOF STATE]
proof (chain)
picking this:
extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` insert V W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` insert V W)\<rangle>
V \<notin> W
[PROOF STEP]
have "extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` insert V W)\<rangle>"
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e,(hp (h, x(V := vo)), lcl (h, x(V := vo)) |` insert V W)\<rangle> -ta\<rightarrow> \<langle>e',(hp (h', x'), lcl (h', x') |` insert V W)\<rangle>
V \<notin> W

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` insert V W)\<rangle>
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` insert V W)\<rangle>

goal (1 subgoal):
 1. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
V \<notin> W
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` insert V W)\<rangle>
[PROOF STEP]
have "extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', (x' |` W))\<rangle>"
[PROOF STATE]
proof (prove)
using this:
V \<notin> W
extTA,P,t \<turnstile> \<langle>e,(h, (x |` W)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x' |` insert V W)\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', x' |` W)\<rangle>
[PROOF STEP]
by -(drule red_reds.BlockRed[where T=T],simp)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', x' |` W)\<rangle>

goal (1 subgoal):
 1. V \<notin> W \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
V \<notin> W
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', x' |` W)\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V \<notin> W
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, x |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', x' |` W)\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>
[PROOF STEP]
by(simp del: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), lcl (h, x) |` W)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), lcl (h', x'(V := x V)) |` W)\<rangle>

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

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

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>try Throw a_ catch(C_ V_) e2_,(hp s_, lcl s_ |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a_,(hp s_, lcl s_ |` W)\<rangle>
[PROOF STEP]
by(auto intro: red_reds.RedTryFail)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>try Throw a_ catch(C_ V_) e2_,(hp s_, lcl s_ |` W)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a_,(hp s_, lcl s_ |` W)\<rangle>

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


[STATEMENT]
lemma red_notfree_unchanged: "\<lbrakk> extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>; V \<notin> fv e \<rbrakk> \<Longrightarrow> lcl s' V = lcl s V"
  and reds_notfree_unchanged: "\<lbrakk> extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle>; V \<notin> fvs es \<rbrakk> \<Longrightarrow> lcl s' V = lcl s V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; V \<notin> fv e\<rbrakk> \<Longrightarrow> lcl s' V = lcl s V) &&& (\<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; V \<notin> fvs es\<rbrakk> \<Longrightarrow> lcl s' V = lcl s V)
[PROOF STEP]
apply(induct rule: red_reds.inducts)
[PROOF STATE]
proof (prove)
goal (98 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); V \<notin> fv (new C)\<rbrakk> \<Longrightarrow> lcl (h', l) V = lcl (h, l) V
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; V \<notin> fv (new C)\<rbrakk> \<Longrightarrow> lcl (h, l) V = lcl (h, l) V
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; V \<notin> fv e \<Longrightarrow> lcl s' V = lcl s V; V \<notin> fv (newA T\<lfloor>e\<rceil>)\<rbrakk> \<Longrightarrow> lcl s' V = lcl s V
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); V \<notin> fv (newA T\<lfloor>Val (Intg i)\<rceil>)\<rbrakk> \<Longrightarrow> lcl (h', l) V = lcl (h, l) V
 5. \<And>i T s. \<lbrakk>i <s 0; V \<notin> fv (newA T\<lfloor>Val (Intg i)\<rceil>)\<rbrakk> \<Longrightarrow> lcl s V = lcl s V
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; V \<notin> fv (newA T\<lfloor>Val (Intg i)\<rceil>)\<rbrakk> \<Longrightarrow> lcl (h, l) V = lcl (h, l) V
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; V \<notin> fv e \<Longrightarrow> lcl s' V = lcl s V; V \<notin> fv (Cast C e)\<rbrakk> \<Longrightarrow> lcl s' V = lcl s V
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; V \<notin> fv (Cast T (Val v))\<rbrakk> \<Longrightarrow> lcl s V = lcl s V
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; V \<notin> fv (Cast T (Val v))\<rbrakk> \<Longrightarrow> lcl s V = lcl s V
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; V \<notin> fv e \<Longrightarrow> lcl s' V = lcl s V; V \<notin> fv (e instanceof T)\<rbrakk> \<Longrightarrow> lcl s' V = lcl s V
A total of 98 subgoals...
[PROOF STEP]
apply(fastforce)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_dom_lcl: "extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fv e"
  and reds_dom_lcl: "extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fvs es"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fv e) &&& (extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fvs es)
[PROOF STEP]
proof (induct rule:red_reds.inducts)
[PROOF STATE]
proof (state)
goal (98 subgoals):
 1. \<And>h' a h C l. (h', a) \<in> allocate h (Class_type C) \<Longrightarrow> dom (lcl (h', l)) \<subseteq> dom (lcl (h, l)) \<union> fv (new C)
 2. \<And>h C l. allocate h (Class_type C) = {} \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h, l)) \<union> fv (new C)
 3. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s') \<subseteq> dom (lcl s) \<union> fv e\<rbrakk> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fv (newA T\<lfloor>e\<rceil>)
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i)))\<rbrakk> \<Longrightarrow> dom (lcl (h', l)) \<subseteq> dom (lcl (h, l)) \<union> fv (newA T\<lfloor>Val (Intg i)\<rceil>)
 5. \<And>i T s. i <s 0 \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s) \<union> fv (newA T\<lfloor>Val (Intg i)\<rceil>)
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}\<rbrakk> \<Longrightarrow> dom (lcl (h, l)) \<subseteq> dom (lcl (h, l)) \<union> fv (newA T\<lfloor>Val (Intg i)\<rceil>)
 7. \<And>e s ta e' s' C. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s') \<subseteq> dom (lcl s) \<union> fv e\<rbrakk> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fv (Cast C e)
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s) \<union> fv (Cast T (Val v))
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> dom (lcl s) \<subseteq> dom (lcl s) \<union> fv (Cast T (Val v))
 10. \<And>e s ta e' s' T. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; dom (lcl s') \<subseteq> dom (lcl s) \<union> fv e\<rbrakk> \<Longrightarrow> dom (lcl s') \<subseteq> dom (lcl s) \<union> fv (e instanceof T)
A total of 98 subgoals...
[PROOF STEP]
case (BlockRed e h x V vo ta e' h' x' T)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>e,(h, x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x')\<rangle>
dom (lcl (h', x')) \<subseteq> dom (lcl (h, x(V := vo))) \<union> fv e

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

goal (1 subgoal):
 1. dom (lcl (h', x'(V := x V))) \<subseteq> dom (lcl (h, x)) \<union> fv {V:T=vo; e}
[PROOF STEP]
by(clarsimp)(fastforce split:if_split_asm)
[PROOF STATE]
proof (state)
this:
dom (lcl (h', x'(V := x V))) \<subseteq> dom (lcl (h, x)) \<union> fv {V:T=vo; e}

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


[STATEMENT]
lemma red_Suspend_is_call:
  "\<lbrakk> convert_extTA extNTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<rbrakk>
  \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait:Ts\<rightarrow>Tr = Native in D"
  and reds_Suspend_is_calls:
  "\<lbrakk> convert_extTA extNTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<rbrakk>
  \<Longrightarrow> \<exists>a vs hT Ts Tr D. calls es' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait:Ts\<rightarrow>Tr = Native in D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D) &&& (\<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. calls es' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D)
[PROOF STEP]
proof(induct 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); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 3. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (newA T\<lfloor>e'\<rceil>) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 5. \<And>i T s. \<lbrakk>i <s 0; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt NegativeArraySize)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 7. \<And>e s ta e' s' C. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Cast C e') = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Val v) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt ClassCast)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 10. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (e' instanceof T) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
A total of 98 subgoals...
[PROOF STEP]
case RedCallExternal
[PROOF STATE]
proof (state)
this:
typeof_addr (hp s_) a_ = \<lfloor>hU_\<rfloor>
P \<turnstile> class_type_of hU_ sees M_: Ts_\<rightarrow>T_ = Native in D_
P,t \<turnstile> \<langle>a_\<bullet>M_(vs_),hp s_\<rangle> -ta_\<rightarrow>ext \<langle>va_,h'_\<rangle>
ta'_ = convert_extTA extNTA ta_
e'_ = extRet2J (addr a_\<bullet>M_(map Val vs_)) va_
s'_ = (h'_, lcl s_)
Suspend w \<in> set \<lbrace>ta'_\<rbrace>\<^bsub>w\<^esub>

goal (98 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 3. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (newA T\<lfloor>e'\<rceil>) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 5. \<And>i T s. \<lbrakk>i <s 0; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt NegativeArraySize)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 7. \<And>e s ta e' s' C. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Cast C e') = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Val v) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt ClassCast)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 10. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (e' instanceof T) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
A total of 98 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_ = Native in D_
P,t \<turnstile> \<langle>a_\<bullet>M_(vs_),hp s_\<rangle> -ta_\<rightarrow>ext \<langle>va_,h'_\<rangle>
ta'_ = convert_extTA extNTA ta_
e'_ = extRet2J (addr a_\<bullet>M_(map Val vs_)) va_
s'_ = (h'_, lcl s_)
Suspend w \<in> set \<lbrace>ta'_\<rbrace>\<^bsub>w\<^esub>

goal (1 subgoal):
 1. \<exists>a vs hT Ts Tr D. call e'_ = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s_) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr (hp s_) a_ = \<lfloor>hU_\<rfloor>; P \<turnstile> class_type_of hU_ sees M_: Ts_\<rightarrow>T_ = Native in D_; P,t \<turnstile> \<langle>a_\<bullet>M_(vs_),hp s_\<rangle> -ta_\<rightarrow>ext \<langle>va_,h'_\<rangle>; ta'_ = convert_extTA extNTA ta_; e'_ = extRet2J (addr a_\<bullet>M_(map Val vs_)) va_; s'_ = (h'_, lcl s_); Suspend w \<in> set \<lbrace>ta_\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>vsa. call (extRet2J (addr a_\<bullet>M_(map Val vs_)) va_) = \<lfloor>(aa, wait, vsa)\<rfloor>) \<and> (\<exists>hT. typeof_addr (hp s_) aa = \<lfloor>hT\<rfloor> \<and> (\<exists>Ts Tr. Ex (Method_native P (class_type_of hT) wait Ts Tr)))
[PROOF STEP]
apply(frule red_external_Suspend_StaySame, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr (hp s_) a_ = \<lfloor>hU_\<rfloor>; P \<turnstile> class_type_of hU_ sees M_: Ts_\<rightarrow>T_ = Native in D_; P,t \<turnstile> \<langle>a_\<bullet>M_(vs_),hp s_\<rangle> -ta_\<rightarrow>ext \<langle>va_,h'_\<rangle>; ta'_ = convert_extTA extNTA ta_; e'_ = extRet2J (addr a_\<bullet>M_(map Val vs_)) va_; s'_ = (h'_, lcl s_); Suspend w \<in> set \<lbrace>ta_\<rbrace>\<^bsub>w\<^esub>; va_ = RetStaySame\<rbrakk> \<Longrightarrow> \<exists>aa. (\<exists>vsa. call (extRet2J (addr a_\<bullet>M_(map Val vs_)) va_) = \<lfloor>(aa, wait, vsa)\<rfloor>) \<and> (\<exists>hT. typeof_addr (hp s_) aa = \<lfloor>hT\<rfloor> \<and> (\<exists>Ts Tr. Ex (Method_native P (class_type_of hT) wait Ts Tr)))
[PROOF STEP]
apply(drule red_external_Suspend_waitD, fastforce+)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<exists>a vs hT Ts Tr D. call e'_ = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s_) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D

goal (97 subgoals):
 1. \<And>h' a h C l. \<lbrakk>(h', a) \<in> allocate h (Class_type C); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 2. \<And>h C l. \<lbrakk>allocate h (Class_type C) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 3. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (newA T\<lfloor>e'\<rceil>) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 4. \<And>i h' a h T l. \<lbrakk>0 \<le>s i; (h', a) \<in> allocate h (Array_type T (nat (sint i))); Suspend w \<in> set \<lbrace>\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>aa vs hT Ts Tr D. call (addr a) = \<lfloor>(aa, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) aa = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 5. \<And>i T s. \<lbrakk>i <s 0; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt NegativeArraySize)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 6. \<And>i h T l. \<lbrakk>0 \<le>s i; allocate h (Array_type T (nat (sint i))) = {}; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt OutOfMemory)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp (h, l)) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 7. \<And>e s ta e' s' C. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Cast C e') = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 8. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Val v) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 9. \<And>s v U T. \<lbrakk>typeof\<^bsub>hp s\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T; Suspend w \<in> set \<lbrace>\<lbrace>\<rbrace>\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (Throw (addr_of_sys_xcpt ClassCast)) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
 10. \<And>e s ta e' s' T. \<lbrakk>convert_extTA extNTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call e' = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D; Suspend w \<in> set \<lbrace>ta\<rbrace>\<^bsub>w\<^esub>\<rbrakk> \<Longrightarrow> \<exists>a vs hT Ts Tr D. call (e' instanceof T) = \<lfloor>(a, wait, vs)\<rfloor> \<and> typeof_addr (hp s) a = \<lfloor>hT\<rfloor> \<and> P \<turnstile> class_type_of hT sees wait: Ts\<rightarrow>Tr = Native in D
A total of 97 subgoals...
[PROOF STEP]
qed auto


[STATEMENT]
lemma red_hext_incr: "extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s'"
  and reds_hext_incr: "extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s') &&& (extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle> \<Longrightarrow> hp s \<unlhd> hp s')
[PROOF STEP]
by(induct rule:red_reds.inducts)(auto intro: hext_heap_ops red_external_hext)


[STATEMENT]
lemma red_preserves_tconf: "\<lbrakk> extTA,P,t \<turnstile> \<langle>e, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle>; P,hp s \<turnstile> t \<surd>t \<rbrakk> \<Longrightarrow> P,hp s' \<turnstile> t \<surd>t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle>; P,hp s \<turnstile> t \<surd>t\<rbrakk> \<Longrightarrow> P,hp s' \<turnstile> t \<surd>t
[PROOF STEP]
by(drule red_hext_incr)(rule tconf_hext_mono)


[STATEMENT]
lemma RedCall_code:
  "\<lbrakk> is_vals es; 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;
    size es = size pns; size Ts = size pns \<rbrakk>
  \<Longrightarrow> extTA,P,t \<turnstile> \<langle>(addr a)\<bullet>M(es), s\<rangle> -\<epsilon>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # map the_Val es) body, s\<rangle>"

  and RedCallExternal_code:
  "\<lbrakk> is_vals es; typeof_addr (hp s) a = \<lfloor>hU\<rfloor>; P \<turnstile> class_type_of hU sees M:Ts\<rightarrow>T = Native in D;
     P,t \<turnstile> \<langle>a\<bullet>M(map the_Val es), hp s\<rangle> -ta\<rightarrow>ext \<langle>va, h'\<rangle> \<rbrakk>
  \<Longrightarrow> extTA,P,t \<turnstile> \<langle>(addr a)\<bullet>M(es), s\<rangle> -extTA ta\<rightarrow> \<langle>extRet2J ((addr a)\<bullet>M(es)) va, (h', lcl s)\<rangle>"

  and RedCallNull_code:
  "is_vals es \<Longrightarrow> extTA,P,t \<turnstile> \<langle>null\<bullet>M(es), s\<rangle> -\<epsilon>\<rightarrow> \<langle>THROW NullPointer, s\<rangle>"

  and CallThrowParams_code:
  "is_Throws es \<Longrightarrow> extTA,P,t \<turnstile> \<langle>(Val v)\<bullet>M(es), s\<rangle> -\<epsilon>\<rightarrow> \<langle>hd (dropWhile is_val es), s\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>is_vals es; 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 es = length pns; length Ts = length pns\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>addr a\<bullet>M(es),s\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>blocks (this # pns) (Class D # Ts) (Addr a # map the_Val es) body,s\<rangle>) &&& (\<lbrakk>is_vals es; typeof_addr (hp s) a = \<lfloor>hU\<rfloor>; P \<turnstile> class_type_of hU sees M: Ts\<rightarrow>T = Native in D; P,t \<turnstile> \<langle>a\<bullet>M(map the_Val es),hp s\<rangle> -ta\<rightarrow>ext \<langle>va,h'\<rangle>\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>addr a\<bullet>M(es),s\<rangle> -extTA ta\<rightarrow> \<langle>extRet2J (addr a\<bullet>M(es)) va,(h', lcl s)\<rangle>)) &&& (is_vals es \<Longrightarrow> extTA,P,t \<turnstile> \<langle>null\<bullet>M(es),s\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NullPointer),s\<rangle>) &&& (is_Throws es \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Val v\<bullet>M(es),s\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>hd (dropWhile is_val es),s\<rangle>)
[PROOF STEP]
apply(auto simp add: is_vals_conv is_Throws_conv o_def intro: RedCall RedCallExternal RedCallNull simp del: blocks.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>vs a es'. es = map Val vs @ Throw a # es' \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Val v\<bullet>M(map Val vs @ Throw a # es'),s\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>hd (dropWhile is_val (map Val vs @ Throw a # es')),s\<rangle>
[PROOF STEP]
apply(subst dropWhile_append2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>vs a es' x. \<lbrakk>es = map Val vs @ Throw a # es'; x \<in> set (map Val vs)\<rbrakk> \<Longrightarrow> is_val x
 2. \<And>vs a es'. es = map Val vs @ Throw a # es' \<Longrightarrow> extTA,P,t \<turnstile> \<langle>Val v\<bullet>M(map Val vs @ Throw a # es'),s\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>hd (dropWhile is_val (Throw a # es')),s\<rangle>
[PROOF STEP]
apply(auto intro: CallThrowParams)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done