[STATEMENT]
lemma sim_move10_CallParams:
  "sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs'
  \<Longrightarrow> sim_move10 P t ta1 (Val v\<bullet>M(es1)) (Val v\<bullet>M(es1')) (Val v\<bullet>M(es)) h xs ta (Val v\<bullet>M(es')) h' xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs' \<Longrightarrow> sim_move10 P t ta1 (Val v\<bullet>M(es1)) (Val v\<bullet>M(es1')) (Val v\<bullet>M(es)) h xs ta (Val v\<bullet>M(es')) h' xs'
[PROOF STEP]
unfolding sim_move10_def sim_moves10_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> finals es1 \<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> final (Val v\<bullet>M(es1)) \<and> (if \<tau>move1 P h (Val v\<bullet>M(es1)) then (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(simp split: if_split_asm split del: if_split add: is_vals_conv)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<tau>moves1 P h es1; \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlocks es1' < countInitBlocks es1 \<and> es' = es \<and> xs' = xs)
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce simp add: \<tau>red0t_Val \<tau>red0r_Val \<tau>reds0t_map_Val \<tau>reds0r_map_Val intro: Call_\<tau>red0r_param Call_\<tau>red0t_param CallParams split: if_split_asm split del: if_split intro!: if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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> if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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> if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule if_intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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''); (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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))))\<rbrakk> \<Longrightarrow> (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(es) \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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''); \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1 \<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''); \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(clarsimp split del: if_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''\<rbrakk> \<Longrightarrow> if (if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule if_intro)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(clarsimp split: if_split_asm simp add: is_vals_conv)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>es'' xs'' vs a. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (map Val vs, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<forall>vs. es1 \<noteq> map Val vs; es = map Val vs; v = Addr a; calls1 es1 = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (addr a\<bullet>M(map Val vs), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>addr a\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 4. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule exI conjI)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>es'' xs'' vs a. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (map Val vs, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<forall>vs. es1 \<noteq> map Val vs; es = map Val vs; v = Addr a; calls1 es1 = None\<rbrakk> \<Longrightarrow> \<tau>red0r (extTA2J0 P) P t h (addr a\<bullet>M(map Val vs), xs) (?e''250 es'' xs'' vs a, ?xs''252 es'' xs'' vs a)
 2. \<And>es'' xs'' vs a. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (map Val vs, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<forall>vs. es1 \<noteq> map Val vs; es = map Val vs; v = Addr a; calls1 es1 = None\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>?e''250 es'' xs'' vs a,(h, ?xs''252 es'' xs'' vs a)\<rangle> -ta\<rightarrow> \<langle>addr a\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (?e''250 es'' xs'' vs a) \<and> \<not> \<tau>move0 P h (?e''250 es'' xs'' vs a)
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 4. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 5. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(erule Call_\<tau>red0r_param)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>es'' xs'' vs a. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (map Val vs, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<forall>vs. es1 \<noteq> map Val vs; es = map Val vs; v = Addr a; calls1 es1 = None\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>addr a\<bullet>M(es''),(h, xs'')\<rangle> -ta\<rightarrow> \<langle>addr a\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (addr a\<bullet>M(es'')) \<and> \<not> \<tau>move0 P h (addr a\<bullet>M(es''))
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 4. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce intro: CallParams)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule exI conjI)+
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (?e''302 es'' xs'', ?xs''304 es'' xs'')
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>?e''302 es'' xs'',(h, ?xs''304 es'' xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (?e''302 es'' xs'') \<and> \<not> \<tau>move0 P h (?e''302 es'' xs'')
 3. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 4. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(erule Call_\<tau>red0r_param)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); calls es = None \<or> calls1 es1 = None\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es''),(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es'')) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es''))
 2. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 3. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(fastforce intro!: CallParams)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>es'' xs''. \<lbrakk>\<not> \<tau>moves1 P h es1; calls es = None \<or> calls1 es1 = None; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, body). compE1 (this # pns) body) P) ta1); \<tau>reds0r (extTA2J0 P) P t h (es, xs) (es'', xs''); extTA2J0 P,P,t \<turnstile> \<langle>es'',(h, xs'')\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es''; \<not> \<tau>moves0 P h es''; \<not> ((if is_vals es \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es = map Val vs)\<rfloor> else calls es) = None \<or> (if is_vals es1 \<and> (\<exists>a. v = Addr a) then \<lfloor>(THE a. Val v = addr a, M, THE vs. es1 = map Val vs)\<rfloor> else calls1 es1) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(clarsimp split del: if_split split: if_split_asm simp add: is_vals_conv \<tau>reds0r_map_Val)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>vs a aa ab b. \<lbrakk>\<not> \<tau>moves1 P h es1; \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); extTA2J0 P,P,t \<turnstile> \<langle>map Val vs,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; \<forall>vs. es1 \<noteq> map Val vs; es = map Val vs; v = Addr a; calls1 es1 = \<lfloor>(aa, ab, b)\<rfloor>\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>addr a\<bullet>M(map Val vs),(h, xs)\<rangle> -ta\<rightarrow> \<langle>addr a\<bullet>M(es'),(h', xs')\<rangle> \<and> synthesized_call P h (a, M, vs) \<and> (\<forall>vsa a es'. map Val vs \<noteq> map Val vsa @ Throw a # es') \<and> (\<exists>T. (\<exists>z. typeof_addr h a = \<lfloor>z\<rfloor> \<and> ty_of_htype z = T) \<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)))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1)) \<and> (if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> \<not> final (Val v\<bullet>M(es1))
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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> if (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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 (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(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 call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
[PROOF STEP]
apply(rule if_intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; (\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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))))\<rbrakk> \<Longrightarrow> (\<tau>red0t (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (Val v\<bullet>M(es'), xs') \<or> countInitBlock (Val v\<bullet>M(es1')) < countInitBlock (Val v\<bullet>M(es1)) \<and> Val v\<bullet>M(es') = Val v\<bullet>M(es) \<and> xs' = xs) \<and> h' = h \<and> ta1 = \<lbrace>\<rbrace> \<and> ta = \<lbrace>\<rbrace>
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> ta_bisim01 ta (extTA2J1 (compP1 P) ta1) \<and> (if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es)))
[PROOF STEP]
apply(rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> ta_bisim01 ta (extTA2J1 (compP1 P) ta1)
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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)))))\<rbrakk> \<Longrightarrow> if call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None then \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e'' else extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
[PROOF STEP]
apply(rule if_intro)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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))))); call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None\<rbrakk> \<Longrightarrow> \<exists>e'' xs''. \<tau>red0r (extTA2J0 P) P t h (Val v\<bullet>M(es), xs) (e'', xs'') \<and> extTA2J0 P,P,t \<turnstile> \<langle>e'',(h, xs'')\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h e'' \<and> \<not> \<tau>move0 P h e''
 2. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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))))); \<not> (call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
[PROOF STEP]
apply(clarsimp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<exists>y. calls es = \<lfloor>y\<rfloor>) \<and> (\<exists>y. calls1 es1 = \<lfloor>y\<rfloor>); \<not> finals es1 \<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; \<not> ((\<exists>vs a es'. es1 = map Val vs @ Throw a # es') \<or> (\<exists>vs. es1 = 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))))); \<not> (call (Val v\<bullet>M(es)) = None \<or> call1 (Val v\<bullet>M(es1)) = None)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> no_call P h (Val v\<bullet>M(es)) \<and> \<not> \<tau>move0 P h (Val v\<bullet>M(es))
[PROOF STEP]
apply(clarsimp split: if_split_asm split del: if_split simp add: is_vals_conv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba. \<lbrakk>\<not> \<tau>moves1 P h es1; (\<forall>vs. es1 \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a); \<not> finals es1; \<forall>vs a es'. es1 \<noteq> map Val vs @ Throw a # es'; (\<forall>vs. es1 \<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))); ta_bisim01 ta (extTA2J1 (compP (\<lambda>C M Ts T (pns, y). compE1 (this # pns) y) P) ta1); extTA2J0 P,P,t \<turnstile> \<langle>es,(h, xs)\<rangle> [-ta\<rightarrow>] \<langle>es',(h', xs')\<rangle>; no_calls P h es; \<not> \<tau>moves0 P h es; calls es = \<lfloor>(a, aa, b)\<rfloor>; calls1 es1 = \<lfloor>(ab, ac, ba)\<rfloor>; (\<forall>vs. es \<noteq> map Val vs) \<or> (\<forall>a. v \<noteq> Addr a)\<rbrakk> \<Longrightarrow> extTA2J0 P,P,t \<turnstile> \<langle>Val v\<bullet>M(es),(h, xs)\<rangle> -ta\<rightarrow> \<langle>Val v\<bullet>M(es'),(h', xs')\<rangle> \<and> (if (\<exists>vs. es = map Val vs) \<and> (\<exists>a. v = Addr a) then synthesized_call P h (THE a. Val v = addr a, M, THE vs. es = map Val vs) else no_calls P h es) \<and> (\<forall>vs a es'. es \<noteq> map Val vs @ Throw a # es') \<and> ((\<forall>vs. es \<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))))
[PROOF STEP]
apply(fastforce intro: CallParams)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done