[STATEMENT]
lemma sim_move01_reds:
  "\<lbrakk> (h', a) \<in> allocate h (Class_type C); ta0 = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>; ta = \<lbrace>NewHeapElem a (Class_type C)\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (new C) (new C) h xs ta (addr a) h' xs"
  "allocate h (Class_type C) = {} \<Longrightarrow> sim_move01 P t \<epsilon> (new C) (new C) h xs \<epsilon> (THROW OutOfMemory) h xs"
  "\<lbrakk> (h', a) \<in> allocate h (Array_type T (nat (sint i))); 0 <=s i;
     ta0 = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>; ta = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (newA T\<lfloor>Val (Intg i)\<rceil>) (newA T\<lfloor>Val (Intg i)\<rceil>) h xs ta (addr a) h' xs"
  "i <s 0 \<Longrightarrow> sim_move01 P t \<epsilon> (newA T\<lfloor>Val (Intg i)\<rceil>) (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_move01 P t \<epsilon> (newA T\<lfloor>Val (Intg i)\<rceil>) (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_move01 P t \<epsilon> (Cast T (Val v)) (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_move01 P t \<epsilon> (Cast T (Val v)) (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_move01 P t \<epsilon> ((Val v) instanceof T) ((Val v) instanceof T) h xs \<epsilon> (Val (Bool b)) h xs"
  "binop bop v1 v2 = Some (Inl v) \<Longrightarrow> sim_move01 P t \<epsilon> ((Val v1) \<guillemotleft>bop\<guillemotright> (Val v2)) (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<epsilon> (Val v) h xs"
  "binop bop v1 v2 = Some (Inr a) \<Longrightarrow> sim_move01 P t \<epsilon> ((Val v1) \<guillemotleft>bop\<guillemotright> (Val v2)) (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<epsilon> (Throw a) h xs"
  "\<lbrakk> xs!V = v; V < size xs \<rbrakk> \<Longrightarrow> sim_move01 P t \<epsilon> (Var V') (Var V) h xs \<epsilon> (Val v) h xs"
  "V < length xs \<Longrightarrow> sim_move01 P t \<epsilon> (V' := Val v) (V := Val v) h xs \<epsilon> unit h (xs[V := v])"
  "sim_move01 P t \<epsilon> (null\<lfloor>Val v\<rceil>) (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_move01 P t \<epsilon> (addr a\<lfloor>Val (Intg i)\<rceil>) ((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;
     ta0 = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>;
     ta = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (addr a\<lfloor>Val (Intg i)\<rceil>) ((addr a)\<lfloor>Val (Intg i)\<rceil>) h xs ta (Val v) h xs"
  "sim_move01 P t \<epsilon> (null\<lfloor>Val v\<rceil> := Val v') (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_move01 P t \<epsilon> (AAss (addr a) (Val (Intg i)) (Val v)) (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_move01 P t \<epsilon> (AAss (addr a) (Val (Intg i)) (Val v)) (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';
     ta0 = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>WriteMem a (ACell (nat (sint i))) v \<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (AAss (addr a) (Val (Intg i)) (Val v)) (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_move01 P t \<epsilon> (addr a\<bullet>length) (addr a\<bullet>length) h xs \<epsilon> (Val (Intg (word_of_int (int n)))) h xs"
  "sim_move01 P t \<epsilon> (null\<bullet>length) (null\<bullet>length) h xs \<epsilon> (THROW NullPointer) h xs"

  "\<lbrakk> heap_read h a (CField D F) v; ta0 = \<lbrace>ReadMem a (CField D F) v\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>F{D}) (addr a\<bullet>F{D}) h xs ta (Val v) h xs"
  "sim_move01 P t \<epsilon> (null\<bullet>F{D}) (null\<bullet>F{D}) h xs \<epsilon> (THROW NullPointer) h xs"
  "\<lbrakk> heap_write h a (CField D F) v h'; ta0 = \<lbrace>WriteMem a (CField D F) v\<rbrace>; ta = \<lbrace>WriteMem a (CField D F) v\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>F{D} := Val v) (addr a\<bullet>F{D} := Val v) h xs ta unit h' xs"
  "sim_move01 P t \<epsilon> (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (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;
     ta0 = \<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_move01 P t ta0 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (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;
     ta0 = \<lbrace>ReadMem a (CField D F) v''\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v''\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta false h xs"
  "sim_move01 P t \<epsilon> (null\<bullet>F{D} := Val v) (null\<bullet>F{D} := Val v) h xs \<epsilon> (THROW NullPointer) h xs"
  "sim_move01 P t \<epsilon> ({V':T=vo; Val u}) ({V:T=None; Val u}) h xs \<epsilon> (Val u) h xs"
  "V < length xs \<Longrightarrow> sim_move01 P t \<epsilon> (sync(null) e0) (sync\<^bsub>V\<^esub> (null) e1) h xs \<epsilon> (THROW NullPointer) h (xs[V := Null])"
  "sim_move01 P t \<epsilon> (Val v;;e0) (Val v;; e1) h xs \<epsilon> e1 h xs"
  "sim_move01 P t \<epsilon> (if (true) e0 else e0') (if (true) e1 else e1') h xs \<epsilon> e1 h xs"
  "sim_move01 P t \<epsilon> (if (false) e0 else e0') (if (false) e1 else e1') h xs \<epsilon> e1' h xs"
  "sim_move01 P t \<epsilon> (throw null) (throw null) h xs \<epsilon> (THROW NullPointer) h xs"
  "sim_move01 P t \<epsilon> (try (Val v) catch(C V') e0) (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; V < length xs \<rbrakk>
  \<Longrightarrow> sim_move01 P t \<epsilon> (try (Throw a) catch(C V') e0) (try (Throw a) catch(C V) e1) h xs \<epsilon> ({V:Class C=None; e1}) h (xs[V := Addr a])"
  "sim_move01 P t \<epsilon> (newA T\<lfloor>Throw a\<rceil>) (newA T\<lfloor>Throw a\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Cast T (Throw a)) (Cast T (Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> ((Throw a) instanceof T) ((Throw a) instanceof T) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> ((Throw a) \<guillemotleft>bop\<guillemotright> e0) ((Throw a) \<guillemotleft>bop\<guillemotright> e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v \<guillemotleft>bop\<guillemotright> (Throw a)) (Val v \<guillemotleft>bop\<guillemotright> (Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (V' := Throw a) (V := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<lfloor>e0\<rceil>) (Throw a\<lfloor>e1\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<lfloor>Throw a\<rceil>) (Val v\<lfloor>Throw a\<rceil>) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<lfloor>e0\<rceil> := e0') (Throw a\<lfloor>e1\<rceil> := e1') h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<lfloor>Throw a\<rceil> := e0) (Val v\<lfloor>Throw a\<rceil> := e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<lfloor>Val v'\<rceil> := Throw a) (Val v\<lfloor>Val v'\<rceil> := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<bullet>length) (Throw a\<bullet>length) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<bullet>F{D}) (Throw a\<bullet>F{D}) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<bullet>F{D} := e0) (Throw a\<bullet>F{D} := e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<bullet>F{D} := Throw a) (Val v\<bullet>F{D} := Throw a) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) (Throw a\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e3)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e3')) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a\<bullet>M(es0)) (Throw a\<bullet>M(es1)) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> ({V':T=vo; Throw a}) ({V:T=None; Throw a}) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (sync(Throw a) e0) (sync\<^bsub>V\<^esub>(Throw a) e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (Throw a;;e0) (Throw a;;e1) h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (if (Throw a) e0 else e0') (if (Throw a) e1 else e1') h xs \<epsilon> (Throw a) h xs"
  "sim_move01 P t \<epsilon> (throw (Throw a)) (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); ta0 = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>; ta = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (new C) (new C) h xs ta (addr a) h' xs) &&& (allocate h (Class_type C) = {} \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (new C) (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; ta0 = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>; ta = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (newA T\<lfloor>Val (Intg i)\<rceil>) (newA T\<lfloor>Val (Intg i)\<rceil>) h xs ta (addr a) h' xs)) &&& ((i <s 0 \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (newA T\<lfloor>Val (Intg i)\<rceil>) (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_move01 P t \<lbrace>\<rbrace> (newA T\<lfloor>Val (Intg i)\<rceil>) (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_move01 P t \<lbrace>\<rbrace> (Cast T (Val v)) (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_move01 P t \<lbrace>\<rbrace> (Cast T (Val v)) (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_move01 P t \<lbrace>\<rbrace> (Val v instanceof T) (Val v instanceof T) h xs \<lbrace>\<rbrace> (Val (Bool b)) h xs) &&& (binop bop v1 v2 = \<lfloor>Inl v\<rfloor> \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) (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_move01 P t \<lbrace>\<rbrace> (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (\<lbrakk>xs ! V = v; V < length xs\<rbrakk> \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (Var V') (Var V) h xs \<lbrace>\<rbrace> (Val v) h xs)) &&& ((V < length xs \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (V':=Val v) (V:=Val v) h xs \<lbrace>\<rbrace> unit h (xs[V := v])) &&& sim_move01 P t \<lbrace>\<rbrace> (null\<lfloor>Val v\<rceil>) (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_move01 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil>) (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; ta0 = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>ReadMem a (ACell (nat (sint i))) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (addr a\<lfloor>Val (Intg i)\<rceil>) (addr a\<lfloor>Val (Intg i)\<rceil>) h xs ta (Val v) h xs)) &&& ((sim_move01 P t \<lbrace>\<rbrace> (null\<lfloor>Val v\<rceil> := Val v') (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_move01 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) (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_move01 P t \<lbrace>\<rbrace> (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) (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'; ta0 = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>; ta = \<lbrace>WriteMem a (ACell (nat (sint i))) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (addr a\<lfloor>Val (Intg i)\<rceil> := Val v) (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_move01 P t \<lbrace>\<rbrace> (addr a\<bullet>length) (addr a\<bullet>length) h xs \<lbrace>\<rbrace> (Val (Intg (word_of_int (int n)))) h xs)) &&& sim_move01 P t \<lbrace>\<rbrace> (null\<bullet>length) (null\<bullet>length) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs &&& (\<lbrakk>heap_read h a (CField D F) v; ta0 = \<lbrace>ReadMem a (CField D F) v\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>F{D}) (addr a\<bullet>F{D}) h xs ta (Val v) h xs)) &&& ((sim_move01 P t \<lbrace>\<rbrace> (null\<bullet>F{D}) (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'; ta0 = \<lbrace>WriteMem a (CField D F) v\<rbrace>; ta = \<lbrace>WriteMem a (CField D F) v\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>F{D} := Val v) (addr a\<bullet>F{D} := Val v) h xs ta unit h' xs)) &&& sim_move01 P t \<lbrace>\<rbrace> (null\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (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; ta0 = \<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_move01 P t ta0 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (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; ta0 = \<lbrace>ReadMem a (CField D F) v''\<rbrace>; ta = \<lbrace>ReadMem a (CField D F) v''\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) (addr a\<bullet>compareAndSwap(D\<bullet>F, Val v, Val v')) h xs ta false h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (null\<bullet>F{D} := Val v) (null\<bullet>F{D} := Val v) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> {V':T=vo; Val u} {V:T=None; Val u} h xs \<lbrace>\<rbrace> (Val u) h xs &&& (V < length xs \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (sync(null) e0) (sync\<^bsub>V\<^esub> (null) e1) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h (xs[V := Null]))) &&& (((sim_move01 P t \<lbrace>\<rbrace> (Val v;; e0) (Val v;; e1) h xs \<lbrace>\<rbrace> e1 h xs &&& sim_move01 P t \<lbrace>\<rbrace> (if (true) e0 else e0') (if (true) e1 else e1') h xs \<lbrace>\<rbrace> e1 h xs &&& sim_move01 P t \<lbrace>\<rbrace> (if (false) e0 else e0') (if (false) e1 else e1') h xs \<lbrace>\<rbrace> e1' h xs) &&& (sim_move01 P t \<lbrace>\<rbrace> (throw null) (throw null) h xs \<lbrace>\<rbrace> (Throw (addr_of_sys_xcpt NullPointer)) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (try Val v catch(C V') e0) (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; V < length xs\<rbrakk> \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> (try Throw a catch(C V') e0) (try Throw a catch(C V) e1) h xs \<lbrace>\<rbrace> {V:Class C=None; e1} h (xs[V := Addr a])) &&& sim_move01 P t \<lbrace>\<rbrace> (newA T\<lfloor>Throw a\<rceil>) (newA T\<lfloor>Throw a\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& ((sim_move01 P t \<lbrace>\<rbrace> (Cast T (Throw a)) (Cast T (Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a instanceof T) (Throw a instanceof T) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a \<guillemotleft>bop\<guillemotright> e0) (Throw a \<guillemotleft>bop\<guillemotright> e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Val v \<guillemotleft>bop\<guillemotright> Throw a) (Val v \<guillemotleft>bop\<guillemotright> Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move01 P t \<lbrace>\<rbrace> (V':=Throw a) (V:=Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<lfloor>e0\<rceil>) (Throw a\<lfloor>e1\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (Val v\<lfloor>Throw a\<rceil>) (Val v\<lfloor>Throw a\<rceil>) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<lfloor>e0\<rceil> := e0') (Throw a\<lfloor>e1\<rceil> := e1') h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& ((sim_move01 P t \<lbrace>\<rbrace> (Val v\<lfloor>Throw a\<rceil> := e0) (Val v\<lfloor>Throw a\<rceil> := e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Val v\<lfloor>Val v'\<rceil> := Throw a) (Val v\<lfloor>Val v'\<rceil> := Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<bullet>length) (Throw a\<bullet>length) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move01 P t \<lbrace>\<rbrace> (Throw a\<bullet>F{D}) (Throw a\<bullet>F{D}) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<bullet>F{D} := e0) (Throw a\<bullet>F{D} := e1) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (Val v\<bullet>F{D} := Throw a) (Val v\<bullet>F{D} := Throw a) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) (Throw a\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& ((sim_move01 P t \<lbrace>\<rbrace> (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e3)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Throw a, e3')) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a\<bullet>M(es0)) (Throw a\<bullet>M(es1)) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> {V':T=vo; Throw a} {V:T=None; Throw a} h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& (sim_move01 P t \<lbrace>\<rbrace> (sync(Throw a) e0) (sync\<^bsub>V\<^esub> (Throw a) e1) h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (Throw a;; e0) (Throw a;; e1) h xs \<lbrace>\<rbrace> (Throw a) h xs) &&& sim_move01 P t \<lbrace>\<rbrace> (if (Throw a) e0 else e0') (if (Throw a) e1 else e1') h xs \<lbrace>\<rbrace> (Throw a) h xs &&& sim_move01 P t \<lbrace>\<rbrace> (throw (Throw a)) (throw (Throw a)) h xs \<lbrace>\<rbrace> (Throw a) h xs
[PROOF STEP]
apply(simp_all add: sim_move01_def ta_bisim_def split: if_split_asm split del: if_split)
[PROOF STATE]
proof (prove)
goal (60 subgoals):
 1. \<lbrakk>(h', a) \<in> allocate h (Class_type C); ta0 = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>; ta = \<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rbrakk> \<Longrightarrow> \<not> final (new C) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (new C, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>NewHeapElem a (Class_type C)\<rbrace>\<rightarrow> \<langle>addr a,(h', xs)\<rangle> \<and> \<not> \<tau>move1 P h e'')
 2. allocate h (Class_type C) = {} \<Longrightarrow> \<not> final (new C) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (new C, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'')
 3. \<lbrakk>(h', a) \<in> allocate h (Array_type T (nat (sint i))); 0 \<le>s i; ta0 = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>; ta = \<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rbrakk> \<Longrightarrow> \<not> final (newA T\<lfloor>Val (Intg i)\<rceil>) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (newA T\<lfloor>Val (Intg i)\<rceil>, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>NewHeapElem a (Array_type T (nat (sint i)))\<rbrace>\<rightarrow> \<langle>addr a,(h', xs)\<rangle> \<and> \<not> \<tau>move1 P h e'')
 4. i <s 0 \<Longrightarrow> \<not> final (newA T\<lfloor>Val (Intg i)\<rceil>) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (newA T\<lfloor>Val (Intg i)\<rceil>, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt NegativeArraySize),(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'')
 5. \<lbrakk>allocate h (Array_type T (nat (sint i))) = {}; 0 \<le>s i\<rbrakk> \<Longrightarrow> \<not> final (newA T\<lfloor>Val (Intg i)\<rceil>) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (newA T\<lfloor>Val (Intg i)\<rceil>, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw (addr_of_sys_xcpt OutOfMemory),(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'')
 6. \<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> \<not> final (Cast T (Val v)) \<and> \<tau>red1't P t h (Cast T (Val v), xs) (Val v, xs)
 7. \<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; \<not> P \<turnstile> U \<le> T\<rbrakk> \<Longrightarrow> \<not> final (Cast T (Val v)) \<and> \<tau>red1't P t h (Cast T (Val v), xs) (Throw (addr_of_sys_xcpt ClassCast), xs)
 8. \<lbrakk>typeof\<^bsub>h\<^esub> v = \<lfloor>U\<rfloor>; b = (v \<noteq> Null \<and> P \<turnstile> U \<le> T)\<rbrakk> \<Longrightarrow> \<not> final (Val v instanceof T) \<and> \<tau>red1't P t h (Val v instanceof T, xs) (Val (Bool (v \<noteq> Null \<and> P \<turnstile> U \<le> T)), xs)
 9. binop bop v1 v2 = \<lfloor>Inl v\<rfloor> \<Longrightarrow> \<not> final (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) \<and> \<tau>red1't P t h (Val v1 \<guillemotleft>bop\<guillemotright> Val v2, xs) (Val v, xs)
 10. binop bop v1 v2 = \<lfloor>Inr a\<rfloor> \<Longrightarrow> \<not> final (Val v1 \<guillemotleft>bop\<guillemotright> Val v2) \<and> \<tau>red1't P t h (Val v1 \<guillemotleft>bop\<guillemotright> Val v2, xs) (Throw a, xs)
A total of 60 subgoals...
[PROOF STEP]
apply(fastforce intro: red1_reds1.intros)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move01_ThrowParams:
  "sim_move01 P t \<epsilon> (Val v\<bullet>M(map Val vs @ Throw a # es0)) (Val v\<bullet>M(map Val vs @ Throw a # es1)) h xs \<epsilon> (Throw a) h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move01 P t \<lbrace>\<rbrace> (Val v\<bullet>M(map Val vs @ Throw a # es0)) (Val v\<bullet>M(map Val vs @ Throw a # es1)) h xs \<lbrace>\<rbrace> (Throw a) h xs
[PROOF STEP]
apply(simp add: sim_move01_def split del: if_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> final (Val v\<bullet>M(map Val vs @ Throw a # es0)) \<and> (if (\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M)))) then h = h \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (Throw a, xs) else ta_bisim01 \<lbrace>\<rbrace> (extTA2J1 P \<lbrace>\<rbrace>) \<and> (if call (Val v\<bullet>M(map Val vs @ Throw a # es0)) = None \<or> call1 (Val v\<bullet>M(map Val vs @ Throw a # es1)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(map Val vs @ Throw a # es1),(h, xs)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(map Val vs @ Throw a # es1))))
[PROOF STEP]
apply(rule conjI, fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if (\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M)))) then h = h \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (Throw a, xs) else ta_bisim01 \<lbrace>\<rbrace> (extTA2J1 P \<lbrace>\<rbrace>) \<and> (if call (Val v\<bullet>M(map Val vs @ Throw a # es0)) = None \<or> call1 (Val v\<bullet>M(map Val vs @ Throw a # es1)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(map Val vs @ Throw a # es1),(h, xs)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(map Val vs @ Throw a # es1)))
[PROOF STEP]
apply(split if_split)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M)))) \<longrightarrow> h = h \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (Throw a, xs)) \<and> (\<not> ((\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M))))) \<longrightarrow> ta_bisim01 \<lbrace>\<rbrace> (extTA2J1 P \<lbrace>\<rbrace>) \<and> (if call (Val v\<bullet>M(map Val vs @ Throw a # es0)) = None \<or> call1 (Val v\<bullet>M(map Val vs @ Throw a # es1)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(map Val vs @ Throw a # es1),(h, xs)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(map Val vs @ Throw a # es1))))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M)))) \<longrightarrow> h = h \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<lbrace>\<rbrace> = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (Throw a, xs)
 2. \<not> ((\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M))))) \<longrightarrow> ta_bisim01 \<lbrace>\<rbrace> (extTA2J1 P \<lbrace>\<rbrace>) \<and> (if call (Val v\<bullet>M(map Val vs @ Throw a # es0)) = None \<or> call1 (Val v\<bullet>M(map Val vs @ Throw a # es1)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(map Val vs @ Throw a # es1),(h, xs)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(map Val vs @ Throw a # es1)))
[PROOF STEP]
apply(fastforce intro: red1_reds1.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> ((\<exists>vsa aa es'. map Val vs @ Throw a # es0 = map Val vsa @ Throw aa # es') \<or> (\<exists>vsa. map Val vs @ Throw a # es0 = map Val vsa) \<and> (v = Null \<or> (\<forall>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<longrightarrow> (\<forall>C. class_type_of' T = \<lfloor>C\<rfloor> \<longrightarrow> (\<forall>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<longrightarrow> \<tau>external_defs D M))))) \<longrightarrow> ta_bisim01 \<lbrace>\<rbrace> (extTA2J1 P \<lbrace>\<rbrace>) \<and> (if call (Val v\<bullet>M(map Val vs @ Throw a # es0)) = None \<or> call1 (Val v\<bullet>M(map Val vs @ Throw a # es1)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(map Val vs @ Throw a # es1), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(map Val vs @ Throw a # es1),(h, xs)\<rangle> -\<lbrace>\<rbrace>\<rightarrow> \<langle>Throw a,(h, xs)\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(map Val vs @ Throw a # es1)))
[PROOF STEP]
apply(fastforce simp add: sim_move01_def intro: red1_reds1.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move01_CallNull:
  "sim_move01 P t \<epsilon> (null\<bullet>M(map Val vs)) (null\<bullet>M(map Val vs)) h xs \<epsilon> (THROW NullPointer) h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move01 P t \<lbrace>\<rbrace> (null\<bullet>M(map Val vs)) (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_move01_def map_eq_append_conv intro: red1_reds1.intros)


[STATEMENT]
lemma sim_move01_SyncLocks:
  "\<lbrakk> V < length xs; ta0 = \<lbrace>Lock\<rightarrow>a, SyncLock a\<rbrace>; ta = \<lbrace>Lock\<rightarrow>a, SyncLock a\<rbrace> \<rbrakk>
   \<Longrightarrow> sim_move01 P t ta0 (sync(addr a) e0) (sync\<^bsub>V\<^esub> (addr a) e1) h xs ta (insync\<^bsub>V\<^esub> (a) e1) h (xs[V := Addr a])"
  "\<lbrakk> xs ! V = Addr a'; V < length xs; ta0 = \<lbrace>Unlock\<rightarrow>a', SyncUnlock a'\<rbrace>; ta = \<lbrace>Unlock\<rightarrow>a', SyncUnlock a'\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (insync(a') (Val v)) (insync\<^bsub>V\<^esub> (a) (Val v)) h xs ta (Val v) h xs"
  "\<lbrakk> xs ! V = Addr a'; V < length xs; ta0 = \<lbrace>Unlock\<rightarrow>a', SyncUnlock a'\<rbrace>; ta = \<lbrace>Unlock\<rightarrow>a', SyncUnlock a'\<rbrace> \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 (insync(a') (Throw a'')) (insync\<^bsub>V\<^esub> (a) (Throw a'')) h xs ta (Throw a'') h xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>V < length xs; ta0 = \<lbrace>(Lock, a), SyncLock a\<rbrace>; ta = \<lbrace>(Lock, a), SyncLock a\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (sync(addr a) e0) (sync\<^bsub>V\<^esub> (addr a) e1) h xs ta (insync\<^bsub>V\<^esub> (a) e1) h (xs[V := Addr a])) &&& (\<lbrakk>xs ! V = Addr a'; V < length xs; ta0 = \<lbrace>(Unlock, a'), SyncUnlock a'\<rbrace>; ta = \<lbrace>(Unlock, a'), SyncUnlock a'\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (insync(a') Val v) (insync\<^bsub>V\<^esub> (a) Val v) h xs ta (Val v) h xs) &&& (\<lbrakk>xs ! V = Addr a'; V < length xs; ta0 = \<lbrace>(Unlock, a'), SyncUnlock a'\<rbrace>; ta = \<lbrace>(Unlock, a'), SyncUnlock a'\<rbrace>\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 (insync(a') Throw a'') (insync\<^bsub>V\<^esub> (a) Throw a'') h xs ta (Throw a'') h xs)
[PROOF STEP]
by(fastforce simp add: sim_move01_def ta_bisim_def expand_finfun_eq fun_eq_iff finfun_upd_apply ta_upd_simps  intro: red1_reds1.intros[simplified] split: if_split_asm)+


[STATEMENT]
lemma sim_move01_TryFail:
  "\<lbrakk> typeof_addr h a = \<lfloor>Class_type D\<rfloor>; \<not> P \<turnstile> D \<preceq>\<^sup>* C \<rbrakk>
  \<Longrightarrow> sim_move01 P t \<epsilon> (try (Throw a) catch(C V') e0) (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_move01 P t \<lbrace>\<rbrace> (try Throw a catch(C V') e0) (try Throw a catch(C V) e1) h xs \<lbrace>\<rbrace> (Throw a) h xs
[PROOF STEP]
by(auto simp add: sim_move01_def intro!: Red1TryFail)


[STATEMENT]
lemma sim_move01_BlockSome:
  "\<lbrakk> sim_move01 P t ta0 e0 e h (xs[V := v]) ta e' h' xs'; V < length xs \<rbrakk>
  \<Longrightarrow> sim_move01 P t ta0 ({V':T=\<lfloor>v\<rfloor>; e0}) ({V:T=\<lfloor>v\<rfloor>; e}) h xs ta ({V:T=None; e'}) h' xs'"
  "V < length xs \<Longrightarrow> sim_move01 P t \<epsilon> ({V':T=\<lfloor>v\<rfloor>; Val u}) ({V:T=\<lfloor>v\<rfloor>; Val u}) h xs \<epsilon> (Val u) h (xs[V := v])"
  "V < length xs \<Longrightarrow> sim_move01 P t \<epsilon> ({V':T=\<lfloor>v\<rfloor>; Throw a}) ({V:T=\<lfloor>v\<rfloor>; Throw a}) h xs \<epsilon> (Throw a) h (xs[V := v])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>sim_move01 P t ta0 e0 e h (xs[V := v]) ta e' h' xs'; V < length xs\<rbrakk> \<Longrightarrow> sim_move01 P t ta0 {V':T=\<lfloor>v\<rfloor>; e0} {V:T=\<lfloor>v\<rfloor>; e} h xs ta {V:T=None; e'} h' xs') &&& (V < length xs \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> {V':T=\<lfloor>v\<rfloor>; Val u} {V:T=\<lfloor>v\<rfloor>; Val u} h xs \<lbrace>\<rbrace> (Val u) h (xs[V := v])) &&& (V < length xs \<Longrightarrow> sim_move01 P t \<lbrace>\<rbrace> {V':T=\<lfloor>v\<rfloor>; Throw a} {V:T=\<lfloor>v\<rfloor>; Throw a} h xs \<lbrace>\<rbrace> (Throw a) h (xs[V := v]))
[PROOF STEP]
apply(auto simp add: sim_move01_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>V < length xs; \<not> final e0; \<not> \<tau>move0 P h e0; \<forall>a. e0 \<noteq> Throw a; \<forall>v. e0 \<noteq> Val v; ta_bisim01 ta0 (extTA2J1 P ta); if call e0 = None \<or> call1 e = None then \<exists>e'' xs''. \<tau>red1'r P t h (e, xs[V := v]) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>e,(h, xs[V := v])\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red1'r P t h ({V:T=\<lfloor>v\<rfloor>; e}, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>{V:T=None; e'},(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 2. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Val u}, xs) (Val u, xs[V := v])
 3. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Throw a}, xs) (Throw a, xs[V := v])
[PROOF STEP]
apply(split if_split_asm)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>V < length xs; \<not> final e0; \<not> \<tau>move0 P h e0; \<forall>a. e0 \<noteq> Throw a; \<forall>v. e0 \<noteq> Val v; ta_bisim01 ta0 (extTA2J1 P ta); call e0 = None \<or> call1 e = None; \<exists>e'' xs''. \<tau>red1'r P t h (e, xs[V := v]) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red1'r P t h ({V:T=\<lfloor>v\<rfloor>; e}, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>{V:T=None; e'},(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 2. \<lbrakk>V < length xs; \<not> final e0; \<not> \<tau>move0 P h e0; \<forall>a. e0 \<noteq> Throw a; \<forall>v. e0 \<noteq> Val v; ta_bisim01 ta0 (extTA2J1 P ta); \<not> (call e0 = None \<or> call1 e = None); False,P,t \<turnstile>1 \<langle>e,(h, xs[V := v])\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red1'r P t h ({V:T=\<lfloor>v\<rfloor>; e}, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>{V:T=None; e'},(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 3. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Val u}, xs) (Val u, xs[V := v])
 4. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Throw a}, xs) (Throw a, xs[V := v])
[PROOF STEP]
apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_\<tau>red1r_Some)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>V < length xs; \<not> final e0; \<not> \<tau>move0 P h e0; \<forall>a. e0 \<noteq> Throw a; \<forall>v. e0 \<noteq> Val v; ta_bisim01 ta0 (extTA2J1 P ta); \<not> (call e0 = None \<or> call1 e = None); False,P,t \<turnstile>1 \<langle>e,(h, xs[V := v])\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red1'r P t h ({V:T=\<lfloor>v\<rfloor>; e}, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>{V:T=None; e'},(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 2. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Val u}, xs) (Val u, xs[V := v])
 3. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Throw a}, xs) (Throw a, xs[V := v])
[PROOF STEP]
apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_\<tau>red1r_Some)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Val u}, xs) (Val u, xs[V := v])
 2. V < length xs \<Longrightarrow> \<tau>red1't P t h ({V:T=\<lfloor>v\<rfloor>; Throw a}, xs) (Throw a, xs[V := v])
[PROOF STEP]
apply(fastforce simp add: sim_move01_def intro!: \<tau>red1t_2step[OF Block1Some] \<tau>red1r_1step[OF Block1Some] Red1Block Block1Throw)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move01_preserves_len: "sim_move01 P t ta0 e0 e h xs ta e' h' xs' \<Longrightarrow> length xs' = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_move01 P t ta0 e0 e h xs ta e' h' xs' \<Longrightarrow> length xs' = length xs
[PROOF STEP]
by(fastforce simp add: sim_move01_def split: if_split_asm dest: \<tau>red1r_preserves_len \<tau>red1t_preserves_len red1_preserves_len)


[STATEMENT]
lemma sim_move01_preserves_unmod:
  "\<lbrakk> sim_move01 P t ta0 e0 e h xs ta e' h' xs'; unmod e i; i < length xs \<rbrakk> \<Longrightarrow> xs' ! i = xs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sim_move01 P t ta0 e0 e h xs ta e' h' xs'; unmod e i; i < length xs\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(auto simp add: sim_move01_def split: if_split_asm dest: \<tau>red1t_preserves_unmod)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call e0 = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 2. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 3. \<And>a aa ab ac b ba. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; call e0 = \<lfloor>(a, ab, b)\<rfloor>; call1 e = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule (2) \<tau>red1'r_preserves_unmod)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call e0 = None; xs'' ! i = xs ! i\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 2. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 3. \<And>a aa ab ac b ba. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; call e0 = \<lfloor>(a, ab, b)\<rfloor>; call1 e = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule (1) \<tau>red1r_unmod_preserved)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call e0 = None; xs'' ! i = xs ! i; unmod e'' i\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 2. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 3. \<And>a aa ab ac b ba. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; call e0 = \<lfloor>(a, ab, b)\<rfloor>; call1 e = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule \<tau>red1r_preserves_len)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call e0 = None; xs'' ! i = xs ! i; unmod e'' i; length xs'' = length xs\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 2. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
 3. \<And>a aa ab ac b ba. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; call e0 = \<lfloor>(a, ab, b)\<rfloor>; call1 e = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(auto dest: red1_preserves_unmod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule (2) \<tau>red1'r_preserves_unmod)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None; xs'' ! i = xs ! i\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule (1) \<tau>red1r_unmod_preserved)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None; xs'' ! i = xs ! i; unmod e'' i\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(frule \<tau>red1r_preserves_len)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>e'' xs''. \<lbrakk>unmod e i; i < length xs; \<not> \<tau>move0 P h e0; \<not> final e0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>red1'r P t h (e, xs) (e'', xs''); False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; \<not> \<tau>move1 P h e''; call1 e = None; xs'' ! i = xs ! i; unmod e'' i; length xs'' = length xs\<rbrakk> \<Longrightarrow> xs' ! i = xs ! i
[PROOF STEP]
apply(auto dest: red1_preserves_unmod)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done