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

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

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

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

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

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

goal (2 subgoals):
 1. vo = None \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
 2. \<And>a. vo = \<lfloor>a\<rfloor> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
from IH[of "l0(V := vo)"]
[PROOF STATE]
proof (chain)
picking this:
extTA,P,t \<turnstile> \<langle>e,(h, l0(V := vo) ++ x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e,(h, l0(V := vo) ++ x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle>

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
apply(simp del: fun_upd_apply add: lrew)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>e,(h, (l0 ++ x)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', l0 ++ x'(V := x V))\<rangle>
[PROOF STEP]
apply(drule red_reds.BlockRed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:?T1=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:?T1=(l0(V := vo) ++ x') V; e'},(h', (l0(V := vo) ++ x')(V := (l0 ++ x) V))\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(h', l0 ++ x'(V := x V))\<rangle>
[PROOF STEP]
by(simp only: lrew1 None lrew2)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>

goal (1 subgoal):
 1. \<And>a. vo = \<lfloor>a\<rfloor> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. vo = \<lfloor>a\<rfloor> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
case (Some v)
[PROOF STATE]
proof (state)
this:
vo = \<lfloor>v\<rfloor>

goal (1 subgoal):
 1. \<And>a. vo = \<lfloor>a\<rfloor> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
with \<open>extTA,P,t \<turnstile> \<langle>e,(h, x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x')\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
extTA,P,t \<turnstile> \<langle>e,(h, x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x')\<rangle>
vo = \<lfloor>v\<rfloor>
[PROOF STEP]
have "x' V \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e,(h, x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', x')\<rangle>
vo = \<lfloor>v\<rfloor>

goal (1 subgoal):
 1. x' V \<noteq> None
[PROOF STEP]
by -(drule red_lcl_incr, auto split: if_split_asm)
[PROOF STATE]
proof (state)
this:
x' V \<noteq> None

goal (1 subgoal):
 1. \<And>a. vo = \<lfloor>a\<rfloor> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
with IH[of "l0(V := vo)"]
[PROOF STATE]
proof (chain)
picking this:
extTA,P,t \<turnstile> \<langle>e,(h, l0(V := vo) ++ x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle>
x' V \<noteq> None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
extTA,P,t \<turnstile> \<langle>e,(h, l0(V := vo) ++ x(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle>
x' V \<noteq> None

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>
[PROOF STEP]
apply(clarsimp simp del: fun_upd_apply simp add: lrew)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>extTA,P,t \<turnstile> \<langle>e,(h, (l0 ++ x)(V := vo))\<rangle> -ta\<rightarrow> \<langle>e',(h', l0(V := vo) ++ x')\<rangle>; x' V = \<lfloor>y\<rfloor>\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:T=\<lfloor>y\<rfloor>; e'},(h', l0 ++ x'(V := x V))\<rangle>
[PROOF STEP]
apply(drule red_reds.BlockRed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>x' V = \<lfloor>y\<rfloor>; extTA,P,t \<turnstile> \<langle>{V:?T3 y=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:?T3 y=(l0(V := vo) ++ x') V; e'},(h', (l0(V := vo) ++ x')(V := (l0 ++ x) V))\<rangle>\<rbrakk> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(h, l0 ++ x)\<rangle> -ta\<rightarrow> \<langle>{V:T=\<lfloor>y\<rfloor>; e'},(h', l0 ++ x'(V := x V))\<rangle>
[PROOF STEP]
by(simp add: lrew1 Some del: fun_upd_apply)
[PROOF STATE]
proof (state)
this:
extTA,P,t \<turnstile> \<langle>{V:T=vo; e},(hp (h, x), l0 ++ lcl (h, x))\<rangle> -ta\<rightarrow> \<langle>{V:T=x' V; e'},(hp (h', x'(V := x V)), l0 ++ lcl (h', x'(V := x V)))\<rangle>

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

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

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

goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>try Throw a_ catch(C_ V_) e2_,(hp s_, l0 ++ lcl s_)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a_,(hp s_, l0 ++ lcl s_)\<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_, l0 ++ lcl s_)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a_,(hp s_, l0 ++ lcl s_)\<rangle>

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


[STATEMENT]
lemma red_lcl_add: "extTA,P,t \<turnstile> \<langle>e, (h, l)\<rangle> -ta\<rightarrow> \<langle>e', (h', l')\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e, (h, l0 ++ l)\<rangle> -ta\<rightarrow> \<langle>e', (h', l0 ++ l')\<rangle>"
  and reds_lcl_add: "extTA,P,t \<turnstile> \<langle>es, (h, l)\<rangle> [-ta\<rightarrow>] \<langle>es', (h', l')\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>es, (h, l0 ++ l)\<rangle> [-ta\<rightarrow>] \<langle>es', (h', l0 ++ l')\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (extTA,P,t \<turnstile> \<langle>e,(h, l)\<rangle> -ta\<rightarrow> \<langle>e',(h', l')\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>e,(h, l0 ++ l)\<rangle> -ta\<rightarrow> \<langle>e',(h', l0 ++ l')\<rangle>) &&& (extTA,P,t \<turnstile> \<langle>es,(h, l)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', l')\<rangle> \<Longrightarrow> extTA,P,t \<turnstile> \<langle>es,(h, l0 ++ l)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', l0 ++ l')\<rangle>)
[PROOF STEP]
by(auto dest:red_lcl_add_aux reds_lcl_add_aux)


[STATEMENT]
lemma reds_no_val [dest]:
  "\<lbrakk> extTA,P,t \<turnstile> \<langle>es, s\<rangle> [-ta\<rightarrow>] \<langle>es', s'\<rangle>; is_vals es \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals es\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(induct es arbitrary: s ta es' s')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s ta es' s'. \<lbrakk>extTA,P,t \<turnstile> \<langle>[],s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals []\<rbrakk> \<Longrightarrow> False
 2. \<And>a es s ta es' s'. \<lbrakk>\<And>s ta es' s'. \<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals es\<rbrakk> \<Longrightarrow> False; extTA,P,t \<turnstile> \<langle>a # es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals (a # es)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(blast elim: reds.cases)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a es s ta es' s'. \<lbrakk>\<And>s ta es' s'. \<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals es\<rbrakk> \<Longrightarrow> False; extTA,P,t \<turnstile> \<langle>a # es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals (a # es)\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(erule reds.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a es s ta es' s' e sa taa e' s'a esa. \<lbrakk>\<And>s ta es' s'. \<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals es\<rbrakk> \<Longrightarrow> False; is_vals (a # es); a # es = e # esa; s = sa; ta = taa; es' = e' # esa; s' = s'a; extTA,P,t \<turnstile> \<langle>e,sa\<rangle> -taa\<rightarrow> \<langle>e',s'a\<rangle>\<rbrakk> \<Longrightarrow> False
 2. \<And>a es s ta es' s' esa sa taa es'a s'a v. \<lbrakk>\<And>s ta es' s'. \<lbrakk>extTA,P,t \<turnstile> \<langle>es,s\<rangle> [-ta\<rightarrow>] \<langle>es',s'\<rangle>; is_vals es\<rbrakk> \<Longrightarrow> False; is_vals (a # es); a # es = Val v # esa; s = sa; ta = taa; es' = Val v # es'a; s' = s'a; extTA,P,t \<turnstile> \<langle>esa,sa\<rangle> [-taa\<rightarrow>] \<langle>es'a,s'a\<rangle>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(auto, blast)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma red_no_Throw [dest!]:
  "extTA,P,t \<turnstile> \<langle>Throw a, s\<rangle> -ta\<rightarrow> \<langle>e', s'\<rangle> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extTA,P,t \<turnstile> \<langle>Throw a,s\<rangle> -ta\<rightarrow> \<langle>e',s'\<rangle> \<Longrightarrow> False
[PROOF STEP]
by(auto elim!: red_cases)