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

section ‹Unlocking a sync block never fails›

J0J1Bisim
"../Framework/FWInitFinLift"
begin

definition lock_oks1 ::
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))"

where
"el_loc_ok (new C) xs ⟷ True"
| "el_loc_ok (newA T⌊e⌉) 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 (a⌊i⌉) xs ⟷ el_loc_ok a xs ∧ el_loc_ok i xs"
| "el_loc_ok (a⌊i⌉ := 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 (e∙F{D}) xs ⟷ el_loc_ok e xs"
| "el_loc_ok (e∙F{D} := e') xs ⟷ el_loc_ok e xs ∧ el_loc_ok e' xs"
| "el_loc_ok (e∙compareAndSwap(D∙F, e', e'')) xs ⟷ el_loc_ok e xs ∧ el_loc_ok e' xs ∧ el_loc_ok e'' xs"
| "el_loc_ok (e∙M(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)
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

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))"

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)
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"
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"

lemma lock_oks1D1:
"⟦ lock_oks1 ls ts; ts t = None ⟧ ⟹ ∀l. has_locks (ls \$ l) t = 0"
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"
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 ::
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 = ⦃UnlockFail→l⦄ ∧ 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 = ⦃UnlockFail→l⦄ ∧ 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 = ⦃UnlockFail→l⦄ ∧ 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"
"⟦ uf,P,t ⊢1 ⟨e, s⟩ -ta→ ⟨e', s'⟩; NewThread t' (C, M, a) h ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ el_loc_ok1 (({0:Class (fst (method P C M))=None; the (snd (snd (snd (method P C M))))}, xs), [])"

"⟦ uf,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; NewThread t' (C, M, a) h ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ 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!: 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

assumes wf: "wf_J1_prog P"
shows "⟦ uf,P,t ⊢1 ⟨ex/exs,m⟩ -ta→ ⟨ex'/exs',m'⟩; NewThread t' exexs m' ∈ set ⦃ta⦄⇘t⇙ ⟧
⟹ el_loc_ok1 exexs"

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 = ⦃UnlockFail→l⦄ ∧ 0 < expr_lockss (fst ex # map fst exs) l"
then obtain l where ta: "ta = ⦃UnlockFail→l⦄"
and el: "expr_lockss (fst ex # map fst exs) l > 0" by blast
from aoe have "lock_actions_ok (locks s \$ l) t (⦃ta⦄⇘l⇙ \$ l)"
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"
"⟦ uf,P,t ⊢1 ⟨e,s⟩ -TA→ ⟨e',s'⟩; NewThread t' (ex, exs) h ∈ set (map (convert_new_thread_action (extNTA2J1 P)) ⦃TA⦄⇘t⇙) ⟧
⟹ expr_lockss (map fst (ex # exs)) = (λad. 0)"
"⟦ uf,P,t ⊢1 ⟨es,s⟩ [-TA→] ⟨es',s'⟩; NewThread t' (ex, exs) h ∈ set (map (convert_new_thread_action (extNTA2J1 P)) ⦃TA⦄⇘t⇙) ⟧
⟹ 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')
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"
hence "¬ contains_insync body" by(rule WT1_not_contains_insync)
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) ⦃ta⦄⇘l⇙ = 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) ⦃ta⦄⇘l⇙ = 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) ⟧
and "⟦ False,P,t ⊢1 ⟨es, s⟩ [-ta→] ⟨es', s'⟩; sync_oks es; els_loc_ok es (lcl s) ⟧
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) ⦃ta⦄⇘l⇙ = 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) ⦃ta⦄⇘l⇙ = int ∘ expr_lockss es'"
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) ⦃ta⦄⇘l⇙ = 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) ⦃ta⦄⇘l⇙ = int o expr_lockss es'"
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)) ⦃TA⦄⇘t⇙))(t ↦ (((e', x'), exs), redT_updLns (locks s1) t (snd (the (thr s1 t))) ⦃TA⦄⇘l⇙))) t' = None"
{ fix l
from aoe have "lock_actions_ok (locks s1 \$ l) t (⦃ta⦄⇘l⇙ \$ l)" by(auto simp add: lock_ok_las_def)
with None have "has_locks ((redT_updLs (locks s1) t ⦃ta⦄⇘l⇙) \$ 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 (⦃TA⦄⇘l⇙ \$ l)) t' = 0" by simp }
hence "∀l. has_locks (upd_locks (locks s1 \$ l) t (⦃TA⦄⇘l⇙ \$ l)) t' = 0" .. }
moreover {
fix t' eX eXS LN
assume Some: "((redT_updTs (thr s1) (map (convert_new_thread_action (extNTA2J1 P)) ⦃TA⦄⇘t⇙))(t ↦ (((e', x'), exs), redT_updLns (locks s1) t (snd (the (thr s1 t))) ⦃TA⦄⇘l⇙))) t' = ⌊((eX, eXS), LN)⌋"
{ fix l
from aoe have lao: "lock_actions_ok (locks s1 \$ l) t (⦃ta⦄⇘l⇙ \$ l)" by(auto simp add: lock_ok_las_def)
have "has_locks ((redT_updLs (locks s1) t ⦃ta⦄⇘l⇙) \$ 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"
hence "lock_expr_locks_ok (locks s1 \$ l) t 0 (int (expr_locks e l + expr_lockss (map fst exs) l))"
with lao have "lock_expr_locks_ok (upd_locks (locks s1 \$ l) t (⦃ta⦄⇘l⇙ \$ l)) t (upd_threadRs 0 (locks s1 \$ l) t (⦃ta⦄⇘l⇙ \$ l))
(upd_expr_lock_actions (int (expr_locks e l + expr_lockss (map fst exs) l)) (⦃ta⦄⇘l⇙ \$ 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) ⦃TA⦄⇘l⇙ = int ∘ expr_locks e'" by(simp)
hence "upd_expr_lock_actions (int (expr_locks e l)) (⦃TA⦄⇘l⇙ \$ l) = int (expr_locks e' l)"
ultimately show ?thesis using lao Some thrst x True
next
case False
from aoe have tok: "thread_oks (thr s1) ⦃ta⦄⇘t⇙" 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)) ⦃TA⦄⇘t⇙)"
and [simp]: "LN = no_wait_locks" by(auto dest: redT_updTs_new_thread)
moreover from loks True have "has_locks (locks s1 \$ l) t' = 0"
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 ⦃ta⦄⇘l⇙) \$ 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: Ts→T = ⌊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 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)
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:Ts→T=⌊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"

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])
qed

end

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

context J1_heap_base begin

abbreviation if_lock_oks1 ::
⇒ bool"
where
"if_lock_oks1 ls ts ≡ lock_oks1 ls (init_fin_descend_thr ts)"

definition if_mbisim_Red1'_Red1 ::
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)
next
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)"
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)"
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])
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)