Theory Bisimulation
section ‹Various notions of bisimulation›
theory Bisimulation
imports
LTS
begin
type_synonym ('a, 'b) bisim = "'a ⇒ 'b ⇒ bool"
subsection ‹Strong bisimulation›
locale bisimulation_base = r1: trsys trsys1 + r2: trsys trsys2
for trsys1 :: "('s1, 'tl1) trsys" (‹_/ -1-_→/ _› [50,0,50] 60)
and trsys2 :: "('s2, 'tl2) trsys" (‹_/ -2-_→/ _› [50,0,50] 60) +
fixes bisim :: "('s1, 's2) bisim" (‹_/ ≈ _› [50, 50] 60)
and tlsim :: "('tl1, 'tl2) bisim" (‹_/ ∼ _› [50, 50] 60)
begin
notation
r1.Trsys (‹_/ -1-_→*/ _› [50,0,50] 60) and
r2.Trsys (‹_/ -2-_→*/ _› [50,0,50] 60)
notation
r1.inf_step (‹_ -1-_→* ∞› [50, 0] 80) and
r2.inf_step (‹_ -2-_→* ∞› [50, 0] 80)
notation
r1.inf_step_table (‹_ -1-_→*t ∞› [50, 0] 80) and
r2.inf_step_table (‹_ -2-_→*t ∞› [50, 0] 80)
abbreviation Tlsim :: "('tl1 list, 'tl2 list) bisim" (‹_/ [∼] _› [50, 50] 60)
where "Tlsim tl1 tl2 ≡ list_all2 tlsim tl1 tl2"
abbreviation Tlsiml :: "('tl1 llist, 'tl2 llist) bisim" (‹_/ [[∼]] _› [50, 50] 60)
where "Tlsiml tl1 tl2 ≡ llist_all2 tlsim tl1 tl2"
end
locale bisimulation = bisimulation_base +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
assumes simulation1: "⟦ s1 ≈ s2; s1 -1-tl1→ s1' ⟧ ⟹ ∃s2' tl2. s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2"
and simulation2: "⟦ s1 ≈ s2; s2 -2-tl2→ s2' ⟧ ⟹ ∃s1' tl1. s1 -1-tl1→ s1' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2"
begin
lemma bisimulation_flip:
"bisimulation trsys2 trsys1 (flip bisim) (flip tlsim)"
by(unfold_locales)(unfold flip_simps,(blast intro: simulation1 simulation2)+)
end
lemma bisimulation_flip_simps [flip_simps]:
"bisimulation trsys2 trsys1 (flip bisim) (flip tlsim) = bisimulation trsys1 trsys2 bisim tlsim"
by(auto dest: bisimulation.bisimulation_flip simp only: flip_flip)
context bisimulation begin
lemma simulation1_rtrancl:
"⟦s1 -1-tls1→* s1'; s1 ≈ s2⟧
⟹ ∃s2' tls2. s2 -2-tls2→* s2' ∧ s1' ≈ s2' ∧ tls1 [∼] tls2"
proof(induct rule: rtrancl3p.induct)
case rtrancl3p_refl thus ?case by(auto intro: rtrancl3p.rtrancl3p_refl)
next
case (rtrancl3p_step s1 tls1 s1' tl1 s1'')
from ‹s1 ≈ s2 ⟹ ∃s2' tls2. s2 -2-tls2→* s2' ∧ s1' ≈ s2' ∧ tls1 [∼] tls2› ‹s1 ≈ s2›
obtain s2' tls2 where "s2 -2-tls2→* s2'" "s1' ≈ s2'" "tls1 [∼] tls2" by blast
moreover from ‹s1' -1-tl1→ s1''› ‹s1' ≈ s2'›
obtain s2'' tl2 where "s2' -2-tl2→ s2''" "s1'' ≈ s2''" "tl1 ∼ tl2" by(auto dest: simulation1)
ultimately have "s2 -2-tls2 @ [tl2]→* s2''" "tls1 @ [tl1] [∼] tls2 @ [tl2]"
by(auto intro: rtrancl3p.rtrancl3p_step list_all2_appendI)
with ‹s1'' ≈ s2''› show ?case by(blast)
qed
lemma simulation2_rtrancl:
"⟦s2 -2-tls2→* s2'; s1 ≈ s2⟧
⟹ ∃s1' tls1. s1 -1-tls1→* s1' ∧ s1' ≈ s2' ∧ tls1 [∼] tls2"
using bisimulation.simulation1_rtrancl[OF bisimulation_flip]
unfolding flip_simps .
lemma simulation1_inf_step:
assumes red1: "s1 -1-tls1→* ∞" and bisim: "s1 ≈ s2"
shows "∃tls2. s2 -2-tls2→* ∞ ∧ tls1 [[∼]] tls2"
proof -
from r1.inf_step_imp_inf_step_table[OF red1]
obtain stls1 where red1': "s1 -1-stls1→*t ∞"
and tls1: "tls1 = lmap (fst ∘ snd) stls1" by blast
define tl1_to_tl2 where "tl1_to_tl2 s2 stls1 = unfold_llist
(λ(s2, stls1). lnull stls1)
(λ(s2, stls1). let (s1, tl1, s1') = lhd stls1;
(tl2, s2') = SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2
in (s2, tl2, s2'))
(λ(s2, stls1). let (s1, tl1, s1') = lhd stls1;
(tl2, s2') = SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2
in (s2', ltl stls1))
(s2, stls1)"
for s2 :: 's2 and stls1 :: "('s1 × 'tl1 × 's1) llist"
have tl1_to_tl2_simps [simp]:
"⋀s2 stls1. lnull (tl1_to_tl2 s2 stls1) ⟷ lnull stls1"
"⋀s2 stls1. ¬ lnull stls1 ⟹ lhd (tl1_to_tl2 s2 stls1) =
(let (s1, tl1, s1') = lhd stls1;
(tl2, s2') = SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2
in (s2, tl2, s2'))"
"⋀s2 stls1. ¬ lnull stls1 ⟹ ltl (tl1_to_tl2 s2 stls1) =
(let (s1, tl1, s1') = lhd stls1;
(tl2, s2') = SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2
in tl1_to_tl2 s2' (ltl stls1))"
"⋀s2. tl1_to_tl2 s2 LNil = LNil"
"⋀s2 s1 tl1 s1' stls1'. tl1_to_tl2 s2 (LCons (s1, tl1, s1') stls1') =
LCons (s2, SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2)
(tl1_to_tl2 (snd (SOME (tl2, s2'). trsys2 s2 tl2 s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2)) stls1')"
by(simp_all add: tl1_to_tl2_def split_beta)
have [simp]: "llength (tl1_to_tl2 s2 stls1) = llength stls1"
by(coinduction arbitrary: s2 stls1 rule: enat_coinduct)(auto simp add: epred_llength split_beta)
from red1' bisim have "s2 -2-tl1_to_tl2 s2 stls1→*t ∞"
proof(coinduction arbitrary: s2 s1 stls1)
case (inf_step_table s2 s1 stls1)
note red1' = ‹s1 -1-stls1→*t ∞› and bisim = ‹s1 ≈ s2›
from red1' show ?case
proof(cases)
case (inf_step_tableI s1' stls1' tl1)
hence stls1: "stls1 = LCons (s1, tl1, s1') stls1'"
and r: "s1 -1-tl1→ s1'" and reds1: "s1' -1-stls1'→*t ∞" by simp_all
let ?tl2s2' = "SOME (tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2"
let ?tl2 = "fst ?tl2s2'" let ?s2' = "snd ?tl2s2'"
from simulation1[OF bisim r] obtain s2' tl2
where "s2 -2-tl2→ s2'" "s1' ≈ s2'" "tl1 ∼ tl2" by blast
hence "(λ(tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2) (tl2, s2')" by simp
hence "(λ(tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2) ?tl2s2'" by(rule someI)
hence "s2 -2-?tl2→ ?s2'" "s1' ≈ ?s2'" "tl1 ∼ ?tl2" by(simp_all add: split_beta)
then show ?thesis using reds1 stls1 by(fastforce intro: prod_eqI)
qed
qed
hence "s2 -2-lmap (fst ∘ snd) (tl1_to_tl2 s2 stls1)→* ∞"
by(rule r2.inf_step_table_imp_inf_step)
moreover have "tls1 [[∼]] lmap (fst ∘ snd) (tl1_to_tl2 s2 stls1)"
proof(rule llist_all2_all_lnthI)
show "llength tls1 = llength (lmap (fst ∘ snd) (tl1_to_tl2 s2 stls1))"
using tls1 by simp
next
fix n
assume "enat n < llength tls1"
thus "lnth tls1 n ∼ lnth (lmap (fst ∘ snd) (tl1_to_tl2 s2 stls1)) n"
using red1' bisim unfolding tls1
proof(induct n arbitrary: s1 s2 stls1 rule: nat_less_induct)
case (1 n)
hence IH: "⋀m s1 s2 stls1. ⟦ m < n; enat m < llength (lmap (fst ∘ snd) stls1);
s1 -1-stls1→*t ∞; s1 ≈ s2 ⟧
⟹ lnth (lmap (fst ∘ snd) stls1) m ∼ lnth (lmap (fst ∘ snd) (tl1_to_tl2 s2 stls1)) m"
by blast
from ‹s1 -1-stls1→*t ∞› show ?case
proof cases
case (inf_step_tableI s1' stls1' tl1)
hence stls1: "stls1 = LCons (s1, tl1, s1') stls1'"
and r: "s1 -1-tl1→ s1'" and reds: "s1' -1-stls1'→*t ∞" by simp_all
let ?tl2s2' = "SOME (tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2"
let ?tl2 = "fst ?tl2s2'" let ?s2' = "snd ?tl2s2'"
from simulation1[OF ‹s1 ≈ s2› r] obtain s2' tl2
where "s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2" by blast
hence "(λ(tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2) (tl2, s2')" by simp
hence "(λ(tl2, s2'). s2 -2-tl2→ s2' ∧ s1' ≈ s2' ∧ tl1 ∼ tl2) ?tl2s2'" by(rule someI)
hence bisim': "s1' ≈ ?s2'" and tlsim: "tl1 ∼ ?tl2" by(simp_all add: split_beta)
show ?thesis
proof(cases n)
case 0
with stls1 tlsim show ?thesis by simp
next
case (Suc m)
hence "m < n" by simp
moreover have "enat m < llength (lmap (fst ∘ snd) stls1')"
using stls1 ‹enat n < llength (lmap (fst ∘ snd) stls1)› Suc by(simp add: Suc_ile_eq)
ultimately have "lnth (lmap (fst ∘ snd) stls1') m ∼ lnth (lmap (fst ∘ snd) (tl1_to_tl2 ?s2' stls1')) m"
using reds bisim' by(rule IH)
with Suc stls1 show ?thesis by(simp del: o_apply)
qed
qed
qed
qed
ultimately show ?thesis by blast
qed
lemma simulation2_inf_step:
"⟦ s2 -2-tls2→* ∞; s1 ≈ s2 ⟧ ⟹ ∃tls1. s1 -1-tls1→* ∞ ∧ tls1 [[∼]] tls2"
using bisimulation.simulation1_inf_step[OF bisimulation_flip]
unfolding flip_simps .
end
locale bisimulation_final_base =
bisimulation_base +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
fixes final1 :: "'s1 ⇒ bool"
and final2 :: "'s2 ⇒ bool"
locale bisimulation_final = bisimulation_final_base + bisimulation +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and final1 :: "'s1 ⇒ bool"
and final2 :: "'s2 ⇒ bool"
assumes bisim_final: "s1 ≈ s2 ⟹ final1 s1 ⟷ final2 s2"
begin
lemma bisimulation_final_flip:
"bisimulation_final trsys2 trsys1 (flip bisim) (flip tlsim) final2 final1"
apply(intro_locales)
apply(rule bisimulation_flip)
apply(unfold_locales)
by(unfold flip_simps, rule bisim_final[symmetric])
end
lemma bisimulation_final_flip_simps [flip_simps]:
"bisimulation_final trsys2 trsys1 (flip bisim) (flip tlsim) final2 final1 =
bisimulation_final trsys1 trsys2 bisim tlsim final1 final2"
by(auto dest: bisimulation_final.bisimulation_final_flip simp only: flip_flip)
context bisimulation_final begin
lemma final_simulation1:
"⟦ s1 ≈ s2; s1 -1-tls1→* s1'; final1 s1' ⟧
⟹ ∃s2' tls2. s2 -2-tls2→* s2' ∧ s1' ≈ s2' ∧ final2 s2' ∧ tls1 [∼] tls2"
by(auto dest: bisim_final dest!: simulation1_rtrancl)
lemma final_simulation2:
"⟦ s1 ≈ s2; s2 -2-tls2→* s2'; final2 s2' ⟧
⟹ ∃s1' tls1. s1 -1-tls1→* s1' ∧ s1' ≈ s2' ∧ final1 s1' ∧ tls1 [∼] tls2"
by(auto dest: bisim_final dest!: simulation2_rtrancl)
end
subsection ‹Delay bisimulation›
locale delay_bisimulation_base =
bisimulation_base +
trsys1?: τtrsys trsys1 τmove1 +
trsys2?: τtrsys trsys2 τmove2
for τmove1 τmove2 +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
begin
notation
trsys1.silent_move (‹_/ -τ1→ _› [50, 50] 60) and
trsys2.silent_move (‹_/ -τ2→ _› [50, 50] 60)
notation
trsys1.silent_moves (‹_/ -τ1→* _› [50, 50] 60) and
trsys2.silent_moves (‹_/ -τ2→* _› [50, 50] 60)
notation
trsys1.silent_movet (‹_/ -τ1→+ _› [50, 50] 60) and
trsys2.silent_movet (‹_/ -τ2→+ _› [50, 50] 60)
notation
trsys1.τrtrancl3p (‹_ -τ1-_→* _› [50, 0, 50] 60) and
trsys2.τrtrancl3p (‹_ -τ2-_→* _› [50, 0, 50] 60)
notation
trsys1.τinf_step (‹_ -τ1-_→* ∞› [50, 0] 80) and
trsys2.τinf_step (‹_ -τ2-_→* ∞› [50, 0] 80)
notation
trsys1.τdiverge (‹_ -τ1→ ∞› [50] 80) and
trsys2.τdiverge (‹_ -τ2→ ∞› [50] 80)
notation
trsys1.τinf_step_table (‹_ -τ1-_→*t ∞› [50, 0] 80) and
trsys2.τinf_step_table (‹_ -τ2-_→*t ∞› [50, 0] 80)
notation
trsys1.τRuns (‹_ ⇓1 _› [50, 50] 51) and
trsys2.τRuns (‹_ ⇓2 _› [50, 50] 51)
lemma simulation_silent1I':
assumes "∃s2'. (if μ1 s1' s1 then trsys2.silent_moves else trsys2.silent_movet) s2 s2' ∧ s1' ≈ s2'"
shows "s1' ≈ s2 ∧ μ1^++ s1' s1 ∨ (∃s2'. s2 -τ2→+ s2' ∧ s1' ≈ s2')"
proof -
from assms obtain s2' where red: "(if μ1 s1' s1 then trsys2.silent_moves else trsys2.silent_movet) s2 s2'"
and bisim: "s1' ≈ s2'" by blast
show ?thesis
proof(cases "μ1 s1' s1")
case True
with red have "s2 -τ2→* s2'" by simp
thus ?thesis using bisim True by cases(blast intro: rtranclp_into_tranclp1)+
next
case False
with red bisim show ?thesis by auto
qed
qed
lemma simulation_silent2I':
assumes "∃s1'. (if μ2 s2' s2 then trsys1.silent_moves else trsys1.silent_movet) s1 s1' ∧ s1' ≈ s2'"
shows "s1 ≈ s2' ∧ μ2^++ s2' s2 ∨ (∃s1'. s1 -τ1→+ s1' ∧ s1' ≈ s2')"
using assms
by(rule delay_bisimulation_base.simulation_silent1I')
end
locale delay_bisimulation_obs = delay_bisimulation_base _ _ _ _ τmove1 τmove2
for τmove1 :: "'s1 ⇒ 'tl1 ⇒ 's1 ⇒ bool"
and τmove2 :: "'s2 ⇒ 'tl2 ⇒ 's2 ⇒ bool" +
assumes simulation1:
"⟦ s1 ≈ s2; s1 -1-tl1→ s1'; ¬ τmove1 s1 tl1 s1' ⟧
⟹ ∃s2' s2'' tl2. s2 -τ2→* s2' ∧ s2' -2-tl2→ s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ s1' ≈ s2'' ∧ tl1 ∼ tl2"
and simulation2:
"⟦ s1 ≈ s2; s2 -2-tl2→ s2'; ¬ τmove2 s2 tl2 s2' ⟧
⟹ ∃s1' s1'' tl1. s1 -τ1→* s1' ∧ s1' -1-tl1→ s1'' ∧ ¬ τmove1 s1' tl1 s1'' ∧ s1'' ≈ s2' ∧ tl1 ∼ tl2"
begin
lemma delay_bisimulation_obs_flip: "delay_bisimulation_obs trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1"
apply(unfold_locales)
apply(unfold flip_simps)
by(blast intro: simulation1 simulation2)+
end
lemma delay_bisimulation_obs_flip_simps [flip_simps]:
"delay_bisimulation_obs trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 =
delay_bisimulation_obs trsys1 trsys2 bisim tlsim τmove1 τmove2"
by(auto dest: delay_bisimulation_obs.delay_bisimulation_obs_flip simp only: flip_flip)
locale delay_bisimulation_diverge = delay_bisimulation_obs _ _ _ _ τmove1 τmove2
for τmove1 :: "'s1 ⇒ 'tl1 ⇒ 's1 ⇒ bool"
and τmove2 :: "'s2 ⇒ 'tl2 ⇒ 's2 ⇒ bool" +
assumes simulation_silent1:
"⟦ s1 ≈ s2; s1 -τ1→ s1' ⟧ ⟹ ∃s2'. s2 -τ2→* s2' ∧ s1' ≈ s2'"
and simulation_silent2:
"⟦ s1 ≈ s2; s2 -τ2→ s2' ⟧ ⟹ ∃s1'. s1 -τ1→* s1' ∧ s1' ≈ s2'"
and τdiverge_bisim_inv: "s1 ≈ s2 ⟹ s1 -τ1→ ∞ ⟷ s2 -τ2→ ∞"
begin
lemma delay_bisimulation_diverge_flip: "delay_bisimulation_diverge trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1"
apply(rule delay_bisimulation_diverge.intro)
apply(rule delay_bisimulation_obs_flip)
apply(unfold_locales)
apply(unfold flip_simps)
by(blast intro: simulation_silent1 simulation_silent2 τdiverge_bisim_inv[symmetric] del: iffI)+
end
lemma delay_bisimulation_diverge_flip_simps [flip_simps]:
"delay_bisimulation_diverge trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 =
delay_bisimulation_diverge trsys1 trsys2 bisim tlsim τmove1 τmove2"
by(auto dest: delay_bisimulation_diverge.delay_bisimulation_diverge_flip simp only: flip_flip)
context delay_bisimulation_diverge begin
lemma simulation_silents1:
assumes bisim: "s1 ≈ s2" and moves: "s1 -τ1→* s1'"
shows "∃s2'. s2 -τ2→* s2' ∧ s1' ≈ s2'"
using moves bisim
proof induct
case base thus ?case by(blast)
next
case (step s1' s1'')
from ‹s1 ≈ s2 ⟹ ∃s2'. s2 -τ2→* s2' ∧ s1' ≈ s2'› ‹s1 ≈ s2›
obtain s2' where "s2 -τ2→* s2'" "s1' ≈ s2'" by blast
from simulation_silent1[OF ‹s1' ≈ s2'› ‹s1' -τ1→ s1''›]
obtain s2'' where "s2' -τ2→* s2''" "s1'' ≈ s2''" by blast
from ‹s2 -τ2→* s2'› ‹s2' -τ2→* s2''› have "s2 -τ2→* s2''" by(rule rtranclp_trans)
with ‹s1'' ≈ s2''› show ?case by blast
qed
lemma simulation_silents2:
"⟦ s1 ≈ s2; s2 -τ2→* s2' ⟧ ⟹ ∃s1'. s1 -τ1→* s1' ∧ s1' ≈ s2'"
using delay_bisimulation_diverge.simulation_silents1[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma simulation1_τrtrancl3p:
"⟦ s1 -τ1-tls1→* s1'; s1 ≈ s2 ⟧
⟹ ∃tls2 s2'. s2 -τ2-tls2→* s2' ∧ s1' ≈ s2' ∧ tls1 [∼] tls2"
proof(induct arbitrary: s2 rule: trsys1.τrtrancl3p.induct)
case (τrtrancl3p_refl s)
thus ?case by(auto intro: τtrsys.τrtrancl3p.intros)
next
case (τrtrancl3p_step s1 s1' tls1 s1'' tl1)
from simulation1[OF ‹s1 ≈ s2› ‹s1 -1-tl1→ s1'› ‹¬ τmove1 s1 tl1 s1'›]
obtain s2' s2'' tl2 where τred: "s2 -τ2→* s2'"
and red: "s2' -2-tl2→ s2''" and nτ: "¬ τmove2 s2' tl2 s2''"
and bisim': "s1' ≈ s2''" and tlsim: "tl1 ∼ tl2" by blast
from bisim' ‹s1' ≈ s2'' ⟹ ∃tls2 s2'. s2'' -τ2-tls2→* s2' ∧ s1'' ≈ s2' ∧ tls1 [∼] tls2›
obtain tls2 s2''' where IH: "s2'' -τ2-tls2→* s2'''" "s1'' ≈ s2'''" "tls1 [∼] tls2" by blast
from τred have "s2 -τ2-[]→* s2'" by(rule trsys2.silent_moves_into_τrtrancl3p)
also from red nτ IH(1) have "s2' -τ2-tl2 # tls2→* s2'''" by(rule τrtrancl3p.τrtrancl3p_step)
finally show ?case using IH tlsim by fastforce
next
case (τrtrancl3p_τstep s1 s1' tls1 s1'' tl1)
from ‹s1 -1-tl1→ s1'› ‹τmove1 s1 tl1 s1'› have "s1 -τ1→ s1'" ..
from simulation_silent1[OF ‹s1 ≈ s2› this]
obtain s2' where τred: "s2 -τ2→* s2'" and bisim': "s1' ≈ s2'" by blast
from τred have "s2 -τ2-[]→* s2'" by(rule trsys2.silent_moves_into_τrtrancl3p)
also from bisim' ‹s1' ≈ s2' ⟹ ∃tls2 s2''. s2' -τ2-tls2→* s2'' ∧ s1'' ≈ s2'' ∧ tls1 [∼] tls2›
obtain tls2 s2'' where IH: "s2' -τ2-tls2→* s2''" "s1'' ≈ s2''" "tls1 [∼] tls2" by blast
note ‹s2' -τ2-tls2→* s2''›
finally show ?case using IH by auto
qed
lemma simulation2_τrtrancl3p:
"⟦ s2 -τ2-tls2→* s2'; s1 ≈ s2 ⟧
⟹ ∃tls1 s1'. s1 -τ1-tls1→* s1' ∧ s1' ≈ s2' ∧ tls1 [∼] tls2"
using delay_bisimulation_diverge.simulation1_τrtrancl3p[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma simulation1_τinf_step:
assumes τinf1: "s1 -τ1-tls1→* ∞" and bisim: "s1 ≈ s2"
shows "∃tls2. s2 -τ2-tls2→* ∞ ∧ tls1 [[∼]] tls2"
proof -
from trsys1.τinf_step_imp_τinf_step_table[OF τinf1]
obtain sstls1 where τinf1': "s1 -τ1-sstls1→*t ∞"
and tls1: "tls1 = lmap (fst ∘ snd ∘ snd) sstls1" by blast
define tl1_to_tl2 where "tl1_to_tl2 s2 sstls1 = unfold_llist
(λ(s2, sstls1). lnull sstls1)
(λ(s2, sstls1).
let (s1, s1', tl1, s1'') = lhd sstls1;
(s2', tl2, s2'') = SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2
in (s2, s2', tl2, s2''))
(λ(s2, sstls1).
let (s1, s1', tl1, s1'') = lhd sstls1;
(s2', tl2, s2'') = SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2
in (s2'', ltl sstls1))
(s2, sstls1)"
for s2 :: 's2 and sstls1 :: "('s1 × 's1 × 'tl1 × 's1) llist"
have [simp]:
"⋀s2 sstls1. lnull (tl1_to_tl2 s2 sstls1) ⟷ lnull sstls1"
"⋀s2 sstls1. ¬ lnull sstls1 ⟹ lhd (tl1_to_tl2 s2 sstls1) =
(let (s1, s1', tl1, s1'') = lhd sstls1;
(s2', tl2, s2'') = SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2
in (s2, s2', tl2, s2''))"
"⋀s2 sstls1. ¬ lnull sstls1 ⟹ ltl (tl1_to_tl2 s2 sstls1) =
(let (s1, s1', tl1, s1'') = lhd sstls1;
(s2', tl2, s2'') = SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2
in tl1_to_tl2 s2'' (ltl sstls1))"
"⋀s2. tl1_to_tl2 s2 LNil = LNil"
"⋀s2 s1 s1' tl1 s1'' stls1'. tl1_to_tl2 s2 (LCons (s1, s1', tl1, s1'') stls1') =
LCons (s2, SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2)
(tl1_to_tl2 (snd (snd (SOME (s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2)))
stls1')"
by(simp_all add: tl1_to_tl2_def split_beta)
have [simp]: "llength (tl1_to_tl2 s2 sstls1) = llength sstls1"
by(coinduction arbitrary: s2 sstls1 rule: enat_coinduct)(auto simp add: epred_llength split_beta)
define sstls2 where "sstls2 = tl1_to_tl2 s2 sstls1"
with τinf1' bisim have "∃s1 sstls1. s1 -τ1-sstls1→*t ∞ ∧ sstls2 = tl1_to_tl2 s2 sstls1 ∧ s1 ≈ s2" by blast
from τinf1' bisim have "s2 -τ2-tl1_to_tl2 s2 sstls1→*t ∞"
proof(coinduction arbitrary: s2 s1 sstls1)
case (τinf_step_table s2 s1 sstls1)
note τinf' = ‹s1 -τ1-sstls1→*t ∞› and bisim = ‹s1 ≈ s2›
from τinf' show ?case
proof(cases)
case (τinf_step_table_Cons s1' s1'' sstls1' tl1)
hence sstls1: "sstls1 = LCons (s1, s1', tl1, s1'') sstls1'"
and τs: "s1 -τ1→* s1'" and r: "s1' -1-tl1→ s1''" and nτ: "¬ τmove1 s1' tl1 s1''"
and reds1: "s1'' -τ1-sstls1'→*t ∞" by simp_all
let ?P = "λ(s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2"
let ?s2tl2s2' = "Eps ?P"
let ?s2'' = "snd (snd ?s2tl2s2')"
from simulation_silents1[OF ‹s1 ≈ s2› τs]
obtain s2' where "s2 -τ2→* s2'" "s1' ≈ s2'" by blast
from simulation1[OF ‹s1' ≈ s2'› r nτ] obtain s2'' s2''' tl2
where "s2' -τ2→* s2''"
and rest: "s2'' -2-tl2→ s2'''" "¬ τmove2 s2'' tl2 s2'''" "s1'' ≈ s2'''" "tl1 ∼ tl2" by blast
from ‹s2 -τ2→* s2'› ‹s2' -τ2→* s2''› have "s2 -τ2→* s2''" by(rule rtranclp_trans)
with rest have "?P (s2'', tl2, s2''')" by simp
hence "?P ?s2tl2s2'" by(rule someI)
then show ?thesis using reds1 sstls1 by fastforce
next
case τinf_step_table_Nil
hence [simp]: "sstls1 = LNil" and "s1 -τ1→ ∞" by simp_all
from ‹s1 -τ1→ ∞› ‹s1 ≈ s2› have "s2 -τ2→ ∞" by(simp add: τdiverge_bisim_inv)
thus ?thesis using sstls2_def by simp
qed
qed
hence "s2 -τ2-lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 s2 sstls1)→* ∞"
by(rule trsys2.τinf_step_table_into_τinf_step)
moreover have "tls1 [[∼]] lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 s2 sstls1)"
proof(rule llist_all2_all_lnthI)
show "llength tls1 = llength (lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 s2 sstls1))"
using tls1 by simp
next
fix n
assume "enat n < llength tls1"
thus "lnth tls1 n ∼ lnth (lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 s2 sstls1)) n"
using τinf1' bisim unfolding tls1
proof(induct n arbitrary: s1 s2 sstls1 rule: less_induct)
case (less n)
note IH = ‹⋀m s1 s2 sstls1. ⟦ m < n; enat m < llength (lmap (fst ∘ snd ∘ snd) sstls1);
s1 -τ1-sstls1→*t ∞; s1 ≈ s2 ⟧
⟹ lnth (lmap (fst ∘ snd ∘ snd) sstls1) m ∼ lnth (lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 s2 sstls1)) m›
from ‹s1 -τ1-sstls1→*t ∞› show ?case
proof cases
case (τinf_step_table_Cons s1' s1'' sstls1' tl1)
hence sstls1: "sstls1 = LCons (s1, s1', tl1, s1'') sstls1'"
and τs: "s1 -τ1→* s1'" and r: "s1' -1-tl1→ s1''"
and nτ: "¬ τmove1 s1' tl1 s1''" and reds: "s1'' -τ1-sstls1'→*t ∞" by simp_all
let ?P = "λ(s2', tl2, s2''). s2 -τ2→* s2' ∧ trsys2 s2' tl2 s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2"
let ?s2tl2s2' = "Eps ?P" let ?tl2 = "fst (snd ?s2tl2s2')" let ?s2'' = "snd (snd ?s2tl2s2')"
from simulation_silents1[OF ‹s1 ≈ s2› τs] obtain s2'
where "s2 -τ2→* s2'" "s1' ≈ s2'" by blast
from simulation1[OF ‹s1' ≈ s2'› r nτ] obtain s2'' s2''' tl2
where "s2' -τ2→* s2''"
and rest: "s2'' -2-tl2→ s2'''" "¬ τmove2 s2'' tl2 s2'''" "s1'' ≈ s2'''" "tl1 ∼ tl2" by blast
from ‹s2 -τ2→* s2'› ‹s2' -τ2→* s2''› have "s2 -τ2→* s2''" by(rule rtranclp_trans)
with rest have "?P (s2'', tl2, s2''')" by auto
hence "?P ?s2tl2s2'" by(rule someI)
hence "s1'' ≈ ?s2''" "tl1 ∼ ?tl2" by(simp_all add: split_beta)
show ?thesis
proof(cases n)
case 0
with sstls1 ‹tl1 ∼ ?tl2› show ?thesis by simp
next
case (Suc m)
hence "m < n" by simp
moreover have "enat m < llength (lmap (fst ∘ snd ∘ snd) sstls1')"
using sstls1 ‹enat n < llength (lmap (fst ∘ snd ∘ snd) sstls1)› Suc by(simp add: Suc_ile_eq)
ultimately have "lnth (lmap (fst ∘ snd ∘ snd) sstls1') m ∼ lnth (lmap (fst ∘ snd ∘ snd) (tl1_to_tl2 ?s2'' sstls1')) m"
using reds ‹s1'' ≈ ?s2''› by(rule IH)
with Suc sstls1 show ?thesis by(simp del: o_apply)
qed
next
case τinf_step_table_Nil
with ‹enat n < llength (lmap (fst ∘ snd ∘ snd) sstls1)› have False by simp
thus ?thesis ..
qed
qed
qed
ultimately show ?thesis by blast
qed
lemma simulation2_τinf_step:
"⟦ s2 -τ2-tls2→* ∞; s1 ≈ s2 ⟧ ⟹ ∃tls1. s1 -τ1-tls1→* ∞ ∧ tls1 [[∼]] tls2"
using delay_bisimulation_diverge.simulation1_τinf_step[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma no_τmove1_τs_to_no_τmove2:
assumes "s1 ≈ s2"
and no_τmoves1: "⋀s1'. ¬ s1 -τ1→ s1'"
shows "∃s2'. s2 -τ2→* s2' ∧ (∀s2''. ¬ s2' -τ2→ s2'') ∧ s1 ≈ s2'"
proof -
have "¬ s1 -τ1→ ∞"
proof
assume "s1 -τ1→ ∞"
then obtain s1' where "s1 -τ1→ s1'" by cases
with no_τmoves1[of s1'] show False by contradiction
qed
with ‹s1 ≈ s2› have "¬ s2 -τ2→ ∞" by(simp add: τdiverge_bisim_inv)
from trsys2.not_τdiverge_to_no_τmove[OF this]
obtain s2' where "s2 -τ2→* s2'" and "⋀s2''. ¬ s2' -τ2→ s2''" by blast
moreover from simulation_silents2[OF ‹s1 ≈ s2› ‹s2 -τ2→* s2'›]
obtain s1' where "s1 -τ1→* s1'" and "s1' ≈ s2'" by blast
from ‹s1 -τ1→* s1'› no_τmoves1 have "s1' = s1"
by(auto elim: converse_rtranclpE)
ultimately show ?thesis using ‹s1' ≈ s2'› by blast
qed
lemma no_τmove2_τs_to_no_τmove1:
"⟦ s1 ≈ s2; ⋀s2'. ¬ s2 -τ2→ s2' ⟧ ⟹ ∃s1'. s1 -τ1→* s1' ∧ (∀s1''. ¬ s1' -τ1→ s1'') ∧ s1' ≈ s2"
using delay_bisimulation_diverge.no_τmove1_τs_to_no_τmove2[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma no_move1_to_no_move2:
assumes "s1 ≈ s2"
and no_moves1: "⋀tl1 s1'. ¬ s1 -1-tl1→ s1'"
shows "∃s2'. s2 -τ2→* s2' ∧ (∀tl2 s2''. ¬ s2' -2-tl2→ s2'') ∧ s1 ≈ s2'"
proof -
from no_moves1 have "⋀s1'. ¬ s1 -τ1→ s1'" by(auto)
from no_τmove1_τs_to_no_τmove2[OF ‹s1 ≈ s2› this]
obtain s2' where "s2 -τ2→* s2'" and "s1 ≈ s2'"
and no_τmoves2: "⋀s2''. ¬ s2' -τ2→ s2''" by blast
moreover
have "⋀tl2 s2''. ¬ s2' -2-tl2→ s2''"
proof
fix tl2 s2''
assume "s2' -2-tl2→ s2''"
with no_τmoves2[of s2''] have "¬ τmove2 s2' tl2 s2''" by(auto)
from simulation2[OF ‹s1 ≈ s2'› ‹s2' -2-tl2→ s2''› this]
obtain s1' s1'' tl1 where "s1 -τ1→* s1'" and "s1' -1-tl1→ s1''" by blast
with no_moves1 show False by(fastforce elim: converse_rtranclpE)
qed
ultimately show ?thesis by blast
qed
lemma no_move2_to_no_move1:
"⟦ s1 ≈ s2; ⋀tl2 s2'. ¬ s2 -2-tl2→ s2' ⟧
⟹ ∃s1'. s1 -τ1→* s1' ∧ (∀tl1 s1''. ¬ s1' -1-tl1→ s1'') ∧ s1' ≈ s2"
using delay_bisimulation_diverge.no_move1_to_no_move2[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
lemma simulation_τRuns_table1:
assumes bisim: "s1 ≈ s2"
and run1: "trsys1.τRuns_table s1 stlsss1"
shows "∃stlsss2. trsys2.τRuns_table s2 stlsss2 ∧ tllist_all2 (λ(tl1, s1'') (tl2, s2''). tl1 ∼ tl2 ∧ s1'' ≈ s2'') (rel_option bisim) stlsss1 stlsss2"
proof(intro exI conjI)
let ?P = "λ(s2 :: 's2) (stlsss1 :: ('tl1 × 's1, 's1 option) tllist) (tl2, s2'').
∃s2'. s2 -τ2→* s2' ∧ s2' -2-tl2→ s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ snd (thd stlsss1) ≈ s2'' ∧ fst (thd stlsss1) ∼ tl2"
define tls1_to_tls2 where "tls1_to_tls2 s2 stlsss1 = unfold_tllist
(λ(s2, stlsss1). is_TNil stlsss1)
(λ(s2, stlsss1). map_option (λs1'. SOME s2'. s2 -τ2→* s2' ∧ (∀tl s2''. ¬ s2' -2-tl→ s2'') ∧ s1' ≈ s2') (terminal stlsss1))
(λ(s2, stlsss1). let (tl2, s2'') = Eps (?P s2 stlsss1) in (tl2, s2''))
(λ(s2, stlsss1). let (tl2, s2'') = Eps (?P s2 stlsss1) in (s2'', ttl stlsss1))
(s2, stlsss1)"
for s2 stlsss1
have [simp]:
"⋀s2 stlsss1. is_TNil (tls1_to_tls2 s2 stlsss1) ⟷ is_TNil stlsss1"
"⋀s2 stlsss1. is_TNil stlsss1 ⟹ terminal (tls1_to_tls2 s2 stlsss1) = map_option (λs1'. SOME s2'. s2 -τ2→* s2' ∧ (∀tl s2''. ¬ s2' -2-tl→ s2'') ∧ s1' ≈ s2') (terminal stlsss1)"
"⋀s2 stlsss1. ¬ is_TNil stlsss1 ⟹ thd (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = Eps (?P s2 stlsss1) in (tl2, s2''))"
"⋀s2 stlsss1. ¬ is_TNil stlsss1 ⟹ ttl (tls1_to_tls2 s2 stlsss1) = (let (tl2, s2'') = Eps (?P s2 stlsss1) in tls1_to_tls2 s2'' (ttl stlsss1))"
"⋀s2 os1. tls1_to_tls2 s2 (TNil os1) =
TNil (map_option (λs1'. SOME s2'. s2 -τ2→* s2' ∧ (∀tl s2''. ¬ s2' -2-tl→ s2'') ∧ s1' ≈ s2') os1)"
by(simp_all add: tls1_to_tls2_def split_beta)
have [simp]:
"⋀s2 s1 s1' tl1 s1'' stlsss1.
tls1_to_tls2 s2 (TCons (tl1, s1'') stlsss1) =
(let (tl2, s2'') = SOME (tl2, s2''). ∃s2'. s2 -τ2→* s2' ∧ s2' -2-tl2→ s2'' ∧
¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2
in TCons (tl2, s2'') (tls1_to_tls2 s2'' stlsss1))"
by(rule tllist.expand)(simp_all add: split_beta)
from bisim run1
show "trsys2.τRuns_table s2 (tls1_to_tls2 s2 stlsss1)"
proof(coinduction arbitrary: s2 s1 stlsss1)
case (τRuns_table s2 s1 stlsss1)
note bisim = ‹s1 ≈ s2›
and run1 = ‹trsys1.τRuns_table s1 stlsss1›
from run1 show ?case
proof cases
case (Terminate s1')
let ?P = "λs2'. s2 -τ2→* s2' ∧ (∀tl2 s2''. ¬ s2' -2-tl2→ s2'') ∧ s1' ≈ s2'"
from simulation_silents1[OF bisim ‹s1 -τ1→* s1'›]
obtain s2' where "s2 -τ2→* s2'" and "s1' ≈ s2'" by blast
moreover from no_move1_to_no_move2[OF ‹s1' ≈ s2'› ‹⋀tl1 s1''. ¬ s1' -1-tl1→ s1''›]
obtain s2'' where "s2' -τ2→* s2''" and "s1' ≈ s2''"
and "⋀tl2 s2'''. ¬ s2'' -2-tl2→ s2'''" by blast
ultimately have "?P s2''" by(blast intro: rtranclp_trans)
hence "?P (Eps ?P)" by(rule someI)
hence ?Terminate using ‹stlsss1 = TNil ⌊s1'⌋› by simp
thus ?thesis ..
next
case Diverge
with τdiverge_bisim_inv[OF bisim]
have ?Diverge by simp
thus ?thesis by simp
next
case (Proceed s1' s1'' stlsss1' tl1)
let ?P = "λ(tl2, s2''). ∃s2'. s2 -τ2→* s2' ∧ s2' -2-tl2→ s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ s1'' ≈ s2'' ∧ tl1 ∼ tl2"
from simulation_silents1[OF bisim ‹s1 -τ1→* s1'›]
obtain s2' where "s2 -τ2→* s2'" and "s1' ≈ s2'" by blast
moreover from simulation1[OF ‹s1' ≈ s2'› ‹s1' -1-tl1→ s1''› ‹¬ τmove1 s1' tl1 s1''›]
obtain s2'' s2''' tl2 where "s2' -τ2→* s2''"
and "s2'' -2-tl2→ s2'''" and "¬ τmove2 s2'' tl2 s2'''"
and "s1'' ≈ s2'''" and "tl1 ∼ tl2" by blast
ultimately have "?P (tl2, s2''')" by(blast intro: rtranclp_trans)
hence "?P (Eps ?P)" by(rule someI)
hence ?Proceed
using ‹stlsss1 = TCons (tl1, s1'') stlsss1'› ‹trsys1.τRuns_table s1'' stlsss1'›
by auto blast
thus ?thesis by simp
qed
qed
let ?Tlsim = "λ(tl1, s1'') (tl2, s2''). tl1 ∼ tl2 ∧ s1'' ≈ s2''"
let ?Bisim = "rel_option bisim"
from run1 bisim
show "tllist_all2 ?Tlsim ?Bisim stlsss1 (tls1_to_tls2 s2 stlsss1)"
proof(coinduction arbitrary: s1 s2 stlsss1)
case (tllist_all2 s1 s2 stlsss1)
note Runs = ‹trsys1.τRuns_table s1 stlsss1› and bisim = ‹s1 ≈ s2›
from Runs show ?case
proof cases
case (Terminate s1')
let ?P = "λs2'. s2 -τ2→* s2' ∧ (∀tl2 s2''. ¬ s2' -2-tl2→ s2'') ∧ s1' ≈ s2'"
from simulation_silents1[OF bisim ‹s1 -τ1→* s1'›]
obtain s2' where "s2 -τ2→* s2'" and "s1' ≈ s2'" by blast
moreover
from no_move1_to_no_move2[OF ‹s1' ≈ s2'› ‹⋀tl1 s1''. ¬ s1' -1-tl1→ s1''›]
obtain s2'' where "s2' -τ2→* s2''" and "s1' ≈ s2''"
and "⋀tl2 s2'''. ¬ s2'' -2-tl2→ s2'''" by blast
ultimately have "?P s2''" by(blast intro: rtranclp_trans)
hence "?P (Eps ?P)" by(rule someI)
thus ?thesis using ‹stlsss1 = TNil ⌊s1'⌋› bisim by(simp)
next
case (Proceed s1' s1'' stlsss1' tl1)
from simulation_silents1[OF bisim ‹s1 -τ1→* s1'›]
obtain s2' where "s2 -τ2→* s2'" and "s1' ≈ s2'" by blast
moreover from simulation1[OF ‹s1' ≈ s2'› ‹s1' -1-tl1→ s1''› ‹¬ τmove1 s1' tl1 s1''›]
obtain s2'' s2''' tl2 where "s2' -τ2→* s2''"
and "s2'' -2-tl2→ s2'''" and "¬ τmove2 s2'' tl2 s2'''"
and "s1'' ≈ s2'''" and "tl1 ∼ tl2" by blast
ultimately have "?P s2 stlsss1 (tl2, s2''')"
using ‹stlsss1 = TCons (tl1, s1'') stlsss1'› by(auto intro: rtranclp_trans)
hence "?P s2 stlsss1 (Eps (?P s2 stlsss1))" by(rule someI)
thus ?thesis using ‹stlsss1 = TCons (tl1, s1'') stlsss1'› ‹trsys1.τRuns_table s1'' stlsss1'› bisim
by auto blast
qed simp
qed
qed
lemma simulation_τRuns_table2:
assumes "s1 ≈ s2"
and "trsys2.τRuns_table s2 stlsss2"
shows "∃stlsss1. trsys1.τRuns_table s1 stlsss1 ∧ tllist_all2 (λ(tl1, s1'') (tl2, s2''). tl1 ∼ tl2 ∧ s1'' ≈ s2'') (rel_option bisim) stlsss1 stlsss2"
using delay_bisimulation_diverge.simulation_τRuns_table1[OF delay_bisimulation_diverge_flip, unfolded flip_simps, OF assms]
by(subst tllist_all2_flip[symmetric])(simp only: flip_def split_def)
lemma simulation_τRuns1:
assumes bisim: "s1 ≈ s2"
and run1: "s1 ⇓1 tls1"
shows "∃tls2. s2 ⇓2 tls2 ∧ tllist_all2 tlsim (rel_option bisim) tls1 tls2"
proof -
from trsys1.τRuns_into_τRuns_table[OF run1]
obtain stlsss1 where tls1: "tls1 = tmap fst id stlsss1"
and τRuns1: "trsys1.τRuns_table s1 stlsss1" by blast
from simulation_τRuns_table1[OF bisim τRuns1]
obtain stlsss2 where τRuns2: "trsys2.τRuns_table s2 stlsss2"
and tlsim: "tllist_all2 (λ(tl1, s1'') (tl2, s2''). tl1 ∼ tl2 ∧ s1'' ≈ s2'')
(rel_option bisim) stlsss1 stlsss2" by blast
from τRuns2 have "s2 ⇓2 tmap fst id stlsss2"
by(rule τRuns_table_into_τRuns)
moreover have "tllist_all2 tlsim (rel_option bisim) tls1 (tmap fst id stlsss2)"
using tlsim unfolding tls1
by(fastforce simp add: tllist_all2_tmap1 tllist_all2_tmap2 elim: tllist_all2_mono rel_option_mono)
ultimately show ?thesis by blast
qed
lemma simulation_τRuns2:
"⟦ s1 ≈ s2; s2 ⇓2 tls2 ⟧
⟹ ∃tls1. s1 ⇓1 tls1 ∧ tllist_all2 tlsim (rel_option bisim) tls1 tls2"
using delay_bisimulation_diverge.simulation_τRuns1[OF delay_bisimulation_diverge_flip]
unfolding flip_simps .
end
locale delay_bisimulation_final_base =
delay_bisimulation_base _ _ _ _ τmove1 τmove2 +
bisimulation_final_base _ _ _ _ final1 final2
for τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
and final1 :: "'s1 ⇒ bool"
and final2 :: "'s2 ⇒ bool" +
assumes final1_simulation: "⟦ s1 ≈ s2; final1 s1 ⟧ ⟹ ∃s2'. s2 -τ2→* s2' ∧ s1 ≈ s2' ∧ final2 s2'"
and final2_simulation: "⟦ s1 ≈ s2; final2 s2 ⟧ ⟹ ∃s1'. s1 -τ1→* s1' ∧ s1' ≈ s2 ∧ final1 s1'"
begin
lemma delay_bisimulation_final_base_flip:
"delay_bisimulation_final_base trsys2 trsys1 (flip bisim) τmove2 τmove1 final2 final1"
apply(unfold_locales)
apply(unfold flip_simps)
by(blast intro: final1_simulation final2_simulation)+
end
lemma delay_bisimulation_final_base_flip_simps [flip_simps]:
"delay_bisimulation_final_base trsys2 trsys1 (flip bisim) τmove2 τmove1 final2 final1 =
delay_bisimulation_final_base trsys1 trsys2 bisim τmove1 τmove2 final1 final2"
by(auto dest: delay_bisimulation_final_base.delay_bisimulation_final_base_flip simp only: flip_flip)
context delay_bisimulation_final_base begin
lemma τRuns_terminate_final1:
assumes "s1 ⇓1 tls1"
and "s2 ⇓2 tls2"
and "tllist_all2 tlsim (rel_option bisim) tls1 tls2"
and "tfinite tls1"
and "terminal tls1 = Some s1'"
and "final1 s1'"
shows "∃s2'. tfinite tls2 ∧ terminal tls2 = Some s2' ∧ final2 s2'"
using assms(4) assms(1-3,5-)
apply(induct arbitrary: tls2 s1 s2 rule: tfinite_induct)
apply(auto 4 4 simp add: tllist_all2_TCons1 tllist_all2_TNil1 option_rel_Some1 trsys1.τRuns_simps trsys2.τRuns_simps dest: final1_simulation elim: converse_rtranclpE)
done
lemma τRuns_terminate_final2:
"⟦ s1 ⇓1 tls1; s2 ⇓2 tls2; tllist_all2 tlsim (rel_option bisim) tls1 tls2;
tfinite tls2; terminal tls2 = Some s2'; final2 s2' ⟧
⟹ ∃s1'. tfinite tls1 ∧ terminal tls1 = Some s1' ∧ final1 s1'"
using delay_bisimulation_final_base.τRuns_terminate_final1[where tlsim = "flip tlsim", OF delay_bisimulation_final_base_flip]
unfolding flip_simps by -
end
locale delay_bisimulation_diverge_final =
delay_bisimulation_diverge +
delay_bisimulation_final_base +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
and final1 :: "'s1 ⇒ bool"
and final2 :: "'s2 ⇒ bool"
begin
lemma delay_bisimulation_diverge_final_flip:
"delay_bisimulation_diverge_final trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 final2 final1"
apply(rule delay_bisimulation_diverge_final.intro)
apply(rule delay_bisimulation_diverge_flip)
apply(unfold_locales, unfold flip_simps)
apply(blast intro: final1_simulation final2_simulation)+
done
end
lemma delay_bisimulation_diverge_final_flip_simps [flip_simps]:
"delay_bisimulation_diverge_final trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 final2 final1 =
delay_bisimulation_diverge_final trsys1 trsys2 bisim tlsim τmove1 τmove2 final1 final2"
by(auto dest: delay_bisimulation_diverge_final.delay_bisimulation_diverge_final_flip simp only: flip_flip)
context delay_bisimulation_diverge_final begin
lemma delay_bisimulation_diverge:
"delay_bisimulation_diverge trsys1 trsys2 bisim tlsim τmove1 τmove2"
by(unfold_locales)
lemma delay_bisimulation_final_base:
"delay_bisimulation_final_base trsys1 trsys2 bisim τmove1 τmove2 final1 final2"
by(unfold_locales)
lemma final_simulation1:
"⟦ s1 ≈ s2; s1 -τ1-tls1→* s1'; final1 s1' ⟧
⟹ ∃s2' tls2. s2 -τ2-tls2→* s2' ∧ s1' ≈ s2' ∧ final2 s2' ∧ tls1 [∼] tls2"
by(blast dest: simulation1_τrtrancl3p final1_simulation intro: τrtrancl3p_trans[OF _ silent_moves_into_τrtrancl3p, simplified])
lemma final_simulation2:
"⟦ s1 ≈ s2; s2 -τ2-tls2→* s2'; final2 s2' ⟧
⟹ ∃s1' tls1. s1 -τ1-tls1→* s1' ∧ s1' ≈ s2' ∧ final1 s1' ∧ tls1 [∼] tls2"
by(rule delay_bisimulation_diverge_final.final_simulation1[OF delay_bisimulation_diverge_final_flip, unfolded flip_simps])
end
locale delay_bisimulation_measure_base =
delay_bisimulation_base +
constrains trsys1 :: "'s1 ⇒ 'tl1 ⇒ 's1 ⇒ bool"
and trsys2 :: "'s2 ⇒ 'tl2 ⇒ 's2 ⇒ bool"
and bisim :: "'s1 ⇒ 's2 ⇒ bool"
and tlsim :: "'tl1 ⇒ 'tl2 ⇒ bool"
and τmove1 :: "'s1 ⇒ 'tl1 ⇒ 's1 ⇒ bool"
and τmove2 :: "'s2 ⇒ 'tl2 ⇒ 's2 ⇒ bool"
fixes μ1 :: "'s1 ⇒ 's1 ⇒ bool"
and μ2 :: "'s2 ⇒ 's2 ⇒ bool"
locale delay_bisimulation_measure =
delay_bisimulation_measure_base _ _ _ _ τmove1 τmove2 μ1 μ2 +
delay_bisimulation_obs trsys1 trsys2 bisim tlsim τmove1 τmove2
for τmove1 :: "'s1 ⇒ 'tl1 ⇒ 's1 ⇒ bool"
and τmove2 :: "'s2 ⇒ 'tl2 ⇒ 's2 ⇒ bool"
and μ1 :: "'s1 ⇒ 's1 ⇒ bool"
and μ2 :: "'s2 ⇒ 's2 ⇒ bool" +
assumes simulation_silent1:
"⟦ s1 ≈ s2; s1 -τ1→ s1' ⟧ ⟹ s1' ≈ s2 ∧ μ1^++ s1' s1 ∨ (∃s2'. s2 -τ2→+ s2' ∧ s1' ≈ s2')"
and simulation_silent2:
"⟦ s1 ≈ s2; s2 -τ2→ s2' ⟧ ⟹ s1 ≈ s2' ∧ μ2^++ s2' s2 ∨ (∃s1'. s1 -τ1→+ s1' ∧ s1' ≈ s2')"
and wf_μ1: "wfP μ1"
and wf_μ2: "wfP μ2"
begin
lemma delay_bisimulation_measure_flip:
"delay_bisimulation_measure trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 μ2 μ1"
apply(rule delay_bisimulation_measure.intro)
apply(rule delay_bisimulation_obs_flip)
apply(unfold_locales)
apply(unfold flip_simps)
apply(rule simulation_silent1 simulation_silent2 wf_μ1 wf_μ2|assumption)+
done
end
lemma delay_bisimulation_measure_flip_simps [flip_simps]:
"delay_bisimulation_measure trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 μ2 μ1 =
delay_bisimulation_measure trsys1 trsys2 bisim tlsim τmove1 τmove2 μ1 μ2"
by(auto dest: delay_bisimulation_measure.delay_bisimulation_measure_flip simp only: flip_simps)
context delay_bisimulation_measure begin
lemma simulation_silentst1:
assumes bisim: "s1 ≈ s2" and moves: "s1 -τ1→+ s1'"
shows "s1' ≈ s2 ∧ μ1^++ s1' s1 ∨ (∃s2'. s2 -τ2→+ s2' ∧ s1' ≈ s2')"
using moves bisim
proof induct
case (base s1') thus ?case by(auto dest: simulation_silent1)
next
case (step s1' s1'')
hence "s1' ≈ s2 ∧ μ1⇧+⇧+ s1' s1 ∨ (∃s2'. s2 -τ2→+ s2' ∧ s1' ≈ s2')" by blast
thus ?case
proof
assume "s1' ≈ s2 ∧ μ1⇧+⇧+ s1' s1"
hence "s1' ≈ s2" "μ1⇧+⇧+ s1' s1" by simp_all
with simulation_silent1[OF ‹s1' ≈ s2› ‹s1' -τ1→ s1''›]
show ?thesis by(auto)
next
assume "∃s2'. trsys2.silent_move⇧+⇧+ s2 s2' ∧ s1' ≈ s2'"
then obtain s2' where "s2 -τ2→+ s2'" "s1' ≈ s2'" by blast
with simulation_silent1[OF ‹s1' ≈ s2'› ‹s1' -τ1→ s1''›]
show ?thesis by(auto intro: tranclp_trans)
qed
qed
lemma simulation_silentst2:
"⟦ s1 ≈ s2; s2 -τ2→+ s2' ⟧ ⟹ s1 ≈ s2' ∧ μ2^++ s2' s2 ∨ (∃s1'. s1 -τ1→+ s1' ∧ s1' ≈ s2')"
using delay_bisimulation_measure.simulation_silentst1[OF delay_bisimulation_measure_flip]
unfolding flip_simps .
lemma τdiverge_simulation1:
assumes diverge1: "s1 -τ1→ ∞"
and bisim: "s1 ≈ s2"
shows "s2 -τ2→ ∞"
proof -
from assms have "s1 -τ1→ ∞ ∧ s1 ≈ s2" by blast
thus ?thesis using wfp_tranclp[OF wf_μ1]
proof(coinduct rule: trsys2.τdiverge_trancl_measure_coinduct)
case (τdiverge s2 s1)
hence "s1 -τ1→ ∞" "s1 ≈ s2" by simp_all
then obtain s1' where "trsys1.silent_move s1 s1'" "s1' -τ1→ ∞"
by(fastforce elim: trsys1.τdiverge.cases)
from simulation_silent1[OF ‹s1 ≈ s2› ‹trsys1.silent_move s1 s1'›] ‹s1' -τ1→ ∞›
show ?case by auto
qed
qed
lemma τdiverge_simulation2:
"⟦ s2 -τ2→ ∞; s1 ≈ s2 ⟧ ⟹ s1 -τ1→ ∞"
using delay_bisimulation_measure.τdiverge_simulation1[OF delay_bisimulation_measure_flip]
unfolding flip_simps .
lemma τdiverge_bisim_inv:
"s1 ≈ s2 ⟹ s1 -τ1→ ∞ ⟷ s2 -τ2→ ∞"
by(blast intro: τdiverge_simulation1 τdiverge_simulation2)
end
sublocale delay_bisimulation_measure < delay_bisimulation_diverge
proof
fix s1 s2 s1'
assume "s1 ≈ s2" "s1 -τ1→ s1'"
from simulation_silent1[OF this]
show "∃s2'. s2 -τ2→* s2' ∧ s1' ≈ s2'" by(auto intro: tranclp_into_rtranclp)
next
fix s1 s2 s2'
assume "s1 ≈ s2" "s2 -τ2→ s2'"
from simulation_silent2[OF this]
show "∃s1'. s1 -τ1→* s1' ∧ s1' ≈ s2'" by(auto intro: tranclp_into_rtranclp)
next
fix s1 s2
assume "s1 ≈ s2"
thus "s1 -τ1→ ∞ ⟷ s2 -τ2→ ∞" by(rule τdiverge_bisim_inv)
qed
text ‹
Counter example for
@{prop "delay_bisimulation_diverge trsys1 trsys2 bisim tlsim τmove1 τmove2 ⟹ ∃μ1 μ2. delay_bisimulation_measure trsys1 trsys2 bisim tlsim τmove1 τmove2 μ1 μ2"}
(only ‹τ›moves):
\begin{verbatim}
--|
| v
--a ~ x
| |
| |
v v
--b ~ y--
| ^ ^ |
--| |--
\end{verbatim}
›
locale delay_bisimulation_measure_final =
delay_bisimulation_measure +
delay_bisimulation_final_base +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
and μ1 :: "'s1 ⇒ 's1 ⇒ bool"
and μ2 :: "'s2 ⇒ 's2 ⇒ bool"
and final1 :: "'s1 ⇒ bool"
and final2 :: "'s2 ⇒ bool"
sublocale delay_bisimulation_measure_final < delay_bisimulation_diverge_final
by unfold_locales
locale τinv = delay_bisimulation_base +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
and τmoves1 :: "'s1 ⇒ 's1 ⇒ bool"
and τmoves2 :: "'s2 ⇒ 's2 ⇒ bool"
assumes τinv: "⟦ s1 ≈ s2; s1 -1-tl1→ s1'; s2 -2-tl2→ s2'; s1' ≈ s2'; tl1 ∼ tl2 ⟧
⟹ τmove1 s1 tl1 s1' ⟷ τmove2 s2 tl2 s2'"
begin
lemma τinv_flip:
"τinv trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1"
by(unfold_locales)(unfold flip_simps,rule τinv[symmetric])
end
lemma τinv_flip_simps [flip_simps]:
"τinv trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 = τinv trsys1 trsys2 bisim tlsim τmove1 τmove2"
by(auto dest: τinv.τinv_flip simp only: flip_simps)
locale bisimulation_into_delay =
bisimulation + τinv +
constrains trsys1 :: "('s1, 'tl1) trsys"
and trsys2 :: "('s2, 'tl2) trsys"
and bisim :: "('s1, 's2) bisim"
and tlsim :: "('tl1, 'tl2) bisim"
and τmove1 :: "('s1, 'tl1) trsys"
and τmove2 :: "('s2, 'tl2) trsys"
begin
lemma bisimulation_into_delay_flip:
"bisimulation_into_delay trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1"
by(intro_locales)(intro bisimulation_flip τinv_flip)+
end
lemma bisimulation_into_delay_flip_simps [flip_simps]:
"bisimulation_into_delay trsys2 trsys1 (flip bisim) (flip tlsim) τmove2 τmove1 =
bisimulation_into_delay trsys1 trsys2 bisim tlsim τmove1 τmove2"
by(auto dest: bisimulation_into_delay.bisimulation_into_delay_flip simp only: flip_simps)
context bisimulation_into_delay begin
lemma simulation_silent1_aux:
assumes bisim: "s1 ≈ s2" and "s1 -τ1→ s1'"
shows "s1' ≈ s2 ∧ μ1⇧+⇧+ s1' s1 ∨ (∃s2'. s2 -τ2→+ s2' ∧ s1' ≈ s2')"
proof -
from assms obtain tl1 where tr1: "s1 -1-tl1→ s1'"
and τ1: "τmove1 s1 tl1 s1'" by(auto)
from simulation1[OF bisim tr1]
obtain s2' tl2 where tr2: "s2 -2-tl2→ s2'"
and bisim': "s1' ≈ s2'" and tlsim: "tl1 ∼ tl2" by blast
from τinv[OF bisim tr1 tr2 bisim' tlsim] τ1 have τ2: "τmove2 s2 tl2 s2'" by simp
from tr2 τ2 have "s2 -τ2→+ s2'" by(auto)
with bisim' show ?thesis by blast
qed
lemma simulation_silent2_aux:
"⟦ s1 ≈ s2; s2 -τ2→ s2' ⟧ ⟹ s1 ≈ s2' ∧ μ2⇧+⇧+ s2' s2 ∨ (∃s1'. s1 -τ1→+ s1' ∧ s1' ≈ s2')"
using bisimulation_into_delay.simulation_silent1_aux[OF bisimulation_into_delay_flip]
unfolding flip_simps .
lemma simulation1_aux:
assumes bisim: "s1 ≈ s2" and tr1: "s1 -1-tl1→ s1'" and τ1: "¬ τmove1 s1 tl1 s1'"
shows "∃s2' s2'' tl2. s2 -τ2→* s2' ∧ s2' -2-tl2→ s2'' ∧ ¬ τmove2 s2' tl2 s2'' ∧ s1' ≈ s2'' ∧ tl1 ∼ tl2"
proof -
from simulation1[OF bisim tr1]
obtain s2' tl2 where tr2: "s2 -2-tl2→ s2'"
and bisim': "s1' ≈ s2'" and tlsim: "tl1 ∼ tl2" by blast
from τinv[OF bisim tr1 tr2 bisim' tlsim] τ1 have τ2: "¬ τmove2 s2 tl2 s2'" by simp
with bisim' tr2 tlsim show ?thesis by blast
qed
lemma simulation2_aux:
"⟦ s1 ≈ s2; s2 -2-tl2→ s2'; ¬ τmove2 s2 tl2 s2' ⟧
⟹ ∃s1' s1'' tl1. s1 -τ1→* s1' ∧ s1' -1-tl1→ s1'' ∧ ¬ τmove1 s1' tl1 s1'' ∧ s1'' ≈ s2' ∧ tl1 ∼ tl2"
using bisimulation_into_delay.simulation1_aux[OF bisimulation_into_delay_flip]
unfolding flip_simps .
lemma delay_bisimulation_measure:
assumes wf_μ1: "wfP μ1"
and wf_μ2: "wfP μ2"
shows "delay_bisimulation_measure trsys1 trsys2 bisim tlsim τmove1 τmove2 μ1 μ2"
apply(unfold_locales)
apply(rule simulation_silent1_aux simulation_silent2_aux simulation1_aux simulation2_aux wf_μ1 wf_μ2|assumption)+
done
lemma delay_bisimulation:
"delay_bisimulation_diverge trsys1 trsys2 bisim tlsim τmove1 τmove2"
proof -
interpret delay_bisimulation_measure trsys1 trsys2 bisim tlsim τmove1 τmove2 "λs s'. False" "λs s'. False"
by(blast intro: delay_bisimulation_measure wfp_empty)
show ?thesis ..
qed
end
sublocale bisimulation_into_delay < delay_bisimulation_diverge
by(rule delay_bisimulation)
lemma delay_bisimulation_conv_bisimulation:
"delay_bisimulation_diverge trsys1 trsys2 bisim tlsim (λs tl s'. False) (λs tl s'. False) =
bisimulation trsys1 trsys2 bisim tlsim"
(is "?lhs = ?rhs")
proof
assume ?lhs
then interpret delay_bisimulation_diverge trsys1 trsys2 bisim tlsim "λs tl s'. False" "λs tl s'. False" .
show ?rhs by(unfold_locales)(fastforce simp add: τmoves_False dest: simulation1 simulation2)+
next
assume ?rhs
then interpret bisimulation trsys1 trsys2 bisim tlsim .
interpret bisimulation_into_delay trsys1 trsys2 bisim tlsim "λs tl s'. False" "λs tl s'. False"
by(unfold_locales)(rule refl)
show ?lhs by unfold_locales
qed
context bisimulation_final begin
lemma delay_bisimulation_final_base:
"delay_bisimulation_final_base trsys1 trsys2 bisim τmove1 τmove2 final1 final2"
by(unfold_locales)(auto simp add: bisim_final)
end
sublocale bisimulation_final < delay_bisimulation_final_base
by(rule delay_bisimulation_final_base)
subsection ‹Transitivity for bisimulations›
definition bisim_compose :: "('s1, 's2) bisim ⇒ ('s2, 's3) bisim ⇒ ('s1, 's3) bisim" (infixr ‹∘⇩B› 60)
where "(bisim1 ∘⇩B bisim2) s1 s3 ≡ ∃s2. bisim1 s1 s2 ∧ bisim2 s2 s3"
lemma bisim_composeI [intro]:
"⟦ bisim12 s1 s2; bisim23 s2 s3 ⟧ ⟹ (bisim12 ∘⇩B bisim23) s1 s3"
by(auto simp add: bisim_compose_def)
lemma bisim_composeE [elim!]:
assumes bisim: "(bisim12 ∘⇩B bisim23) s1 s3"
obtains s2 where "bisim12 s1 s2" "bisim23 s2 s3"
by(atomize_elim)(rule bisim[unfolded bisim_compose_def])
lemma bisim_compose_assoc [simp]:
"(bisim12 ∘⇩B bisim23) ∘⇩B bisim34 = bisim12 ∘⇩B bisim23 ∘⇩B bisim34"
by(auto simp add: fun_eq_iff)
lemma bisim_compose_conv_relcomp:
"case_prod (bisim_compose bisim12 bisim23) = (λx. x ∈ relcomp (Collect (case_prod bisim12)) (Collect (case_prod bisim23)))"
by(auto simp add: relcomp_unfold)
lemma list_all2_bisim_composeI:
"⟦ list_all2 A xs ys; list_all2 B ys zs ⟧
⟹ list_all2 (A ∘⇩B B) xs zs"
by(rule list_all2_trans) auto+
lemma delay_bisimulation_diverge_compose:
assumes wbisim12: "delay_bisimulation_diverge trsys1 trsys2 bisim12 tlsim12 τmove1 τmove2"
and wbisim23: "delay_bisimulation_diverge trsys2 trsys3 bisim23 tlsim23 τmove2 τmove3"
shows "delay_bisimulation_diverge trsys1 trsys3 (bisim12 ∘⇩B bisim23) (tlsim12 ∘⇩B tlsim23) τmove1 τmove3"
proof -
interpret trsys1: τtrsys trsys1 τmove1 .
interpret trsys2: τtrsys trsys2 τmove2 .
interpret trsys3: τtrsys trsys3 τmove3 .
interpret wb12: delay_bisimulation_diverge trsys1 trsys2 bisim12 tlsim12 τmove1 τmove2 by(auto intro: wbisim12)
interpret wb23: delay_bisimulation_diverge trsys2 trsys3 bisim23 tlsim23 τmove2 τmove3 by(auto intro: wbisim23)
show ?thesis
proof
fix s1 s3 s1'
assume bisim: "(bisim12 ∘⇩B bisim23) s1 s3" and tr1: "trsys1.silent_move s1 s1'"
from bisim obtain s2 where bisim1: "bisim12 s1 s2" and bisim2: "bisim23 s2 s3" by blast
from wb12.simulation_silent1[OF bisim1 tr1] obtain s2'
where tr2: "trsys2.silent_moves s2 s2'" and bisim1': "bisim12 s1' s2'" by blast
from wb23.simulation_silents1[OF bisim2 tr2] obtain s3'
where "trsys3.silent_moves s3 s3'" "bisim23 s2' s3'" by blast
with bisim1' show "∃s3'. trsys3.silent_moves s3 s3' ∧ (bisim12 ∘⇩B bisim23) s1' s3'"
by(blast intro: bisim_composeI)
next
fix s1 s3 s3'
assume bisim: "(bisim12 ∘⇩B bisim23) s1 s3" and tr3: "trsys3.silent_move s3 s3'"
from bisim obtain s2 where bisim1: "bisim12 s1 s2" and bisim2: "bisim23 s2 s3" by blast
from wb23.simulation_silent2[OF bisim2 tr3] obtain s2'
where tr2: "trsys2.silent_moves s2 s2'" and bisim2': "bisim23 s2' s3'" by blast
from wb12.simulation_silents2[OF bisim1 tr2] obtain s1'
where "trsys1.silent_moves s1 s1'" "bisim12 s1' s2'" by blast
with bisim2' show "∃s1'. trsys1.silent_moves s1 s1' ∧ (bisim12 ∘⇩B bisim23) s1' s3'"
by(blast intro: bisim_composeI)
next
fix s1 s3 tl1 s1'
assume bisim: "(bisim12 ∘⇩B bisim23) s1 s3"
and tr1: "trsys1 s1 tl1 s1'" and τ1: "¬ τmove1 s1 tl1 s1'"
from bisim obtain s2 where bisim1: "bisim12 s1 s2" and bisim2: "bisim23 s2 s3" by blast
from wb12.simulation1[OF bisim1 tr1 τ1] obtain s2' s2'' tl2
where tr21: "trsys2.silent_moves s2 s2'" and tr22: "trsys2 s2' tl2 s2''" and τ2: "¬ τmove2 s2' tl2 s2''"
and bisim1': "bisim12 s1' s2''" and tlsim1: "tlsim12 tl1 tl2" by blast
from wb23.simulation_silents1[OF bisim2 tr21] obtain s3'
where tr31: "trsys3.silent_moves s3 s3'" and bisim2': "bisim23 s2' s3'" by blast
from wb23.simulation1[OF bisim2' tr22 τ2] obtain s3'' s3''' tl3
where "trsys3.silent_moves s3' s3''" "trsys3 s3'' tl3 s3'''"
"¬ τmove3 s3'' tl3 s3'''" "bisim23 s2'' s3'''" "tlsim23 tl2 tl3" by blast
with tr31 bisim1' tlsim1
show "∃s3' s3'' tl3. trsys3.silent_moves s3 s3' ∧ trsys3 s3' tl3 s3'' ∧ ¬ τmove3 s3' tl3 s3'' ∧
(bisim12 ∘⇩B bisim23) s1' s3'' ∧ (tlsim12 ∘⇩B tlsim23) tl1 tl3"
by(blast intro: rtranclp_trans bisim_composeI)
next
fix s1 s3 tl3 s3'
assume bisim: "(bisim12 ∘⇩B bisim23) s1 s3"
and tr3: "trsys3 s3 tl3 s3'" and τ3: "¬ τmove3 s3 tl3 s3'"
from bisim obtain s2 where bisim1: "bisim12 s1 s2" and bisim2: "bisim23 s2 s3" by blast
from wb23.simulation2[OF bisim2 tr3 τ3] obtain s2' s2'' tl2
where tr21: "trsys2.silent_moves s2 s2'" and tr22: "trsys2 s2' tl2 s2''" and τ2: "¬ τmove2 s2' tl2 s2''"
and bisim2': "bisim23 s2'' s3'" and tlsim2: "tlsim23 tl2 tl3" by blast
from wb12.simulation_silents2[OF bisim1 tr21] obtain s1'
where tr11: "trsys1.silent_moves s1 s1'" and bisim1': "bisim12 s1' s2'" by blast
from wb12.simulation2[OF bisim1' tr22 τ2] obtain s1'' s1''' tl1
where "trsys1.silent_moves s1' s1''" "trsys1 s1'' tl1 s1'''"
"¬ τmove1 s1'' tl1 s1'''" "bisim12 s1''' s2''" "tlsim12 tl1 tl2" by blast
with tr11 bisim2' tlsim2
show "∃s1' s1'' tl1. trsys1.silent_moves s1 s1' ∧ trsys1 s1' tl1 s1'' ∧ ¬ τmove1 s1' tl1 s1'' ∧
(bisim12 ∘⇩B bisim23) s1'' s3' ∧ (tlsim12 ∘⇩B tlsim23) tl1 tl3"
by(blast intro: rtranclp_trans bisim_composeI)
next
fix s1 s2
assume "(bisim12 ∘⇩B bisim23) s1 s2"
thus "τtrsys.τdiverge trsys1 τmove1 s1 = τtrsys.τdiverge trsys3 τmove3 s2"
by(auto simp add: wb12.τdiverge_bisim_inv wb23.τdiverge_bisim_inv)
qed
qed
lemma bisimulation_bisim_compose:
"⟦ bisimulation trsys1 trsys2 bisim12 tlsim12; bisimulation trsys2 trsys3 bisim23 tlsim23 ⟧
⟹ bisimulation trsys1 trsys3 (bisim_compose bisim12 bisim23) (bisim_compose tlsim12 tlsim23)"
unfolding delay_bisimulation_conv_bisimulation[symmetric]
by(rule delay_bisimulation_diverge_compose)
lemma delay_bisimulation_diverge_final_compose:
fixes τmove1 τmove2
assumes wbisim12: "delay_bisimulation_diverge_final trsys1 trsys2 bisim12 tlsim12 τmove1 τmove2 final1 final2"
and wbisim23: "delay_bisimulation_diverge_final trsys2 trsys3 bisim23 tlsim23 τmove2 τmove3 final2 final3"
shows "delay_bisimulation_diverge_final trsys1 trsys3 (bisim12 ∘⇩B bisim23) (tlsim12 ∘⇩B tlsim23) τmove1 τmove3 final1 final3"
proof -
interpret trsys1: τtrsys trsys1 τmove1 .
interpret trsys2: τtrsys trsys2 τmove2 .
interpret trsys3: τtrsys trsys3 τmove3 .
interpret wb12: delay_bisimulation_diverge_final trsys1 trsys2 bisim12 tlsim12 τmove1 τmove2 final1 final2
by(auto intro: wbisim12)
interpret wb23: delay_bisimulation_diverge_final trsys2 trsys3 bisim23 tlsim23 τmove2 τmove3 final2 final3
by(auto intro: wbisim23)
interpret delay_bisimulation_diverge trsys1 trsys3 "bisim12 ∘⇩B bisim23" "tlsim12 ∘⇩B tlsim23" τmove1 τmove3
by(rule delay_bisimulation_diverge_compose)(unfold_locales)
show ?thesis
proof
fix s1 s3
assume "(bisim12 ∘⇩B bisim23) s1 s3" "final1 s1"
from ‹(bisim12 ∘⇩B bisim23) s1 s3› obtain s2 where "bisim12 s1 s2" and "bisim23 s2 s3" ..
from wb12.final1_simulation[OF ‹bisim12 s1 s2› ‹final1 s1›]
obtain s2' where "trsys2.silent_moves s2 s2'" "bisim12 s1 s2'" "final2 s2'" by blast
from wb23.simulation_silents1[OF ‹bisim23 s2 s3› ‹trsys2.silent_moves s2 s2'›]
obtain s3' where "trsys3.silent_moves s3 s3'" "bisim23 s2' s3'" by blast
from wb23.final1_simulation[OF ‹bisim23 s2' s3'› ‹final2 s2'›]
obtain s3'' where "trsys3.silent_moves s3' s3''" "bisim23 s2' s3''" "final3 s3''" by blast
from ‹trsys3.silent_moves s3 s3'› ‹trsys3.silent_moves s3' s3''›
have "trsys3.silent_moves s3 s3''" by(rule rtranclp_trans)
moreover from ‹bisim12 s1 s2'› ‹bisim23 s2' s3''›
have "(bisim12 ∘⇩B bisim23) s1 s3''" ..
ultimately show "∃s3'. trsys3.silent_moves s3 s3' ∧ (bisim12 ∘⇩B bisim23) s1 s3' ∧ final3 s3'"
using ‹final3 s3''› by iprover
next
fix s1 s3
assume "(bisim12 ∘⇩B bisim23) s1 s3" "final3 s3"
from ‹(bisim12 ∘⇩B bisim23) s1 s3› obtain s2 where "bisim12 s1 s2" and "bisim23 s2 s3" ..
from wb23.final2_simulation[OF ‹bisim23 s2 s3› ‹final3 s3›]
obtain s2' where "trsys2.silent_moves s2 s2'" "bisim23 s2' s3" "final2 s2'" by blast
from wb12.simulation_silents2[OF ‹bisim12 s1 s2› ‹trsys2.silent_moves s2 s2'›]
obtain s1' where "trsys1.silent_moves s1 s1'" "bisim12 s1' s2'" by blast
from wb12.final2_simulation[OF ‹bisim12 s1' s2'› ‹final2 s2'›]
obtain s1'' where "trsys1.silent_moves s1' s1''" "bisim12 s1'' s2'" "final1 s1''" by blast
from ‹trsys1.silent_moves s1 s1'› ‹trsys1.silent_moves s1' s1''›
have "trsys1.silent_moves s1 s1''" by(rule rtranclp_trans)
moreover from ‹bisim12 s1'' s2'› ‹bisim23 s2' s3›
have "(bisim12 ∘⇩B bisim23) s1'' s3" ..
ultimately show "∃s1'. trsys1.silent_moves s1 s1' ∧ (bisim12 ∘⇩B bisim23) s1' s3 ∧ final1 s1'"
using ‹final1 s1''› by iprover
qed
qed
end