[STATEMENT]
lemma sim_move10_Block:
  "sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'
  \<Longrightarrow> sim_move10 P t ta1 ({V:T=None; e1}) ({V:T=None; e1'}) ({V':T=vo; e}) h xs ta ({V':T=xs' V'; e'}) h' (xs'(V' := xs V'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
assume "sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'"
[PROOF STATE]
proof (state)
this:
sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
fix e'' xs''
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
assume "extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>"
[PROOF STATE]
proof (state)
this:
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
hence "extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs''(V' := xs V', V' := xs'' V'))\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>"
[PROOF STATE]
proof (prove)
using this:
extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>

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

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
from BlockRed[OF this, of T]
[PROOF STATE]
proof (chain)
picking this:
extTA2J0 P,P,t \<turnstile> \<langle>{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := (xs''(V' := xs V')) V'))\<rangle>
[PROOF STEP]
have "extTA2J0 P,P,t \<turnstile> \<langle>{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>"
[PROOF STATE]
proof (prove)
using this:
extTA2J0 P,P,t \<turnstile> \<langle>{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := (xs''(V' := xs V')) V'))\<rangle>

goal (1 subgoal):
 1. extTA2J0 P,P,t \<turnstile> \<langle>{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
extTA2J0 P,P,t \<turnstile> \<langle>{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
extTA2J0 P,P,t \<turnstile> \<langle>?e''33,(h, ?xs''33)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>{V':T=?xs''33 V'; ?e''33},(h, ?xs''33(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>

goal (1 subgoal):
 1. sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs' \<Longrightarrow> sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'
extTA2J0 P,P,t \<turnstile> \<langle>?e''33,(h, ?xs''33)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>{V':T=?xs''33 V'; ?e''33},(h, ?xs''33(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'
extTA2J0 P,P,t \<turnstile> \<langle>?e''33,(h, ?xs''33)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>{V':T=?xs''33 V'; ?e''33},(h, ?xs''33(V' := xs V'))\<rangle> -ta\<rightarrow> \<langle>{V':T=xs' V'; e'},(h', xs'(V' := xs V'))\<rangle>

goal (1 subgoal):
 1. sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))
[PROOF STEP]
by(fastforce simp add: sim_move10_def final_iff split: if_split_asm)
[PROOF STATE]
proof (state)
this:
sim_move10 P t ta1 {V:T=None; e1} {V:T=None; e1'} {V':T=vo; e} h xs ta {V':T=xs' V'; e'} h' (xs'(V' := xs V'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sim_move10_reds:
  "\<lbrakk> (h', a) \<in> allocate h (Class_type C); ta1 = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>; ta = \<lbrace>NewHeapElem a (Class_type C)\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (new C) e1' (new C) h xs ta (addr a) h' xs"
  "allocate h (Class_type C) = {} \<Longrightarrow> sim_move10 P t \<epsilon> (new C) e1' (new C) h xs \<epsilon> (THROW OutOfMemory) h xs"
  "\<lbrakk> (h', a) \<in> allocate h (Array_type T (nat (sint i))); 0 <=s i;
     ta1 = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>; ta = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs ta (addr a) h' xs"
  "i <s 0 \<Longrightarrow> sim_move10 P t \<epsilon> (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs \<epsilon> (THROW NegativeArraySize) h xs"
  "\<lbrakk> allocate h (Array_type T (nat (sint i))) = {}; 0 <=s i \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs \<epsilon> (THROW OutOfMemory) h xs"
  "\<lbrakk> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (Cast T (Val v)) e1' (Cast T (Val v)) h xs \<epsilon> (Val v) h xs"
  "\<lbrakk> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (Cast T (Val v)) e1' (Cast T (Val v)) h xs \<epsilon> (THROW ClassCast) h xs"
  "\<lbrakk> typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; b \<longleftrightarrow> v \<noteq> Null \<and> P \<turnstile> U \<le> T \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> ((Val v) instanceof T) e1' ((Val v) instanceof T) h xs \<epsilon> (Val (Bool b)) h xs"
  "binop bop v1 v2 = Some (Inl v) \<Longrightarrow> sim_move10 P t \<epsilon> ((Val v1) \<guillemotleft>bop\<guillemotright> (Val v2)) e1' (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<epsilon> (Val v) h xs"
  "binop bop v1 v2 = Some (Inr a) \<Longrightarrow> sim_move10 P t \<epsilon> ((Val v1) \<guillemotleft>bop\<guillemotright> (Val v2)) e1' (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<epsilon> (Throw a) h xs"
  "xs V = \<lfloor>v\<rfloor> \<Longrightarrow> sim_move10 P t \<epsilon> (Var V') e1' (Var V) h xs \<epsilon> (Val v) h xs"
  "sim_move10 P t \<epsilon> (V' := Val v) e1' (V := Val v) h xs \<epsilon> unit h (xs(V \<mapsto> v))"
  "sim_move10 P t \<epsilon> (null\<lfloor>Val v\<rceil>) e1' (null\<lfloor>Val v\<rceil>) h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; i <s 0 \<or> sint i \<ge> int n \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (addr a\<lfloor>Val (Intg i)\<rceil>) e1' ((addr a)\<lfloor>Val (Intg i)\<rceil>) h xs \<epsilon> (THROW ArrayIndexOutOfBounds) h xs"
  "\<lbrakk> typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 <=s i; sint i < int n;
     heap_read h a (ACell (nat (sint i))) v;
     ta1 = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (addr a\<lfloor>Val (Intg i)\<rceil>) e1' ((addr a)\<lfloor>Val (Intg i)\<rceil>) h xs ta (Val v) h xs"
  "sim_move10 P t \<epsilon> (null\<lfloor>Val v\<rceil> := Val v') e1' (null\<lfloor>Val v\<rceil> := Val v') h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; i <s 0 \<or> sint i \<ge> int n \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs \<epsilon> (THROW ArrayIndexOutOfBounds) h xs"
 "\<lbrakk> typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 <=s i; sint i < int n; typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; \<not> (P \<turnstile> U \<le> T) \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs \<epsilon> (THROW ArrayStore) h xs"
  "\<lbrakk> typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 <=s i; sint i < int n; typeof\<^bsub>h\<^esub> v = Some U; P \<turnstile> U \<le> T;
     heap_write h a (ACell (nat (sint i))) v h';
     ta1 = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs ta unit h' xs"
  "typeof_addr h a = \<lfloor>Array_type T n\<rfloor> \<Longrightarrow> sim_move10 P t \<epsilon> (addr a\<bullet>length) e1' (addr a\<bullet>length) h xs \<epsilon> (Val (Intg (word_of_nat n))) h xs"
  "sim_move10 P t \<epsilon> (null\<bullet>length) e1' (null\<bullet>length) h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> heap_read h a (CField D F) v; ta1 = \<lbrace>ReadMem a (CField D F) v\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>F{D}) e1' (addr a\<bullet>F{D}) h xs ta (Val v) h xs"
  "sim_move10 P t \<epsilon> (null\<bullet>F{D}) e1' (null\<bullet>F{D}) h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> heap_write h a (CField D F) v h'; ta1 = \<lbrace>WriteMem a (CField D F) v\<rbrace>; ta = \<lbrace>WriteMem a (CField D F) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>F{D} := Val v) e1' (addr a\<bullet>F{D} := Val v) h xs ta unit h' xs"
  "sim_move10 P t \<epsilon> (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> heap_read h a (CField D F) v''; heap_write h a (CField D F) v' h'; v'' = v;
     ta1 = \<lbrace> ReadMem a (CField D F) v'', WriteMem a (CField D F) v' \<rbrace>; ta = \<lbrace> ReadMem a (CField D F) v'', WriteMem a (CField D F) v' \<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta true h' xs"
  "\<lbrakk> heap_read h a (CField D F) v''; v'' \<noteq> v;
     ta1 = \<lbrace> ReadMem a (CField D F) v'' \<rbrace>; ta = \<lbrace> ReadMem a (CField D F) v'' \<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta false h xs"

  "sim_move10 P t \<epsilon> (null\<bullet>F{D} := Val v) e1' (null\<bullet>F{D} := Val v) h xs \<epsilon> (THROW NullPointer) h xs"
  "sim_move10 P t \<epsilon> ({V':T=None; Val u}) e1' ({V:T=vo; Val u}) h xs \<epsilon> (Val u) h xs"
  "sim_move10 P t \<epsilon> ({V':T=\<lfloor>v\<rfloor>; e}) ({V':T=None; e}) ({V:T=vo; e'}) h xs \<epsilon> ({V:T=vo; e'}) h xs"

  "sim_move10 P t \<epsilon> (sync\<^bsub>V'\<^esub>(null) e0) e1' (sync(null) e1) h xs \<epsilon> (THROW NullPointer) h xs"
  "sim_move10 P t \<epsilon> (Val v;;e0) e1' (Val v;; e1) h xs \<epsilon> e1 h xs"
  "sim_move10 P t \<epsilon> (if (true) e0 else e0') e1' (if (true) e1 else e2) h xs \<epsilon> e1 h xs"
  "sim_move10 P t \<epsilon> (if (false) e0 else e0') e1' (if (false) e1 else e2) h xs \<epsilon> e2 h xs"
  "sim_move10 P t \<epsilon> (throw null) e1' (throw null) h xs \<epsilon> (THROW NullPointer) h xs"
  "sim_move10 P t \<epsilon> (try (Val v) catch(C V') e0) e1' (try (Val v) catch(C V) e1) h xs \<epsilon> (Val v) h xs"
  "\<lbrakk> typeof_addr h a = \<lfloor>Class_type D\<rfloor>; P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (try (Throw a) catch(C V') e0) e1' (try (Throw a) catch(C V) e1) h xs \<epsilon> ({V:Class C=\<lfloor>Addr a\<rfloor>; e1}) h xs"
  "sim_move10 P t \<epsilon> (newA T\<lfloor>Throw a\<rceil>) e1' (newA T\<lfloor>Throw a\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Cast T (Throw a)) e1' (Cast T (Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> ((Throw a) instanceof T) e1' ((Throw a) instanceof T) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> ((Throw a) \<guillemotleft>bop\<guillemotright> e0) e1' ((Throw a) \<guillemotleft>bop\<guillemotright> e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v \<guillemotleft>bop\<guillemotright> (Throw a)) e1' (Val v \<guillemotleft>bop\<guillemotright> (Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (V' := Throw a) e1' (V := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<lfloor>e0\<rceil>) e1' (Throw a\<lfloor>e1\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v\<lfloor>Throw a\<rceil>) e1' (Val v\<lfloor>Throw a\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<lfloor>e0\<rceil> := e0') e1' (Throw a\<lfloor>e1\<rceil> := e2) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v\<lfloor>Throw a\<rceil> := e0) e1' (Val v\<lfloor>Throw a\<rceil> := e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v\<lfloor>Val v'\<rceil> := Throw a) e1' (Val v\<lfloor>Val v'\<rceil> := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<bullet>length) e1' (Throw a\<bullet>length) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<bullet>F{D}) e1' (Throw a\<bullet>F{D}) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<bullet>F{D} := e0) e1' (Throw a\<bullet>F{D} := e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v\<bullet>F{D} := Throw a) e1' (Val v\<bullet>F{D} := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (CompareAndSwap (Throw a) D F e0 e0') e1' (Throw a\<bullet>compareAndSwap(D\<bullet>F, e1'', e1''')) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (CompareAndSwap (Val v) D F (Throw a) e0') e1' (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e1'')) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (CompareAndSwap (Val v) D F (Val v') (Throw a)) e1' (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a\<bullet>M(es0)) e1' (Throw a\<bullet>M(es1)) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Val v\<bullet>M(map Val vs @ Throw a # es0)) e1' (Val v\<bullet>M(map Val vs @ Throw a # es1)) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> ({V':T=None; Throw a}) e1' ({V:T=vo; Throw a}) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (sync\<^bsub>V'\<^esub>(Throw a) e0) e1' (sync(Throw a) e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (Throw a;;e0) e1' (Throw a;;e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (if (Throw a) e0 else e0') e1' (if (Throw a) e1 else e2) h xs \<epsilon> (Throw a) h xs"
  "sim_move10 P t \<epsilon> (throw (Throw a)) e1' (throw (Throw a)) h xs \<epsilon> (Throw a) h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((((\<lbrakk>(h', a) \<in> allocate h (Class_type C); ta1 = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>; ta = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (new C) e1' (new C) h xs ta (addr a) h' xs) &&& (allocate h (Class_type C) = {} \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (new C) e1' (new C) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt OutOfMemory)) h xs) &&& (\<lbrakk>(h', a) \<in> allocate h (Array_type T (nat (sint i))); 0 \<le>s i; ta1 = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>; ta = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs ta (addr a) h' xs)) &&& ((i <s 0 \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NegativeArraySize)) h xs) &&& (\<lbrakk>allocate h (Array_type T (nat (sint i))) = {}; 0 \<le>s i\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (newA T\<lfloor>Val (Intg i)\<rceil>) e1' (newA T\<lfloor>Val (Intg i)\<rceil>) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt OutOfMemory)) h xs)) &&& (\<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Cast T (Val v)) e1' (Cast T (Val v)) h xs \<lbrace>\<rbrace> (Val v) h xs) &&& (\<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Cast T (Val v)) e1' (Cast T (Val v)) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt ClassCast)) h xs)) &&& (((\<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; b = (v \<noteq> Null \<and> P \<turnstile> U \<le> T)\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Val v instanceof T) e1' (Val v instanceof T) h xs \<lbrace>\<rbrace> (Val (Bool b)) h xs) &&& (binop bop v1 v2 = \<lfloor>Inl v\<rfloor> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) e1' (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<lbrace>\<rbrace> (Val v) h xs)) &&& (binop bop v1 v2 = \<lfloor>Inr a\<rfloor> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) e1' (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (xs V = \<lfloor>v\<rfloor> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (Var V') e1' (Var V) h xs \<lbrace>\<rbrace> (Val v) h xs)) &&& (sim_move10 P t \<lbrace>\<rbrace> (V':=Val v) e1' (V:=Val v) h xs \<lbrace>\<rbrace> unit h (xs(V \<mapsto> v)) &&& sim_move10 P t \<lbrace>\<rbrace> (null\<lfloor>Val v\<rceil>) e1' (null\<lfloor>Val v\<rceil>) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& (\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; i <s 0 \<or> int n \<le> sint i\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil>) e1' (addr a\<lfloor>Val (Intg i)\<rceil>) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt ArrayIndexOutOfBounds)) h xs) &&& (\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 \<le>s i; sint i < int n; heap_read h a (ACell (nat (sint i))) v; ta1 = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<lfloor>Val (Intg i)\<rceil>) e1' (addr a\<lfloor>Val (Intg i)\<rceil>) h xs ta (Val v) h xs)) &&& (((sim_move10 P t \<lbrace>\<rbrace> (null\<lfloor>Val v\<rceil> := Val v') e1' (null\<lfloor>Val v\<rceil> := Val v') h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs &&& (\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; i <s 0 \<or> int n \<le> sint i\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) e1' (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt ArrayIndexOutOfBounds)) h xs)) &&& (\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 \<le>s i; sint i < int n; typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) e1' (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt ArrayStore)) h xs) &&& (\<lbrakk>typeof_addr h a = \<lfloor>Array_type T n\<rfloor>; 0 \<le>s i; sint i < int n; typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T; heap_write h a (ACell (nat (sint i))) v h'; ta1 = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) e1' (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) h xs ta unit h' xs)) &&& ((typeof_addr h a = \<lfloor>Array_type T n\<rfloor> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (addr a\<bullet>length) e1' (addr a\<bullet>length) h xs \<lbrace>\<rbrace> (Val (Intg (word_of_nat n))) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (null\<bullet>length) e1' (null\<bullet>length) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& (\<lbrakk>heap_read h a (CField D F) v; ta1 = \<lbrace>ReadMem a (CField D F) v\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>F{D}) e1' (addr a\<bullet>F{D}) h xs ta (Val v) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (null\<bullet>F{D}) e1' (null\<bullet>F{D}) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& (((\<lbrakk>heap_write h a (CField D F) v h'; ta1 = \<lbrace>WriteMem a (CField D F) v\<rbrace>; ta = \<lbrace>WriteMem a (CField D F) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>F{D} := Val v) e1' (addr a\<bullet>F{D} := Val v) h xs ta unit h' xs) &&& sim_move10 P t \<lbrace>\<rbrace> (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& (\<lbrakk>heap_read h a (CField D F) v''; heap_write h a (CField D F) v' h'; v'' = v; ta1 = \<lbrace>ReadMem a (CField D F) v'', WriteMem a (CField D F) v'\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v'', WriteMem a (CField D F) v'\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta true h' xs) &&& (\<lbrakk>heap_read h a (CField D F) v''; v'' \<noteq> v; ta1 = \<lbrace>ReadMem a (CField D F) v''\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v''\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) e1' (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta false h xs)) &&& (sim_move10 P t \<lbrace>\<rbrace> (null\<bullet>F{D} := Val v) e1' (null\<bullet>F{D} := Val v) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs &&& sim_move10 P t \<lbrace>\<rbrace> {V':T=None; Val u} e1' {V:T=vo; Val u} h xs \<lbrace>\<rbrace> (Val u) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> {V':T=\<lfloor>v\<rfloor>; e} {V':T=None; e} {V:T=vo; e'} h xs \<lbrace>\<rbrace> {V:T=vo; e'} h xs &&& sim_move10 P t \<lbrace>\<rbrace> (sync\<^bsub>V'\<^esub> (null) e0) e1' (sync(null) e1) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& (((sim_move10 P t \<lbrace>\<rbrace> (Val v;; e0) e1' (Val v;; e1) h xs \<lbrace>\<rbrace> e1 h xs &&& sim_move10 P t \<lbrace>\<rbrace> (if (true) e0 else e0') e1' (if (true) e1 else e2) h xs \<lbrace>\<rbrace> e1 h xs &&& sim_move10 P t \<lbrace>\<rbrace> (if (false) e0 else e0') e1' (if (false) e1 else e2) h xs \<lbrace>\<rbrace> e2 h xs) &&& (sim_move10 P t \<lbrace>\<rbrace> (throw null) e1' (throw null) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (try Val v catch(C V') e0) e1' (try Val v catch(C V) e1) h xs \<lbrace>\<rbrace> (Val v) h xs) &&& (\<lbrakk>typeof_addr h a = \<lfloor>Class_type D\<rfloor>; P \<turnstile> D \<preceq>\<^sup>* C\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (try Throw a catch(C V') e0) e1' (try Throw a catch(C V) e1) h xs \<lbrace>\<rbrace> {V:Class C=\<lfloor>Addr a\<rfloor>; e1} h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (newA T\<lfloor>Throw a\<rceil>) e1' (newA T\<lfloor>Throw a\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& ((sim_move10 P t \<lbrace>\<rbrace> (Cast T (Throw a)) e1' (Cast T (Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a instanceof T) e1' (Throw a instanceof T) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a \<guillemotleft>bop\<guillemotright> e0) e1' (Throw a \<guillemotleft>bop\<guillemotright> e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Val v \<guillemotleft>bop\<guillemotright> Throw a) e1' (Val v \<guillemotleft>bop\<guillemotright> Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move10 P t \<lbrace>\<rbrace> (V':=Throw a) e1' (V:=Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<lfloor>e0\<rceil>) e1' (Throw a\<lfloor>e1\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (Val v\<lfloor>Throw a\<rceil>) e1' (Val v\<lfloor>Throw a\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<lfloor>e0\<rceil> := e0') e1' (Throw a\<lfloor>e1\<rceil> := e2) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (((sim_move10 P t \<lbrace>\<rbrace> (Val v\<lfloor>Throw a\<rceil> := e0) e1' (Val v\<lfloor>Throw a\<rceil> := e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Val v\<lfloor>Val v'\<rceil> := Throw a) e1' (Val v\<lfloor>Val v'\<rceil> := Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<bullet>length) e1' (Throw a\<bullet>length) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<bullet>F{D}) e1' (Throw a\<bullet>F{D}) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move10 P t \<lbrace>\<rbrace> (Throw a\<bullet>F{D} := e0) e1' (Throw a\<bullet>F{D} := e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Val v\<bullet>F{D} := Throw a) e1' (Val v\<bullet>F{D} := Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<bullet>compareAndSwap(D\<bullet>F, e0, e0')) e1' (Throw a\<bullet>compareAndSwap(D\<bullet>F, e1'', e1''')) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e0')) e1' (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e1'')) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& ((sim_move10 P t \<lbrace>\<rbrace> (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) e1' (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a\<bullet>M(es0)) e1' (Throw a\<bullet>M(es1)) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (Val v\<bullet>M(map Val vs @ Throw a # es0)) e1' (Val v\<bullet>M(map Val vs @ Throw a # es1)) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> {V':T=None; Throw a} e1' {V:T=vo; Throw a} h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move10 P t \<lbrace>\<rbrace> (sync\<^bsub>V'\<^esub> (Throw a) e0) e1' (sync(Throw a) e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (Throw a;; e0) e1' (Throw a;; e1) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move10 P t \<lbrace>\<rbrace> (if (Throw a) e0 else e0') e1' (if (Throw a) e1 else e2) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move10 P t \<lbrace>\<rbrace> (throw (Throw a)) e1' (throw (Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs
[PROOF STEP]
apply(fastforce simp add: sim_move10_def no_calls_def no_call_def ta_bisim_def intro: red_reds.intros)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move10_CallNull:
  "sim_move10 P t \<epsilon> (null\<bullet>M(map Val vs)) e1' (null\<bullet>M(map Val vs)) h xs \<epsilon> (THROW NullPointer) h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move10 P t \<lbrace>\<rbrace> (null\<bullet>M(map Val vs)) e1' (null\<bullet>M(map Val vs)) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs
[PROOF STEP]
by(fastforce simp add: sim_move10_def map_eq_append_conv intro: RedCallNull)


[STATEMENT]
lemma sim_move10_SyncLocks:
  "\<lbrakk> ta1 = \<lbrace>Lock\<rightarrow>a, SyncLock a\<rbrace>; ta = \<lbrace>Lock\<rightarrow>a, SyncLock a\<rbrace> \<rbrakk>
   \<Longrightarrow> sim_move10 P t ta1 (sync\<^bsub>V\<^esub>(addr a) e0) e1' (sync(addr a) e1) h xs ta (insync(a) e1) h xs"
  "\<lbrakk> ta1 = \<lbrace>Unlock\<rightarrow>a, SyncUnlock a\<rbrace>; ta = \<lbrace>Unlock\<rightarrow>a, SyncUnlock a\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (insync\<^bsub>V\<^esub>(a') (Val v)) e1' (insync(a) (Val v)) h xs ta (Val v) h xs"
  "\<lbrakk> ta1 = \<lbrace>Unlock\<rightarrow>a, SyncUnlock a\<rbrace>; ta = \<lbrace>Unlock\<rightarrow>a, SyncUnlock a\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move10 P t ta1 (insync\<^bsub>V\<^esub>(a') (Throw a'')) e1' (insync(a) (Throw a'')) h xs ta (Throw a'') h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>ta1 = \<lbrace>(Lock, a), SyncLock a\<rbrace>; ta = \<lbrace>(Lock, a), SyncLock a\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (sync\<^bsub>V\<^esub> (addr a) e0) e1' (sync(addr a) e1) h xs ta (insync(a) e1) h xs) &&& (\<lbrakk>ta1 = \<lbrace>(Unlock, a), SyncUnlock a\<rbrace>; ta = \<lbrace>(Unlock, a), SyncUnlock a\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (insync\<^bsub>V\<^esub> (a') Val v) e1' (insync(a) Val v) h xs ta (Val v) h xs) &&& (\<lbrakk>ta1 = \<lbrace>(Unlock, a), SyncUnlock a\<rbrace>; ta = \<lbrace>(Unlock, a), SyncUnlock a\<rbrace>\<rbrakk> \<Longrightarrow> sim_move10 P t ta1 (insync\<^bsub>V\<^esub> (a') Throw a'') e1' (insync(a) Throw a'') h xs ta (Throw a'') h xs)
[PROOF STEP]
by(fastforce simp add: sim_move10_def ta_bisim_def ta_upd_simps intro: red_reds.intros[simplified])+


[STATEMENT]
lemma sim_move10_TryFail:
  "\<lbrakk> typeof_addr h a = \<lfloor>Class_type D\<rfloor>; \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
  \<Longrightarrow> sim_move10 P t \<epsilon> (try (Throw a) catch(C V') e0) e1' (try (Throw a) catch(C V) e1) h xs \<epsilon> (Throw a) h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typeof_addr h a = \<lfloor>Class_type D\<rfloor>; \<not> P \<turnstile> D \<preceq>\<^sup>* C\<rbrakk> \<Longrightarrow> sim_move10 P t \<lbrace>\<rbrace> (try Throw a catch(C V') e0) e1' (try Throw a catch(C V) e1) h xs \<lbrace>\<rbrace> (Throw a) h xs
[PROOF STEP]
by(auto simp add: sim_move10_def intro!: RedTryFail)


[STATEMENT]
lemma sim_move10_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "\<lbrakk> sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs'; \<D> e \<lfloor>dom xs\<rfloor> \<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs'; \<D> e \<lfloor>dom xs\<rfloor>\<rbrakk> \<Longrightarrow> \<D> e' \<lfloor>dom xs'\<rfloor>
[PROOF STEP]
by(auto simp add: sim_move10_def split: if_split_asm dest!: \<tau>red0r_preserves_defass[OF wf] \<tau>red0t_preserves_defass[OF wf] red_preserves_defass[OF wf])