```(*  Title:      JinjaThreads/Framework/FWBisimDeadlock.thy
Author:     Andreas Lochbihler
*)

section ‹Preservation of deadlock across bisimulations›

imports
FWBisimulation
begin

context FWdelay_bisimulation_obs begin

lemma actions_ok1_ex_actions_ok2:
assumes "r1.actions_ok s1 t ta1"
and "ta1 ∼m ta2"
obtains s2 where "r2.actions_ok s2 t ta2"
proof -
let ?s2 = "(locks s1, (λt. map_option (λ(x1, ln). (SOME x2. if final1 x1 then final2 x2 else ¬ final2 x2, ln)) (thr s1 t), undefined), wset s1, interrupts s1)"
from ‹ta1 ∼m ta2› have "⦃ta1⦄⇘c⇙ = ⦃ta2⦄⇘c⇙" by(simp add: ta_bisim_def)
with ‹r1.actions_ok s1 t ta1› have cao1: "r1.cond_action_oks s1 t ⦃ta2⦄⇘c⇙" by auto
have "r2.cond_action_oks ?s2 t ⦃ta2⦄⇘c⇙" unfolding r2.cond_action_oks_conv_set
proof
fix ct
assume "ct ∈ set ⦃ta2⦄⇘c⇙"
with cao1 have "r1.cond_action_ok s1 t ct"
unfolding r1.cond_action_oks_conv_set by auto
thus "r2.cond_action_ok ?s2 t ct" using ex_final1_conv_ex_final2
by(cases ct)(fastforce intro: someI_ex[where P=final2])+
qed
hence "r2.actions_ok ?s2 t ta2"
using assms by(auto simp add: ta_bisim_def split del: if_split elim: rev_iffD1[OF _ thread_oks_bisim_inv])
thus thesis by(rule that)
qed

lemma actions_ok2_ex_actions_ok1:
assumes "r2.actions_ok s2 t ta2"
and "ta1 ∼m ta2"
obtains s1 where "r1.actions_ok s1 t ta1"
using FWdelay_bisimulation_obs.actions_ok1_ex_actions_ok2[OF FWdelay_bisimulation_obs_flip] assms
unfolding flip_simps .

lemma ex_actions_ok1_conv_ex_actions_ok2:
"ta1 ∼m ta2 ⟹ (∃s1. r1.actions_ok s1 t ta1) ⟷ (∃s2. r2.actions_ok s2 t ta2)"
by(metis actions_ok1_ex_actions_ok2 actions_ok2_ex_actions_ok1)

end

context FWdelay_bisimulation_diverge begin

lemma no_τMove1_τs_to_no_τMove2:
fixes no_τmoves1 no_τmoves2
defines "no_τmoves1 ≡ λs1 t. wset s1 t = None ∧ (∃x. thr s1 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r1.silent_move t (x, shr s1) (x', m')))"
defines "no_τmoves2 ≡ λs2 t. wset s2 t = None ∧ (∃x. thr s2 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r2.silent_move t (x, shr s2) (x', m')))"
assumes mbisim: "s1 ≈m (ls2, (ts2, m2), ws2, is2)"

shows "∃ts2'. r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2) ∧
(∀t. no_τmoves1 s1 t ⟶ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t) ∧ s1 ≈m (ls2, (ts2', m2), ws2, is2)"
proof -
from mbisim have "finite (dom (thr s1))" by(simp add: mbisim_def)
hence "finite {t. no_τmoves1 s1 t}" unfolding no_τmoves1_def
by-(rule finite_subset, auto)
thus ?thesis using ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›
proof(induct A≡"{t. no_τmoves1 s1 t}" arbitrary: s1 ts2 rule: finite_induct)
case empty
from ‹{} = {t. no_τmoves1 s1 t}›[symmetric] have "no_τmoves1 s1 = (λt. False)"
by(auto intro: ext)
thus ?case using ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)› by auto
next
case (insert t A)
note mbisim = ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›
from ‹insert t A = {t. no_τmoves1 s1 t}›
have "no_τmoves1 s1 t" by auto
then obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and ws1t: "wset s1 t = None"
and τ1: "⋀x1m1'. ¬ r1.silent_move t (x1, shr s1) x1m1'"

from ts1t mbisim obtain x2 where ts2t: "ts2 t = ⌊(x2, no_wait_locks)⌋"
and "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD1)
from mbisim ws1t have "ws2 t = None" by(simp add: mbisim_def)

let ?s1 = "(locks s1, ((thr s1)(t := None), shr s1), wset s1, interrupts s1)"
let ?s2 = "(ls2, (ts2(t := None), m2), ws2, is2)"
from ‹insert t A = {t. no_τmoves1 s1 t}› ‹t ∉ A›
have A: "A = {t. no_τmoves1 ?s1 t}" by(auto simp add: no_τmoves1_def)
have "?s1 ≈m ?s2"
proof(rule mbisimI)
from mbisim
show "finite (dom (thr ?s1))" "locks ?s1 = locks ?s2" "wset ?s1 = wset ?s2" "interrupts ?s1 = interrupts ?s2"
next
next
fix t'
assume "thr ?s1 t' = None"
with mbisim_thrNone_eq[OF mbisim, of t']
show "thr ?s2 t' = None" by auto
next
fix t' x1 ln
assume "thr ?s1 t' = ⌊(x1, ln)⌋"
hence "thr s1 t' = ⌊(x1, ln)⌋" "t' ≠ t" by(auto split: if_split_asm)
with mbisim_thrD1[OF mbisim ‹thr s1 t' = ⌊(x1, ln)⌋›] mbisim
show "∃x2. thr ?s2 t' = ⌊(x2, ln)⌋ ∧ t' ⊢ (x1, shr ?s1) ≈ (x2, shr ?s2) ∧ (wset ?s2 t' = None ∨ x1 ≈w x2)"
qed
with A have "∃ts2'. r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2) ∧ (∀t. no_τmoves1 ?s1 t ⟶ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t) ∧ ?s1 ≈m (ls2, (ts2', m2), ws2, is2)" by(rule insert)
then obtain ts2' where "r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t. no_τmoves1 ?s1 t ⟹ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t"
and "?s1 ≈m (ls2, (ts2', m2), ws2, is2)" by auto
let ?s2' = "(ls2, (ts2'(t ↦ (x2, no_wait_locks)), m2), ws2, is2)"
from ts2t have "ts2(t ↦ (x2, no_wait_locks)) = ts2" by(auto intro: ext)
with r2.τmRedT_add_thread_inv[OF ‹r2.mthr.silent_moves ?s2 (ls2, (ts2', m2), ws2, is2)›, of t "(x2, no_wait_locks)"]
have "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2'" by simp
from no_τmove1_τs_to_no_τmove2[OF ‹t ⊢ (x1, shr s1) ≈ (x2, m2)› τ1]
obtain x2' m2' where "r2.silent_moves t (x2, m2) (x2', m2')"
and "⋀x2'' m2''. ¬ r2.silent_move t (x2', m2') (x2'', m2'')"
and "t ⊢ (x1, shr s1) ≈ (x2', m2')" by auto
let ?s2'' = "(ls2, (ts2'(t ↦ (x2', no_wait_locks)), m2'), ws2, is2)"
from red2_rtrancl_τ_heapD[OF ‹r2.silent_moves t (x2, m2) (x2', m2')› ‹t ⊢ (x1, shr s1) ≈ (x2, m2)›]
have "m2' = m2" by simp
with ‹r2.silent_moves t (x2, m2) (x2', m2')› have "r2.silent_moves t (x2, shr ?s2') (x2', m2)" by simp
hence "r2.mthr.silent_moves ?s2' (redT_upd_ε ?s2' t x2' m2)"
by(rule red2_rtrancl_τ_into_RedT_τ)(auto simp add: ‹ws2 t = None› intro: ‹t ⊢ (x1, shr s1) ≈ (x2, m2)›)
also have "redT_upd_ε ?s2' t x2' m2 = ?s2''" using ‹m2' = m2›
by(auto simp add: fun_eq_iff redT_updLns_def finfun_Diag_const2 o_def)
finally (back_subst) have "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2''"
using ‹r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) ?s2'› by-(rule rtranclp_trans)
moreover {
fix t'
assume no_τ1: "no_τmoves1 s1 t'"
have "no_τmoves2 ?s2'' t'"
proof(cases "t' = t")
case True thus ?thesis
using ‹ws2 t = None› ‹⋀x2'' m2''. ¬ r2.silent_move t (x2', m2') (x2'', m2'')› by(simp add: no_τmoves2_def)
next
case False
with no_τ1 have "no_τmoves1 ?s1 t'" by(simp add: no_τmoves1_def)
hence "no_τmoves2 (ls2, (ts2', m2), ws2, is2) t'"
by(rule ‹no_τmoves1 ?s1 t' ⟹ no_τmoves2 (ls2, (ts2', m2), ws2, is2) t'›)
with False ‹m2' = m2› show ?thesis by(simp add: no_τmoves2_def)
qed }
moreover have "s1 ≈m ?s2''"
proof(rule mbisimI)
from mbisim
show "finite (dom (thr s1))" "locks s1 = locks ?s2''" "wset s1 = wset ?s2''" "interrupts s1 = interrupts ?s2''"
next
next
fix t'
assume "thr s1 t' = None"
hence "thr ?s1 t' = None" "t' ≠ t" using ts1t by auto
with mbisim_thrNone_eq[OF ‹?s1 ≈m (ls2, (ts2', m2), ws2, is2)›, of t']
show "thr ?s2'' t' = None" by simp
next
fix t' x1' ln'
assume "thr s1 t' = ⌊(x1', ln')⌋"
show "∃x2. thr ?s2'' t' = ⌊(x2, ln')⌋ ∧ t' ⊢ (x1', shr s1) ≈ (x2, shr ?s2'') ∧ (wset ?s2'' t' = None ∨ x1' ≈w x2)"
proof(cases "t = t'")
case True
with ‹thr s1 t' = ⌊(x1', ln')⌋› ts1t ‹t ⊢ (x1, shr s1) ≈ (x2', m2')› ‹m2' = m2› ‹ws2 t = None›
show ?thesis by auto
next
case False
with mbisim_thrD1[OF ‹?s1 ≈m (ls2, (ts2', m2), ws2, is2)›, of t' x1' ln'] ‹thr s1 t' = ⌊(x1', ln')⌋› ‹m2' = m2› mbisim
show ?thesis by(auto simp add: mbisim_def)
qed
qed
ultimately show ?case unfolding ‹m2' = m2› by blast
qed
qed

lemma no_τMove2_τs_to_no_τMove1:
fixes no_τmoves1 no_τmoves2
defines "no_τmoves1 ≡ λs1 t. wset s1 t = None ∧ (∃x. thr s1 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r1.silent_move t (x, shr s1) (x', m')))"
defines "no_τmoves2 ≡ λs2 t. wset s2 t = None ∧ (∃x. thr s2 t = ⌊(x, no_wait_locks)⌋ ∧ (∀x' m'. ¬ r2.silent_move t (x, shr s2) (x', m')))"
assumes "(ls1, (ts1, m1), ws1, is1) ≈m s2"

shows "∃ts1'. r1.mthr.silent_moves (ls1, (ts1, m1), ws1, is1) (ls1, (ts1', m1), ws1, is1) ∧
(∀t. no_τmoves2 s2 t ⟶ no_τmoves1 (ls1, (ts1', m1), ws1, is1) t) ∧ (ls1, (ts1', m1), ws1, is1) ≈m s2"
using assms FWdelay_bisimulation_diverge.no_τMove1_τs_to_no_τMove2[OF FWdelay_bisimulation_diverge_flip]
unfolding flip_simps by blast

and mbisim: "s1 ≈m s2"
proof -
from nfin obtain x1 ln where "thr s1 t = ⌊(x1, ln)⌋" by cases auto
with mbisim obtain x2 where "thr s2 t = ⌊(x2, ln)⌋" "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" "wset s1 t = None ∨ x1 ≈w x2"
by(auto dest: mbisim_thrD1)
proof(cases "wset s1 t = None ∧ ln = no_wait_locks")
case False
with ‹r1.not_final_thread s1 t› ‹thr s1 t = ⌊(x1, ln)⌋› ‹thr s2 t = ⌊(x2, ln)⌋› mbisim
next
case True
with ‹r1.not_final_thread s1 t› ‹thr s1 t = ⌊(x1, ln)⌋› have "¬ final1 x1" by(cases) auto
have "¬ final2 x2"
proof
assume "final2 x2"
with final2_simulation[OF ‹t ⊢ (x1, shr s1) ≈ (x2, shr s2)›]
obtain x1' m1' where "r1.silent_moves t (x1, shr s1) (x1', m1')" "t ⊢ (x1', m1') ≈ (x2, shr s2)" "final1 x1'" by auto
from ‹r1.silent_moves t (x1, shr s1) (x1', m1')› have "x1' = x1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step x1'' m1'')
from ‹r1.silent_move t (x1, shr s1) (x1'', m1'')›
have "t ⊢ (x1, shr s1) -1-ε→ (x1'', m1'')" by(auto dest: r1.silent_tl)
hence "r1.redT s1 (t, ε) (redT_upd_ε s1 t x1'' m1'')"
using ‹thr s1 t = ⌊(x1, ln)⌋› True
by -(erule r1.redT_normal, auto simp add: redT_updLns_def finfun_Diag_const2 o_def redT_updWs_def)
thus ?thesis ..
qed simp
with ‹¬ final1 x1› ‹final1 x1'› show False by simp
qed
thus ?thesis using ‹thr s2 t = ⌊(x2, ln)⌋› by(auto simp add: r2.not_final_thread_iff)
qed
qed

assumes mbisim: "s1 ≈m s2"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ t ∈ r2.deadlocked s2' ∧ s1 ≈m s2'"
proof -
from mfinal1_inv_simulation[OF mbisim]
obtain ls2 ts2 m2 ws2 is2 where red1: "r2.mthr.silent_moves s2 (ls2, (ts2, m2), ws2, is2)"
and "s1 ≈m (ls2, (ts2, m2), ws2, is2)" and "m2 = shr s2"
and fin: "⋀t. r1.final_thread s1 t ⟹ r2.final_thread (ls2, (ts2, m2), ws2, is2) t" by fastforce
from no_τMove1_τs_to_no_τMove2[OF ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›]
obtain ts2' where red2: "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t x1 x2 x2' m2'. ⟦ wset s1 t = None; thr s1 t = ⌊(x1, no_wait_locks)⌋; ts2' t = ⌊(x2, no_wait_locks)⌋;
⋀x' m'. r1.silent_move t (x1, shr s1) (x', m') ⟹ False ⟧
⟹  ¬ r2.silent_move t (x2, m2) (x2', m2')"
and mbisim: "s1 ≈m (ls2, (ts2', m2), ws2, is2)" by fastforce
from mbisim have mbisim_eqs: "ls2 = locks s1" "ws2 = wset s1" "is2 = interrupts s1"
let ?s2 = "(ls2, (ts2', m2), ws2, is2)"
from red2 have fin': "⋀t. r1.final_thread s1 t ⟹ r2.final_thread ?s2 t"
proof(coinduct)
thus ?case
case (lock x1)
hence csmw: "⋀LT. r1.can_sync t x1 (shr s1) LT ⟹
by blast
from ‹thr s1 t = ⌊(x1, no_wait_locks)⌋› mbisim obtain x2
where "ts2' t = ⌊(x2, no_wait_locks)⌋" and bisim: "t ⊢ (x1, shr s1) ≈ (x2, m2)"
by(auto dest: mbisim_thrD1)
note ‹ts2' t = ⌊(x2, no_wait_locks)⌋› moreover
{ from ‹r1.must_sync t x1 (shr s1)› obtain ta1 x1' m1'
where r1: "t ⊢ (x1, shr s1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
have "¬ τmove1 (x1, shr s1) ta1 (x1', m1')" (is "¬ ?τ")
proof
assume "?τ"
hence "ta1 = ε" by(rule r1.silent_tl)
with r1 have "r1.can_sync t x1 (shr s1) {}"
by(auto intro!: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
from csmw[OF this] show False by blast
qed
from simulation1[OF bisim r1 this]
obtain x2' m2' x2'' m2'' ta2 where r2: "r2.silent_moves t (x2, m2) (x2', m2')"
and r2': "t ⊢ (x2', m2') -2-ta2→  (x2'', m2'')"
and τ2: "¬ τmove2 (x2', m2') ta2 (x2'', m2'')"
and bisim': "t ⊢ (x1', m1') ≈ (x2'', m2'')" and tasim: "ta1 ∼m ta2" by auto
from r2
have "∃ta2 x2' m2' s2'. t ⊢ (x2, m2) -2-ta2→ (x2', m2') ∧ r2.actions_ok s2' t ta2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names base step])
case base
from r2'[folded base] s1'[unfolded ex_actions_ok1_conv_ex_actions_ok2[OF tasim]]
show ?thesis by blast
next
case (step x2''' m2''')
hence "t ⊢ (x2, m2) -2-ε→ (x2''', m2''')" by(auto dest: r2.silent_tl)
moreover have "r2.actions_ok (undefined, (undefined, undefined), Map.empty, undefined) t ε" by auto
ultimately show ?thesis by-(rule exI conjI|assumption)+
qed
hence "r2.must_sync t x2 m2" unfolding r2.must_sync_def2 . }
moreover
{ fix LT
assume "r2.can_sync t x2 m2 LT"
then obtain ta2 x2' m2' where r2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and LT: "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
by(auto elim: r2.can_syncE)
from ‹wset s1 t = None› ‹thr s1 t = ⌊(x1, no_wait_locks)⌋› ‹ts2' t = ⌊(x2, no_wait_locks)⌋›
have "¬ r2.silent_move t (x2, m2) (x2', m2')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t (x1, shr s1) (x1', m1')"
hence "t ⊢ (x1, shr s1) -1-ε→ (x1', m1')" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] show False by blast
qed
with r2 have "¬ τmove2 (x2, m2) ta2 (x2', m2')" by auto
from simulation2[OF bisim r2 this] obtain x1' m1' x1'' m1'' ta1
where τr1: "r1.silent_moves t (x1, shr s1) (x1', m1')"
and r1: "t ⊢ (x1', m1') -1-ta1→ (x1'', m1'')"
and nτ1: "¬ τmove1 (x1', m1') ta1 (x1'', m1'')"
and bisim': "t ⊢ (x1'', m1'') ≈ (x2', m2')"
and tlsim: "ta1 ∼m ta2" by auto
from τr1 obtain [simp]: "x1' = x1" "m1' = shr s1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step X M)
from ‹r1.silent_move t (x1, shr s1) (X, M)›
have "t ⊢ (x1, shr s1) -1-ε→ (X, M)" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] have False by blast
thus ?thesis ..
qed blast
from tlsim LT have "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙"
with r1 have "r1.can_sync t x1 (shr s1) LT" by(auto intro: r1.can_syncI)
from csmw[OF this] obtain lt
where lt: "lt ∈ LT" and mw: "r1.must_wait s1 t lt (r1.deadlocked s1 ∪ r1.final_threads s1)" by blast
by(auto dest: fin')
proof(cases rule: r1.must_wait_elims)
case lock thus ?thesis by(auto simp add: mbisim_eqs dest!: fin')
next
case (join t')
from ‹r1.not_final_thread s1 t'› obtain x1 ln
where "thr s1 t' = ⌊(x1, ln)⌋" by cases auto
with mbisim obtain x2 where "ts2' t' = ⌊(x2, ln)⌋" "t' ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD1)
show ?thesis
proof(cases "wset s1 t' = None ∧ ln = no_wait_locks")
case False
with ‹r1.not_final_thread s1 t'› ‹thr s1 t' = ⌊(x1, ln)⌋› ‹ts2' t' = ⌊(x2, ln)⌋› ‹lt = Inr (Inl t')› join
next
case True
with ‹r1.not_final_thread s1 t'› ‹thr s1 t' = ⌊(x1, ln)⌋› have "¬ final1 x1" by(cases) auto
with join ‹thr s1 t' = ⌊(x1, ln)⌋› have "t' ∈ r1.deadlocked s1" by(auto simp add: r1.final_thread_def)
have "¬ final2 x2"
proof
assume "final2 x2"
with final2_simulation[OF ‹t' ⊢ (x1, shr s1) ≈ (x2, m2)›]
obtain x1' m1' where "r1.silent_moves t' (x1, shr s1) (x1', m1')"
and "t' ⊢ (x1', m1') ≈ (x2, m2)" "final1 x1'" by auto
from ‹r1.silent_moves t' (x1, shr s1) (x1', m1')› have "x1' = x1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step x1'' m1'')
from ‹r1.silent_move t' (x1, shr s1) (x1'', m1'')›
have "t' ⊢ (x1, shr s1) -1-ε→ (x1'', m1'')" by(auto dest: r1.silent_tl)
hence "r1.redT s1 (t', ε) (redT_upd_ε s1 t' x1'' m1'')"
using ‹thr s1 t' = ⌊(x1, ln)⌋› True
by -(erule r1.redT_normal, auto simp add: redT_updLns_def redT_updWs_def finfun_Diag_const2 o_def)
thus ?thesis ..
qed simp
with ‹¬ final1 x1› ‹final1 x1'› show False by simp
qed
thus ?thesis using ‹ts2' t' = ⌊(x2, ln)⌋› join
qed
next
case (interrupt t')
proof(rule r2.all_final_exceptI)
fix t''
then obtain x2 ln where "thr ?s2 t'' = ⌊(x2, ln)⌋"
and fin: "¬ final2 x2 ∨ ln ≠ no_wait_locks ∨ wset ?s2 t'' ≠ None"
from ‹thr ?s2 t'' = ⌊(x2, ln)⌋› mbisim
obtain x1 where ts1t'': "thr s1 t'' = ⌊(x1, ln)⌋"
and bisim'': "t'' ⊢ (x1, shr s1) ≈ (x2, shr ?s2)"
by(auto dest: mbisim_thrD2)
proof(cases "wset ?s2 t'' = None ∧ ln = no_wait_locks")
case True
with fin have "¬ final2 x2" by simp
hence "¬ final1 x1"
proof(rule contrapos_nn)
assume "final1 x1"
with final1_simulation[OF bisim'']
obtain x2' m2' where τs2: "r2.silent_moves t'' (x2, shr ?s2) (x2', m2')"
and bisim''': "t'' ⊢ (x1, shr s1) ≈ (x2', m2')"
and "final2 x2'" by auto
from τs2 have "x2' = x2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case refl thus ?thesis by simp
next
case (step x2'' m2'')
from True have "wset s1 t'' = None" "thr s1 t'' = ⌊(x1, no_wait_locks)⌋" "ts2' t'' = ⌊(x2, no_wait_locks)⌋"
using ts1t'' ‹thr ?s2 t'' = ⌊(x2, ln)⌋› mbisim by(simp_all add: mbisim_def)
hence no_τ2: "¬ r2.silent_move t'' (x2, m2) (x2'', m2'')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t'' (x1, shr s1) (x1', m1')"
with ‹final1 x1› show False by(auto dest: r1.final_no_red)
qed
with ‹r2.silent_move t'' (x2, shr ?s2) (x2'', m2'')› have False by simp
thus ?thesis ..
qed
with ‹final2 x2'› show "final2 x2" by simp
qed
with ts1t'' show ?thesis ..
next
case False
qed
by(auto dest: fin' simp add: mbisim_eqs)
qed
thus ?thesis using interrupt mbisim by(auto simp add: mbisim_def)
qed
using ‹lt ∈ LT› by blast }
moreover from mbisim ‹wset s1 t = None› have "wset ?s2 t = None" by(simp add: mbisim_def)
ultimately have ?Lock by simp
thus ?thesis ..
next
case (wait x1 ln)
from mbisim ‹thr s1 t = ⌊(x1, ln)⌋›
obtain x2 where "ts2' t = ⌊(x2, ln)⌋" by(auto dest: mbisim_thrD1)
moreover
proof(rule r2.all_final_exceptI)
fix t
then obtain x2 ln where "ts2' t = ⌊(x2, ln)⌋" by(auto simp add: r2.not_final_thread_iff)
with mbisim obtain x1 where "thr s1 t = ⌊(x1, ln)⌋" "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD2)
hence "r1.not_final_thread s1 t" using ‹r2.not_final_thread ?s2 t› ‹ts2' t = ⌊(x2, ln)⌋› mbisim fin'[of t]
show "t ∈ r1.deadlocked s1" by(rule r1.all_final_exceptD)
qed
by(rule r2.all_final_except_mono') blast
moreover
from ‹waiting (wset s1 t)› mbisim
have "waiting (wset ?s2 t)" by(simp add: mbisim_def)
ultimately have ?Wait by simp
thus ?thesis by blast
next
case (acquire x1 ln l t')
from mbisim ‹thr s1 t = ⌊(x1, ln)⌋›
obtain x2 where "ts2' t = ⌊(x2, ln)⌋" by(auto dest: mbisim_thrD1)
moreover
have "(t' ∈ r1.deadlocked s1 ∨ t' ∈ r2.deadlocked ?s2) ∨ r2.final_thread ?s2 t'" by(blast dest: fin')
moreover
from mbisim ‹has_lock (locks s1 \$ l) t'›
have "has_lock (locks ?s2 \$ l) t'" by(simp add: mbisim_def)
ultimately have ?Acquire
using ‹0 < ln \$ l› ‹t ≠ t'› ‹¬ waiting (wset s1 t)› mbisim
thus ?thesis by blast
qed
qed
with red1 red2 mbisim show ?thesis by(blast intro: rtranclp_trans)
qed

"⟦ s1 ≈m s2; t ∈ r2.deadlocked s2 ⟧
⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ t ∈ r1.deadlocked s1' ∧ s1' ≈m s2"
unfolding flip_simps .

assumes mbisim: "s1 ≈m s2"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ r2.deadlock s2' ∧ s1 ≈m s2'"
case True
then obtain t where nfin: "r1.not_final_thread s1 t" ..
from mfinal1_inv_simulation[OF mbisim]
obtain ls2 ts2 m2 ws2 is2 where red1: "r2.mthr.silent_moves s2 (ls2, (ts2, m2), ws2, is2)"
and "s1 ≈m (ls2, (ts2, m2), ws2, is2)" and "m2 = shr s2"
and fin: "⋀t. r1.final_thread s1 t ⟹ r2.final_thread (ls2, (ts2, m2), ws2, is2) t" by fastforce
from no_τMove1_τs_to_no_τMove2[OF ‹s1 ≈m (ls2, (ts2, m2), ws2, is2)›]
obtain ts2' where red2: "r2.mthr.silent_moves (ls2, (ts2, m2), ws2, is2) (ls2, (ts2', m2), ws2, is2)"
and no_τ: "⋀t x1 x2 x2' m2'. ⟦ wset s1 t = None; thr s1 t = ⌊(x1, no_wait_locks)⌋; ts2' t = ⌊(x2, no_wait_locks)⌋;
⋀x' m'. r1.silent_move t (x1, shr s1) (x', m') ⟹ False ⟧
⟹  ¬ r2.silent_move t (x2, m2) (x2', m2')"
and mbisim: "s1 ≈m (ls2, (ts2', m2), ws2, is2)" by fastforce
from mbisim have mbisim_eqs: "ls2 = locks s1" "ws2 = wset s1" "is2 = interrupts s1"
let ?s2 = "(ls2, (ts2', m2), ws2, is2)"
from red2 have fin': "⋀t. r1.final_thread s1 t ⟹ r2.final_thread ?s2 t"
case (1 t x2)
note ts2t = ‹thr ?s2 t = ⌊(x2, no_wait_locks)⌋›
with mbisim obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and bisim: "t ⊢ (x1, shr s1) ≈ (x2, m2)" by(auto dest: mbisim_thrD2)
from ‹wset ?s2 t = None› mbisim have ws1t: "wset s1 t = None" by(simp add: mbisim_def)
have "¬ final1 x1"
proof
assume "final1 x1"
hence "r2.final_thread ?s2 t" by(rule fin')
with ‹¬ final2 x2› ts2t ‹wset ?s2 t = None› show False by(simp add: r2.final_thread_def)
qed
have ms: "r1.must_sync t x1 (shr s1)"
and csmw: "⋀LT. r1.can_sync t x1 (shr s1) LT ⟹ ∃lt∈LT. r1.must_wait s1 t lt (dom (thr s1))"
by blast+
{
from ‹r1.must_sync t x1 (shr s1)› obtain ta1 x1' m1'
where r1: "t ⊢ (x1, shr s1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
have "¬ τmove1 (x1, shr s1) ta1 (x1', m1')" (is "¬ ?τ")
proof
assume "?τ"
hence "ta1 = ε" by(rule r1.silent_tl)
with r1 have "r1.can_sync t x1 (shr s1) {}"
by(auto intro!: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
from csmw[OF this] show False by blast
qed
from simulation1[OF bisim r1 this]
obtain x2' m2' x2'' m2'' ta2 where r2: "r2.silent_moves t (x2, m2) (x2', m2')"
and r2': "t ⊢ (x2', m2') -2-ta2→  (x2'', m2'')"
and bisim': "t ⊢ (x1', m1') ≈ (x2'', m2'')" and tasim: "ta1 ∼m ta2" by auto
from r2
have "∃ta2 x2' m2' s2'. t ⊢ (x2, m2) -2-ta2→ (x2', m2') ∧ r2.actions_ok s2' t ta2"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names base step])
case base
from r2'[folded base] s1'[unfolded ex_actions_ok1_conv_ex_actions_ok2[OF tasim]]
show ?thesis by blast
next
case (step x2''' m2''')
hence "t ⊢ (x2, m2) -2-ε→ (x2''', m2''')" by(auto dest: r2.silent_tl)
moreover have "r2.actions_ok (undefined, (undefined, undefined), Map.empty, undefined) t ε" by auto
ultimately show ?thesis by-(rule exI conjI|assumption)+
qed
hence "r2.must_sync t x2 m2" unfolding r2.must_sync_def2 . }
moreover
{ fix LT
assume "r2.can_sync t x2 m2 LT"
then obtain ta2 x2' m2' where r2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and LT: "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
by(auto elim: r2.can_syncE)
from ts2t have "ts2' t = ⌊(x2, no_wait_locks)⌋" by simp
with ws1t ts1t have "¬ r2.silent_move t (x2, m2) (x2', m2')"
proof(rule no_τ)
fix x1' m1'
assume "r1.silent_move t (x1, shr s1) (x1', m1')"
hence "t ⊢ (x1, shr s1) -1-ε→ (x1', m1')" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] show False by blast
qed
with r2 have "¬ τmove2 (x2, m2) ta2 (x2', m2')" by auto
from simulation2[OF bisim r2 this] obtain x1' m1' x1'' m1'' ta1
where τr1: "r1.silent_moves t (x1, shr s1) (x1', m1')"
and r1: "t ⊢ (x1', m1') -1-ta1→ (x1'', m1'')"
and nτ1: "¬ τmove1 (x1', m1') ta1 (x1'', m1'')"
and bisim': "t ⊢ (x1'', m1'') ≈ (x2', m2')"
and tlsim: "ta1 ∼m ta2" by auto
from τr1 obtain [simp]: "x1' = x1" "m1' = shr s1"
proof(cases rule: converse_rtranclpE2[consumes 1, case_names refl step])
case (step X M)
from ‹r1.silent_move t (x1, shr s1) (X, M)›
have "t ⊢ (x1, shr s1) -1-ε→ (X, M)" by(auto dest: r1.silent_tl)
hence "r1.can_sync t x1 (shr s1) {}"
by(auto intro: r1.can_syncI simp add: collect_locks_def collect_interrupts_def)
with csmw[OF this] have False by blast
thus ?thesis ..
qed blast
from tlsim LT have "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙"
with r1 have "r1.can_sync t x1 (shr s1) LT" by(auto intro: r1.can_syncI)
from csmw[OF this] obtain lt
where lt: "lt ∈ LT" "r1.must_wait s1 t lt (dom (thr s1))" by blast
from ‹r1.must_wait s1 t lt (dom (thr s1))› have "r2.must_wait ?s2 t lt (dom (thr ?s2))"
proof(cases rule: r1.must_wait_elims)
case (lock l)
with mbisim_dom_eq[OF mbisim] show ?thesis by(auto simp add: mbisim_eqs)
next
case (join t')
have "r2.not_final_thread ?s2 t'" by auto
thus ?thesis using join mbisim_dom_eq[OF mbisim] by auto
next
case (interrupt t')
have "r2.all_final_except ?s2 (dom (thr ?s2))" by(auto intro!: r2.all_final_exceptI)
with interrupt show ?thesis by(auto simp add: mbisim_eqs)
qed
with lt have "∃lt∈LT. r2.must_wait ?s2 t lt (dom (thr ?s2))" by blast }
ultimately show ?case by fastforce
next
case (2 t x2 ln l)
from mbisim ‹thr ?s2 t = ⌊(x2, ln)⌋›
obtain x1 where "thr s1 t = ⌊(x1, ln)⌋" by(auto dest: mbisim_thrD2)
moreover note ‹0 < ln \$ l›
moreover from ‹¬ waiting (wset ?s2 t)› mbisim
have "¬ waiting (wset s1 t)" by(simp add: mbisim_def)
ultimately obtain l' t' where "0 < ln \$ l'" "t ≠ t'" "thr s1 t' ≠ None" "has_lock (locks s1 \$ l') t'"
thus ?case using mbisim_thrNone_eq[OF mbisim, of t'] mbisim by(auto simp add: mbisim_def)
next
case (3 t x2 w)
from mbisim_thrD2[OF mbisim this]
obtain x1 where "thr s1 t = ⌊(x1, no_wait_locks)⌋" by auto
with mbisim show ?case by(simp add: mbisim_def)
qed
with red1 red2 mbisim show ?thesis by(blast intro: rtranclp_trans)
next
case False
from mfinal1_simulation[OF mbisim this]
obtain s2' where "τmRed2 s2 s2'" "s1 ≈m s2'" "r2.mfinal s2'" "shr s2' = shr s2" by blast
qed

"⟦ s1 ≈m s2; r2.deadlock s2 ⟧
⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ r1.deadlock s1' ∧ s1' ≈m s2"
unfolding flip_simps .

"⟦ s1 ≈m s2; r1.deadlocked' s1 ⟧
⟹ ∃s2'. r2.mthr.silent_moves s2 s2' ∧ r2.deadlocked' s2' ∧ s1 ≈m s2'"

"⟦ s1 ≈m s2; r2.deadlocked' s2 ⟧ ⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ r1.deadlocked' s1' ∧ s1' ≈m s2"

end

context FWbisimulation begin

assumes mbisim: "s1 ≈m s2" and fin: "r1.final_thread s1 t"
proof -
from fin obtain x1 where ts1t: "thr s1 t = ⌊(x1, no_wait_locks)⌋"
and fin1: "final1 x1" and ws1t: "wset s1 t = None"
from mbisim ts1t obtain x2
where ts2t: "thr s2 t = ⌊(x2, no_wait_locks)⌋"
and bisim: "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" by(auto dest: mbisim_thrD1)
note ts2t moreover from fin1 bisim have "final2 x2" by(auto dest: bisim_final)
moreover from mbisim ws1t have "wset s2 t = None" by(simp add: mbisim_def)
qed

"⟦ s1 ≈m s2; r2.final_thread s2 t ⟧ ⟹ r1.final_thread s1 t"
unfolding flip_simps .

assumes bisim: "mbisim s1 s2"
proof(rule ext)
fix t
proof(cases "thr s1 t")
case None
with mbisim_thrNone_eq[OF bisim, of t] have "thr s2 t = None" by simp
with None show ?thesis
next
case (Some a)
then obtain x1 ln where tst1: "thr s1 t = ⌊(x1, ln)⌋" by(cases a) auto
from mbisim_thrD1[OF bisim tst1] obtain x2
where tst2: "thr s2 t = ⌊(x2, ln)⌋" and bisimt: "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" by blast
from bisim have "wset s2 = wset s1" by(simp add: mbisim_def)
with tst2 tst1 bisim_final[OF bisimt] show ?thesis
qed
qed

proof -
obtain s2' where "r2.mthr.silent_moves s2 s2'"
and "t ∈ r2.deadlocked s2'" by blast
from ‹r2.mthr.silent_moves s2 s2'› have "s2' = s2"
by(rule converse_rtranclpE)(auto elim: r2.mτmove.cases)
with ‹t ∈ r2.deadlocked s2'› show ?thesis by simp
qed

"⟦ s1 ≈m s2; t ∈ r2.deadlocked s2 ⟧ ⟹ t ∈ r1.deadlocked s1"
unfolding flip_simps .

end

(* Nice to have, but not needed any more *)

context FWbisimulation begin

lemma bisim_can_sync_preserve1:
assumes bisim: "t ⊢ (x1, m1) ≈ (x2, m2)" and cs: "t ⊢ ⟨x1, m1⟩ LT ≀1"
shows "t ⊢ ⟨x2, m2⟩ LT ≀2"
proof -
from cs obtain ta1 x1' m1' where red1: "t ⊢ (x1, m1) -1-ta1→ (x1', m1')"
and LT: "LT = collect_locks ⦃ta1⦄⇘l⇙ <+> collect_cond_actions ⦃ta1⦄⇘c⇙ <+> collect_interrupts ⦃ta1⦄⇘i⇙" by(rule r1.can_syncE)
from bisimulation.simulation1[OF bisimulation_axioms, OF bisim red1] obtain x2' ta2 m2'
where red2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and tasim: "ta1 ∼m ta2" by fastforce
from tasim LT have "LT = collect_locks ⦃ta2⦄⇘l⇙ <+> collect_cond_actions ⦃ta2⦄⇘c⇙ <+> collect_interrupts ⦃ta2⦄⇘i⇙"
with red2 show ?thesis by(rule r2.can_syncI)
qed

lemma bisim_can_sync_preserve2:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); t ⊢ ⟨x2, m2⟩ LT ≀2 ⟧ ⟹ t ⊢ ⟨x1, m1⟩ LT ≀1"
using FWbisimulation.bisim_can_sync_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .

lemma bisim_can_sync_inv:
"t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ⟨x1, m1⟩ LT ≀1 ⟷ t ⊢ ⟨x2, m2⟩ LT ≀2"
by(blast intro: bisim_can_sync_preserve1 bisim_can_sync_preserve2)

lemma bisim_must_sync_preserve1:
assumes bisim: "t ⊢ (x1, m1) ≈ (x2, m2)" and ms: "t ⊢ ⟨x1, m1⟩ ≀1"
shows "t ⊢ ⟨x2, m2⟩ ≀2"
proof -
from ms obtain ta1 x1' m1' where red1: "t ⊢ (x1, m1) -1-ta1→ (x1', m1')"
and s1': "∃s1'. r1.actions_ok s1' t ta1" by(fastforce elim: r1.must_syncE)
from bisimulation.simulation1[OF bisimulation_axioms, OF bisim red1] obtain x2' ta2 m2'
where red2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
and tasim: "ta1 ∼m ta2" by fastforce
from ex_actions_ok1_conv_ex_actions_ok2[OF tasim, of t] s1' red2
show ?thesis unfolding r2.must_sync_def2 by blast
qed

lemma bisim_must_sync_preserve2:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); t ⊢ ⟨x2, m2⟩ ≀2 ⟧ ⟹ t ⊢ ⟨x1, m1⟩ ≀1"
using FWbisimulation.bisim_must_sync_preserve1[OF FWbisimulation_flip]
unfolding flip_simps .

lemma bisim_must_sync_inv:
"t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ⟨x1, m1⟩ ≀1 ⟷ t ⊢ ⟨x2, m2⟩ ≀2"
by(blast intro: bisim_must_sync_preserve1 bisim_must_sync_preserve2)

end

end
```