[STATEMENT]
lemma sim_move10_expr:
  assumes "sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs'"
  shows
  "sim_move10 P t ta1 (newA T\<lfloor>e1\<rceil>) (newA T\<lfloor>e1'\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs'"
  "sim_move10 P t ta1 (Cast T e1) (Cast T e1') (Cast T e) h xs ta (Cast T e') h' xs'"
  "sim_move10 P t ta1 (e1 instanceof T) (e1' instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs'"
  "sim_move10 P t ta1 (e1 \<guillemotleft>bop\<guillemotright> e2) (e1' \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs'"
  "sim_move10 P t ta1 (Val v \<guillemotleft>bop\<guillemotright> e1) (Val v \<guillemotleft>bop\<guillemotright> e1') (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs'"
  "sim_move10 P t ta1 (V := e1) (V := e1') (V' := e) h xs ta (V' := e') h' xs'"
  "sim_move10 P t ta1 (e1\<lfloor>e2\<rceil>) (e1'\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs'"
  "sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil>) (Val v\<lfloor>e1'\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs'"
  "sim_move10 P t ta1 (e1\<lfloor>e2\<rceil> := e3) (e1'\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs'"
  "sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil> := e3) (Val v\<lfloor>e1'\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs'"
  "sim_move10 P t ta1 (AAss (Val v) (Val v') e1) (AAss (Val v) (Val v') e1') (AAss (Val v) (Val v') e) h xs ta (AAss (Val v) (Val v') e') h' xs'"
  "sim_move10 P t ta1 (e1\<bullet>length) (e1'\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs'"
  "sim_move10 P t ta1 (e1\<bullet>F{D}) (e1'\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs'"
  "sim_move10 P t ta1 (FAss e1 F D e2) (FAss e1' F D e2) (FAss e F' D' e2') h xs ta (FAss e' F' D' e2') h' xs'"
  "sim_move10 P t ta1 (FAss (Val v) F D e1) (FAss (Val v) F D e1') (FAss (Val v) F' D' e) h xs ta (FAss (Val v) F' D' e') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap e1 F D e2 e3) (CompareAndSwap e1' F D e2 e3) (CompareAndSwap e F' D' e2' e3') h xs ta (CompareAndSwap e' F' D' e2' e3') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap (Val v) F D e1 e3) (CompareAndSwap (Val v) F D e1' e3) (CompareAndSwap (Val v) F' D' e e3') h xs ta (CompareAndSwap (Val v) F' D' e' e3') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap (Val v) F D (Val v') e1) (CompareAndSwap (Val v) F D (Val v') e1') (CompareAndSwap (Val v) F' D' (Val v') e) h xs ta (CompareAndSwap (Val v) F' D' (Val v') e') h' xs'"
  "sim_move10 P t ta1 (e1\<bullet>M(es)) (e1'\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs'"
  "sim_move10 P t ta1 (sync\<^bsub>V\<^esub>(e1) e2) (sync\<^bsub>V\<^esub>(e1') e2) (sync(e) e2') h xs ta (sync(e') e2') h' xs'"
  "sim_move10 P t ta1 (insync\<^bsub>V\<^esub>(a) e1) (insync\<^bsub>V\<^esub>(a) e1') (insync(a') e) h xs ta (insync(a') e') h' xs'"
  "sim_move10 P t ta1 (e1;;e2) (e1';;e2) (e;;e2') h xs ta (e';;e2') h' xs'"
  "sim_move10 P t ta1 (if (e1) e2 else e3) (if (e1') e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs'"
  "sim_move10 P t ta1 (throw e1) (throw e1') (throw e) h xs ta (throw e') h' xs'"
  "sim_move10 P t ta1 (try e1 catch(C V) e2) (try e1' 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_move10 P t ta1 (newA T\<lfloor>e1\<rceil>) (newA T\<lfloor>e1'\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs' &&& sim_move10 P t ta1 (Cast T e1) (Cast T e1') (Cast T e) h xs ta (Cast T e') h' xs' &&& sim_move10 P t ta1 (e1 instanceof T) (e1' instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs') &&& sim_move10 P t ta1 (e1 \<guillemotleft>bop\<guillemotright> e2) (e1' \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs' &&& sim_move10 P t ta1 (Val v \<guillemotleft>bop\<guillemotright> e1) (Val v \<guillemotleft>bop\<guillemotright> e1') (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs' &&& sim_move10 P t ta1 (V:=e1) (V:=e1') (V':=e) h xs ta (V':=e') h' xs') &&& (sim_move10 P t ta1 (e1\<lfloor>e2\<rceil>) (e1'\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs' &&& sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil>) (Val v\<lfloor>e1'\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs' &&& sim_move10 P t ta1 (e1\<lfloor>e2\<rceil> := e3) (e1'\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs') &&& sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil> := e3) (Val v\<lfloor>e1'\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs' &&& sim_move10 P t ta1 (Val v\<lfloor>Val v'\<rceil> := e1) (Val v\<lfloor>Val v'\<rceil> := e1') (Val v\<lfloor>Val v'\<rceil> := e) h xs ta (Val v\<lfloor>Val v'\<rceil> := e') h' xs' &&& sim_move10 P t ta1 (e1\<bullet>length) (e1'\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs') &&& ((sim_move10 P t ta1 (e1\<bullet>F{D}) (e1'\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs' &&& sim_move10 P t ta1 (e1\<bullet>F{D} := e2) (e1'\<bullet>F{D} := e2) (e\<bullet>F'{D'} := e2') h xs ta (e'\<bullet>F'{D'} := e2') h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>F{D} := e1) (Val v\<bullet>F{D} := e1') (Val v\<bullet>F'{D'} := e) h xs ta (Val v\<bullet>F'{D'} := e') h' xs') &&& sim_move10 P t ta1 (e1\<bullet>compareAndSwap(F\<bullet>D, e2, e3)) (e1'\<bullet>compareAndSwap(F\<bullet>D, e2, e3)) (e\<bullet>compareAndSwap(F'\<bullet>D', e2', e3')) h xs ta (e'\<bullet>compareAndSwap(F'\<bullet>D', e2', e3')) h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>compareAndSwap(F\<bullet>D, e1, e3)) (Val v\<bullet>compareAndSwap(F\<bullet>D, e1', e3)) (Val v\<bullet>compareAndSwap(F'\<bullet>D', e, e3')) h xs ta (Val v\<bullet>compareAndSwap(F'\<bullet>D', e', e3')) h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>compareAndSwap(F\<bullet>D, Val v', e1)) (Val v\<bullet>compareAndSwap(F\<bullet>D, Val v', e1')) (Val v\<bullet>compareAndSwap(F'\<bullet>D', Val v', e)) h xs ta (Val v\<bullet>compareAndSwap(F'\<bullet>D', Val v', e')) h' xs') &&& (sim_move10 P t ta1 (e1\<bullet>M(es)) (e1'\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs' &&& sim_move10 P t ta1 (sync\<^bsub>V\<^esub> (e1) e2) (sync\<^bsub>V\<^esub> (e1') e2) (sync(e) e2') h xs ta (sync(e') e2') h' xs' &&& sim_move10 P t ta1 (insync\<^bsub>V\<^esub> (a) e1) (insync\<^bsub>V\<^esub> (a) e1') (insync(a') e) h xs ta (insync(a') e') h' xs') &&& (sim_move10 P t ta1 (e1;; e2) (e1';; e2) (e;; e2') h xs ta (e';; e2') h' xs' &&& sim_move10 P t ta1 (if (e1) e2 else e3) (if (e1') e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs') &&& sim_move10 P t ta1 (throw e1) (throw e1') (throw e) h xs ta (throw e') h' xs' &&& sim_move10 P t ta1 (try e1 catch(C V) e2) (try e1' 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_move10 P t ta1 e1 e1' e h xs ta e' h' xs'

goal (1 subgoal):
 1. (((sim_move10 P t ta1 (newA T\<lfloor>e1\<rceil>) (newA T\<lfloor>e1'\<rceil>) (newA T\<lfloor>e\<rceil>) h xs ta (newA T\<lfloor>e'\<rceil>) h' xs' &&& sim_move10 P t ta1 (Cast T e1) (Cast T e1') (Cast T e) h xs ta (Cast T e') h' xs' &&& sim_move10 P t ta1 (e1 instanceof T) (e1' instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs') &&& sim_move10 P t ta1 (e1 \<guillemotleft>bop\<guillemotright> e2) (e1' \<guillemotleft>bop\<guillemotright> e2) (e \<guillemotleft>bop\<guillemotright> e2') h xs ta (e' \<guillemotleft>bop\<guillemotright> e2') h' xs' &&& sim_move10 P t ta1 (Val v \<guillemotleft>bop\<guillemotright> e1) (Val v \<guillemotleft>bop\<guillemotright> e1') (Val v \<guillemotleft>bop\<guillemotright> e) h xs ta (Val v \<guillemotleft>bop\<guillemotright> e') h' xs' &&& sim_move10 P t ta1 (V:=e1) (V:=e1') (V':=e) h xs ta (V':=e') h' xs') &&& (sim_move10 P t ta1 (e1\<lfloor>e2\<rceil>) (e1'\<lfloor>e2\<rceil>) (e\<lfloor>e2'\<rceil>) h xs ta (e'\<lfloor>e2'\<rceil>) h' xs' &&& sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil>) (Val v\<lfloor>e1'\<rceil>) (Val v\<lfloor>e\<rceil>) h xs ta (Val v\<lfloor>e'\<rceil>) h' xs' &&& sim_move10 P t ta1 (e1\<lfloor>e2\<rceil> := e3) (e1'\<lfloor>e2\<rceil> := e3) (e\<lfloor>e2'\<rceil> := e3') h xs ta (e'\<lfloor>e2'\<rceil> := e3') h' xs') &&& sim_move10 P t ta1 (Val v\<lfloor>e1\<rceil> := e3) (Val v\<lfloor>e1'\<rceil> := e3) (Val v\<lfloor>e\<rceil> := e3') h xs ta (Val v\<lfloor>e'\<rceil> := e3') h' xs' &&& sim_move10 P t ta1 (Val v\<lfloor>Val v'\<rceil> := e1) (Val v\<lfloor>Val v'\<rceil> := e1') (Val v\<lfloor>Val v'\<rceil> := e) h xs ta (Val v\<lfloor>Val v'\<rceil> := e') h' xs' &&& sim_move10 P t ta1 (e1\<bullet>length) (e1'\<bullet>length) (e\<bullet>length) h xs ta (e'\<bullet>length) h' xs') &&& ((sim_move10 P t ta1 (e1\<bullet>F{D}) (e1'\<bullet>F{D}) (e\<bullet>F'{D'}) h xs ta (e'\<bullet>F'{D'}) h' xs' &&& sim_move10 P t ta1 (e1\<bullet>F{D} := e2) (e1'\<bullet>F{D} := e2) (e\<bullet>F'{D'} := e2') h xs ta (e'\<bullet>F'{D'} := e2') h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>F{D} := e1) (Val v\<bullet>F{D} := e1') (Val v\<bullet>F'{D'} := e) h xs ta (Val v\<bullet>F'{D'} := e') h' xs') &&& sim_move10 P t ta1 (e1\<bullet>compareAndSwap(F\<bullet>D, e2, e3)) (e1'\<bullet>compareAndSwap(F\<bullet>D, e2, e3)) (e\<bullet>compareAndSwap(F'\<bullet>D', e2', e3')) h xs ta (e'\<bullet>compareAndSwap(F'\<bullet>D', e2', e3')) h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>compareAndSwap(F\<bullet>D, e1, e3)) (Val v\<bullet>compareAndSwap(F\<bullet>D, e1', e3)) (Val v\<bullet>compareAndSwap(F'\<bullet>D', e, e3')) h xs ta (Val v\<bullet>compareAndSwap(F'\<bullet>D', e', e3')) h' xs' &&& sim_move10 P t ta1 (Val v\<bullet>compareAndSwap(F\<bullet>D, Val v', e1)) (Val v\<bullet>compareAndSwap(F\<bullet>D, Val v', e1')) (Val v\<bullet>compareAndSwap(F'\<bullet>D', Val v', e)) h xs ta (Val v\<bullet>compareAndSwap(F'\<bullet>D', Val v', e')) h' xs') &&& (sim_move10 P t ta1 (e1\<bullet>M(es)) (e1'\<bullet>M(es)) (e\<bullet>M(es')) h xs ta (e'\<bullet>M(es')) h' xs' &&& sim_move10 P t ta1 (sync\<^bsub>V\<^esub> (e1) e2) (sync\<^bsub>V\<^esub> (e1') e2) (sync(e) e2') h xs ta (sync(e') e2') h' xs' &&& sim_move10 P t ta1 (insync\<^bsub>V\<^esub> (a) e1) (insync\<^bsub>V\<^esub> (a) e1') (insync(a') e) h xs ta (insync(a') e') h' xs') &&& (sim_move10 P t ta1 (e1;; e2) (e1';; e2) (e;; e2') h xs ta (e';; e2') h' xs' &&& sim_move10 P t ta1 (if (e1) e2 else e3) (if (e1') e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs') &&& sim_move10 P t ta1 (throw e1) (throw e1') (throw e) h xs ta (throw e') h' xs' &&& sim_move10 P t ta1 (try e1 catch(C V) e2) (try e1' 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_move10_def final_iff split del: if_split split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (75 subgoals):
 1. \<lbrakk>\<tau>move1 P h e1; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> \<tau>red0t (extTA2J0 P) P t h (newA T\<lfloor>e\<rceil>, xs) (newA T\<lfloor>e'\<rceil>, xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs
 2. \<lbrakk>\<not> \<tau>move1 P h e1; call e = None \<or> call1 e1 = None; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> (\<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'')\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (newA T\<lfloor>e\<rceil>, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 3. \<lbrakk>\<not> \<tau>move1 P h e1; (\<exists>y. call e = \<lfloor>y\<rfloor>) \<and> (\<exists>y. call1 e1 = \<lfloor>y\<rfloor>); (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> extTA2J0 P,P,t \<turnstile> \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> if call e = None \<or> call1 e1 = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (newA T\<lfloor>e\<rceil>, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>newA T\<lfloor>e\<rceil>,(h, xs)\<rangle> -ta\<rightarrow> \<langle>newA T\<lfloor>e'\<rceil>,(h', xs')\<rangle> \<and> no_call P h (newA T\<lfloor>e\<rceil>) \<and> \<not> \<tau>move0 P h (newA T\<lfloor>e\<rceil>)
 4. \<lbrakk>\<tau>move1 P h e1; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> \<tau>red0t (extTA2J0 P) P t h (Cast T e, xs) (Cast T e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs
 5. \<lbrakk>\<not> \<tau>move1 P h e1; call e = None \<or> call1 e1 = None; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> (\<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'')\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Cast T e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 6. \<lbrakk>\<not> \<tau>move1 P h e1; (\<exists>y. call e = \<lfloor>y\<rfloor>) \<and> (\<exists>y. call1 e1 = \<lfloor>y\<rfloor>); (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> extTA2J0 P,P,t \<turnstile> \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> if call e = None \<or> call1 e1 = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Cast T e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Cast T e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>Cast T e',(h', xs')\<rangle> \<and> no_call P h (Cast T e) \<and> \<not> \<tau>move0 P h (Cast T e)
 7. \<lbrakk>\<tau>move1 P h e1; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> \<tau>red0t (extTA2J0 P) P t h (e instanceof T, xs) (e' instanceof T, xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs
 8. \<lbrakk>\<not> \<tau>move1 P h e1; call e = None \<or> call1 e1 = None; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> (\<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'')\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e instanceof T, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 9. \<lbrakk>\<not> \<tau>move1 P h e1; (\<exists>y. call e = \<lfloor>y\<rfloor>) \<and> (\<exists>y. call1 e1 = \<lfloor>y\<rfloor>); (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> extTA2J0 P,P,t \<turnstile> \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> if call e = None \<or> call1 e1 = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e instanceof T, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>e instanceof T,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e' instanceof T,(h', xs')\<rangle> \<and> no_call P h (e instanceof T) \<and> \<not> \<tau>move0 P h (e instanceof T)
 10. \<lbrakk>\<tau>move1 P h e1; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> \<tau>red0t (extTA2J0 P) P t h (e \<guillemotleft>bop\<guillemotright> e2', xs) (e' \<guillemotleft>bop\<guillemotright> e2', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs
A total of 75 subgoals...
[PROOF STEP]
apply(fastforce simp: \<tau>red0t_Val \<tau>red0r_Val intro: red_reds.intros split!: if_splits)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sim_moves10_expr:
  "sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs' \<Longrightarrow> sim_moves10 P t ta1 (e1 # es2) (e1' # es2) (e # es2') h xs ta (e' # es2') h' xs'"
  "sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs' \<Longrightarrow> sim_moves10 P t ta1 (Val v # es1) (Val v # es1') (Val v # es) h xs ta (Val v # es') h' xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs' \<Longrightarrow> sim_moves10 P t ta1 (e1 # es2) (e1' # es2) (e # es2') h xs ta (e' # es2') h' xs') &&& (sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs' \<Longrightarrow> sim_moves10 P t ta1 (Val v # es1) (Val v # es1') (Val v # es) h xs ta (Val v # es') h' xs')
[PROOF STEP]
unfolding sim_moves10_def sim_move10_def final_iff finals_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> ((\<exists>v. e1 = Val v) \<or> (\<exists>a. e1 = Throw a)) \<and> (if \<tau>move1 P h e1 then (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if call e = None \<or> call1 e1 = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e)) \<Longrightarrow> \<not> ((\<exists>vs. e1 # es2 = map Val vs) \<or> (\<exists>vs a es'. e1 # es2 = map Val vs @ Throw a # es')) \<and> (if \<tau>moves1 P h (e1 # es2) then (\<tau>reds0t (extTA2J0 P) P t h (e # es2', xs) (e' # es2', xs') \<or> countInitBlocks (e1' # es2) < countInitBlocks (e1 # es2) \<and> e' # es2' = e # es2' \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if calls (e # es2') = None \<or> calls1 (e1 # es2) = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (e # es2', xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h (e # es2') \<and> \<not> \<tau>moves0 P h (e # es2')))) &&& (\<not> ((\<exists>vs. es1 = map Val vs) \<or> (\<exists>vs a es'. es1 = map Val vs @ Throw a # es')) \<and> (if \<tau>moves1 P h es1 then (\<tau>reds0t (extTA2J0 P) P t h (es, xs) (es', xs') \<or> countInitBlocks es1' < countInitBlocks es1 \<and> es' = es \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if calls es = None \<or> calls1 es1 = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> no_calls P h es \<and> \<not> \<tau>moves0 P h es)) \<Longrightarrow> \<not> ((\<exists>vs. Val v # es1 = map Val vs) \<or> (\<exists>vs a es'. Val v # es1 = map Val vs @ Throw a # es')) \<and> (if \<tau>moves1 P h (Val v # es1) then (\<tau>reds0t (extTA2J0 P) P t h (Val v # es, xs) (Val v # es', xs') \<or> countInitBlocks (Val v # es1') < countInitBlocks (Val v # es1) \<and> Val v # es' = Val v # es \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace> else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if calls (Val v # es) = None \<or> calls1 (Val v # es1) = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (Val v # es, xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v # es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> no_calls P h (Val v # es) \<and> \<not> \<tau>moves0 P h (Val v # es))))
[PROOF STEP]
apply(simp_all add: Cons_eq_append_conv split del: if_split split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>\<tau>move1 P h e1; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> (\<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>vs. e1 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e1 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> (\<tau>reds0t (extTA2J0 P) P t h (e # es2', xs) (e' # es2', xs') \<or> countInitBlock e1' < countInitBlock e1 \<and> e' = e \<and> xs' = xs)
 2. \<lbrakk>\<not> \<tau>move1 P h e1; call e = None \<or> call1 e1 = None; (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> (\<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'')\<rbrakk> \<Longrightarrow> (\<forall>vs. e1 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e1 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> (if (if is_val e then calls es2' else call e) = None \<or> (if is_val e1 then calls1 es2 else call1 e1) = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (e # es2', xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h (e # es2') \<and> \<not> \<tau>moves0 P h (e # es2'))
 3. \<lbrakk>\<not> \<tau>move1 P h e1; (\<exists>y. call e = \<lfloor>y\<rfloor>) \<and> (\<exists>y. call1 e1 = \<lfloor>y\<rfloor>); (\<forall>v. e1 \<noteq> Val v) \<and> (\<forall>a. e1 \<noteq> Throw a) \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> extTA2J0 P,P,t \<turnstile> \<langle>e,(h, xs)\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle> \<and> no_call P h e \<and> \<not> \<tau>move0 P h e\<rbrakk> \<Longrightarrow> (\<forall>vs. e1 # es2 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. e1 # ys' = map Val vs \<longrightarrow> es2 \<noteq> ys' @ Throw a # es') \<and> (if (if is_val e then calls es2' else call e) = None \<or> (if is_val e1 then calls1 es2 else call1 e1) = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (e # es2', xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h (e # es2') \<and> \<not> \<tau>moves0 P h (e # es2'))
 4. \<lbrakk>\<tau>moves1 P h es1; (\<forall>vs. es1 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es') \<and> (\<tau>reds0t (extTA2J0 P) P t h (es, xs) (es', xs') \<or> countInitBlocks es1' < countInitBlocks es1 \<and> es' = es \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es1 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es1 \<noteq> ys' @ Throw a # es') \<and> (\<tau>reds0t (extTA2J0 P) P t h (Val v # es, xs) (Val v # es', xs') \<or> countInitBlocks es1' < countInitBlocks es1 \<and> es' = es \<and> xs' = xs)
 5. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; (\<forall>vs. es1 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es') \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> (\<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'')\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es1 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es1 \<noteq> ys' @ Throw a # es') \<and> (\<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (Val v # es, xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'')
 6. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); (\<forall>vs. es1 \<noteq> map Val vs) \<and> (\<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es') \<and> ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1) \<and> extTA2J0 P,P,t \<turnstile> \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle> \<and> no_calls P h es \<and> \<not> \<tau>moves0 P h es\<rbrakk> \<Longrightarrow> (\<forall>vs. Val v # es1 \<noteq> map Val vs) \<and> (\<forall>vs a es' ys'. Val v # ys' = map Val vs \<longrightarrow> es1 \<noteq> ys' @ Throw a # es') \<and> (if calls es = None \<or> calls1 es1 = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (Val v # es, xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v # es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>Val v # es',(h', xs')\<rangle> \<and> no_calls P h (Val v # es) \<and> \<not> \<tau>moves0 P h (Val v # es))
[PROOF STEP]
apply(safe intro!: if_split)
[PROOF STATE]
proof (prove)
goal (30 subgoals):
 1. \<And>vs z zs. \<lbrakk>\<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs'); es2 = map Val zs; e1 = Val z\<rbrakk> \<Longrightarrow> False
 2. \<And>vs a es' ys' z zs. \<lbrakk>\<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs'); e1 = Val z; es2 = map Val zs @ Throw a # es'\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<tau>move1 P h e1; \<forall>v. e1 \<noteq> Val v; \<forall>a. e1 \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs'); \<not> \<tau>reds0t (extTA2J0 P) P t h (e # es2', xs) (e' # es2', xs')\<rbrakk> \<Longrightarrow> countInitBlock e1' < countInitBlock e1
 4. \<lbrakk>\<tau>move1 P h e1; \<forall>v. e1 \<noteq> Val v; \<forall>a. e1 \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs'); \<not> \<tau>reds0t (extTA2J0 P) P t h (e # es2', xs) (e' # es2', xs')\<rbrakk> \<Longrightarrow> e' = e
 5. \<lbrakk>\<tau>move1 P h e1; \<forall>v. e1 \<noteq> Val v; \<forall>a. e1 \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; \<tau>red0t (extTA2J0 P) P t h (e, xs) (e', xs'); \<not> \<tau>reds0t (extTA2J0 P) P t h (e # es2', xs) (e' # es2', xs')\<rbrakk> \<Longrightarrow> xs' = xs
 6. \<And>vs z zs. \<lbrakk>\<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; countInitBlock e1' < countInitBlock (Val z); xs' = xs; e' = e; es2 = map Val zs; e1 = Val z\<rbrakk> \<Longrightarrow> False
 7. \<And>vs a es' ys' z zs. \<lbrakk>\<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; h' = h; ta1 = \<lbrace>\<rbrace>; ta = \<lbrace>\<rbrace>; countInitBlock e1' < countInitBlock (Val z); xs' = xs; e' = e; e1 = Val z; es2 = map Val zs @ Throw a # es'\<rbrakk> \<Longrightarrow> False
 8. \<And>e'' xs'' vs z zs. \<lbrakk>\<not> \<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call e = None; es2 = map Val zs; e1 = Val z\<rbrakk> \<Longrightarrow> False
 9. \<And>e'' xs'' vs a es' ys' z zs. \<lbrakk>\<not> \<tau>move1 P h (Val z); \<forall>v. Val z \<noteq> Val v; \<forall>a. Val z \<noteq> Throw a; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call e = None; e1 = Val z; es2 = map Val zs @ Throw a # es'\<rbrakk> \<Longrightarrow> False
 10. \<And>e'' xs''. \<lbrakk>\<not> \<tau>move1 P h e1; \<forall>v. e1 \<noteq> Val v; \<forall>a. e1 \<noteq> Throw a; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>red0r (extTA2J0 P) P t h (e, xs) (e'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>e',(h', xs')\<rangle>; no_call P h e''; \<not> \<tau>move0 P h e''; call e = None\<rbrakk> \<Longrightarrow> if (if is_val e then calls es2' else call e) = None \<or> (if is_val e1 then calls1 es2 else call1 e1) = None then \<exists>es'' xs''. \<tau>reds0r (extTA2J0 P) P t h (e # es2', xs) (es'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h es'' \<and> \<not> \<tau>moves0 P h es'' else extTA2J0 P,P,t \<turnstile> \<langle>e # es2',(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>e' # es2',(h', xs')\<rangle> \<and> no_calls P h (e # es2') \<and> \<not> \<tau>moves0 P h (e # es2')
A total of 30 subgoals...
[PROOF STEP]
apply(fastforce simp add: is_vals_conv \<tau>reds0t_map_Val \<tau>reds0r_map_Val \<tau>red0t_Val \<tau>red0r_Val intro!: \<tau>red0r_inj_\<tau>reds0r \<tau>reds0r_cons_\<tau>reds0r \<tau>red0t_inj_\<tau>reds0t \<tau>reds0t_cons_\<tau>reds0t ListRed1 ListRed2 split: if_split_asm)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done