Theory Correctness1

(*  Title:      JinjaThreads/Compiler/Correctness1.thy
    Author:     Andreas Lochbihler, Tobias Nipkow

    reminiscent of the Jinja theory Compiler/Correctness1
*)

section ‹Semantic Correctness of Stage 1›

theory Correctness1 imports
  J0J1Bisim
  "../J/DefAssPreservation"
begin

lemma finals_map_Val [simp]: "finals (map Val vs)"
by(simp add: finals_iff)

context J_heap_base begin

lemma τred0r_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "⟦ τred0r extTA P t h (e, xs) (e', xs'); 𝒟 e ⌊dom xs⌋ ⟧ ⟹ 𝒟 e' ⌊dom xs'⌋"
by(induct rule: rtranclp_induct2)(auto dest: red_preserves_defass[OF wf])

lemma τred0t_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "⟦ τred0t extTA P t h (e, xs) (e', xs'); 𝒟 e ⌊dom xs⌋ ⟧ ⟹ 𝒟 e' ⌊dom xs'⌋"
by(rule τred0r_preserves_defass[OF wf])(rule tranclp_into_rtranclp)

end

lemma LAss_lem:
  "⟦x ∈ set xs; size xs ≤ size ys ⟧
  ⟹ m1 ⊆⇩m m2(xs[↦]ys) ⟹ m1(x↦y) ⊆⇩m m2(xs[↦]ys[index xs x := y])"
apply(simp add:map_le_def)
apply(simp add:fun_upds_apply index_less_aux eq_sym_conv)
done

lemma Block_lem:
fixes l :: "'a ⇀ 'b"
assumes 0: "l ⊆⇩m [Vs [↦] ls]"
    and 1: "l' ⊆⇩m [Vs [↦] ls', V↦v]"
    and hidden: "V ∈ set Vs ⟹ ls ! index Vs V = ls' ! index Vs V"
    and size: "size ls = size ls'"    "size Vs < size ls'"
shows "l'(V := l V) ⊆⇩m [Vs [↦] ls']"
proof -
  have "l'(V := l V) ⊆⇩m [Vs [↦] ls', V↦v](V := l V)"
    using 1 by(rule map_le_upd)
  also have "… = [Vs [↦] ls'](V := l V)" by simp
  also have "… ⊆⇩m [Vs [↦] ls']"
  proof (cases "l V")
    case None thus ?thesis by simp
  next
    case (Some w)
    hence "[Vs [↦] ls] V = Some w"
      using 0 by(force simp add: map_le_def split:if_splits)
    hence VinVs: "V ∈ set Vs" and w: "w = ls ! index Vs V"
      using size by(auto simp add:fun_upds_apply split:if_splits)
    hence "w = ls' ! index Vs V" using hidden[OF VinVs] by simp
    hence "[Vs [↦] ls'](V := l V) = [Vs [↦] ls']"
      using Some size VinVs by(simp add:index_less_aux map_upds_upd_conv_index)
    thus ?thesis by simp
  qed
  finally show ?thesis .
qed

subsection ‹Correctness proof›

locale J0_J1_heap_base =
  J?: J_heap_base +
  J1?: J1_heap_base + 
  constrains addr2thread_id :: "('addr :: addr) ⇒ 'thread_id"
  and thread_id2addr :: "'thread_id ⇒ 'addr"
  and empty_heap :: "'heap"
  and allocate :: "'heap ⇒ htype ⇒ ('heap × 'addr) set"
  and typeof_addr :: "'heap ⇒ 'addr ⇀ htype"
  and heap_read :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ bool"
  and heap_write :: "'heap ⇒ 'addr ⇒ addr_loc ⇒ 'addr val ⇒ 'heap ⇒ bool"
begin

lemma ta_bisim01_extTA2J0_extTA2J1:
  assumes wf: "wf_J_prog P"
  and nt: "⋀n T C M a h. ⟦ n < length ⦃ta⦄⇘t⇙; ⦃ta⦄⇘t⇙ ! n = NewThread T (C, M, a) h ⟧
           ⟹ typeof_addr h a = ⌊Class_type C⌋ ∧ (∃T meth D. P ⊢ C sees M:[]→T =⌊meth⌋ in D)"
  shows "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
apply(simp add: ta_bisim_def ta_upd_simps)
apply(auto intro!: list_all2_all_nthI)
apply(case_tac "⦃ta⦄⇘t⇙ ! n")
  apply(auto simp add: bisim_red0_Red1_def)
apply(drule (1) nt)
apply(clarify)
apply(erule bisim_list_extTA2J0_extTA2J1[OF wf, simplified])
done

lemma red_external_ta_bisim01: 
  "⟦ wf_J_prog P; P,t ⊢ ⟨a∙M(vs), h⟩ -ta→ext ⟨va, h'⟩ ⟧ ⟹ ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
apply(rule ta_bisim01_extTA2J0_extTA2J1, assumption)
apply(drule (1) red_external_new_thread_sees, auto simp add: in_set_conv_nth)
apply(drule red_ext_new_thread_heap, auto simp add: in_set_conv_nth)
done

lemmas τred1t_expr =
  NewArray_τred1t_xt Cast_τred1t_xt InstanceOf_τred1t_xt BinOp_τred1t_xt1 BinOp_τred1t_xt2 LAss_τred1t
  AAcc_τred1t_xt1 AAcc_τred1t_xt2 AAss_τred1t_xt1 AAss_τred1t_xt2 AAss_τred1t_xt3
  ALength_τred1t_xt FAcc_τred1t_xt FAss_τred1t_xt1 FAss_τred1t_xt2 
  CAS_τred1t_xt1 CAS_τred1t_xt2 CAS_τred1t_xt3 Call_τred1t_obj
  Call_τred1t_param Block_None_τred1t_xt Block_τred1t_Some Sync_τred1t_xt InSync_τred1t_xt
  Seq_τred1t_xt Cond_τred1t_xt Throw_τred1t_xt Try_τred1t_xt

lemmas τred1r_expr =
  NewArray_τred1r_xt Cast_τred1r_xt InstanceOf_τred1r_xt BinOp_τred1r_xt1 BinOp_τred1r_xt2 LAss_τred1r
  AAcc_τred1r_xt1 AAcc_τred1r_xt2 AAss_τred1r_xt1 AAss_τred1r_xt2 AAss_τred1r_xt3
  ALength_τred1r_xt FAcc_τred1r_xt FAss_τred1r_xt1 FAss_τred1r_xt2
  CAS_τred1r_xt1 CAS_τred1r_xt2 CAS_τred1r_xt3 Call_τred1r_obj
  Call_τred1r_param Block_None_τred1r_xt Block_τred1r_Some Sync_τred1r_xt InSync_τred1r_xt
  Seq_τred1r_xt Cond_τred1r_xt Throw_τred1r_xt Try_τred1r_xt

definition sim_move01 :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr ⇒ 'addr expr1 ⇒ 'heap
  ⇒ 'addr locals1 ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 ⇒ 'heap ⇒ 'addr locals1 ⇒ bool"
where
  "sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟷ ¬ final e0 ∧
  (if τmove0 P h e0 then h' = h ∧ ta0 = ε ∧ ta = ε ∧ τred1't P t h (e, xs) (e', xs')
   else ta_bisim01 ta0 (extTA2J1 P ta) ∧
     (if call e0 = None ∨ call1 e = None
      then (∃e'' xs''. τred1'r P t h (e, xs) (e'', xs'') ∧ False,P,t ⊢1 ⟨e'', (h, xs'')⟩ -ta→ ⟨e', (h', xs')⟩ ∧
                       ¬ τmove1 P h e'')
      else False,P,t ⊢1 ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩ ∧ ¬ τmove1 P h e))"

definition sim_moves01 :: 
  "'addr J1_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr list ⇒ 'addr expr1 list ⇒ 'heap
  ⇒ 'addr locals1 ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 list ⇒ 'heap ⇒ 'addr locals1 ⇒ bool"
where
  "sim_moves01 P t ta0 es0 es h xs ta es' h' xs' ⟷ ¬ finals es0 ∧
  (if τmoves0 P h es0 then h' = h ∧ ta0 = ε ∧ ta = ε ∧ τreds1't P t h (es, xs) (es', xs')
   else ta_bisim01 ta0 (extTA2J1 P ta) ∧
     (if calls es0 = None ∨ calls1 es = None
      then (∃es'' xs''. τreds1'r P t h (es, xs) (es'', xs'') ∧ False,P,t ⊢1 ⟨es'', (h, xs'')⟩ [-ta→] ⟨es', (h', xs')⟩ ∧ 
                        ¬ τmoves1 P h es'')
      else False,P,t ⊢1 ⟨es, (h, xs)⟩ [-ta→] ⟨es', (h', xs')⟩ ∧ ¬ τmoves1 P h es))"

declare τred1t_expr [elim!] τred1r_expr[elim!]

lemma sim_move01_expr:
  assumes "sim_move01 P t ta0 e0 e h xs ta e' h' xs'"
  shows
  "sim_move01 P t ta0 (newA T⌊e0⌉) (newA T⌊e⌉) h xs ta (newA T⌊e'⌉) h' xs'"
  "sim_move01 P t ta0 (Cast T e0) (Cast T e) h xs ta (Cast T e') h' xs'"
  "sim_move01 P t ta0 (e0 instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs'"
  "sim_move01 P t ta0 (e0 «bop» e2) (e «bop» e2') h xs ta (e' «bop» e2') h' xs'"
  "sim_move01 P t ta0 (Val v «bop» e0) (Val v «bop» e) h xs ta (Val v «bop» e') h' xs'"
  "sim_move01 P t ta0 (V := e0) (V' := e) h xs ta (V' := e') h' xs'"
  "sim_move01 P t ta0 (e0⌊e2⌉) (e⌊e2'⌉) h xs ta (e'⌊e2'⌉) h' xs'"
  "sim_move01 P t ta0 (Val v⌊e0⌉) (Val v⌊e⌉) h xs ta (Val v⌊e'⌉) h' xs'"
  "sim_move01 P t ta0 (e0⌊e2⌉ := e3) (e⌊e2'⌉ := e3') h xs ta (e'⌊e2'⌉ := e3') h' xs'"
  "sim_move01 P t ta0 (Val v⌊e0⌉ := e3) (Val v⌊e⌉ := e3') h xs ta (Val v⌊e'⌉ := e3') h' xs'"
  "sim_move01 P t ta0 (AAss (Val v) (Val v') e0) (AAss (Val v) (Val v') e) h xs ta (AAss (Val v) (Val v') e') h' xs'"
  "sim_move01 P t ta0 (e0∙length) (e∙length) h xs ta (e'∙length) h' xs'"
  "sim_move01 P t ta0 (e0∙F{D}) (e∙F'{D'}) h xs ta (e'∙F'{D'}) h' xs'"
  "sim_move01 P t ta0 (FAss e0 F D e2) (FAss e F' D' e2') h xs ta (FAss e' F' D' e2') h' xs'"
  "sim_move01 P t ta0 (FAss (Val v) F D e0) (FAss (Val v) F' D' e) h xs ta (FAss (Val v) F' D' e') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap e0 D F e2 e3) (CompareAndSwap e D F e2' e3') h xs ta (CompareAndSwap e' D F e2' e3') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap (Val v) D F e0 e3) (CompareAndSwap (Val v) D F e e3') h xs ta (CompareAndSwap (Val v) D F e' e3') h' xs'"
  "sim_move01 P t ta0 (CompareAndSwap (Val v) D F (Val v') e0) (CompareAndSwap (Val v) D F (Val v') e) h xs ta (CompareAndSwap (Val v) D F (Val v') e') h' xs'"
  "sim_move01 P t ta0 (e0∙M(es)) (e∙M(es')) h xs ta (e'∙M(es')) h' xs'"
  "sim_move01 P t ta0 ({V:T=vo; e0}) ({V':T=None; e}) h xs ta ({V':T=None; e'}) h' xs'"
  "sim_move01 P t ta0 (sync(e0) e2) (sync⇘V'⇙(e) e2') h xs ta (sync⇘V'⇙(e') e2') h' xs'"
  "sim_move01 P t ta0 (insync(a) e0) (insync⇘V'⇙(a') e) h xs ta (insync⇘V'⇙(a') e') h' xs'"
  "sim_move01 P t ta0 (e0;;e2) (e;;e2') h xs ta (e';;e2') h' xs'"
  "sim_move01 P t ta0 (if (e0) e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs'"
  "sim_move01 P t ta0 (throw e0) (throw e) h xs ta (throw e') h' xs'"
  "sim_move01 P t ta0 (try e0 catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'"
using assms
apply(simp_all add: sim_move01_def final_iff τred1r_Val τred1t_Val split: if_split_asm split del: if_split)
apply(fastforce simp add: final_iff τred1r_Val τred1t_Val split!: if_splits intro: red1_reds1.intros)+
done

lemma sim_moves01_expr:
  "sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟹ sim_moves01 P t ta0 (e0 # es2) (e # es2') h xs ta (e' # es2') h' xs'"
  "sim_moves01 P t ta0 es0 es h xs ta es' h' xs' ⟹ sim_moves01 P t ta0 (Val v # es0) (Val v # es) h xs ta (Val v # es') h' xs'"
apply(simp_all add: sim_move01_def sim_moves01_def final_iff finals_iff Cons_eq_append_conv τred1t_Val τred1r_Val split: if_split_asm split del: if_split)
apply(auto simp add: Cons_eq_append_conv τred1t_Val τred1r_Val split!: if_splits intro: List1Red1 List1Red2 τred1t_inj_τreds1t τred1r_inj_τreds1r τreds1t_cons_τreds1t τreds1r_cons_τreds1r)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τred1r_inj_τreds1r List1Red1)
apply(force elim!: τreds1r_cons_τreds1r intro!: List1Red2)
apply(force elim!: τreds1r_cons_τreds1r intro!: List1Red2)
done

lemma sim_move01_CallParams:
  "sim_moves01 P t ta0 es0 es h xs ta es' h' xs'
  ⟹ sim_move01 P t ta0 (Val v∙M(es0)) (Val v∙M(es)) h xs ta (Val v∙M(es')) h' xs'"
apply(clarsimp simp add: sim_move01_def sim_moves01_def τreds1r_map_Val τreds1t_map_Val is_vals_conv split: if_split_asm split del: if_split)
  apply(fastforce simp add: sim_move01_def sim_moves01_def τreds1r_map_Val τreds1t_map_Val intro: Call_τred1r_param Call1Params)
 apply(rule conjI, fastforce)
 apply(split if_split)
 apply(rule conjI)
  apply(clarsimp simp add: finals_iff)
 apply(clarify)
 apply(split if_split)
 apply(rule conjI)
  apply(simp del: call.simps calls.simps call1.simps calls1.simps)
  apply(fastforce simp add: sim_move01_def sim_moves01_def τred1r_Val τred1t_Val τreds1r_map_Val_Throw intro: Call_τred1r_param Call1Params split: if_split_asm)
 apply(fastforce split: if_split_asm simp add: is_vals_conv τreds1r_map_Val τreds1r_map_Val_Throw)
apply(rule conjI, fastforce)
apply(fastforce simp add: sim_move01_def sim_moves01_def τred1r_Val τred1t_Val τreds1t_map_Val τreds1r_map_Val is_vals_conv intro: Call_τred1r_param Call1Params split: if_split_asm)
done

lemma sim_move01_reds:
  "⟦ (h', a) ∈ allocate h (Class_type C); ta0 = ⦃NewHeapElem a (Class_type C)⦄; ta = ⦃NewHeapElem a (Class_type C)⦄ ⟧
  ⟹ sim_move01 P t ta0 (new C) (new C) h xs ta (addr a) h' xs"
  "allocate h (Class_type C) = {} ⟹ sim_move01 P t ε (new C) (new C) h xs ε (THROW OutOfMemory) h xs"
  "⟦ (h', a) ∈ allocate h (Array_type T (nat (sint i))); 0 <=s i;
     ta0 = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄; ta = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄ ⟧
  ⟹ sim_move01 P t ta0 (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ta (addr a) h' xs"
  "i <s 0 ⟹ sim_move01 P t ε (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ε (THROW NegativeArraySize) h xs"
  "⟦ allocate h (Array_type T (nat (sint i))) = {}; 0 <=s i ⟧
  ⟹ sim_move01 P t ε (newA T⌊Val (Intg i)⌉) (newA T⌊Val (Intg i)⌉) h xs ε (THROW OutOfMemory) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; P ⊢ U ≤ T ⟧
  ⟹ sim_move01 P t ε (Cast T (Val v)) (Cast T (Val v)) h xs ε (Val v) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; ¬ P ⊢ U ≤ T ⟧
  ⟹ sim_move01 P t ε (Cast T (Val v)) (Cast T (Val v)) h xs ε (THROW ClassCast) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; b ⟷ v ≠ Null ∧ P ⊢ U ≤ T ⟧
  ⟹ sim_move01 P t ε ((Val v) instanceof T) ((Val v) instanceof T) h xs ε (Val (Bool b)) h xs"
  "binop bop v1 v2 = Some (Inl v) ⟹ sim_move01 P t ε ((Val v1) «bop» (Val v2)) (Val v1 «bop» Val v2) h xs ε (Val v) h xs"
  "binop bop v1 v2 = Some (Inr a) ⟹ sim_move01 P t ε ((Val v1) «bop» (Val v2)) (Val v1 «bop» Val v2) h xs ε (Throw a) h xs"
  "⟦ xs!V = v; V < size xs ⟧ ⟹ sim_move01 P t ε (Var V') (Var V) h xs ε (Val v) h xs"
  "V < length xs ⟹ sim_move01 P t ε (V' := Val v) (V := Val v) h xs ε unit h (xs[V := v])"
  "sim_move01 P t ε (null⌊Val v⌉) (null⌊Val v⌉) h xs ε (THROW NullPointer) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
  ⟹ sim_move01 P t ε (addr a⌊Val (Intg i)⌉) ((addr a)⌊Val (Intg i)⌉) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n;
     heap_read h a (ACell (nat (sint i))) v;
     ta0 = ⦃ReadMem a (ACell (nat (sint i))) v⦄; 
     ta = ⦃ReadMem a (ACell (nat (sint i))) v⦄ ⟧
  ⟹ sim_move01 P t ta0 (addr a⌊Val (Intg i)⌉) ((addr a)⌊Val (Intg i)⌉) h xs ta (Val v) h xs"
  "sim_move01 P t ε (null⌊Val v⌉ := Val v') (null⌊Val v⌉ := Val v') h xs ε (THROW NullPointer) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
  ⟹ sim_move01 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
 "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = ⌊U⌋; ¬ (P ⊢ U ≤ T) ⟧
  ⟹ sim_move01 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayStore) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = Some U; P ⊢ U ≤ T;
     heap_write h a (ACell (nat (sint i))) v h'; 
     ta0 = ⦃WriteMem a (ACell (nat (sint i))) v⦄; ta = ⦃WriteMem a (ACell (nat (sint i))) v ⦄ ⟧
  ⟹ sim_move01 P t ta0 (AAss (addr a) (Val (Intg i)) (Val v)) (AAss (addr a) (Val (Intg i)) (Val v)) h xs ta unit h' xs"
  "typeof_addr h a = ⌊Array_type T n⌋ ⟹ sim_move01 P t ε (addr a∙length) (addr a∙length) h xs ε (Val (Intg (word_of_int (int n)))) h xs"
  "sim_move01 P t ε (null∙length) (null∙length) h xs ε (THROW NullPointer) h xs"

  "⟦ heap_read h a (CField D F) v; ta0 = ⦃ReadMem a (CField D F) v⦄; ta = ⦃ReadMem a (CField D F) v⦄ ⟧
  ⟹ sim_move01 P t ta0 (addr a∙F{D}) (addr a∙F{D}) h xs ta (Val v) h xs"
  "sim_move01 P t ε (null∙F{D}) (null∙F{D}) h xs ε (THROW NullPointer) h xs"
  "⟦ heap_write h a (CField D F) v h'; ta0 = ⦃WriteMem a (CField D F) v⦄; ta = ⦃WriteMem a (CField D F) v⦄ ⟧
  ⟹ sim_move01 P t ta0 (addr a∙F{D} := Val v) (addr a∙F{D} := Val v) h xs ta unit h' xs"
  "sim_move01 P t ε (null∙compareAndSwap(D∙F, Val v, Val v')) (null∙compareAndSwap(D∙F, Val v, Val v')) h xs ε (THROW NullPointer) h xs"
  "⟦ heap_read h a (CField D F) v''; heap_write h a (CField D F) v' h'; v'' = v; 
     ta0 = ⦃ReadMem a (CField D F) v'', WriteMem a (CField D F) v'⦄; ta = ⦃ReadMem a (CField D F) v'', WriteMem a (CField D F) v'⦄ ⟧
  ⟹ sim_move01 P t ta0 (addr a∙compareAndSwap(D∙F, Val v, Val v')) (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta true h' xs"
  "⟦ heap_read h a (CField D F) v''; v'' ≠ v; 
     ta0 = ⦃ReadMem a (CField D F) v''⦄; ta = ⦃ReadMem a (CField D F) v''⦄ ⟧
  ⟹ sim_move01 P t ta0 (addr a∙compareAndSwap(D∙F, Val v, Val v')) (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta false h xs"
  "sim_move01 P t ε (null∙F{D} := Val v) (null∙F{D} := Val v) h xs ε (THROW NullPointer) h xs"
  "sim_move01 P t ε ({V':T=vo; Val u}) ({V:T=None; Val u}) h xs ε (Val u) h xs"
  "V < length xs ⟹ sim_move01 P t ε (sync(null) e0) (sync⇘V⇙ (null) e1) h xs ε (THROW NullPointer) h (xs[V := Null])"
  "sim_move01 P t ε (Val v;;e0) (Val v;; e1) h xs ε e1 h xs"
  "sim_move01 P t ε (if (true) e0 else e0') (if (true) e1 else e1') h xs ε e1 h xs"
  "sim_move01 P t ε (if (false) e0 else e0') (if (false) e1 else e1') h xs ε e1' h xs"
  "sim_move01 P t ε (throw null) (throw null) h xs ε (THROW NullPointer) h xs"
  "sim_move01 P t ε (try (Val v) catch(C V') e0) (try (Val v) catch(C V) e1) h xs ε (Val v) h xs"
  "⟦ typeof_addr h a = ⌊Class_type D⌋; P ⊢ D ≼⇧* C; V < length xs ⟧
  ⟹ sim_move01 P t ε (try (Throw a) catch(C V') e0) (try (Throw a) catch(C V) e1) h xs ε ({V:Class C=None; e1}) h (xs[V := Addr a])"
  "sim_move01 P t ε (newA T⌊Throw a⌉) (newA T⌊Throw a⌉) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Cast T (Throw a)) (Cast T (Throw a)) h xs ε (Throw a) h xs"
  "sim_move01 P t ε ((Throw a) instanceof T) ((Throw a) instanceof T) h xs ε (Throw a) h xs"
  "sim_move01 P t ε ((Throw a) «bop» e0) ((Throw a) «bop» e1) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v «bop» (Throw a)) (Val v «bop» (Throw a)) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (V' := Throw a) (V := Throw a) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a⌊e0⌉) (Throw a⌊e1⌉) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v⌊Throw a⌉) (Val v⌊Throw a⌉) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a⌊e0⌉ := e0') (Throw a⌊e1⌉ := e1') h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v⌊Throw a⌉ := e0) (Val v⌊Throw a⌉ := e1) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v⌊Val v'⌉ := Throw a) (Val v⌊Val v'⌉ := Throw a) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a∙length) (Throw a∙length) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a∙F{D}) (Throw a∙F{D}) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a∙F{D} := e0) (Throw a∙F{D} := e1) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v∙F{D} := Throw a) (Val v∙F{D} := Throw a) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a∙compareAndSwap(D∙F, e2, e3)) (Throw a∙compareAndSwap(D∙F, e2', e3')) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v∙compareAndSwap(D∙F, Throw a, e3)) (Val v∙compareAndSwap(D∙F, Throw a, e3')) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Val v∙compareAndSwap(D∙F, Val v', Throw a)) (Val v∙compareAndSwap(D∙F, Val v', Throw a)) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a∙M(es0)) (Throw a∙M(es1)) h xs ε (Throw a) h xs"
  "sim_move01 P t ε ({V':T=vo; Throw a}) ({V:T=None; Throw a}) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (sync(Throw a) e0) (sync⇘V⇙(Throw a) e1) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (Throw a;;e0) (Throw a;;e1) h xs ε (Throw a) h xs"
  "sim_move01 P t ε (if (Throw a) e0 else e0') (if (Throw a) e1 else e1') h xs ε (Throw a) h xs"
  "sim_move01 P t ε (throw (Throw a)) (throw (Throw a)) h xs ε (Throw a) h xs"
apply(simp_all add: sim_move01_def ta_bisim_def split: if_split_asm split del: if_split)
apply(fastforce intro: red1_reds1.intros)+
done

lemma sim_move01_ThrowParams:
  "sim_move01 P t ε (Val v∙M(map Val vs @ Throw a # es0)) (Val v∙M(map Val vs @ Throw a # es1)) h xs ε (Throw a) h xs"
apply(simp add: sim_move01_def split del: if_split)
apply(rule conjI, fastforce)
apply(split if_split)
apply(rule conjI)
 apply(fastforce intro: red1_reds1.intros)
apply(fastforce simp add: sim_move01_def intro: red1_reds1.intros)
done

lemma sim_move01_CallNull:
  "sim_move01 P t ε (null∙M(map Val vs)) (null∙M(map Val vs)) h xs ε (THROW NullPointer) h xs"
by(fastforce simp add: sim_move01_def map_eq_append_conv intro: red1_reds1.intros)

lemma sim_move01_SyncLocks:
  "⟦ V < length xs; ta0 = ⦃Lock→a, SyncLock a⦄; ta = ⦃Lock→a, SyncLock a⦄ ⟧
   ⟹ sim_move01 P t ta0 (sync(addr a) e0) (sync⇘V⇙ (addr a) e1) h xs ta (insync⇘V⇙ (a) e1) h (xs[V := Addr a])"
  "⟦ xs ! V = Addr a'; V < length xs; ta0 = ⦃Unlock→a', SyncUnlock a'⦄; ta = ⦃Unlock→a', SyncUnlock a'⦄ ⟧
  ⟹ sim_move01 P t ta0 (insync(a') (Val v)) (insync⇘V⇙ (a) (Val v)) h xs ta (Val v) h xs"
  "⟦ xs ! V = Addr a'; V < length xs; ta0 = ⦃Unlock→a', SyncUnlock a'⦄; ta = ⦃Unlock→a', SyncUnlock a'⦄ ⟧
  ⟹ sim_move01 P t ta0 (insync(a') (Throw a'')) (insync⇘V⇙ (a) (Throw a'')) h xs ta (Throw a'') h xs"
by(fastforce simp add: sim_move01_def ta_bisim_def expand_finfun_eq fun_eq_iff finfun_upd_apply ta_upd_simps  intro: red1_reds1.intros[simplified] split: if_split_asm)+

lemma sim_move01_TryFail:
  "⟦ typeof_addr h a = ⌊Class_type D⌋; ¬ P ⊢ D ≼⇧* C ⟧
  ⟹ sim_move01 P t ε (try (Throw a) catch(C V') e0) (try (Throw a) catch(C V) e1) h xs ε (Throw a) h xs"
by(auto simp add: sim_move01_def intro!: Red1TryFail)

lemma sim_move01_BlockSome:
  "⟦ sim_move01 P t ta0 e0 e h (xs[V := v]) ta e' h' xs'; V < length xs ⟧
  ⟹ sim_move01 P t ta0 ({V':T=⌊v⌋; e0}) ({V:T=⌊v⌋; e}) h xs ta ({V:T=None; e'}) h' xs'"
  "V < length xs ⟹ sim_move01 P t ε ({V':T=⌊v⌋; Val u}) ({V:T=⌊v⌋; Val u}) h xs ε (Val u) h (xs[V := v])"
  "V < length xs ⟹ sim_move01 P t ε ({V':T=⌊v⌋; Throw a}) ({V:T=⌊v⌋; Throw a}) h xs ε (Throw a) h (xs[V := v])"
apply(auto simp add: sim_move01_def)
apply(split if_split_asm)
 apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_τred1r_Some)
apply(fastforce intro: intro: converse_rtranclp_into_rtranclp Block1Some Block1Red Block_τred1r_Some)
apply(fastforce simp add: sim_move01_def intro!: τred1t_2step[OF Block1Some] τred1r_1step[OF Block1Some] Red1Block Block1Throw)+
done

lemmas sim_move01_intros =
  sim_move01_expr sim_move01_reds sim_move01_ThrowParams sim_move01_CallNull sim_move01_TryFail
  sim_move01_BlockSome sim_move01_CallParams

declare sim_move01_intros[intro]

lemma sim_move01_preserves_len: "sim_move01 P t ta0 e0 e h xs ta e' h' xs' ⟹ length xs' = length xs"
by(fastforce simp add: sim_move01_def split: if_split_asm dest: τred1r_preserves_len τred1t_preserves_len red1_preserves_len)

lemma sim_move01_preserves_unmod:
  "⟦ sim_move01 P t ta0 e0 e h xs ta e' h' xs'; unmod e i; i < length xs ⟧ ⟹ xs' ! i = xs ! i"
apply(auto simp add: sim_move01_def split: if_split_asm dest: τred1t_preserves_unmod)
apply(frule (2) τred1'r_preserves_unmod)
apply(frule (1) τred1r_unmod_preserved)
apply(frule τred1r_preserves_len)
apply(auto dest: red1_preserves_unmod)
apply(frule (2) τred1'r_preserves_unmod)
apply(frule (1) τred1r_unmod_preserved)
apply(frule τred1r_preserves_len)
apply(auto dest: red1_preserves_unmod)
done

lemma assumes wf: "wf_J_prog P"
  shows red1_simulates_red_aux:
  "⟦ extTA2J0 P,P,t ⊢ ⟨e1, S⟩ -TA→ ⟨e1', S'⟩; bisim vs e1 e2 XS; fv e1 ⊆ set vs;
     lcl S ⊆⇩m [vs [↦] XS]; length vs + max_vars e1 ≤ length XS;
     ∀aMvs. call e1 = ⌊aMvs⌋ ⟶ synthesized_call P (hp S) aMvs ⟧
  ⟹ ∃ta e2' XS'. sim_move01 (compP1 P) t TA e1 e2 (hp S) XS ta e2' (hp S') XS' ∧ bisim vs e1' e2' XS' ∧ lcl S' ⊆⇩m [vs [↦] XS']"
  (is "⟦ _; _; _; _; _; ?synth e1 S ⟧ ⟹ ?concl e1 e2 S XS e1' S' TA vs")

  and reds1_simulates_reds_aux:
  "⟦ extTA2J0 P,P,t ⊢ ⟨es1, S⟩ [-TA→] ⟨es1', S'⟩; bisims vs es1 es2 XS; fvs es1 ⊆ set vs;
    lcl S ⊆⇩m [vs [↦] XS]; length vs + max_varss es1 ≤ length XS;
    ∀aMvs. calls es1 = ⌊aMvs⌋ ⟶ synthesized_call P (hp S) aMvs ⟧
  ⟹ ∃ta es2' xs'. sim_moves01 (compP1 P) t TA es1 es2 (hp S) XS ta es2' (hp S') xs' ∧ bisims vs es1' es2' xs' ∧ lcl S' ⊆⇩m [vs [↦] xs']"
  (is "⟦ _; _; _; _; _; ?synths es1 S ⟧ ⟹ ?concls es1 es2 S XS es1' S' TA vs")
proof(induct arbitrary: vs e2 XS and vs es2 XS rule: red_reds.inducts)
  case (BinOpRed1 e s ta e' s' bop e2 Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs (e «bop» e2) E2 xs› obtain E
    where "E2 = E «bop» compE1 Vs e2" and "bisim Vs e E xs" and "¬ contains_insync e2" by auto
  with IH[of Vs E xs] ‹fv (e «bop» e2) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e›
    ‹length Vs + max_vars (e «bop» e2) ≤ length xs› ‹?synth (e «bop» e2) s› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
  show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
  case (BinOpRed2 e s ta e' s' v bop Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹bisim Vs (Val v «bop» e) E2 xs› obtain E
    where "E2 = Val v «bop» E" and "bisim Vs e E xs" by auto
  with IH[of Vs E xs] ‹fv (Val v «bop» e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
    ‹length Vs + max_vars (Val v «bop» e) ≤ length xs› ‹?synth (Val v «bop» e) s› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
  show ?case by(fastforce elim!: sim_move01_expr)
next
  case RedVar thus ?case
    by(fastforce simp add: index_less_aux map_le_def fun_upds_apply intro!: exI dest: bspec)
next
  case RedLAss thus ?case
    by(fastforce intro: index_less_aux LAss_lem intro!: exI simp del: fun_upd_apply)
next
  case (AAccRed1 a s ta a' s' i Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs a e2 XS; fv a ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars a ≤ length XS;
            ?synth a s ⟧ ⟹ ?concl a e2 s XS a' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
  with ‹bisim Vs (a⌊i⌉) E2 xs› obtain E
    where "E2 = E⌊compE1 Vs i⌉" and "bisim Vs a E xs" and "¬ contains_insync i" by auto
  with IH[of Vs E xs] ‹fv (a⌊i⌉) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val a›
    ‹length Vs + max_vars (a⌊i⌉) ≤ length xs› ‹?synth (a⌊i⌉) s› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
  show ?case by(cases "is_val a'")(fastforce elim!: sim_move01_expr)+
next
  case (AAccRed2 i s ta i' s' a Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs i e2 XS; fv i ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars i ≤ length XS;
            ?synth i s ⟧ ⟹ ?concl i e2 s XS i' s' ta vs›
  from ‹bisim Vs (Val a⌊i⌉) E2 xs› obtain E
    where "E2 = Val a⌊E⌉" and "bisim Vs i E xs" by auto
  with IH[of Vs E xs] ‹fv (Val a⌊i⌉) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
    ‹length Vs + max_vars (Val a⌊i⌉) ≤ length xs› ‹?synth (Val a⌊i⌉) s› ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩›
  show ?case by(fastforce elim!: sim_move01_expr)
next
  case RedAAcc thus ?case by(auto simp del: split_paired_Ex)
next
  case (AAssRed1 a s ta a' s' i e Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs a e2 XS; fv a ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars a ≤ length XS;
            ?synth a s ⟧ ⟹ ?concl a e2 s XS a' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
  with ‹bisim Vs (a⌊i⌉:=e) E2 xs› obtain E
    where E2: "E2 = E⌊compE1 Vs i⌉:=compE1 Vs e" and "bisim Vs a E xs"
    and sync: "¬ contains_insync i" "¬ contains_insync e" by auto
  with IH[of Vs E xs] ‹fv (a⌊i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
    ‹length Vs + max_vars (a⌊i⌉:=e) ≤ length xs› ‹?synth (a⌊i⌉:=e) s›
  obtain ta' e2' xs'
    where IH': "sim_move01 (compP1 P) t ta a E (hp s) xs ta' e2' (hp s') xs'"
    "bisim Vs a' e2' xs'" "lcl s' ⊆⇩m [Vs [↦] xs']"
    by auto
  show ?case
  proof(cases "is_val a'")
    case True
    from ‹fv (a⌊i⌉:=e) ⊆ set Vs› sync
    have "bisim Vs i (compE1 Vs i) xs'" "bisim Vs e (compE1 Vs e) xs'" by auto
    with IH' E2 True sync  ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩› show ?thesis
      by(cases "is_val i")(fastforce elim!: sim_move01_expr)+
  next
    case False with IH' E2 sync ‹¬ is_val a› ‹extTA2J0 P,P,t ⊢ ⟨a,s⟩ -ta→ ⟨a',s'⟩›
    show ?thesis by(fastforce elim!: sim_move01_expr)
  qed
next
  case (AAssRed2 i s ta i' s' a e Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs i e2 XS; fv i ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars i ≤ length XS;
            ?synth i s ⟧ ⟹ ?concl i e2 s XS i' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩› have "¬ is_val i" by auto
  with ‹bisim Vs (Val a⌊i⌉ := e) E2 xs› obtain E
    where "E2 = Val a⌊E⌉:=compE1 Vs e" and "bisim Vs i E xs" and "¬ contains_insync e" by auto
  with IH[of Vs E xs] ‹fv (Val a⌊i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val i› ‹extTA2J0 P,P,t ⊢ ⟨i,s⟩ -ta→ ⟨i',s'⟩›
    ‹length Vs + max_vars (Val a⌊i⌉:=e) ≤ length xs› ‹?synth (Val a⌊i⌉:=e) s›
  show ?case by(cases "is_val i'")(fastforce elim!: sim_move01_expr)+
next
  case (AAssRed3 e s ta e' s' a i Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹bisim Vs (Val a⌊Val i⌉ := e) E2 xs› obtain E
    where "E2 = Val a⌊Val i⌉:=E" and "bisim Vs e E xs" by auto
  with IH[of Vs E xs] ‹fv (Val a⌊Val i⌉:=e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars (Val a⌊Val i⌉:=e) ≤ length xs› ‹?synth (Val a⌊Val i⌉:=e) s›
  show ?case by(fastforce elim!: sim_move01_expr)
next
  case RedAAssStore thus ?case by(auto intro!: exI)
next
  case (FAssRed1 e s ta e' s' F D e2 Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs (e∙F{D} := e2) E2 xs› obtain E
    where "E2 = E∙F{D} := compE1 Vs e2" and "bisim Vs e E xs" and "¬ contains_insync e2" by auto
  with IH[of Vs E xs] ‹fv (e∙F{D} := e2) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars (e∙F{D} := e2) ≤ length xs› ‹?synth (e∙F{D} := e2) s›
  show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
  case (FAssRed2 e s ta e' s' v F D Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹bisim Vs (Val v∙F{D} := e) E2 xs› obtain E
    where "E2 = Val v∙F{D} := E" and "bisim Vs e E xs" by auto
  with IH[of Vs E xs] ‹fv (Val v∙F{D} := e) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars (Val v∙F{D} := e) ≤ length xs› ‹?synth (Val v∙F{D} := e) s›
  show ?case by(fastforce elim!: sim_move01_expr)
next
  case (CASRed1 e s ta e' s' D F e2 e3 Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs _ E2 xs› obtain E
    where E2: "E2 = E∙compareAndSwap(D∙F, compE1 Vs e2, compE1 Vs e3)" and "bisim Vs e E xs"
    and sync: "¬ contains_insync e2" "¬ contains_insync e3" by(auto)
  with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
  obtain ta' e2' xs'
    where IH': "sim_move01 (compP1 P) t ta e E (hp s) xs ta' e2' (hp s') xs'"
    "bisim Vs e' e2' xs'" "lcl s' ⊆⇩m [Vs [↦] xs']"
    by auto
  show ?case
  proof(cases "is_val e'")
    case True
    from ‹fv _ ⊆ set Vs› sync
    have "bisim Vs e2 (compE1 Vs e2) xs'" "bisim Vs e3 (compE1 Vs e3) xs'" by auto
    with IH' E2 True sync  ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› show ?thesis
      by(cases "is_val e2")(fastforce elim!: sim_move01_expr)+
  next
    case False with IH' E2 sync ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    show ?thesis by(fastforce elim!: sim_move01_expr)
  qed
next
  case (CASRed2 e s ta e' s' v D F e3 Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs _ E2 xs› obtain E
    where "E2 = Val v∙compareAndSwap(D∙F, E, compE1 Vs e3)" and "bisim Vs e E xs" and "¬ contains_insync e3" by(auto)
  with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹¬ is_val e› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
  show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr)+
next
  case (CASRed3 e s ta e' s' v D F v' Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹bisim Vs _ E2 xs› obtain E
    where "E2 = Val v∙compareAndSwap(D∙F, Val v', E)" and "bisim Vs e E xs" by auto
  with IH[of Vs E xs] ‹fv _ ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_vars _ ≤ length xs› ‹?synth _ s›
  show ?case by(fastforce elim!: sim_move01_expr)
next
  case (CallObj e s ta e' s' M es Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs (e∙M(es)) E2 xs› obtain E
    where "E2 = E∙M(compEs1 Vs es)" and "bisim Vs e E xs" and "¬ contains_insyncs es"
    by(auto simp add: compEs1_conv_map)
  with IH[of Vs E xs] ‹fv (e∙M(es)) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]›
    ‹length Vs + max_vars (e∙M(es)) ≤ length xs› ‹?synth (e∙M(es)) s›
  show ?case by(cases "is_val e'")(fastforce elim!: sim_move01_expr split: if_split_asm)+
next
  case (CallParams es s ta es' s' v M Vs E2 xs)
  note IH = ‹⋀vs es2 XS. ⟦bisims vs es es2 XS; fvs es ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_varss es ≤ length XS;
            ?synths es s ⟧ ⟹ ?concls es es2 s XS es' s' ta vs›
  from ‹bisim Vs (Val v∙M(es)) E2 xs› obtain Es 
    where "E2 = Val v∙M(Es)" and "bisims Vs es Es xs" by auto
  moreover from ‹extTA2J0 P,P,t ⊢ ⟨es,s⟩ [-ta→] ⟨es',s'⟩› have "¬ is_vals es" by auto
  with ‹?synth (Val v∙M(es)) s› have "?synths es s" by(auto)
  moreover note IH[of Vs Es xs] ‹fv (Val v∙M(es)) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› 
    ‹length Vs + max_vars (Val v∙M(es)) ≤ length xs›
  ultimately show ?case by(fastforce elim!: sim_move01_CallParams)
next
  case (RedCall s a U M Ts T pns body D vs Vs E2 xs)
  from ‹typeof_addr (hp s) a = ⌊U⌋›
  have "call (addr a∙M(map Val vs)) = ⌊(a, M, vs)⌋" by auto
  with ‹?synth (addr a∙M(map Val vs)) s› have "synthesized_call P (hp s) (a, M, vs)" by auto
  with ‹typeof_addr (hp s) a = ⌊U⌋› ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D›
  have False by(auto simp add: synthesized_call_conv dest: sees_method_fun)
  thus ?case ..
next
  case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s' Vs E2 xs)
  from ‹bisim Vs (addr a∙M(map Val vs)) E2 xs› have "E2 = addr a∙M(map Val vs)" by auto
  moreover note ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D› ‹typeof_addr (hp s) a = ⌊T⌋› ‹ta' = extTA2J0 P ta›
    ‹e' = extRet2J (addr a∙M(map Val vs)) va› ‹s' = (h', lcl s)› ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
    ‹lcl s ⊆⇩m [Vs [↦] xs]›
  moreover from wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
  have "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)" by(rule red_external_ta_bisim01)
  moreover from ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩› ‹typeof_addr (hp s) a = ⌊T⌋›
    ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D›
  have "τexternal_defs D M ⟹ h' = hp s ∧ ta = ε"
    by(fastforce dest: τexternal'_red_external_heap_unchanged τexternal'_red_external_TA_empty simp add: τexternal'_def τexternal_def)
  ultimately show ?case 
    by(cases va)(fastforce intro!: exI[where x=ta] intro: Red1CallExternal simp add: map_eq_append_conv sim_move01_def dest: sees_method_fun simp del: split_paired_Ex)+
next
  case (BlockRed e h x V vo ta e' h' x' T Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl (h, x(V := vo)) ⊆⇩m [vs [↦] XS];
                         length vs + max_vars e ≤ length XS; ?synth e (h, (x(V := vo)))⟧
            ⟹ ?concl e e2 (h, x(V := vo)) XS e' (h', x') ta vs›
  note red = ‹extTA2J0 P,P,t ⊢ ⟨e,(h, x(V := vo))⟩ -ta→ ⟨e',(h', x')⟩›
  note len = ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
  from ‹fv {V:T=vo; e} ⊆ set Vs› have fv: "fv e ⊆ set (Vs@[V])" by auto
  from ‹bisim Vs {V:T=vo; e} E2 xs› show ?case
  proof(cases rule: bisim_cases(7)[consumes 1, case_names BlockNone BlockSome BlockSomeNone])
    case (BlockNone E')
    with red IH[of "Vs@[V]" E' xs] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
      ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
    obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h xs TA' e2' h' xs'"
      and bisim': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto 
    from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
    have "length (Vs@[V]) + max_vars e ≤ length xs'"
      by(fastforce simp add: sim_move01_def dest: red1_preserves_len τred1t_preserves_len τred1r_preserves_len split: if_split_asm)
    with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
    moreover 
    { assume "V ∈ set Vs"
      hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
      with ‹bisim (Vs @ [V]) e E' xs› have "unmod E' (index Vs V)"
        by -(rule hidden_bisim_unmod)
      moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
      have "index Vs V < length xs" by(auto intro: index_less_aux)
      ultimately have "xs ! index Vs V = xs' ! index Vs V"
        using sim_move01_preserves_unmod[OF red'] by(simp) }
    moreover from red' have "length xs = length xs'" by(rule sim_move01_preserves_len[symmetric])
    ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
      using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
      by(auto intro: Block_lem)
    show ?thesis
    proof(cases "x' V")
      case None
      with red' bisim' BlockNone len
      show ?thesis by(fastforce simp del: split_paired_Ex fun_upd_apply intro: rel)
    next
      case (Some v)
      moreover
      with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v⌋"
        by(auto simp add: map_le_def dest: bspec)
      moreover
      from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
      ultimately have "xs' ! length Vs = v" using ‹length xs = length xs'› by(simp)
      with red' bisim' BlockNone Some len
      show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
    qed
  next
    case (BlockSome E' v)
    with red IH[of "Vs@[V]" E' "xs[length Vs := v]"] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
      ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
    obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h (xs[length Vs := v]) TA' e2' h' xs'"
      and bisim': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto
    from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
    have "length (Vs@[V]) + max_vars e ≤ length xs'" by(auto dest: sim_move01_preserves_len)
    with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
    moreover 
    { assume "V ∈ set Vs"
      hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
      with ‹bisim (Vs @ [V]) e E' (xs[length Vs := v])› have "unmod E' (index Vs V)"
        by -(rule hidden_bisim_unmod)
      moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
      have "index Vs V < length xs" by(auto intro: index_less_aux)
      moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
      have "(xs[length Vs := v]) ! index Vs V = xs ! index Vs V" by(simp)
      ultimately have "xs ! index Vs V = xs' ! index Vs V"
        using sim_move01_preserves_unmod[OF red', of "index Vs V"] by(simp) }
    moreover from red' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
    ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
      using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
      by(auto intro: Block_lem)
    from BlockSome red obtain v' where Some: "x' V = ⌊v'⌋" by(auto dest!: red_lcl_incr)
    with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v'⌋"
      by(auto simp add: map_le_def dest: bspec)
    moreover
    from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
    ultimately have "xs' ! length Vs = v'" using ‹length xs = length xs'› by(simp)
    with red' bisim' BlockSome Some ‹length Vs < length xs›
    show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
  next 
    case (BlockSomeNone E')
    with red IH[of "Vs@[V]" E' xs] fv ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]›
      ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹?synth {V:T=vo; e} (h, x)›
    obtain TA' e2' xs' where red': "sim_move01 (compP1 P) t ta e E' h xs TA' e2' h' xs'"
      and IH': "bisim (Vs @ [V]) e' e2' xs'" "x' ⊆⇩m [Vs @ [V] [↦] xs']" by auto
    from red' ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
    have "length (Vs@[V]) + max_vars e ≤ length xs'" by(auto dest: sim_move01_preserves_len)
    with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "x' ⊆⇩m [Vs [↦] xs', V ↦ xs' ! length Vs]" by(simp)
    moreover 
    { assume "V ∈ set Vs"
      hence "hidden (Vs @ [V]) (index Vs V)" by(rule hidden_index)
      with ‹bisim (Vs @ [V]) e E' xs› have "unmod E' (index Vs V)"
        by -(rule hidden_bisim_unmod)
      moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
      have "index Vs V < length xs" by(auto intro: index_less_aux)
      moreover from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› ‹V ∈ set Vs›
      have "(xs[length Vs := v]) ! index Vs V = xs ! index Vs V" by(simp)
      ultimately have "xs ! index Vs V = xs' ! index Vs V"
        using sim_move01_preserves_unmod[OF red', of "index Vs V"] by(simp) }
    moreover from red' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
    ultimately have rel: "x'(V := x V) ⊆⇩m [Vs [↦] xs']"
      using ‹lcl (h, x) ⊆⇩m [Vs [↦] xs]› ‹length Vs + max_vars {V:T=vo; e} ≤ length xs›
      by(auto intro: Block_lem)
    from BlockSomeNone red obtain v' where Some: "x' V = ⌊v'⌋" by(auto dest!: red_lcl_incr)
    with ‹x' ⊆⇩m [Vs @ [V] [↦] xs']› have "[Vs @ [V] [↦] xs'] V = ⌊v'⌋"
      by(auto simp add: map_le_def dest: bspec)
    moreover
    from ‹length Vs + max_vars {V:T=vo; e} ≤ length xs› have "length Vs < length xs" by auto
    ultimately have "xs' ! length Vs = v'" using ‹length xs = length xs'› by(simp)
    with red' IH' BlockSomeNone Some ‹length Vs < length xs›
    show ?thesis by(fastforce simp del: fun_upd_apply intro: rel)
  qed
next
  case (RedBlock V T vo u s Vs E2 xs)
  from ‹bisim Vs {V:T=vo; Val u} E2 xs› obtain vo'
    where [simp]: "E2 = {length Vs:T=vo'; Val u}" by auto
  from RedBlock show ?case
  proof(cases vo)
    case (Some v)
    with ‹bisim Vs {V:T=vo; Val u} E2 xs›
    have vo': "case vo' of None ⇒ xs ! length Vs = v | Some v' ⇒ v = v'" by auto
    have "sim_move01 (compP1 P) t ε {V:T=vo; Val u} E2 (hp s) xs ε (Val u) (hp s) (xs[length Vs := v])"
    proof(cases vo')
      case None with vo'
      have "xs[length Vs := v] = xs" by auto
      thus ?thesis using Some None by auto
    next
      case Some
      from ‹length Vs + max_vars {V:T=vo; Val u} ≤ length xs› have "length Vs < length xs" by simp
      with vo' Some show ?thesis using ‹vo = Some v› by auto
    qed
    thus ?thesis using RedBlock by fastforce
  qed fastforce
next
  case SynchronizedNull thus ?case by fastforce
next
  case (LockSynchronized a e s Vs E2 xs)
  from ‹bisim Vs (sync(addr a) e) E2 xs›
  have E2: "E2 = sync⇘length Vs⇙ (addr a) (compE1 (Vs@[fresh_var Vs]) e)" 
    and sync: "¬ contains_insync e" by auto
  moreover have "fresh_var Vs ∉ set Vs" by(rule fresh_var_fresh)
  with ‹fv (sync(addr a) e) ⊆ set Vs› have "fresh_var Vs ∉ fv e" by auto
  from E2 ‹fv (sync(addr a) e) ⊆ set Vs› sync
  have "bisim (Vs@[fresh_var Vs]) e (compE1 (Vs@[fresh_var Vs]) e) (xs[length Vs := Addr a])"
    by(auto intro!: compE1_bisim)
  hence "bisim Vs (insync(a) e) (insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e)) (xs[length Vs := Addr a])"
    using ‹fresh_var Vs ∉ fv e› ‹length Vs + max_vars (sync(addr a) e) ≤ length xs› by auto
  moreover from ‹length Vs + max_vars (sync(addr a) e) ≤ length xs›
  have "False,compP1 P,t ⊢1 ⟨sync⇘length Vs⇙ (addr a) (compE1 (Vs@[fresh_var Vs]) e), (hp s, xs)⟩
        -⦃Lock→a, SyncLock a⦄→
        ⟨insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e), (hp s, xs[length Vs := Addr a])⟩"
    by -(rule Lock1Synchronized, auto)
  hence "sim_move01 (compP1 P) t ⦃Lock→a, SyncLock a⦄ (sync(addr a) e) E2 (hp s) xs ⦃Lock→a, SyncLock a⦄ (insync⇘length Vs⇙ (a) (compE1 (Vs@[fresh_var Vs]) e)) (hp s) (xs[length Vs := Addr a])"
    using E2 by(fastforce simp add: sim_move01_def ta_bisim_def)
  moreover have "zip Vs (xs[length Vs := Addr a]) = (zip Vs xs)[length Vs := (arbitrary, Addr a)]"
    by(rule sym)(simp add: update_zip)
  hence "zip Vs (xs[length Vs := Addr a]) = zip Vs xs" by simp
  with ‹lcl s ⊆⇩m [Vs [↦] xs]› have "lcl s ⊆⇩m [Vs [↦] xs[length Vs := Addr a]]"
    by(auto simp add: map_le_def map_upds_def)
  ultimately show ?case using ‹lcl s ⊆⇩m [Vs [↦] xs]› by fastforce
next
  case (SynchronizedRed2 e s ta e' s' a Vs E2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
            ?synth e s ⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹bisim Vs (insync(a) e) E2 xs› obtain E
    where E2: "E2 = insync⇘length Vs⇙ (a) E" and bisim: "bisim (Vs@[fresh_var Vs]) e E xs"
    and xsa: "xs ! length Vs = Addr a" by auto
  from ‹fv (insync(a) e) ⊆ set Vs› fresh_var_fresh[of Vs] have fv: "fresh_var Vs ∉ fv e" by auto
  from ‹length Vs + max_vars (insync(a) e) ≤ length xs› have "length Vs < length xs" by simp
  { assume "lcl s (fresh_var Vs) ≠ None"
    then obtain v where "lcl s (fresh_var Vs) = ⌊v⌋" by auto
    with ‹lcl s ⊆⇩m [Vs [↦] xs]› have "[Vs [↦] xs] (fresh_var Vs) = ⌊v⌋" 
      by(auto simp add: map_le_def dest: bspec)
    hence "fresh_var Vs ∈ set Vs" 
      by(auto simp add: map_upds_def set_zip dest!: map_of_SomeD )
    moreover have "fresh_var Vs ∉ set Vs" by(rule fresh_var_fresh)
    ultimately have False by contradiction }
  hence "lcl s (fresh_var Vs) = None" by(cases "lcl s (fresh_var Vs)", auto)
  hence "(lcl s)(fresh_var Vs := None) = lcl s" by(auto intro: ext)
  moreover from ‹lcl s ⊆⇩m [Vs [↦] xs]›
  have "(lcl s)(fresh_var Vs := None) ⊆⇩m [Vs [↦] xs, fresh_var Vs ↦ xs ! length Vs]" by(simp)
  ultimately have "lcl s ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs]"
    using ‹length Vs < length xs› by(auto)
  with IH[of "Vs@[fresh_var Vs]" E xs] ‹fv (insync(a) e) ⊆ set Vs› bisim
    ‹length Vs + max_vars (insync(a) e) ≤ length xs› ‹?synth (insync(a) e) s› 
  obtain TA' e2' xs' where IH': "sim_move01 (compP1 P) t ta e E (hp s) xs TA' e2' (hp s') xs'"
    "bisim (Vs @ [fresh_var Vs]) e' e2' xs'" "lcl s' ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs']" by auto
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "dom (lcl s') ⊆ dom (lcl s) ∪ fv e" by(auto dest: red_dom_lcl)
  with fv ‹lcl s (fresh_var Vs) = None› have "(fresh_var Vs) ∉ dom (lcl s')" by auto
  hence "lcl s' (fresh_var Vs) = None" by auto
  moreover from IH' have "length xs = length xs'" by(auto dest: sim_move01_preserves_len)
  moreover note ‹lcl s' ⊆⇩m [Vs @ [fresh_var Vs] [↦] xs']› ‹length Vs < length xs›
  ultimately have "lcl s' ⊆⇩m [Vs [↦] xs']" by(auto simp add: map_le_def dest: bspec)
  moreover from bisim fv have "unmod E (length Vs)" by(auto intro: bisim_fv_unmod)
  with IH' ‹length Vs < length xs› have "xs ! length Vs = xs' ! length Vs"
    by(auto dest!: sim_move01_preserves_unmod)
  with xsa have "xs' ! length Vs = Addr a" by simp
  ultimately show ?case using IH' E2 by(fastforce)
next
  case (UnlockSynchronized a v s Vs E2 xs)
  from ‹bisim Vs (insync(a) Val v) E2 xs› have E2: "E2 = insync⇘length Vs⇙ (a) Val v" 
    and xsa: "xs ! length Vs = Addr a" by auto
  moreover from ‹length Vs + max_vars (insync(a) Val v) ≤ length xs› xsa
  have "False,compP1 P,t ⊢1 ⟨insync⇘length Vs⇙ (a) (Val v), (hp s, xs)⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Val v, (hp s, xs)⟩"
    by-(rule Unlock1Synchronized, auto)
  hence "sim_move01 (compP1 P) t ⦃Unlock→a, SyncUnlock a⦄ (insync(a) Val v) (insync⇘length Vs⇙ (a) Val v) (hp s) xs ⦃Unlock→a, SyncUnlock a⦄ (Val v) (hp s) xs"
    by(fastforce simp add: sim_move01_def ta_bisim_def)
  ultimately show ?case using ‹lcl s ⊆⇩m [Vs [↦] xs]› by fastforce
next
  case (RedWhile b c s Vs E2 xs)
  from ‹bisim Vs (while (b) c) E2 xs› have "E2 = while (compE1 Vs b) (compE1 Vs c)"
    and sync: "¬ contains_insync b" "¬ contains_insync c" by auto
  moreover have "False,compP1 P,t ⊢1 ⟨while(compE1 Vs b) (compE1 Vs c), (hp s, xs)⟩ 
                 -ε→ ⟨if (compE1 Vs b) (compE1 Vs c;;while(compE1 Vs b) (compE1 Vs c)) else unit, (hp s, xs)⟩"
    by(rule Red1While)
  hence "sim_move01 (compP1 P) t ε (while (b) c) (while (compE1 Vs b) (compE1 Vs c)) (hp s) xs ε (if (compE1 Vs b) (compE1 Vs c;;while(compE1 Vs b) (compE1 Vs c)) else unit) (hp s) xs"
    by(auto simp add: sim_move01_def)
  moreover from ‹fv (while (b) c) ⊆ set Vs› sync
  have "bisim Vs (if (b) (c;; while (b) c) else unit)
                 (if (compE1 Vs b) (compE1 Vs (c;; while(b) c)) else (compE1 Vs unit)) xs"
    by -(rule bisimCond, auto)
  ultimately show ?case using ‹lcl s ⊆⇩m [Vs [↦] xs]›
    by(simp)((rule exI)+, erule conjI, auto)
next
  case (RedTryCatch s a D C V e2 Vs E2 xs)
  thus ?case by(auto intro!: exI)(auto intro!: compE1_bisim)
next
  case RedTryFail thus ?case by(auto intro!: exI)
next
  case (ListRed1 e s ta e' s' es Vs ES2 xs)
  note IH = ‹⋀vs e2 XS. ⟦bisim vs e e2 XS; fv e ⊆ set vs; lcl s ⊆⇩m [vs [↦] XS]; length vs + max_vars e ≤ length XS;
                         ?synth e s⟧ ⟹ ?concl e e2 s XS e' s' ta vs›
  from ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisims Vs (e # es) ES2 xs› obtain E' 
    where "bisim Vs e E' xs" and ES2: "ES2 = E' # compEs1 Vs es" 
    and sync: "¬ contains_insyncs es" by(auto simp add: compEs1_conv_map)
  with IH[of Vs E' xs] ‹fvs (e # es) ⊆ set Vs› ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹extTA2J0 P,P,t ⊢ ⟨e,s⟩ -ta→ ⟨e',s'⟩›
    ‹length Vs + max_varss (e # es) ≤ length xs› ‹?synths (e # es) s› ‹¬ is_val e›
  show ?case by(cases "is_val e'")(fastforce elim!: sim_moves01_expr split: if_split_asm)+
next
  case (ListRed2 es s ta es' s' v Vs ES2 xs)
  thus ?case by(fastforce elim!: bisims_cases elim!: sim_moves01_expr)
next
  case CallThrowParams thus ?case
    by(fastforce elim!:bisim_cases simp add: bisims_map_Val_Throw)
next
  case (BlockThrow V T vo a s Vs e2 xs) thus ?case
    by(cases vo)(fastforce elim!: bisim_cases)+
next    
  case (SynchronizedThrow2 a ad s Vs E2 xs)
  from ‹bisim Vs (insync(a) Throw ad) E2 xs› have "xs ! length Vs = Addr a" by auto
  with ‹length Vs + max_vars (insync(a) Throw ad) ≤ length xs›
  have "False,compP1 P,t ⊢1 ⟨insync⇘length Vs⇙ (a) Throw ad, (hp s, xs)⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Throw ad, (hp s, xs)⟩"
    by-(rule Synchronized1Throw2, auto)
  hence "sim_move01 (compP1 P) t ⦃Unlock→a, SyncUnlock a⦄ (insync(a) Throw ad) (insync⇘length Vs⇙ (a) Throw ad) (hp s) xs ⦃Unlock→a, SyncUnlock a⦄ (Throw ad) (hp s) xs"
    by(fastforce simp add: sim_move01_def ta_bisim_def fun_eq_iff expand_finfun_eq finfun_upd_apply ta_upd_simps split: if_split_asm)
  moreover note ‹lcl s ⊆⇩m [Vs [↦] xs]› ‹bisim Vs (insync(a) Throw ad) E2 xs›
  ultimately show ?case by(fastforce)
next
  case InstanceOfRed thus ?case by(fastforce)
next
  case RedInstanceOf thus ?case by(auto intro!: exI)
next
  case InstanceOfThrow thus ?case by fastforce
qed(fastforce simp del: fun_upd_apply split: if_split_asm)+

end

declare max_dest [iff del]

declare split_paired_Ex [simp del]

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

| "countInitBlocks [] = 0"
| "countInitBlocks (e # es) = countInitBlock e + countInitBlocks es"

context J0_J1_heap_base begin

lemmas τred0r_expr =
  NewArray_τred0r_xt Cast_τred0r_xt InstanceOf_τred0r_xt BinOp_τred0r_xt1 BinOp_τred0r_xt2 LAss_τred0r
  AAcc_τred0r_xt1 AAcc_τred0r_xt2 AAss_τred0r_xt1 AAss_τred0r_xt2 AAss_τred0r_xt3
  ALength_τred0r_xt FAcc_τred0r_xt FAss_τred0r_xt1 FAss_τred0r_xt2
  CAS_τred0r_xt1 CAS_τred0r_xt2 CAS_τred0r_xt3 Call_τred0r_obj
  Call_τred0r_param Block_τred0r_xt Sync_τred0r_xt InSync_τred0r_xt
  Seq_τred0r_xt Cond_τred0r_xt Throw_τred0r_xt Try_τred0r_xt

lemmas τred0t_expr =
  NewArray_τred0t_xt Cast_τred0t_xt InstanceOf_τred0t_xt BinOp_τred0t_xt1 BinOp_τred0t_xt2 LAss_τred0t
  AAcc_τred0t_xt1 AAcc_τred0t_xt2 AAss_τred0t_xt1 AAss_τred0t_xt2 AAss_τred0t_xt3
  ALength_τred0t_xt FAcc_τred0t_xt FAss_τred0t_xt1 FAss_τred0t_xt2
  CAS_τred0t_xt1 CAS_τred0t_xt2 CAS_τred0t_xt3 Call_τred0t_obj
  Call_τred0t_param Block_τred0t_xt Sync_τred0t_xt InSync_τred0t_xt
  Seq_τred0t_xt Cond_τred0t_xt Throw_τred0t_xt Try_τred0t_xt

declare τred0r_expr [elim!]
declare τred0t_expr [elim!]

definition sim_move10 :: 
  "'addr J_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 ⇒ 'addr expr1 ⇒ 'addr expr
  ⇒ 'heap ⇒ 'addr locals ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr ⇒ 'heap ⇒ 'addr locals ⇒ bool"
where
  "sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs' ⟷ ¬ final e1 ∧
  (if τmove1 P h e1 then (τred0t (extTA2J0 P) P t h (e, xs) (e', xs') ∨ countInitBlock e1' < countInitBlock e1 ∧ e' = e ∧ xs' = xs) ∧ h' = h ∧ ta1 = ε ∧ ta = ε
   else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) ∧
     (if call e = None ∨ call1 e1 = None 
      then (∃e'' xs''. τred0r (extTA2J0 P) P t h (e, xs) (e'', xs'') ∧ extTA2J0 P,P,t ⊢ ⟨e'', (h, xs'')⟩ -ta→ ⟨e', (h', xs')⟩ ∧ no_call P h e'' ∧ ¬ τmove0 P h e'')
      else extTA2J0 P,P,t ⊢ ⟨e, (h, xs)⟩ -ta→ ⟨e', (h', xs')⟩ ∧ no_call P h e ∧ ¬ τmove0 P h e))"

definition sim_moves10 :: 
  "'addr J_prog ⇒ 'thread_id ⇒ ('addr, 'thread_id, 'heap) external_thread_action ⇒ 'addr expr1 list ⇒ 'addr expr1 list
  ⇒ 'addr expr list ⇒ 'heap ⇒ 'addr locals ⇒ ('addr, 'thread_id, 'heap) J0_thread_action ⇒ 'addr expr list ⇒ 'heap 
  ⇒ 'addr locals ⇒ bool"
where
  "sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs' ⟷ ¬ finals es1 ∧
  (if τmoves1 P h es1 then (τreds0t (extTA2J0 P) P t h (es, xs) (es', xs') ∨ countInitBlocks es1' < countInitBlocks es1 ∧ es' = es ∧ xs' = xs) ∧ h' = h ∧ ta1 = ε ∧ ta = ε
   else ta_bisim01 ta (extTA2J1 (compP1 P) ta1) ∧
     (if calls es = None ∨ calls1 es1 = None
      then (∃es'' xs''. τreds0r (extTA2J0 P) P t h (es, xs) (es'', xs'') ∧ extTA2J0 P,P,t ⊢ ⟨es'', (h, xs'')⟩ [-ta→] ⟨es', (h', xs')⟩ ∧ no_calls P h es'' ∧ ¬ τmoves0 P h es'')
      else extTA2J0 P,P,t ⊢ ⟨es, (h, xs)⟩ [-ta→] ⟨es', (h', xs')⟩ ∧ no_calls P h es ∧ ¬ τmoves0 P h es))"

lemma sim_move10_expr:
  assumes "sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs'"
  shows
  "sim_move10 P t ta1 (newA T⌊e1⌉) (newA T⌊e1'⌉) (newA T⌊e⌉) h xs ta (newA T⌊e'⌉) h' xs'"
  "sim_move10 P t ta1 (Cast T e1) (Cast T e1') (Cast T e) h xs ta (Cast T e') h' xs'"
  "sim_move10 P t ta1 (e1 instanceof T) (e1' instanceof T) (e instanceof T) h xs ta (e' instanceof T) h' xs'"
  "sim_move10 P t ta1 (e1 «bop» e2) (e1' «bop» e2) (e «bop» e2') h xs ta (e' «bop» e2') h' xs'"
  "sim_move10 P t ta1 (Val v «bop» e1) (Val v «bop» e1') (Val v «bop» e) h xs ta (Val v «bop» e') h' xs'"
  "sim_move10 P t ta1 (V := e1) (V := e1') (V' := e) h xs ta (V' := e') h' xs'"
  "sim_move10 P t ta1 (e1⌊e2⌉) (e1'⌊e2⌉) (e⌊e2'⌉) h xs ta (e'⌊e2'⌉) h' xs'"
  "sim_move10 P t ta1 (Val v⌊e1⌉) (Val v⌊e1'⌉) (Val v⌊e⌉) h xs ta (Val v⌊e'⌉) h' xs'"
  "sim_move10 P t ta1 (e1⌊e2⌉ := e3) (e1'⌊e2⌉ := e3) (e⌊e2'⌉ := e3') h xs ta (e'⌊e2'⌉ := e3') h' xs'"
  "sim_move10 P t ta1 (Val v⌊e1⌉ := e3) (Val v⌊e1'⌉ := e3) (Val v⌊e⌉ := e3') h xs ta (Val v⌊e'⌉ := e3') h' xs'"
  "sim_move10 P t ta1 (AAss (Val v) (Val v') e1) (AAss (Val v) (Val v') e1') (AAss (Val v) (Val v') e) h xs ta (AAss (Val v) (Val v') e') h' xs'"
  "sim_move10 P t ta1 (e1∙length) (e1'∙length) (e∙length) h xs ta (e'∙length) h' xs'"
  "sim_move10 P t ta1 (e1∙F{D}) (e1'∙F{D}) (e∙F'{D'}) h xs ta (e'∙F'{D'}) h' xs'"
  "sim_move10 P t ta1 (FAss e1 F D e2) (FAss e1' F D e2) (FAss e F' D' e2') h xs ta (FAss e' F' D' e2') h' xs'"
  "sim_move10 P t ta1 (FAss (Val v) F D e1) (FAss (Val v) F D e1') (FAss (Val v) F' D' e) h xs ta (FAss (Val v) F' D' e') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap e1 F D e2 e3) (CompareAndSwap e1' F D e2 e3) (CompareAndSwap e F' D' e2' e3') h xs ta (CompareAndSwap e' F' D' e2' e3') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap (Val v) F D e1 e3) (CompareAndSwap (Val v) F D e1' e3) (CompareAndSwap (Val v) F' D' e e3') h xs ta (CompareAndSwap (Val v) F' D' e' e3') h' xs'"
  "sim_move10 P t ta1 (CompareAndSwap (Val v) F D (Val v') e1) (CompareAndSwap (Val v) F D (Val v') e1') (CompareAndSwap (Val v) F' D' (Val v') e) h xs ta (CompareAndSwap (Val v) F' D' (Val v') e') h' xs'"
  "sim_move10 P t ta1 (e1∙M(es)) (e1'∙M(es)) (e∙M(es')) h xs ta (e'∙M(es')) h' xs'"
  "sim_move10 P t ta1 (sync⇘V⇙(e1) e2) (sync⇘V⇙(e1') e2) (sync(e) e2') h xs ta (sync(e') e2') h' xs'"
  "sim_move10 P t ta1 (insync⇘V⇙(a) e1) (insync⇘V⇙(a) e1') (insync(a') e) h xs ta (insync(a') e') h' xs'"
  "sim_move10 P t ta1 (e1;;e2) (e1';;e2) (e;;e2') h xs ta (e';;e2') h' xs'"
  "sim_move10 P t ta1 (if (e1) e2 else e3) (if (e1') e2 else e3) (if (e) e2' else e3') h xs ta (if (e') e2' else e3') h' xs'"
  "sim_move10 P t ta1 (throw e1) (throw e1') (throw e) h xs ta (throw e') h' xs'"
  "sim_move10 P t ta1 (try e1 catch(C V) e2) (try e1' catch(C V) e2) (try e catch(C' V') e2') h xs ta (try e' catch(C' V') e2') h' xs'"
using assms
apply(simp_all add: sim_move10_def final_iff split del: if_split split: if_split_asm)
apply(fastforce simp: τred0t_Val τred0r_Val intro: red_reds.intros split!: if_splits)+
done

lemma sim_moves10_expr:
  "sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs' ⟹ sim_moves10 P t ta1 (e1 # es2) (e1' # es2) (e # es2') h xs ta (e' # es2') h' xs'"
  "sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs' ⟹ sim_moves10 P t ta1 (Val v # es1) (Val v # es1') (Val v # es) h xs ta (Val v # es') h' xs'"
unfolding sim_moves10_def sim_move10_def final_iff finals_iff
apply(simp_all add: Cons_eq_append_conv split del: if_split split: if_split_asm)
apply(safe intro!: if_split)
apply(fastforce simp add: is_vals_conv τreds0t_map_Val τreds0r_map_Val τred0t_Val τred0r_Val intro!: τred0r_inj_τreds0r τreds0r_cons_τreds0r τred0t_inj_τreds0t τreds0t_cons_τreds0t ListRed1 ListRed2 split: if_split_asm)+
done

lemma sim_move10_CallParams:
  "sim_moves10 P t ta1 es1 es1' es h xs ta es' h' xs'
  ⟹ sim_move10 P t ta1 (Val v∙M(es1)) (Val v∙M(es1')) (Val v∙M(es)) h xs ta (Val v∙M(es')) h' xs'"
unfolding sim_move10_def sim_moves10_def
apply(simp split: if_split_asm split del: if_split add: is_vals_conv)
  apply(fastforce simp add: τred0t_Val τred0r_Val τreds0t_map_Val τreds0r_map_Val intro: Call_τred0r_param Call_τred0t_param CallParams split: if_split_asm split del: if_split intro!: if_split)
 apply(rule conjI)
  apply fastforce
 apply(rule if_intro)
  apply fastforce
 apply(clarsimp split del: if_split)
 apply(rule if_intro)
  apply(clarsimp split: if_split_asm simp add: is_vals_conv)
   apply(rule exI conjI)+
    apply(erule Call_τred0r_param)
   apply(fastforce intro: CallParams)
  apply(rule exI conjI)+
   apply(erule Call_τred0r_param)
  apply(fastforce intro!: CallParams)
 apply(clarsimp split del: if_split split: if_split_asm simp add: is_vals_conv τreds0r_map_Val)
 apply fastforce
apply(rule conjI)
 apply fastforce
apply(rule if_intro)
 apply fastforce
apply(rule conjI)
 apply fastforce
apply(rule if_intro)
 apply(clarsimp split: if_split_asm)
apply(clarsimp split: if_split_asm split del: if_split simp add: is_vals_conv)
apply(fastforce intro: CallParams)
done

lemma sim_move10_Block:
  "sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'
  ⟹ sim_move10 P t ta1 ({V:T=None; e1}) ({V:T=None; e1'}) ({V':T=vo; e}) h xs ta ({V':T=xs' V'; e'}) h' (xs'(V' := xs V'))"
proof -
  assume "sim_move10 P t ta1 e1 e1' e h (xs(V' := vo)) ta e' h' xs'"
  moreover {
    fix e'' xs''
    assume "extTA2J0 P,P,t ⊢ ⟨e'',(h, xs'')⟩ -ta→ ⟨e',(h', xs')⟩"
    hence "extTA2J0 P,P,t ⊢ ⟨e'',(h, xs''(V' := xs V', V' := xs'' V'))⟩ -ta→ ⟨e',(h', xs')⟩" by simp
    from BlockRed[OF this, of T]
    have "extTA2J0 P,P,t ⊢ ⟨{V':T=xs'' V'; e''},(h, xs''(V' := xs V'))⟩ -ta→ ⟨{V':T=xs' V'; e'},(h', xs'(V' := xs V'))⟩"
      by simp }
  ultimately show ?thesis
    by(fastforce simp add: sim_move10_def final_iff split: if_split_asm)
qed

lemma sim_move10_reds:
  "⟦ (h', a) ∈ allocate h (Class_type C); ta1 = ⦃NewHeapElem a (Class_type C)⦄; ta = ⦃NewHeapElem a (Class_type C)⦄ ⟧
  ⟹ sim_move10 P t ta1 (new C) e1' (new C) h xs ta (addr a) h' xs"
  "allocate h (Class_type C) = {} ⟹ sim_move10 P t ε (new C) e1' (new C) h xs ε (THROW OutOfMemory) h xs"
  "⟦ (h', a) ∈ allocate h (Array_type T (nat (sint i))); 0 <=s i;
     ta1 = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄; ta = ⦃NewHeapElem a (Array_type T (nat (sint i)))⦄ ⟧
  ⟹ sim_move10 P t ta1 (newA T⌊Val (Intg i)⌉) e1' (newA T⌊Val (Intg i)⌉) h xs ta (addr a) h' xs"
  "i <s 0 ⟹ sim_move10 P t ε (newA T⌊Val (Intg i)⌉) e1' (newA T⌊Val (Intg i)⌉) h xs ε (THROW NegativeArraySize) h xs"
  "⟦ allocate h (Array_type T (nat (sint i))) = {}; 0 <=s i ⟧
  ⟹ sim_move10 P t ε (newA T⌊Val (Intg i)⌉) e1' (newA T⌊Val (Intg i)⌉) h xs ε (THROW OutOfMemory) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; P ⊢ U ≤ T ⟧
  ⟹ sim_move10 P t ε (Cast T (Val v)) e1' (Cast T (Val v)) h xs ε (Val v) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; ¬ P ⊢ U ≤ T ⟧
  ⟹ sim_move10 P t ε (Cast T (Val v)) e1' (Cast T (Val v)) h xs ε (THROW ClassCast) h xs"
  "⟦ typeof⇘h⇙ v = ⌊U⌋; b ⟷ v ≠ Null ∧ P ⊢ U ≤ T ⟧
  ⟹ sim_move10 P t ε ((Val v) instanceof T) e1' ((Val v) instanceof T) h xs ε (Val (Bool b)) h xs"
  "binop bop v1 v2 = Some (Inl v) ⟹ sim_move10 P t ε ((Val v1) «bop» (Val v2)) e1' (Val v1 «bop» Val v2) h xs ε (Val v) h xs"
  "binop bop v1 v2 = Some (Inr a) ⟹ sim_move10 P t ε ((Val v1) «bop» (Val v2)) e1' (Val v1 «bop» Val v2) h xs ε (Throw a) h xs"
  "xs V = ⌊v⌋ ⟹ sim_move10 P t ε (Var V') e1' (Var V) h xs ε (Val v) h xs"
  "sim_move10 P t ε (V' := Val v) e1' (V := Val v) h xs ε unit h (xs(V ↦ v))"
  "sim_move10 P t ε (null⌊Val v⌉) e1' (null⌊Val v⌉) h xs ε (THROW NullPointer) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
  ⟹ sim_move10 P t ε (addr a⌊Val (Intg i)⌉) e1' ((addr a)⌊Val (Intg i)⌉) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n;
     heap_read h a (ACell (nat (sint i))) v;
     ta1 = ⦃ReadMem a (ACell (nat (sint i))) v⦄; ta = ⦃ReadMem a (ACell (nat (sint i))) v⦄ ⟧
  ⟹ sim_move10 P t ta1 (addr a⌊Val (Intg i)⌉) e1' ((addr a)⌊Val (Intg i)⌉) h xs ta (Val v) h xs"
  "sim_move10 P t ε (null⌊Val v⌉ := Val v') e1' (null⌊Val v⌉ := Val v') h xs ε (THROW NullPointer) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; i <s 0 ∨ sint i ≥ int n ⟧
  ⟹ sim_move10 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayIndexOutOfBounds) h xs"
 "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = ⌊U⌋; ¬ (P ⊢ U ≤ T) ⟧
  ⟹ sim_move10 P t ε (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs ε (THROW ArrayStore) h xs"
  "⟦ typeof_addr h a = ⌊Array_type T n⌋; 0 <=s i; sint i < int n; typeof⇘h⇙ v = Some U; P ⊢ U ≤ T;
     heap_write h a (ACell (nat (sint i))) v h';
     ta1 = ⦃WriteMem a (ACell (nat (sint i))) v⦄; ta = ⦃WriteMem a (ACell (nat (sint i))) v⦄ ⟧
  ⟹ sim_move10 P t ta1 (AAss (addr a) (Val (Intg i)) (Val v)) e1' (AAss (addr a) (Val (Intg i)) (Val v)) h xs ta unit h' xs"
  "typeof_addr h a = ⌊Array_type T n⌋ ⟹ sim_move10 P t ε (addr a∙length) e1' (addr a∙length) h xs ε (Val (Intg (word_of_nat n))) h xs"
  "sim_move10 P t ε (null∙length) e1' (null∙length) h xs ε (THROW NullPointer) h xs"
  "⟦ heap_read h a (CField D F) v; ta1 = ⦃ReadMem a (CField D F) v⦄; ta = ⦃ReadMem a (CField D F) v⦄ ⟧
  ⟹ sim_move10 P t ta1 (addr a∙F{D}) e1' (addr a∙F{D}) h xs ta (Val v) h xs"
  "sim_move10 P t ε (null∙F{D}) e1' (null∙F{D}) h xs ε (THROW NullPointer) h xs"
  "⟦ heap_write h a (CField D F) v h'; ta1 = ⦃WriteMem a (CField D F) v⦄; ta = ⦃WriteMem a (CField D F) v⦄ ⟧
  ⟹ sim_move10 P t ta1 (addr a∙F{D} := Val v) e1' (addr a∙F{D} := Val v) h xs ta unit h' xs"
  "sim_move10 P t ε (null∙compareAndSwap(D∙F, Val v, Val v')) e1' (null∙compareAndSwap(D∙F, Val v, Val v')) h xs ε (THROW NullPointer) h xs"
  "⟦ heap_read h a (CField D F) v''; heap_write h a (CField D F) v' h'; v'' = v;
     ta1 = ⦃ ReadMem a (CField D F) v'', WriteMem a (CField D F) v' ⦄; ta = ⦃ ReadMem a (CField D F) v'', WriteMem a (CField D F) v' ⦄ ⟧
  ⟹ sim_move10 P t ta1 (addr a∙compareAndSwap(D∙F, Val v, Val v')) e1' (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta true h' xs"
  "⟦ heap_read h a (CField D F) v''; v'' ≠ v;
     ta1 = ⦃ ReadMem a (CField D F) v'' ⦄; ta = ⦃ ReadMem a (CField D F) v'' ⦄ ⟧
  ⟹ sim_move10 P t ta1 (addr a∙compareAndSwap(D∙F, Val v, Val v')) e1' (addr a∙compareAndSwap(D∙F, Val v, Val v')) h xs ta false h xs"

  "sim_move10 P t ε (null∙F{D} := Val v) e1' (null∙F{D} := Val v) h xs ε (THROW NullPointer) h xs"
  "sim_move10 P t ε ({V':T=None; Val u}) e1' ({V:T=vo; Val u}) h xs ε (Val u) h xs"
  "sim_move10 P t ε ({V':T=⌊v⌋; e}) ({V':T=None; e}) ({V:T=vo; e'}) h xs ε ({V:T=vo; e'}) h xs"

  "sim_move10 P t ε (sync⇘V'⇙(null) e0) e1' (sync(null) e1) h xs ε (THROW NullPointer) h xs"
  "sim_move10 P t ε (Val v;;e0) e1' (Val v;; e1) h xs ε e1 h xs"
  "sim_move10 P t ε (if (true) e0 else e0') e1' (if (true) e1 else e2) h xs ε e1 h xs"
  "sim_move10 P t ε (if (false) e0 else e0') e1' (if (false) e1 else e2) h xs ε e2 h xs"
  "sim_move10 P t ε (throw null) e1' (throw null) h xs ε (THROW NullPointer) h xs"
  "sim_move10 P t ε (try (Val v) catch(C V') e0) e1' (try (Val v) catch(C V) e1) h xs ε (Val v) h xs"
  "⟦ typeof_addr h a = ⌊Class_type D⌋; P ⊢ D ≼⇧* C ⟧
  ⟹ sim_move10 P t ε (try (Throw a) catch(C V') e0) e1' (try (Throw a) catch(C V) e1) h xs ε ({V:Class C=⌊Addr a⌋; e1}) h xs"
  "sim_move10 P t ε (newA T⌊Throw a⌉) e1' (newA T⌊Throw a⌉) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Cast T (Throw a)) e1' (Cast T (Throw a)) h xs ε (Throw a) h xs"
  "sim_move10 P t ε ((Throw a) instanceof T) e1' ((Throw a) instanceof T) h xs ε (Throw a) h xs"
  "sim_move10 P t ε ((Throw a) «bop» e0) e1' ((Throw a) «bop» e1) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v «bop» (Throw a)) e1' (Val v «bop» (Throw a)) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (V' := Throw a) e1' (V := Throw a) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a⌊e0⌉) e1' (Throw a⌊e1⌉) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v⌊Throw a⌉) e1' (Val v⌊Throw a⌉) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a⌊e0⌉ := e0') e1' (Throw a⌊e1⌉ := e2) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v⌊Throw a⌉ := e0) e1' (Val v⌊Throw a⌉ := e1) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v⌊Val v'⌉ := Throw a) e1' (Val v⌊Val v'⌉ := Throw a) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a∙length) e1' (Throw a∙length) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a∙F{D}) e1' (Throw a∙F{D}) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a∙F{D} := e0) e1' (Throw a∙F{D} := e1) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v∙F{D} := Throw a) e1' (Val v∙F{D} := Throw a) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (CompareAndSwap (Throw a) D F e0 e0') e1' (Throw a∙compareAndSwap(D∙F, e1'', e1''')) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (CompareAndSwap (Val v) D F (Throw a) e0') e1' (Val v∙compareAndSwap(D∙F, Throw a, e1'')) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (CompareAndSwap (Val v) D F (Val v') (Throw a)) e1' (Val v∙compareAndSwap(D∙F, Val v', Throw a)) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a∙M(es0)) e1' (Throw a∙M(es1)) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Val v∙M(map Val vs @ Throw a # es0)) e1' (Val v∙M(map Val vs @ Throw a # es1)) h xs ε (Throw a) h xs"
  "sim_move10 P t ε ({V':T=None; Throw a}) e1' ({V:T=vo; Throw a}) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (sync⇘V'⇙(Throw a) e0) e1' (sync(Throw a) e1) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (Throw a;;e0) e1' (Throw a;;e1) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (if (Throw a) e0 else e0') e1' (if (Throw a) e1 else e2) h xs ε (Throw a) h xs"
  "sim_move10 P t ε (throw (Throw a)) e1' (throw (Throw a)) h xs ε (Throw a) h xs"
apply(fastforce simp add: sim_move10_def no_calls_def no_call_def ta_bisim_def intro: red_reds.intros)+
done

lemma sim_move10_CallNull:
  "sim_move10 P t ε (null∙M(map Val vs)) e1' (null∙M(map Val vs)) h xs ε (THROW NullPointer) h xs"
by(fastforce simp add: sim_move10_def map_eq_append_conv intro: RedCallNull)

lemma sim_move10_SyncLocks:
  "⟦ ta1 = ⦃Lock→a, SyncLock a⦄; ta = ⦃Lock→a, SyncLock a⦄ ⟧
   ⟹ sim_move10 P t ta1 (sync⇘V⇙(addr a) e0) e1' (sync(addr a) e1) h xs ta (insync(a) e1) h xs"
  "⟦ ta1 = ⦃Unlock→a, SyncUnlock a⦄; ta = ⦃Unlock→a, SyncUnlock a⦄ ⟧
  ⟹ sim_move10 P t ta1 (insync⇘V⇙(a') (Val v)) e1' (insync(a) (Val v)) h xs ta (Val v) h xs"
  "⟦ ta1 = ⦃Unlock→a, SyncUnlock a⦄; ta = ⦃Unlock→a, SyncUnlock a⦄ ⟧
  ⟹ sim_move10 P t ta1 (insync⇘V⇙(a') (Throw a'')) e1' (insync(a) (Throw a'')) h xs ta (Throw a'') h xs"
by(fastforce simp add: sim_move10_def ta_bisim_def ta_upd_simps intro: red_reds.intros[simplified])+

lemma sim_move10_TryFail:
  "⟦ typeof_addr h a = ⌊Class_type D⌋; ¬ P ⊢ D ≼⇧* C ⟧
  ⟹ sim_move10 P t ε (try (Throw a) catch(C V') e0) e1' (try (Throw a) catch(C V) e1) h xs ε (Throw a) h xs"
by(auto simp add: sim_move10_def intro!: RedTryFail)

lemmas sim_move10_intros =
  sim_move10_expr sim_move10_reds sim_move10_CallNull sim_move10_TryFail sim_move10_Block sim_move10_CallParams

lemma sim_move10_preserves_defass:
  assumes wf: "wf_J_prog P"
  shows "⟦ sim_move10 P t ta1 e1 e1' e h xs ta e' h' xs'; 𝒟 e ⌊dom xs⌋ ⟧ ⟹ 𝒟 e' ⌊dom xs'⌋"
by(auto simp add: sim_move10_def split: if_split_asm dest!: τred0r_preserves_defass[OF wf] τred0t_preserves_defass[OF wf] red_preserves_defass[OF wf])

declare sim_move10_intros[intro]

lemma assumes wf: "wf_J_prog P"
  shows red_simulates_red1_aux:
  "⟦ False,compP1 P,t ⊢1 ⟨e1, S⟩ -TA→ ⟨e1', S'⟩; bisim vs e2 e1 (lcl S); fv e2 ⊆ set vs;
     x ⊆⇩m [vs [↦] lcl S]; length vs + max_vars e1 ≤ length (lcl S);
     𝒟 e2 ⌊dom x⌋ ⟧
  ⟹ ∃ta e2' x'. sim_move10 P t TA e1 e1' e2 (hp S) x ta e2' (hp S') x' ∧ bisim vs e2' e1' (lcl S') ∧ x' ⊆⇩m [vs [↦] lcl S']"
  (is "⟦ _; _; _; _; _; _ ⟧ ⟹ ?concl e1 e1' e2 S x TA S' e1' vs")

  and reds_simulates_reds1_aux:
  "⟦ False,compP1 P,t ⊢1 ⟨es1, S⟩ [-TA→] ⟨es1', S'⟩; bisims vs es2 es1 (lcl S); fvs es2 ⊆ set vs;
     x ⊆⇩m [vs [↦] lcl S]; length vs + max_varss es1 ≤ length (lcl S);
     𝒟s es2 ⌊dom x⌋ ⟧
  ⟹ ∃ta es2' x'. sim_moves10 P t TA es1 es1' es2 (hp S) x ta es2' (hp S') x' ∧ bisims vs es2' es1' (lcl S') ∧ x' ⊆⇩m [vs [↦] lcl S']"
  (is "⟦ _; _; _; _; _; _ ⟧ ⟹ ?concls es1 es1' es2 S x TA S' es1' vs")
proof(induct arbitrary: vs e2 x and vs es2 x rule: red1_reds1.inducts)
  case (Bin1OpRed1 e s ta e' s' bop e2 Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
             ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs E2 (e «bop» e2) (lcl s)› obtain E E2'
    where E2: "E2 = E «bop» E2'" "e2 = compE1 Vs E2'" and "bisim Vs E e (lcl s)"
    and sync: "¬ contains_insync E2'"
    by(auto elim!: bisim_cases)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (e «bop» e2) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  with E2 ‹fv E2 ⊆ set Vs› sync show ?case by(cases "is_val e2'")(auto intro: BinOpRed1)
next
  case (Bin1OpRed2 e s ta e' s' v bop Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
              ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹bisim Vs E2 (Val v «bop» e) (lcl s)› obtain E 
    where E2: "E2 = Val v «bop» E" and "bisim Vs E e (lcl s)" by(auto)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (Val v «bop» e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋› E2
  ultimately show ?case by(auto intro: BinOpRed2)
next
  case (Red1Var s V v Vs E2 X)
  from ‹bisim Vs E2 (Var V) (lcl s)› ‹fv E2 ⊆ set Vs›
  obtain V' where "E2 = Var V'" "V' = Vs ! V" "V = index Vs V'" by(clarify, simp)
  from ‹E2 = Var V'› ‹𝒟 E2 ⌊dom X⌋›
  obtain v' where "X V' = ⌊v'⌋" by(auto simp add: hyperset_defs)
  with ‹X ⊆⇩m [Vs [↦] lcl s]› have "[Vs [↦] lcl s] V' = ⌊v'⌋" by(rule map_le_SomeD)
  with ‹length Vs + max_vars (Var V) ≤ length (lcl s)›
  have "lcl s ! (index Vs V') = v'" by(auto intro: map_upds_Some_eq_nth_index)
  with ‹V = index Vs V'› ‹lcl s ! V = v› have "v = v'" by simp
  with ‹X V' = ⌊v'⌋› ‹E2 = Var V'› ‹X ⊆⇩m [Vs [↦] lcl s]›
  show ?case by(fastforce intro: RedVar)
next
  case (LAss1Red e s ta e' s' V Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹bisim Vs E2 (V:=e) (lcl s)› obtain E V'
    where E2: "E2 = (V':=E)" "V = index Vs V'" and "bisim Vs E e (lcl s)" by auto
  with IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (V:=e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
    E2 show ?case by(auto intro: LAssRed)
next
  case (Red1LAss V l v h Vs E2 X)
  from ‹bisim Vs E2 (V:=Val v) (lcl (h, l))› obtain V' where "E2 = (V' := Val v)" "V = index Vs V'" by(auto)
  moreover with ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl (h, l)]› ‹length Vs + max_vars (V:=Val v) ≤ length (lcl (h, l))›
  have "X(V' ↦ v) ⊆⇩m [Vs [↦] l[index Vs V' := v]]" by(auto intro: LAss_lem)
  ultimately show ?case by(auto intro: RedLAss simp del: fun_upd_apply)
next
  case (AAcc1Red1 a s ta a' s' i Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 a (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars a ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
             ⟹ ?concl a a' e2 s x ta s' a' vs›
  from ‹False,compP1 P,t ⊢1 ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
  with ‹bisim Vs E2 (a⌊i⌉) (lcl s)› obtain E E2'
    where E2: "E2 = E⌊E2'⌉" "i = compE1 Vs E2'" and "bisim Vs E a (lcl s)"
    and sync: "¬ contains_insync E2'" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (a⌊i⌉) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where "sim_move10 P t ta a a' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' a' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  with E2 ‹fv E2 ⊆ set Vs› sync show ?case
    by(cases "is_val e2'")(auto intro: AAccRed1)
next
  case (AAcc1Red2 i s ta i' s' a Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 i (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars i ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl i i' e2 s x ta s' i' vs›
  from ‹bisim Vs E2 (Val a⌊i⌉) (lcl s)› obtain E 
    where E2: "E2 = Val a⌊E⌉" and "bisim Vs E i (lcl s)" by(auto)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]› E2
    ‹length Vs + max_vars (Val a⌊i⌉) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately show ?case by(auto intro: AAccRed2)
next
  case Red1AAcc thus ?case by(fastforce intro: RedAAcc simp del: fun_upd_apply)
next
  case (AAss1Red1 a s ta a' s' i e Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 a (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars a ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋ ⟧
             ⟹ ?concl a a' e2 s x ta s' a' vs›
  from ‹False,compP1 P,t ⊢1 ⟨a,s⟩ -ta→ ⟨a',s'⟩› have "¬ is_val a" by auto
  with ‹bisim Vs E2 (a⌊i⌉:=e) (lcl s)› obtain E E2' E2''
    where E2: "E2 = E⌊E2'⌉:=E2''" "i = compE1 Vs E2'" "e = compE1 Vs E2''" and "bisim Vs E a (lcl s)"
    and sync: "¬ contains_insync E2'" "¬ contains_insync E2''" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (a⌊i⌉:=e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where IH': "sim_move10 P t ta a a' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' a' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  show ?case
  proof(cases "is_val e2'")
    case True
    from E2 ‹fv E2 ⊆ set Vs› sync have "bisim Vs E2' i (lcl s')" "bisim Vs E2'' e (lcl s')" by auto
    with IH' E2 True sync show ?thesis
      by(cases "is_val E2'")(fastforce intro: AAssRed1)+
  next
    case False with IH' E2 sync show ?thesis by(fastforce intro: AAssRed1)
  qed
next
  case (AAss1Red2 i s ta i' s' a e Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 i (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars i ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl i i' e2 s x ta s' i' vs›
  from ‹False,compP1 P,t ⊢1 ⟨i,s⟩ -ta→ ⟨i',s'⟩› have "¬ is_val i" by auto
  with ‹bisim Vs E2 (Val a⌊i⌉:=e) (lcl s)› obtain E E2'
    where E2: "E2 = Val a⌊E⌉:=E2'" "e = compE1 Vs E2'" and "bisim Vs E i (lcl s)"
    and sync: "¬ contains_insync E2'" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (Val a⌊i⌉:=e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where "sim_move10 P t ta i i' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' i' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  with E2 ‹fv E2 ⊆ set Vs› sync show ?case
    by(cases "is_val e2'")(fastforce intro: AAssRed2)+
next
  case (AAss1Red3 e s ta e' s' a i Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹bisim Vs E2 (Val a⌊Val i⌉:=e) (lcl s)› obtain E
    where E2: "E2 = Val a⌊Val i⌉:=E" and "bisim Vs E e (lcl s)" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]› E2
    ‹length Vs + max_vars (Val a⌊Val i⌉:=e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately show ?case by(fastforce intro: AAssRed3)
next
  case Red1AAssStore thus ?case by(auto)((rule exI conjI)+, auto)
next
  case Red1AAss thus ?case 
    by(fastforce simp del: fun_upd_apply)
next 
  case (FAss1Red1 e s ta e' s' F D e2 Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
             ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs E2 (e∙F{D}:=e2) (lcl s)› obtain E E2'
    where E2: "E2 = E∙F{D}:=E2'" "e2 = compE1 Vs E2'" and "bisim Vs E e (lcl s)" 
    and sync: "¬ contains_insync E2'" by(fastforce)
  with IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (e∙F{D}:=e2) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  obtain TA' e2' x' where "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(fastforce)
  with E2 ‹fv E2 ⊆ set Vs› sync show ?case by(cases "is_val e2'")(auto intro: FAssRed1)
next 
  case (FAss1Red2 e s ta e' s' v F D Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹bisim Vs E2 (Val v∙F{D}:=e) (lcl s)› obtain E
    where E2: "E2 = (Val v∙F{D}:=E)" and "bisim Vs E e (lcl s)" by(fastforce)
  with IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (Val v∙F{D}:=e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
    E2 show ?case by(fastforce intro: FAssRed2)
next
  case (CAS1Red1 e s ta e' s' D F e2 e3 Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋ ⟧
             ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs E2 _ (lcl s)› obtain E E2' E2''
    where E2: "E2 = E∙compareAndSwap(D∙F, E2', E2'')" "e2 = compE1 Vs E2'" "e3 = compE1 Vs E2''" and "bisim Vs E e (lcl s)"
    and sync: "¬ contains_insync E2'" "¬ contains_insync E2''" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars _ ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where IH': "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  show ?case
  proof(cases "is_val e2'")
    case True
    from E2 ‹fv E2 ⊆ set Vs› sync have "bisim Vs E2' e2 (lcl s')" "bisim Vs E2'' e3 (lcl s')" by auto
    with IH' E2 True sync show ?thesis by(cases "is_val E2'")(fastforce)+
  next
    case False with IH' E2 sync show ?thesis by(fastforce)
  qed
next
  case (CAS1Red2 e s ta e' s' v D F e3 Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› have "¬ is_val e" by auto
  with ‹bisim Vs E2 _ (lcl s)› obtain E E2'
    where E2: "E2 = (Val v∙compareAndSwap(D∙F, E, E2'))" "e3 = compE1 Vs E2'" and "bisim Vs E e (lcl s)"
    and sync: "¬ contains_insync E2'" by(auto)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars _ ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(auto)
  with E2 ‹fv E2 ⊆ set Vs› sync show ?case
    by(cases "is_val e2'")(fastforce)+
next
  case (CAS1Red3 e s ta e' s' v D F v' Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
             x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
            ⟹ ?concl e e' e2 s x ta s' e' vs›
  from ‹bisim Vs E2 _ (lcl s)› obtain E
    where E2: "E2 = (Val v∙compareAndSwap(D∙F, Val v', E))" and "bisim Vs E e (lcl s)" by(fastforce)
  moreover note IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]› E2
    ‹length Vs + max_vars _ ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately show ?case by(fastforce)
next
  case (Call1Obj e s ta e' s' M es Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
            x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s);
            𝒟 e2 ⌊dom x⌋ ⟧ ⟹ ?concl e e' e2 s x ta s' e' vs› 
  from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› ‹bisim Vs E2 (e∙M(es)) (lcl s)›
  obtain E es' where E2: "E2 = E∙M(es')" "es = compEs1 Vs es'" and "bisim Vs E e (lcl s)"
    and sync: "¬ contains_insyncs es'" by(auto elim!: bisim_cases simp add: compEs1_conv_map)
  with IH[of Vs E X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (e∙M(es)) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  obtain TA' e2' x' where IH': "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by(fastforce)
  with E2 ‹fv E2 ⊆ set Vs› ‹E2 = E∙M(es')› sync show ?case
    by(cases "is_val e2'")(auto intro: CallObj)
next
  case (Call1Params es s ta es' s' v M Vs E2 X)
  note IH = ‹⋀vs es2 x. ⟦ bisims vs es2 es (lcl s); fvs es2 ⊆ set vs;
            x ⊆⇩m [vs [↦] lcl s]; length vs + max_varss es ≤ length (lcl s); 𝒟s es2 ⌊dom x⌋⟧ 
           ⟹ ?concls es es' es2 s x ta s' es' vs›
  from ‹bisim Vs E2 (Val v∙M(es)) (lcl s)› obtain Es
    where "E2 = Val v ∙M(Es)" "bisims Vs Es es (lcl s)" by(auto)
  with IH[of Vs Es X] ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_vars (Val v∙M(es)) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
    ‹E2 = Val v ∙M(Es)› show ?case by(fastforce intro: CallParams)
next
  case (Red1CallExternal s a T M Ts Tr D vs ta va h' e' s' Vs E2 X)
  from ‹bisim Vs E2 (addr a∙M(map Val vs)) (lcl s)› have E2: "E2 = addr a∙M(map Val vs)" by auto
  moreover from ‹compP1 P ⊢ class_type_of T sees M: Ts→Tr = Native in D›
  have "P ⊢ class_type_of T sees M: Ts→Tr = Native in D" by simp
  moreover from ‹compP1 P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
  have "P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩" by simp
  moreover from wf ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
  have "ta_bisim01 (extTA2J0 P ta) (extTA2J1 (compP1 P) ta)"
    by(rule red_external_ta_bisim01)
  moreover note ‹typeof_addr (hp s) a = ⌊T⌋› ‹e' = extRet2J1 (addr a∙M(map Val vs)) va› ‹s' = (h', lcl s)›
  moreover from ‹typeof_addr (hp s) a = ⌊T⌋› ‹P,t ⊢ ⟨a∙M(vs),hp s⟩ -ta→ext ⟨va,h'⟩›
    ‹P ⊢ class_type_of T sees M: Ts→Tr = Native in D›
  have "τexternal_defs D M ⟹ ta = ε ∧ h' = hp s"
    by(fastforce dest: τexternal'_red_external_heap_unchanged τexternal'_red_external_TA_empty simp add: τexternal'_def τexternal_def)
  ultimately show ?case using ‹X ⊆⇩m [Vs [↦] lcl s]›
    by(fastforce intro!: exI[where x="extTA2J0 P ta"] intro: RedCallExternal simp add: map_eq_append_conv sim_move10_def synthesized_call_def dest: sees_method_fun del: disjCI intro: disjI1 disjI2)
next
  case (Block1Red e h x ta e' h' x' V T Vs E2 X)
  note IH = ‹⋀vs e2 xa. ⟦ bisim vs e2 e (lcl (h, x)); fv e2 ⊆ set vs; xa ⊆⇩m [vs [↦] lcl (h, x)];
                       length vs + max_vars e ≤ length (lcl (h, x)); 𝒟 e2 ⌊dom xa⌋⟧
             ⟹ ?concl e e' e2 (h, x) xa ta (h', x') e' vs› 
  from ‹False,compP1 P,t ⊢1 ⟨e,(h, x)⟩ -ta→ ⟨e',(h', x')⟩›
  have "length x = length x'" by(auto dest: red1_preserves_len)
  with ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))›
  have "length Vs < length x'" by simp
  from ‹bisim Vs E2 {V:T=None; e} (lcl (h, x))›
  show ?case
  proof(cases rule: bisim_cases(14)[consumes 1, case_names BlockNone BlockSome BlockSomeNone])
    case (BlockNone V' E)
    with ‹fv E2 ⊆ set Vs› have "fv E ⊆ set (Vs@[V'])" by auto
    with IH[of "Vs@[V']" E "X(V' := None)"] BlockNone ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl (h, x)]›
      ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› ‹𝒟 E2 ⌊dom X⌋›
    obtain TA' e2' X' where IH': "sim_move10 P t ta e e' E h (X(V' := None)) TA' e2' h' X'"
      "bisim (Vs @ [V']) e2' e' x'" "X' ⊆⇩m [Vs @ [V'] [↦] x']"
      by(fastforce simp del: fun_upd_apply)
    { assume "V' ∈ set Vs"
      hence "hidden (Vs @ [V']) (index Vs V')" by(rule hidden_index)
      with ‹bisim (Vs @ [V']) E e (lcl (h, x))› have "unmod e (index Vs V')"
        by(auto intro: hidden_bisim_unmod)
      moreover from ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› ‹V' ∈ set Vs›
      have "index Vs V' < length x" by(auto intro: index_less_aux)
      ultimately have "x ! index Vs V' = x' ! index Vs V'"
        using red1_preserves_unmod[OF ‹False,compP1 P,t ⊢1 ⟨e,(h, x)⟩ -ta→ ⟨e',(h', x')⟩›]
        by(simp) }
    with ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› 
      ‹X' ⊆⇩m [Vs @ [V'] [↦] x']› ‹length x = length x'› ‹X ⊆⇩m [Vs [↦] lcl (h, x)]›
    have rel: "X'(V' := X V') ⊆⇩m [Vs [↦] x']" by(auto intro: Block_lem)

    show ?thesis
    proof(cases "X' V'")
      case None
      with BlockNone IH' rel show ?thesis by(fastforce intro: BlockRed)
    next
      case (Some v)
      with ‹X' ⊆⇩m [Vs @ [V'] [↦] x']› ‹length Vs < length x'›
      have "x' ! length Vs = v" by(auto dest: map_le_SomeD)
      with BlockNone IH' rel Some show ?thesis by(fastforce intro: BlockRed)
    qed
  next
    case BlockSome thus ?thesis by simp
  next
    case (BlockSomeNone V' E)
    with ‹fv E2 ⊆ set Vs› have "fv E ⊆ set (Vs@[V'])" by auto
    with IH[of "Vs@[V']" E "X(V' ↦ x ! length Vs)"] BlockSomeNone ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl (h, x)]›
      ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› ‹𝒟 E2 ⌊dom X⌋›
    obtain TA' e2' X' where IH': "sim_move10 P t ta e e' E h (X(V' ↦ x ! length Vs)) TA' e2' h' X'"
      "bisim (Vs @ [V']) e2' e' x'" "X' ⊆⇩m [Vs @ [V'] [↦] x']"
      by(fastforce simp del: fun_upd_apply)
    { assume "V' ∈ set Vs"
      hence "hidden (Vs @ [V']) (index Vs V')" by(rule hidden_index)
      with ‹bisim (Vs @ [V']) E e (lcl (h, x))› have "unmod e (index Vs V')"
        by(auto intro: hidden_bisim_unmod)
      moreover from ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› ‹V' ∈ set Vs›
      have "index Vs V' < length x" by(auto intro: index_less_aux)
      ultimately have "x ! index Vs V' = x' ! index Vs V'"
        using red1_preserves_unmod[OF ‹False,compP1 P,t ⊢1 ⟨e,(h, x)⟩ -ta→ ⟨e',(h', x')⟩›]
        by(simp) }
    with ‹length Vs + max_vars {V:T=None; e} ≤ length (lcl (h, x))› 
      ‹X' ⊆⇩m [Vs @ [V'] [↦] x']› ‹length x = length x'› ‹X ⊆⇩m [Vs [↦] lcl (h, x)]›
    have rel: "X'(V' := X V') ⊆⇩m [Vs [↦] x']" by(auto intro: Block_lem)
    from ‹sim_move10 P t ta e e' E h (X(V' ↦ x ! length Vs)) TA' e2' h' X'›
    obtain v' where "X' V' = ⌊v'⌋"
      by(auto simp: sim_move10_def split: if_split_asm dest!: τred0t_lcl_incr τred0r_lcl_incr red_lcl_incr subsetD)
    with ‹X' ⊆⇩m [Vs @ [V'] [↦] x']› ‹length Vs < length x'›
    have "x' ! length Vs = v'" by(auto dest: map_le_SomeD)
    with BlockSomeNone IH' rel ‹X' V' = ⌊v'⌋›
    show ?thesis by(fastforce intro: BlockRed)
  qed
next
  case(Block1Some V xs T v e h)
  from ‹bisim vs e2 {V:T=⌊v⌋; e} (lcl (h, xs))› obtain e' V' where "e2 = {V':T=⌊v⌋; e'}"
    and "V = length vs" "bisim (vs @ [V']) e' e (xs[length vs := v])" by(fastforce)
  moreover have "sim_move10 P t ε {length vs:T=⌊v⌋; e} {length vs:T=None; e} {V':T=⌊v⌋; e'} h x ε {V':T=⌊v⌋; e'} h x"
    by(auto)
  moreover from ‹bisim (vs @ [V']) e' e (xs[length vs := v])›
    ‹length vs + max_vars {V:T=⌊v⌋; e} ≤ length (lcl (h, xs))›
  have "bisim vs {V':T=⌊v⌋; e'} {length vs:T=None; e} (xs[length vs := v])" by auto
  moreover from ‹x ⊆⇩m [vs [↦] lcl (h, xs)]› ‹length vs + max_vars {V:T=⌊v⌋; e} ≤ length (lcl (h, xs))›
  have "x ⊆⇩m [vs [↦] xs[length vs := v]]" by auto
  ultimately show ?case by auto
next
  case (Lock1Synchronized V xs a e h Vs E2 X)
  note len = ‹length Vs + max_vars (sync⇘V⇙ (addr a) e) ≤ length (lcl (h, xs))›
  from ‹bisim Vs E2 (sync⇘V⇙ (addr a) e) (lcl (h, xs))› obtain E
    where E2: "E2 = sync(addr a) E" "e = compE1 (Vs@[fresh_var Vs]) E" 
    and sync: "¬ contains_insync E" and [simp]: "V = length Vs" by auto
  moreover
  have "extTA2J0 P,P,t ⊢ ⟨sync(addr a) E, (h, X)⟩ -⦃Lock→a, SyncLock a⦄→ ⟨insync(a) E, (h, X)⟩"
    by(rule LockSynchronized)
  moreover from ‹fv E2 ⊆ set Vs› fresh_var_fresh[of Vs] sync len
  have "bisim Vs (insync(a) E) (insync⇘length Vs⇙ (a) e) (xs[length Vs := Addr a])"
    unfolding ‹e = compE1 (Vs@[fresh_var Vs]) E› ‹E2 = sync(addr a) E›
    by -(rule bisimInSynchronized,rule compE1_bisim, auto)
  moreover have "zip Vs (xs[length Vs := Addr a]) = (zip Vs xs)[length Vs := (arbitrary, Addr a)]"
    by(rule sym)(simp add: update_zip)
  hence "zip Vs (xs[length Vs := Addr a]) = zip Vs xs" by simp
  with ‹X ⊆⇩m [Vs [↦] (lcl (h, xs))]› have "X ⊆⇩m [Vs [↦] xs[length Vs := Addr a]]"
    by(auto simp add: map_le_def map_upds_def)
  ultimately show ?case by(fastforce intro: sim_move10_SyncLocks)
next
  case (Synchronized1Red2 e s ta e' s' V a Vs E2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
            x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s);
            𝒟 e2 ⌊dom x⌋ ⟧ ⟹ ?concl e e' e2 s x ta s' e' vs› 
  from ‹bisim Vs E2 (insync⇘V⇙ (a) e) (lcl s)› obtain E
    where E2: "E2 = insync(a) E" and bisim: "bisim (Vs@[fresh_var Vs]) E e (lcl s)"
    and xsa: "lcl s ! length Vs = Addr a" and [simp]: "V = length Vs" by auto
  with ‹fv E2 ⊆ set Vs› fresh_var_fresh[of Vs] have fv: "(fresh_var Vs) ∉ fv E" by auto
  from ‹length Vs + max_vars (insync⇘V⇙ (a) e) ≤ length (lcl s)› have "length Vs < length (lcl s)" by simp
  { assume "X (fresh_var Vs) ≠ None"
    then obtain v where "X (fresh_var Vs) = ⌊v⌋" by auto
    with ‹X ⊆⇩m [Vs [↦] lcl s]› have "[Vs [↦] lcl s] (fresh_var Vs) = ⌊v⌋" 
      by(auto simp add: map_le_def dest: bspec)
    hence "(fresh_var Vs) ∈ set Vs" 
      by(auto simp add: map_upds_def set_zip dest!: map_of_SomeD )
    moreover have "(fresh_var Vs) ∉ set Vs" by(rule fresh_var_fresh)
    ultimately have False by contradiction }
  hence "X (fresh_var Vs) = None" by(cases "X (fresh_var Vs)", auto)
  hence "X(fresh_var Vs := None) = X" by(auto intro: ext)
  moreover from ‹X ⊆⇩m [Vs [↦] lcl s]›
  have "X(fresh_var Vs := None) ⊆⇩m [Vs [↦] lcl s, (fresh_var Vs) ↦ (lcl s) ! length Vs]" by(simp)
  ultimately have "X ⊆⇩m [Vs @ [fresh_var Vs] [↦] lcl s]"
    using ‹length Vs < length (lcl s)› by(auto)
  moreover note IH[of "Vs@[fresh_var Vs]" E X] bisim E2 ‹fv E2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]› 
    ‹length Vs + max_vars (insync⇘V⇙ (a) e) ≤ length (lcl s)› ‹𝒟 E2 ⌊dom X⌋›
  ultimately obtain TA' e2' x' where IH': "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim (Vs @ [fresh_var Vs]) e2' e' (lcl s')" "x' ⊆⇩m [Vs @ [fresh_var Vs] [↦] lcl s']" by auto
  hence "dom x' ⊆ dom X ∪ fv E"
    by(fastforce iff del: domIff simp add: sim_move10_def dest: red_dom_lcl τred0r_dom_lcl[OF wf_prog_wwf_prog[OF wf]] τred0t_dom_lcl[OF wf_prog_wwf_prog[OF wf]] τred0r_fv_subset[OF wf_prog_wwf_prog[OF wf]] split: if_split_asm)
  with fv ‹X (fresh_var Vs) = None› have "(fresh_var Vs) ∉ dom x'" by auto
  hence "x' (fresh_var Vs) = None" by auto
  moreover from ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩›
  have "length (lcl s) = length (lcl s')" by(auto dest: red1_preserves_len)
  moreover note ‹x' ⊆⇩m [Vs @ [fresh_var Vs] [↦] lcl s']› ‹length Vs < length (lcl s)›
  ultimately have "x' ⊆⇩m [Vs [↦] lcl s']" by(auto simp add: map_le_def dest: bspec)
  moreover from bisim fv have "unmod e (length Vs)" by(auto intro: bisim_fv_unmod)
  with ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩› ‹length Vs < length (lcl s)›
  have "lcl s ! length Vs = lcl s' ! length Vs"
    by(auto dest!: red1_preserves_unmod)
  with xsa have "lcl s' ! length Vs = Addr a" by simp
  ultimately show ?case using IH' E2 by(auto intro: SynchronizedRed2)
next
  case (Unlock1Synchronized xs V a' a v h Vs E2 X)
  from ‹bisim Vs E2 (insync⇘V⇙ (a) Val v) (lcl (h, xs))›
  have E2: "E2 = insync(a) Val v" "V = length Vs" "xs ! length Vs = Addr a" by auto
  moreover with ‹xs ! V = Addr a'› have [simp]: "a' = a" by simp
  have "extTA2J0 P,P,t ⊢ ⟨insync(a) (Val v), (h, X)⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Val v, (h, X)⟩"
    by(rule UnlockSynchronized)
  ultimately show ?case using ‹X ⊆⇩m [Vs [↦] lcl (h, xs)]› by(fastforce intro: sim_move10_SyncLocks)
next
  case (Unlock1SynchronizedNull xs V a v h Vs E2 X)
  from ‹bisim Vs E2 (insync⇘V⇙ (a) Val v) (lcl (h, xs))›
  have "V = length Vs" "xs ! length Vs = Addr a" by(auto)
  with ‹xs ! V = Null› have False by simp
  thus ?case ..
next
  case (Unlock1SynchronizedFail xs V A' a' v h Vs E2 X)
  from ‹False› show ?case ..
next
  case (Red1While b c s Vs E2 X)
  from ‹bisim Vs E2 (while (b) c) (lcl s)› obtain B C
    where E2: "E2 = while (B) C" "b = compE1 Vs B" "c = compE1 Vs C" 
    and sync: "¬ contains_insync B" "¬ contains_insync C" by auto
  moreover have "extTA2J0 P,P,t ⊢ ⟨while (B) C, (hp s, X)⟩ -ε→ ⟨if (B) (C;;while (B) C) else unit, (hp s, X)⟩"
    by(rule RedWhile)
  hence "sim_move10 P t ε (while (compE1 Vs B) (compE1 Vs C)) (if (compE1 Vs B) (compE1 Vs C;;while (compE1 Vs B) (compE1 Vs C)) else unit) (while (B) C) (hp s) X ε (if (B) (C;;while (B) C) else unit) (hp s) X"
    by(auto simp add: sim_move10_def)
  moreover from ‹fv E2 ⊆ set Vs› E2 sync
  have "bisim Vs (if (B) (C;; while (B) C) else unit)
                 (if (compE1 Vs B) (compE1 Vs (C;; while(B) C)) else (compE1 Vs unit)) (lcl s)"
    by -(rule bisimCond, auto)
  ultimately show ?case using ‹X ⊆⇩m [Vs [↦] lcl s]›
    by(simp)(rule exI, rule exI, rule exI, erule conjI, auto)
next
  case (Red1TryCatch h a D C V x e2 Vs E2 X)
  from ‹bisim Vs E2 (try Throw a catch(C V) e2) (lcl (h, x))›
  obtain E2' V' where "E2 = try Throw a catch(C V') E2'" "V = length Vs" "e2 = compE1 (Vs @ [V']) E2'"
    and sync: "¬ contains_insync E2'" by(auto)
  with ‹fv E2 ⊆ set Vs› have "fv E2' ⊆ set (Vs @[V'])" by auto
  with ‹e2 = compE1 (Vs @ [V']) E2'›  sync have "bisim (Vs @[V']) E2' e2 (x[V := Addr a])"
    by(auto intro!: compE1_bisim)
  with ‹V = length Vs› ‹length Vs + max_vars (try Throw a catch(C V) e2) ≤ length (lcl (h, x))›
  have "bisim Vs {V':Class C=⌊Addr a⌋; E2'} {length Vs:Class C=None; e2} (x[V := Addr a])"
    by(auto intro: bisimBlockSomeNone)
  moreover from ‹length Vs + max_vars (try Throw a catch(C V) e2) ≤ length (lcl (h, x))›
  have "[Vs [↦] x[length Vs := Addr a]] = [Vs [↦] x]" by simp
  with ‹X ⊆⇩m [Vs [↦] lcl (h, x)]› have "X ⊆⇩m [Vs [↦] x[length Vs := Addr a]]" by simp
  moreover note ‹e2 = compE1 (Vs @ [V']) E2'› ‹E2 = try Throw a catch(C V') E2'›
    ‹typeof_addr h a = ⌊Class_type D⌋› ‹compP1 P ⊢ D ≼⇧* C› ‹V = length Vs›
  ultimately show ?case by(auto intro!: exI)
next
  case Red1TryFail thus ?case by(auto intro!: exI sim_move10_TryFail)
next
  case (List1Red1 e s ta e' s' es Vs ES2 X)
  note IH = ‹⋀vs e2 x. ⟦ bisim vs e2 e (lcl s); fv e2 ⊆ set vs;
            x ⊆⇩m [vs [↦] lcl s]; length vs + max_vars e ≤ length (lcl s); 𝒟 e2 ⌊dom x⌋⟧
           ⟹ ∃TA' e2' x'. sim_move10 P t ta e e' e2 (hp s) x TA' e2' (hp s') x' ∧ 
                 bisim vs e2' e' (lcl s') ∧ x' ⊆⇩m [vs [↦] lcl s']›
  from ‹bisims Vs ES2 (e # es) (lcl s)› ‹False,compP1 P,t ⊢1 ⟨e,s⟩ -ta→ ⟨e',s'⟩›
  obtain E ES where "ES2 = E # ES" "¬ is_val E" "es = compEs1 Vs ES" "bisim Vs E e (lcl s)"
    and sync: "¬ contains_insyncs ES" by(auto elim!: bisims_cases simp add: compEs1_conv_map)
  with IH[of Vs E X] ‹fvs ES2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_varss (e # es) ≤ length (lcl s)› ‹𝒟s ES2 ⌊dom X⌋›
  obtain TA' e2' x' where IH': "sim_move10 P t ta e e' E (hp s) X TA' e2' (hp s') x'"
    "bisim Vs e2' e' (lcl s')" "x' ⊆⇩m [Vs [↦] lcl s']" by fastforce
  show ?case
  proof(cases "is_val e2'")
    case False
    with IH' ‹ES2 = E # ES› ‹es = compEs1 Vs ES› sync show ?thesis by(auto intro: sim_moves10_expr)
  next
    case True
    from ‹fvs ES2 ⊆ set Vs› ‹ES2 = E # ES› ‹es = compEs1 Vs ES› sync
    have "bisims Vs ES es (lcl s')" by(auto intro: compEs1_bisims)
    with IH' True ‹ES2 = E # ES› ‹es = compEs1 Vs ES› show ?thesis by(auto intro: sim_moves10_expr)
  qed
next
  case (List1Red2 es s ta es' s' v Vs ES2 X)
  note IH = ‹⋀vs es2 x. ⟦bisims vs es2 es (lcl s); fvs es2 ⊆ set vs;
            x ⊆⇩m [vs [↦] lcl s]; length vs + max_varss es ≤ length (lcl s); 𝒟s es2 ⌊dom x⌋⟧
           ⟹ ∃TA' es2' x'. sim_moves10 P t ta es es' es2 (hp s) x TA' es2' (hp s') x' ∧ bisims vs es2' es' (lcl s') ∧ x' ⊆⇩m [vs [↦] lcl s']›
  from ‹bisims Vs ES2 (Val v # es) (lcl s)› obtain ES where "ES2 = Val v # ES" "bisims Vs ES es (lcl s)"
    by(auto elim!: bisims_cases)
  with IH[of Vs ES X] ‹fvs ES2 ⊆ set Vs› ‹X ⊆⇩m [Vs [↦] lcl s]›
    ‹length Vs + max_varss (Val v # es) ≤ length (lcl s)› ‹𝒟s ES2 ⌊dom X⌋›
    ‹ES2 = Val v # ES› show ?case by(fastforce intro: sim_moves10_expr)
next
  case Call1ThrowParams
  thus ?case by(fastforce intro: CallThrowParams elim!: bisim_cases simp add: bisims_map_Val_Throw2)
next
  case (Synchronized1Throw2 xs V a' a ad h Vs E2 X)
  from ‹bisim Vs E2 (insync⇘V⇙ (a) Throw ad) (lcl (h, xs))›
  have "xs ! length Vs = Addr a" and "V = length Vs" by auto
  with ‹xs ! V = Addr a'› have [simp]: "a' = a" by simp
  have "extTA2J0 P,P,t ⊢ ⟨insync(a) Throw ad, (h, X)⟩ -⦃Unlock→a, SyncUnlock a⦄→ ⟨Throw ad, (h, X)⟩"
    by(rule SynchronizedThrow2)
  with ‹X ⊆⇩m [Vs [↦] lcl (h, xs)]› ‹bisim Vs E2 (insync⇘V⇙ (a) Throw ad) (lcl (h, xs))›
  show ?case by(auto intro: sim_move10_SyncLocks intro!: exI)
next
  case (Synchronized1Throw2Null xs V a a' h Vs E2 X)
  from ‹bisim Vs E2 (insync⇘V⇙ (a) Throw a') (lcl (h, xs))›
  have "V = length Vs" "xs ! length Vs = Addr a" by(auto)
  with ‹xs ! V = Null› have False by simp
  thus ?case ..
next
  case (Synchronized1Throw2Fail xs V A' a' a h Vs E2 X)
  from ‹False› show ?case ..
next
  case InstanceOf1Red thus ?case by auto(blast)
next
  case Red1InstanceOf thus ?case by hypsubst_thin auto
next
  case InstanceOf1Throw thus ?case by auto
next
  case CAS1Throw thus ?case by fastforce
next
  case CAS1Throw2 thus ?case by fastforce
next
  case CAS1Throw3 thus ?case by fastforce
qed(simp_all del: fun_upd_apply, (fastforce intro: red_reds.intros simp del: fun_upd_apply simp add: finfun_upd_apply)+)

lemma bisim_call_Some_call1:
  "⟦ bisim Vs e e' xs; call e = ⌊aMvs⌋; length Vs + max_vars e' ≤ length xs ⟧
  ⟹ ∃e'' xs'. τred1'r P t h (e', xs) (e'', xs') ∧ call1 e'' = ⌊aMvs⌋ ∧ 
               bisim Vs e e'' xs' ∧ take (length Vs) xs = take (length Vs) xs'"

  and bisims_calls_Some_calls1:
  "⟦ bisims Vs es es' xs; calls es = ⌊aMvs⌋; length Vs + max_varss es' ≤ length xs ⟧ 
  ⟹ ∃es'' xs'. τreds1'r P t h (es', xs) (es'', xs') ∧ calls1 es'' = ⌊aMvs⌋ ∧ 
                bisims Vs es es'' xs' ∧ take (length Vs) xs = take (length Vs) xs'"
proof(induct rule: bisim_bisims.inducts)
  case bisimCallParams thus ?case
    by(fastforce simp add: is_vals_conv split: if_split_asm)
next
  case bisimBlockNone thus ?case by(fastforce intro: take_eq_take_le_eq)
next
  case (bisimBlockSome Vs V e e' xs v T)
  from ‹length Vs + max_vars {length Vs:T=⌊v⌋; e'} ≤ length xs›
  have "τred1'r P t h ({length Vs:T=⌊v⌋; e'}, xs) ({length Vs:T=None; e'}, xs[length Vs := v])"
    by(auto intro!: τred1r_1step Block1Some)
  also from bisimBlockSome obtain e'' xs'
    where "τred1'r P t h (e', xs[length Vs := v]) (e'', xs')"
    and "call1 e'' = ⌊aMvs⌋" "bisim (Vs @ [V]) e e'' xs'" 
    and "take (length (Vs @ [V])) (xs[length Vs := v]) = take (length (Vs @ [V])) xs'" by auto
  hence "τred1'r P t h ({length Vs:T=None; e'}, xs[length Vs := v]) ({length Vs:T=None; e''}, xs')" by auto
  also from ‹call1 e'' = ⌊aMvs⌋› have "call1 {length Vs:T=None; e''} = ⌊aMvs⌋" by simp
  moreover from ‹take (length (Vs @ [V])) (xs[length Vs := v]) = take (length (Vs @ [V])) xs'›
  have "take (length Vs) xs = take (length Vs) xs'"
    by(auto dest: take_eq_take_le_eq[where m="length Vs"] simp add: take_update_cancel)
  moreover {
    have "xs' ! length Vs = take (length (Vs @ [V])) xs' ! length Vs" by simp
    also note ‹take (length (Vs @ [V])) (xs[length Vs := v]) = take (length (Vs @ [V])) xs'›[symmetric]
    also have "take (length (Vs @ [V])) (xs[length Vs := v]) ! length Vs = v"
      using ‹length Vs + max_vars {length Vs:T=⌊v⌋; e'} ≤ length xs› by simp
    finally have "bisim Vs {V:T=⌊v⌋; e} {length Vs:T=None; e''} xs'"
      using ‹bisim (Vs @ [V]) e e'' xs'› by auto }
  ultimately show ?case by blast
next
  case (bisimBlockSomeNone Vs V e e' xs v T)
  then obtain e'' xs' where "τred1'r P t h (e', xs) (e'', xs')" "call1 e'' = ⌊aMvs⌋" "bisim (Vs @ [V]) e e'' xs'"
    and "take (length (Vs @ [V])) xs = take (length (Vs @ [V])) xs'" by auto
  hence "τred1'r P t h ({length Vs:T=None; e'}, xs) ({length Vs:T=None; e''}, xs')" by auto
  moreover from ‹call1 e'' = ⌊aMvs⌋› have "call1 ({length Vs:T=None; e''}) = ⌊aMvs⌋" by simp
  moreover from ‹take (length (Vs @ [V])) xs = take (length (Vs @ [V])) xs'›
  have "take (length Vs) xs = take (length Vs) xs'" by(auto intro: take_eq_take_le_eq)
  moreover {
    have "xs' ! length Vs = take (length (Vs @ [V])) xs' ! length Vs" by simp
    also note ‹take (length (Vs @ [V])) xs = take (length (Vs @ [V])) xs'›[symmetric]
    also have "take (length (Vs @ [V])) xs ! length Vs = v" using ‹xs ! length Vs = v› by simp
    finally have "bisim Vs {V:T=⌊v⌋; e} {length Vs:T=None; e''} xs'"
      using ‹bisim (Vs @ [V]) e e'' xs'› by auto }
  ultimately show ?case by blast
next
  case (bisimInSynchronized Vs e e' xs a)
  then obtain e'' xs' where "τred1'r P t h (e', xs) (e'', xs')" "call1 e'' = ⌊aMvs⌋" "bisim (Vs @ [fresh_var Vs]) e e'' xs'"
    and "take (Suc (length Vs)) xs = take (Suc (length Vs)) xs'" by auto
  hence "τred1'r P t h (insync⇘length Vs⇙ (a) e', xs) (insync⇘length Vs⇙ (a) e'', xs')" by auto
  moreover from ‹call1 e'' = ⌊aMvs⌋› have "call1 (insync⇘length Vs⇙ (a) e'') = ⌊aMvs⌋" by simp
  moreover from ‹take (Suc (length Vs)) xs = take (Suc (length Vs)) xs'›
  have "take (length Vs) xs = take (length Vs) xs'" by(auto intro: take_eq_take_le_eq)
  moreover {
    have "xs' ! length Vs = take (Suc (length Vs)) xs' ! length Vs" by simp
    also note ‹take (Suc (length Vs)) xs = take (Suc (length Vs)) xs'›[symmetric]
    also have "take (Suc (length Vs)) xs ! length Vs = Addr a"
      using ‹xs ! length Vs = Addr a› by simp
    finally have "bisim Vs (insync(a) e) (insync⇘length Vs⇙ (a) e'') xs'"
      using ‹bisim (Vs @ [fresh_var Vs]) e e'' xs'› by auto }
  ultimately show ?case by blast
next
  case bisimsCons1 thus ?case by(fastforce intro!: τred1r_inj_τreds1r)
next
  case bisimsCons2 thus ?case by(fastforce intro!: τreds1r_cons_τreds1r)
qed fastforce+

lemma sim_move01_into_Red1:
  "sim_move01 P t ta e E' h xs ta' e2' h' xs'
  ⟹ if τMove0 P h (e, es1)
      then τRed1't P t h ((E', xs), exs2) ((e2', xs'), exs2) ∧ ta = ε ∧ h = h'
      else ∃ex2' exs2' ta'. τRed1'r P t h ((E', xs), exs2) (ex2', exs2') ∧
                           (call e = None ∨ call1 E' = None ∨ ex2' = (E', xs) ∧ exs2' = exs2) ∧
                           False,P,t ⊢1 ⟨ex2'/exs2',h⟩ -ta'→ ⟨(e2', xs')/exs2,h'⟩ ∧
                           ¬ τMove1 P h (ex2', exs2') ∧ ta_bisim01 ta ta'"
apply(auto simp add: sim_move01_def intro: τred1t_into_τRed1t τred1r_into_τRed1r red1Red split: if_split_asm)
apply(fastforce intro: red1Red intro!: τred1r_into_τRed1r)+
done

lemma sim_move01_max_vars_decr:
  "sim_move01 P t ta e0 e h xs ta' e' h' xs' ⟹ max_vars e' ≤ max_vars e"
by(fastforce simp add: sim_move01_def split: if_split_asm dest: τred1t_max_vars red1_max_vars_decr τred1r_max_vars)

lemma Red1_simulates_red0:
  assumes wf: "wf_J_prog P"
  and red: "P,t ⊢0 ⟨e1/es1, h⟩ -ta→ ⟨e1'/es1', h'⟩"
  and bisiml: "bisim_list1 (e1, es1) (ex2, exs2)"
  shows "∃ex2'' exs2''. bisim_list1 (e1', es1') (ex2'', exs2'') ∧
        (if τMove0 P h (e1, es1)
         then τRed1't (compP1 P) t h (ex2, exs2) (ex2'', exs2'') ∧ ta = ε ∧ h = h'
         else ∃ex2' exs2' ta'. τRed1'r (compP1 P) t h (ex2, exs2) (ex2', exs2') ∧ 
                               (call e1 = None ∨ call1 (fst ex2) = None ∨ ex2' = ex2 ∧ exs2' = exs2) ∧
                               False,compP1 P,t ⊢1 ⟨ex2'/exs2', h⟩ -ta'→ ⟨ex2''/exs2'', h'⟩ ∧
                               ¬ τMove1 P h (ex2', exs2') ∧ ta_bisim01 ta ta')"
  (is "∃ex2'' exs2'' . _ ∧ ?red ex2'' exs2''")
using red
proof(cases)
  case (red0Red XS')
  note [simp] = ‹es1' = es1›
    and red = ‹extTA2J0 P,P,t ⊢ ⟨e1,(h, Map.empty)⟩ -ta→ ⟨e1',(h', XS')⟩›
    and notsynth = ‹∀aMvs. call e1 = ⌊aMvs⌋ ⟶ synthesized_call P h aMvs›
  from bisiml obtain E xs where ex2: "ex2 = (E, xs)"
    and bisim: "bisim [] e1 E xs" and fv: "fv e1 = {}" 
    and length: "max_vars E ≤ length xs" and bsl: "bisim_list es1 exs2"
    and D: "𝒟 e1 ⌊{}⌋" by(auto elim!: bisim_list1_elim)
  from bisim_max_vars[OF bisim] length red1_simulates_red_aux[OF wf red bisim] fv notsynth
  obtain ta' e2' xs' where sim: "sim_move01 (compP1 P) t ta e1 E h xs ta' e2' h' xs'"
    and bisim': "bisim [] e1' e2' xs'" and XS': "XS' ⊆⇩m Map.empty" by auto
  from sim_move01_into_Red1[OF sim, of es1 exs2]
  have "?red (e2', xs') exs2" unfolding ex2 by auto
  moreover {
    note bsl bisim' moreover
    from fv red_fv_subset[OF wf_prog_wwf_prog[OF wf] red]
    have "fv e1' = {}" by simp
    moreover from red D have "𝒟 e1' ⌊dom XS'⌋"
      by(auto dest: red_preserves_defass[OF wf] split: if_split_asm)
    with red_dom_lcl[OF red] ‹fv e1 = {}› have "𝒟 e1' ⌊{}⌋"
      by(auto elim!: D_mono' simp add: hyperset_defs)
    moreover from sim have "length xs = length xs'" "max_vars e2' ≤ max_vars E"
      by(auto dest: sim_move01_preserves_len sim_move01_max_vars_decr)
    with length have length': "max_vars e2' ≤ length xs'" by(auto)
    ultimately have "bisim_list1 (e1', es1) ((e2', xs'), exs2)" by(rule bisim_list1I) }
  ultimately show ?thesis using ex2 by(simp split del: if_split)(rule exI conjI|assumption)+
next
  case (red0Call a M vs U Ts T pns body D)
  note [simp] = ‹ta = ε› ‹h' = h›
    and es1' = ‹es1' = e1 # es1›
    and e1' = ‹e1' = blocks (this # pns) (Class D # Ts) (Addr a # vs) body›
    and call = ‹call e1 = ⌊(a, M, vs)⌋›
    and ha = ‹typeof_addr h a = ⌊U⌋›
    and sees = ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D›
    and len = ‹length vs = length pns› ‹length Ts = length pns›
  from bisiml obtain E xs where ex2: "ex2 = (E, xs)"
    and bisim: "bisim [] e1 E xs" and fv: "fv e1 = {}" 
    and length: "max_vars E ≤ length xs" and bsl: "bisim_list es1 exs2"
    and D: "𝒟 e1 ⌊{}⌋" by(auto elim!: bisim_list1_elim)
  
  from bisim_call_Some_call1[OF bisim call, of "compP1 P" t h] length
  obtain e' xs' where red: "τred1'r (compP1 P) t h (E, xs) (e', xs')"
    and "call1 e' = ⌊(a, M, vs)⌋" "bisim [] e1 e' xs'" 
    and "take 0 xs = take 0 xs'" by auto
    
  let ?e1' = "blocks (this # pns) (Class D # Ts) (Addr a # vs) body"
  let ?e2' = "blocks1 0 (Class D#Ts) (compE1 (this # pns) body)"
  let ?xs2' = "Addr a # vs @ replicate (max_vars (compE1 (this # pns) body)) undefined_value"
  let ?exs2' = "(e', xs') # exs2"

  have "τRed1'r (compP1 P) t h ((E, xs), exs2) ((e', xs'), exs2)"
    using red by(rule τred1r_into_τRed1r)
  moreover {
    note ‹call1 e' = ⌊(a, M, vs)⌋› 
    moreover note ha
    moreover have "compP1 P ⊢ class_type_of U sees M:Ts → T = map_option (λ(pns, body). compE1 (this # pns) body) ⌊(pns, body)⌋ in D"
      using sees unfolding compP1_def by(rule sees_method_compP)
    hence sees': "compP1 P ⊢ class_type_of U sees M:Ts → T = ⌊compE1 (this # pns) body⌋ in D" by simp
    moreover from len have "length vs = length Ts" by simp
    ultimately have "False,compP1 P,t ⊢1 ⟨(e', xs')/exs2,h⟩ -ε→ ⟨(?e2', ?xs2')/?exs2', h⟩" by(rule red1Call) 
    moreover have "τMove1 P h ((e', xs'), exs2)" using ‹call1 e' = ⌊(a, M, vs)⌋› ha sees
      by(auto simp add: synthesized_call_def τexternal'_def dest: sees_method_fun dest!: τmove1_not_call1[where P=P and h=h])
    ultimately have "τRed1' (compP1 P) t h ((e', xs'), exs2) ((?e2', ?xs2'), ?exs2')" by auto }
  ultimately have "τRed1't (compP1 P) t h ((E, xs), exs2) ((?e2', ?xs2'), ?exs2')" by(rule rtranclp_into_tranclp1)
  moreover
  { from red have "length xs' = length xs" by(rule τred1r_preserves_len)
    moreover from red have "max_vars e' ≤ max_vars E" by(rule τred1r_max_vars)
    ultimately have "max_vars e' ≤ length xs'" using length by simp }
  with bsl ‹bisim [] e1 e' xs'› fv D have "bisim_list (e1 # es1) ?exs2'"
    using ‹call e1 = ⌊(a, M, vs)⌋› ‹call1 e' = ⌊(a, M, vs)⌋› by(rule bisim_listCons)
  hence "bisim_list1 (e1', es1') ((?e2', ?xs2'), ?exs2')"
    unfolding e1' es1'
  proof(rule bisim_list1I)
    from wf_prog_wwf_prog[OF wf] sees
    have "wf_mdecl wwf_J_mdecl P D (M,Ts,T,⌊(pns,body)⌋)" by(rule sees_wf_mdecl)
    hence fv': "fv body ⊆ set pns ∪ {this}" by(auto simp add: wf_mdecl_def)
    moreover from ‹P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, body)⌋ in D› have "¬ contains_insync body"
      by(auto dest!: sees_wf_mdecl[OF wf] WT_expr_locks simp add: wf_mdecl_def contains_insync_conv)
    ultimately have "bisim ([this] @ pns) body (compE1 ([this] @ pns) body) ?xs2'"
      by -(rule compE1_bisim, auto)
    with ‹length vs = length pns› ‹length Ts = length pns›
    have "bisim ([] @ [this]) (blocks pns Ts vs body) (blocks1 (Suc 0) Ts (compE1 (this # pns) body)) ?xs2'"
      by -(drule blocks_bisim,auto simp add: nth_append)
    from bisimBlockSomeNone[OF this, of "Addr a" "Class D"]
    show "bisim [] ?e1' ?e2' ?xs2'" by simp
    from fv' len show "fv ?e1' = {}" by auto

    from wf sees
    have "wf_mdecl wf_J_mdecl P D (M,Ts,T,⌊(pns,body)⌋)" by(rule sees_wf_mdecl)
    hence "𝒟 body ⌊set pns ∪ {this}⌋" by(auto simp add: wf_mdecl_def)
    with ‹length vs = length pns› ‹length Ts = length pns›
    have "𝒟 (blocks pns Ts vs body) ⌊dom [this ↦ Addr a]⌋" by(auto)
    thus "𝒟 ?e1' ⌊{}⌋" by auto
    
    from len show "max_vars ?e2' ≤ length ?xs2'" by(auto simp add: blocks1_max_vars)
  qed
  moreover have "τMove0 P h (e1, es1)" using call ha sees
    by(fastforce simp add: synthesized_call_def  τexternal'_def dest: sees_method_fun τmove0_callD[where P=P and h=h])
  ultimately show ?thesis using ex2 ‹call e1 = ⌊(a, M, vs)⌋› 
    by(simp del: τMove1.simps)(rule exI conjI|assumption)+
next
  case (red0Return e)
  note es1 = ‹es1 = e # es1'› and e1' = ‹e1' = inline_call e1 e›
    and [simp] = ‹ta = ε› ‹h' = h›
    and fin = ‹final e1›
  from bisiml es1 obtain E' xs' E xs exs' aMvs where ex2: "ex2 = (E', xs')" and exs2: "exs2 = (E, xs) # exs'"
    and bisim': "bisim [] e1 E' xs'"
    and bisim: "bisim [] e E xs"
    and fv: "fv e = {}"
    and length: "max_vars E ≤ length xs"
    and bisiml: "bisim_list es1' exs'"
    and D: "𝒟 e ⌊{}⌋"
    and call: "call e = ⌊aMvs⌋"
    and call1: "call1 E = ⌊aMvs⌋"
    by(fastforce elim: bisim_list1_elim)
  let ?e2' = "inline_call E' E"

  from ‹final e1› bisim' have "final E'" by(auto)
  hence red': "False,compP1 P,t ⊢1 ⟨ex2/exs2, h⟩ -ε→ ⟨(?e2', xs)/exs', h⟩"
    unfolding ex2 exs2 by(rule red1Return)
  moreover have "τMove0 P h (e1, es1) = τMove1 P h ((E', xs'), exs2)"
    using ‹final e1› ‹final E'› by auto
  moreover {
    note bisiml
    moreover
    from bisim' fin bisim
    have "bisim [] (inline_call e1 e) (inline_call E' E) xs"
      using call by(rule bisim_inline_call)(simp add: fv)
    moreover from fv_inline_call[of e1 e] fv fin 
    have "fv (inline_call e1 e) = {}" by auto
    moreover from fin have "𝒟 (inline_call e1 e) ⌊{}⌋"
      using call D by(rule defass_inline_call)
    moreover have "max_vars ?e2' ≤ max_vars E + max_vars E'" by(rule inline_call_max_vars1)
    with ‹final E'› length have "max_vars ?e2' ≤ length xs" by(auto elim!: final.cases)
    ultimately have "bisim_list1 (inline_call e1 e, es1') ((?e2', xs), exs')"
      by(rule bisim_list1I) }
  ultimately show ?thesis using e1' ‹final e1› ‹final E'› ex2 
    apply(simp del: τMove0.simps τMove1.simps)
    apply(rule exI conjI impI|assumption)+
     apply(rule tranclp.r_into_trancl, simp)
    apply blast
    done
qed

lemma sim_move10_into_red0:
  assumes wwf: "wwf_J_prog P"
  and sim: "sim_move10 P t ta e2 e2' e h Map.empty ta' e' h' x'"
  and fv: "fv e = {}"
  shows "if τmove1 P h e2
         then (τRed0t P t h (e, es) (e', es) ∨ countInitBlock e2' < countInitBlock e2 ∧ e' = e ∧ x' = Map.empty) ∧ ta = ε ∧ h = h'
         else ∃e'' ta'. τRed0r P t h (e, es) (e'', es) ∧
                        (call1 e2 = None ∨ call e = None ∨ e'' = e) ∧
                        P,t ⊢0 ⟨e''/es,h⟩ -ta'→ ⟨e'/es,h'⟩ ∧
                        ¬ τMove0 P h (e'', es) ∧ ta_bisim01 ta' (extTA2J1 (compP1 P) ta)"
proof(cases "τmove1 P h e2")
  case True
  with sim have "¬ final e2"
    and red: "τred0t (extTA2J0 P) P t h (e, Map.empty) (e', x') ∨
              countInitBlock e2' < countInitBlock e2 ∧ e' = e ∧ x' = Map.empty"
    and [simp]: "h' = h" "ta = ε" "ta' = ε" by(simp_all add: sim_move10_def)
  from red have "τRed0t P t h (e, es) (e', es) ∨
                 countInitBlock e2' < countInitBlock e2 ∧ e' = e ∧ x' = Map.empty"
  proof
    assume red: "τred0t (extTA2J0 P) P t h (e, Map.empty) (e', x')"
    from τred0t_fv_subset[OF wwf red] τred0t_dom_lcl[OF wwf red] fv
    have "dom x' ⊆ {}" by(auto split: if_split_asm)
    hence "x' = Map.empty" by auto
    with red have "τred0t (extTA2J0 P) P t h (e, Map.empty) (e', Map.empty)" by simp
    with wwf have "τRed0t P t h (e, es) (e', es)"
      using fv by(rule τred0t_into_τRed0t)
    thus ?thesis ..
  qed simp
  with True show ?thesis by simp
next
  case False
  with sim obtain e'' xs'' where "¬ final e2"
    and τred: "τred0r (extTA2J0 P) P t h (e, Map.empty) (e'', xs'')"
    and red: "extTA2J0 P,P,t ⊢ ⟨e'',(h, xs'')⟩ -ta'→ ⟨e',(h', x')⟩"
    and call: "call1 e2 = None ∨ call e = None ∨ e'' = e"
    and "¬ τmove0 P h e''" "ta_bisim01 ta' (extTA2J1 (compP1 P) ta)" "no_call P h e''"
    by(auto simp add: sim_move10_def split: if_split_asm)
  from τred0r_fv_subset[OF wwf τred] τred0r_dom_lcl[OF wwf τred] fv
  have "dom xs'' ⊆ {}" by(auto)
  hence "xs'' = Map.empty" by(auto)
  with τred have "τred0r (extTA2J0 P) P t h (e, Map.empty) (e'', Map.empty)" by simp
  with wwf have "τRed0r P t h (e, es) (e'', es)"
    using fv by(rule τred0r_into_τRed0r)
  moreover from red ‹xs'' = Map.empty›
  have "extTA2J0 P,P,t ⊢ ⟨e'',(h, Map.empty)⟩ -ta'→ ⟨e',(h', x')⟩" by simp
  from red0Red[OF this] ‹no_call P h e''› 
  have "P,t ⊢0 ⟨e''/es,h⟩ -ta'→ ⟨e'/es,h'⟩" by(simp add: no_call_def)
  moreover from ‹¬ τmove0 P h e''› red
  have "¬ τMove0 P h (e'', es)" by auto
  ultimately show ?thesis using False ‹ta_bisim01 ta' (extTA2J1 (compP1 P) ta)› call
    by(simp del: τMove0.simps) blast
qed

lemma red0_simulates_Red1:
  assumes wf: "wf_J_prog P"
  and red: "False,compP1 P,t ⊢1 ⟨ex2/exs2, h⟩ -ta→ ⟨ex2'/exs2', h'⟩"
  and bisiml: "bisim_list1 (e, es) (ex2, exs2)"
  shows "∃e' es'. bisim_list1 (e', es') (ex2', exs2') ∧
                 (if τMove1 P h (ex2, exs2)
                  then (τRed0t P t h (e, es) (e', es') ∨ countInitBlock (fst ex2') < countInitBlock (fst ex2) ∧ exs2' = exs2 ∧ e' = e ∧ es' = es) ∧
                        ta = ε ∧ h = h'
                  else ∃e'' es'' ta'. τRed0r P t h (e, es) (e'', es'') ∧
                                      (call1 (fst ex2) = None ∨ call e = None ∨ e'' = e ∧ es'' = es) ∧
                                      P,t ⊢0 ⟨e''/es'', h⟩ -ta'→ ⟨e'/es', h'⟩ ∧
                                      ¬ τMove0 P h (e'', es'') ∧ ta_bisim01 ta' ta)"
  (is "∃e' es' . _ ∧ ?red e' es'")
using red
proof(cases)
  case (red1Red E xs TA E' xs')
  note red = ‹False,compP1 P,t ⊢1 ⟨E,(h, xs)⟩ -TA→ ⟨E',(h', xs')⟩›
    and ex2 = ‹ex2 = (E, xs)›
    and ex2' = ‹ex2' = (E', xs')›
    and [simp] = ‹ta = extTA2J1 (compP1 P) TA› ‹exs2' = exs2›
  from bisiml ex2 have bisim: "bisim [] e E xs" and fv: "fv e = {}"
    and length: "max_vars E ≤ length xs" and bsl: "bisim_list es exs2"
    and D: "𝒟 e ⌊{}⌋" by(auto elim: bisim_list1_elim)
  from red_simulates_red1_aux[OF wf red, simplified, OF bisim, of Map.empty] fv length D
  obtain TA' e2' x' where red': "sim_move10 P t TA E E' e h Map.empty TA' e2' h' x'"
    and bisim'': "bisim [] e2' E' xs'" and lcl': "x' ⊆⇩m Map.empty" by auto
  from red have "¬ final E" by auto
  with sim_move10_into_red0[OF wf_prog_wwf_prog[OF wf] red', of es] fv ex2 ex2'
  have red'': "?red e2' es" by fastforce
  moreover {
    note bsl bisim''
    moreover from red' fv have "fv e2' = {}"
      by(fastforce simp add: sim_move10_def split: if_split_asm dest: τred0r_fv_subset[OF wf_prog_wwf_prog[OF wf]] τred0t_fv_subset[OF wf_prog_wwf_prog[OF wf]] red_fv_subset[OF wf_prog_wwf_prog[OF wf]])
    moreover from red' have "dom x' ⊆ dom (Map.empty) ∪ fv e"
      unfolding sim_move10_def
      apply(auto split: if_split_asm del: subsetI dest: τred0r_dom_lcl[OF wf_prog_wwf_prog[OF wf]] τred0t_dom_lcl[OF wf_prog_wwf_prog[OF wf]])
      apply(frule_tac [1-2] τred0r_fv_subset[OF wf_prog_wwf_prog[OF wf]])
      apply(auto dest!: τred0r_dom_lcl[OF wf_prog_wwf_prog[OF wf]] red_dom_lcl del: subsetI, blast+)
      done
    with fv have "dom x' ⊆ {}" by(auto)
    hence "x' = Map.empty" by(auto)
    with D red' have "𝒟 e2' ⌊{}⌋"
      by(auto dest!: sim_move10_preserves_defass[OF wf] split: if_split_asm)
    moreover from red have "length xs' = length xs" by(auto dest: red1_preserves_len)
    with red1_max_vars[OF red] length
    have "max_vars E' ≤ length xs'" by simp
    ultimately have "bisim_list1 (e2', es) ((E', xs'), exs2)"
      by(rule bisim_list1I) }
  ultimately show ?thesis using ex2'
    by(clarsimp split: if_split_asm)(rule exI conjI|assumption|simp)+
next
  case (red1Call E a M vs U Ts T body D xs)
  note [simp] = ‹ex2 = (E, xs)› ‹h' = h› ‹ta = ε›
    and ex2' = ‹ex2' = (blocks1 0 (Class D#Ts) body, Addr a # vs @ replicate (max_vars body) undefined_value)›
    and exs' = ‹exs2' = (E, xs) # exs2›
    and call = ‹call1 E = ⌊(a, M, vs)⌋› and ha = ‹typeof_addr h a = ⌊U⌋›
    and sees = ‹compP1 P ⊢ class_type_of U sees M: Ts→T = ⌊body⌋ in D›
    and len = ‹length vs = length Ts›
  let ?e2' = "blocks1 0 (Class D#Ts) body"
  let ?xs2' = "Addr a # vs @ replicate (max_vars body) undefined_value"
  from bisiml have bisim: "bisim [] e E xs" and fv: "fv e = {}"
    and length: "max_vars E ≤ length xs" and bsl: "bisim_list es exs2"
    and D: "𝒟 e ⌊{}⌋" by(auto elim: bisim_list1_elim)

  from bisim ‹call1 E = ⌊(a, M, vs)⌋›
  have "call e = ⌊(a, M, vs)⌋" by(rule bisim_call1_Some_call)
  moreover note ha
  moreover from ‹compP1 P ⊢ class_type_of U sees M: Ts→T = ⌊body⌋ in D›
  obtain pns Jbody where sees': "P ⊢ class_type_of U sees M: Ts→T = ⌊(pns, Jbody)⌋ in D"
    and body: "body = compE1 (this # pns) Jbody"
    by(auto dest: sees_method_compPD)
  let ?e' = "blocks (this # pns) (Class D # Ts) (Addr a # vs) Jbody"
  note sees' moreover from wf sees' have "length Ts = length pns"
    by(auto dest!: sees_wf_mdecl simp add: wf_mdecl_def)
  with len have "length vs = length pns" "length Ts = length pns" by simp_all
  ultimately have red': "P,t ⊢0 ⟨e/es, h⟩ -ε→ ⟨?e'/e#es, h⟩" by(rule red0Call)
  moreover from ‹call e = ⌊(a, M, vs)⌋› ha sees'
  have "τMove0 P h (e, es)"
    by(fastforce simp add: synthesized_call_def dest: τmove0_callD[where P=P and h=h] sees_method_fun)
  ultimately have "τRed0t P t h (e, es) (?e', e#es)" by auto
  moreover
  from bsl bisim fv D length ‹call e = ⌊(a, M, vs)⌋› ‹call1 E = ⌊(a, M, vs)⌋›
  have "bisim_list (e # es) ((E, xs) # exs2)" by(rule bisim_list.intros)
  hence "bisim_list1 (?e', e # es) (ex2', (E, xs) # exs2)" unfolding ex2'
  proof(rule bisim_list1I)
    from wf_prog_wwf_prog[OF wf] sees'
    have "wf_mdecl wwf_J_mdecl P D (M,Ts,T,⌊(pns,Jbody)⌋)" by(rule sees_wf_mdecl)
    hence "fv Jbody ⊆ set pns ∪ {this}" by(auto simp add: wf_mdecl_def)
    moreover from sees' have "¬ contains_insync Jbody"
      by(auto dest!: sees_wf_mdecl[OF wf] WT_expr_locks simp add: wf_mdecl_def contains_insync_conv)
    ultimately have "bisim ([] @ this # pns) Jbody (compE1 ([] @ this # pns) Jbody) ?xs2'"
      by -(rule compE1_bisim, auto)
    with ‹length vs = length Ts› ‹length Ts = length pns› body
    have "bisim [] ?e' (blocks1 (length ([] :: vname list)) (Class D # Ts) body) ?xs2'"
      by -(rule blocks_bisim, auto simp add: nth_append nth_Cons')
    thus "bisim [] ?e' ?e2' ?xs2'" by simp
    from ‹length vs = length Ts› ‹length Ts = length pns› ‹fv Jbody ⊆ set pns ∪ {this}›
    show "fv ?e' = {}" by auto
    from wf sees'
    have "wf_mdecl wf_J_mdecl P D (M,Ts,T,⌊(pns,Jbody)⌋)" by(rule sees_wf_mdecl)
    hence "𝒟 Jbody ⌊set pns ∪ {this}⌋" by(auto simp add: wf_mdecl_def)
    with ‹length vs = length Ts› ‹length Ts = length pns›
    have "𝒟 (blocks pns Ts vs Jbody) ⌊dom [this ↦ Addr a]⌋" by(auto)
    thus "𝒟 ?e' ⌊{}⌋" by simp
    from len show "max_vars ?e2' ≤ length ?xs2'" by(simp add: blocks1_max_vars)
  qed
  moreover have "τMove1 P h (ex2, exs2)" using ha ‹call1 E = ⌊(a, M, vs)⌋› sees'
    by(auto simp add: synthesized_call_def τexternal'_def dest!: τmove1_not_call1[where P=P and h=h] dest: sees_method_fun)
  ultimately show ?thesis using exs'
    by(simp del: τMove1.simps τMove0.simps)(rule exI conjI rtranclp.rtrancl_refl|assumption)+
next
  case (red1Return E' x' E x)
  note [simp] = ‹h' = h› ‹ta = ε›
    and ex2 = ‹ex2 = (E', x')› and exs2 = ‹exs2 = (E, x) # exs2'›
    and ex2' = ‹ex2' = (inline_call E' E, x)›
    and fin = ‹final E'›
  from bisiml ex2 exs2 obtain e' es' aMvs where es: "es = e' # es'"
    and bsl: "bisim_list es' exs2'"
    and bisim: "bisim [] e E' x'"
    and bisim': "bisim [] e' E x"
    and fv: "fv e' = {}"
    and length: "max_vars E ≤ length x"
    and D: "𝒟 e' ⌊{}⌋"
    and call: "call e' = ⌊aMvs⌋"
    and call1: "call1 E = ⌊aMvs⌋"
    by(fastforce elim!: bisim_list1_elim)
  
  from ‹final E'› bisim have fin': "final e" by(auto)
  hence "P,t ⊢0 ⟨e/e' # es',h⟩ -ε→ ⟨inline_call e e'/es',h⟩" by(rule red0Return)
  moreover from bisim fin' bisim' call
  have "bisim [] (inline_call e e') (inline_call E' E) x"
    by(rule bisim_inline_call)(simp add: fv)
  with bsl have "bisim_list1 (inline_call e e', es') (ex2', exs2')" unfolding ex2'
  proof(rule bisim_list1I)
    from fin' fv_inline_call[of e e'] fv show "fv (inline_call e e') = {}" by auto
    from fin' show "𝒟 (inline_call e e') ⌊{}⌋" using call D by(rule defass_inline_call)
    
    from call1_imp_call[OF call1]
    have "max_vars (inline_call E' E) ≤ max_vars E + max_vars E'"
      by(rule inline_call_max_vars)
    with fin length show "max_vars (inline_call E' E) ≤ length x" by(auto elim!: final.cases)
  qed
  moreover have "τMove1 P h (ex2, exs2) = τMove0 P h (e, es)" using ex2 call1 call fin fin' by(auto)
  ultimately show ?thesis using es
    by(simp del: τMove1.simps τMove0.simps) blast
qed

end

sublocale J0_J1_heap_base < red0_Red1': FWdelay_bisimulation_base
  final_expr0
  "mred0 P"
  final_expr1
  "mred1' (compP1 P)"
  convert_RA
  "λt. bisim_red0_Red1" 
  bisim_wait01
  "τMOVE0 P"
  "τMOVE1 (compP1 P)"
  for P
.

context J0_J1_heap_base begin

lemma delay_bisimulation_red0_Red1: 
  assumes wf: "wf_J_prog P"
  shows "delay_bisimulation_measure (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 (ta_bisim (λt. bisim_red0_Red1)) (τMOVE0 P) (τMOVE1 (compP1 P)) (λes es'. False) (λ(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e'< countInitBlock e)"
  (is "delay_bisimulation_measure _ _ _ _ _ _ ?μ1 ?μ2")
proof(unfold_locales)
  fix s1 s2 s1'
  assume "bisim_red0_Red1 s1 s2" "red0_mthr.silent_move P t s1 s1'"
  moreover obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)" by(cases s1, auto)
  moreover obtain ex1' exs1' h1' where s1': "s1' = ((ex1', exs1'), h1')" by(cases s1', auto)
  moreover obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)" by(cases s2, auto)
  ultimately have bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and heap: "h1 = h2"
    and red: "P,t ⊢0 ⟨ex1/exs1,h1⟩ -ε→ ⟨ex1'/exs1',h1'⟩"
    and τ: "τMove0 P h1 (ex1, exs1)"
    by(auto simp add: bisim_red0_Red1_def red0_mthr.silent_move_iff)
  from Red1_simulates_red0[OF wf red bisim] τ
  obtain ex2'' exs2'' where bisim': "bisim_list1 (ex1', exs1') (ex2'', exs2'')" 
    and red': "τRed1't (compP1 P) t h1 (ex2, exs2) (ex2'', exs2'')"
    and [simp]: "h1' = h1" by auto
  from τRed1't_into_Red1'_τmthr_silent_movet[OF red'] bisim' heap
  have "∃s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' ∧ bisim_red0_Red1 s1' s2'"
    unfolding s2 s1' by(auto simp add: bisim_red0_Red1_def)
  thus "bisim_red0_Red1 s1' s2 ∧ ?μ1^++ s1' s1 ∨ (∃s2'. Red1_mthr.silent_movet False (compP1 P) t s2 s2' ∧ bisim_red0_Red1 s1' s2')" ..
next
  fix s1 s2 s2'
  assume "bisim_red0_Red1 s1 s2" "Red1_mthr.silent_move False (compP1 P) t s2 s2'"
  moreover obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)" by(cases s1, auto)
  moreover obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)" by(cases s2, auto)
  moreover obtain ex2' exs2' h2' where s2': "s2' = ((ex2', exs2'), h2')" by(cases s2', auto)
  ultimately have bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and heap: "h1 = h2"
    and red: "False,compP1 P,t ⊢1 ⟨ex2/exs2,h2⟩ -ε→ ⟨ex2'/exs2',h2'⟩"
    and τ: "τMove1 P h2 (ex2, exs2)"
    by(fastforce simp add: bisim_red0_Red1_def Red1_mthr.silent_move_iff)+
  from red0_simulates_Red1[OF wf red bisim] τ
  obtain e' es' where bisim': "bisim_list1 (e', es') (ex2', exs2')"
    and red': "τRed0t P t h2 (ex1, exs1) (e', es') ∨ 
               countInitBlock (fst ex2') < countInitBlock (fst ex2) ∧ exs2' = exs2 ∧ e' = ex1 ∧ es' = exs1"
    and [simp]: "h2' = h2" by auto
  from red'
  show "bisim_red0_Red1 s1 s2' ∧ ?μ2^++ s2' s2 ∨ (∃s1'. red0_mthr.silent_movet P t s1 s1' ∧ bisim_red0_Red1 s1' s2')"
    (is "?refl ∨ ?step")
  proof
    assume "τRed0t P t h2 (ex1, exs1) (e', es')"
    from τRed0t_into_red0_τmthr_silent_movet[OF this] bisim' heap
    have ?step unfolding s1 s2' by(auto simp add: bisim_red0_Red1_def)
    thus ?thesis ..
  next
    assume "countInitBlock (fst ex2') < countInitBlock (fst ex2) ∧ exs2' = exs2 ∧ e' = ex1 ∧ es' = exs1"
    hence ?refl using bisim' heap unfolding s1 s2' s2
      by (auto simp add: bisim_red0_Red1_def split_beta)
    thus ?thesis ..
  qed
next
  fix s1 s2 ta1 s1'
  assume "bisim_red0_Red1 s1 s2"  and "mred0 P t s1 ta1 s1'" and τ: "¬ τMOVE0 P s1 ta1 s1'"
  moreover obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)" by(cases s1, auto)
  moreover obtain ex1' exs1' h1' where s1': "s1' = ((ex1', exs1'), h1')" by(cases s1', auto)
  moreover obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)" by(cases s2, auto)
  ultimately have heap: "h2 = h1"
    and bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and red: "P,t ⊢0 ⟨ex1/exs1,h1⟩ -ta1→ ⟨ex1'/exs1',h1'⟩"
    by(auto simp add: bisim_red0_Red1_def)
  from τ have "¬ τMove0 P h1 (ex1, exs1)" unfolding s1
    using red by(auto elim!: red0.cases dest: red_τ_taD[where extTA="extTA2J0 P", OF extTA2J0_ε])
  with Red1_simulates_red0[OF wf red bisim]
  obtain ex2'' exs2'' ex2' exs2' ta'
    where bisim': "bisim_list1 (ex1', exs1') (ex2'', exs2'')"
    and red': "τRed1'r (compP1 P) t h1 (ex2, exs2) (ex2', exs2')"
    and red'': "False,compP1 P,t ⊢1 ⟨ex2'/exs2',h1⟩ -ta'→ ⟨ex2''/exs2'',h1'⟩"
    and τ': "¬ τMove1 P h1 (ex2', exs2')"
    and ta: "ta_bisim01 ta1 ta'" by fastforce
  from red'' have "mred1' (compP1 P) t ((ex2', exs2'), h1) ta' ((ex2'', exs2''), h1')" by auto
  moreover from τ' have "¬ τMOVE1 (compP1 P) ((ex2', exs2'), h1) ta' ((ex2'', exs2''), h1')" by simp
  moreover from red' have "Red1_mthr.silent_moves False (compP1 P) t s2 ((ex2', exs2'), h1)"
    unfolding s2 heap by(rule τRed1'r_into_Red1'_τmthr_silent_moves)
  moreover from bisim' have "bisim_red0_Red1 ((ex1', exs1'), h1') ((ex2'', exs2''), h1')"
    by(auto simp add: bisim_red0_Red1_def)
  ultimately
  show "∃s2' s2'' ta2. Red1_mthr.silent_moves False (compP1 P) t s2 s2' ∧ mred1' (compP1 P) t s2' ta2 s2'' ∧
             ¬ τMOVE1 (compP1 P) s2' ta2 s2'' ∧ bisim_red0_Red1 s1' s2'' ∧ ta_bisim01 ta1 ta2"
    using ta unfolding s1' by blast
next
  fix s1 s2 ta2 s2'
  assume "bisim_red0_Red1 s1 s2"  and "mred1' (compP1 P) t s2 ta2 s2'" and τ: "¬ τMOVE1 (compP1 P) s2 ta2 s2'"
  moreover obtain ex1 exs1 h1 where s1: "s1 = ((ex1, exs1), h1)" by(cases s1, auto)
  moreover obtain ex2 exs2 h2 where s2: "s2 = ((ex2, exs2), h2)" by(cases s2, auto)
  moreover obtain ex2' exs2' h2' where s2': "s2' = ((ex2', exs2'), h2')" by(cases s2', auto)
  ultimately have heap: "h2 = h1"
    and bisim: "bisim_list1 (ex1, exs1) (ex2, exs2)"
    and red: "False,compP1 P,t ⊢1 ⟨ex2/exs2,h1⟩ -ta2→ ⟨ex2'/exs2',h2'⟩"
    by(auto simp add: bisim_red0_Red1_def)
  from τ heap have "¬ τMove1 P h2 (ex2, exs2)" unfolding s2
    using red by(fastforce elim!: Red1.cases dest: red1_τ_taD)
  with red0_simulates_Red1[OF wf red bisim]
  obtain e' es' e'' es'' ta'
    where bisim': "bisim_list1 (e', es') (ex2', exs2')"
    and red': "τRed0r P t h1 (ex1, exs1) (e'', es'')"
    and red'': "P,t ⊢0 ⟨e''/es'',h1⟩ -ta'→ ⟨e'/es',h2'⟩"
    and τ': "¬ τMove0 P h1 (e'', es'')"
    and ta: "ta_bisim01 ta' ta2" using heap by fastforce
  from red'' have "mred0 P t ((e'', es''), h1) ta' ((e', es'), h2')" by auto
  moreover from red' have "red0_mthr.silent_moves P t ((ex1, exs1), h1) ((e'', es''), h1)"
    by(rule τRed0r_into_red0_τmthr_silent_moves)
  moreover from τ' have "¬ τMOVE0 P ((e'', es''), h1) ta' ((e', es'), h2')" by simp
  moreover from bisim' have "bisim_red0_Red1 ((e', es'), h2') ((ex2', exs2'), h2')"
    by(auto simp add: bisim_red0_Red1_def)
  ultimately
  show "∃s1' s1'' ta1. red0_mthr.silent_moves P t s1 s1' ∧
             mred0 P t s1' ta1 s1'' ∧ ¬ τMOVE0 P s1' ta1 s1'' ∧
             bisim_red0_Red1 s1'' s2' ∧ ta_bisim01 ta1 ta2"
    using ta unfolding s1 s2' by blast
next
  show "wfP ?μ1" by auto
next
  have "wf (measure countInitBlock)" ..
  hence "wf (inv_image (measure countInitBlock) (λ(((e', xs'), exs'), h'). e'))" ..
  also have "inv_image (measure countInitBlock) (λ(((e', xs'), exs'), h'). e') = {(s2', s2). ?μ2 s2' s2}"
    by(simp add: inv_image_def split_beta)
  finally show "wfP ?μ2" by(simp add: wfp_def)
qed

lemma delay_bisimulation_diverge_red0_Red1: 
  assumes "wf_J_prog P"
  shows "delay_bisimulation_diverge (mred0 P t) (mred1' (compP1 P) t) bisim_red0_Red1 (ta_bisim (λt. bisim_red0_Red1)) (τMOVE0 P) (τMOVE1 (compP1 P))"
proof -
  interpret delay_bisimulation_measure
    "mred0 P t" "mred1' (compP1 P) t" "bisim_red0_Red1" "ta_bisim (λt. bisim_red0_Red1)" "τMOVE0 P" "τMOVE1 (compP1 P)"
    "λes es'. False" "λ(((e', xs'), exs'), h') (((e, xs), exs), h). countInitBlock e'< countInitBlock e"
    using assms by(rule delay_bisimulation_red0_Red1)
  show ?thesis by unfold_locales
qed

lemma red0_Red1'_FWweak_bisim:
  assumes wf: "wf_J_prog P"
  shows "FWdelay_bisimulation_diverge final_expr0 (mred0 P) final_expr1 (mred1' (compP1 P))
           (λt. bisim_red0_Red1) bisim_wait01 (τMOVE0 P) (τMOVE1 (compP1 P))"
proof -
  interpret delay_bisimulation_diverge
    "mred0 P t"
    "mred1' (compP1 P) t" 
    bisim_red0_Red1 
    "ta_bisim (λt. bisim_red0_Red1)" "τMOVE0 P" "τMOVE1 (compP1 P)"
    for t
    using wf by(rule delay_bisimulation_diverge_red0_Red1)
  show ?thesis
  proof
    fix t and s1 and s2 :: "(('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list) × 'heap"
    assume "bisim_red0_Red1 s1 s2" "(λ(x1, m). final_expr0 x1) s1"
    moreover hence "(λ(x2, m). final_expr1 x2) s2"
      by(cases s1)(cases s2,auto simp add: bisim_red0_Red1_def final_iff elim!: bisim_list1_elim elim: bisim_list.cases)
    ultimately show "∃s2'. Red1_mthr.silent_moves False (compP1 P) t s2 s2' ∧ bisim_red0_Red1 s1 s2' ∧ (λ(x2, m). final_expr1 x2) s2'"
      by blast
  next
    fix t s1 and s2 :: "(('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list) × 'heap"
    assume "bisim_red0_Red1 s1 s2" "(λ(x2, m). final_expr1 x2) s2"
    moreover hence "(λ(x1, m). final_expr0 x1) s1"
      by(cases s1)(cases s2,auto simp add: bisim_red0_Red1_def final_iff elim!: bisim_list1_elim elim: bisim_list.cases)
    ultimately show "∃s1'. red0_mthr.silent_moves P t s1 s1' ∧ bisim_red0_Red1 s1' s2 ∧ (λ(x1, m). final_expr0 x1) s1'"
      by blast
  next
    fix t' x m1 x' m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'
    assume b: "bisim_red0_Red1 (x, m1) (x', m2)"
      and bo: "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and τred1: "red0_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red1: "mred0 P t (x1', m1) ta1 (x1'', m1')"
      and τ1: "¬ τMOVE0 P (x1', m1) ta1 (x1'', m1')"
      and τred2: "Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)"
      and red2: "mred1' (compP1 P) t (x2', m2) ta2 (x2'', m2')"
      and bo': "bisim_red0_Red1 (x1'', m1') (x2'', m2')"
      and tb: "ta_bisim (λt. bisim_red0_Red1) ta1 ta2"
    from b have "m1 = m2" by(auto simp add: bisim_red0_Red1_def split_beta)
    moreover from bo' have "m1' = m2'" by(auto simp add: bisim_red0_Red1_def split_beta)
    ultimately show "bisim_red0_Red1 (x, m1') (x', m2')" using b
      by(auto simp add: bisim_red0_Red1_def split_beta)
  next
    fix t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w
    assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "red0_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red0: "mred0 P t (x1', m1) ta1 (x1'', m1')"
      and "¬ τMOVE0 P (x1', m1) ta1 (x1'', m1')"
      and "Red1_mthr.silent_moves False (compP1 P) t (x2, m2) (x2', m2)"
      and red1: "mred1' (compP1 P) t (x2', m2) ta2 (x2'', m2')"
      and "¬ τMOVE1 (compP1 P) (x2', m2) ta2 (x2'', m2')"
      and "bisim_red0_Red1 (x1'', m1') (x2'', m2')"
      and "ta_bisim01 ta1 ta2"
      and Suspend: "Suspend w ∈ set ⦃ta1⦄⇘w⇙" "Suspend w ∈ set ⦃ta2⦄⇘w⇙"
    from red0 red1 Suspend show "bisim_wait01 x1'' x2''"
      by(cases x2')(cases x2'', auto dest: Red_Suspend_is_call Red1_Suspend_is_call simp add: split_beta bisim_wait01_def is_call_def)
  next
    fix t x1 m1 x2 m2 ta1 x1' m1'
    assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "bisim_wait01 x1 x2"
      and "mred0 P t (x1, m1) ta1 (x1', m1')"
      and wakeup: "Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙"
    moreover obtain e0 es0 where [simp]: "x1 = (e0, es0)" by(cases x1)
    moreover obtain e0' es0' where [simp]: "x1' = (e0', es0')" by(cases x1')
    moreover obtain e1 xs1 exs1 where [simp]: "x2 = ((e1, xs1), exs1)" by(cases x2) auto
    ultimately have bisim: "bisim_list1 (e0, es0) ((e1, xs1), exs1)"
      and m1: "m2 = m1"
      and call: "call e0 ≠ None" "call1 e1 ≠ None"
      and red: "P,t ⊢0 ⟨e0/es0, m1⟩ -ta1→ ⟨e0'/es0', m1'⟩"
      by(auto simp add: bisim_wait01_def bisim_red0_Red1_def)
    from red wakeup have "¬ τMove0 P m1 (e0, es0)"
      by(auto elim!: red0.cases dest: red_τ_taD[where extTA="extTA2J0 P", simplified])
    with Red1_simulates_red0[OF wf red bisim] call m1
    show "∃ta2 x2' m2'. mred1' (compP1 P) t (x2, m2) ta2 (x2', m2') ∧ bisim_red0_Red1 (x1', m1') (x2', m2') ∧ ta_bisim01 ta1 ta2"
      by(auto simp add: bisim_red0_Red1_def)
  next
    fix t x1 m1 x2 m2 ta2 x2' m2'
    assume "bisim_red0_Red1 (x1, m1) (x2, m2)"
      and "bisim_wait01 x1 x2" 
      and "mred1' (compP1 P) t (x2, m2) ta2 (x2', m2')"
      and wakeup: "Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙"
    moreover obtain e0 es0 where [simp]: "x1 = (e0, es0)" by(cases x1)
    moreover obtain e1 xs1 exs1 where [simp]: "x2 = ((e1, xs1), exs1)" by(cases x2) auto
    moreover obtain e1' xs1' exs1' where [simp]: "x2' = ((e1', xs1'), exs1')" by(cases x2') auto
    ultimately have bisim: "bisim_list1 (e0, es0) ((e1, xs1), exs1)"
      and m1: "m2 = m1"
      and call: "call e0 ≠ None" "call1 e1 ≠ None"
      and red: "False,compP1 P,t ⊢1 ⟨(e1, xs1)/exs1, m1⟩ -ta2→ ⟨(e1', xs1')/exs1', m2'⟩"
      by(auto simp add: bisim_wait01_def bisim_red0_Red1_def)
    from red wakeup have "¬ τMove1 P m1 ((e1, xs1), exs1)"
      by(auto elim!: Red1.cases dest: red1_τ_taD)
    with red0_simulates_Red1[OF wf red bisim] m1 call
    show "∃ta1 x1' m1'. mred0 P t (x1, m1) ta1 (x1', m1') ∧ bisim_red0_Red1 (x1', m1') (x2', m2') ∧ ta_bisim01 ta1 ta2"
      by(auto simp add: bisim_red0_Red1_def)
  next
    show "(∃x. final_expr0 x) ⟷ (∃x. final_expr1 x)"
      by(auto simp add: split_paired_Ex final_iff)
  qed
qed

lemma bisim_J0_J1_start:
  assumes wf: "wf_J_prog P"
  and start: "wf_start_state P C M vs"
  shows "red0_Red1'.mbisim (J0_start_state P C M vs) (J1_start_state (compP1 P) C M vs)"
proof -
  from start obtain Ts T pns body D
    where sees: "P ⊢ C sees M:Ts→T=⌊(pns,body)⌋ in D"
    and conf: "P,start_heap ⊢ vs [:≤] Ts"
    by cases auto
  from conf have vs: "length vs = length Ts" by(rule list_all2_lengthD)
  from sees_wf_mdecl[OF wf_prog_wwf_prog[OF wf] sees]
  have fvbody: "fv body ⊆ {this} ∪ set pns" and len: "length pns = length Ts"
    by(auto simp add: wf_mdecl_def)
  with vs have fv: "fv (blocks pns Ts vs body) ⊆ {this}" by auto
  have wfCM: "wf_J_mdecl P D (M, Ts, T, pns, body)"
    using sees_wf_mdecl[OF wf sees] by(auto simp add: wf_mdecl_def)
  then obtain T' where wtbody: "P,[this # pns [↦] Class D # Ts] ⊢ body :: T'" by auto
  hence elbody: "expr_locks body = (λl. 0)" by(rule WT_expr_locks)
  hence cisbody: "¬ contains_insync body" by(auto simp add: contains_insync_conv)
  from wfCM len vs have dabody: "𝒟 (blocks pns Ts vs body) ⌊{this}⌋" by auto
  from sees have sees1: "compP1 P ⊢ C sees M:Ts→T = ⌊compE1 (this # pns) body⌋ in D"
    by(auto dest: sees_method_compP[where f="(λC M Ts T (pns, body). compE1 (this # pns) body)"])

  let ?e = "blocks1 0 (Class C#Ts) (compE1 (this # pns) body)"
  let ?xs = "Null # vs @ replicate (max_vars body) undefined_value"
  from fvbody cisbody len vs
  have "bisim [] (blocks (this # pns) (Class D # Ts) (Null # vs) body) (blocks1 (length ([] :: vname list)) (Class D # Ts) (compE1 (this # pns) body)) ?xs"
    by-(rule blocks_bisim,(fastforce simp add: nth_Cons' nth_append)+)
  with fv dabody len vs elbody sees sees1
  show ?thesis unfolding start_state_def
    by(auto intro!: red0_Red1'.mbisimI split: if_split_asm)(auto simp add: bisim_red0_Red1_def blocks1_max_vars intro!: bisim_list.intros bisim_list1I wset_thread_okI)
qed

end

end