Theory J1JVM

(*  Title:      JinjaThreads/Compiler/J1JVM.thy
    Author:     Andreas Lochbihler
*)

section ‹Correctness of Stage: From intermediate language to JVM›

theory J1JVM imports J1JVMBisim begin

context J1_JVM_heap_base begin

declare τmove1.simps [simp del] τmoves1.simps [simp del]

lemma bisim1_insync_Throw_exec:
  assumes bisim2: "P,e2,h ⊢ (Throw ad, xs) ↔ (stk, loc, pc, xcp)"
  shows "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), xcp) ([Addr ad], loc, 6 + length (compE2 e1) + length (compE2 e2), None)"
proof -
  from bisim2 have pc: "pc < length (compE2 e2)" and [simp]: "xs = loc" by(auto dest: bisim1_ThrowD)
  let ?pc = "6 + length (compE2 e1) + length (compE2 e2)"
  let ?stk = "Addr ad # drop (size stk - 0) stk"
  from bisim2 have "xcp = ⌊ad⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
  thus ?thesis
  proof
    assume [simp]: "xcp = ⌊ad⌋"
    have "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), ⌊ad⌋) (?stk, loc, ?pc, None)"
    proof(rule τExect1step[unfolded exec_move_def, OF exec_catch])
      from bisim1_xcp_Some_not_caught[OF bisim2[simplified], of "λC M Ts T. compMb2" "Suc (Suc (Suc (length (compE2 e1))))" 0]
      have "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc)))) (compxE2 e2 (Suc (Suc (Suc (length (compE2 e1))))) 0) = None"
        by(simp add: compP2_def)
      thus "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc)))) (compxE2 (sync⇘V⇙ (e1) e2) 0 0) = ⌊(6 + length (compE2 e1) + length (compE2 e2), 0)⌋"
        using pc
        by(auto simp add: compP2_def match_ex_table_append matches_ex_entry_def eval_nat_numeral
                dest: match_ex_table_pc_length_compE2)
    qed(insert pc, auto intro: τmove2xcp)
    thus ?thesis by simp
  next
    assume [simp]: "xcp = None"
    with bisim2 obtain pc'
      where "τExec_movet_a P t e2 h (stk, loc, pc, None) ([Addr ad], loc, pc', ⌊ad⌋)"
      and bisim': "P, e2, h ⊢ (Throw ad, xs) ↔ ([Addr ad], loc, pc', ⌊ad⌋)" and [simp]: "xs = loc"
      by(auto dest: bisim1_Throw_τExec_movet)
    hence "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h (stk, loc, Suc (Suc (Suc (length (compE2 e1) + pc))), None) ([Addr ad], loc, Suc (Suc (Suc (length (compE2 e1) + pc'))), ⌊ad⌋)"
      by-(rule Insync_τExectI)
    also let ?stk = "Addr ad # drop (size [Addr ad] - 0) [Addr ad]"
    from bisim' have pc': "pc' < length (compE2 e2)" by(auto dest: bisim1_ThrowD)
    have "τExec_movet_a P t (sync⇘V⇙ (e1) e2) h ([Addr ad], loc, Suc (Suc (Suc (length (compE2 e1) + pc'))), ⌊ad⌋) (?stk, loc, ?pc, None)"
    proof(rule τExect1step[unfolded exec_move_def, OF exec_catch])
      from bisim1_xcp_Some_not_caught[OF bisim', of "λC M Ts T. compMb2" "Suc (Suc (Suc (length (compE2 e1))))" 0]
      have "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc')))) (compxE2 e2 (Suc (Suc (Suc (length (compE2 e1))))) 0) = None"
        by(simp add: compP2_def)
      thus "match_ex_table (compP2 P) (cname_of h ad) (Suc (Suc (Suc (length (compE2 e1) + pc')))) (compxE2 (sync⇘V⇙ (e1) e2) 0 0) = ⌊(6 + length (compE2 e1) + length (compE2 e2), 0)⌋"
        using pc'
        by(auto simp add: compP2_def match_ex_table_append matches_ex_entry_def eval_nat_numeral
                dest: match_ex_table_pc_length_compE2)
    qed(insert pc', auto intro: τmove2xcp)
    finally (tranclp_trans) show ?thesis by simp
  qed
qed

end

primrec sim12_size :: "('a, 'b, 'addr) exp ⇒ nat"
  and sim12_sizes :: "('a, 'b, 'addr) exp list ⇒ nat"
where
  "sim12_size (new C) = 0"
| "sim12_size (newA T⌊e⌉) = Suc (sim12_size e)"
| "sim12_size (Cast T e) = Suc (sim12_size e)"
| "sim12_size (e instanceof T) = Suc (sim12_size e)"
| "sim12_size (e «bop» e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (Val v) = 0"
| "sim12_size (Var V) = 0"
| "sim12_size (V := e) = Suc (sim12_size e)"
| "sim12_size (a⌊i⌉) = Suc (sim12_size a + sim12_size i)"
| "sim12_size (a⌊i⌉ := e) = Suc (sim12_size a + sim12_size i + sim12_size e)"
| "sim12_size (a∙length) = Suc (sim12_size a)"
| "sim12_size (e∙F{D}) = Suc (sim12_size e)"
| "sim12_size (e∙F{D} := e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (e∙compareAndSwap(D∙F, e', e'')) = Suc (sim12_size e + sim12_size e' + sim12_size e'')"
| "sim12_size (e∙M(es)) = Suc (sim12_size e + sim12_sizes es)"
| "sim12_size ({V:T=vo; e}) = Suc (sim12_size e)"
| "sim12_size (sync⇘V⇙(e) e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (insync⇘V⇙(a) e) = Suc (sim12_size e)"
| "sim12_size (e;; e') = Suc (sim12_size e + sim12_size e')"
| "sim12_size (if (e) e1 else e2) = Suc (sim12_size e)"
| "sim12_size (while(b) c) = Suc (Suc (sim12_size b))"
| "sim12_size (throw e) = Suc (sim12_size e)"
| "sim12_size (try e catch(C V) e') = Suc (sim12_size e)"

| "sim12_sizes [] = 0"
| "sim12_sizes (e # es) = sim12_size e + sim12_sizes es"

lemma sim12_sizes_map_Val [simp]:
  "sim12_sizes (map Val vs) = 0"
by(induct vs) simp_all

lemma sim12_sizes_append [simp]:
  "sim12_sizes (es @ es') = sim12_sizes es + sim12_sizes es'"
by(induct es) simp_all

context JVM_heap_base begin

lemma τExec_mover_length_compE2_conv [simp]:
  assumes pc: "pc ≥ length (compE2 e)"
  shows "τExec_mover ci P t e h (stk, loc, pc, xcp) s ⟷ s = (stk, loc, pc, xcp)"
proof
  assume "τExec_mover ci P t e h (stk, loc, pc, xcp) s"
  thus "s = (stk, loc, pc, xcp)" using pc
    by induct(auto simp add: τexec_move_def)
qed auto

lemma τExec_movesr_length_compE2_conv [simp]:
  assumes pc: "pc ≥ length (compEs2 es)"
  shows "τExec_movesr ci P t es h (stk, loc, pc, xcp) s ⟷ s = (stk, loc, pc, xcp)"
proof
  assume "τExec_movesr ci P t es h (stk, loc, pc, xcp) s"
  thus "s = (stk, loc, pc, xcp)" using pc
    by induct(auto simp add: τexec_moves_def)
qed auto

end

context J1_JVM_heap_base begin

lemma assumes wf: "wf_J1_prog P"
  defines [simp]: "sim_move ≡ λe e'. if sim12_size e' < sim12_size e then τExec_mover_a else τExec_movet_a"
  and [simp]: "sim_moves ≡ λes es'. if sim12_sizes es' < sim12_sizes es then τExec_movesr_a else τExec_movest_a"
  shows exec_instr_simulates_red1:
  "⟦ P, E, h ⊢ (e, xs) ↔ (stk, loc, pc, xcp); True,P,t ⊢1 ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩; bsok E n ⟧
  ⟹ ∃pc'' stk'' loc'' xcp''. P, E, h' ⊢ (e', xs') ↔ (stk'', loc'', pc'', xcp'') ∧
      (if τmove1 P h e
       then h = h' ∧ sim_move e e' P t E h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
       else ∃pc' stk' loc' xcp'. τExec_mover_a P t E h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ∧
                                 exec_move_a P t E h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'') ∧
                                 ¬ τmove2 (compP2 P) h stk' E pc' xcp' ∧
                                 (call1 e = None ∨ no_call2 E pc ∨ pc' = pc ∧ stk' = stk ∧ loc' = loc ∧ xcp' = xcp))"
  (is "⟦ _; _; _ ⟧
       ⟹ ∃pc'' stk'' loc'' xcp''. _ ∧ ?exec ta E e e' h stk loc pc xcp h' pc'' stk'' loc'' xcp''")

  and exec_instr_simulates_reds1:  
  "⟦ P, Es, h ⊢ (es, xs) [↔] (stk, loc, pc, xcp); True,P,t ⊢1 ⟨es, (h, xs)⟩ [-ta→] ⟨es', (h', xs')⟩; bsoks Es n ⟧
  ⟹ ∃pc'' stk'' loc'' xcp''. P, Es, h' ⊢ (es', xs') [↔] (stk'', loc'', pc'', xcp'') ∧
      (if τmoves1 P h es
       then h = h' ∧ sim_moves es es' P t Es h (stk, loc, pc, xcp) (stk'', loc'', pc'', xcp'')
       else ∃pc' stk' loc' xcp'. τExec_movesr_a P t Es h (stk, loc, pc, xcp) (stk', loc', pc', xcp') ∧
                                 exec_moves_a P t Es h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'') ∧ 
                                 ¬ τmoves2 (compP2 P) h stk' Es pc' xcp' ∧
                                 (calls1 es = None ∨ no_calls2 Es pc ∨ pc' = pc ∧ stk' = stk ∧ loc' = loc ∧ xcp' = xcp))"
  (is "⟦ _; _; _ ⟧
       ⟹ ∃pc'' stk'' loc'' xcp''. _ ∧ ?execs ta Es es es' h stk loc pc xcp h' pc'' stk'' loc'' xcp''")
proof(induction E n e xs stk loc pc xcp and Es n es xs stk loc pc xcp
    arbitrary: e' h' xs' Env T Env' T' and es' h' xs' Env Ts Env' Ts' rule: bisim1_bisims1_inducts_split)
  case (bisim1Call1 obj n obj' xs stk loc pc xcp ps M')
  note IHobj = bisim1Call1.IH(2)
  note IHparam = bisim1Call1.IH(4)
  note bisim1 = ‹P,obj,h ⊢ (obj', xs) ↔ (stk, loc, pc, xcp)›
  note bisim2 = ‹⋀xs. P,ps,h ⊢ (ps, xs) [↔] ([], xs, 0, None)›
  note bsok = ‹bsok (obj∙M'(ps)) n›
  note red = ‹True,P,t ⊢1 ⟨obj'∙M'(ps),(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
  from red show ?case
  proof(cases)
    case (Call1Obj E')
    note [simp] = ‹e' = E'∙M'(ps)›
      and red = ‹True,P,t ⊢1 ⟨obj',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
    from red have τ: "τmove1 P h obj' = τmove1 P h (obj'∙M'(ps))" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from red have "call1 (obj'∙M'(ps)) = call1 obj'" by auto
    moreover from IHobj[OF red] bsok
    obtain pc'' stk'' loc'' xcp'' where bisim: "P,obj,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and redo: "?exec ta obj obj' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from bisim
    have "P,obj∙M'(ps),h' ⊢ (E'∙M'(ps), xs') ↔ (stk'', loc'', pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1Call1)
    moreover { 
      assume "no_call2 obj pc"
      hence "no_call2 (obj∙M'(ps)) pc ∨ pc = length (compE2 obj)" by(auto simp add: no_call2_def) }
    ultimately show ?thesis using redo
      by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: Call_τExecrI1 Call_τExectI1 exec_move_CallI1)+
  next
    case (Call1Params es v)
    note [simp] = ‹obj' = Val v› ‹e' = Val v∙M'(es)›
      and red = ‹True,P,t ⊢1 ⟨ps, (h, xs)⟩ [-ta→] ⟨es, (h', xs')⟩›
    from red have τ: "τmove1 P h (obj'∙M'(ps)) = τmoves1 P h ps" by(auto simp add: τmove1.simps τmoves1.simps)
    from bisim1 have s: "xcp = None" "xs = loc"
      and execo: "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
      by-(rule Call_τExecrI1)
    moreover from IHparam[OF red] bsok obtain pc'' stk'' loc'' xcp''
      where bisim': "P,ps,h' ⊢ (es, xs') [↔] (stk'', loc'', pc'', xcp'')"
      and exec': "?execs ta ps ps es h [] xs 0 None h' pc'' stk'' loc'' xcp''" by auto
    have "?exec ta (obj∙M'(ps)) (obj'∙M'(ps)) (obj'∙M(es)) h [v] loc (length (compE2 obj)) None h' (length (compE2 obj) + pc'') (stk'' @ [v]) loc'' xcp''"
    proof(cases "τmove1 P h (obj'∙M'(ps))")
      case True
      with exec' τ have [simp]: "h = h'"
        and e: "sim_moves ps es P t ps h ([], xs, 0, None) (stk'', loc'', pc'', xcp'')" by auto
      from e have "sim_move (obj'∙M'(ps)) (obj'∙M'(es)) P t (obj∙M'(ps)) h ([] @ [v], xs, length (compE2 obj) + 0, None) (stk'' @ [v], loc'', length (compE2 obj) + pc'', xcp'')"
        by(fastforce dest: Call_τExecrI2 Call_τExectI2)
      with s True show ?thesis by auto
    next
      case False
      with exec' τ obtain pc' stk' loc' xcp'
        where e: "τExec_movesr_a P t ps h ([], xs, 0, None) (stk', loc', pc', xcp')"
        and e': "exec_moves_a P t ps h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'')"
        and τ': "¬ τmoves2 (compP2 P) h stk' ps pc' xcp'" 
        and call: "calls1 ps = None ∨ no_calls2 ps 0 ∨ pc' = 0 ∧ stk' = [] ∧ loc' = xs ∧ xcp' = None" by auto
      from e have "τExec_mover_a P t (obj∙M'(ps)) h ([] @ [v], xs, length (compE2 obj) + 0, None) (stk' @ [v], loc', length (compE2 obj) + pc', xcp')" by(rule Call_τExecrI2)
      moreover from e' have "exec_move_a P t (obj∙M'(ps)) h (stk' @ [v], loc', length (compE2 obj) + pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'' @ [v], loc'', length (compE2 obj) + pc'', xcp'')"
        by(rule exec_move_CallI2)
      moreover from τ' e' have "τmove2 (compP2 P) h (stk' @ [v]) (obj∙M'(ps)) (length (compE2 obj) + pc') xcp' ⟹ False"
        by(fastforce simp add: τmove2_iff τmoves2_iff τinstr_stk_drop_exec_moves split: if_split_asm)
      moreover from red have "call1 (obj'∙M'(ps)) = calls1 ps" by(auto simp add: is_vals_conv)
      moreover have "no_calls2 ps 0 ⟹ no_call2 (obj∙M'(ps)) (length (compE2 obj)) ∨ ps = []" "calls1 [] = None"
        by(auto simp add: no_calls2_def no_call2_def)
      ultimately show ?thesis using False s call
        by(auto simp del: split_paired_Ex call1.simps calls1.simps) blast
    qed
    moreover from bisim'
    have "P,obj∙M'(ps),h' ⊢ (Val v∙M'(es), xs') ↔ ((stk'' @ [v]), loc'', length (compE2 obj) + pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1CallParams)
    moreover from bisim1 have "pc ≠ length (compE2 obj) ⟶ no_call2 (obj∙M'(ps)) pc"
      by(auto simp add: no_call2_def dest: bisim_Val_pc_not_Invoke bisim1_pc_length_compE2)
    ultimately show ?thesis using τ execo
      apply(auto simp del: split_paired_Ex call1.simps calls1.simps split: if_split_asm split del: if_split)
      apply(blast intro: τExec_mover_trans|fastforce elim!: τExec_mover_trans simp del: split_paired_Ex call1.simps calls1.simps)+
      done
  next
    case (Call1ThrowObj a)
    note [simp] = ‹obj' = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
    have τ: "τmove1 P h (Throw a∙M'(ps))" by(rule τmove1CallThrowObj)
    from bisim1 have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
    thus ?thesis
    proof
      assume [simp]: "xcp = ⌊a⌋"
      with bisim1 have "P, obj∙M'(ps), h ⊢ (Throw a, xs) ↔ (stk, loc, pc, ⌊a⌋)"
        by(auto intro: bisim1_bisims1.bisim1CallThrowObj)
      thus ?thesis using τ by(fastforce)
    next
      assume [simp]: "xcp = None"
      with bisim1 obtain pc'
        where "τExec_mover_a P t obj h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        and bisim': "P, obj, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
        by(auto dest: bisim1_Throw_τExec_mover)
      hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule Call_τExecrI1)
      moreover from bisim' have "P, obj∙M'(ps), h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        by(rule bisim1CallThrowObj)
      ultimately show ?thesis using τ by auto
    qed
  next
    case (Call1ThrowParams vs a es' v)
    note [simp] = ‹obj' = Val v› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
      and ps = ‹ps = map Val vs @ Throw a # es'›
    from bisim1 have [simp]: "xcp = None" "xs = loc"
      and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([v], loc, length (compE2 obj), None)"
      by-(rule Call_τExecrI1)
    also from bisims1_Throw_τExec_movest[OF bisim2[of xs, unfolded ps]]
    obtain pc' where exec': "τExec_movest_a P t (map Val vs @ Throw a # es') h ([], xs, 0, None) (Addr a # rev vs, xs, pc', ⌊a⌋)"
      and bisim': "P,map Val vs @ Throw a # es',h ⊢ (map Val vs @ Throw a # es', xs) [↔] (Addr a # rev vs, xs, pc', ⌊a⌋)"
      by auto
    from Call_τExectI2[OF exec', of "obj" M' v] ps
    have "τExec_movet_a P t (obj∙M'(ps)) h ([v], loc, length (compE2 obj), None) (Addr a # rev vs @ [v], xs, length (compE2 obj) + pc', ⌊a⌋)" by simp
    also from bisim1_bisims1.bisim1CallThrowParams[OF bisim', of obj M' v] ps
    have bisim'': "P,obj∙M'(ps),h ⊢ (Throw a, xs) ↔ (Addr a # rev vs @ [v], xs, length (compE2 obj) + pc', ⌊a⌋)" by simp
    moreover have "τmove1 P h (obj'∙M'(ps))" using ps by(auto intro: τmove1CallThrowParams)
    ultimately show ?thesis by fastforce
  next
    case (Red1CallExternal a Ta Ts Tr D vs va H')
    hence [simp]: "obj' = addr a" "ps = map Val vs"
      "e' = extRet2J (addr a∙M'(map Val vs)) va" "H' = h'" "xs' = xs"
      and Ta: "typeof_addr h a = ⌊Ta⌋"
      and iec: "P ⊢ class_type_of Ta sees M': Ts→Tr = Native in D"
      and redex: "P,t ⊢ ⟨a∙M'(vs),h⟩ -ta→ext ⟨va,h'⟩" by auto
    from bisim1 have [simp]: "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
    have τ: "τmove1 P h (addr a∙M'(map Val vs)) ⟷  τmove2 (compP2 P) h (rev vs @ [Addr a]) (obj∙M'(ps)) (length (compE2 obj) + length (compEs2 ps)) None" using Ta iec
      by(auto simp add: map_eq_append_conv τmove1.simps τmoves1.simps τmove2_iff compP2_def)
    from bisim1 have s: "xcp = None" "lcl (h, xs) = loc"
      and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (obj∙M'(ps)) h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)"
      by-(rule Call_τExecrI1)
    also have "τExec_movesr_a P t ps h ([], loc, 0, None) (rev vs, loc, length (compEs2 ps), None)"
      unfolding ‹ps = map Val vs› by(rule τExec_movesr_map_Val)
    from Call_τExecrI2[OF this, of obj M' "Addr a"]
    have "τExec_mover_a P t (obj∙M'(ps)) h ([Addr a], loc, length (compE2 obj), None) (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 ps), None)" by simp
    also (rtranclp_trans) from bisim1 have "pc ≤ length (compE2 obj)" by(rule bisim1_pc_length_compE2)
    hence "no_call2 (obj∙M'(ps)) pc ∨ pc = length (compE2 obj) + length (compEs2 ps)"
      using bisim1 by(fastforce simp add: no_call2_def neq_Nil_conv dest: bisim_Val_pc_not_Invoke)
    moreover { 
      assume "pc = length (compE2 obj) + length (compEs2 ps)"
      with ‹τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Addr a], loc, length (compE2 obj), None)›
      have "stk = rev vs @ [Addr a]" "xcp = None" by auto }
    moreover
    let ?ret = "extRet2JVM (length ps) h' (rev vs @ [Addr a]) loc undefined undefined (length (compE2 obj) + length (compEs2 ps)) [] va"
    let ?stk' = "fst (hd (snd (snd ?ret)))"
    let ?xcp' = "fst ?ret"
    let ?pc' = "snd (snd (snd (snd (hd (snd (snd ?ret))))))"
    from redex have redex': "(ta, va, h') ∈ red_external_aggr (compP2 P) t a M' vs h"
      by -(rule red_external_imp_red_external_aggr, simp add: compP2_def)
    with Ta iec redex'
    have "exec_move_a P t (obj∙M'(ps)) h (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 ps), None) (extTA2JVM (compP2 P) ta) h' (?stk', loc, ?pc', ?xcp')"
      unfolding exec_move_def
      by-(rule exec_instr,cases va,(force simp add: compP2_def simp del: split_paired_Ex)+)
    moreover have "P,obj∙M'(ps),h' ⊢ (extRet2J1 (addr a∙M'(map Val vs)) va, loc) ↔ (?stk', loc, ?pc', ?xcp')"
    proof(cases va)
      case (RetVal v)
      have "P,obj∙M'(ps),h' ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (obj∙M'(ps))), None)"
        by(rule bisim1Val2) simp
      thus ?thesis unfolding RetVal by simp
    next
      case (RetExc ad) thus ?thesis by(auto intro: bisim1CallThrow)
    next
      case RetStaySame 
      from bisims1_map_Val_append[OF bisims1Nil, of "map Val vs" vs P h' loc]
      have "P,map Val vs,h' ⊢ (map Val vs, loc) [↔] (rev vs, loc, length (compEs2 (map Val vs)), None)" by simp
      hence "P,obj∙M'(map Val vs),h' ⊢ (addr a∙M'(map Val vs), loc) ↔ (rev vs @ [Addr a], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None)"
        by(rule bisim1CallParams)
      thus ?thesis using RetStaySame by simp
    qed
    moreover from redex Ta iec
    have "τmove1 P h (addr a∙M'(map Val vs)) ⟹ ta = ε ∧ h' = h"
      by(fastforce simp add: τmove1.simps τmoves1.simps map_eq_append_conv τexternal'_def τexternal_def dest: τexternal'_red_external_heap_unchanged τexternal'_red_external_TA_empty sees_method_fun)
    ultimately show ?thesis using τ
      apply(cases "τmove1 P h (addr a∙M'(map Val vs) :: 'addr expr1)")
      apply(auto simp del: split_paired_Ex simp add: compP2_def)
      apply(blast intro: rtranclp.rtrancl_into_rtrancl rtranclp_into_tranclp1 τexec_moveI)+
      done
  next
    case (Red1CallNull vs)
    note [simp] = ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹obj' = null› ‹ps = map Val vs› ‹e' = THROW NullPointer›
    from bisim1 have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t obj h (stk, loc, pc, xcp) ([Null], loc, length (compE2 obj), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (obj∙M'(map Val vs)) h (stk, loc, pc, xcp) ([Null], loc, length (compE2 obj), None)"
      by-(rule Call_τExecrI1)
    also have "τExec_movesr_a P t (map Val vs) h ([], loc, 0, None) (rev vs, loc, length (compEs2 (map Val vs)), None)"
    proof(cases "vs")
      case Nil thus ?thesis by(auto)
    next
      case Cons 
      with bisims1_refl[of P "h" "map Val vs" loc, simplified] show ?thesis
        by -(drule bisims1_Val_τExec_moves, auto)
    qed
    from Call_τExecrI2[OF this, of obj M' Null]
    have "τExec_mover_a P t (obj∙M'(map Val vs)) h ([Null], loc, length (compE2 obj), None) (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None)" by simp
    also (rtranclp_trans) {
      have "τmove2 (compP2 P) h (rev vs @ [Null]) (obj∙M'(map Val vs)) (length (compE2 obj) + length (compEs2 (map Val vs))) None"
        by(simp add: τmove2_iff)
      moreover have "exec_move_a P t (obj∙M'(map Val vs)) h (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None) ε h (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
        unfolding exec_move_def by(cases vs)(auto intro: exec_instr)
      ultimately have "τExec_movet_a P t (obj∙M'(map Val vs)) h  (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), None) (rev vs @ [Null], loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
        by(auto intro: τexec_moveI simp add: compP2_def) }
    also have "τmove1 P h (null∙M'(map Val vs))" by(auto simp add: τmove1.simps τmoves1.simps map_eq_append_conv)
    moreover have "P,obj∙M'(map Val vs),h ⊢ (THROW NullPointer, loc) ↔ ((rev vs @ [Null]), loc, length (compE2 obj) + length (compEs2 (map Val vs)), ⌊addr_of_sys_xcpt NullPointer⌋)"
      by(rule bisim1CallThrow) simp
    ultimately show ?thesis using s by(auto simp del: split_paired_Ex)
  qed
next
  case bisim1Val2 thus ?case by fastforce
next
  case (bisim1New C' n xs)
  have τ: "¬ τmove1 P h (new C')" by(auto simp add: τmove1.simps τmoves1.simps)
  from ‹True,P,t ⊢1 ⟨new C',(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
  proof cases
    case (Red1New a)
    hence "exec_meth_a (compP2 P) [New C'] [] t h ([], xs, 0, None) ⦃NewHeapElem a (Class_type C')⦄ h' ([Addr a], xs, Suc 0, None)"
      and [simp]: "e' = addr a" "xs' = xs" "ta = ⦃NewHeapElem a (Class_type C')⦄"
      by (auto intro!: exec_instr simp add: compP2_def simp del: fun_upd_apply cong cong del: image_cong_simp)
    moreover have "P, new C', h' ⊢ (addr a, xs) ↔ ([Addr a], xs, length (compE2 (new C')), None)"
      by(rule bisim1Val2)(simp)
    moreover have "¬ τmove2 (compP2 P) h [] (new C') 0 None" by(simp add: τmove2_iff)
    ultimately show ?thesis using τ 
      by(fastforce simp add: exec_move_def ta_upd_simps)
  next
    case Red1NewFail
    hence "exec_meth_a (compP2 P) [New C'] [] t h ([], xs, 0, None) ε h' ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"
      and [simp]: "ta = ε" "xs' = xs" "e' = THROW OutOfMemory"
      by(auto intro!:exec_instr simp add: compP2_def simp del: fun_upd_apply)
    moreover have "P, new C', h' ⊢ (THROW OutOfMemory, xs) ↔ ([], xs, 0, ⌊addr_of_sys_xcpt OutOfMemory⌋)"
      by(rule bisim1NewThrow)
    moreover have "¬ τmove2 (compP2 P) h [] (new C') 0 None" by(simp add: τmove2_iff)
    ultimately show ?thesis using τ by(fastforce simp add: exec_move_def)
  qed
next
  case bisim1NewThrow thus ?case by fastforce
next
  case (bisim1NewArray E n e xs stk loc pc xcp U)
  note IH = bisim1NewArray.IH(2)
  note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
  note red = ‹True,P,t ⊢1 ⟨newA U⌊e⌉,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
  note bsok = ‹bsok (newA U⌊E⌉) n›
  from red show ?case
  proof cases 
    case (New1ArrayRed ee')
    note [simp] = ‹e' = newA U⌊ee'⌉›
      and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
    from red have "τmove1 P h (newA U⌊e⌉) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from red have "call1 (newA U⌊e⌉) = call1 e" by auto
    moreover from IH[OF red] bsok
    obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from bisim
    have "P,newA U⌊E⌉,h' ⊢ (newA U⌊ee'⌉, xs') ↔ (stk'', loc'', pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1NewArray)
    moreover { 
      assume "no_call2 E pc"
      hence "no_call2 (newA U⌊E⌉) pc" by(auto simp add: no_call2_def) }
    ultimately show ?thesis using redo
      by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: NewArray_τExecrI NewArray_τExectI exec_move_newArrayI)+
  next
    case (Red1NewArray i a)
    note [simp] = ‹e = Val (Intg i)› ‹ta = ⦃NewHeapElem a (Array_type U (nat (sint i)))⦄› ‹e' = addr a› ‹xs' = xs›
      and new = ‹(h', a) ∈ allocate h (Array_type U (nat (sint i)))›
    from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
    from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (newA U⌊E⌉) h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
      by(rule NewArray_τExecrI)
    moreover from new ‹0 <=s i›
    have "exec_move_a P t (newA U⌊E⌉) h ([Intg i], loc, length (compE2 E), None) ⦃NewHeapElem a (Array_type U (nat (sint i)))⦄ h' ([Addr a], loc, Suc (length (compE2 E)), None)"
      by (auto intro!: exec_instr simp add: compP2_def exec_move_def cong del: image_cong_simp)
    moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
    moreover have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover have "P, newA U⌊E⌉, h' ⊢ (addr a, loc) ↔ ([Addr a], loc, length (compE2 (newA U⌊E⌉)), None)"
      by(rule bisim1Val2) simp
    ultimately show ?thesis using s by(auto simp del: fun_upd_apply simp add: ta_upd_simps) blast
  next
    case (Red1NewArrayNegative i)
    note [simp] = ‹e = Val (Intg i)› ‹e' = THROW NegativeArraySize› ‹h' = h› ‹xs' = xs› ‹ta = ε›
    have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from bisim have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    moreover from ‹i <s 0›
    have "exec_meth_a (compP2 P) (compE2 (newA U⌊E⌉)) (compxE2 (newA U⌊E⌉) 0 0) t h ([Intg i], loc, length (compE2 E), None) ε h ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt NegativeArraySize⌋)"
      by -(rule exec_instr, auto simp add: compP2_def)
    moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
    moreover
    have "P,newA U⌊E⌉,h ⊢ (THROW NegativeArraySize, loc) ↔ ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt NegativeArraySize⌋)"
      by(auto intro!: bisim1_bisims1.bisim1NewArrayFail)
    ultimately show ?thesis using s 
      by(auto simp add: exec_move_def)(blast intro: NewArray_τExecrI)
  next
    case (Red1NewArrayFail i)
    note [simp] = ‹e = Val (Intg i)› ‹e' = THROW OutOfMemory› ‹xs' = xs› ‹ta = ε› ‹h' = h›
      and new = ‹allocate h (Array_type U (nat (sint i))) = {}›
    have "¬ τmove1 P h (newA U⌊Val (Intg i)⌉)" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from bisim have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([Intg i], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    moreover from ‹0 <=s i› new
    have "exec_meth_a (compP2 P) (compE2 (newA U⌊E⌉)) (compxE2 (newA U⌊E⌉) 0 0) t h ([Intg i], loc, length (compE2 E), None) ε h' ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt OutOfMemory⌋)"
      by -(rule exec_instr, auto simp add: compP2_def)
    moreover have "τmove2 (compP2 P) h [Intg i] (newA U⌊E⌉) (length (compE2 E)) None ⟹ False" by(simp add: τmove2_iff)
    moreover
    have "P,newA U⌊E⌉,h' ⊢ (THROW OutOfMemory, loc) ↔ ([Intg i], loc, length (compE2 E), ⌊addr_of_sys_xcpt OutOfMemory⌋)"
      by(auto intro!: bisim1_bisims1.bisim1NewArrayFail)
    ultimately show ?thesis using s by (auto simp add: exec_move_def)(blast intro: NewArray_τExecrI)
  next
    case (New1ArrayThrow a)
    note [simp] = ‹e = Throw a› ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹e' = Throw a›
    have τ: "τmove1 P h (newA U⌊e⌉)" by(auto intro: τmove1NewArrayThrow)
    from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
    thus ?thesis
    proof
      assume [simp]: "xcp = ⌊a⌋"
      with bisim have "P,newA U⌊E⌉, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
        by(auto intro: bisim1_bisims1.bisim1NewArrayThrow)
      thus ?thesis using τ by(fastforce)
    next
      assume [simp]: "xcp = None"
      with bisim obtain pc'
        where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
        by(auto dest: bisim1_Throw_τExec_mover)
      hence "τExec_mover_a P t (newA U⌊E⌉) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule NewArray_τExecrI)
      moreover from bisim' have "P, newA U⌊E⌉, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        by(rule bisim1_bisims1.bisim1NewArrayThrow)
      ultimately show ?thesis using τ by auto
    qed
  qed
next
  case bisim1NewArrayThrow thus ?case by auto
next
  case bisim1NewArrayFail thus ?case by auto
next
  case (bisim1Cast E n e xs stk loc pc xcp U)
  note IH = bisim1Cast.IH(2)
  note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
  note red = ‹True,P,t ⊢1 ⟨Cast U e,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
  note bsok = ‹bsok (Cast U E) n›
  from red show ?case
  proof cases
    case (Cast1Red ee')
    note [simp] = ‹e' = Cast U ee'›
      and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
    from red have "τmove1 P h (Cast U e) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from red have "call1 (Cast U e) = call1 e" by auto
    moreover from IH[OF red] bsok
    obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from bisim
    have "P,Cast U E,h' ⊢ (Cast U ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1Cast)
    moreover { 
      assume "no_call2 E pc"
      hence "no_call2 (Cast U E) pc" by(auto simp add: no_call2_def) }
    ultimately show ?thesis using redo
      by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: Cast_τExecrI Cast_τExectI exec_move_CastI)+
  next
    case (Red1Cast c U')
    hence [simp]: "e = Val c" "ta = ε" "e' = Val c" "h' = h" "xs' = xs"
      and type: "typeof⇘h⇙ c = ⌊U'⌋" "P ⊢ U' ≤ U" by auto
    from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
    from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
      by(rule Cast_τExecrI)
    moreover from type
    have "exec_meth_a (compP2 P) (compE2 (Cast U E)) (compxE2 (Cast U E) 0 0) t h ([c], loc, length (compE2 E), None) ε h' ([c], loc, Suc (length (compE2 E)), None)"
      by(auto intro!: exec_instr simp add: compP2_def)
    moreover have "τmove2 (compP2 P) h [c] (Cast U E) (length (compE2 E)) None" by(simp add: τmove2_iff)
    ultimately have "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([c], loc, Suc (length (compE2 E)), None)"
      by(fastforce elim: rtranclp.rtrancl_into_rtrancl intro: τexec_moveI simp add: exec_move_def compP2_def)
    moreover have "τmove1 P h (Cast U (Val c))" by(rule τmove1CastRed)
    moreover 
    have "P, Cast U E, h' ⊢ (Val c, loc) ↔ ([c], loc, length (compE2 (Cast U E)), None)"
      by(rule bisim1Val2) simp
    ultimately show ?thesis using s by(auto simp add: exec_move_def)
  next
    case (Red1CastFail v U')
    note [simp] = ‹e = Val v› ‹e' = THROW ClassCast› ‹h' = h› ‹xs' = xs› ‹ta = ε›
    moreover from bisim have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t E h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), None)"
      by(auto elim: Cast_τExecrI)
    moreover from ‹typeof⇘hp (h, xs)⇙ v = ⌊U'⌋› ‹¬ P ⊢ U' ≤ U›
    have "exec_meth_a (compP2 P) (compE2 (Cast U E)) (compxE2 (Cast U E) 0 0) t h ([v], loc, length (compE2 E), None) ε h ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
      by -(rule exec_instr, auto simp add: compP2_def)
    moreover have "τmove2 (compP2 P) h [v] (Cast U E) (length (compE2 E)) None" by(simp add: τmove2_iff)
    ultimately have "τExec_movet_a P t (Cast U E) h (stk, loc, pc, xcp) ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
      by(fastforce simp add: exec_move_def compP2_def intro: rtranclp_into_tranclp1 τexec_moveI)
    moreover have "τmove1 P h (Cast U (Val v))" by(rule τmove1CastRed)
    moreover
    have "P,Cast U E,h ⊢ (THROW ClassCast, loc) ↔ ([v], loc, length (compE2 E), ⌊addr_of_sys_xcpt ClassCast⌋)"
      by(auto intro!: bisim1_bisims1.bisim1CastFail)
    ultimately show ?thesis using s by(auto simp add: exec_move_def)
  next
    case [simp]: (Cast1Throw a)
    have τ: "τmove1 P h (Cast U e)" by(auto intro: τmove1CastThrow)
    from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
    thus ?thesis
    proof
      assume [simp]: "xcp = ⌊a⌋"
      with bisim have "P,Cast U E, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
        by(auto intro: bisim1_bisims1.bisim1CastThrow)
      thus ?thesis using τ by(fastforce)
    next
      assume [simp]: "xcp = None"
      with bisim obtain pc'
        where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
        by(auto dest: bisim1_Throw_τExec_mover)
      hence "τExec_mover_a P t (Cast U E) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule Cast_τExecrI)
      moreover from bisim' have "P, Cast U E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule bisim1_bisims1.bisim1CastThrow, auto)
      ultimately show ?thesis using τ by auto
    qed
  qed
next
  case bisim1CastThrow thus ?case by auto
next
  case bisim1CastFail thus ?case by auto
next
  case (bisim1InstanceOf E n e xs stk loc pc xcp U)
  note IH = bisim1InstanceOf(2)
  note bisim = ‹P,E,h ⊢ (e, xs) ↔ (stk, loc, pc, xcp)›
  note red = ‹True,P,t ⊢1 ⟨e instanceof U,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
  note bsok = ‹bsok (E instanceof U) n›
  from red show ?case
  proof cases
    case (InstanceOf1Red ee')
    note [simp] = ‹e' = ee' instanceof U›
      and red = ‹True,P,t ⊢1 ⟨e,(h, xs)⟩ -ta→ ⟨ee', (h', xs')⟩›
    from red have "τmove1 P h (e instanceof U) = τmove1 P h e" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from red have "call1 (e instanceof U) = call1 e" by auto
    moreover from IH[OF red] bsok
    obtain pc'' stk'' loc'' xcp'' where bisim: "P,E,h' ⊢ (ee', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and redo: "?exec ta E e ee' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from bisim
    have "P,E instanceof U,h' ⊢ (ee' instanceof U, xs') ↔ (stk'', loc'', pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1InstanceOf)
    moreover { 
      assume "no_call2 E pc"
      hence "no_call2 (E instanceof U) pc" by(auto simp add: no_call2_def) }
    ultimately show ?thesis using redo
      by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: InstanceOf_τExecrI InstanceOf_τExectI exec_move_InstanceOfI)+
  next
    case (Red1InstanceOf c U' b)
    hence [simp]: "e = Val c" "ta = ε" "e' = Val (Bool (c ≠ Null ∧ P ⊢ U' ≤ U))" "h' = h" "xs' = xs"
      "b = (c ≠ Null ∧ P ⊢ U' ≤ U)"
      and type: "typeof⇘h⇙ c = ⌊U'⌋" by auto
    from bisim have s: "xcp = None" "xs = loc" by(auto dest: bisim_Val_loc_eq_xcp_None)
    from bisim have "τExec_mover_a P t E h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, xcp) ([c], loc, length (compE2 E), None)"
      by(rule InstanceOf_τExecrI)
    moreover from type
    have "exec_meth_a (compP2 P) (compE2 (E instanceof U)) (compxE2 (E instanceof U) 0 0) t h ([c], loc, length (compE2 E), None) ε h' ([Bool b], loc, Suc (length (compE2 E)), None)"
      by(auto intro!: exec_instr simp add: compP2_def)
    moreover have "τmove2 (compP2 P) h [c] (E instanceof U) (length (compE2 E)) None" by(simp add: τmove2_iff)
    ultimately have "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, xcp) ([Bool b], loc, Suc (length (compE2 E)), None)"
      by(fastforce elim: rtranclp.rtrancl_into_rtrancl intro: τexec_moveI simp add: exec_move_def compP2_def)
    moreover have "τmove1 P h ((Val c) instanceof U)" by(rule τmove1InstanceOfRed)
    moreover
    have "P, E instanceof U, h' ⊢ (Val (Bool b), loc) ↔ ([Bool b], loc, length (compE2 (E instanceof U)), None)"
      by(rule bisim1Val2) simp
    ultimately show ?thesis using s by(auto simp add: exec_move_def)
  next
    case (InstanceOf1Throw a)
    note [simp] = ‹e = Throw a› ‹h' = h› ‹xs' = xs› ‹ta = ε› ‹e' = Throw a›
    have τ: "τmove1 P h (e instanceof U)" by(auto intro: τmove1InstanceOfThrow)
    from bisim have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
    thus ?thesis
    proof
      assume [simp]: "xcp = ⌊a⌋"
      with bisim have "P,E instanceof U, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
        by(auto intro: bisim1_bisims1.bisim1InstanceOfThrow)
      thus ?thesis using τ by(fastforce)
    next
      assume [simp]: "xcp = None"
      with bisim obtain pc'
        where "τExec_mover_a P t E h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        and bisim': "P, E, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)" and [simp]: "xs = loc"
        by(auto dest: bisim1_Throw_τExec_mover)
      hence "τExec_mover_a P t (E instanceof U) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule InstanceOf_τExecrI)
      moreover from bisim' have "P, E instanceof U, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule bisim1_bisims1.bisim1InstanceOfThrow, auto)
      ultimately show ?thesis using τ by auto
    qed
  qed
next
  case bisim1InstanceOfThrow thus ?case by auto
next
  case bisim1Val thus ?case by fastforce
next
  case (bisim1Var V n xs)
  from ‹True,P,t ⊢1 ⟨Var V,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
  proof cases
    case (Red1Var v)
    hence "exec_meth_a (compP2 P) [Load V] [] t h ([], xs, 0, None) ε h ([v], xs, 1, None)"
      and [simp]: "ta = ε" "h' = h" "xs' = xs" "e' = Val v"
      by(auto intro: exec_instr)
    moreover have "τmove2 (compP2 P) h [] (Var V) 0 None" by(simp add: τmove2_iff)
    ultimately have "τExec_movet_a P t (Var V) h ([], xs, 0, None) ([v], xs, 1, None)"
      by(auto intro: τExect1step simp add: exec_move_def compP2_def)
    moreover have "P, Var V, h ⊢ (Val v, xs) ↔ ([v], xs, length (compE2 (Var V)), None)"
      by(rule bisim1Val2) simp
    moreover have "τmove1 P h (Var V)" by(rule τmove1Var)
    ultimately show ?thesis by(fastforce)
  qed
next
  case (bisim1BinOp1 e1 n e1' xs stk loc pc xcp e2 bop)
  note IH1 = bisim1BinOp1.IH(2)
  note IH2 = bisim1BinOp1.IH(4)
  note bisim1 = ‹P,e1,h ⊢ (e1', xs) ↔ (stk, loc, pc, xcp)›
  note bisim2 = ‹⋀xs. P,e2,h ⊢ (e2, xs) ↔ ([], xs, 0, None)›
  note bsok = ‹bsok (e1 «bop» e2) n›
  from ‹True,P,t ⊢1 ⟨e1' «bop» e2,(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩› show ?case
  proof cases
    case (Bin1OpRed1 E')
    note [simp] = ‹e' = E' «bop» e2›
      and red = ‹True,P,t ⊢1 ⟨e1',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
    from red have "τmove1 P h (e1' «bop» e2) = τmove1 P h e1'" by(auto simp add: τmove1.simps τmoves1.simps)
    moreover from red have "call1 (e1' «bop» e2) = call1 e1'" by auto
    moreover from IH1[OF red] bsok
    obtain pc'' stk'' loc'' xcp'' where bisim: "P,e1,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and redo: "?exec ta e1 e1' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from bisim 
    have "P,e1«bop»e2,h' ⊢ (E'«bop»e2, xs') ↔ (stk'', loc'', pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1BinOp1)
    moreover { 
      assume "no_call2 e1 pc"
      hence "no_call2 (e1«bop»e2) pc ∨ pc = length (compE2 e1)" by(auto simp add: no_call2_def) }
    ultimately show ?thesis using redo
      by(auto simp del: call1.simps calls1.simps split: if_split_asm split del: if_split)(blast intro: BinOp_τExecrI1 BinOp_τExectI1 exec_move_BinOpI1)+
  next
    case (Bin1OpRed2 E' v)
    note [simp] = ‹e1' = Val v› ‹e' = Val v «bop» E'›
      and red = ‹True,P,t ⊢1 ⟨e2,(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
    from red have τ: "τmove1 P h (Val v «bop» e2) = τmove1 P h e2" by(auto simp add: τmove1.simps τmoves1.simps)
    from bisim1 have s: "xcp = None" "xs = loc"
      and exec1: "τExec_mover_a P t e1 h (stk, loc, pc, None) ([v], xs, length (compE2 e1), None)"
      by(auto dest: bisim1Val2D1)
    from exec1 have "τExec_mover_a P t (e1«bop»e2) h (stk, loc, pc, None) ([v], xs, length (compE2 e1), None)"
      by(rule BinOp_τExecrI1)
    moreover
    from IH2[OF red] bsok obtain pc'' stk'' loc'' xcp''
      where bisim': "P,e2,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and exec': "?exec ta e2 e2 E' h [] xs 0 None h' pc'' stk'' loc'' xcp''" by auto
    have "?exec ta (e1«bop»e2) (Val v«bop»e2) (Val v«bop»E') h ([] @ [v]) xs (length (compE2 e1) + 0) None h' (length (compE2 e1) + pc'') (stk'' @ [v]) loc'' xcp''"
    proof(cases "τmove1 P h (Val v «bop» e2)")
      case True
      with exec' τ have [simp]: "h = h'" and e: "sim_move e2 E' P t e2 h ([], xs, 0, None) (stk'', loc'', pc'', xcp'')" by auto
      from e have "sim_move (Val v«bop»e2) (Val v«bop»E') P t (e1 «bop» e2) h ([] @ [v], xs, length (compE2 e1) + 0, None) (stk'' @ [v], loc'', length (compE2 e1) + pc'', xcp'')"
        by(fastforce dest: BinOp_τExecrI2 BinOp_τExectI2)
      with True show ?thesis by auto
    next
      case False
      with exec' τ obtain pc' stk' loc' xcp'
        where e: "τExec_mover_a P t e2 h ([], xs, 0, None) (stk', loc', pc', xcp')"
        and e': "exec_move_a P t e2 h (stk', loc', pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'', loc'', pc'', xcp'')"
        and τ': "¬ τmove2 (compP2 P) h stk' e2 pc' xcp'" 
        and call: "call1 e2 = None ∨ no_call2 e2 0 ∨ pc' = 0 ∧ stk' = [] ∧ loc' = xs ∧ xcp' = None" by auto
      from e have "τExec_mover_a P t (e1 «bop» e2) h ([] @ [v], xs, length (compE2 e1) + 0, None) (stk' @ [v], loc', length (compE2 e1) + pc', xcp')" by(rule BinOp_τExecrI2)
      moreover from e' have "exec_move_a P t (e1 «bop» e2) h (stk' @ [v], loc', length (compE2 e1) + pc', xcp') (extTA2JVM (compP2 P) ta) h' (stk'' @ [v], loc'', length (compE2 e1) + pc'', xcp'')"
        by(rule exec_move_BinOpI2)
      moreover from e' have "pc' < length (compE2 e2)" by auto
      with τ' e' have "¬ τmove2 (compP2 P) h (stk' @ [v]) (e1 «bop» e2) (length (compE2 e1) + pc') xcp'"
        by(auto simp add: τinstr_stk_drop_exec_move τmove2_iff)
      moreover from red have "call1 (e1'«bop»e2) = call1 e2" by(auto)
      moreover have "no_call2 e2 0 ⟹ no_call2 (e1«bop»e2) (length (compE2 e1))"
        by(auto simp add: no_call2_def)
      ultimately show ?thesis using False call
        by(auto simp del: split_paired_Ex call1.simps calls1.simps) blast
    qed
    moreover from bisim'
    have "P,e1«bop»e2,h' ⊢ (Val v«bop»E', xs') ↔ ((stk'' @ [v]), loc'', length (compE2 e1) + pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1BinOp2)
    moreover from bisim1 have "pc ≠ length (compE2 e1) ⟶ no_call2 (e1«bop»e2) pc"
      by(auto simp add: no_call2_def dest: bisim_Val_pc_not_Invoke bisim1_pc_length_compE2)
    ultimately show ?thesis using τ exec1 s
      apply(auto simp del: split_paired_Ex call1.simps calls1.simps split: if_split_asm split del: if_split)
      apply(blast intro: τExec_mover_trans|fastforce elim!: τExec_mover_trans simp del: split_paired_Ex call1.simps calls1.simps)+
      done
  next
    case (Red1BinOp v1 v2 v)
    note [simp] = ‹e1' = Val v1› ‹e2 = Val v2› ‹ta = ε› ‹e' = Val v› ‹h' = h› ‹xs' = xs›
      and binop = ‹binop bop v1 v2 = ⌊Inl v⌋›
    have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
    from bisim1 have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (e1«bop»Val v2) h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
      by-(rule BinOp_τExecrI1)
    also have "τmove2 (compP2 P) h [v1] (e1 «bop» Val v2) (length (compE2 e1) + 0) None"
      by(rule τmove2BinOp2)(rule τmove2Val)
    with binop have "τExec_mover_a P t (e1«bop»Val v2) h ([v1], loc, length (compE2 e1), None) ([v2, v1], loc, Suc (length (compE2 e1)), None)"
      by-(rule τExecr1step, auto intro!: exec_instr simp add: exec_move_def compP2_def)
    also (rtranclp_trans) from binop
    have "exec_meth_a (compP2 P) (compE2 (e1«bop»Val v2)) (compxE2 (e1«bop»Val v2) 0 0) t
                               h ([v2, v1], loc, Suc (length (compE2 e1)), None) ε
                               h ([v], loc, Suc (Suc (length (compE2 e1))), None)"
      by-(rule exec_instr, auto)
    moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»Val v2) (Suc (length (compE2 e1))) None" by(simp add: τmove2_iff) 
    ultimately have "τExec_mover_a P t (e1 «bop» Val v2) h (stk, loc, pc, xcp) ([v], loc, Suc (Suc (length (compE2 e1))), None)"
      by(fastforce intro: rtranclp.rtrancl_into_rtrancl τexec_moveI simp add: exec_move_def compP2_def)
    moreover
    have "P, e1 «bop» Val v2, h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (e1 «bop» Val v2)), None)"
      by(rule bisim1Val2) simp
    ultimately show ?thesis using s τ by auto
  next
    case (Red1BinOpFail v1 v2 a)
    note [simp] = ‹e1' = Val v1› ‹e2 = Val v2› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
      and binop = ‹binop bop v1 v2 = ⌊Inr a⌋›
    have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
    from bisim1 have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (e1«bop»Val v2) h (stk, loc, pc, xcp) ([v1], loc, length (compE2 e1), None)"
      by-(rule BinOp_τExecrI1)
    also have "τmove2 (compP2 P) h [v1] (e1 «bop» Val v2) (length (compE2 e1) + 0) None"
      by(rule τmove2BinOp2)(rule τmove2Val)
    with binop have "τExec_mover_a P t (e1«bop»Val v2) h ([v1], loc, length (compE2 e1), None) ([v2, v1], loc, Suc (length (compE2 e1)), None)"
      by-(rule τExecr1step, auto intro!: exec_instr simp add: exec_move_def compP2_def)
    also (rtranclp_trans) from binop
    have "exec_meth_a (compP2 P) (compE2 (e1«bop»Val v2)) (compxE2 (e1«bop»Val v2) 0 0) t
                               h ([v2, v1], loc, Suc (length (compE2 e1)), None) ε
                               h ([v2, v1], loc, Suc (length (compE2 e1)), ⌊a⌋)"
      by-(rule exec_instr, auto)
    moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»Val v2) (Suc (length (compE2 e1))) None" by(simp add: τmove2_iff) 
    ultimately have "τExec_movet_a P t (e1 «bop» Val v2) h (stk, loc, pc, xcp) ([v2, v1], loc, Suc (length (compE2 e1)), ⌊a⌋)"
      by(fastforce intro: rtranclp_into_tranclp1 τexec_moveI simp add: exec_move_def compP2_def)
    moreover 
    have "P, e1 «bop» Val v2, h ⊢ (Throw a, loc) ↔ ([v2, v1], loc, length (compE2 e1) + length (compE2 (Val v2)), ⌊a⌋)"
      by(rule bisim1BinOpThrow)
    ultimately show ?thesis using s τ by auto
  next
    case (Bin1OpThrow1 a)
    note [simp] = ‹e1' = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
    have τ: "τmove1 P h (Throw a «bop» e2)" by(rule τmove1BinOpThrow1)
    from bisim1 have "xcp = ⌊a⌋ ∨ xcp = None" by(auto dest: bisim1_ThrowD)
    thus ?thesis
    proof
      assume [simp]: "xcp = ⌊a⌋"
      with bisim1 have "P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ (stk, loc, pc, xcp)"
        by(auto intro: bisim1_bisims1.intros)
      thus ?thesis using τ by(fastforce)
    next
      assume [simp]: "xcp = None"
      with bisim1 obtain pc' where "τExec_mover_a P t e1 h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        and bisim': "P, e1, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        and [simp]: "xs = loc"
        by(auto dest: bisim1_Throw_τExec_mover)
      hence "τExec_mover_a P t (e1«bop»e2) h (stk, loc, pc, None) ([Addr a], loc, pc', ⌊a⌋)"
        by-(rule BinOp_τExecrI1)
      moreover from bisim'
      have "P, e1«bop»e2, h ⊢ (Throw a, xs) ↔ ([Addr a], loc, pc', ⌊a⌋)"
        by(auto intro: bisim1_bisims1.bisim1BinOpThrow1)
      ultimately show ?thesis using τ by auto
    qed
  next
    case (Bin1OpThrow2 v a)
    note [simp] = ‹e1' = Val v› ‹e2 = Throw a› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
    from bisim1 have s: "xcp = None" "xs = loc"
      and "τExec_mover_a P t e1 h (stk, loc, pc, xcp) ([v], loc, length (compE2 e1), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (e1«bop»Throw a) h (stk, loc, pc, xcp) ([v], loc, length (compE2 e1), None)"
      by-(rule BinOp_τExecrI1)
    also have "τExec_mover_a P t (e1«bop»Throw a) h ([v], loc, length (compE2 e1), None) ([Addr a, v], loc, Suc (length (compE2 e1)), ⌊a⌋)"
      by(rule τExecr2step)(auto simp add: exec_move_def exec_meth_instr τmove2_iff τmove1.simps τmoves1.simps)
    also (rtranclp_trans)
    have "P,e1«bop»Throw a,h ⊢ (Throw a, loc) ↔ ([Addr a] @ [v], loc, (length (compE2 e1) + length (compE2 (addr a))), ⌊a⌋)"
      by(rule bisim1BinOpThrow2[OF bisim1Throw2])
    moreover have "τmove1 P h (e1' «bop» e2)" by(auto intro: τmove1BinOpThrow2)
    ultimately show ?thesis using s by auto
  qed
next
  case (bisim1BinOp2 e2 n e2' xs stk loc pc xcp e1 bop v1)
  note IH2 = bisim1BinOp2.IH(2)
  note bisim1 = ‹⋀xs. P,e1,h ⊢ (e1, xs) ↔ ([], xs, 0, None)›
  note bisim2 = ‹P,e2,h ⊢ (e2', xs) ↔ (stk, loc, pc, xcp)›
  note red = ‹True,P,t ⊢1 ⟨Val v1 «bop» e2',(h, xs)⟩ -ta→ ⟨e',(h', xs')⟩›
  note bsok = ‹bsok (e1 «bop» e2) n›
  from red show ?case
  proof cases
    case (Bin1OpRed2 E')
    note [simp] = ‹e' = Val v1 «bop» E'›
      and red = ‹True,P,t ⊢1 ⟨e2',(h, xs)⟩ -ta→ ⟨E',(h', xs')⟩›
    from IH2[OF red] bsok obtain pc'' stk'' loc'' xcp''
      where bisim': "P,e2,h' ⊢ (E', xs') ↔ (stk'', loc'', pc'', xcp'')"
      and exec': "?exec ta e2 e2' E' h stk loc pc xcp h' pc'' stk'' loc'' xcp''" by auto
    from red have τ: "τmove1 P h (Val v1 «bop» e2') = τmove1 P h e2'" by(auto simp add: τmove1.simps τmoves1.simps)
    have "no_call2 e2 pc ⟹ no_call2 (e1 «bop» e2) (length (compE2 e1) + pc)" by(auto simp add: no_call2_def)
    hence "?exec ta (e1«bop»e2) (Val v1«bop»e2') (Val v1«bop»E') h (stk @ [v1]) loc (length (compE2 e1) + pc) xcp h' (length (compE2 e1) + pc'') (stk'' @ [v1]) loc'' xcp''"
      using exec' τ
      apply(cases "τmove1 P h (Val v1 «bop» e2')")
      apply(auto)
      apply(blast intro: BinOp_τExecrI2 BinOp_τExectI2 exec_move_BinOpI2)
      apply(blast intro: BinOp_τExecrI2 BinOp_τExectI2 exec_move_BinOpI2)
      apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2|assumption)+
      apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)
      apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2|assumption)+
      apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)
      apply(rule exI conjI BinOp_τExecrI2 exec_move_BinOpI2 rtranclp.rtrancl_refl|assumption)+
      apply(fastforce simp add: τinstr_stk_drop_exec_move τmove2_iff split: if_split_asm)+
      done
    moreover from bisim'
    have "P,e1«bop»e2,h' ⊢ (Val v1«bop»E', xs') ↔ (stk''@[v1], loc'', length (compE2 e1) + pc'', xcp'')"
      by(rule bisim1_bisims1.bisim1BinOp2)
    ultimately show ?thesis using τ by auto blast+
  next
    case (Red1BinOp v2 v)
    note [simp] = ‹e2' = Val v2› ‹ta = ε› ‹e' = Val v› ‹h' = h› ‹xs' = xs›
      and binop = ‹binop bop v1 v2 = ⌊Inl v⌋›
    have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
    from bisim2 have s: "xcp = None" "xs = loc" 
      and "τExec_mover_a P t e2 h (stk, loc, pc, xcp) ([v2], loc, length (compE2 e2), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (e1«bop»e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v2] @ [v1], loc, length (compE2 e1) + length (compE2 e2), None)"
      by-(rule BinOp_τExecrI2)
    moreover from binop
    have "exec_move_a P t (e1«bop»e2) h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), None) ε
                                  h ([v], loc, Suc (length (compE2 e1) + length (compE2 e2)), None)"
      unfolding exec_move_def by-(rule exec_instr, auto)
    moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»e2) (length (compE2 e1) + length (compE2 e2)) None"
      by(simp add: τmove2_iff)
    ultimately have "τExec_mover_a P t (e1 «bop» e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v], loc, Suc (length (compE2 e1) + length (compE2 e2)), None)"
      by(auto intro: rtranclp.rtrancl_into_rtrancl τexec_moveI simp add: compP2_def)
    moreover 
    have "P, e1 «bop» e2, h ⊢ (Val v, loc) ↔ ([v], loc, length (compE2 (e1 «bop» e2)), None)"
      by(rule bisim1Val2) simp
    ultimately show ?thesis using s τ by(auto)
  next
    case (Red1BinOpFail v2 a)
    note [simp] = ‹e2' = Val v2› ‹ta = ε› ‹e' = Throw a› ‹h' = h› ‹xs' = xs›
      and binop = ‹binop bop v1 v2 = ⌊Inr a⌋›
    have τ: "τmove1 P h (Val v1 «bop» Val v2)" by(rule τmove1BinOp)
    from bisim2 have s: "xcp = None" "xs = loc" 
      and "τExec_mover_a P t e2 h (stk, loc, pc, xcp) ([v2], loc, length (compE2 e2), None)"
      by(auto dest: bisim1Val2D1)
    hence "τExec_mover_a P t (e1«bop»e2) h (stk @ [v1], loc, length (compE2 e1) + pc, xcp) ([v2] @ [v1], loc, length (compE2 e1) + length (compE2 e2), None)"
      by-(rule BinOp_τExecrI2)
    moreover from binop
    have "exec_move_a P t (e1«bop»e2) h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), None) ε
                                  h ([v2, v1], loc, length (compE2 e1) + length (compE2 e2), ⌊a⌋)"
      unfolding exec_move_def by-(rule exec_instr, auto)
    moreover have "τmove2 (compP2 P) h [v2, v1] (e1«bop»e2) (length (compE2 e1) + length (compE2 e2)) None"
      by(simp add: τmove2_iff)
    ultimately have "τExec_movet_a P t (e1 «bop