# Theory FWBisimulation

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

section ‹Bisimulation relations for the multithreaded semantics›

theory FWBisimulation
imports
FWLTS
Bisimulation
begin

subsection ‹Definitions for lifting bisimulation relations›

primrec nta_bisim :: "('t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim) ⇒ (('t,'x1,'m1) new_thread_action, ('t,'x2,'m2) new_thread_action) bisim"
where
[code del]: "nta_bisim bisim (NewThread t x m) ta = (∃x' m'. ta = NewThread t x' m' ∧ bisim t (x, m) (x', m'))"
| "nta_bisim bisim (ThreadExists t b) ta = (ta = ThreadExists t b)"

lemma nta_bisim_1_code [code]:
"nta_bisim bisim (NewThread t x m) ta = (case ta of NewThread t' x' m' ⇒ t = t' ∧ bisim t (x, m) (x', m') | _ ⇒ False)"

lemma nta_bisim_simps_sym [simp]:
"nta_bisim bisim ta (NewThread t x m) = (∃x' m'. ta = NewThread t x' m' ∧ bisim t (x', m') (x, m))"
"nta_bisim bisim ta (ThreadExists t b) = (ta = ThreadExists t b)"
by(cases ta, auto)+

definition ta_bisim :: "('t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim) ⇒ (('l,'t,'x1,'m1,'w,'o) thread_action, ('l,'t,'x2,'m2,'w,'o) thread_action) bisim"
where
"ta_bisim bisim ta1 ta2 ≡
⦃ ta1 ⦄⇘l⇙ = ⦃ ta2 ⦄⇘l⇙ ∧ ⦃ ta1 ⦄⇘w⇙ = ⦃ ta2 ⦄⇘w⇙ ∧ ⦃ ta1 ⦄⇘c⇙ = ⦃ ta2 ⦄⇘c⇙ ∧ ⦃ ta1 ⦄⇘o⇙ = ⦃ ta2 ⦄⇘o⇙ ∧ ⦃ ta1 ⦄⇘i⇙ = ⦃ ta2 ⦄⇘i⇙ ∧
list_all2 (nta_bisim bisim) ⦃ ta1 ⦄⇘t⇙ ⦃ ta2 ⦄⇘t⇙"

lemma ta_bisim_empty [iff]: "ta_bisim bisim ε ε"

lemma ta_bisim_ε [simp]:
"ta_bisim b ε ta' ⟷ ta' = ε" "ta_bisim b ta ε ⟷ ta = ε"
apply(cases ta', fastforce simp add: ta_bisim_def)
apply(cases ta, fastforce simp add: ta_bisim_def)
done

lemma nta_bisim_mono:
assumes major: "nta_bisim bisim ta ta'"
and mono: "⋀t s1 s2. bisim t s1 s2 ⟹ bisim' t s1 s2"
shows "nta_bisim bisim' ta ta'"
using major by(cases ta)(auto intro: mono)

lemma ta_bisim_mono:
assumes major: "ta_bisim bisim ta1 ta2"
and mono: "⋀t s1 s2. bisim t s1 s2 ⟹ bisim' t s1 s2"
shows "ta_bisim bisim' ta1 ta2"
using major
by(auto simp add: ta_bisim_def elim!: List.list_all2_mono nta_bisim_mono intro: mono)

lemma nta_bisim_flip [flip_simps]:
"nta_bisim (λt. flip (bisim t)) = flip (nta_bisim bisim)"
by(rule ext)(case_tac x, auto simp add: flip_simps)

lemma ta_bisim_flip [flip_simps]:
"ta_bisim (λt. flip (bisim t)) = flip (ta_bisim bisim)"
by(auto simp add: fun_eq_iff flip_simps ta_bisim_def)

locale FWbisimulation_base =
r1: multithreaded_base final1 r1 convert_RA +
for final1 :: "'x1 ⇒ bool"
and r1 :: "('l,'t,'x1,'m1,'w,'o) semantics" ("_ ⊢ _ -1-_→ _" [50, 0, 0, 50] 80)
and final2 :: "'x2 ⇒ bool"
and r2 :: "('l,'t,'x2,'m2,'w,'o) semantics" ("_ ⊢ _ -2-_→ _" [50, 0, 0, 50] 80)
and convert_RA :: "'l released_locks ⇒ 'o list"
+
fixes bisim :: "'t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim" ("_ ⊢ _/ ≈ _" [50, 50, 50] 60)
and bisim_wait :: "('x1, 'x2) bisim" ("_/ ≈w _" [50, 50] 60)
begin

notation r1.redT_syntax1 ("_ -1-_▹_→ _" [50,0,0,50] 80)
notation r2.redT_syntax1 ("_ -2-_▹_→ _" [50,0,0,50] 80)

notation r1.RedT ("_ -1-▹_→* _" [50,0,50] 80)
notation r2.RedT ("_ -2-▹_→* _" [50,0,50] 80)

notation r1.must_sync ("_ ⊢ ⟨_,/ _⟩/ ≀1" [50,0,0] 81)
notation r2.must_sync ("_ ⊢ ⟨_,/ _⟩/ ≀2" [50,0,0] 81)

notation r1.can_sync  ("_ ⊢ ⟨_,/ _⟩/ _/ ≀1" [50,0,0,0] 81)
notation r2.can_sync  ("_ ⊢ ⟨_,/ _⟩/ _/ ≀2" [50,0,0,0] 81)

abbreviation ta_bisim_bisim_syntax ("_/ ∼m _" [50, 50] 60)
where "ta1 ∼m ta2 ≡ ta_bisim bisim ta1 ta2"

definition tbisim :: "bool ⇒ 't ⇒ ('x1 × 'l released_locks) option ⇒ 'm1 ⇒ ('x2 × 'l released_locks) option ⇒ 'm2 ⇒ bool" where
"⋀ln. tbisim nw t ts1 m1 ts2 m2 ⟷
(case ts1 of None ⇒ ts2 = None
| ⌊(x1, ln)⌋ ⇒ (∃x2. ts2 = ⌊(x2, ln)⌋ ∧ t ⊢ (x1, m1) ≈ (x2, m2) ∧ (nw ∨ x1 ≈w x2)))"

lemma tbisim_NoneI: "tbisim w t None m None m'"

lemma tbisim_SomeI:
"⋀ln. ⟦ t ⊢ (x, m) ≈ (x', m'); nw ∨ x ≈w x' ⟧ ⟹ tbisim nw t (Some (x, ln)) m (Some (x', ln)) m'"

lemma tbisim_cases[consumes 1, case_names None Some]:
assumes major: "tbisim nw t ts1 m1 ts2 m2"
and "⟦ ts1 = None; ts2 = None ⟧ ⟹ thesis"
and "⋀x ln x'. ⟦ ts1 = ⌊(x, ln)⌋; ts2 = ⌊(x', ln)⌋; t ⊢ (x, m1) ≈ (x', m2); nw ∨ x ≈w x' ⟧ ⟹ thesis"
shows thesis
using assms

definition mbisim :: "(('l,'t,'x1,'m1,'w) state, ('l,'t,'x2,'m2,'w) state) bisim" ("_ ≈m _" [50, 50] 60)
where
"s1 ≈m s2 ≡
finite (dom (thr s1)) ∧ locks s1 = locks s2 ∧ wset s1 = wset s2 ∧ wset_thread_ok (wset s1) (thr s1) ∧
interrupts s1 = interrupts s2 ∧
(∀t. tbisim (wset s2 t = None) t (thr s1 t) (shr s1) (thr s2 t) (shr s2))"

lemma mbisim_thrNone_eq: "s1 ≈m s2 ⟹ thr s1 t = None ⟷ thr s2 t = None"
unfolding mbisim_def tbisim_def
apply(clarify)
apply(erule allE[where x=t])
apply(clarsimp)
done

lemma mbisim_thrD1:
"⋀ln. ⟦ s1 ≈m s2; thr s1 t = ⌊(x, ln)⌋ ⟧
⟹ ∃x'. thr s2 t = ⌊(x', ln)⌋ ∧ t ⊢ (x, shr s1) ≈ (x', shr s2) ∧ (wset s1 t = None ∨ x ≈w x')"

lemma mbisim_thrD2:
"⋀ln. ⟦ s1 ≈m s2; thr s2 t = ⌊(x, ln)⌋ ⟧
⟹ ∃x'. thr s1 t = ⌊(x', ln)⌋ ∧ t ⊢ (x', shr s1) ≈ (x, shr s2) ∧ (wset s2 t = None ∨ x' ≈w x)"
by(frule mbisim_thrNone_eq[where t=t])(cases "thr s1 t",(fastforce simp add: mbisim_def tbisim_def)+)

lemma mbisim_dom_eq: "s1 ≈m s2 ⟹ dom (thr s1) = dom (thr s2)"
apply(clarsimp simp add: dom_def fun_eq_iff simp del: not_None_eq)
apply(rule Collect_cong)
apply(drule mbisim_thrNone_eq)
apply(simp del: not_None_eq)
done

"s1 ≈m s2 ⟹ wset_thread_ok (wset s1) (thr s1)"

assumes "s1 ≈m s2"
shows "wset_thread_ok (wset s2) (thr s2)"
using assms
done

lemma mbisimI:
"⟦ finite (dom (thr s1)); locks s1 = locks s2; wset s1 = wset s2; interrupts s1 = interrupts s2;
⋀t. thr s1 t = None ⟹ thr s2 t = None;
⋀t x1 ln. thr s1 t = ⌊(x1, ln)⌋ ⟹ ∃x2. thr s2 t = ⌊(x2, ln)⌋ ∧ t ⊢ (x1, shr s1) ≈ (x2, shr s2) ∧ (wset s2 t = None ∨ x1 ≈w x2) ⟧
⟹ s1 ≈m s2"

lemma mbisimI2:
"⟦ finite (dom (thr s2)); locks s1 = locks s2; wset s1 = wset s2; interrupts s1 = interrupts s2;
⋀t. thr s2 t = None ⟹ thr s1 t = None;
⋀t x2 ln. thr s2 t = ⌊(x2, ln)⌋ ⟹ ∃x1. thr s1 t = ⌊(x1, ln)⌋ ∧ t ⊢ (x1, shr s1) ≈ (x2, shr s2) ∧ (wset s2 t = None ∨ x1 ≈w x2) ⟧
⟹ s1 ≈m s2"
prefer 2
apply(case_tac "thr s2 t")
apply fastforce
apply(erule back_subst[where P=finite])
apply(clarsimp simp add: dom_def fun_eq_iff simp del: not_None_eq)
defer
apply(rename_tac t)
apply(case_tac [!] "thr s2 t")
by fastforce+

lemma mbisim_finite1:
"s1 ≈m s2 ⟹ finite (dom (thr s1))"

lemma mbisim_finite2:
"s1 ≈m s2 ⟹ finite (dom (thr s2))"

definition mta_bisim :: "('t × ('l,'t,'x1,'m1,'w,'o) thread_action,
("_/ ∼T _" [50, 50] 60)
where "tta1 ∼T tta2 ≡ fst tta1 = fst tta2 ∧ snd tta1 ∼m snd tta2"

lemma mta_bisim_conv [simp]: "(t, ta1) ∼T (t', ta2) ⟷ t = t' ∧ ta1 ∼m ta2"

definition bisim_inv :: "bool" where
"bisim_inv ≡ (∀s1 ta1 s1' s2 t. t ⊢ s1 ≈ s2 ⟶ t ⊢ s1 -1-ta1→ s1' ⟶ (∃s2'. t ⊢ s1' ≈ s2')) ∧
(∀s2 ta2 s2' s1 t. t ⊢ s1 ≈ s2 ⟶ t ⊢ s2 -2-ta2→ s2' ⟶ (∃s1'. t ⊢ s1' ≈ s2'))"

lemma bisim_invI:
"⟦ ⋀s1 ta1 s1' s2 t. ⟦ t ⊢ s1 ≈ s2; t ⊢ s1 -1-ta1→ s1' ⟧ ⟹ ∃s2'. t ⊢ s1' ≈ s2';
⋀s2 ta2 s2' s1 t. ⟦ t ⊢ s1 ≈ s2; t ⊢ s2 -2-ta2→ s2' ⟧ ⟹ ∃s1'. t ⊢ s1' ≈ s2' ⟧
⟹ bisim_inv"

lemma bisim_invD1:
"⟦ bisim_inv; t ⊢ s1 ≈ s2; t ⊢ s1 -1-ta1→ s1' ⟧ ⟹ ∃s2'. t ⊢ s1' ≈ s2'"
unfolding bisim_inv_def by blast

lemma bisim_invD2:
"⟦ bisim_inv; t ⊢ s1 ≈ s2; t ⊢ s2 -2-ta2→ s2' ⟧ ⟹ ∃s1'. t ⊢ s1' ≈ s2'"
unfolding bisim_inv_def by blast

"⟦ ∀t. ts1 t = None ⟷ ts2 t = None; list_all2 (nta_bisim bisim) tas1 tas2 ⟧
proof(induct tas2 arbitrary: tas1 ts1 ts2)
case Nil thus ?case by(simp)
next
case (Cons ta2 TAS2 tas1 TS1 TS2)
note IH = ‹⋀ts1 tas1 ts2. ⟦ ∀t. ts1 t = None ⟷ ts2 t = None; list_all2 (nta_bisim bisim) tas1 TAS2 ⟧
note eqNone = ‹∀t. TS1 t = None ⟷ TS2 t = None›[rule_format]
from ‹list_all2 (nta_bisim bisim) tas1 (ta2 # TAS2)›
obtain ta1 TAS1 where "tas1 = ta1 # TAS1" "nta_bisim bisim ta1 ta2" "list_all2 (nta_bisim bisim) TAS1 TAS2"
moreover
{ fix t
from ‹nta_bisim bisim ta1 ta2› have "redT_updT' TS1 ta1 t = None ⟷ redT_updT' TS2 ta2 t = None"
by(cases ta1, auto split: if_split_asm simp add: eqNone) }
ultimately have "thread_oks (redT_updT' TS1 ta1) TAS1 ⟷ thread_oks (redT_updT' TS2 ta2) TAS2"
by -(rule IH, auto)
moreover from ‹nta_bisim bisim ta1 ta2› fti have "thread_ok TS1 ta1 = thread_ok TS2 ta2" by(cases ta1, auto)
ultimately show ?case using ‹tas1 = ta1 # TAS1› by auto
qed

lemma redT_updT_nta_bisim_inv:
"⟦ nta_bisim bisim ta1 ta2; ts1 T = None ⟷ ts2 T = None ⟧ ⟹ redT_updT ts1 ta1 T = None ⟷ redT_updT ts2 ta2 T = None"
by(cases ta1, auto)

lemma redT_updTs_nta_bisim_inv:
"⟦ list_all2 (nta_bisim bisim) tas1 tas2; ts1 T = None ⟷ ts2 T = None ⟧
⟹ redT_updTs ts1 tas1 T = None ⟷ redT_updTs ts2 tas2 T = None"
proof(induct tas1 arbitrary: tas2 ts1 ts2)
case Nil thus ?case by(simp)
next
case (Cons TA1 TAS1 tas2 TS1 TS2)
note IH = ‹⋀tas2 ts1 ts2. ⟦list_all2 (nta_bisim bisim) TAS1 tas2; (ts1 T = None) = (ts2 T = None)⟧
⟹ (redT_updTs ts1 TAS1 T = None) = (redT_updTs ts2 tas2 T = None)›
from ‹list_all2 (nta_bisim bisim) (TA1 # TAS1) tas2›
obtain TA2 TAS2 where "tas2 = TA2 # TAS2" "nta_bisim bisim TA1 TA2" "list_all2 (nta_bisim bisim) TAS1 TAS2"
from ‹nta_bisim bisim TA1 TA2› ‹(TS1 T = None) = (TS2 T = None)›
have "redT_updT TS1 TA1 T = None ⟷ redT_updT TS2 TA2 T = None"
by(rule redT_updT_nta_bisim_inv)
with IH[OF ‹list_all2 (nta_bisim bisim) TAS1 TAS2›, of "redT_updT TS1 TA1" "redT_updT TS2 TA2"] ‹tas2 = TA2 # TAS2›
show ?case by simp
qed

end

lemma tbisim_flip [flip_simps]:
"FWbisimulation_base.tbisim (λt. flip (bisim t)) (flip bisim_wait) w t ts2 m2 ts1 m1 =
FWbisimulation_base.tbisim bisim bisim_wait w t ts1 m1 ts2 m2"
unfolding FWbisimulation_base.tbisim_def flip_simps by auto

lemma mbisim_flip [flip_simps]:
"FWbisimulation_base.mbisim (λt. flip (bisim t)) (flip bisim_wait) s2 s1 =
FWbisimulation_base.mbisim bisim bisim_wait s1 s2"
apply(rule iffI)
apply(frule FWbisimulation_base.mbisim_dom_eq)
apply(frule FWbisimulation_base.mbisim_dom_eq)
done

lemma mta_bisim_flip [flip_simps]:
"FWbisimulation_base.mta_bisim (λt. flip (bisim t)) = flip (FWbisimulation_base.mta_bisim bisim)"
by(auto simp add: fun_eq_iff flip_simps FWbisimulation_base.mta_bisim_def)

lemma flip_const [simp]: "flip (λa b. c) = (λa b. c)"
by(rule flip_def)

lemma mbisim_K_flip [flip_simps]:
"FWbisimulation_base.mbisim (λt. flip (bisim t)) (λx1 x2. c) s1 s2 =
FWbisimulation_base.mbisim bisim (λx1 x2. c) s2 s1"
using mbisim_flip[of bisim "λx1 x2. c" s1 s2]
unfolding flip_const .

context FWbisimulation_base begin

lemma mbisim_actions_ok_bisim_no_join_12:
assumes mbisim: "mbisim s1 s2"
and "collect_cond_actions ⦃ta1⦄⇘c⇙ = {}"
and "ta_bisim bisim ta1 ta2"
and "r1.actions_ok s1 t ta1"
shows "r2.actions_ok s2 t ta2"
using assms mbisim_thrNone_eq[OF mbisim]

lemma mbisim_actions_ok_bisim_no_join_21:
"⟦ mbisim s1 s2; collect_cond_actions ⦃ta2⦄⇘c⇙ = {}; ta_bisim bisim ta1 ta2; r2.actions_ok s2 t ta2 ⟧
⟹ r1.actions_ok s1 t ta1"
using FWbisimulation_base.mbisim_actions_ok_bisim_no_join_12[where bisim="λt. flip (bisim t)" and bisim_wait="flip bisim_wait"]
unfolding flip_simps .

lemma mbisim_actions_ok_bisim_no_join:
"⟦ mbisim s1 s2; collect_cond_actions ⦃ta1⦄⇘c⇙ = {}; ta_bisim bisim ta1 ta2 ⟧
⟹ r1.actions_ok s1 t ta1 = r2.actions_ok s2 t ta2"
apply(rule iffI)
apply(erule (3) mbisim_actions_ok_bisim_no_join_12)
apply(erule mbisim_actions_ok_bisim_no_join_21[where ?ta2.0 = ta2])
apply assumption+
done

end

locale FWbisimulation_base_aux = FWbisimulation_base +
r1: multithreaded final1 r1 convert_RA +
r2: multithreaded final2 r2 convert_RA +
constrains final1 :: "'x1 ⇒ bool"
and r1 :: "('l,'t,'x1,'m1,'w, 'o) semantics"
and final2 :: "'x2 ⇒ bool"
and r2 :: "('l,'t,'x2,'m2,'w, 'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and bisim :: "'t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim"
and bisim_wait :: "('x1, 'x2) bisim"
begin

lemma FWbisimulation_base_aux_flip:
"FWbisimulation_base_aux final2 r2 final1 r1"
by(unfold_locales)

end

lemma FWbisimulation_base_aux_flip_simps [flip_simps]:
"FWbisimulation_base_aux final2 r2 final1 r1 = FWbisimulation_base_aux final1 r1 final2 r2"
by(blast intro: FWbisimulation_base_aux.FWbisimulation_base_aux_flip)

sublocale FWbisimulation_base_aux < mthr:
bisimulation_final_base
r1.redT
r2.redT
mbisim
mta_bisim
r1.mfinal
r2.mfinal
.

declare split_paired_Ex [simp del]

subsection ‹Lifting for delay bisimulations›

locale FWdelay_bisimulation_base =
FWbisimulation_base _ _ _ r2 convert_RA bisim bisim_wait +
r1: τmultithreaded final1 r1 convert_RA τmove1 +
r2: τmultithreaded final2 r2 convert_RA τmove2
for r2 :: "('l,'t,'x2,'m2,'w,'o) semantics" ("_ ⊢ _ -2-_→ _" [50,0,0,50] 80)
and convert_RA :: "'l released_locks ⇒ 'o list"
and bisim :: "'t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim" ("_ ⊢ _/ ≈ _" [50, 50, 50] 60)
and bisim_wait :: "('x1, 'x2) bisim" ("_/ ≈w _" [50, 50] 60)
and τmove1 :: "('l,'t,'x1,'m1,'w,'o) τmoves"
and τmove2 :: "('l,'t,'x2,'m2,'w,'o) τmoves"
begin

abbreviation τmred1 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x1,'m1,'w) state ⇒ bool"
where "τmred1 ≡ r1.τmredT"

abbreviation τmred2 :: "('l,'t,'x2,'m2,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒ bool"
where "τmred2 ≡ r2.τmredT"

abbreviation mτmove1 :: "(('l,'t,'x1,'m1,'w) state, 't × ('l,'t,'x1,'m1,'w,'o) thread_action) trsys"
where "mτmove1 ≡ r1.mτmove"

abbreviation mτmove2 :: "(('l,'t,'x2,'m2,'w) state, 't × ('l,'t,'x2,'m2,'w,'o) thread_action) trsys"
where "mτmove2 ≡ r2.mτmove"

abbreviation τmRed1 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x1,'m1,'w) state ⇒ bool"
where "τmRed1 ≡ τmred1^**"

abbreviation τmRed2 :: "('l,'t,'x2,'m2,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒ bool"
where "τmRed2 ≡ τmred2^**"

abbreviation τmtRed1 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x1,'m1,'w) state ⇒ bool"
where "τmtRed1 ≡ τmred1^++"

abbreviation τmtRed2 :: "('l,'t,'x2,'m2,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒ bool"
where "τmtRed2 ≡ τmred2^++"

lemma bisim_inv_τs1_inv:
assumes inv: "bisim_inv"
and bisim: "t ⊢ s1 ≈ s2"
and red: "r1.silent_moves t s1 s1'"
obtains s2' where "t ⊢ s1' ≈ s2'"
proof(atomize_elim)
from red bisim show "∃s2'. t ⊢ s1' ≈ s2'"
by(induct rule: rtranclp_induct)(fastforce elim: bisim_invD1[OF inv])+
qed

lemma bisim_inv_τs2_inv:
assumes inv: "bisim_inv"
and bisim: "t ⊢ s1 ≈ s2"
and red: "r2.silent_moves t s2 s2'"
obtains s1' where "t ⊢ s1' ≈ s2'"
proof(atomize_elim)
from red bisim show "∃s1'. t ⊢ s1' ≈ s2'"
by(induct rule: rtranclp_induct)(fastforce elim: bisim_invD2[OF inv])+
qed

primrec activate_cond_action1 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒
't conditional_action ⇒ ('l,'t,'x1,'m1,'w) state"
where
"activate_cond_action1 s1 s2 (Join t) =
(case thr s1 t of None ⇒ s1
| ⌊(x1, ln1)⌋ ⇒ (case thr s2 t of None ⇒ s1
| ⌊(x2, ln2)⌋ ⇒
if final2 x2 ∧ ln2 = no_wait_locks
then redT_upd_ε s1 t
(SOME x1'. r1.silent_moves t (x1, shr s1) (x1', shr s1) ∧ final1 x1' ∧
t ⊢ (x1', shr s1) ≈ (x2, shr s2))
(shr s1)
else s1))"
| "activate_cond_action1 s1 s2 Yield = s1"

primrec activate_cond_actions1 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x2,'m2,'w) state
⇒ ('t conditional_action) list ⇒ ('l,'t,'x1,'m1,'w) state"
where
"activate_cond_actions1 s1 s2 [] = s1"
| "activate_cond_actions1 s1 s2 (ct # cts) = activate_cond_actions1 (activate_cond_action1 s1 s2 ct) s2 cts"

primrec activate_cond_action2 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒
't conditional_action ⇒ ('l,'t,'x2,'m2,'w) state"
where
"activate_cond_action2 s1 s2 (Join t) =
(case thr s2 t of None ⇒ s2
| ⌊(x2, ln2)⌋ ⇒ (case thr s1 t of None ⇒ s2
| ⌊(x1, ln1)⌋ ⇒
if final1 x1 ∧ ln1 = no_wait_locks
then redT_upd_ε s2 t
(SOME x2'. r2.silent_moves t (x2, shr s2) (x2', shr s2) ∧ final2 x2' ∧
t ⊢ (x1, shr s1) ≈ (x2', shr s2))
(shr s2)
else s2))"
| "activate_cond_action2 s1 s2 Yield = s2"

primrec activate_cond_actions2 :: "('l,'t,'x1,'m1,'w) state ⇒ ('l,'t,'x2,'m2,'w) state ⇒
('t conditional_action) list ⇒ ('l,'t,'x2,'m2,'w) state"
where
"activate_cond_actions2 s1 s2 [] = s2"
| "activate_cond_actions2 s1 s2 (ct # cts) = activate_cond_actions2 s1 (activate_cond_action2 s1 s2 ct) cts"

end

lemma activate_cond_action1_flip [flip_simps]:
"FWdelay_bisimulation_base.activate_cond_action1 final2 r2 final1 (λt. flip (bisim t)) τmove2 s2 s1 =
FWdelay_bisimulation_base.activate_cond_action2 final1 final2 r2 bisim τmove2 s1 s2"
apply(rule ext)
apply(case_tac x)
apply(simp_all only: FWdelay_bisimulation_base.activate_cond_action1.simps
FWdelay_bisimulation_base.activate_cond_action2.simps flip_simps)
done

lemma activate_cond_actions1_flip [flip_simps]:
"FWdelay_bisimulation_base.activate_cond_actions1 final2 r2 final1 (λt. flip (bisim t)) τmove2 s2 s1 =
FWdelay_bisimulation_base.activate_cond_actions2 final1 final2 r2 bisim τmove2 s1 s2"
(is "?lhs = ?rhs")
proof(rule ext)
fix xs
show "?lhs xs = ?rhs xs"
by(induct xs arbitrary: s2)
(simp_all only: FWdelay_bisimulation_base.activate_cond_actions1.simps
FWdelay_bisimulation_base.activate_cond_actions2.simps flip_simps)
qed

lemma activate_cond_action2_flip [flip_simps]:
"FWdelay_bisimulation_base.activate_cond_action2 final2 final1 r1 (λt. flip (bisim t)) τmove1 s2 s1 =
FWdelay_bisimulation_base.activate_cond_action1 final1 r1 final2 bisim τmove1 s1 s2"
apply(rule ext)
apply(case_tac x)
apply(simp_all only: FWdelay_bisimulation_base.activate_cond_action1.simps
FWdelay_bisimulation_base.activate_cond_action2.simps flip_simps)
done

lemma activate_cond_actions2_flip [flip_simps]:
"FWdelay_bisimulation_base.activate_cond_actions2 final2 final1 r1 (λt. flip (bisim t)) τmove1 s2 s1 =
FWdelay_bisimulation_base.activate_cond_actions1 final1 r1 final2 bisim τmove1 s1 s2"
(is "?lhs = ?rhs")
proof(rule ext)
fix xs
show "?lhs xs = ?rhs xs"
by(induct xs arbitrary: s1)
(simp_all only: FWdelay_bisimulation_base.activate_cond_actions1.simps
FWdelay_bisimulation_base.activate_cond_actions2.simps flip_simps)
qed

context FWdelay_bisimulation_base begin

lemma shr_activate_cond_action1 [simp]: "shr (activate_cond_action1 s1 s2 ct) = shr s1"
by(cases ct) simp_all

lemma shr_activate_cond_actions1 [simp]: "shr (activate_cond_actions1 s1 s2 cts) = shr s1"
by(induct cts arbitrary: s1) auto

lemma shr_activate_cond_action2 [simp]: "shr (activate_cond_action2 s1 s2 ct) = shr s2"
by(cases ct) simp_all

lemma shr_activate_cond_actions2 [simp]: "shr (activate_cond_actions2 s1 s2 cts) = shr s2"
by(induct cts arbitrary: s2) auto

lemma locks_activate_cond_action1 [simp]: "locks (activate_cond_action1 s1 s2 ct) = locks s1"
by(cases ct) simp_all

lemma locks_activate_cond_actions1 [simp]: "locks (activate_cond_actions1 s1 s2 cts) = locks s1"
by(induct cts arbitrary: s1) auto

lemma locks_activate_cond_action2 [simp]: "locks (activate_cond_action2 s1 s2 ct) = locks s2"
by(cases ct) simp_all

lemma locks_activate_cond_actions2 [simp]: "locks (activate_cond_actions2 s1 s2 cts) = locks s2"
by(induct cts arbitrary: s2) auto

lemma wset_activate_cond_action1 [simp]: "wset (activate_cond_action1 s1 s2 ct) = wset s1"
by(cases ct) simp_all

lemma wset_activate_cond_actions1 [simp]: "wset (activate_cond_actions1 s1 s2 cts) = wset s1"
by(induct cts arbitrary: s1) auto

lemma wset_activate_cond_action2 [simp]: "wset (activate_cond_action2 s1 s2 ct) = wset s2"
by(cases ct) simp_all

lemma wset_activate_cond_actions2 [simp]: "wset (activate_cond_actions2 s1 s2 cts) = wset s2"
by(induct cts arbitrary: s2) auto

lemma interrupts_activate_cond_action1 [simp]: "interrupts (activate_cond_action1 s1 s2 ct) = interrupts s1"
by(cases ct) simp_all

lemma interrupts_activate_cond_actions1 [simp]: "interrupts (activate_cond_actions1 s1 s2 cts) = interrupts s1"
by(induct cts arbitrary: s1) auto

lemma interrupts_activate_cond_action2 [simp]: "interrupts (activate_cond_action2 s1 s2 ct) = interrupts s2"
by(cases ct) simp_all

lemma interrupts_activate_cond_actions2 [simp]: "interrupts (activate_cond_actions2 s1 s2 cts) = interrupts s2"
by(induct cts arbitrary: s2) auto

end

locale FWdelay_bisimulation_lift_aux =
FWdelay_bisimulation_base _ _ _ _ _ _ _ τmove1 τmove2 +
r1: τmultithreaded_wf final1 r1 convert_RA τmove1 +
r2: τmultithreaded_wf final2 r2 convert_RA τmove2
for τmove1 :: "('l,'t,'x1,'m1,'w,'o) τmoves"
and τmove2 :: "('l,'t,'x2,'m2,'w,'o) τmoves"
begin

lemma FWdelay_bisimulation_lift_aux_flip:
"FWdelay_bisimulation_lift_aux final2 r2 final1 r1 τmove2 τmove1"
by unfold_locales

end

lemma FWdelay_bisimulation_lift_aux_flip_simps [flip_simps]:
"FWdelay_bisimulation_lift_aux final2 r2 final1 r1 τmove2 τmove1 =
FWdelay_bisimulation_lift_aux final1 r1 final2 r2 τmove1 τmove2"
by(auto dest: FWdelay_bisimulation_lift_aux.FWdelay_bisimulation_lift_aux_flip simp only: flip_flip)

context FWdelay_bisimulation_lift_aux begin

lemma cond_actions_ok_τmred1_inv:
assumes red: "τmred1 s1 s1'"
and ct: "r1.cond_action_ok s1 t ct"
shows "r1.cond_action_ok s1' t ct"
using ct
proof(cases ct)
case (Join t')
show ?thesis using red ct
proof(cases "thr s1 t'")
case None with red ct Join show ?thesis
by(fastforce elim!: r1.mthr.silent_move.cases r1.redT.cases r1.mτmove.cases rtrancl3p_cases
dest: r1.silent_tl split: if_split_asm)
next
case (Some a) with red ct Join show ?thesis
by(fastforce elim!: r1.mthr.silent_move.cases r1.redT.cases r1.mτmove.cases rtrancl3p_cases
dest: r1.silent_tl r1.final_no_red split: if_split_asm simp add: redT_updWs_def)
qed
next
case Yield thus ?thesis by simp
qed

lemma cond_actions_ok_τmred2_inv:
"⟦ τmred2 s2 s2'; r2.cond_action_ok s2 t ct ⟧ ⟹ r2.cond_action_ok s2' t ct"
using FWdelay_bisimulation_lift_aux.cond_actions_ok_τmred1_inv[OF FWdelay_bisimulation_lift_aux_flip] .

lemma cond_actions_ok_τmRed1_inv:
"⟦ τmRed1 s1 s1'; r1.cond_action_ok s1 t ct ⟧ ⟹ r1.cond_action_ok s1' t ct"
by(induct rule: rtranclp_induct)(blast intro: cond_actions_ok_τmred1_inv)+

lemma cond_actions_ok_τmRed2_inv:
"⟦ τmRed2 s2 s2'; r2.cond_action_ok s2 t ct ⟧ ⟹ r2.cond_action_ok s2' t ct"
by(rule FWdelay_bisimulation_lift_aux.cond_actions_ok_τmRed1_inv[OF FWdelay_bisimulation_lift_aux_flip])

end

locale FWdelay_bisimulation_lift =
FWdelay_bisimulation_lift_aux +
constrains final1 :: "'x1 ⇒ bool"
and r1 :: "('l, 't, 'x1, 'm1, 'w, 'o) semantics"
and final2 :: "'x2 ⇒ bool"
and r2 :: "('l, 't, 'x2, 'm2, 'w, 'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and bisim :: "'t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim"
and bisim_wait :: "('x1, 'x2) bisim"
and τmove1 :: "('l, 't, 'x1, 'm1, 'w, 'o) τmoves"
and τmove2 :: "('l, 't, 'x2, 'm2, 'w, 'o) τmoves"
assumes τinv_locale: "τinv (r1 t) (r2 t) (bisim t) (ta_bisim bisim) τmove1 τmove2"

sublocale FWdelay_bisimulation_lift < τinv "r1 t" "r2 t" "bisim t" "ta_bisim bisim" τmove1 τmove2 for t
by(rule τinv_locale)

context FWdelay_bisimulation_lift begin

lemma FWdelay_bisimulation_lift_flip:
"FWdelay_bisimulation_lift final2 r2 final1 r1 (λt. flip (bisim t)) τmove2 τmove1"
apply(rule FWdelay_bisimulation_lift.intro)
apply(rule FWdelay_bisimulation_lift_aux_flip)
apply(rule FWdelay_bisimulation_lift_axioms.intro)
apply(unfold flip_simps)
apply(unfold_locales)
done

end

lemma FWdelay_bisimulation_lift_flip_simps [flip_simps]:
"FWdelay_bisimulation_lift final2 r2 final1 r1 (λt. flip (bisim t)) τmove2 τmove1 =
FWdelay_bisimulation_lift final1 r1 final2 r2 bisim τmove1 τmove2"
by(auto dest: FWdelay_bisimulation_lift.FWdelay_bisimulation_lift_flip simp only: flip_flip)

context FWdelay_bisimulation_lift begin

lemma τinv_lift: "τinv r1.redT r2.redT mbisim mta_bisim mτmove1 mτmove2"
proof
fix s1 s2 tl1 s1' tl2 s2'
assume "s1 ≈m s2" "s1' ≈m s2'" "tl1 ∼T tl2" "r1.redT s1 tl1 s1'" "r2.redT s2 tl2 s2'"
moreover obtain t ta1 where tl1: "tl1 = (t, ta1)" by(cases tl1)
moreover obtain t' ta2 where tl2: "tl2 = (t', ta2)" by(cases tl2)
moreover obtain ls1 ts1 ws1 m1 is1 where s1: "s1 = (ls1, (ts1, m1), ws1, is1)" by(cases s1) fastforce
moreover obtain ls2 ts2 ws2 m2 is2 where s2: "s2 = (ls2, (ts2, m2), ws2, is2)" by(cases s2) fastforce
moreover obtain ls1' ts1' ws1' m1' is1' where s1': "s1' = (ls1', (ts1', m1'), ws1', is1')" by(cases s1') fastforce
moreover obtain ls2' ts2' ws2' m2' is2' where s2': "s2' = (ls2', (ts2', m2'), ws2', is2')" by(cases s2') fastforce
ultimately have mbisim: "(ls1, (ts1, m1), ws1, is1) ≈m (ls2, (ts2, m2), ws2, is2)"
and mbisim': "(ls1', (ts1', m1'), ws1', is1') ≈m (ls2', (ts2', m2'), ws2', is2')"
and mred1: "(ls1, (ts1, m1), ws1, is1) -1-t▹ta1→ (ls1', (ts1', m1'), ws1', is1')"
and mred2: "(ls2, (ts2, m2), ws2, is2) -2-t▹ta2→ (ls2', (ts2', m2'), ws2', is2')"
and tasim: "ta1 ∼m ta2" and tt': "t' = t" by simp_all
from mbisim have ls: "ls1 = ls2" and ws: "ws1 = ws2" and "is": "is1 = is2"
and tbisim: "⋀t. tbisim (ws2 t = None) t (ts1 t) m1 (ts2 t) m2" by(simp_all add: mbisim_def)
from mbisim' have ls': "ls1' = ls2'" and ws': "ws1' = ws2'" and is': "is1' = is2'"
and tbisim': "⋀t. tbisim (ws2' t = None) t (ts1' t) m1' (ts2' t) m2'" by(simp_all add: mbisim_def)
obtain x1 ln1 x1' ln1' where tst1: "ts1 t = ⌊(x1, ln1)⌋"
and tst1': "ts1' t = ⌊(x1', ln1')⌋"
by(fastforce elim!: r1.redT.cases)
obtain x2 ln2 x2' ln2' where tst2: "ts2 t = ⌊(x2, ln2)⌋"
and tst2': "ts2' t = ⌊(x2', ln2')⌋" by(fastforce elim!: r2.redT.cases)
from tbisim[of t] tst1 tst2 ws have bisim: "t ⊢ (x1, m1) ≈ (x2, m2)"
and ln: "ln1 = ln2" by(auto simp add: tbisim_def)
from tbisim'[of t] tst1' tst2' have bisim': "t ⊢ (x1', m1') ≈ (x2', m2')"
and ln': "ln1' = ln2'" by(auto simp add: tbisim_def)
show "mτmove1 s1 tl1 s1' = mτmove2 s2 tl2 s2'" unfolding s1 s2 s1' s2' tt' tl1 tl2
proof -
show "mτmove1 (ls1, (ts1, m1), ws1, is1) (t, ta1) (ls1', (ts1', m1'), ws1', is1') =
mτmove2 (ls2, (ts2, m2), ws2, is2) (t, ta2) (ls2', (ts2', m2'), ws2', is2')"
(is "?lhs = ?rhs")
proof
assume mτ: ?lhs
with tst1 tst1' obtain τ1: "τmove1 (x1, m1) ta1 (x1', m1')"
and ln1: "ln1 = no_wait_locks" by(fastforce elim!: r1.mτmove.cases)
from τ1 have "ta1 = ε" by(rule r1.silent_tl)
with mred1 τ1 tst1 tst1' ln1 have red1: "t ⊢ (x1, m1) -1-ta1→ (x1', m1')"
by(auto elim!: r1.redT.cases rtrancl3p_cases)
from tasim ‹ta1 = ε› have [simp]: "ta2 = ε" by(simp)
with mred2 ln1 ln tst2 tst2' have red2: "t ⊢ (x2, m2) -2-ε→ (x2', m2')"
by(fastforce elim!: r2.redT.cases rtrancl3p_cases)
from τ1 τinv[OF bisim red1 red2] bisim' tasim
have τ2: "τmove2 (x2, m2) ε (x2', m2')" by simp
with tst2 tst2' ln ln1 show ?rhs by -(rule r2.mτmove.intros, auto)
next
assume mτ: ?rhs
with tst2 tst2' obtain τ2: "τmove2 (x2, m2) ta2 (x2', m2')"
and ln2: "ln2 = no_wait_locks" by(fastforce elim!: r2.mτmove.cases)
from τ2 have "ta2 = ε" by(rule r2.silent_tl)
with mred2 τ2 tst2 tst2' ln2 have red2: "t ⊢ (x2, m2) -2-ta2→ (x2', m2')"
by(auto elim!: r2.redT.cases rtrancl3p_cases)
from tasim ‹ta2 = ε› have [simp]: "ta1 = ε" by simp
with mred1 ln2 ln tst1 tst1' have red1: "t ⊢ (x1, m1) -1-ε→ (x1', m1')"
by(fastforce elim!: r1.redT.cases rtrancl3p_cases)
from τ2 τinv[OF bisim red1 red2] bisim' tasim
have τ1: "τmove1 (x1, m1) ε (x1', m1')" by auto
with tst1 tst1' ln ln2 show ?lhs unfolding ‹ta1 = ε›
by-(rule r1.mτmove.intros, auto)
qed
qed
qed

end

sublocale FWdelay_bisimulation_lift < mthr: τinv r1.redT r2.redT mbisim mta_bisim mτmove1 mτmove2
by(rule τinv_lift)

locale FWdelay_bisimulation_final_base =
FWdelay_bisimulation_lift_aux +
constrains final1 :: "'x1 ⇒ bool"
and r1 :: "('l,'t,'x1,'m1,'w, 'o) semantics"
and final2 :: "'x2 ⇒ bool"
and r2 :: "('l,'t,'x2,'m2,'w, 'o) semantics"
and convert_RA :: "'l released_locks ⇒ 'o list"
and bisim :: "'t ⇒ ('x1 × 'm1, 'x2 × 'm2) bisim"
and bisim_wait :: "('x1, 'x2) bisim"
and τmove1 :: "('l,'t,'x1,'m1,'w, 'o) τmoves"
and τmove2 :: "('l,'t,'x2,'m2,'w, 'o) τmoves"
assumes delay_bisim_locale:
"delay_bisimulation_final_base (r1 t) (r2 t) (bisim t) τmove1 τmove2 (λ(x1, m). final1 x1) (λ(x2, m). final2 x2)"

sublocale FWdelay_bisimulation_final_base <
delay_bisimulation_final_base "r1 t" "r2 t" "bisim t" "ta_bisim bisim" τmove1 τmove2
"λ(x1, m). final1 x1" "λ(x2, m). final2 x2"
for t
by(rule delay_bisim_locale)

context FWdelay_bisimulation_final_base begin

lemma FWdelay_bisimulation_final_base_flip:
"FWdelay_bisimulation_final_base final2 r2 final1 r1 (λt. flip (bisim t)) τmove2 τmove1"
apply(rule FWdelay_bisimulation_final_base.intro)
apply(rule FWdelay_bisimulation_lift_aux_flip)
apply(rule FWdelay_bisimulation_final_base_axioms.intro)
apply(rule delay_bisimulation_final_base_flip)
done

end

lemma FWdelay_bisimulation_final_base_flip_simps [flip_simps]:
"FWdelay_bisimulation_final_base final2 r2 final1 r1 (λt. flip (bisim t)) τmove2 τmove1 =
FWdelay_bisimulation_final_base final1 r1 final2 r2 bisim τmove1 τmove2"
by(auto dest: FWdelay_bisimulation_final_base.FWdelay_bisimulation_final_base_flip simp only: flip_flip)

context FWdelay_bisimulation_final_base begin

lemma cond_actions_ok_bisim_ex_τ1_inv:
fixes ls ts1 m1 ws "is" ts2 m2 ct
defines "s1' ≡ activate_cond_action1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) ct"
assumes mbisim: "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2"
and ts1t: "ts1 t = Some xln"
and ts2t: "ts2 t = Some xln'"
and ct: "r2.cond_action_ok (ls, (ts2, m2), ws, is) t ct"
shows "τmRed1 (ls, (ts1, m1), ws, is) s1'"
and "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (thr s1' t') m1 (ts2 t') m2"
and "r1.cond_action_ok s1' t ct"
and "thr s1' t = Some xln"
proof -
have "τmRed1 (ls, (ts1, m1), ws, is) s1' ∧
(∀t'. t' ≠ t ⟶ tbisim (ws t' = None) t' (thr s1' t') m1 (ts2 t') m2) ∧
r1.cond_action_ok s1' t ct ∧ thr s1' t = ⌊xln⌋"
using ct
proof(cases ct)
case (Join t')
show ?thesis
proof(cases "ts1 t'")
case None
with mbisim ts1t have "t ≠ t'" by auto
moreover from None Join have "s1' = (ls, (ts1, m1), ws, is)" by(simp add: s1'_def)
ultimately show ?thesis using mbisim Join ct None ts1t by(simp add: tbisim_def)
next
case (Some xln)
moreover obtain x1 ln where "xln = (x1, ln)" by(cases xln)
ultimately have ts1t': "ts1 t' = ⌊(x1, ln)⌋" by simp
from Join ct Some ts2t have tt': "t' ≠ t" by auto
from mbisim[OF tt'] ts1t' obtain x2 where ts2t': "ts2 t' = ⌊(x2, ln)⌋"
and bisim: "t' ⊢ (x1, m1) ≈ (x2, m2)" by(auto simp add: tbisim_def)
from ct Join ts2t' have final2: "final2 x2" and ln: "ln = no_wait_locks"
and wst': "ws t' = None" by simp_all
let ?x1' = "SOME x. r1.silent_moves t' (x1, m1) (x, m1) ∧ final1 x ∧ t' ⊢ (x, m1) ≈ (x2, m2)"
{ from final2_simulation[OF bisim] final2 obtain x1' m1'
where "r1.silent_moves t' (x1, m1) (x1', m1')" and "t' ⊢ (x1', m1') ≈ (x2, m2)"
and "final1 x1'" by auto
moreover hence "m1' = m1" using bisim by(auto dest: r1.red_rtrancl_τ_heapD_inv)
ultimately have "∃x. r1.silent_moves t' (x1, m1) (x, m1) ∧ final1 x ∧ t' ⊢ (x, m1) ≈ (x2, m2)"
by blast }
from someI_ex[OF this] have red1: "r1.silent_moves t' (x1, m1) (?x1', m1)"
and final1: "final1 ?x1'" and bisim': "t' ⊢ (?x1', m1) ≈ (x2, m2)" by blast+
let ?S1' = "redT_upd_ε (ls, (ts1, m1), ws, is) t' ?x1' m1"
from r1.silent_moves_into_RedT_τ_inv[where ?s="(ls, (ts1, m1), ws, is)" and t=t', simplified, OF red1]
bisim ts1t' ln wst'
have Red1: "τmRed1 (ls, (ts1, m1), ws, is) ?S1'" by auto
moreover from Join ln ts1t' final1 wst' tt'
have ct': "r1.cond_action_ok ?S1' t ct" by(auto intro: finfun_ext)
{ fix t''
assume "t ≠ t''"
with Join mbisim[OF this[symmetric]] bisim' ts1t' ts2t' wst' s1'_def
have "tbisim (ws t'' = None) t'' (thr s1' t'') m1 (ts2 t'') m2"
by(auto simp add: tbisim_def redT_updLns_def o_def finfun_Diag_const2) }
moreover from Join ts1t' ts2t' final2 ln have "s1' = ?S1'" by(simp add: s1'_def)
ultimately show ?thesis using Red1 ct' ts1t' tt' ts1t by(auto)
qed
next
case Yield thus ?thesis using mbisim ts1t by(simp add: s1'_def)
qed
thus "τmRed1 (ls, (ts1, m1), ws, is) s1'"
and "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (thr s1' t') m1 (ts2 t') m2"
and "r1.cond_action_ok s1' t ct"
and "thr s1' t = ⌊xln⌋" by blast+
qed

lemma cond_actions_oks_bisim_ex_τ1_inv:
fixes ls ts1 m1 ws "is" ts2 m2 cts
defines "s1' ≡ activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts"
assumes tbisim: "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2"
and ts1t: "ts1 t = Some xln"
and ts2t: "ts2 t = Some xln'"
and ct: "r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts"
shows "τmRed1 (ls, (ts1, m1), ws, is) s1'"
and "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (thr s1' t') m1 (ts2 t') m2"
and "r1.cond_action_oks s1' t cts"
and "thr s1' t = Some xln"
using tbisim ts1t ct unfolding s1'_def
proof(induct cts arbitrary: ts1)
case (Cons ct cts)
note IH1 = ‹⋀ts1. ⟦⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2; ts1 t = ⌊xln⌋;
r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts⟧
⟹ τmred1⇧*⇧* (ls, (ts1, m1), ws, is) (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts)›
note IH2 = ‹⋀t' ts1. ⟦t' ≠ t; ⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2; ts1 t = ⌊xln⌋;
r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts⟧
⟹ tbisim (ws t' = None) t' (thr (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts) t') m1 (ts2 t') m2›
note IH3 = ‹⋀ts1. ⟦⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2; ts1 t = ⌊xln⌋;
r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts⟧
⟹ r1.cond_action_oks (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts) t cts›
note IH4 = ‹⋀ts1. ⟦⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2; ts1 t = ⌊xln⌋;
r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts⟧
⟹ thr (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts) t = ⌊xln⌋›
{ fix ts1
assume tbisim: "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2"
and ts1t: "ts1 t = ⌊xln⌋"
and ct: "r2.cond_action_oks (ls, (ts2, m2), ws, is) t (ct # cts)"
from ct have 1: "r2.cond_action_ok (ls, (ts2, m2), ws, is) t ct"
and 2: "r2.cond_action_oks (ls, (ts2, m2), ws, is) t cts" by auto
let ?s1' = "activate_cond_action1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) ct"
from cond_actions_ok_bisim_ex_τ1_inv[OF tbisim, OF _ ts1t ts2t 1]
have tbisim': "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (thr ?s1' t') m1 (ts2 t') m2"
and red: "τmRed1 (ls, (ts1, m1), ws, is) ?s1'" and ct': "r1.cond_action_ok ?s1' t ct"
and ts1't: "thr ?s1' t = ⌊xln⌋" by blast+
let ?s1'' = "activate_cond_actions1 ?s1' (ls, (ts2, m2), ws, is) cts"
have "locks ?s1' = ls" "shr ?s1' = m1" "wset ?s1' = ws" "interrupts ?s1' = is" by simp_all
hence s1': "(ls, (thr ?s1', m1), ws, is) = ?s1'" by(cases "?s1'") auto
from IH1[OF tbisim', OF _ ts1't 2] s1' have red': "τmRed1 ?s1' ?s1''" by simp
with red show "τmRed1 (ls, (ts1, m1), ws, is) (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) (ct # cts))"
by auto
{ fix t'
assume t't: "t' ≠ t"
from IH2[OF t't tbisim', OF _ ts1't 2] s1'
show "tbisim (ws t' = None) t' (thr (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) (ct # cts)) t') m1 (ts2 t') m2"
by auto }
from red' ct' have "r1.cond_action_ok ?s1'' t ct" by(rule cond_actions_ok_τmRed1_inv)
with IH3[OF tbisim', OF _ ts1't 2] s1'
show "r1.cond_action_oks (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) (ct # cts)) t (ct # cts)"
by auto
from ts1't IH4[OF tbisim', OF _ ts1't 2] s1'
show "thr (activate_cond_actions1 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) (ct # cts)) t = ⌊xln⌋" by auto }
qed(auto)

lemma cond_actions_ok_bisim_ex_τ2_inv:
fixes ls ts1 m1 "is" ws ts2 m2 ct
defines "s2' ≡ activate_cond_action2 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) ct"
assumes mbisim: "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2"
and ts1t: "ts1 t = Some xln"
and ts2t: "ts2 t = Some xln'"
and ct: "r1.cond_action_ok (ls, (ts1, m1), ws, is) t ct"
shows "τmRed2 (ls, (ts2, m2), ws, is) s2'"
and "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (thr s2' t') m2"
and "r2.cond_action_ok s2' t ct"
and "thr s2' t = Some xln'"
unfolding s2'_def
by(blast intro: FWdelay_bisimulation_final_base.cond_actions_ok_bisim_ex_τ1_inv[OF FWdelay_bisimulation_final_base_flip, where bisim_wait = "flip bisim_wait", unfolded flip_simps, OF mbisim _ _ ct, OF _ ts2t ts1t])+

lemma cond_actions_oks_bisim_ex_τ2_inv:
fixes ls ts1 m1 ws "is" ts2 m2 cts
defines "s2' ≡ activate_cond_actions2 (ls, (ts1, m1), ws, is) (ls, (ts2, m2), ws, is) cts"
assumes tbisim: "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (ts2 t') m2"
and ts1t: "ts1 t = Some xln"
and ts2t: "ts2 t = Some xln'"
and ct: "r1.cond_action_oks (ls, (ts1, m1), ws, is) t cts"
shows "τmRed2 (ls, (ts2, m2), ws, is) s2'"
and "⋀t'. t' ≠ t ⟹ tbisim (ws t' = None) t' (ts1 t') m1 (thr s2' t') m2"
and "r2.cond_action_oks s2' t cts"
and "thr s2' t = Some xln'"
unfolding s2'_def
by(blast intro: FWdelay_bisimulation_final_base.cond_actions_oks_bisim_ex_τ1_inv[OF FWdelay_bisimulation_final_base_flip, where bisim_wait = "flip bisim_wait", unfolded flip_simps, OF tbisim _ _ ct, OF _ ts2t ts1t])+

lemma mfinal1_inv_simulation:
assumes "s1 ≈m s2"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ s1 ≈m s2' ∧ r1.final_threads s1 ⊆ r2.final_threads s2' ∧ shr s2' = shr s2"
proof -
from ‹s1 ≈m s2› have "finite (dom (thr s1))" by(auto dest: mbisim_finite1)
ultimately have "finite (r1.final_threads s1)" by(blast intro: finite_subset)
thus ?thesis using ‹s1 ≈m s2›
proof(induct A≡"r1.final_threads s1" arbitrary: s1 s2 rule: finite_induct)
case empty
from ‹{} = r1.final_threads s1›[symmetric] have "∀t. ¬ r1.final_thread s1 t" by(auto)
with ‹s1 ≈m s2› show ?case by blast
next
case (insert t A)
define s1' where "s1' = (locks s1, ((thr s1)(t := None), shr s1), wset s1, interrupts s1)"
define s2' where "s2' = (locks s2, ((thr s2)(t := None), shr s2), wset s2, interrupts s2)"
from ‹t ∉ A› ‹insert t A = r1.final_threads s1› have "A = r1.final_threads s1'"
moreover from ‹insert t A = r1.final_threads s1› have "r1.final_thread s1 t" by auto
with ‹s1 ≈m s2› have "s1' ≈m s2'" unfolding s1'_def s2'_def
ultimately have "∃s2''. r2.mthr.silent_moves s2' s2'' ∧ s1' ≈m s2'' ∧ r1.final_threads s1' ⊆ r2.final_threads s2'' ∧ shr s2'' = shr s2'" by(rule insert)
then obtain s2'' where reds: "r2.mthr.silent_moves s2' s2''"
and "s1' ≈m s2''" and fin: "⋀t. r1.final_thread s1' t ⟹ r2.final_thread s2'' t" and "shr s2'' = shr s2'" by blast
have "thr s2' t = None" unfolding s2'_def by simp
with ‹r2.mthr.silent_moves s2' s2''›
have "r2.mthr.silent_moves (locks s2', ((thr s2')(t ↦ the (thr s2 t)), shr s2'), wset s2', interrupts s2')
(locks s2'', ((thr s2'')(t ↦ the (thr s2 t)), shr s2''), wset s2'', interrupts s2'')"
also let ?s2'' = "(locks s2, ((thr s2'')(t ↦ the (thr s2 t)), shr s2), wset s2, interrupts s2)"
from ‹shr s2'' = shr s2'› ‹s1' ≈m s2''› ‹s1 ≈m s2›
have "(locks s2'', ((thr s2'')(t ↦ the (thr s2 t)), shr s2''), wset s2'', interrupts s2'') = ?s2''"
unfolding s2'_def s1'_def by(simp add: mbisim_def)
also (back_subst) from ‹s1 ≈m s2› have "dom (thr s1) = dom (thr s2)" by(rule mbisim_dom_eq)
then obtain x2 ln where tst2: "thr s2 t = ⌊(x2, ln)⌋" by auto
hence "(locks s2', ((thr s2')(t ↦ the (thr s2 t)), shr s2'), wset s2', interrupts s2') = s2"
unfolding s2'_def by(cases s2)(auto intro!: ext)
also from ‹s1 ≈m s2› tst2 obtain x1
where tst1: "thr s1 t = ⌊(x1, ln)⌋"
and bisim: "t ⊢ (x1, shr s1) ≈ (x2, shr s2)" by(auto dest: mbisim_thrD2)
from ‹shr s2'' = shr s2'› have "shr ?s2'' = shr s2" by(simp add: s2'_def)
have final: "final1 x1" "ln = no_wait_locks" "wset s1 t = None" by(auto simp add: r1.final_thread_def)
with final1_simulation[OF bisim] ‹shr ?s2'' = shr s2› obtain x2' m2'
where red: "r2.silent_moves t (x2, shr ?s2'') (x2', m2')"
and bisim': "t ⊢ (x1, shr s1) ≈ (x2', m2')" and "final2 x2'" by auto
from ‹wset s1 t = None› ‹s1 ≈m s2› have "wset s2 t = None" by(simp add: mbisim_def)
with bisim r2.silent_moves_into_RedT_τ_inv[OF red] tst2 ‹ln = no_wait_locks›
have "r2.mthr.silent_moves ?s2'' (redT_upd_ε ?s2'' t x2' m2')" unfolding s2'_def by auto
also (rtranclp_trans)
from bisim r2.red_rtrancl_τ_heapD_inv[OF red] have "m2' = shr s2" by auto
hence "s1 ≈m (redT_upd_ε ?s2'' t x2' m2')"
using ‹s1' ≈m s2''› ‹s1 ≈m s2› tst1 tst2 ‹shr ?s2'' = shr s2› bisim' ‹shr s2'' = shr s2'› ‹wset s2 t = None›
unfolding s1'_def s2'_def by(auto simp add: mbisim_def redT_updLns_def split: if_split_asm intro: tbisim_SomeI)
moreover {
fix t'
with fin[of t'] ‹final2 x2'› tst2 ‹ln = no_wait_locks› ‹wset s2 t = None› ‹s1' ≈m s2''› ‹s1 ≈m s2›
have "r2.final_thread (redT_upd_ε ?s2'' t x2' m2') t'" unfolding s1'_def
}
moreover have "shr (redT_upd_ε ?s2'' t x2' m2') = shr s2" using ‹m2' = shr s2› by simp
ultimately show ?case by blast
qed
qed

lemma mfinal2_inv_simulation:
"s1 ≈m s2 ⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ s1' ≈m s2 ∧ r2.final_threads s2 ⊆ r1.final_threads s1' ∧ shr s1' = shr s1"
using FWdelay_bisimulation_final_base.mfinal1_inv_simulation[OF FWdelay_bisimulation_final_base_flip, where bisim_wait="flip bisim_wait"]
by(unfold flip_simps)

lemma mfinal1_simulation:
assumes "s1 ≈m s2" and "r1.mfinal s1"
shows "∃s2'. r2.mthr.silent_moves s2 s2' ∧ s1 ≈m s2' ∧ r2.mfinal s2' ∧ shr s2' = shr s2"
proof -
from mfinal1_inv_simulation[OF ‹s1 ≈m s2›]
obtain s2' where 1: "r2.mthr.silent_moves s2 s2'" "s1 ≈m s2'" "shr s2' = shr s2"
and fin: "⋀t. r1.final_thread s1 t ⟹ r2.final_thread s2' t" by blast
have "r2.mfinal s2'"
proof(rule r2.mfinalI)
fix t x2 ln
assume "thr s2' t = ⌊(x2, ln)⌋"
with ‹s1 ≈m s2'› obtain x1 where "thr s1 t = ⌊(x1, ln)⌋" "t ⊢ (x1, shr s1) ≈ (x2, shr s2')"
by(auto dest: mbisim_thrD2)
from ‹thr s1 t = ⌊(x1, ln)⌋› ‹r1.mfinal s1› have "r1.final_thread s1 t"
hence "r2.final_thread s2' t" by(rule fin)
thus "final2 x2 ∧ ln = no_wait_locks ∧ wset s2' t = None"
qed
with 1 show ?thesis by blast
qed

lemma mfinal2_simulation:
"⟦ s1 ≈m s2; r2.mfinal s2 ⟧
⟹ ∃s1'. r1.mthr.silent_moves s1 s1' ∧ s1' ≈m s2 ∧ r1.mfinal s1' ∧ shr s1' = shr s1"
using FWdelay_bisimulation_final_base.mfinal1_simulation[OF FWdelay_bisimulation_final_base_flip, where bisim_wait = "flip bisim_wait"]
by(unfold flip_simps)

end

locale FWdelay_bisimulation_obs =
FWdelay_bisimulation_final_base _ _ _ _ _ _ _ τmove1 τmove2
for τmove1 :: "('l,'t,'x1,'m1,'w, 'o) τmoves"
and τmove2 :: "('l,'t,'x2,'m2,'w, 'o) τmoves" +
assumes delay_bisimulation_obs_locale: "delay_bisimulation_obs (r1 t) (r2 t) (bisim t) (ta_bisim bisim) τmove1 τmove2"
and bisim_inv_red_other:
"⟦ t' ⊢ (x, m1) ≈ (xx, m2); t ⊢ (x1, m1) ≈ (x2, m2);
r1.silent_moves t (x1, m1) (x1', m1);
t ⊢ (x1', m1) -1-ta1→ (x1'', m1'); ¬ τmove1 (x1', m1) ta1 (x1'', m1');
r2.silent_moves t (x2, m2) (x2', m2);
t ⊢ (x2', m2) -2-ta2→ (x2'', m2'); ¬ τmove2 (x2', m2) ta2 (x2'', m2');
t ⊢ (x1'', m1') ≈ (x2'', m2'); ta_bisim bisim ta1 ta2 ⟧
⟹ t' ⊢ (x, m1') ≈ (xx, m2')"
and bisim_waitI:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); r1.silent_moves t (x1, m1) (x1', m1);
t ⊢ (x1', m1) -1-ta1→ (x1'', m1'); ¬ τmove1 (x1', m1) ta1 (x1'', m1');
r2.silent_moves t (x2, m2) (x2', m2);
t ⊢ (x2', m2) -2-ta2→ (x2'', m2'); ¬ τmove2 (x2', m2) ta2 (x2'', m2');
t ⊢ (x1'', m1') ≈ (x2'', m2'); ta_bisim bisim ta1 ta2;
Suspend w ∈ set ⦃ta1⦄⇘w⇙; Suspend w ∈ set ⦃ta2⦄⇘w⇙ ⟧
⟹ x1'' ≈w x2''"
and simulation_Wakeup1:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); x1 ≈w x2; t ⊢ (x1, m1) -1-ta1→ (x1', m1'); Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙ ⟧
⟹ ∃ta2 x2' m2'. t ⊢ (x2, m2) -2-ta2→ (x2', m2') ∧ t ⊢ (x1', m1') ≈ (x2', m2') ∧ ta_bisim bisim ta1 ta2"
and simulation_Wakeup2:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); x1 ≈w x2; t ⊢ (x2, m2) -2-ta2→ (x2', m2'); Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙ ⟧
⟹ ∃ta1 x1' m1'. t ⊢ (x1, m1) -1-ta1→ (x1', m1') ∧ t ⊢ (x1', m1') ≈ (x2', m2') ∧ ta_bisim bisim ta1 ta2"
and ex_final1_conv_ex_final2:
"(∃x1. final1 x1) ⟷ (∃x2. final2 x2)"

sublocale FWdelay_bisimulation_obs <
delay_bisimulation_obs "r1 t" "r2 t" "bisim t" "ta_bisim bisim" τmove1 τmove2 for t
by(rule delay_bisimulation_obs_locale)

context FWdelay_bisimulation_obs begin

lemma FWdelay_bisimulation_obs_flip:
"FWdelay_bisimulation_obs final2 r2 final1 r1 (λt. flip (bisim t)) (flip bisim_wait) τmove2 τmove1"
apply(rule FWdelay_bisimulation_obs.intro)
apply(rule FWdelay_bisimulation_final_base_flip)
apply(rule FWdelay_bisimulation_obs_axioms.intro)
apply(unfold flip_simps)
apply(rule delay_bisimulation_obs_axioms)
apply(erule (9) bisim_inv_red_other)
apply(erule (10) bisim_waitI)
apply(erule (3) simulation_Wakeup2)
apply(erule (3) simulation_Wakeup1)
apply(rule ex_final1_conv_ex_final2[symmetric])
done

end

lemma FWdelay_bisimulation_obs_flip_simps [flip_simps]:
"FWdelay_bisimulation_obs final2 r2 final1 r1 (λt. flip (bisim t)) (flip bisim_wait) τmove2 τmove1 =
FWdelay_bisimulation_obs final1 r1 final2 r2 bisim bisim_wait τmove1 τmove2"
by(auto dest: FWdelay_bisimulation_obs.FWdelay_bisimulation_obs_flip simp only: flip_flip)

context FWdelay_bisimulation_obs begin

lemma mbisim_redT_upd:
fixes s1 t ta1 x1' m1' s2 ta2 x2' m2' ln
assumes s1': "redT_upd s1 t ta1 x1' m1' s1'"
and s2': "redT_upd s2 t ta2 x2' m2' s2'"
and [simp]: "wset s1 = wset s2" "locks s1 = locks s2"
and wset: "wset s1' = wset s2'"
and interrupts: "interrupts s1' = interrupts s2'"
and fin1: "finite (dom (thr s1))"
and wsts: "wset_thread_ok (wset s1) (thr s1)"
and tst: "thr s1 t = ⌊(x1, ln)⌋"
and tst': "thr s2 t = ⌊(x2, ln)⌋"
and aoe1: "r1.actions_ok s1 t ta1"
and aoe2: "r2.actions_ok s2 t ta2"
and tasim: "ta_bisim bisim ta1 ta2"
and bisim': "t ⊢ (x1', m1') ≈ (x2', m2')"
and bisimw: "wset s1' t = None ∨ x1' ≈w x2'"
and τred1: "r1.silent_moves t (x1'', shr s1) (x1, shr s1)"
and red1: "t ⊢ (x1, shr s1) -1-ta1→ (x1', m1')"
and τred2: "r2.silent_moves t (x2'', shr s2) (x2, shr s2)"
and red2: "t ⊢ (x2, shr s2) -2-ta2→ (x2', m2')"
and bisim: "t ⊢ (x1'', shr s1) ≈ (x2'', shr s2)"
and τ1: "¬ τmove1 (x1, shr s1) ta1 (x1', m1')"
and τ2: "¬ τmove2 (x2, shr s2) ta2 (x2', m2')"
and tbisim: "⋀t'. t ≠ t' ⟹ tbisim (wset s1 t' = None) t' (thr s1 t') (shr s1) (thr s2 t') (shr s2)"
shows "s1' ≈m s2'"
proof(rule mbisimI)
from fin1 s1' show "finite (dom (thr s1'))"
next
from tasim s1' s2' show "locks s1' = locks s2'"
by(auto simp add: redT_updLs_def o_def ta_bisim_def)
next
from wset show "wset s1' = wset s2'" .
next
from interrupts show "interrupts s1' = interrupts s2'" .
next
from wsts s1' s2' wset show "wset_thread_ok (wset s1') (thr s1')"
next
fix T
assume "thr s1' T = None"
moreover with tst s1' have [simp]: "t ≠ T" by auto
from tbisim[OF this] have "(thr s1 T = None) = (thr s2 T = None)"
hence "(redT_updTs (thr s1) ⦃ta1⦄⇘t⇙ T = None) = (redT_updTs (thr s2) ⦃ta2⦄⇘t⇙ T = None)"
using tasim by -(rule redT_updTs_nta_bisim_inv, simp_all add: ta_bisim_def)
ultimately show "thr s2' T = None" using s2' s1' by(auto split: if_split_asm)
next
fix T X1 LN
assume tsT: "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 "thr s1 T")
case None
with tst have "t ≠ T" by auto
with tbisim[OF this] None have tsT': "thr s2 T = None" by(simp add: tbisim_def)
from None ‹t ≠ T› tsT aoe1 s1' obtain M1
where ntset: "NewThread T X1 M1 ∈ set ⦃ta1⦄⇘t⇙" and [simp]: "LN = no_wait_locks"
from ntset obtain tas1 tas1' where "⦃ta1⦄⇘t⇙ = tas1 @ NewThread T X1 M1 # tas1'"
with tasim obtain tas2 X2 M2 tas2' where "⦃ta2⦄⇘t⇙ = tas2 @ NewThread T X2 M2 # tas2'"
"length tas2 = length tas2" "length tas1' = length tas2'" and Bisim: "T ⊢ (X1, M1) ≈ (X2, M2)"
by(auto simp add: list_all2_append1 list_all2_Cons1 ta_bisim_def)
hence ntset': "NewThread T X2 M2 ∈ set ⦃ta2⦄⇘t⇙" by auto
with tsT' ‹t ≠ T› aoe2 s2' have "thr s2' T = ⌊(X2, no_wait_locks)⌋"
moreover from ntset' red2 have "m2' = M2" by(auto dest: r2.new_thread_memory)
moreover from ntset red1 have "m1' = M1"
moreover from wsts None have "wset s1 T = None" by(rule wset_thread_okD)
ultimately show ?thesis using Bisim ‹t ≠ T› s1' s2'
next
case (Some a)
show ?thesis
proof(cases "t = T")
case True
with tst tsT s1' have [simp]: "X1 = x1'" "LN = redT_updLns (locks s1) t ln ⦃ta1⦄⇘l⇙" by(auto)
show ?thesis using True bisim' bisimw tasim tst tst' s1' s2' wset
next
case False
with Some aoe1 tsT s1' have "thr s1 T = ⌊(X1, LN)⌋" by(auto dest: redT_updTs_Some)
with tbisim[OF False] obtain X2
where tsT': "thr s2 T = ⌊(X2, LN)⌋" and Bisim: "T ⊢ (X1, shr s1) ≈ (X2, shr s2)"
and bisimw: "wset s1 T = None ∨ X1 ≈w X2" by(auto simp add: tbisim_def)
with aoe2 False s2' have tsT': "thr s2' T = ⌊(X2, LN)⌋" by(auto simp add: redT_updTs_Some)
moreover from Bisim bisim τred1 red1 τ1 τred2 red2 τ2 bisim' tasim
have "T ⊢ (X1, m1') ≈ (X2, m2')" by(rule bisim_inv_red_other)
ultimately show ?thesis using False bisimw s1' s2'
qed
qed
qed

theorem mbisim_simulation1:
assumes mbisim: "mbisim s1 s2" and "¬ mτmove1 s1 tl1 s1'" "r1.redT s1 tl1 s1'"
shows "∃s2' s2'' tl2. r2.mthr.silent_moves s2 s2' ∧ r2.redT s2' tl2 s2'' ∧
¬ mτmove2 s2' tl2 s2'' ∧ mbisim s1' s2'' ∧ mta_bisim tl1 tl2"
proof -
from assms obtain t ta1 where tl1 [simp]: "tl1 = (t, ta1)" and redT: "s1 -1-t▹ta1→ s1'"
and mτ: "¬ mτmove1 s1 (t, ta1) s1'" by(cases tl1) fastforce
obtain ls1 ts1 m1 ws1 is1 where [simp]: "s1 = (ls1, (ts1, m1), ws1, is1)" by(cases s1) fastforce
obtain ls1' ts1' m1' ws1' is1' where [simp]: "s1' = (ls1', (ts1', m1'), ws1', is1')" by(cases s1') fastforce
obtain ls2 ts2 m2 ws2 is2 where [simp]: "s2 = (ls2, (ts2, m2), ws2, is2)" by(cases s2) fastforce
from mbisim have [simp]: "ls2 = ls1" "ws2 = ws1" "is2 = is1" "finite (dom ts1)" by(auto simp add: mbisim_def)
from redT show ?thesis
proof cases
case (redT_normal x1 x1' M1')
hence red: "t ⊢ (x1, m1) -1-ta1→ (x1', M1')"
and tst: "ts1 t = ⌊(x1, no_wait_locks)⌋"
and aoe: "r1.actions_ok s1 t ta1"
and s1': "redT_upd s1 t ta1 x1' M1' s1'" by auto
from mbisim tst obtain x2 where tst': "ts2 t = ⌊(x2, no_wait_locks)⌋"
and bisim: "t ⊢ (x1, m1) ≈ (x2, m2)" by(auto dest: mbisim_thrD1)
from mτ have τ: "¬ τmove1 (x1, m1) ta1 (x1', M1')"
proof(rule contrapos_nn)
assume τ: "τmove1 (x1, m1) ta1 (x1', M1')"
moreover hence [simp]: "ta1 = ε" by(rule r1.silent_tl)
moreover have [simp]: "M1' = m1" by(rule r1.τmove_heap[OF red τ, symmetric])
ultimately show "mτmove1 s1 (t, ta1) s1'" using s1' tst s1'
by(auto simp add: redT_updLs_def o_def intro: r1.mτmove.intros elim: rtrancl3p_cases)
qed
show ?thesis
proof(cases "ws1 t")
case None
note wst = this
from simulation1[OF bisim red τ] obtain x2' M2' x2'' M2'' ta2
where red21: "r2.silent_moves t (x2, m2) (x2', M2')"
and red22: "t ⊢ (x2', M2') -2-ta2→ (x2'', M2'')" and τ2: "¬ τmove2 (x2', M2') ta2 (x2'', M2'')"
and bisim': "t ⊢ (x1', M1') ≈ (x2'', M2'')"
and tasim: "ta_bisim bisim ta1 ta2" by auto
let ?s2' = "redT_upd_ε s2 t x2' M2'"
let ?S2' = "activate_cond_actions2 s1 ?s2' ⦃ta2⦄⇘c⇙"
let ?s2'' = "(redT_updLs (locks ?S2') t ⦃ta2⦄⇘l⇙, ((redT_updTs (thr ?S2') ⦃ta2⦄⇘t⇙)(t ↦ (x2'', redT_updLns (locks ?S2') t (snd (the (thr ?S2' t))) ⦃ta2⦄⇘l⇙)), M2''), wset s1', interrupts s1')"
from red21 tst' wst bisim have "τmRed2 s2 ?s2'"
by -(rule r2.silent_moves_into_RedT_τ_inv, auto)
moreover from red21 bisim have [simp]: "M2' = m2" by(auto dest: r2.red_rtrancl_τ_heapD_inv)
from tasim have [simp]: "⦃ ta1 ⦄⇘l⇙ = ⦃ ta2 ⦄⇘l⇙" "⦃ ta1 ⦄⇘w⇙ = ⦃ ta2 ⦄⇘w⇙" "⦃ ta1 ⦄⇘c⇙ = ⦃ ta2 ⦄⇘c⇙" "⦃ ta1 ⦄⇘i⇙ = ⦃ ta2 ⦄⇘i⇙"
and nta: "list_all2 (nta_bisim bisim) ⦃ ta1 ⦄⇘t⇙ ⦃ ta2 ⦄⇘t⇙" by(auto simp add: ta_bisim_def)
from mbisim have tbisim: "⋀t. tbisim (ws1 t = None) t (ts1 t) m1 (ts2 t) m2" by(simp add: mbisim_def)
hence tbisim': "⋀t'. t' ≠ t ⟹ tbisim (ws1 t' = None) t' (ts1 t') m1 (thr ?s2' t') m2" by(auto)
from aoe have cao1: "r1.cond_action_oks (ls1, (ts1, m1), ws1, is1) t ⦃ta2⦄⇘c⇙" by auto
from tst' have "thr ?s2' t = ⌊(x2', no_wait_locks)⌋" by(auto simp add: redT_updLns_def o_def finfun_Diag_const2)
from cond_actions_oks_bisim_ex_τ2_inv[OF tbisim', OF _ tst this cao1]
have red21': "τmRed2 ?s2' ?S2'" and tbisim'': "⋀t'. t' ≠ t ⟹ tbisim (ws1 t' = None) t' (ts1 t') m1 (thr ?S2' t') m2"
and cao2: "r2.cond_action_oks ?S2' t ⦃ta2⦄⇘c⇙" and tst'': "thr ?S2' t = ⌊(x2', no_wait_locks)⌋"
by(auto simp del: fun_upd_apply)
note red21' also (rtranclp_trans)
from tbisim'' tst'' tst have "∀t'. ts1 t' = None ⟷ thr ?S2' t' = None" by(force simp add: tbisim_def)
from aoe thread_oks_bisim_inv[OF this nta] have "thread_oks (thr ?S2') ⦃ta2⦄⇘t⇙" by simp
with cao2 aoe have aoe': "r2.actions_ok ?S2' t ta2" by auto
with red22 tst'' s1' have "?S2' -2-t▹ta2→ ?s2''"
by -(rule r2.redT.redT_normal, auto)
moreover
from τ2 have "¬ mτmove2 ?S2' (t, ta2) ?s2''"
proof(rule contrapos_nn)
assume mτ: "mτmove2 ?S2' (t, ta2) ?s2''"
thus "τmove2 (x2', M2') ta2 (x2'', M2'')" using tst'' tst'
by cases auto
qed
moreover
{
note s1'
moreover have "redT_upd ?S2' t ta2 x2'' M2'' ?s2''" using s1' by auto
moreover have "wset s1 = wset ?S2'" "locks s1 = locks ?S2'" by simp_all
moreover have "wset s1' = wset ?s2''" by simp
moreover have "interrupts s1' = interrupts ?s2''" by simp
moreover have "finite (dom (thr s1))" by simp
moreover from mbisim have "wset_thread_ok (wset s1) (thr s1)" by(simp add: mbisim_def)
moreover from tst have "thr s1 t = ⌊(x1, no_wait_locks)⌋" by simp
moreover note tst'' aoe aoe' tasim bisim'
moreover have "wset s1' t = None ∨ x1' ≈w x2''"
proof(cases "wset s1' t")
case None thus ?thesis ..
next
case (Some w)
with wst s1' obtain w' where Suspend1: "Suspend w' ∈ set ⦃ta1⦄⇘w⇙"
by(auto dest: redT_updWs_None_SomeD)
with tasim have Suspend2: "Suspend w' ∈ set ⦃ta2⦄⇘w⇙" by(simp add: ta_bisim_def)
from bisim_waitI[OF bisim rtranclp.rtrancl_refl red τ _ _ _ bisim' tasim Suspend1 this, of x2'] red21 red22```