[STATEMENT]
lemma sim_move01_expr:
  assumes "sim_move01 P t ta0 e0 e h xs ta e' h' xs'"
  shows
  "sim_move01 P t ta0 (newA T\<lfloor>e0\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs'"
  "sim_move01 P t ta0 (Cast T e0) (Cast T e) h xs ta (Cast T e') h' xs'"
  "sim_move01 P t ta0 (e0 instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs'"
  "sim_move01 P t ta0 (e0 \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs'"
  "sim_move01 P t ta0 (Val v \<guillemotleft>bop\<guillemotright> e0) (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs'"
  "sim_move01 P t ta0 (V := e0) (V' := e) h xs ta (V' := e') h' xs'"
  "sim_move01 P t ta0 (e0\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs'"
  "sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs'"
  "sim_move01 P t ta0 (e0\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs'"
  "sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs'"
  "sim_move01 P t ta0 (AAss (Val v) (Val v') e0) (AAss (Val v) (Val v') e) h xs ta (AAss (Val v) (Val v') e') h' xs'"
  "sim_move01 P t ta0 (e0\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs'"
  "sim_move01 P t ta0 (e0\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs'"
  "sim_move01 P t ta0 (FAss e0 F D e2) (FAss e F' D' e2') h xs ta (FAss e' F' D' e2') h' xs'"
  "sim_move01 P t ta0 (FAss (Val v) F D e0) (FAss (Val v) F' D' e) h xs ta (FAss (Val v) F' D' e') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap e0 D F e2 e3) (CompareAndSwap e D F e2' e3') h xs ta (CompareAndSwap e' D F e2' e3') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap (Val v) D F e0 e3) (CompareAndSwap (Val v) D F e e3') h xs ta (CompareAndSwap (Val v) D F e' e3') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap (Val v) D F (Val v') e0) (CompareAndSwap (Val v) D F (Val v') e) h xs ta (CompareAndSwap (Val v) D F (Val v') e') h' xs'"
  "sim_move01 P t ta0 (e0\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs'"
  "sim_move01 P t ta0 ({V:T=vo; e0}) ({V':T=None; e}) h xs ta ({V':T=None; e'}) h' xs'"
  "sim_move01 P t ta0 (sync(e0) e2) (sync\<^bsub>V'\<^esub>(e) e2') h xs ta (sync\<^bsub>V'\<^esub>(e') e2') h' xs'"
  "sim_move01 P t ta0 (insync(a) e0) (insync\<^bsub>V'\<^esub>(a') e) h xs ta (insync\<^bsub>V'\<^esub>(a') e') h' xs'"
  "sim_move01 P t ta0 (e0;;e2) (e;;e2') h xs ta (e';;e2') h' xs'"
  "sim_move01 P t ta0 (if (e0) e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs'"
  "sim_move01 P t ta0 (throw e0) (throw e) h xs ta (throw e') h' xs'"
  "sim_move01 P t ta0 (try e0 catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((sim_move01 P t ta0 (newA T\<lfloor>e0\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs' &&& sim_move01 P t ta0 (Cast T e0) (Cast T e) h xs ta (Cast T e') h' xs' &&& sim_move01 P t ta0 (e0 instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs') &&& sim_move01 P t ta0 (e0 \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs' &&& sim_move01 P t ta0 (Val v \<guillemotleft>bop\<guillemotright> e0) (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs' &&& sim_move01 P t ta0 (V:=e0) (V':=e) h xs ta (V':=e') h' xs') &&& (sim_move01 P t ta0 (e0\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs' &&& sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs' &&& sim_move01 P t ta0 (e0\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs') &&& (sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs' &&& sim_move01 P t ta0 (Val v\<lfloor>Val v'\<rceil> := e0) (Val v\<lfloor>Val v'\<rceil> := e) h xs ta (Val v\<lfloor>Val v'\<rceil> := e') h' xs') &&& sim_move01 P t ta0 (e0\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs' &&& sim_move01 P t ta0 (e0\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs') &&& ((sim_move01 P t ta0 (e0\<bullet>F{D} := e2) (e\<bullet>F'{D'} := e2') h xs ta (e'\<bullet>F'{D'} := e2') h' xs' &&& sim_move01 P t ta0 (Val v\<bullet>F{D} := e0) (Val v\<bullet>F'{D'} := e) h xs ta (Val v\<bullet>F'{D'} := e') h' xs' &&& sim_move01 P t ta0 (e0\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) (e\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h xs ta (e'\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h' xs') &&& sim_move01 P t ta0 (Val v\<bullet>compareAndSwap(D\<bullet>F, e0, e3)) (Val v\<bullet>compareAndSwap(D\<bullet>F, e, e3')) h xs ta (Val v\<bullet>compareAndSwap(D\<bullet>F, e', e3')) h' xs' &&& sim_move01 P t ta0 (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e0)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e)) h xs ta (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e')) h' xs' &&& sim_move01 P t ta0 (e0\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs') &&& (sim_move01 P t ta0 {V:T=vo; e0} {V':T=None; e} h xs ta {V':T=None; e'} h' xs' &&& sim_move01 P t ta0 (sync(e0) e2) (sync\<^bsub>V'\<^esub> (e) e2') h xs ta (sync\<^bsub>V'\<^esub> (e') e2') h' xs' &&& sim_move01 P t ta0 (insync(a) e0) (insync\<^bsub>V'\<^esub> (a') e) h xs ta (insync\<^bsub>V'\<^esub> (a') e') h' xs') &&& (sim_move01 P t ta0 (e0;; e2) (e;; e2') h xs ta (e';; e2') h' xs' &&& sim_move01 P t ta0 (if (e0) e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs') &&& sim_move01 P t ta0 (throw e0) (throw e) h xs ta (throw e') h' xs' &&& sim_move01 P t ta0 (try e0 catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sim_move01 P t ta0 e0 e h xs ta e' h' xs'

goal (1 subgoal):
 1. (((sim_move01 P t ta0 (newA T\<lfloor>e0\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs' &&& sim_move01 P t ta0 (Cast T e0) (Cast T e) h xs ta (Cast T e') h' xs' &&& sim_move01 P t ta0 (e0 instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs') &&& sim_move01 P t ta0 (e0 \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs' &&& sim_move01 P t ta0 (Val v \<guillemotleft>bop\<guillemotright> e0) (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs' &&& sim_move01 P t ta0 (V:=e0) (V':=e) h xs ta (V':=e') h' xs') &&& (sim_move01 P t ta0 (e0\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs' &&& sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs' &&& sim_move01 P t ta0 (e0\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs') &&& (sim_move01 P t ta0 (Val v\<lfloor>e0\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs' &&& sim_move01 P t ta0 (Val v\<lfloor>Val v'\<rceil> := e0) (Val v\<lfloor>Val v'\<rceil> := e) h xs ta (Val v\<lfloor>Val v'\<rceil> := e') h' xs') &&& sim_move01 P t ta0 (e0\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs' &&& sim_move01 P t ta0 (e0\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs') &&& ((sim_move01 P t ta0 (e0\<bullet>F{D} := e2) (e\<bullet>F'{D'} := e2') h xs ta (e'\<bullet>F'{D'} := e2') h' xs' &&& sim_move01 P t ta0 (Val v\<bullet>F{D} := e0) (Val v\<bullet>F'{D'} := e) h xs ta (Val v\<bullet>F'{D'} := e') h' xs' &&& sim_move01 P t ta0 (e0\<bullet>compareAndSwap(D\<bullet>F, e2, e3)) (e\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h xs ta (e'\<bullet>compareAndSwap(D\<bullet>F, e2', e3')) h' xs') &&& sim_move01 P t ta0 (Val v\<bullet>compareAndSwap(D\<bullet>F, e0, e3)) (Val v\<bullet>compareAndSwap(D\<bullet>F, e, e3')) h xs ta (Val v\<bullet>compareAndSwap(D\<bullet>F, e', e3')) h' xs' &&& sim_move01 P t ta0 (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e0)) (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e)) h xs ta (Val v\<bullet>compareAndSwap(D\<bullet>F, Val v', e')) h' xs' &&& sim_move01 P t ta0 (e0\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs') &&& (sim_move01 P t ta0 {V:T=vo; e0} {V':T=None; e} h xs ta {V':T=None; e'} h' xs' &&& sim_move01 P t ta0 (sync(e0) e2) (sync\<^bsub>V'\<^esub> (e) e2') h xs ta (sync\<^bsub>V'\<^esub> (e') e2') h' xs' &&& sim_move01 P t ta0 (insync(a) e0) (insync\<^bsub>V'\<^esub> (a') e) h xs ta (insync\<^bsub>V'\<^esub> (a') e') h' xs') &&& (sim_move01 P t ta0 (e0;; e2) (e;; e2') h xs ta (e';; e2') h' xs' &&& sim_move01 P t ta0 (if (e0) e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs') &&& sim_move01 P t ta0 (throw e0) (throw e) h xs ta (throw e') h' xs' &&& sim_move01 P t ta0 (try e0 catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'
[PROOF STEP]
apply(simp_all add: sim_move01_def final_iff \<tau>red1r_Val \<tau>red1t_Val split: if_split_asm split del: if_split)
[PROOF STATE]
proof (prove)
goal (78 subgoals):
 1. \<lbrakk>\<tau>move0 P h e0; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (e, xs) (e', xs')\<rbrakk> \<Longrightarrow> \<tau>red1't P t h (newA T\<lfloor>e\<rceil>, xs) (newA T\<lfloor>e'\<rceil>, xs')
 2. \<lbrakk>\<not> \<tau>move0 P h e0; call e0 = None \<or> call1 e = None; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (e, xs) (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 (newA T\<lfloor>e\<rceil>, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 3. \<lbrakk>\<not> \<tau>move0 P h e0; (\<exists>a aa b. call e0 = \<lfloor>(a, aa, b)\<rfloor>) \<and> (\<exists>a aa b. call1 e = \<lfloor>(a, aa, b)\<rfloor>); (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<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> if call e0 = None \<or> call1 e = None then \<exists>e'' xs''. \<tau>red1'r P t h (newA T\<lfloor>e\<rceil>, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>newA T\<lfloor>e\<rceil>,(h, xs)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (newA T\<lfloor>e\<rceil>)
 4. \<lbrakk>\<tau>move0 P h e0; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (e, xs) (e', xs')\<rbrakk> \<Longrightarrow> \<tau>red1't P t h (Cast T e, xs) (Cast T e', xs')
 5. \<lbrakk>\<not> \<tau>move0 P h e0; call e0 = None \<or> call1 e = None; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (e, xs) (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 (Cast T e, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 6. \<lbrakk>\<not> \<tau>move0 P h e0; (\<exists>a aa b. call e0 = \<lfloor>(a, aa, b)\<rfloor>) \<and> (\<exists>a aa b. call1 e = \<lfloor>(a, aa, b)\<rfloor>); (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<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> if call e0 = None \<or> call1 e = None then \<exists>e'' xs''. \<tau>red1'r P t h (Cast T e, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Cast T e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Cast T e)
 7. \<lbrakk>\<tau>move0 P h e0; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (e, xs) (e', xs')\<rbrakk> \<Longrightarrow> \<tau>red1't P t h (e instanceof T, xs) (e' instanceof T, xs')
 8. \<lbrakk>\<not> \<tau>move0 P h e0; call e0 = None \<or> call1 e = None; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (e, xs) (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 (e instanceof T, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''
 9. \<lbrakk>\<not> \<tau>move0 P h e0; (\<exists>a aa b. call e0 = \<lfloor>(a, aa, b)\<rfloor>) \<and> (\<exists>a aa b. call1 e = \<lfloor>(a, aa, b)\<rfloor>); (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<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> if call e0 = None \<or> call1 e = None then \<exists>e'' xs''. \<tau>red1'r P t h (e instanceof T, xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>e instanceof T,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (e instanceof T)
 10. \<lbrakk>\<tau>move0 P h e0; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (e, xs) (e', xs')\<rbrakk> \<Longrightarrow> \<tau>red1't P t h (e \<guillemotleft>bop\<guillemotright> e2', xs) (e' \<guillemotleft>bop\<guillemotright> e2', xs')
A total of 78 subgoals...
[PROOF STEP]
apply(fastforce simp add: final_iff \<tau>red1r_Val \<tau>red1t_Val split!: if_splits intro: red1_reds1.intros)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_moves01_expr:
  "sim_move01 P t ta0 e0 e h xs ta e' h' xs' \<Longrightarrow> sim_moves01 P t ta0 (e0 # es2) (e # es2') h xs ta (e' # es2') h' xs'"
  "sim_moves01 P t ta0 es0 es h xs ta es' h' xs' \<Longrightarrow> sim_moves01 P t ta0 (Val v # es0) (Val v # es) h xs ta (Val v # es') h' xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sim_move01 P t ta0 e0 e h xs ta e' h' xs' \<Longrightarrow> sim_moves01 P t ta0 (e0 # es2) (e # es2') h xs ta (e' # es2') h' xs') &&& (sim_moves01 P t ta0 es0 es h xs ta es' h' xs' \<Longrightarrow> sim_moves01 P t ta0 (Val v # es0) (Val v # es) h xs ta (Val v # es') h' xs')
[PROOF STEP]
apply(simp_all add: sim_move01_def sim_moves01_def final_iff finals_iff Cons_eq_append_conv \<tau>red1t_Val \<tau>red1r_Val split: if_split_asm split del: if_split)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<tau>move0 P h e0; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (e, xs) (e', xs')\<rbrakk> \<Longrightarrow> (\<forall>vs. e0 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e0 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> \<tau>reds1't P t h (e # es2', xs) (e' # es2', xs')
 2. \<lbrakk>\<not> \<tau>move0 P h e0; call e0 = None \<or> call1 e = None; (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> (\<exists>e'' xs''. \<tau>red1'r P t h (e, xs) (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> (\<forall>vs. e0 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e0 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> (if (if is_val e0 then calls es2 else call e0) = None \<or> (if is_val e then calls1 es2' else call1 e) = None then \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es'' else False,P,t \<turnstile>1 \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h (e # es2'))
 3. \<lbrakk>\<not> \<tau>move0 P h e0; (\<exists>a aa b. call e0 = \<lfloor>(a, aa, b)\<rfloor>) \<and> (\<exists>a aa b. call1 e = \<lfloor>(a, aa, b)\<rfloor>); (\<forall>v. e0 \<noteq> Val v) \<and> (\<forall>a. e0 \<noteq> Throw a) \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<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> (\<forall>vs. e0 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e0 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> (if (if is_val e0 then calls es2 else call e0) = None \<or> (if is_val e then calls1 es2' else call1 e) = None then \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es'' else False,P,t \<turnstile>1 \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h (e # es2'))
 4. \<lbrakk>\<tau>moves0 P h es0; (\<forall>vs. es0 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es') \<and> h' = h \<and> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>reds1't P t h (es, xs) (es', xs')\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es0 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es0 \<noteq> ys' @ Throw a # es') \<and> \<tau>reds1't P t h (Val v # es, xs) (Val v # es', xs')
 5. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; (\<forall>vs. es0 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es') \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> (\<exists>es'' xs''. \<tau>reds1'r P t h (es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es'')\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es0 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es0 \<noteq> ys' @ Throw a # es') \<and> (\<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es'')
 6. \<lbrakk>\<not> \<tau>moves0 P h es0; (\<exists>a aa b. calls es0 = \<lfloor>(a, aa, b)\<rfloor>) \<and> (\<exists>a aa b. calls1 es = \<lfloor>(a, aa, b)\<rfloor>); (\<forall>vs. es0 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es') \<and> ta_bisim01 ta0 (extTA2J1 P ta) \<and> False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es0 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es0 \<noteq> ys' @ Throw a # es') \<and> (if calls es0 = None \<or> calls1 es = None then \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es'' else False,P,t \<turnstile>1 \<langle>Val v # es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h (Val v # es))
[PROOF STEP]
apply(auto simp add: Cons_eq_append_conv \<tau>red1t_Val \<tau>red1r_Val split!: if_splits intro: List1Red1 List1Red2 \<tau>red1t_inj_\<tau>reds1t \<tau>red1r_inj_\<tau>reds1r \<tau>reds1t_cons_\<tau>reds1t \<tau>reds1r_cons_\<tau>reds1r)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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''; \<not> is_val e0; call e0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 3. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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; \<not> is_val e0; call e0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 4. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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''; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 5. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls es0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 6. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>red1r_inj_\<tau>reds1r List1Red1)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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; \<not> is_val e0; call e0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 3. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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''; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 4. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls es0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 5. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>red1r_inj_\<tau>reds1r List1Red1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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; \<not> is_val e0; call e0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 2. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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''; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls es0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 4. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>red1r_inj_\<tau>reds1r List1Red1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move0 P h e0; \<forall>v. e0 \<noteq> Val v; \<forall>a. e0 \<noteq> Throw a; 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''; \<not> is_val e; call1 e = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (e # es2', xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls es0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>red1r_inj_\<tau>reds1r List1Red1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls es0 = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>reds1r_cons_\<tau>reds1r intro!: List1Red2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; \<forall>vs. es0 \<noteq> map Val vs; \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; calls1 es = None\<rbrakk> \<Longrightarrow> \<exists>es'' xs''. \<tau>reds1'r P t h (Val v # es, xs) (es'', xs'') \<and> False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> \<not> \<tau>moves1 P h es''
[PROOF STEP]
apply(force elim!: \<tau>reds1r_cons_\<tau>reds1r intro!: List1Red2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_move01_CallParams:
  "sim_moves01 P t ta0 es0 es h xs ta es' h' xs'
  \<Longrightarrow> sim_move01 P t ta0 (Val v\<bullet>M(es0)) (Val v\<bullet>M(es)) h xs ta (Val v\<bullet>M(es')) h' xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_moves01 P t ta0 es0 es h xs ta es' h' xs' \<Longrightarrow> sim_move01 P t ta0 (Val v\<bullet>M(es0)) (Val v\<bullet>M(es)) h xs ta (Val v\<bullet>M(es')) h' xs'
[PROOF STEP]
apply(clarsimp simp add: sim_move01_def sim_moves01_def \<tau>reds1r_map_Val \<tau>reds1t_map_Val is_vals_conv split: if_split_asm split del: if_split)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<tau>moves0 P h es0; \<not> finals es0; h' = h; ta0 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>reds1't P t h (es, xs) (es', xs')\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs')
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
 3. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce simp add: sim_move01_def sim_moves01_def \<tau>reds1r_map_Val \<tau>reds1t_map_Val intro: Call_\<tau>red1r_param Call1Params)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI, fastforce)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es)))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(split if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> ((\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs')) \<and> (\<not> ((\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs')
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> \<not> ((\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es)))
 3. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(clarsimp simp add: finals_iff)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''\<rbrakk> \<Longrightarrow> \<not> ((\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es)))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(clarify)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(split if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> (call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None \<longrightarrow> (\<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'')) \<and> (\<not> (call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None) \<longrightarrow> False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es)))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None \<longrightarrow> (\<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'')
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> \<not> (call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None) \<longrightarrow> False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))
 3. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(simp del: call.simps calls.simps call1.simps calls1.simps)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; (\<forall>vs. es0 \<noteq> map Val vs) \<or> v \<noteq> Null \<and> (\<exists>T. typeof\<^bsub>h\<^esub> v = \<lfloor>T\<rfloor> \<and> (\<exists>C. class_type_of' T = \<lfloor>C\<rfloor> \<and> (\<exists>Ts Tr D. P \<turnstile> C sees M: Ts\<rightarrow>Tr = Native in D \<and> \<not> \<tau>external_defs D M))); \<forall>vs a es'. es0 \<noteq> map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> (call (Val v\<bullet>M(es0)) = None \<longrightarrow> (\<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'')) \<and> (call1 (Val v\<bullet>M(es)) = None \<longrightarrow> (\<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e''))
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> \<not> (call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None) \<longrightarrow> False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))
 3. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce simp add: sim_move01_def sim_moves01_def \<tau>red1r_Val \<tau>red1t_Val \<tau>reds1r_map_Val_Throw intro: Call_\<tau>red1r_param Call1Params split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = None \<or> calls1 es = None; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); \<tau>reds1'r P t h (es, xs) (es'', xs''); False,P,t \<turnstile>1 \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es''; \<not> ((\<exists>vs. es0 = map Val vs) \<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))))); \<nexists>vs a es'. es0 = map Val vs @ Throw a # es'\<rbrakk> \<Longrightarrow> \<not> (call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None) \<longrightarrow> False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))
 2. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce split: if_split_asm simp add: is_vals_conv \<tau>reds1r_map_Val \<tau>reds1r_map_Val_Throw)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> \<not> final (Val v\<bullet>M(es0)) \<and> (if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI, fastforce)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa ab ac b ba. \<lbrakk>\<not> \<tau>moves0 P h es0; calls es0 = \<lfloor>(a, ab, b)\<rfloor>; calls1 es = \<lfloor>(aa, ac, ba)\<rfloor>; \<not> finals es0; ta_bisim01 ta0 (extTA2J1 P ta); False,P,t \<turnstile>1 \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<not> \<tau>moves1 P h es\<rbrakk> \<Longrightarrow> if (\<exists>vs a es'. es0 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es0 = map Val vs) \<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> ta0 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> \<and> \<tau>red1't P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') else ta_bisim01 ta0 (extTA2J1 P ta) \<and> (if call (Val v\<bullet>M(es0)) = None \<or> call1 (Val v\<bullet>M(es)) = None then \<exists>e'' xs''. \<tau>red1'r P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> False,P,t \<turnstile>1 \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h e'' else False,P,t \<turnstile>1 \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> \<not> \<tau>move1 P h (Val v\<bullet>M(es)))
[PROOF STEP]
apply(fastforce simp add: sim_move01_def sim_moves01_def \<tau>red1r_Val \<tau>red1t_Val \<tau>reds1t_map_Val \<tau>reds1r_map_Val is_vals_conv intro: Call_\<tau>red1r_param Call1Params split: if_split_asm)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done