Theory J0Bisim

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

section ‹Bisimulation proof for between source code small step semantics
  with and without callstacks for single threads›

theory J0Bisim imports
  J0
  "../J/JWellForm"
  "../Common/ExternalCallWF"
begin

inductive wf_state :: "'addr expr × 'addr expr list  bool"
  where
  " fvs (e # es) = {}; e  set es. is_call e 
    wf_state (e, es)"

inductive bisim_red_red0 :: "('addr expr × 'addr locals) × 'heap  ('addr expr × 'addr expr list) × 'heap  bool"
  where
  "wf_state ees  bisim_red_red0 ((collapse ees, Map.empty), h) (ees, h)"

abbreviation ta_bisim0 :: "('addr, 'thread_id, 'heap) J_thread_action  ('addr, 'thread_id, 'heap) J0_thread_action  bool"
where "ta_bisim0  ta_bisim (λt. bisim_red_red0)"

lemma wf_state_iff [simp, code]:
  "wf_state (e, es)  fvs (e # es) = {}  (e  set es. is_call e)"
by(simp add: wf_state.simps)

lemma bisim_red_red0I [intro]:
  " e' = collapse ees; xs = Map.empty; h' = h; wf_state ees   bisim_red_red0 ((e', xs), h') (ees, h)"
by(simp add: bisim_red_red0.simps del: split_paired_Ex)

lemma bisim_red_red0_final0D:
  " bisim_red_red0 (x1, m1) (x2, m2); final_expr0 x2   final_expr x1"
by(erule bisim_red_red0.cases) auto

context J_heap_base begin

lemma red0_preserves_wf_state:
  assumes wf: "wwf_J_prog P"
  and red: "P,t ⊢0 e / es, h -ta e' / es', h'"
  and wf_state: "wf_state (e, es)"
  shows "wf_state (e', es')"
using wf_state
proof(cases)
  assume "fvs (e # es) = {}" and icl: "e  set es. is_call e"
  hence fv: "fv e = {}" "fvs es = {}" by auto
  show ?thesis
  proof
    from red show "fvs (e' # es') = {}"
    proof cases
      case (red0Red xs')
      hence [simp]: "es' = es"
        and red: "extTA2J0 P,P,t  e,(h, Map.empty) -ta e',(h', xs')" by auto
      from red_fv_subset[OF wf red] fv have "fv e' = {}" by auto
      with fv show ?thesis by simp
    next
      case (red0Call a M vs U Ts T pns body D)
      hence [simp]: "ta = ε"
        "e' = blocks (this # pns) (Class D # Ts) (Addr a # vs) body"
        "es' = e # es" "h' = h"
        and sees: "P  class_type_of U sees M: TsT = (pns, body) in D" by auto
      from sees_wf_mdecl[OF wf sees]
      have "fv body  insert this (set pns)" "length Ts = length pns" by(simp_all add: wf_mdecl_def)
      thus ?thesis using fv length vs = length pns by auto
    next
      case (red0Return E)
      with fv_inline_call[of e E] show ?thesis using fv by auto
    qed
  next
    from red icl show "eset es'. is_call e"
      by cases(simp_all add: is_call_def)
  qed
qed

lemma new_thread_bisim0_extNTA2J_extNTA2J0:
  assumes wf: "wwf_J_prog P"
  and red: "P,t  a'M'(vs), h -ta→ext va, h'"
  and nt: "NewThread t' CMa m  set tat"
  shows "bisim_red_red0 (extNTA2J P CMa, m) (extNTA2J0 P CMa, m)"
proof -
  obtain C M a where CMa [simp]: "CMa = (C, M, a)" by(cases CMa)
  from red nt have [simp]: "m = h'" by(rule red_ext_new_thread_heap)
  from red_external_new_thread_sees[OF wf red nt[unfolded CMa]]
  obtain T pns body D where h'a: "typeof_addr h' a = Class_type C"
    and sees: "P  C sees M: []T = (pns, body) in D" by auto
  from sees_wf_mdecl[OF wf sees] have "fv body  {this}" by(auto simp add: wf_mdecl_def)
  with red nt h'a sees show ?thesis by(fastforce simp add: is_call_def intro: bisim_red_red0.intros)
qed

lemma ta_bisim0_extNTA2J_extNTA2J0:
  " wwf_J_prog P; P,t  a'M'(vs), h -ta→ext va, h' 
   ta_bisim0 (extTA2J P ta) (extTA2J0 P ta)"
apply(auto simp add: ta_bisim_def intro!: list_all2_all_nthI)
apply(case_tac "tat ! n")
apply(simp_all)
apply(erule (1) new_thread_bisim0_extNTA2J_extNTA2J0)
apply(auto simp add: in_set_conv_nth)
done

lemma assumes wf: "wwf_J_prog P"
  shows red_red0_tabisim0:
  "P,t  e, s -ta e', s'  ta'. extTA2J0 P,P,t  e, s -ta' e', s'  ta_bisim0 ta ta'"
  and reds_reds0_tabisim0:
  "P,t  es, s [-ta→] es', s'  ta'. extTA2J0 P,P,t  es, s [-ta'→] es', s'  ta_bisim0 ta ta'"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s')
  note red = P,t  aM(vs),hp s -ta→ext va,h'
  note T = typeof_addr (hp s) a = T
  from T P  class_type_of T sees M: TsTr = Native in D red
  have "extTA2J0 P,P,t  addr aM(map Val vs),s -extTA2J0 P ta e',(h', lcl s)"
    by(rule red_reds.RedCallExternal)(simp_all add: e' = extRet2J (addr aM(map Val vs)) va)
  moreover from ta' = extTA2J P ta T red wf
  have "ta_bisim0 ta' (extTA2J0 P ta)" by(auto intro: ta_bisim0_extNTA2J_extNTA2J0)
  ultimately show ?case unfolding s' = (h', lcl s) by blast
next
  case RedTryFail thus ?case by(force intro: red_reds.RedTryFail)
qed(fastforce intro: red_reds.intros simp add: ta_bisim_def ta_upd_simps)+

lemma assumes wf: "wwf_J_prog P"
  shows red0_red_tabisim0:
  "extTA2J0 P,P,t  e, s -ta e', s'  ta'. P,t  e, s -ta' e', s'  ta_bisim0 ta' ta"
  and reds0_reds_tabisim0:
  "extTA2J0 P,P,t  es, s [-ta→] es', s'  ta'. P,t  es, s [-ta'→] es', s'  ta_bisim0 ta' ta"
proof(induct rule: red_reds.inducts)
  case (RedCallExternal s a T M Ts Tr D vs ta va h' ta' e' s')
  note red = P,t  aM(vs),hp s -ta→ext va,h'
  note T = typeof_addr (hp s) a = T
  from T P  class_type_of T sees M: TsTr = Native in D red
  have "P,t  addr aM(map Val vs),s -extTA2J P ta e',(h', lcl s)"
    by(rule red_reds.RedCallExternal)(simp_all add: e' = extRet2J (addr aM(map Val vs)) va)
  moreover from ta' = extTA2J0 P ta T red wf
  have "ta_bisim0 (extTA2J P ta) ta'" by(auto intro: ta_bisim0_extNTA2J_extNTA2J0)
  ultimately show ?case unfolding s' = (h', lcl s) by blast
next
  case RedTryFail thus ?case by(force intro: red_reds.RedTryFail)
qed(fastforce intro: red_reds.intros simp add: ta_bisim_def ta_upd_simps)+

lemma red_inline_call_red:
  assumes red: "P,t  e, (h, Map.empty) -ta e', (h', Map.empty)"
  shows "call E = aMvs  P,t  inline_call e E, (h, x) -ta inline_call e' E, (h', x)"
  (is "_  ?concl E x")

  and
  "calls Es = aMvs  P,t  inline_calls e Es, (h, x) [-ta→] inline_calls e' Es, (h', x)"
  (is "_  ?concls Es x")
proof(induct E and Es arbitrary: x and x rule: call.induct calls.induct)
  case (Call obj M pns x)
  note IHobj = x. call obj = aMvs  ?concl obj x
  note IHpns = x. calls pns = aMvs  ?concls pns x
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
  from call (objM(pns)) = aMvs have "call (objM(pns)) = (a, M', vs)" by simp
  thus ?case
  proof(induct rule: call_callE)
    case CallObj
    with IHobj[of x] show ?case by(fastforce intro: red_reds.CallObj)
  next
    case (CallParams v'')
    with IHpns[of x] show ?case by(fastforce intro: red_reds.CallParams)
  next
    case Call
    from red_lcl_add[OF red, where ?l0.0=x]
    have "P,t  e,(h, x) -ta e', (h', x)" by simp
    with Call show ?case by(fastforce dest: BlockRed)
  qed
next
  case (Block V T' vo exp x)
  note IH = x. call exp = aMvs  ?concl exp x
  from IH[of "x(V := vo)"] call {V:T'=vo; exp} = aMvs
  show ?case by(clarsimp simp del: fun_upd_apply)(drule BlockRed, auto)
next
  case (Cons_exp exp exps x)
  show ?case
  proof(cases "is_val exp")
    case True
    with calls (exp # exps) = aMvs have "calls exps = aMvs" by auto
    with calls exps = aMvs  ?concls exps x True
    show ?thesis by(fastforce intro: ListRed2)
  next
    case False
    with calls (exp # exps) = aMvs have "call exp = aMvs" by auto
    with call exp = aMvs  ?concl exp x
    show ?thesis by(fastforce intro: ListRed1)
  qed
qed(fastforce intro: red_reds.intros)+

lemma 
  assumes "P  class_type_of T sees M:UsU = (pns, body) in D" "length vs = length pns" "length Us = length pns"
  shows is_call_red_inline_call:
  " call e = (a, M, vs); typeof_addr (hp s) a = T  
   P,t  e, s -ε inline_call (blocks (this # pns) (Class D # Us) (Addr a # vs) body) e, s"
  (is "_  _  ?red e s")
  and is_calls_reds_inline_calls:
  " calls es = (a, M, vs); typeof_addr (hp s) a = T  
   P,t  es, s [-ε→] inline_calls (blocks (this # pns) (Class D # Us) (Addr a # vs) body) es, s"
  (is "_  _  ?reds es s")
proof(induct e and es arbitrary: s and s rule: call.induct calls.induct)
  case (Call obj M' params s)
  note IHObj = s. call obj = (a, M, vs); typeof_addr (hp s) a = T   ?red obj s
  note IHParams = s.  calls params = (a, M, vs); typeof_addr (hp s) a = T   ?reds params s
  from call (objM'(params)) = (a, M, vs)
  show ?case
  proof(induct rule: call_callE)
    case CallObj
    from IHObj[OF CallObj] typeof_addr (hp s) a = T have "?red obj s" by blast
    moreover from CallObj have "¬ is_val obj" by auto
    ultimately show ?case by(auto intro: red_reds.CallObj)
  next
    case (CallParams v)
    from IHParams[OF calls params = (a, M, vs)] typeof_addr (hp s) a = T
    have "?reds params s" by blast
    moreover from CallParams have "¬ is_vals params" by auto
    ultimately show ?case using obj = Val v by(auto intro: red_reds.CallParams)
  next
    case Call
    with RedCall[where s=s, simplified, OF typeof_addr (hp s) a = T P  class_type_of T sees M:UsU = (pns, body) in D length vs = length pns length Us = length pns] 
    show ?thesis by(simp)
  qed
next
  case (Block V ty vo exp s)
  note IH = s. call exp = (a, M, vs); typeof_addr (hp s) a = T   ?red exp s
  from call {V:ty=vo; exp} = (a, M, vs) IH[of "(hp s, (lcl s)(V := vo))"] typeof_addr (hp s) a = T
  show ?case by(cases s, simp del: fun_upd_apply)(drule red_reds.BlockRed, simp)
qed(fastforce intro: red_reds.intros)+

lemma red_inline_call_red':
  assumes fv: "fv ee = {}"
  and eefin: "¬ final ee"
  shows " call E = aMvs; P,t  inline_call ee E, (h, x) -ta E', (h', x')  
          ee'. E' = inline_call ee' E  P,t  ee, (h, Map.empty) -ta ee', (h', Map.empty)  x = x'"
  (is " _; _   ?concl E E' x x'")
  and   " calls Es = aMvs; P,t  inline_calls ee Es, (h, x) [-ta→] Es', (h', x')  
          ee'. Es' = inline_calls ee' Es  P,t  ee, (h, Map.empty) -ta ee', (h', Map.empty)  x = x'"
  (is " _; _   ?concls Es Es' x x'")
proof(induct E and Es arbitrary: E' x x' and Es' x x' rule: call.induct calls.induct)
  case new thus ?case by simp
next
  case (newArray T exp E' x x')
  thus ?case using eefin by(auto elim!: red_cases)
next
  case Cast thus ?case using eefin by(auto elim!:red_cases) 
next
  case InstanceOf thus ?case using eefin by(auto elim!:red_cases) 
next
  case Val thus ?case by simp
next
  case Var thus ?case by simp
next
  case LAss
  thus ?case using eefin by(auto elim!: red_cases)
next
  case BinOp
  thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case AAcc
  thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case AAss thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case ALen thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case FAcc thus ?case using eefin by(auto elim!: red_cases)
next
  case FAss thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case CompareAndSwap thus ?case using eefin by(auto elim!: red_cases split: if_split_asm)
next
  case (Call obj M pns E' x x')
  note IHobj = x E' x'. call obj = aMvs; P,t  inline_call ee obj,(h, x) -ta E',(h', x')
                 ?concl obj E' x x'
  note IHpns = Es' x x'. calls pns = aMvs; P,t  inline_calls ee pns,(h, x) [-ta→] Es',(h', x')
                ?concls pns Es' x x'
  note red = P,t  inline_call ee (objM(pns)),(h, x) -ta  E',(h', x')
  obtain a M' vs where [simp]: "aMvs = (a, M', vs)" by(cases aMvs, auto)
  from call (objM(pns)) = aMvs have "call (objM(pns)) = (a,M',vs)" by simp
  thus ?case
  proof(cases rule: call_callE)
    case CallObj
    hence "¬ is_val obj" by auto
    with red CallObj eefin obtain obj' where "E' = obj'M(pns)" 
      and red': "P,t  inline_call ee obj,(h, x) -ta obj',(h', x')"
      by(auto elim!: red_cases)
    from IHobj[OF _ red'] CallObj obtain ee' 
      where "inline_call ee' obj = obj'" "x = x'"
      and "P,t  ee,(h, Map.empty) -ta ee',(h', Map.empty)" by(auto simp del: fun_upd_apply)
    with E' = obj'M(pns) CallObj red' show ?thesis by(fastforce simp del: fun_upd_apply)
  next
    case (CallParams v'')
    hence "¬ is_vals pns" by auto
    with red CallParams eefin obtain pns' where "E' = objM(pns')" 
      and red': "P,t  inline_calls ee pns,(h, x) [-ta→] pns',(h', x')"
      by(auto elim!: red_cases)
    from IHpns[OF _ red'] CallParams obtain ee' 
      where "inline_calls ee' pns = pns'" "x = x'"
      and "P,t  ee,(h, Map.empty) -ta ee',(h', Map.empty)"
      by(auto simp del: fun_upd_apply)
    with E' = objM(pns') CallParams red' ¬ is_vals pns
    show ?thesis by(auto simp del: fun_upd_apply)
  next
    case Call
    with red have red': "P,t  ee,(h, x) -ta E',(h', x')" by(auto)
    from red_lcl_sub[OF red', of "{}"] fv
    have "P,t  ee,(h, Map.empty) -ta E',(h', Map.empty)" by simp
    moreover have "x' = x"
    proof(rule ext)
      fix V
      from red_notfree_unchanged[OF red', of V] fv
      show "x' V = x V" by simp
    qed
    ultimately show ?thesis using Call by simp
  qed
next
  case (Block V ty voo exp E' x x')
  note IH = x E' x'. call exp = aMvs; P,t  inline_call ee exp,(h, x) -ta E',(h', x')
             ?concl exp E' x x'
  from call {V:ty=voo; exp} = aMvs have ic: "call exp = aMvs" by simp
  note red = P,t  inline_call ee {V:ty=voo; exp},(h, x) -ta E',(h', x')
  hence "P,t  {V:ty=voo; inline_call ee exp},(h, x) -ta E',(h', x')" by simp
  with ic eefin obtain exp' x'' where "E' = {V:ty=x'' V; exp'}"
    and red': "P,t  inline_call ee exp,(h, fun_upd x V voo) -ta exp',(h', x'')"
    and "x' = fun_upd x'' V (x V)"
    by -(erule red.cases,auto dest: inline_call_eq_Val)
  from IH[OF ic red'] obtain ee' vo' 
    where icl: "inline_call ee' exp = exp'" "x'' = fun_upd x V voo"
    and red'': "P,t  ee,(h, Map.empty) -ta ee',(h', Map.empty)" by blast
  from x'' = fun_upd x V voo have "x'' V = voo" by(simp add: fun_eq_iff)
  with icl red'' E' = {V:ty=x'' V; exp'} x' = fun_upd x'' V (x V) red'
  show ?case by(auto simp del: fun_upd_apply)
next
  case Synchronized thus ?case using eefin by(auto elim!: red_cases)
next
  case InSynchronized thus ?case using eefin by(auto elim!: red_cases)
next
  case Seq 
  thus ?case using eefin by(auto elim!: red_cases)
next
  case Cond thus ?case using eefin by(auto elim!: red_cases)
next
  case While thus ?case by simp
next
  case throw
  thus ?case using eefin by(auto elim!: red_cases)
next
  case TryCatch
  thus ?case using eefin by(auto elim!: red_cases)
next
  case Nil_exp thus ?case by simp
next
  case Cons_exp
  thus ?case using eefin by(auto elim!: reds_cases split: if_split_asm)
qed

lemma assumes sees: "P  class_type_of T sees M:UsU = (pns, body) in D"
  shows is_call_red_inline_callD:
  " P,t  e, s -ta e', s'; call e = (a, M, vs); typeof_addr (hp s) a = T 
   e' = inline_call (blocks (this # pns) (Class D # Us) (Addr a # vs) body) e"
  and is_calls_reds_inline_callsD:
  " P,t  es, s [-ta→] es', s'; calls es = (a, M, vs); typeof_addr (hp s) a = T 
   es' = inline_calls (blocks (this # pns) (Class D # Us) (Addr a # vs) body) es"
proof(induct rule: red_reds.inducts)
  case RedCall with sees show ?case by(auto dest: sees_method_fun)
next
  case RedCallExternal
  with sees show ?case by(auto dest: sees_method_fun)
next
  case (BlockRed e h x V vo ta e' h' x' T')
  from call {V:T'=vo; e} = (a, M, vs) typeof_addr (hp (h, x)) a = T sees
  have "call e = (a, M, vs)" and "¬ synthesized_call P h (a, M, vs)"
    by(auto simp add: synthesized_call_conv dest: sees_method_fun)
  with P,t  e,(h, x(V := vo)) -ta e',(h', x')
  have "x(V := vo) = x'" by(auto dest: is_call_red_state_unchanged)
  hence "x' V = vo" by auto
  with BlockRed show ?case by(simp)
qed(fastforce split: if_split_asm)+

lemma (in -) wf_state_ConsD: "wf_state (e, e' # es)  wf_state (e', es)"
by(simp)

lemma red_fold_exs:
  " P,t  e,(h, Map.empty) -ta e',(h', Map.empty); wf_state (e, es) 
    P,t  collapse (e, es), (h, Map.empty) -ta collapse (e', es), (h', Map.empty)"
  (is " _; _   ?concl e e' es")
proof(induction es arbitrary: e e')
  case Nil thus ?case by simp
next
  case (Cons E es)
  note wf = wf_state (e, E # es)
  note red = P,t  e,(h, Map.empty) -ta e',(h', Map.empty)
  from wf obtain a M vs arrobj where call: "call E = (a, M, vs)" 
    by(auto simp add: is_call_def)
  from red call have "P,t  inline_call e E,(h, Map.empty) -ta inline_call e' E,(h', Map.empty)"
    by(rule red_inline_call_red)
  hence "P,t  collapse (inline_call e E, es),(h, Map.empty) -ta  collapse (inline_call e' E, es),(h', Map.empty)"
  proof(rule Cons.IH)
    from wf have "fv E = {}" "fv e = {}" by auto
    with fv_inline_call[of e E] have "fv (inline_call e E) = {}" by auto
    thus "wf_state (inline_call e E, es)" using wf by auto
  qed
  thus ?case by simp
qed

lemma red_fold_exs':
  " P,t  collapse (e, es), (h, Map.empty) -ta e', (h', x'); wf_state (e, es); ¬ final e 
   E'. e' = collapse (E', es)  P,t  e, (h, Map.empty) -ta E', (h', Map.empty)"
  (is " _; _; _   ?concl e es")
proof(induction es arbitrary: e)
  case Nil
  hence red': "P,t  e,(h, Map.empty) -ta e',(h', x')" by simp
  with red_dom_lcl[OF this] wf_state (e, []) show ?case by auto
next
  case (Cons E es)
  note wf = wf_state (e, E # es)
  note nfin = ¬ final e
  from wf have "fv e = {}" by simp
  from wf obtain a M vs where call: "call E = (a, M, vs)" by(auto simp add: is_call_def)
  from P,t  collapse (e, E # es),(h, Map.empty) -ta e',(h', x')
  have "P,t  collapse (inline_call e E, es),(h, Map.empty) -ta e',(h', x')" by simp
  moreover from wf fv_inline_call[of e E] have "wf_state (inline_call e E, es)" by auto
  moreover from nfin call have "¬ final (inline_call e E)" by(auto elim!: final.cases)
  ultimately have "?concl (inline_call e E) es" by(rule Cons.IH)
  then obtain E' where e': "e' = collapse (E', es)" 
    and red': "P,t  inline_call e E,(h, Map.empty) -ta E',(h', Map.empty)" by blast
  from red_inline_call_red'(1)[OF fv e = {} nfin call E = (a, M, vs) red']
  obtain e' where "E' = inline_call e' E" "P,t  e,(h, Map.empty) -ta e',(h', Map.empty)" by auto
  thus ?case using e' by auto
qed

lemma τRed0r_inline_call_not_final:
  "e' es'. τRed0r P t h (e, es) (e', es')  (final e'  es' = [])  collapse (e, es) = collapse (e', es')"
proof(induct es arbitrary: e)
  case Nil thus ?case by blast
next
  case (Cons e es E) show ?case
  proof(cases "final E")
    case True
    hence "τRed0 P t h (E, e # es) (inline_call E e, es)" by(auto intro: red0Return)
    moreover from Cons[of "inline_call E e"] obtain e' es'
      where "τRed0r P t h (inline_call E e, es) (e', es')" "final e'  es' = []"
      "collapse (inline_call E e, es) = collapse (e', es')" by blast
    ultimately show ?thesis unfolding collapse.simps by(blast intro: converse_rtranclp_into_rtranclp)
  qed blast
qed

lemma τRed0_preserves_wf_state:
  " wwf_J_prog P; τRed0 P t h (e, es) (e', es'); wf_state (e, es)   wf_state (e', es')"
by(auto simp del: wf_state_iff intro: red0_preserves_wf_state)

lemma τRed0r_preserves_wf_state:
  assumes wf: "wwf_J_prog P"
  shows " τRed0r P t h (e, es) (e', es'); wf_state (e, es)   wf_state (e', es')"
by(induct rule: rtranclp_induct2)(blast intro: τRed0_preserves_wf_state[OF wf])+

lemma τRed0t_preserves_wf_state:
  assumes wf: "wwf_J_prog P"
  shows " τRed0t P t h (e, es) (e', es'); wf_state (e, es)   wf_state (e', es')"
by(induct rule: tranclp_induct2)(blast intro: τRed0_preserves_wf_state[OF wf])+

lemma collapse_τmove0_inv:
  " eset es. is_call e; ¬ final e   τmove0 P h (collapse (e, es)) = τmove0 P h e"
proof(induction es arbitrary: e)
  case Nil thus ?case by clarsimp
next
  case (Cons e es e'')
  from aset (e # es). is_call a obtain aMvs where calls: "eset es. is_call e"
    and call: "call e = aMvs" by(auto simp add: is_call_def)
  note calls moreover
  from ¬ final e'' call have "¬ final (inline_call e'' e)" by(auto simp add: final_iff)
  ultimately have "τmove0 P h (collapse (inline_call e'' e, es)) = τmove0 P h (inline_call e'' e)"
    by(rule Cons.IH)
  also from call ¬ final e'' have " = τmove0 P h e''" by(auto simp add: inline_call_τmove0_inv)
  finally show ?case by simp
qed

lemma τRed0r_into_silent_moves:
  "τRed0r P t h (e, es) (e', es')  red0_mthr.silent_moves P t ((e, es), h) ((e', es'), h)"
by(induct rule: rtranclp_induct2)(fastforce intro: τtrsys.silent_move.intros elim!: rtranclp.rtrancl_into_rtrancl)+

lemma τRed0t_into_silent_movet:
  "τRed0t P t h (e, es) (e', es')  red0_mthr.silent_movet P t ((e, es), h) ((e', es'), h)"
by(induct rule: tranclp_induct2)(fastforce intro: τtrsys.silent_move.intros elim!: tranclp.trancl_into_trancl)+

lemma red_simulates_red0:
  assumes wwf: "wwf_J_prog P"
  and sim: "bisim_red_red0 s1 s2" "mred0 P t s2 ta2 s2'" "¬ τMOVE0 P s2 ta2 s2'"
  shows "s1' ta1. mred P t s1 ta1 s1'  ¬ τMOVE P s1 ta1 s1'  bisim_red_red0 s1' s2'  ta_bisim0 ta1 ta2"
proof -
  note sim
  moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
  moreover obtain e' es' h2' where s2': "s2' = ((e', es'), h2')" by(cases s2', auto)
  moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
  ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
    and red: "P,t ⊢0 e/es, h2 -ta2 e'/es', h2'" 
    and τ: "¬ τmove0 P h2 e  ¬ final e  ta2  ε" by auto
  from red τ have τ: "¬ τmove0 P h2 e" and nfin: "¬ final e"
    by(cases, auto dest: red_τ_taD[where extTA="extTA2J0 P", OF extTA2J0_ε])+
  from bisim have heap: "h1 = h2" and fold: "e1 = collapse (e, es)"
    and x1: "x1 = Map.empty" and wf_state: "wf_state (e, es)"
    by(auto elim!: bisim_red_red0.cases)
  from red wf_state have wf_state': "wf_state (e', es')" by(rule red0_preserves_wf_state[OF wwf])
  from red show ?thesis
  proof(cases)
    case (red0Red xs')
    hence [simp]: "es' = es"
      and "extTA2J0 P,P,t  e, (h2, Map.empty) -ta2 e', (h2', xs')" by auto
    from red0_red_tabisim0[OF wwf this(2)] obtain ta1
      where red': "P,t  e,(h2, Map.empty) -ta1 e',(h2', xs')"
      and tasim: "ta_bisim0 ta1 ta2" by auto
    moreover from wf_state have "fv e = {}" by auto
    with red_dom_lcl[OF red'] red_fv_subset[OF wwf red'] have "xs' = Map.empty" by auto
    ultimately have "P,t  e,(h2, Map.empty) -ta1 e',(h2', Map.empty)" by simp
    with wf_state have "P,t  collapse (e, es),(h2, Map.empty) -ta1 collapse (e', es),(h2', Map.empty)"
      by -(erule red_fold_exs, auto)
    moreover from τ wf_state fold nfin have "¬ τmove0 P h2 e1" by(auto simp add: collapse_τmove0_inv)
    hence "¬ τMOVE P ((collapse (e, es), Map.empty), h2) ta1 ((collapse (e', es), Map.empty), h2')"
      unfolding fold by auto
    moreover from wf_state' have "bisim_red_red0 ((collapse (e', es), Map.empty), h2') s2'" 
      unfolding s2' by(auto)
    ultimately show ?thesis unfolding heap s1 s2 s2' fold x1
      using tasim by(fastforce intro!: exI rtranclp.rtrancl_refl)
  next
    case red0Call
    with τ have False
      by(auto simp add: synthesized_call_def τexternal'_def dest!: τmove0_callD[where P=P and h=h2] dest: sees_method_fun)
    thus ?thesis ..
  next
    case red0Return with nfin show ?thesis by simp
  qed
qed

lemma delay_bisimulation_measure_red_red0:
  assumes wf: "wwf_J_prog P"
  shows "delay_bisimulation_measure (mred P t) (mred0 P t) bisim_red_red0 ta_bisim0 (τMOVE P) (τMOVE0 P) (λe e'. False) (λ((e, es), h) ((e, es'), h). length es < length es')"
proof
  show "wfP (λe e'. False)" by auto
next
  have "wf {(x :: nat, y). x < y}" by(rule wf_less)
  hence "wf (inv_image {(x :: nat, y). x < y} (length o snd o fst))" by(rule wf_inv_image)
  also have "inv_image {(x :: nat, y). x < y} (length o snd o fst) = {(x, y). (λ((e, es), h) ((e, es'), h). length es < length es') x y}" by auto
  finally show "wfP (λ((e, es), h) ((e, es'), h). length es < length es')"
    unfolding wfP_def .
next
  fix s1 s2 s1'
  assume "bisim_red_red0 s1 s2" and "red_mthr.silent_move P t s1 s1'"
  moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
  moreover obtain e1' h1' x1' where s1': "s1' = ((e1', x1'), h1')" by(cases s1', auto)
  moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
  ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
    and red: "P,t  e1, (h1, x1) -ε e1', (h1', x1')" 
    and τ: "τmove0 P h1 e1" by(auto elim: τtrsys.silent_move.cases)
  from bisim have heap: "h1 = h2"
    and fold: "e1 = collapse (e, es)"
    and x1: "x1 = Map.empty"
    and wf_state: "wf_state (e, es)"
    by(auto elim!: bisim_red_red0.cases)
  from τRed0r_inline_call_not_final[of P t h1 e es]
  obtain e' es' where red1: "τRed0r P t h1 (e, es) (e', es')"
    and "final e'  es' = []" 
    and feq: "collapse (e, es) = collapse (e', es')" by blast
  have nfin: "¬ final e'"
  proof
    assume fin: "final e'"
    hence "es' = []" by(rule final e'  es' = [])
    with fold fin feq have "final e1" by simp
    with red show False by auto
  qed
  from red1 wf_state have wf_state': "wf_state (e', es')" by(rule τRed0r_preserves_wf_state[OF wf])
  hence fv: "fvs (e' # es') = {}" and icl: "eset es'. is_call e" by auto
  from red_fold_exs'[OF red[unfolded fold x1 feq] wf_state' nfin]
  obtain E' where e1': "e1' = collapse (E', es')" 
    and red': "P,t  e',(h1, Map.empty) -ε E',(h1', Map.empty)" by auto
  from fv fv_collapse[of es e] wf_state fold feq have "fv e1 = {}" by(auto)
  with red_dom_lcl[OF red] x1 have x1': "x1' = Map.empty" by simp
  from red_red0_tabisim0[OF wf red']
  have red'': "extTA2J0 P,P,t  e',(h1, Map.empty) -ε E',(h1', Map.empty)" by simp
  show "bisim_red_red0 s1' s2  (λe e'. False)^++ s1' s1 
        (s2'. red0_mthr.silent_movet P t s2 s2'  bisim_red_red0 s1' s2')"
  proof(cases "no_call P h1 e'")
    case True
    with red'' have "P,t ⊢0 e'/es', h1 -ε E'/es', h1'" unfolding no_call_def by(rule red0Red)
    moreover from red τ have [simp]: "h1' = h1" by(auto dest: τmove0_heap_unchanged)
    moreover from τ fold feq icl nfin have "τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
    ultimately have "τRed0 P t h1 (e', es') (E', es')" using τmove0 P h1 e' by auto
    with red1 have "τRed0t P t h1 (e, es) (E', es')" by(rule rtranclp_into_tranclp1)
    moreover hence "wf_state (E', es')" using wf_state by(rule τRed0t_preserves_wf_state[OF wf])
    hence "bisim_red_red0 ((e1', x1'), h1) ((E', es'), h1)" unfolding x1' e1' by(auto)
    ultimately show ?thesis using s1 s1' s2 heap by simp(blast intro:  τRed0t_into_silent_movet)
  next
    case False
    then obtain a M vs where call: "call e' = (a, M, vs)"
      and notsynth: "¬ synthesized_call P h1 (a, M, vs)" by(auto simp add: no_call_def)
    from notsynth called_methodD[OF red'' call] obtain T D Us U pns body
      where "h1' = h1"
      and ha: "typeof_addr h1 a = T"
      and sees: "P  class_type_of T sees M: UsU = (pns, body) in D"
      and length: "length vs = length pns" "length Us = length pns"
      by(auto)
    let ?e = "blocks (this # pns) (Class D # Us) (Addr a # vs) body"
    from call ha have "P,t ⊢0 e'/es',h1 -ε ?e/e' # es',h1"
      using sees length by(rule red0Call)
    moreover from τ fold feq icl nfin False have "τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
    ultimately have "τRed0 P t h1 (e', es') (?e, e' # es')" by auto
    with red1 have "τRed0t P t h1 (e, es) (?e, e' # es')" by(rule rtranclp_into_tranclp1)
    moreover {
      from P,t ⊢0 e'/es',h1 -ε ?e/e' # es',h1 have "wf_state (?e, e' # es')"
        using wf_state' by(rule red0_preserves_wf_state[OF wf])
      moreover from is_call_red_inline_callD[OF sees red' call] ha
      have "E' = inline_call ?e e'" by auto
      ultimately have "bisim_red_red0 s1' ((?e, e' # es'), h1')" unfolding s1' e1' x1'
        by(auto del: wf_state.cases wf_state.intros) }
    moreover from red' call notsynth have "h1 = h1'"
      by(auto dest: is_call_red_state_unchanged)
    ultimately show ?thesis unfolding heap x1' x1 s2 s1' h1' = h1
      by(blast intro: τRed0t_into_silent_movet)
  qed
next
  fix s1 s2 s2'
  assume "bisim_red_red0 s1 s2" and "red0_mthr.silent_move P t s2 s2'"
  moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
  moreover obtain e' es' h2' where s2': "s2' = ((e', es'), h2')" by(cases s2', auto)
  moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
  ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
    and red: "P,t ⊢0 e/es, h2 -ε e'/es', h2'" 
    and τ: "τmove0 P h2 e  final e" by(auto elim: τtrsys.silent_move.cases)
  from bisim have heap: "h1 = h2"
    and fold: "e1 = collapse (e, es)"
    and x1: "x1 = Map.empty" and wf_state: "wf_state (e, es)"
    by(auto elim!: bisim_red_red0.cases)
  from red wf_state have wf_state': "wf_state (e', es')" by(rule red0_preserves_wf_state[OF wf])
  from red show "bisim_red_red0 s1 s2'  (λ((e, es), h) ((e, es'), h). length es < length es')++ s2' s2 
        (s1'. red_mthr.silent_movet P t s1 s1'  bisim_red_red0 s1' s2')"
  proof cases
    case (red0Red xs')
    hence [simp]: "es' = es"
      and "extTA2J0 P,P,t  e, (h2, Map.empty) -ε e', (h2', xs')" by auto
    from red0_red_tabisim0[OF wf this(2)] have red': "P,t  e,(h2, Map.empty) -ε e',(h2', xs')" by auto
    moreover from wf_state have "fv e = {}" by auto
    with red_dom_lcl[OF red'] red_fv_subset[OF wf red'] have "xs' = Map.empty" by auto
    ultimately have "P,t  e,(h2, Map.empty) -ε e',(h2', Map.empty)" by simp
    hence "P,t  collapse (e, es),(h2, Map.empty) -ε collapse (e', es),(h2', Map.empty)" 
      using wf_state by(rule red_fold_exs)
    moreover from red' have "¬ final e" by auto
    with τ wf_state fold have "τmove0 P h2 e1" by(auto simp add: collapse_τmove0_inv)
    ultimately have "red_mthr.silent_movet P t s1 ((collapse (e', es), Map.empty), h2')"
      using s1 fold τ x1 heap by(auto intro: τtrsys.silent_move.intros)
    moreover from wf_state' have "bisim_red_red0 ((collapse (e', es), Map.empty), h2') s2'"
      unfolding s2' by(auto)
    ultimately show ?thesis by blast
  next
    case (red0Call a M vs U Ts T pns body D)
    hence [simp]: "es' = e # es" "h2' = h2" "e' = blocks (this # pns) (Class D # Ts) (Addr a # vs) body"
      and call: "call e = (a, M, vs)"
      and ha: "typeof_addr h2 a = U"
      and sees: "P  class_type_of U sees M: TsT = (pns, body) in D"
      and len: "length vs = length pns" "length Ts = length pns" by auto
    from is_call_red_inline_call(1)[OF sees len call, of "(h2, Map.empty)"] ha
    have "P,t  e,(h2, Map.empty) -ε inline_call e' e, (h2, Map.empty)" by simp
    hence "P,t  collapse (e, es), (h2, Map.empty) -ε collapse (inline_call e' e, es), (h2, Map.empty)"
      using wf_state by(rule red_fold_exs)
    moreover from call ha wf_state τ have "τmove0 P h2 (collapse (e, es))"
      by(subst collapse_τmove0_inv) auto
    hence "τMOVE P ((collapse (e, es), Map.empty), h2) ε ((collapse (inline_call e' e, es), Map.empty), h2)" by auto
    moreover from wf_state'
    have "bisim_red_red0 ((collapse (inline_call e' e, es), Map.empty), h2) ((e', es'), h2')"
      by(auto)
    ultimately show ?thesis unfolding s1 s2 s2' fold heap x1 by(fastforce)
  next
    case (red0Return E)
    hence [simp]: "es = E # es'" "e' = inline_call e E" "h2' = h2" by auto
    from fold wf_state'
    have "bisim_red_red0 ((e1, Map.empty), h1) ((inline_call e E, es'), h2)"
      unfolding heap by(auto)
    thus ?thesis using s1 s2' s2 x1 by auto
  qed
next
  fix s1 s2 ta1 s1'
  assume "bisim_red_red0 s1 s2" and "mred P t s1 ta1 s1'" and "¬ τMOVE P s1 ta1 s1'"
  moreover obtain e1 h1 x1 where s1: "s1 = ((e1, x1), h1)" by(cases s1, auto)
  moreover obtain e1' h1' x1' where s1': "s1' = ((e1', x1'), h1')" by(cases s1', auto)
  moreover obtain e es h2 where s2: "s2 = ((e, es), h2)" by(cases s2, auto)
  ultimately have bisim: "bisim_red_red0 ((e1, x1), h1) ((e, es), h2)"
    and red: "P,t  e1, (h1, x1) -ta1 e1', (h1', x1')" 
    and τ: "¬ τmove0 P h1 e1" by(auto dest: red_τ_taD[where extTA="extTA2J P", OF extTA2J_ε])
  from bisim have heap: "h1 = h2"
    and fold: "e1 = collapse (e, es)"
    and x1: "x1 = Map.empty"
    and wf_state: "wf_state (e, es)"
    by(auto elim!: bisim_red_red0.cases)
  from τRed0r_inline_call_not_final[of P t h1 e es]
  obtain e' es' where red1: "τRed0r P t h1 (e, es) (e', es')"
    and "final e'  es' = []" and feq: "collapse (e, es) = collapse (e', es')" by blast
  hence red1': "red0_mthr.silent_moves P t ((e, es), h2) ((e', es'), h2)"
    unfolding heap by -(rule τRed0r_into_silent_moves)
  have nfin: "¬ final e'"
  proof
    assume fin: "final e'"
    hence "es' = []" by(rule final e'  es' = [])
    with fold fin feq have "final e1" by simp
    with red show False by auto
  qed
  from red1 wf_state have wf_state': "wf_state (e', es')" by(rule τRed0r_preserves_wf_state[OF wf])
  hence fv: "fvs (e' # es') = {}" and icl: "e  set es'. is_call e" by auto
  from red_fold_exs'[OF red[unfolded fold x1 feq] wf_state' nfin]
  obtain E' where e1': "e1' = collapse (E', es')" 
    and red': "P,t  e',(h1, Map.empty) -ta1 E',(h1', Map.empty)" by auto
  from fv fv_collapse[OF icl, of e'] fold feq have "fv e1 = {}" by(auto)
  with red_dom_lcl[OF red] x1 have x1': "x1' = Map.empty" by simp
  from red_red0_tabisim0[OF wf red'] obtain ta2
    where red'': "extTA2J0 P,P,t  e',(h1, Map.empty) -ta2 E',(h1', Map.empty)"
    and tasim: "ta_bisim0 ta1 ta2" by auto
  from τ fold feq icl nfin have "¬ τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
  hence "aMvs. call e' = aMvs  synthesized_call P h1 aMvs"
    by(auto dest: τmove0_callD)
  with red'' have red''': "P,t ⊢0 e'/es', h1 -ta2 E'/es', h1'" by(rule red0Red)
  moreover from τ fold feq icl nfin have "¬ τmove0 P h1 e'" by(simp add: collapse_τmove0_inv)
  hence "¬ τMOVE0 P ((e', es'), h1) ta2 ((E', es'), h1')" using nfin by auto
  moreover from red''' wf_state' have "wf_state (E', es')" by(rule red0_preserves_wf_state[OF wf])
  hence "bisim_red_red0 s1' ((E', es'), h1')" unfolding s1' e1' x1' by(auto)
  ultimately show "s2' s2'' ta2. red0_mthr.silent_moves P t s2 s2'  mred0 P t s2' ta2 s2'' 
                       ¬ τMOVE0 P s2' ta2 s2''  bisim_red_red0 s1' s2''  ta_bisim0 ta1 ta2"
    using tasim red1' heap unfolding s1' s2 by -(rule exI conjI|assumption|auto)+
next
  fix s1 s2 ta2 s2'
  assume "bisim_red_red0 s1 s2" and "mred0 P t s2 ta2 s2'" "¬ τMOVE0 P s2 ta2 s2'"
  from red_simulates_red0[OF wf this]
  show "s1' s1'' ta1. red_mthr.silent_moves P t s1 s1'  mred P t s1' ta1 s1'' 
                       ¬ τMOVE P s1' ta1 s1''  bisim_red_red0 s1'' s2'  ta_bisim0 ta1 ta2"
    by(blast intro: rtranclp.rtrancl_refl)
qed

lemma delay_bisimulation_diverge_red_red0:
  assumes "wwf_J_prog P"
  shows "delay_bisimulation_diverge (mred P t) (mred0 P t) bisim_red_red0 ta_bisim0 (τMOVE P) (τMOVE0 P)"
proof -
  interpret delay_bisimulation_measure
    "mred P t" "mred0 P t" "bisim_red_red0" "ta_bisim0" "τMOVE P" "τMOVE0 P"
    "λe e'. False" "λ((e, es), h) ((e, es'), h). length es < length es'"
    using assms by(rule delay_bisimulation_measure_red_red0)
  show ?thesis by unfold_locales
qed

lemma bisim_red_red0_finalD:
  assumes bisim: "bisim_red_red0 (x1, m1) (x2, m2)"
  and "final_expr x1"
  shows "x2'. red0_mthr.silent_moves P t (x2, m2) (x2', m2)  bisim_red_red0 (x1, m1) (x2', m2)  final_expr0 x2'"
proof -
  from bisim
  obtain e' e es where wf_state: "wf_state (e, es)"
    and [simp]: "x1 = (e', Map.empty)" "x2 = (e, es)" "e' = collapse (e, es)" "m2 = m1"
    by cases(cases x2, auto)
  from final_expr x1 have "final (collapse (e, es))" by simp
  moreover from wf_state have "eset es. is_call e" by auto
  ultimately have "red0_mthr.silent_moves P t ((e, es), m1) ((collapse (e, es), []), m1)"
  proof(induction es arbitrary: e)
    case Nil thus ?case by simp
  next
    case (Cons e' es)
    from final (collapse (e, e' # es)) have "final (collapse (inline_call e e', es))" by simp
    moreover from eset (e' # es). is_call e have "eset es. is_call e" by simp
    ultimately have "red0_mthr.silent_moves P t ((inline_call e e', es), m1) ((collapse (inline_call e e', es), []), m1)"
      by(rule Cons.IH)
    moreover from final (collapse (e, e' # es)) eset (e' # es). is_call e
    have "final e" by(rule collapse_finalD)
    hence "P,t ⊢0 e/e'#es, m1 -ε inline_call e e'/es, m1" by(rule red0Return)
    with final e have "red0_mthr.silent_move P t ((e, e'#es), m1) ((inline_call e e', es), m1)" by auto
    ultimately show ?case by -(erule converse_rtranclp_into_rtranclp, simp)
  qed
  moreover have "bisim_red_red0 ((collapse (e, es), Map.empty), m1) ((collapse (e, es), []), m1)"
    using final (collapse (e, es)) by(auto intro!: bisim_red_red0I)
  ultimately show ?thesis using final (collapse (e, es)) by auto
qed

lemma red0_simulates_red_not_final:
  assumes wwf: "wwf_J_prog P"
  assumes bisim: "bisim_red_red0 ((e, xs), h) ((e0, es0), h0)"
  and red: "P,t  e, (h, xs) -ta e', (h', xs')"
  and fin: "¬ final e0"
  and : "¬ τmove0 P h e"
  shows "e0' ta0. P,t ⊢0 e0/es0, h -ta0 e0'/es0, h'  bisim_red_red0 ((e', xs'), h') ((e0', es0), h')  ta_bisim0 ta ta0"
proof -
  from bisim have [simp]: "xs = Map.empty" "h0 = h" and e: "e = collapse (e0, es0)"
    and wfs: "wf_state (e0, es0)" by(auto elim!: bisim_red_red0.cases)
  with red have "P,t  collapse (e0, es0), (h, Map.empty) -ta e', (h', xs')" by simp
  from wfs red_fold_exs'[OF this] fin obtain e0' where e': "e' = collapse (e0', es0)"
    and red': "P,t  e0,(h, Map.empty) -ta e0',(h', Map.empty)" by(auto)
  from wfs fv_collapse[of es0, of e0] e have "fv e = {}" by(auto)
  with red_dom_lcl[OF red] have [simp]: "xs' = Map.empty" by simp
  from red_red0_tabisim0[OF wwf red'] obtain ta0
    where red'': "extTA2J0 P,P,t  e0,(h, Map.empty) -ta0 e0',(h', Map.empty)"
    and tasim: "ta_bisim0 ta ta0" by auto
  from  e wfs fin have "¬ τmove0 P h e0" by(auto simp add: collapse_τmove0_inv)
  hence "aMvs. call e0 = aMvs  synthesized_call P h aMvs"
    by(auto dest: τmove0_callD)
  with red'' have red''': "P,t ⊢0 e0/es0, h -ta0 e0'/es0, h'" by(rule red0Red)
  moreover from red''' wfs have "wf_state (e0', es0)" by(rule red0_preserves_wf_state[OF wwf])
  hence "bisim_red_red0 ((e', xs'), h') ((e0', es0), h')" unfolding e' by(auto)
  ultimately show ?thesis using tasim by(auto simp del: split_paired_Ex)
qed

lemma red_red0_FWbisim:
  assumes wf: "wwf_J_prog P"
  shows "FWdelay_bisimulation_diverge final_expr (mred P) final_expr0 (mred0 P)
                                      (λt. bisim_red_red0) (λexs (e0, es0). ¬ final e0) (τMOVE P) (τMOVE0 P)"
proof -
  interpret delay_bisimulation_diverge "mred P t" "mred0 P t" "bisim_red_red0" "ta_bisim0" "τMOVE P" "τMOVE0 P"
    for t by(rule delay_bisimulation_diverge_red_red0[OF wf])
  show ?thesis
  proof
    fix t and s1 :: "(('addr expr × 'addr locals) × 'heap)" and s2 :: "(('addr expr × 'addr expr list) × 'heap)"
    assume "bisim_red_red0 s1 s2" "(λ(x1, m). final_expr x1) s1"
    moreover obtain x1 m1 where [simp]: "s1 = (x1, m1)" by(cases s1)
    moreover obtain x2 m2 where [simp]: "s2 = (x2, m2)" by(cases s2)
    ultimately have "bisim_red_red0 (x1, m1) (x2, m2)" "final_expr x1" by simp_all
    from bisim_red_red0_finalD[OF this, of P t]
    show "s2'. red0_mthr.silent_moves P t s2 s2'  bisim_red_red0 s1 s2'  (λ(x2, m). final_expr0 x2) s2'" by auto
  next
    fix t and s1 :: "(('addr expr × 'addr locals) × 'heap)" and s2 :: "(('addr expr × 'addr expr list) × 'heap)"
    assume "bisim_red_red0 s1 s2" "(λ(x2, m). final_expr0 x2) s2"
    moreover obtain x1 m1 where [simp]: "s1 = (x1, m1)" by(cases s1)
    moreover obtain x2 m2 where [simp]: "s2 = (x2, m2)" by(cases s2)
    ultimately have "bisim_red_red0 (x1, m1) (x2, m2)" "final_expr0 x2" by simp_all
    moreover hence "final_expr x1" by(rule bisim_red_red0_final0D)
    ultimately show "s1'. red_mthr.silent_moves P t s1 s1'  bisim_red_red0 s1' s2  (λ(x1, m). final_expr x1) s1'" by auto
  next
    fix t' x m1 xx m2 t x1 x2 x1' ta1 x1'' m1' x2' ta2 x2'' m2'
    assume b: "bisim_red_red0 (x, m1) (xx, m2)" and bo: "bisim_red_red0 (x1, m1) (x2, m2)"
      and "red_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red1: "mred P t (x1', m1) ta1 (x1'', m1')" and "¬ τMOVE P (x1', m1) ta1 (x1'', m1')"
      and "red0_mthr.silent_moves P t (x2, m2) (x2', m2)"
      and red2: "mred0 P t (x2', m2) ta2 (x2'', m2')" and "¬ τMOVE0 P (x2', m2) ta2 (x2'', m2')"
      and bo': "bisim_red_red0 (x1'', m1') (x2'', m2')"
      and tb: "ta_bisim0 ta1 ta2"
    from b have "m1 = m2" by(auto elim: bisim_red_red0.cases)
    moreover from bo' have "m1' = m2'" by(auto elim: bisim_red_red0.cases)
    ultimately show "bisim_red_red0 (x, m1') (xx, m2')" using b
      by(auto elim: bisim_red_red0.cases)
  next
    fix t x1 m1 x2 m2 x1' ta1 x1'' m1' x2' ta2 x2'' m2' w
    assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
      and "red_mthr.silent_moves P t (x1, m1) (x1', m1)"
      and red1: "mred P t (x1', m1) ta1 (x1'', m1')" and "¬ τMOVE P (x1', m1) ta1 (x1'', m1')"
      and "red0_mthr.silent_moves P t (x2, m2) (x2', m2)" 
      and red2: "mred0 P t (x2', m2) ta2 (x2'', m2')" and "¬ τMOVE0 P (x2', m2) ta2 (x2'', m2')"
      and b': "bisim_red_red0 (x1'', m1') (x2'', m2')" and "ta_bisim0 ta1 ta2"
      and Suspend: "Suspend w  set ta1w" "Suspend w  set ta2w"
    hence "(λexs (e0, es0). is_call e0) x1'' x2''"
      by(cases x1')(cases x2', auto dest: Red_Suspend_is_call simp add: final_iff)
    thus "(λexs (e0, es0). ¬ final e0) x1'' x2''" by(auto simp add: final_iff is_call_def)
  next
    fix t x1 m1 x2 m2 ta1 x1' m1'
    assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
      and c: "(λ(e0, es0). ¬ final e0) x2"
      and red1: "mred P t (x1, m1) ta1 (x1', m1')"
      and wakeup: "Notified  set ta1w  WokenUp  set ta1w"
    from c have "¬ final (fst x2)" by(auto simp add: is_call_def)
    moreover from red1 wakeup have "¬ τmove0 P m1 (fst x1)"
      by(cases x1)(auto dest: red_τ_taD[where extTA="extTA2J P", simplified] simp add: ta_upd_simps)
    moreover from b have "m2 = m1" by(cases) auto
    ultimately obtain e0' ta0 where "P,t ⊢0 fst x2/snd x2,m2 -ta0 e0'/snd x2,m1'"
      "bisim_red_red0 ((fst x1', snd x1'), m1') ((e0', snd x2), m1')" "ta_bisim0 ta1 ta0"
      using red0_simulates_red_not_final[OF wf, of "fst x1" "snd x1" m1 "fst x2" "snd x2" m2 t ta1 "fst x1'" m1' "snd x1'"]
      using b red1 by(auto simp add: split_beta)
    thus "ta2 x2' m2'. mred0 P t (x2, m2) ta2 (x2', m2')  bisim_red_red0 (x1', m1') (x2', m2')  ta_bisim0 ta1 ta2"
      by(cases ta0)(fastforce simp add: split_beta)
  next
    fix t x1 m1 x2 m2 ta2 x2' m2'
    assume b: "bisim_red_red0 (x1, m1) (x2, m2)"
      and c: "(λ(e0, es0). ¬ final e0) x2"
      and red2: "mred0 P t (x2, m2) ta2 (x2', m2')"
      and wakeup: "Notified  set ta2w  WokenUp  set ta2w"
    from b have [simp]: "m1 = m2" by cases auto
    with red_simulates_red0[OF wf b red2] wakeup obtain s1' ta1
      where "mred P t (x1, m1) ta1 s1'" "bisim_red_red0 s1' (x2', m2')" "ta_bisim0 ta1 ta2"
      by(fastforce simp add: split_paired_Ex)
    moreover from bisim_red_red0 s1' (x2', m2') have "m2' = snd s1'" by cases auto
    ultimately
    show "ta1 x1' m1'. mred P t (x1, m1) ta1 (x1', m1')  bisim_red_red0 (x1', m1') (x2', m2')  ta_bisim0 ta1 ta2"
      by(cases ta1)(fastforce simp add: split_beta)
  next
    show "(x. final_expr x)  (x. final_expr0 x)"
      by(auto simp add: final_iff)
  qed
qed

end

sublocale J_heap_base < red_red0:
  FWdelay_bisimulation_base 
    final_expr
    "mred P"
    final_expr0 
    "mred0 P"
    convert_RA
    "λt. bisim_red_red0" 
    "λexs (e0, es0). ¬ final e0"
    "τMOVE P" "τMOVE0 P" 
  for P
by(unfold_locales)

context J_heap_base begin

lemma bisim_J_J0_start:
  assumes wf: "wwf_J_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "red_red0.mbisim (J_start_state P C M vs) (J0_start_state P C M vs)"
proof -
  from wf_start obtain Ts T pns body D
    where sees: "P  C sees M:TsT=(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 sees] 
  have wwfCM: "wwf_J_mdecl P D (M, Ts, T, pns, body)"
    and len: "length pns = length Ts" by(auto simp add: wf_mdecl_def)
  from wwfCM have fvbody: "fv body  {this}  set pns"
    and pns: "length pns = length Ts" by simp_all
  with vs len have fv: "fv (blocks pns Ts vs body)  {this}" by auto
  with len vs sees show ?thesis unfolding start_state_def
    by(auto intro!: red_red0.mbisimI)(auto intro!: bisim_red_red0.intros wset_thread_okI simp add: is_call_def split: if_split_asm)
qed

end

end