Theory FWBisimLift
theory FWBisimLift imports
FWInitFinLift
FWBisimulation
begin
context FWbisimulation_base begin
inductive init_fin_bisim :: "'t ⇒ ((status × 'x1) × 'm1, (status × 'x2) × 'm2) bisim"
(‹_ ⊢ _ ≈i _›[50,50,50] 60)
for t :: 't
where
PreStart: "t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ((PreStart, x1), m1) ≈i ((PreStart, x2), m2)"
| Running: "t ⊢ (x1, m1) ≈ (x2, m2) ⟹ t ⊢ ((Running, x1), m1) ≈i ((Running, x2), m2)"
| Finished:
"⟦ t ⊢ (x1, m1) ≈ (x2, m2); final1 x1; final2 x2 ⟧
⟹ t ⊢ ((Finished, x1), m1) ≈i ((Finished, x2), m2)"
definition init_fin_bisim_wait :: "(status × 'x1, status × 'x2) bisim" (‹_ ≈iw _› [50,50] 60)
where
"init_fin_bisim_wait = (λ(status1, x1) (status2, x2). status1 = Running ∧ status2 = Running ∧ x1 ≈w x2)"
inductive_simps init_fin_bisim_simps [simp]:
"t ⊢ ((PreStart, x1), m1) ≈i ((s2, x2), m2)"
"t ⊢ ((Running, x1), m1) ≈i ((s2, x2), m2)"
"t ⊢ ((Finished, x1), m1) ≈i ((s2, x2), m2)"
"t ⊢ ((s1, x1), m1) ≈i ((PreStart, x2), m2)"
"t ⊢ ((s1, x1), m1) ≈i ((Running, x2), m2)"
"t ⊢ ((s1, x1), m1) ≈i ((Finished, x2), m2)"
lemma init_fin_bisim_iff:
"t ⊢ ((s1, x1), m1) ≈i ((s2, x2), m2) ⟷
s1 = s2 ∧ t ⊢ (x1, m1) ≈ (x2, m2) ∧ (s2 = Finished ⟶ final1 x1 ∧ final2 x2)"
by(cases s1) auto
lemma nta_bisim_init_fin_bisim [simp]:
"nta_bisim init_fin_bisim (convert_new_thread_action (Pair PreStart) nt1)
(convert_new_thread_action (Pair PreStart) nt2) =
nta_bisim bisim nt1 nt2"
by(cases nt1) simp_all
lemma ta_bisim_init_fin_bisim_convert [simp]:
"ta_bisim init_fin_bisim (convert_TA_initial (convert_obs_initial ta1)) (convert_TA_initial (convert_obs_initial ta2)) ⟷ ta1 ∼m ta2"
by(auto simp add: ta_bisim_def list_all2_map1 list_all2_map2)
lemma ta_bisim_init_fin_bisim_InitialThreadAction [simp]:
"ta_bisim init_fin_bisim ⦃InitialThreadAction⦄ ⦃InitialThreadAction⦄"
by(simp add: ta_bisim_def)
lemma ta_bisim_init_fin_bisim_ThreadFinishAction [simp]:
"ta_bisim init_fin_bisim ⦃ThreadFinishAction⦄ ⦃ThreadFinishAction⦄"
by(simp add: ta_bisim_def)
lemma init_fin_bisim_wait_simps [simp]:
"(status1, x1) ≈iw (status2, x2) ⟷ status1 = Running ∧ status2 = Running ∧ x1 ≈w x2"
by(simp add: init_fin_bisim_wait_def)
lemma init_fin_lift_state_mbisimI:
"s ≈m s' ⟹
FWbisimulation_base.mbisim init_fin_bisim init_fin_bisim_wait (init_fin_lift_state Running s) (init_fin_lift_state Running s')"
apply(rule FWbisimulation_base.mbisimI)
apply(simp add: thr_init_fin_list_state' o_def dom_map_option mbisim_finite1)
apply(simp add: locks_init_fin_lift_state mbisim_def)
apply(simp add: wset_init_fin_lift_state mbisim_def)
apply(simp add: interrupts_init_fin_lift_stae mbisim_def)
apply(clarsimp simp add: wset_init_fin_lift_state mbisim_def thr_init_fin_list_state' o_def wset_thread_ok_conv_dom dom_map_option del: subsetI)
apply(drule_tac t=t in mbisim_thrNone_eq)
apply(simp add: thr_init_fin_list_state)
apply(clarsimp simp add: thr_init_fin_list_state shr_init_fin_lift_state wset_init_fin_lift_state init_fin_bisim_iff)
apply(frule (1) mbisim_thrD1)
apply(simp add: mbisim_def)
done
end
context FWdelay_bisimulation_base begin
lemma init_fin_delay_bisimulation_final_base:
"delay_bisimulation_final_base (r1.init_fin t) (r2.init_fin t) (init_fin_bisim t)
r1.init_fin_τmove r2.init_fin_τmove (λ(x1, m). r1.init_fin_final x1) (λ(x2, m). r2.init_fin_final x2)"
by(unfold_locales)(auto 4 3)
end
lemma init_fin_bisim_flip [flip_simps]:
"FWbisimulation_base.init_fin_bisim final2 final1 (λt. flip (bisim t)) =
(λt. flip (FWbisimulation_base.init_fin_bisim final1 final2 bisim t))"
by(auto simp only: FWbisimulation_base.init_fin_bisim_iff flip_simps fun_eq_iff split_paired_Ex)
lemma init_fin_bisim_wait_flip [flip_simps]:
"FWbisimulation_base.init_fin_bisim_wait (flip bisim_wait) =
flip (FWbisimulation_base.init_fin_bisim_wait bisim_wait)"
by(auto simp add: fun_eq_iff FWbisimulation_base.init_fin_bisim_wait_simps flip_simps)
context FWdelay_bisimulation_lift_aux begin
lemma init_fin_FWdelay_bisimulation_lift_aux:
"FWdelay_bisimulation_lift_aux r1.init_fin_final r1.init_fin r2.init_fin_final r2.init_fin r1.init_fin_τmove r2.init_fin_τmove"
by(intro FWdelay_bisimulation_lift_aux.intro r1.τmultithreaded_wf_init_fin r2.τmultithreaded_wf_init_fin)
lemma init_fin_FWdelay_bisimulation_final_base:
"FWdelay_bisimulation_final_base
r1.init_fin_final r1.init_fin r2.init_fin_final r2.init_fin
init_fin_bisim r1.init_fin_τmove r2.init_fin_τmove"
by(intro FWdelay_bisimulation_final_base.intro init_fin_FWdelay_bisimulation_lift_aux FWdelay_bisimulation_final_base_axioms.intro init_fin_delay_bisimulation_final_base)
end
context FWdelay_bisimulation_obs begin
lemma init_fin_simulation1:
assumes bisim: "t ⊢ s1 ≈i s2"
and red1: "r1.init_fin t s1 tl1 s1'"
and τ1: "¬ r1.init_fin_τmove s1 tl1 s1'"
shows "∃s2' s2'' tl2. (τtrsys.silent_move (r2.init_fin t) r2.init_fin_τmove)⇧*⇧* s2 s2' ∧
r2.init_fin t s2' tl2 s2'' ∧ ¬ r2.init_fin_τmove s2' tl2 s2'' ∧
t ⊢ s1' ≈i s2'' ∧ ta_bisim init_fin_bisim tl1 tl2"
proof -
from bisim obtain status x1 m1 x2 m2
where s1: "s1 = ((status, x1), m1)"
and s2: "s2 = ((status, x2), m2)"
and bisim: "t ⊢ (x1, m1) ≈ (x2, m2)"
and finished: "status = Finished ⟹ final1 x1 ∧ final2 x2"
by(cases s1)(cases s2, fastforce simp add: init_fin_bisim_iff)
from red1 show ?thesis unfolding s1
proof(cases)
case (NormalAction ta1 x1' m1')
with τ1 s1 have "¬ τmove1 (x1, m1) ta1 (x1', m1')" by(simp)
from simulation1[OF bisim ‹t ⊢ (x1, m1) -1-ta1→ (x1', m1')› this]
obtain x2' m2' x2'' m2'' ta2
where red2: "r2.silent_moves t (x2, m2) (x2', m2')"
and red2': "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
let ?s2' = "((Running, x2'), m2')"
let ?s2'' = "((Running, x2''), m2'')"
let ?ta2 = "(convert_TA_initial (convert_obs_initial ta2))"
from red2 have "τtrsys.silent_moves (r2.init_fin t) r2.init_fin_τmove s2 ?s2'"
unfolding s2 ‹status = Running› by(rule r2.init_fin_silent_moves_RunningI)
moreover from red2' have "r2.init_fin t ?s2' ?ta2 ?s2''" by(rule r2.init_fin.NormalAction)
moreover from τ2 have "¬ r2.init_fin_τmove ?s2' ?ta2 ?s2''" by simp
moreover from bisim' have "t ⊢ s1' ≈i ?s2''"using ‹s1' = ((Running, x1'), m1')› by simp
moreover from tasim ‹tl1 = convert_TA_initial (convert_obs_initial ta1)›
have "ta_bisim init_fin_bisim tl1 ?ta2" by simp
ultimately show ?thesis by blast
next
case InitialThreadAction
with s1 s2 bisim show ?thesis by(auto simp del: split_paired_Ex)
next
case ThreadFinishAction
from final1_simulation[OF bisim] ‹final1 x1›
obtain x2' m2' where red2: "r2.silent_moves t (x2, m2) (x2', m2')"
and bisim': "t ⊢ (x1, m1) ≈ (x2', m2')"
and fin2: "final2 x2'" by auto
let ?s2' = "((Running, x2'), m2')"
let ?s2'' = "((Finished, x2'), m2')"
from red2 have "τtrsys.silent_moves (r2.init_fin t) r2.init_fin_τmove s2 ?s2'"
unfolding s2 ‹status = Running› by(rule r2.init_fin_silent_moves_RunningI)
moreover from fin2 have "r2.init_fin t ?s2' ⦃ThreadFinishAction⦄ ?s2''" ..
moreover have "¬ r2.init_fin_τmove ?s2' ⦃ThreadFinishAction⦄ ?s2''" by simp
moreover have "t ⊢ s1' ≈i ?s2''"
using ‹s1' = ((Finished, x1), m1)› fin2 ‹final1 x1› bisim' by simp
ultimately show ?thesis unfolding ‹tl1 = ⦃ThreadFinishAction⦄›
by(blast intro: ta_bisim_init_fin_bisim_ThreadFinishAction)
qed
qed
lemma init_fin_simulation2:
"⟦ t ⊢ s1 ≈i s2; r2.init_fin t s2 tl2 s2'; ¬ r2.init_fin_τmove s2 tl2 s2' ⟧
⟹ ∃s1' s1'' tl1. (τtrsys.silent_move (r1.init_fin t) r1.init_fin_τmove)⇧*⇧* s1 s1' ∧
r1.init_fin t s1' tl1 s1'' ∧ ¬ r1.init_fin_τmove s1' tl1 s1'' ∧
t ⊢ s1'' ≈i s2' ∧ ta_bisim init_fin_bisim tl1 tl2"
using FWdelay_bisimulation_obs.init_fin_simulation1[OF FWdelay_bisimulation_obs_flip]
unfolding flip_simps .
lemma init_fin_simulation_Wakeup1:
assumes bisim: "t ⊢ (sx1, m1) ≈i (sx2, m2)"
and wait: "sx1 ≈iw sx2"
and red1: "r1.init_fin t (sx1, m1) ta1 (sx1', m1')"
and wakeup: "Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙"
shows "∃ta2 sx2' m2'. r2.init_fin t (sx2, m2) ta2 (sx2', m2') ∧ t ⊢ (sx1', m1') ≈i (sx2', m2') ∧
ta_bisim init_fin_bisim ta1 ta2"
proof -
from bisim wait obtain status x1 x2
where sx1: "sx1 = (status, x1)"
and sx2: "sx2 = (status, x2)"
and Bisim: "t ⊢ (x1, m1) ≈ (x2, m2)"
and Wait: "x1 ≈w x2" by cases auto
from red1 wakeup sx1 obtain x1' ta1'
where sx1': "sx1' = (Running, x1')"
and status: "status = Running"
and Red1: "t ⊢ (x1, m1) -1-ta1'→ (x1', m1')"
and ta1: "ta1 = convert_TA_initial (convert_obs_initial ta1')"
and Wakeup: "Notified ∈ set ⦃ta1'⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1'⦄⇘w⇙"
by cases auto
from simulation_Wakeup1[OF Bisim Wait Red1 Wakeup] obtain ta2' x2' m2'
where red2: "t ⊢ (x2, m2) -2-ta2'→ (x2', m2')"
and bisim': "t ⊢ (x1', m1') ≈ (x2', m2')"
and tasim: "ta1' ∼m ta2'" by blast
let ?sx2' = "(Running, x2')"
let ?ta2 = "convert_TA_initial (convert_obs_initial ta2')"
from red2 have "r2.init_fin t (sx2, m2) ?ta2 (?sx2', m2')" unfolding sx2 status ..
moreover from bisim' sx1' have "t ⊢ (sx1', m1') ≈i (?sx2', m2')" by simp
moreover from tasim ta1 have "ta_bisim init_fin_bisim ta1 ?ta2" by simp
ultimately show ?thesis by blast
qed
lemma init_fin_simulation_Wakeup2:
"⟦ t ⊢ (sx1, m1) ≈i (sx2, m2); sx1 ≈iw sx2; r2.init_fin t (sx2, m2) ta2 (sx2', m2');
Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙ ⟧
⟹ ∃ta1 sx1' m1'. r1.init_fin t (sx1, m1) ta1 (sx1', m1') ∧ t ⊢ (sx1', m1') ≈i (sx2', m2') ∧
ta_bisim init_fin_bisim ta1 ta2"
using FWdelay_bisimulation_obs.init_fin_simulation_Wakeup1[OF FWdelay_bisimulation_obs_flip]
unfolding flip_simps .
lemma init_fin_delay_bisimulation_obs:
"delay_bisimulation_obs (r1.init_fin t) (r2.init_fin t) (init_fin_bisim t) (ta_bisim init_fin_bisim)
r1.init_fin_τmove r2.init_fin_τmove"
by(unfold_locales)(erule (2) init_fin_simulation1 init_fin_simulation2)+
lemma init_fin_FWdelay_bisimulation_obs:
"FWdelay_bisimulation_obs r1.init_fin_final r1.init_fin r2.init_fin_final r2.init_fin init_fin_bisim init_fin_bisim_wait r1.init_fin_τmove r2.init_fin_τmove"
proof(intro FWdelay_bisimulation_obs.intro init_fin_FWdelay_bisimulation_final_base FWdelay_bisimulation_obs_axioms.intro init_fin_delay_bisimulation_obs)
fix t' sx m1 sxx m2 t sx1 sx2 sx1' ta1 sx1'' m1' sx2' ta2 sx2'' m2'
assume bisim: "t' ⊢ (sx, m1) ≈i (sxx, m2)"
and bisim1: "t ⊢ (sx1, m1) ≈i (sx2, m2)"
and red1: "τtrsys.silent_moves (r1.init_fin t) r1.init_fin_τmove (sx1, m1) (sx1', m1)"
and red1': "r1.init_fin t (sx1', m1) ta1 (sx1'', m1')"
and τ1: "¬ r1.init_fin_τmove (sx1', m1) ta1 (sx1'', m1')"
and red2: "τtrsys.silent_moves (r2.init_fin t) r2.init_fin_τmove (sx2, m2) (sx2', m2)"
and red2':"r2.init_fin t (sx2', m2) ta2 (sx2'', m2')"
and τ2: "¬ r2.init_fin_τmove (sx2', m2) ta2 (sx2'', m2')"
and bisim1': "t ⊢ (sx1'', m1') ≈i (sx2'', m2')"
and tasim: "ta_bisim init_fin_bisim ta1 ta2"
from bisim obtain status x xx
where sx:"sx = (status, x)"
and sxx: "sxx = (status, xx)"
and Bisim: "t' ⊢ (x, m1) ≈ (xx, m2)"
and Finish: "status = Finished ⟹ final1 x ∧ final2 xx"
by(cases sx)(cases sxx, auto simp add: init_fin_bisim_iff)
from bisim1 obtain status1 x1 x2
where sx1: "sx1 = (status1, x1)"
and sx2: "sx2 = (status1, x2)"
and Bisim1: "t ⊢ (x1, m1) ≈ (x2, m2)"
by(cases sx1)(cases sx2, auto simp add: init_fin_bisim_iff)
from bisim1' obtain status1' x1'' x2''
where sx1'': "sx1'' = (status1', x1'')"
and sx2'': "sx2'' = (status1', x2'')"
and Bisim1': "t ⊢ (x1'', m1') ≈ (x2'', m2')"
by(cases sx1'')(cases sx2'', auto simp add: init_fin_bisim_iff)
from red1 sx1 obtain x1' where sx1': "sx1' = (status1, x1')"
and Red1: "r1.silent_moves t (x1, m1) (x1', m1)"
by(cases sx1')(auto dest: r1.init_fin_silent_movesD)
from red2 sx2 obtain x2' where sx2': "sx2' = (status1, x2')"
and Red2: "r2.silent_moves t (x2, m2) (x2', m2)"
by(cases sx2')(auto dest: r2.init_fin_silent_movesD)
show "t' ⊢ (sx, m1') ≈i (sxx, m2')"
proof(cases "status1 = Running ∧ status1' = Running")
case True
with red1' sx1' sx1'' obtain ta1'
where Red1': "t ⊢ (x1', m1) -1-ta1'→ (x1'', m1')"
and ta1: "ta1 = convert_TA_initial (convert_obs_initial ta1')"
by cases auto
from red2' sx2' sx2'' True obtain ta2'
where Red2': "t ⊢ (x2', m2) -2-ta2'→ (x2'', m2')"
and ta2: "ta2 = convert_TA_initial (convert_obs_initial ta2')"
by cases auto
from τ1 sx1' sx1'' ta1 True have τ1':"¬ τmove1 (x1', m1) ta1' (x1'', m1')" by simp
from τ2 sx2' sx2'' ta2 True have τ2':"¬ τmove2 (x2', m2) ta2' (x2'', m2')" by simp
from tasim ta1 ta2 have "ta1' ∼m ta2'" by simp
with Bisim Bisim1 Red1 Red1' τ1' Red2 Red2' τ2' Bisim1'
have "t' ⊢ (x, m1') ≈ (xx, m2')" by(rule bisim_inv_red_other)
with True Finish show ?thesis unfolding sx sxx by(simp add: init_fin_bisim_iff)
next
case False
with red1' sx1' sx1'' have "m1' = m1" by cases auto
moreover from red2' sx2' sx2'' False have "m2' = m2" by cases auto
ultimately show ?thesis using bisim by simp
qed
next
fix t sx1 m1 sx2 m2 sx1' ta1 sx1'' m1' sx2' ta2 sx2'' m2' w
assume bisim: "t ⊢ (sx1, m1) ≈i (sx2, m2)"
and red1: "τtrsys.silent_moves (r1.init_fin t) r1.init_fin_τmove (sx1, m1) (sx1', m1)"
and red1': "r1.init_fin t (sx1', m1) ta1 (sx1'', m1')"
and τ1: "¬ r1.init_fin_τmove (sx1', m1) ta1 (sx1'', m1')"
and red2: "τtrsys.silent_moves (r2.init_fin t) r2.init_fin_τmove (sx2, m2) (sx2', m2)"
and red2': "r2.init_fin t (sx2', m2) ta2 (sx2'', m2')"
and τ2: "¬ r2.init_fin_τmove (sx2', m2) ta2 (sx2'', m2')"
and bisim': "t ⊢ (sx1'', m1') ≈i (sx2'', m2')"
and tasim: "ta_bisim init_fin_bisim ta1 ta2"
and suspend1: "Suspend w ∈ set ⦃ta1⦄⇘w⇙"
and suspend2: "Suspend w ∈ set ⦃ta2⦄⇘w⇙"
from bisim obtain status x1 x2
where sx1: "sx1 = (status, x1)"
and sx2: "sx2 = (status, x2)"
and Bisim: "t ⊢ (x1, m1) ≈ (x2, m2)"
by(cases sx1)(cases sx2, auto simp add: init_fin_bisim_iff)
from bisim' obtain status' x1'' x2''
where sx1'': "sx1'' = (status', x1'')"
and sx2'': "sx2'' = (status', x2'')"
and Bisim': "t ⊢ (x1'', m1') ≈ (x2'', m2')"
by(cases sx1'')(cases sx2'', auto simp add: init_fin_bisim_iff)
from red1 sx1 obtain x1' where sx1': "sx1' = (status, x1')"
and Red1: "r1.silent_moves t (x1, m1) (x1', m1)"
by(cases sx1')(auto dest: r1.init_fin_silent_movesD)
from red2 sx2 obtain x2' where sx2': "sx2' = (status, x2')"
and Red2: "r2.silent_moves t (x2, m2) (x2', m2)"
by(cases sx2')(auto dest: r2.init_fin_silent_movesD)
from red1' sx1' sx1'' suspend1 obtain ta1'
where Red1': "t ⊢ (x1', m1) -1-ta1'→ (x1'', m1')"
and ta1: "ta1 = convert_TA_initial (convert_obs_initial ta1')"
and Suspend1: "Suspend w ∈ set ⦃ta1'⦄⇘w⇙"
and status: "status = Running" "status' = Running" by cases auto
from red2' sx2' sx2'' suspend2 obtain ta2'
where Red2': "t ⊢ (x2', m2) -2-ta2'→ (x2'', m2')"
and ta2: "ta2 = convert_TA_initial (convert_obs_initial ta2')"
and Suspend2: "Suspend w ∈ set ⦃ta2'⦄⇘w⇙" by cases auto
from τ1 sx1' sx1'' ta1 status have τ1':"¬ τmove1 (x1', m1) ta1' (x1'', m1')" by simp
from τ2 sx2' sx2'' ta2 status have τ2':"¬ τmove2 (x2', m2) ta2' (x2'', m2')" by simp
from tasim ta1 ta2 have "ta1' ∼m ta2'" by simp
with Bisim Red1 Red1' τ1' Red2 Red2' τ2' Bisim' have "x1'' ≈w x2''"
using Suspend1 Suspend2 by(rule bisim_waitI)
thus "sx1'' ≈iw sx2''" using sx1'' sx2'' status by simp
next
fix t sx1 m1 sx2 m2 ta1 sx1' m1'
assume "t ⊢ (sx1, m1) ≈i (sx2, m2)" and "sx1 ≈iw sx2"
and "r1.init_fin t (sx1, m1) ta1 (sx1', m1')"
and "Notified ∈ set ⦃ta1⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta1⦄⇘w⇙"
thus "∃ta2 sx2' m2'. r2.init_fin t (sx2, m2) ta2 (sx2', m2') ∧ t ⊢ (sx1', m1') ≈i (sx2', m2') ∧
ta_bisim init_fin_bisim ta1 ta2"
by(rule init_fin_simulation_Wakeup1)
next
fix t sx1 m1 sx2 m2 ta2 sx2' m2'
assume "t ⊢ (sx1, m1) ≈i (sx2, m2)" and "sx1 ≈iw sx2"
and "r2.init_fin t (sx2, m2) ta2 (sx2', m2')"
and "Notified ∈ set ⦃ta2⦄⇘w⇙ ∨ WokenUp ∈ set ⦃ta2⦄⇘w⇙"
thus "∃ta1 sx1' m1'. r1.init_fin t (sx1, m1) ta1 (sx1', m1') ∧ t ⊢ (sx1', m1') ≈i (sx2', m2') ∧
ta_bisim init_fin_bisim ta1 ta2"
by(rule init_fin_simulation_Wakeup2)
next
show "(∃sx1. r1.init_fin_final sx1) = (∃sx2. r2.init_fin_final sx2)"
using ex_final1_conv_ex_final2 by(auto)
qed
end
context FWdelay_bisimulation_diverge begin
lemma init_fin_simulation_silent1:
"⟦ t ⊢ sxm1 ≈i sxm2; τtrsys.silent_move (r1.init_fin t) r1.init_fin_τmove sxm1 sxm1' ⟧
⟹ ∃sxm2'. τtrsys.silent_moves (r2.init_fin t) r2.init_fin_τmove sxm2 sxm2' ∧ t ⊢ sxm1' ≈i sxm2'"
by(cases sxm1')(auto 4 4 elim!: init_fin_bisim.cases dest!: r1.init_fin_silent_moveD dest: simulation_silent1 intro!: r2.init_fin_silent_moves_RunningI)
lemma init_fin_simulation_silent2:
"⟦ t ⊢ sxm1 ≈i sxm2; τtrsys.silent_move (r2.init_fin t) r2.init_fin_τmove sxm2 sxm2' ⟧
⟹ ∃sxm1'. τtrsys.silent_moves (r1.init_fin t) r1.init_fin_τmove sxm1 sxm1' ∧ t ⊢ sxm1' ≈i sxm2'"
using FWdelay_bisimulation_diverge.init_fin_simulation_silent1[OF FWdelay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma init_fin_τdiverge_bisim_inv:
"t ⊢ sxm1 ≈i sxm2
⟹ τtrsys.τdiverge (r1.init_fin t) r1.init_fin_τmove sxm1 =
τtrsys.τdiverge (r2.init_fin t) r2.init_fin_τmove sxm2"
by(cases sxm1)(cases sxm2, auto simp add: r1.init_fin_τdiverge_conv r2.init_fin_τdiverge_conv init_fin_bisim_iff τdiverge_bisim_inv)
lemma init_fin_delay_bisimulation_diverge:
"delay_bisimulation_diverge (r1.init_fin t) (r2.init_fin t) (init_fin_bisim t) (ta_bisim init_fin_bisim)
r1.init_fin_τmove r2.init_fin_τmove"
by(blast intro: delay_bisimulation_diverge.intro init_fin_delay_bisimulation_obs delay_bisimulation_diverge_axioms.intro init_fin_simulation_silent1 init_fin_simulation_silent2 init_fin_τdiverge_bisim_inv del: iffI)+
lemma init_fin_FWdelay_bisimulation_diverge:
"FWdelay_bisimulation_diverge r1.init_fin_final r1.init_fin r2.init_fin_final r2.init_fin init_fin_bisim init_fin_bisim_wait r1.init_fin_τmove r2.init_fin_τmove"
by(intro FWdelay_bisimulation_diverge.intro init_fin_FWdelay_bisimulation_obs FWdelay_bisimulation_diverge_axioms.intro init_fin_delay_bisimulation_diverge)
end
context FWbisimulation begin
lemma init_fin_simulation1:
assumes "t ⊢ s1 ≈i s2" and "r1.init_fin t s1 tl1 s1'"
shows "∃s2' tl2. r2.init_fin t s2 tl2 s2' ∧ t ⊢ s1' ≈i s2' ∧ ta_bisim init_fin_bisim tl1 tl2"
using init_fin_simulation1[OF assms] by(auto simp add: τmoves_False init_fin_τmoves_False)
lemma init_fin_simulation2:
"⟦ t ⊢ s1 ≈i s2; r2.init_fin t s2 tl2 s2' ⟧
⟹ ∃s1' tl1. r1.init_fin t s1 tl1 s1' ∧ t ⊢ s1' ≈i s2' ∧ ta_bisim init_fin_bisim tl1 tl2"
using FWbisimulation.init_fin_simulation1[OF FWbisimulation_flip]
unfolding flip_simps .
lemma init_fin_bisimulation:
"bisimulation (r1.init_fin t) (r2.init_fin t) (init_fin_bisim t) (ta_bisim init_fin_bisim)"
by(unfold_locales)(erule (1) init_fin_simulation1 init_fin_simulation2)+
lemma init_fin_FWbisimulation:
"FWbisimulation r1.init_fin_final r1.init_fin r2.init_fin_final r2.init_fin init_fin_bisim"
proof(intro FWbisimulation.intro r1.multithreaded_init_fin r2.multithreaded_init_fin FWbisimulation_axioms.intro init_fin_bisimulation)
fix t sx1 m1 sx2 m2
assume "t ⊢ (sx1, m1) ≈i (sx2, m2)"
thus "r1.init_fin_final sx1 = r2.init_fin_final sx2"
by cases simp_all
next
fix t' sx m1 sxx m2 t sx1 sx2 ta1 sx1' m1' ta2 sx2' m2'
assume "t' ⊢ (sx, m1) ≈i (sxx, m2)" "t ⊢ (sx1, m1) ≈i (sx2, m2)"
and "r1.init_fin t (sx1, m1) ta1 (sx1', m1')"
and "r2.init_fin t (sx2, m2) ta2 (sx2', m2')"
and "t ⊢ (sx1', m1') ≈i (sx2', m2')"
and "ta_bisim init_fin_bisim ta1 ta2"
from FWdelay_bisimulation_obs.bisim_inv_red_other
[OF init_fin_FWdelay_bisimulation_obs, OF this(1-2) _ this(3) _ _ this(4) _ this(5-6)]
show "t' ⊢ (sx, m1') ≈i (sxx, m2')" by(simp add: init_fin_τmoves_False)
next
show "(∃sx1. r1.init_fin_final sx1) = (∃sx2. r2.init_fin_final sx2)"
using ex_final1_conv_ex_final2 by(auto)
qed
end
end