Theory Correctness1Threaded

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

section ‹Unlocking a sync block never fails›

theory Correctness1Threaded imports 
  J0J1Bisim
  "../Framework/FWInitFinLift"
begin

definition lock_oks1 :: 
  "('addr,'thread_id) locks 
   ('addr,'thread_id,(('a,'b,'addr) exp × 'c) × (('a,'b,'addr) exp × 'c) list) thread_info  bool" 
where
  "ln. lock_oks1 ls ts  t. (case (ts t) of None     (l. has_locks (ls $ l) t = 0)
                            | ((ex, exs), ln)  (l. has_locks (ls $ l) t + ln $ l = expr_lockss (map fst (ex # exs)) l))"

primrec el_loc_ok :: "'addr expr1  'addr locals1  bool"
  and els_loc_ok :: "'addr expr1 list  'addr locals1  bool"
where
  "el_loc_ok (new C) xs  True"
| "el_loc_ok (newA Te) xs  el_loc_ok e xs"
| "el_loc_ok (Cast T e) xs  el_loc_ok e xs"
| "el_loc_ok (e instanceof T) xs  el_loc_ok e xs"
| "el_loc_ok (e«bop»e') xs  el_loc_ok e xs  el_loc_ok e' xs"
| "el_loc_ok (Var V) xs  True"
| "el_loc_ok (Val v) xs  True"
| "el_loc_ok (V := e) xs  el_loc_ok e xs"
| "el_loc_ok (ai) xs  el_loc_ok a xs  el_loc_ok i xs"
| "el_loc_ok (ai := e) xs  el_loc_ok a xs  el_loc_ok i xs  el_loc_ok e xs"
| "el_loc_ok (a∙length) xs  el_loc_ok a xs"
| "el_loc_ok (eF{D}) xs  el_loc_ok e xs"
| "el_loc_ok (eF{D} := e') xs  el_loc_ok e xs  el_loc_ok e' xs"
| "el_loc_ok (e∙compareAndSwap(DF, e', e'')) xs  el_loc_ok e xs  el_loc_ok e' xs  el_loc_ok e'' xs"
| "el_loc_ok (eM(ps)) xs  el_loc_ok e xs  els_loc_ok ps xs"
| "el_loc_ok {V:T=vo; e} xs  (case vo of None  el_loc_ok e xs | v  el_loc_ok e (xs[V := v]))"
| "el_loc_ok (sync⇘V(e) e') xs  el_loc_ok e xs  el_loc_ok e' xs  unmod e' V"
| "el_loc_ok (insync⇘V(a) e) xs  xs ! V = Addr a  el_loc_ok e xs  unmod e V"
| "el_loc_ok (e;;e') xs  el_loc_ok e xs  el_loc_ok e' xs"
| "el_loc_ok (if (b) e else e') xs  el_loc_ok b xs  el_loc_ok e xs  el_loc_ok e' xs"
| "el_loc_ok (while (b) c) xs  el_loc_ok b xs  el_loc_ok c xs"
| "el_loc_ok (throw e) xs  el_loc_ok e xs"
| "el_loc_ok (try e catch(C V) e') xs  el_loc_ok e xs  el_loc_ok e' xs"

| "els_loc_ok [] xs  True"
| "els_loc_ok (e # es) xs  el_loc_ok e xs  els_loc_ok es xs"

lemma el_loc_okI: " ¬ contains_insync e; syncvars e;  e n   el_loc_ok e xs"
  and els_loc_okI: " ¬ contains_insyncs es; syncvarss es; ℬs es n   els_loc_ok es xs"
by(induct e and es arbitrary: xs n and xs n rule: el_loc_ok.induct els_loc_ok.induct)(auto intro: fv_B_unmod)

lemma el_loc_ok_compE1: " ¬ contains_insync e; fv e  set Vs   el_loc_ok (compE1 Vs e) xs"
  and els_loc_ok_compEs1: " ¬ contains_insyncs es; fvs es  set Vs   els_loc_ok (compEs1 Vs es) xs"
by(auto intro: el_loc_okI els_loc_okI syncvars_compE1 syncvarss_compEs1  ℬs simp del: compEs1_conv_map)

lemma shows el_loc_ok_not_contains_insync_local_change:
  " ¬ contains_insync e; el_loc_ok e xs   el_loc_ok e xs'"
  and els_loc_ok_not_contains_insyncs_local_change:
  " ¬ contains_insyncs es; els_loc_ok es xs   els_loc_ok es xs'"
by(induct e and es arbitrary: xs xs' and xs xs' rule: el_loc_ok.induct els_loc_ok.induct)(fastforce)+

lemma el_loc_ok_update: "  e n; V < n   el_loc_ok e (xs[V := v]) = el_loc_ok e xs"
  and els_loc_ok_update: " ℬs es n; V < n   els_loc_ok es (xs[V := v]) = els_loc_ok es xs"
apply(induct e and es arbitrary: n xs and n xs rule: el_loc_ok.induct els_loc_ok.induct) 
apply(auto simp add: list_update_swap)
done

lemma els_loc_ok_map_Val [simp]:
  "els_loc_ok (map Val vs) xs"
by(induct vs) auto

lemma els_loc_ok_map_Val_append [simp]:
  "els_loc_ok (map Val vs @ es) xs = els_loc_ok es xs"
by(induct vs) auto

lemma el_loc_ok_extRet2J [simp]:
  "el_loc_ok e xs  el_loc_ok (extRet2J e va) xs"
by(cases va) auto

definition el_loc_ok1 :: "((nat, nat, 'addr) exp × 'addr locals1) × ((nat, nat, 'addr) exp × 'addr locals1) list  bool"
  where "el_loc_ok1 = (λ((e, xs), exs). el_loc_ok e xs  sync_ok e  ((e,xs)set exs. el_loc_ok e xs  sync_ok e))"

lemma el_loc_ok1_simps:
  "el_loc_ok1 ((e, xs), exs) = (el_loc_ok e xs  sync_ok e  ((e,xs)set exs. el_loc_ok e xs  sync_ok e))"
by(simp add: el_loc_ok1_def)

lemma el_loc_ok_blocks1 [simp]:
   "el_loc_ok (blocks1 n Ts body) xs = el_loc_ok body xs"
by(induct n Ts body rule: blocks1.induct) auto

lemma sync_oks_blocks1 [simp]: "sync_ok (blocks1 n Ts e) = sync_ok e"
by(induct n Ts e rule: blocks1.induct) auto

lemma assumes fin: "final e'"
  shows el_loc_ok_inline_call: "el_loc_ok e xs  el_loc_ok (inline_call e' e) xs"
  and els_loc_ok_inline_calls: "els_loc_ok es xs  els_loc_ok (inline_calls e' es) xs"
apply(induct e and es arbitrary: xs and xs rule: el_loc_ok.induct els_loc_ok.induct)
apply(insert fin)
apply(auto simp add: unmod_inline_call)
done

lemma assumes "sync_ok e'"
  shows sync_ok_inline_call: "sync_ok e  sync_ok (inline_call e' e)"
  and sync_oks_inline_calls: "sync_oks es  sync_oks (inline_calls e' es)"
apply(induct e and es rule: sync_ok.induct sync_oks.induct)
apply(insert sync_ok e')
apply auto
done

lemma bisim_sync_ok:
  "bisim Vs e e' xs  sync_ok e"
  "bisim Vs e e' xs  sync_ok e'"

  and bisims_sync_oks:
  "bisims Vs es es' xs  sync_oks es"
  "bisims Vs es es' xs  sync_oks es'"
apply(induct rule: bisim_bisims.inducts)
apply(auto intro: not_contains_insync_sync_ok not_contains_insyncs_sync_oks simp del: compEs1_conv_map)
done  

lemma assumes "final e'"
  shows expr_locks_inline_call_final:
  "expr_locks (inline_call e' e) = expr_locks e"
  and expr_lockss_inline_calls_final:
  "expr_lockss (inline_calls e' es) = expr_lockss es"
apply(induct e and es rule: expr_locks.induct expr_lockss.induct)
apply(insert final e')
apply(auto simp add: is_vals_conv intro: ext)
done

lemma lock_oks1I:
  " t l. ts t = None  has_locks (ls $ l) t = 0;
     t e x exs ln l. ts t = (((e, x), exs), ln)  has_locks (ls $ l) t + ln $ l= expr_locks e l + expr_lockss (map fst exs) l 
   lock_oks1 ls ts"
apply(fastforce simp add: lock_oks1_def)
done

lemma lock_oks1E:
  " lock_oks1 ls ts;
     t. ts t = None  (l. has_locks (ls $ l) t = 0)  Q;
     t e x exs ln. ts t = (((e, x), exs), ln)  (l. has_locks (ls $ l) t + ln $ l = expr_locks e l + expr_lockss (map fst exs) l)  Q 
   Q"
by(fastforce simp add: lock_oks1_def)

lemma lock_oks1D1:
  " lock_oks1 ls ts; ts t = None   l. has_locks (ls $ l) t = 0"
apply(simp add: lock_oks1_def)
apply(erule_tac x="t" in allE)
apply(auto)
done

lemma lock_oks1D2:
  "ln.  lock_oks1 ls ts; ts t = (((e, x), exs), ln)  
   l. has_locks (ls $ l) t + ln $ l = expr_locks e l + expr_lockss (map fst exs) l"
apply(fastforce simp add: lock_oks1_def)
done

lemma lock_oks1_thr_updI:
  "ln.  lock_oks1 ls ts; ts t = (((e, xs), exs), ln);
     l. expr_locks e l + expr_lockss (map fst exs) l = expr_locks e' l + expr_lockss (map fst exs') l 
   lock_oks1 ls (ts(t  (((e', xs'), exs'), ln)))"
by(rule lock_oks1I)(auto split: if_split_asm dest: lock_oks1D2 lock_oks1D1)


definition mbisim_Red1'_Red1 ::
  "(('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr) state, 
    ('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr) state) bisim"
where
  "mbisim_Red1'_Red1 s1 s2 = 
  (s1 = s2  lock_oks1 (locks s1) (thr s1)  ts_ok (λt exexs h. el_loc_ok1 exexs) (thr s1) (shr s1))"

lemma sync_ok_blocks:
  " length vs = length pns; length Ts = length pns
   sync_ok (blocks pns Ts vs body) = sync_ok body"
by(induct pns Ts vs body rule: blocks.induct) auto

context J1_heap_base begin

lemma red1_True_into_red1_False:
  " True,P,t ⊢1 e, s -ta e', s'; el_loc_ok e (lcl s)  
   False,P,t ⊢1 e, s -ta e', s'  (l. ta = UnlockFaill  expr_locks e l > 0)"
  and reds1_True_into_reds1_False:
  " True,P,t ⊢1 es, s [-ta→] es', s'; els_loc_ok es (lcl s) 
   False,P,t ⊢1 es, s [-ta→] es', s'  (l. ta = UnlockFaill  expr_lockss es l > 0)"
apply(induct rule: red1_reds1.inducts)
apply(auto intro: red1_reds1.intros split: if_split_asm)
done

lemma Red1_True_into_Red1_False:
  assumes "True,P,t ⊢1 ex/exs,shr s -ta ex'/exs',m'"
  and "el_loc_ok1 (ex, exs)"
  shows "False,P,t ⊢1 ex/exs,shr s -ta ex'/exs',m'  
         (l. ta = UnlockFaill  expr_lockss (fst ex # map fst exs) l > 0)"
using assms
by(cases)(auto dest: Red1.intros red1_True_into_red1_False simp add: el_loc_ok1_def ta_upd_simps)

lemma shows red1_preserves_el_loc_ok:
  " uf,P,t ⊢1 e, s -ta e', s'; sync_ok e; el_loc_ok e (lcl s)   el_loc_ok e' (lcl s')"

  and reds1_preserves_els_loc_ok:
  " uf,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es; els_loc_ok es (lcl s)   els_loc_ok es' (lcl s')"
proof(induct rule: red1_reds1.inducts)
  case (Synchronized1Red2 e s ta e' s' V a)
  from el_loc_ok (insync⇘V(a) e) (lcl s)
  have "el_loc_ok e (lcl s)" "unmod e V" "lcl s ! V = Addr a" by auto
  from sync_ok (insync⇘V(a) e) have "sync_ok e" by simp
  hence "el_loc_ok e' (lcl s')"
    using el_loc_ok e (lcl s)
    by(rule Synchronized1Red2)
  moreover from uf,P,t ⊢1 e,s -ta e',s' unmod e V have "unmod e' V"
    by(rule red1_unmod_preserved)
  moreover from red1_preserves_unmod[OF uf,P,t ⊢1 e,s -ta e',s' unmod e V] lcl s ! V = Addr a
  have "lcl s' ! V = Addr a" by simp
  ultimately show ?case by auto
qed(auto elim: el_loc_ok_not_contains_insync_local_change els_loc_ok_not_contains_insyncs_local_change)

lemma red1_preserves_sync_ok: " uf,P,t ⊢1 e, s -ta e', s'; sync_ok e   sync_ok e'"
  and reds1_preserves_sync_oks: " uf,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es   sync_oks es'"
by(induct rule: red1_reds1.inducts)(auto elim: not_contains_insync_sync_ok)

lemma Red1_preserves_el_loc_ok1:
  assumes wf: "wf_J1_prog P"
  shows " uf,P,t ⊢1 ex/exs,m -ta ex'/exs',m'; el_loc_ok1 (ex, exs)    el_loc_ok1 (ex', exs')"
apply(erule Red1.cases)
  apply(auto simp add: el_loc_ok1_def dest: red1_preserves_el_loc_ok red1_preserves_sync_ok intro: el_loc_ok_inline_call sync_ok_inline_call)
 apply(fastforce dest!: sees_wf_mdecl[OF wf] simp add: wf_mdecl_def intro!: el_loc_okI dest: WT1_not_contains_insync intro: not_contains_insync_sync_ok)+
done

lemma assumes wf: "wf_J1_prog P"
  shows red1_el_loc_ok1_new_thread:
  " uf,P,t ⊢1 e, s -ta e', s'; NewThread t' (C, M, a) h  set tat 
   el_loc_ok1 (({0:Class (fst (method P C M))=None; the (snd (snd (snd (method P C M))))}, xs), [])"

  and reds1_el_loc_ok1_new_thread:
  " uf,P,t ⊢1 es, s [-ta→] es', s'; NewThread t' (C, M, a) h  set tat 
   el_loc_ok1 (({0:Class (fst (method P C M))=None; the (snd (snd (snd (method P C M))))}, xs), [])"
proof(induct rule: red1_reds1.inducts)
  case Red1CallExternal thus ?case
    apply(auto dest!: red_external_new_thread_sees[OF wf] simp add: el_loc_ok1_simps)
    apply(auto dest!: sees_wf_mdecl[OF wf] WT1_not_contains_insync simp add: wf_mdecl_def intro!: el_loc_okI not_contains_insync_sync_ok)
    done
qed auto

lemma Red1_el_loc_ok1_new_thread:
  assumes wf: "wf_J1_prog P"
  shows " uf,P,t ⊢1 ex/exs,m -ta ex'/exs',m'; NewThread t' exexs m'  set tat 
          el_loc_ok1 exexs"
by(erule Red1.cases)(fastforce elim: red1_el_loc_ok1_new_thread[OF wf] simp add: ta_upd_simps)+

lemma Red1_el_loc_ok: 
  assumes wf: "wf_J1_prog P"
  shows "lifting_wf final_expr1 (mred1g uf P) (λt exexs h. el_loc_ok1 exexs)"
by(unfold_locales)(auto elim: Red1_preserves_el_loc_ok1[OF wf] Red1_el_loc_ok1_new_thread[OF wf])

lemma mred1_eq_mred1':
  assumes lok: "lock_oks1 (locks s) (thr s)"
  and elo: "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr s) (shr s)"
  and tst: "thr s t = (exexs, no_wait_locks)"
  and aoe: "Red1_mthr.actions_ok s t ta"
  shows "mred1 P t (exexs, shr s) ta = mred1' P t (exexs, shr s) ta"
proof(intro ext iffI)
  fix xm'
  assume "mred1 P t (exexs, shr s) ta xm'"
  moreover obtain ex exs where exexs [simp]: "exexs = (ex, exs)" by(cases exexs)
  moreover obtain ex' exs' m' where xm' [simp]: "xm' = ((ex', exs'), m')" by(cases xm') auto
  ultimately have red: "True,P,t ⊢1 ex/exs,shr s -ta ex'/exs',m'" by simp
  from elo tst have "el_loc_ok1 (ex, exs)" by(auto dest: ts_okD)
  from Red1_True_into_Red1_False[OF red this]
  have "False,P,t ⊢1 ex/exs,shr s -ta ex'/exs',m'"
  proof
    assume "l. ta = UnlockFaill  0 < expr_lockss (fst ex # map fst exs) l"
    then obtain l where ta: "ta = UnlockFaill" 
      and el: "expr_lockss (fst ex # map fst exs) l > 0" by blast
    from aoe have "lock_actions_ok (locks s $ l) t (tal $ l)"
      by(auto simp add: lock_ok_las_def)
    with ta have "has_locks (locks s $ l) t = 0" by simp
    with lok tst have "expr_lockss (map fst (ex # exs)) l = 0"
      by(cases ex)(auto 4 6 simp add: lock_oks1_def)
    with el have False by simp
    thus ?thesis ..
  qed
  thus "mred1' P t (exexs, shr s) ta xm'" by simp
next
  fix xm'
  assume "mred1' P t (exexs, shr s) ta xm'"
  thus "mred1 P t (exexs, shr s) ta xm'"
    by(cases xm')(auto simp add: split_beta intro: Red1_False_into_Red1_True)
qed

lemma Red1_mthr_eq_Red1_mthr':
  assumes lok: "lock_oks1 (locks s) (thr s)"
  and elo: "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr s) (shr s)"
  shows "Red1_mthr.redT True P s = Red1_mthr.redT False P s"
proof(intro ext)
  fix tta s'
  show "Red1_mthr.redT True P s tta s' = Red1_mthr.redT False P s tta s'" (is "?lhs = ?rhs")
  proof
    assume "?lhs" thus ?rhs
    proof cases
      case (redT_normal t x ta x' m')
      from mred1 P t (x, shr s) ta (x', m') have "mred1' P t (x, shr s) ta (x', m')"
        unfolding mred1_eq_mred1'[OF lok elo thr s t = (x, no_wait_locks) Red1_mthr.actions_ok s t ta] .
      thus ?thesis using redT_normal(3-) unfolding tta = (t, ta) ..
    next
      case (redT_acquire t x ln n)
      from this(2-) show ?thesis unfolding redT_acquire(1) ..
    qed
  next
    assume ?rhs thus ?lhs
    proof(cases)
      case (redT_normal t x ta x' m')
      from mred1' P t (x, shr s) ta (x', m') have "mred1 P t (x, shr s) ta (x', m')"
        unfolding mred1_eq_mred1'[OF lok elo thr s t = (x, no_wait_locks) Red1_mthr.actions_ok s t ta] .
      thus ?thesis using redT_normal(3-) unfolding tta = (t, ta) ..
    next
      case (redT_acquire t x ln n)
      from this(2-) show ?thesis unfolding redT_acquire(1) ..
    qed
  qed
qed

lemma assumes wf: "wf_J1_prog P"
  shows expr_locks_new_thread1:
  " uf,P,t ⊢1 e,s -TA e',s'; NewThread t' (ex, exs) h  set (map (convert_new_thread_action (extNTA2J1 P)) TAt) 
   expr_lockss (map fst (ex # exs)) = (λad. 0)"
  and expr_lockss_new_thread1:
  " uf,P,t ⊢1 es,s [-TA→] es',s'; NewThread t' (ex, exs) h  set (map (convert_new_thread_action (extNTA2J1 P)) TAt) 
   expr_lockss (map fst (ex # exs)) = (λad. 0)"
proof(induct rule: red1_reds1.inducts)
  case (Red1CallExternal s a T M vs ta va h' e' s')
  then obtain C fs ad where subThread: "P  C * Thread" and ext: "extNTA2J1 P (C, run, ad) = (ex, exs)"
    by(fastforce dest: red_external_new_thread_sub_thread)
  from sub_Thread_sees_run[OF wf subThread] obtain D body
    where sees: "P  C sees run: []Void = body in D" by auto
  from sees_wf_mdecl[OF wf this] obtain T where "P,[Class D] ⊢1 body :: T"
    by(auto simp add: wf_mdecl_def)
  hence "¬ contains_insync body" by(rule WT1_not_contains_insync)
  hence "expr_locks body = (λad. 0)" by(auto simp add: contains_insync_conv fun_eq_iff)
  with sees ext show ?case by(auto)
qed auto

lemma assumes wf: "wf_J1_prog P"
  shows red1_update_expr_locks:
  " False,P,t ⊢1 e, s -ta e', s'; sync_ok e; el_loc_ok e (lcl s) 
   upd_expr_locks (int o expr_locks e) tal = int o expr_locks e'"

  and reds1_update_expr_lockss:
  " False,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es; els_loc_ok es (lcl s) 
   upd_expr_locks (int o expr_lockss es) tal = int o expr_lockss es'"
proof -
  have " False,P,t ⊢1 e, s -ta e', s'; sync_ok e; el_loc_ok e (lcl s)  
        upd_expr_locks (λad. 0) tal = (λad. (int o expr_locks e') ad - (int o expr_locks e) ad)"
    and " False,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es; els_loc_ok es (lcl s) 
        upd_expr_locks (λad. 0) tal = (λad. (int o expr_lockss es') ad - (int o expr_lockss es) ad)"
  proof(induct rule: red1_reds1.inducts)
    case Red1CallExternal thus ?case
      by(auto simp add: fun_eq_iff contains_insync_conv contains_insyncs_conv finfun_upd_apply elim!: red_external.cases)
  qed(fastforce simp add: fun_eq_iff contains_insync_conv contains_insyncs_conv finfun_upd_apply)+
  hence " False,P,t ⊢1 e, s -ta e', s'; sync_ok e; el_loc_ok e (lcl s) 
         upd_expr_locks (λad. 0 + (int  expr_locks e) ad) tal = int  expr_locks e'"
    and " False,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es; els_loc_ok es (lcl s) 
         upd_expr_locks (λad. 0 + (int  expr_lockss es) ad) tal = int  expr_lockss es'"
    by(fastforce simp only: upd_expr_locks_add)+
  thus " False,P,t ⊢1 e, s -ta e', s'; sync_ok e; el_loc_ok e (lcl s) 
         upd_expr_locks (int o expr_locks e) tal = int o expr_locks e'"
    and " False,P,t ⊢1 es, s [-ta→] es', s'; sync_oks es; els_loc_ok es (lcl s) 
         upd_expr_locks (int o expr_lockss es) tal = int o expr_lockss es'"
    by(auto simp add: o_def)
qed

lemma Red1'_preserves_lock_oks:
  assumes wf: "wf_J1_prog P"
  and Red: "Red1_mthr.redT False P s1 ta1 s1'"
  and loks: "lock_oks1 (locks s1) (thr s1)"
  and sync: "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr s1) (shr s1)"
  shows "lock_oks1 (locks s1') (thr s1')"
using Red
proof(cases rule: Red1_mthr.redT.cases)
  case (redT_normal t x ta x' m')
  note [simp] = ta1 = (t, ta)
  obtain ex exs where x: "x = (ex, exs)" by (cases x)
  obtain ex' exs' where x': "x' = (ex', exs')" by (cases x')
  note thrst = thr s1 t = (x, no_wait_locks)
  note aoe = Red1_mthr.actions_ok s1 t ta
  from mred1' P t (x, shr s1) ta (x', m')
  have red: "False,P,t ⊢1 ex/exs,shr s1 -ta ex'/exs',m'"
    unfolding x x' by simp_all
  note s1' = redT_upd s1 t ta x' m' s1'
  moreover from red 
  have "lock_oks1 (locks s1') (thr s1')"
  proof cases
    case (red1Red e x TA e' x')
    note [simp] = ex = (e, x) ta = extTA2J1 P TA ex' = (e', x') exs' = exs
      and red = False,P,t ⊢1 e,(shr s1, x) -TA e',(m', x')
    { fix t'
      assume None: "((redT_updTs (thr s1) (map (convert_new_thread_action (extNTA2J1 P)) TAt))(t  (((e', x'), exs), redT_updLns (locks s1) t (snd (the (thr s1 t))) TAl))) t' = None"
      { fix l
        from aoe have "lock_actions_ok (locks s1 $ l) t (tal $ l)" by(auto simp add: lock_ok_las_def)
        with None have "has_locks ((redT_updLs (locks s1) t tal) $ l) t' = has_locks (locks s1 $ l) t'"
          by(auto split: if_split_asm)
        also from loks None have "has_locks (locks s1 $ l) t' = 0" unfolding lock_oks1_def
          by(force split: if_split_asm dest!: redT_updTs_None)
        finally have "has_locks (upd_locks (locks s1 $ l) t (TAl $ l)) t' = 0" by simp }
      hence "l. has_locks (upd_locks (locks s1 $ l) t (TAl $ l)) t' = 0" .. }
    moreover {
      fix t' eX eXS LN
      assume Some: "((redT_updTs (thr s1) (map (convert_new_thread_action (extNTA2J1 P)) TAt))(t  (((e', x'), exs), redT_updLns (locks s1) t (snd (the (thr s1 t))) TAl))) t' = ((eX, eXS), LN)"
      { fix l
        from aoe have lao: "lock_actions_ok (locks s1 $ l) t (tal $ l)" by(auto simp add: lock_ok_las_def)
        have "has_locks ((redT_updLs (locks s1) t tal) $ l) t' + LN $ l = expr_lockss (map fst (eX # eXS)) l"
        proof(cases "t = t'")
          case True
          from loks thrst x
          have "has_locks (locks s1 $ l) t = expr_locks e l + expr_lockss (map fst exs) l"
            by(force simp add: lock_oks1_def)
          hence "lock_expr_locks_ok (locks s1 $ l) t 0 (int (expr_locks e l + expr_lockss (map fst exs) l))"
            by(simp add: lock_expr_locks_ok_def)
          with lao have "lock_expr_locks_ok (upd_locks (locks s1 $ l) t (tal $ l)) t (upd_threadRs 0 (locks s1 $ l) t (tal $ l))
 (upd_expr_lock_actions (int (expr_locks e l + expr_lockss (map fst exs) l)) (tal $ l))"
            by(rule upd_locks_upd_expr_lock_preserve_lock_expr_locks_ok)
          moreover from sync thrst x have "sync_ok e" "el_loc_ok e x"
            unfolding el_loc_ok1_def by(auto dest: ts_okD)
          with red1_update_expr_locks[OF wf red]
          have "upd_expr_locks (int  expr_locks e) TAl = int  expr_locks e'" by(simp)
          hence "upd_expr_lock_actions (int (expr_locks e l)) (TAl $ l) = int (expr_locks e' l)"
            by(simp add: upd_expr_locks_def fun_eq_iff)
          ultimately show ?thesis using lao Some thrst x True
            by(auto simp add: lock_expr_locks_ok_def upd_expr_locks_def)
        next
          case False
          from aoe have tok: "thread_oks (thr s1) tat" by auto
          show ?thesis
          proof(cases "thr s1 t' = None")
            case True
            with Some tok False obtain m 
              where nt: "NewThread t' (eX, eXS) m  set (map (convert_new_thread_action (extNTA2J1 P)) TAt)"
              and [simp]: "LN = no_wait_locks" by(auto dest: redT_updTs_new_thread)
            note expr_locks_new_thread1[OF wf red nt]
            moreover from loks True have "has_locks (locks s1 $ l) t' = 0"
              by(force simp add: lock_oks1_def)
            ultimately show ?thesis using lao False by simp
          next
            case False
            with Some t  t' tok 
            have "thr s1 t' = ((eX, eXS), LN)" by(fastforce dest: redT_updTs_Some[OF _ tok])
            with loks tok lao t  t' show ?thesis by(cases eX)(auto simp add: lock_oks1_def)
          qed
        qed }
      hence "l. has_locks ((redT_updLs (locks s1) t tal) $ l) t' + LN $ l = expr_lockss (map fst (eX # eXS)) l" .. }
    ultimately show ?thesis using s1' unfolding lock_oks1_def x' by(clarsimp simp del: fun_upd_apply)
  next
    case (red1Call e a M vs U Ts T body D x)
    from wf P  class_type_of U sees M: TsT = body in D
    obtain T' where "P,Class D # Ts ⊢1 body :: T'"
      by(auto simp add: wf_mdecl_def dest!: sees_wf_mdecl)
    hence "expr_locks (blocks1 0 (Class D#Ts) body) = (λl. 0)"
      by(auto simp add: expr_locks_blocks1 contains_insync_conv fun_eq_iff dest!: WT1_not_contains_insync)
    thus ?thesis using red1Call thrst loks s1'
      unfolding lock_oks1_def x' x
      by auto force+
  next
    case (red1Return e' x' e x)
    thus ?thesis using thrst loks s1'
      unfolding lock_oks1_def x' x
      apply(auto simp add: redT_updWs_def elim!: rtrancl3p_cases)
       apply(erule_tac x=t in allE)
       apply(erule conjE)
       apply(erule disjE)
        apply(force simp add: expr_locks_inline_call_final ac_simps)
       apply(fastforce simp add: expr_locks_inline_call_final)
      apply hypsubst_thin
      apply(erule_tac x=ta in allE)
      apply fastforce
      done
  qed
  moreover from sync mred1' P t (x, shr s1) ta (x', m') thrst aoe s1'
  have "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr s1') (shr s1')"
    by(auto intro: lifting_wf.redT_updTs_preserves[OF Red1_el_loc_ok[OF wf]])
  ultimately show ?thesis by simp
next
  case (redT_acquire t x n ln)
  thus ?thesis using loks unfolding lock_oks1_def
    apply auto
     apply force
    apply(case_tac "ln $ l::nat")
     apply simp
     apply(erule allE)
     apply(erule conjE)
     apply(erule allE)+
     apply(erule (1) impE)
     apply(erule_tac x=l in allE)
     apply fastforce
    apply(erule may_acquire_allE)
    apply(erule allE)
    apply(erule_tac x=l in allE)
    apply(erule impE)
     apply simp
    apply(simp only: has_locks_acquire_locks_conv)
    apply(erule conjE)
    apply(erule allE)+
    apply(erule (1) impE)
    apply(erule_tac x=l in allE)
    apply simp
    done
qed

lemma Red1'_Red1_bisimulation:
  assumes wf: "wf_J1_prog P"
  shows "bisimulation (Red1_mthr.redT False P) (Red1_mthr.redT True P) mbisim_Red1'_Red1 (=)"
proof
  fix s1 s2 tl1 s1'
  assume "mbisim_Red1'_Red1 s1 s2" and "Red1_mthr.redT False P s1 tl1 s1'"
  thus "s2' tl2. Red1_mthr.redT True P s2 tl2 s2'  mbisim_Red1'_Red1 s1' s2'  tl1 = tl2"
    by(cases tl1)(auto simp add: mbisim_Red1'_Red1_def Red1_mthr_eq_Red1_mthr' simp del: split_paired_Ex elim: Red1'_preserves_lock_oks[OF wf] lifting_wf.redT_preserves[OF Red1_el_loc_ok, OF wf])
next
  fix s1 s2 tl2 s2'
  assume "mbisim_Red1'_Red1 s1 s2" "Red1_mthr.redT True P s2 tl2 s2'"
  thus "s1' tl1. Red1_mthr.redT False P s1 tl1 s1'  mbisim_Red1'_Red1 s1' s2'  tl1 = tl2"
    by(cases tl2)(auto simp add: mbisim_Red1'_Red1_def Red1_mthr_eq_Red1_mthr' simp del: split_paired_Ex elim: Red1'_preserves_lock_oks[OF wf] lifting_wf.redT_preserves[OF Red1_el_loc_ok, OF wf])
qed

lemma Red1'_Red1_bisimulation_final:
  "wf_J1_prog P 
   bisimulation_final (Red1_mthr.redT False P) (Red1_mthr.redT True P) 
       mbisim_Red1'_Red1 (=) Red1_mthr.mfinal Red1_mthr.mfinal"
apply(intro_locales)
 apply(erule Red1'_Red1_bisimulation)
apply(unfold_locales)
apply(auto simp add: mbisim_Red1'_Red1_def)
done

lemma bisim_J1_J1_start:
  assumes wf: "wf_J1_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "mbisim_Red1'_Red1 (J1_start_state P C M vs) (J1_start_state P C M vs)"
proof -
  from wf_start obtain Ts T body D 
    where sees: "P  C sees M:TsT=body in D"
    and conf: "P,start_heap  vs [:≤] Ts"
    by cases
  let ?e = "blocks1 0 (Class C#Ts) body"
  let ?xs = "Null # vs @ replicate (max_vars body) undefined_value"

  from sees_wf_mdecl[OF wf sees] obtain T'
    where B: " body (Suc (length Ts))"
    and wt: "P,Class D # Ts ⊢1 body :: T'"
    and da: "𝒟 body {..length Ts}"
    and sv: "syncvars body"
    by(auto simp add: wf_mdecl_def)

  from wt have "expr_locks ?e = (λ_. 0)" by(auto intro: WT1_expr_locks)
  thus ?thesis using da sees sv B
    unfolding start_state_def
    by(fastforce simp add: mbisim_Red1'_Red1_def lock_oks1_def el_loc_ok1_def contains_insync_conv intro!: ts_okI expr_locks_sync_ok split: if_split_asm intro: el_loc_okI)
qed

lemma Red1'_Red1_bisim_into_weak:
  assumes wf: "wf_J1_prog P"
  shows "bisimulation_into_delay (Red1_mthr.redT False P) (Red1_mthr.redT True P) mbisim_Red1'_Red1 (=) (Red1_mthr.mτmove P) (Red1_mthr.mτmove P)"
proof -
  interpret b: bisimulation "Red1_mthr.redT False P" "Red1_mthr.redT True P" "mbisim_Red1'_Red1" "(=)"
    by(rule Red1'_Red1_bisimulation[OF wf])
  show ?thesis by(unfold_locales)(simp add: mbisim_Red1'_Red1_def)
qed

end

sublocale J1_heap_base < Red1_mthr:
  if_τmultithreaded_wf
    final_expr1
    "mred1g uf P"
    convert_RA
    "τMOVE1 P"
  for uf P
by(unfold_locales)

context J1_heap_base begin

abbreviation if_lock_oks1 ::
  "('addr,'thread_id) locks 
   ('addr,'thread_id,(status × (('a,'b,'addr) exp × 'c) × (('a,'b,'addr) exp × 'c) list)) thread_info
   bool" 
where
  "if_lock_oks1 ls ts  lock_oks1 ls (init_fin_descend_thr ts)"

definition if_mbisim_Red1'_Red1 ::
  "(('addr,'thread_id,status × (('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list),'heap,'addr) state, 
    ('addr,'thread_id,status × (('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list),'heap,'addr) state) bisim"
where
  "if_mbisim_Red1'_Red1 s1 s2 
  s1 = s2  if_lock_oks1 (locks s1) (thr s1)  ts_ok (init_fin_lift (λt exexs h. el_loc_ok1 exexs)) (thr s1) (shr s1)"

lemma if_mbisim_Red1'_Red1_imp_mbisim_Red1'_Red1:
  "if_mbisim_Red1'_Red1 s1 s2  mbisim_Red1'_Red1 (init_fin_descend_state s1) (init_fin_descend_state s2)"
by(auto simp add: mbisim_Red1'_Red1_def if_mbisim_Red1'_Red1_def ts_ok_init_fin_descend_state)

lemma if_Red1_mthr_imp_if_Red1_mthr':
  assumes lok: "if_lock_oks1 (locks s) (thr s)"
  and elo: "ts_ok (init_fin_lift (λt exexs h. el_loc_ok1 exexs)) (thr s) (shr s)"
  and Red: "Red1_mthr.if.redT uf P s tta s'"
  shows "Red1_mthr.if.redT (¬ uf) P s tta s'"
using Red
proof(cases)
  case (redT_acquire t x ln n)
  from this(2-) show ?thesis unfolding redT_acquire(1) ..
next
  case (redT_normal t x ta x' m')
  note aok = Red1_mthr.if.actions_ok s t ta
    and tst = thr s t = (x, no_wait_locks)
  from Red1_mthr.init_fin uf P t (x, shr s) ta (x', m')
  have "Red1_mthr.init_fin (¬ uf) P t (x, shr s) ta (x', m')"
  proof(cases)
    case InitialThreadAction show ?thesis unfolding InitialThreadAction ..
  next
    case (ThreadFinishAction exexs)
    from final_expr1 exexs show ?thesis unfolding ThreadFinishAction ..
  next
    case (NormalAction exexs ta' exexs')
    let ?s = "init_fin_descend_state s"

    from lok have "lock_oks1 (locks ?s) (thr ?s)" by(simp)
    moreover from elo have elo: "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr ?s) (shr ?s)"
      by(simp add: ts_ok_init_fin_descend_state)
    moreover from tst x = (Running, exexs)
    have "thr ?s t = (exexs, no_wait_locks)" by simp
    moreover from aok have "Red1_mthr.actions_ok ?s t ta'"
      using ta = convert_TA_initial (convert_obs_initial ta') by auto
    ultimately have "mred1 P t (exexs, shr ?s) ta' = mred1' P t (exexs, shr ?s) ta'"
      by(rule mred1_eq_mred1')
    with mred1g uf P t (exexs, shr s) ta' (exexs', m')
    have "mred1g (¬ uf) P t (exexs, shr s) ta' (exexs', m')"
      by(cases uf) simp_all
    thus ?thesis unfolding NormalAction(1-3) by(rule Red1_mthr.init_fin.NormalAction)
  qed
  thus ?thesis using tst aok redT_upd s t ta x' m' s' unfolding tta = (t, ta) ..
qed

lemma if_Red1_mthr_eq_if_Red1_mthr':
  assumes lok: "if_lock_oks1 (locks s) (thr s)"
  and elo: "ts_ok (init_fin_lift (λt exexs h. el_loc_ok1 exexs)) (thr s) (shr s)"
  shows "Red1_mthr.if.redT True P s = Red1_mthr.if.redT False P s"
using if_Red1_mthr_imp_if_Red1_mthr'[OF assms, of True P, simplified]
  if_Red1_mthr_imp_if_Red1_mthr'[OF assms, of False P, simplified]
by(blast del: equalityI)

lemma if_Red1_el_loc_ok: 
  assumes wf: "wf_J1_prog P"
  shows "lifting_wf Red1_mthr.init_fin_final (Red1_mthr.init_fin uf P) (init_fin_lift (λt exexs h. el_loc_ok1 exexs))"
by(rule lifting_wf.lifting_wf_init_fin_lift)(rule Red1_el_loc_ok[OF wf])

lemma if_Red1'_preserves_if_lock_oks:
  assumes wf: "wf_J1_prog P"
  and Red: "Red1_mthr.if.redT False P s1 ta1 s1'"
  and loks: "if_lock_oks1 (locks s1) (thr s1)"
  and sync: "ts_ok (init_fin_lift (λt exexs h. el_loc_ok1 exexs)) (thr s1) (shr s1)"
  shows "if_lock_oks1 (locks s1') (thr s1')"
proof -
  let ?s1 = "init_fin_descend_state s1"
  let ?s1' = "init_fin_descend_state s1'"
  from loks have loks': "lock_oks1 (locks ?s1) (thr ?s1)" by simp
  from sync have sync': "ts_ok (λt exexs h. el_loc_ok1 exexs) (thr ?s1) (shr ?s1)"
    by(simp add: ts_ok_init_fin_descend_state)
  from Red show ?thesis
  proof(cases)
    case (redT_acquire t x n ln)
    hence "Red1_mthr.redT False P ?s1 (t, K$ [], [], [], [], [], convert_RA ln) ?s1'"
      by(cases x)(auto intro!: Red1_mthr.redT.redT_acquire simp add: init_fin_descend_thr_def)
    with wf have "lock_oks1 (locks ?s1') (thr ?s1')" using loks' sync' by(rule Red1'_preserves_lock_oks)
    thus ?thesis by simp
  next
    case (redT_normal t sx ta sx' m')
    note tst = thr s1 t = (sx, no_wait_locks)
    from Red1_mthr.init_fin False P t (sx, shr s1) ta (sx', m')
    show ?thesis
    proof(cases)
      case (InitialThreadAction x) thus ?thesis using redT_normal loks
        by(cases x)(auto 4 3 simp add: init_fin_descend_thr_def redT_updLns_def expand_finfun_eq fun_eq_iff intro: lock_oks1_thr_updI)
    next
      case (ThreadFinishAction x) thus ?thesis using redT_normal loks
        by(cases x)(auto 4 3 simp add: init_fin_descend_thr_def redT_updLns_def expand_finfun_eq fun_eq_iff intro: lock_oks1_thr_updI)
    next
      case (NormalAction x ta' x')
      note ta = ta = convert_TA_initial (convert_obs_initial ta')
      from mred1' P t (x, shr s1) ta' (x', m')
      have "mred1' P t (x, shr ?s1) ta' (x', m')" by simp
      moreover have tst': "thr ?s1 t = (x, no_wait_locks)" 
        using tst sx = (Running, x) by simp
      moreover have "Red1_mthr.actions_ok ?s1 t ta'"
        using ta Red1_mthr.if.actions_ok s1 t ta by simp
      moreover from redT_upd s1 t ta sx' m' s1' tst tst' ta sx' = (Running, x')
      have "redT_upd ?s1 t ta' x' m' ?s1'" by auto
      ultimately have "Red1_mthr.redT False P ?s1 (t, ta') ?s1'" ..
      with wf have "lock_oks1 (locks ?s1') (thr ?s1')" using loks' sync' by(rule Red1'_preserves_lock_oks)
      thus ?thesis by simp
    qed
  qed
qed

lemma Red1'_Red1_if_bisimulation:
  assumes wf: "wf_J1_prog P"
  shows "bisimulation (Red1_mthr.if.redT False P) (Red1_mthr.if.redT True P) if_mbisim_Red1'_Red1 (=)"
proof
  fix s1 s2 tl1 s1'
  assume "if_mbisim_Red1'_Red1 s1 s2" and "Red1_mthr.if.redT False P s1 tl1 s1'"
  thus "s2' tl2. Red1_mthr.if.redT True P s2 tl2 s2'  if_mbisim_Red1'_Red1 s1' s2'  tl1 = tl2"
    by(cases tl1)(auto simp add: if_mbisim_Red1'_Red1_def if_Red1_mthr_eq_if_Red1_mthr' simp del: split_paired_Ex elim: if_Red1'_preserves_if_lock_oks[OF wf] lifting_wf.redT_preserves[OF if_Red1_el_loc_ok, OF wf])
next
  fix s1 s2 tl2 s2'
  assume "if_mbisim_Red1'_Red1 s1 s2" "Red1_mthr.if.redT True P s2 tl2 s2'"
  thus "s1' tl1. Red1_mthr.if.redT False P s1 tl1 s1'  if_mbisim_Red1'_Red1 s1' s2'  tl1 = tl2"
    by(cases tl2)(auto simp add: if_mbisim_Red1'_Red1_def if_Red1_mthr_eq_if_Red1_mthr' simp del: split_paired_Ex elim: if_Red1'_preserves_if_lock_oks[OF wf] lifting_wf.redT_preserves[OF if_Red1_el_loc_ok, OF wf])
qed

lemma if_bisim_J1_J1_start:
  assumes wf: "wf_J1_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "if_mbisim_Red1'_Red1 (init_fin_lift_state status (J1_start_state P C M vs)) (init_fin_lift_state status (J1_start_state P C M vs))"
proof -
  from assms have "mbisim_Red1'_Red1 (J1_start_state P C M vs) (J1_start_state P C M vs)" by(rule bisim_J1_J1_start)
  thus ?thesis
    by(simp add: if_mbisim_Red1'_Red1_def mbisim_Red1'_Red1_def)(simp add: init_fin_lift_state_conv_simps init_fin_descend_thr_def thr_init_fin_list_state' o_def map_option.compositionality map_option.identity split_beta)
qed

lemma if_Red1'_Red1_bisim_into_weak:
  assumes wf: "wf_J1_prog P"
  shows "bisimulation_into_delay (Red1_mthr.if.redT False P) (Red1_mthr.if.redT True P) if_mbisim_Red1'_Red1 (=) (Red1_mthr.if.mτmove P) (Red1_mthr.if.mτmove P)"
proof -
  interpret b: bisimulation "Red1_mthr.if.redT False P" "Red1_mthr.if.redT True P" "if_mbisim_Red1'_Red1" "(=)"
    by(rule Red1'_Red1_if_bisimulation[OF wf])
  show ?thesis by(unfold_locales)(simp add: if_mbisim_Red1'_Red1_def)
qed

lemma if_Red1'_Red1_bisimulation_final:
  "wf_J1_prog P 
   bisimulation_final (Red1_mthr.if.redT False P) (Red1_mthr.if.redT True P) 
       if_mbisim_Red1'_Red1 (=) Red1_mthr.if.mfinal Red1_mthr.if.mfinal"
apply(intro_locales)
 apply(erule Red1'_Red1_if_bisimulation)
apply(unfold_locales)
apply(auto simp add: if_mbisim_Red1'_Red1_def)
done

end

end