Theory Coupled_Simulation
section ‹Coupled Simulation›
theory Coupled_Simulation
imports Contrasimulation
begin
context lts_tau
begin
subsection ‹Van Glabbeeks's Coupled Simulation›
text ‹We mainly use van Glabbeek's coupled simulation from his 2017 CSP paper @{cite "glabbeek2017"}.
Later on, we will compare it to other definitions of coupled (delay/weak) simulations.›
definition coupled_simulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹coupled_simulation R ≡ ∀ p q .
R p q ⟶
(∀ p' a. p ⟼a p' ⟶
(∃ q'. R p' q' ∧ q ⇒^a q')) ∧
(∃ q'. q ⟼*tau q' ∧ R q' p)›
abbreviation coupled_simulated_by :: ‹'s ⇒ 's ⇒ bool› (‹_ ⊑cs _› [60, 60] 65)
where ‹coupled_simulated_by p q ≡ ∃ R . coupled_simulation R ∧ R p q›
abbreviation coupled_similar :: ‹'s ⇒ 's ⇒ bool› (‹_ ≡cs _› [60, 60] 65)
where ‹coupled_similar p q ≡ p ⊑cs q ∧ q ⊑cs p›
text ‹We call ‹⊑cs› "coupled simulation preorder" and ‹≡cs› coupled similarity.›
subsection ‹Position between Weak Simulation and Weak Bisimulation›
text ‹Coupled simulations are special weak simulations, and symmetric weak bisimulations also
are coupled simulations.›
lemma coupled_simulation_weak_simulation:
‹coupled_simulation R =
(weak_simulation R ∧ (∀ p q . R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p)))›
unfolding coupled_simulation_def weak_simulation_def by blast
corollary coupled_simulation_implies_weak_simulation:
assumes ‹coupled_simulation R›
shows ‹weak_simulation R›
using assms unfolding coupled_simulation_weak_simulation ..
corollary coupledsim_enabled_subs:
assumes
‹p ⊑cs q›
‹weak_enabled p a›
‹¬ tau a›
shows ‹weak_enabled q a›
using assms weak_sim_enabled_subs coupled_simulation_implies_weak_simulation by blast
lemma coupled_simulation_implies_coupling:
assumes
‹coupled_simulation R›
‹R p q›
shows
‹∃ q'. q ⟼*tau q' ∧ R q' p›
using assms unfolding coupled_simulation_weak_simulation by blast
lemma weak_bisim_implies_coupled_sim_gla17:
assumes
wbisim: ‹weak_bisimulation R› and
symmetry: ‹⋀ p q . R p q ⟹ R q p›
shows ‹coupled_simulation R›
unfolding coupled_simulation_def proof safe
fix p q p' a
assume ‹R p q› ‹p ⟼a p'›
thus ‹∃q'. R p' q' ∧ (q ⇒^a q')›
using wbisim unfolding weak_bisimulation_def by simp
next
fix p q
assume ‹R p q›
thus ‹∃q'. q ⟼* tau q' ∧ R q' p›
using symmetry steps.refl[of q tau] by auto
qed
subsection ‹Coupled Simulation and Silent Steps›
text ‹Coupled simulation shares important patterns with weak simulation when it comes to the
treatment of silent steps.›
lemma coupledsim_step_gla17:
‹coupled_simulation (λ p1 q1 . q1 ⟼* tau p1)›
unfolding coupled_simulation_def
using lts.steps.simps by metis
corollary coupledsim_step:
assumes
‹p ⟼* tau q›
shows
‹q ⊑cs p›
using assms coupledsim_step_gla17 by auto
text ‹A direct implication of this is that states on a tau loop are coupled similar.›
corollary strongly_tau_connected_coupled_similar:
assumes
‹p ⟼* tau q›
‹q ⟼* tau p›
shows ‹p ≡cs q›
using assms coupledsim_step by auto
lemma silent_steps_retain_coupled_simulation:
assumes
‹coupled_simulation R›
‹R p q›
‹p ⟼* A p'›
‹A = tau›
shows ‹∃ q' . q ⟼* A q' ∧ R p' q'›
using assms(1,3,2,4) steps_retain_weak_sim
unfolding coupled_simulation_weak_simulation by blast
lemma coupled_simulation_weak_premise:
‹coupled_simulation R =
(∀ p q . R p q ⟶
(∀ p' a. p ⇒^a p' ⟶
(∃ q'. R p' q' ∧ q ⇒^a q')) ∧
(∃ q'. q ⟼*tau q' ∧ R q' p))›
unfolding coupled_simulation_weak_simulation weak_sim_weak_premise by blast
subsection ‹Closure, Preorder and Symmetry Properties›
text ‹The coupled simulation preorder ‹⊑cs› @{emph ‹is›} a preoder and symmetric at the
stable states.›
lemma coupledsim_union:
assumes
‹coupled_simulation R1›
‹coupled_simulation R2›
shows
‹coupled_simulation (λ p q . R1 p q ∨ R2 p q)›
using assms unfolding coupled_simulation_def by (blast)
lemma coupledsim_refl:
‹p ⊑cs p›
using coupledsim_step steps.refl by auto
lemma coupledsim_trans:
assumes
‹p ⊑cs pq›
‹pq ⊑cs q›
shows
‹p ⊑cs q›
proof -
obtain R1 where R1_def: ‹coupled_simulation R1› ‹R1 p pq›
using assms(1) by blast
obtain R2 where R2_def: ‹coupled_simulation R2› ‹R2 pq q›
using assms(2) by blast
define R where R_def: ‹R ≡ λ p q . ∃ pq . (R1 p pq ∧ R2 pq q) ∨ (R2 p pq ∧ R1 pq q)›
have ‹weak_simulation R› ‹R p q›
using weak_sim_trans_constructive
R1_def(2) R2_def(2)
coupled_simulation_implies_weak_simulation[OF R1_def(1)]
coupled_simulation_implies_weak_simulation[OF R2_def(1)]
unfolding R_def by auto
moreover have ‹(∀ p q . R p q ⟶ (∃ q'. q ⟼*tau q' ∧ R q' p))›
unfolding R_def
proof safe
fix p q pq
assume r1r2: ‹R1 p pq› ‹R2 pq q›
then obtain pq' where ‹R1 pq' p› ‹pq ⟼* tau pq'›
using r1r2 R1_def(1) unfolding coupled_simulation_weak_premise by blast
then moreover obtain q' where ‹R2 pq' q'› ‹q ⟼* tau q'›
using r1r2 R2_def(1) weak_step_tau_tau[OF `pq ⟼* tau pq'`] tau_tau
unfolding coupled_simulation_weak_premise by blast
then moreover obtain q'' where ‹R2 q'' pq'› ‹q' ⟼* tau q''›
using R2_def(1) unfolding coupled_simulation_weak_premise by blast
ultimately show ‹∃q'. q ⟼* tau q' ∧ (∃pq. R1 q' pq ∧ R2 pq p ∨ R2 q' pq ∧ R1 pq p)›
using steps_concat by blast
next
fix p q pq
assume r2r1: ‹R2 p pq› ‹R1 pq q›
then obtain pq' where ‹R2 pq' p› ‹pq ⟼* tau pq'›
using r2r1 R2_def(1) unfolding coupled_simulation_weak_premise by blast
then moreover obtain q' where ‹R1 pq' q'› ‹q ⟼* tau q'›
using r2r1 R1_def(1) weak_step_tau_tau[OF `pq ⟼* tau pq'`] tau_tau
unfolding coupled_simulation_weak_premise by blast
then moreover obtain q'' where ‹R1 q'' pq'› ‹q' ⟼* tau q''›
using R1_def(1) unfolding coupled_simulation_weak_premise by blast
ultimately show ‹∃q'. q ⟼* tau q' ∧ (∃pq. R1 q' pq ∧ R2 pq p ∨ R2 q' pq ∧ R1 pq p)›
using steps_concat by blast
qed
ultimately have ‹R p q› ‹coupled_simulation R›
using coupled_simulation_weak_simulation by auto
thus ?thesis by blast
qed
interpretation preorder ‹λ p q. p ⊑cs q› ‹λ p q. p ⊑cs q ∧ ¬(q ⊑cs p)›
by (standard, blast, fact coupledsim_refl, fact coupledsim_trans)
lemma coupled_similarity_equivalence:
‹equivp (λ p q. p ≡cs q)›
proof (rule equivpI)
show ‹reflp coupled_similar›
unfolding reflp_def by blast
next
show ‹symp coupled_similar›
unfolding symp_def by blast
next
show ‹transp coupled_similar›
unfolding transp_def using coupledsim_trans by meson
qed
lemma coupledsim_tau_max_eq:
assumes
‹p ⊑cs q›
‹tau_max q›
shows ‹p ≡cs q›
using assms using coupled_simulation_weak_simulation coupling_tau_max_symm by metis
corollary coupledsim_stable_eq:
assumes
‹p ⊑cs q›
‹stable_state q›
shows ‹p ≡cs q›
using assms using coupled_simulation_weak_simulation coupling_stability_symm by metis
subsection ‹Coinductive Coupled Simulation Preorder›
text ‹‹⊑cs› can also be characterized coinductively. ‹⊑cs› is the greatest
coupled simulation.›
coinductive greatest_coupled_simulation :: ‹'s ⇒ 's ⇒ bool›
where gcs:
‹⟦⋀ a p' . p ⟼a p' ⟹ ∃q'. q ⇒^^ a q' ∧ greatest_coupled_simulation p' q';
∃ q' . q ⟼* tau q' ∧ greatest_coupled_simulation q' p⟧
⟹ greatest_coupled_simulation p q›
lemma gcs_implies_gws:
assumes ‹greatest_coupled_simulation p q›
shows ‹greatest_weak_simulation p q›
using assms by (metis greatest_coupled_simulation.cases greatest_weak_simulation.coinduct)
lemma gcs_is_coupled_simulation:
shows ‹coupled_simulation greatest_coupled_simulation›
unfolding coupled_simulation_def
proof safe
fix p q p' a
assume ih:
‹greatest_coupled_simulation p q›
‹p ⟼a p'›
hence ‹(∀x xa. p ⟼x xa ⟶ (∃q'. q ⇒^^ x q' ∧ greatest_coupled_simulation xa q'))›
by (meson greatest_coupled_simulation.simps)
then obtain q' where ‹q ⇒^^ a q' ∧ greatest_coupled_simulation p' q'› using ih by blast
thus ‹∃q'. greatest_coupled_simulation p' q' ∧ q ⇒^a q'›
unfolding weak_step_tau2_def by blast
next
fix p q
assume
‹greatest_coupled_simulation p q›
thus ‹∃q'. q ⟼* tau q' ∧ greatest_coupled_simulation q' p›
by (meson greatest_coupled_simulation.simps)
qed
lemma coupled_similarity_implies_gcs:
assumes ‹p ⊑cs q›
shows ‹greatest_coupled_simulation p q›
using assms
proof (coinduct)
case (greatest_coupled_simulation p1 q1)
then obtain R where ‹coupled_simulation R› ‹R p1 q1›
‹weak_simulation R› using coupled_simulation_implies_weak_simulation by blast
then have ‹(∀x xa. p1 ⟼x xa ⟶
(∃q'. q1 ⇒^x q' ∧ (xa ⊑cs q' ∨ greatest_coupled_simulation xa q'))) ∧
(∃q'. q1 ⟼* tau q' ∧
(q' ⊑cs p1 ∨ greatest_coupled_simulation q' p1))›
unfolding weak_step_tau2_def
using coupled_simulation_implies_coupling
weak_sim_ruleformat[OF ‹weak_simulation R›]
by (metis (no_types, lifting))
thus ?case by simp
qed
lemma gcs_eq_coupled_sim_by:
shows ‹p ⊑cs q = greatest_coupled_simulation p q›
using coupled_similarity_implies_gcs gcs_is_coupled_simulation by blast
lemma coupled_sim_by_is_coupled_sim:
shows
‹coupled_simulation (λ p q . p ⊑cs q)›
unfolding gcs_eq_coupled_sim_by using gcs_is_coupled_simulation .
lemma coupledsim_unfold:
shows ‹p ⊑cs q =
((∀a p'. p ⟼a p' ⟶ (∃q'. q ⇒^a q' ∧ p' ⊑cs q')) ∧
(∃q'. q ⟼* tau q' ∧ q' ⊑cs p))›
unfolding gcs_eq_coupled_sim_by weak_step_tau2_def[symmetric]
by (metis lts_tau.greatest_coupled_simulation.simps)
subsection ‹Coupled Simulation Join›
text ‹The following lemmas reproduce Proposition 3 from @{cite glabbeek2017} that internal choice
acts as a least upper bound within the semi-lattice of CSP terms related by ‹⊑cs› taking ‹≡cs›
as equality.›
lemma coupledsim_choice_1:
assumes
‹p ⊑cs q›
‹⋀ pq a . pqc ⟼a pq ⟷ (a = τ ∧ (pq = p ∨ pq = q))›
shows
‹pqc ⊑cs q›
‹q ⊑cs pqc›
proof -
define R1 where ‹R1 ≡ (λp1 q1. q1 ⟼* tau p1)›
have ‹R1 q pqc›
using assms(2) steps_one_step R1_def by simp
moreover have ‹coupled_simulation R1›
unfolding R1_def using coupledsim_step_gla17 .
ultimately show q_pqc: ‹q ⊑cs pqc› by blast
define R where ‹R ≡ λ p0 q0 . p0 = q ∧ q0 = pqc ∨ p0 = pqc ∧ q0 = q ∨ p0 = p ∧ q0 = q›
hence ‹R pqc q› by blast
thus ‹pqc ⊑cs q›
unfolding gcs_eq_coupled_sim_by
proof (coinduct)
case (greatest_coupled_simulation p1 q1)
then show ?case
unfolding weak_step_tau2_def R_def
proof safe
assume ‹q1 = pqc› ‹p1 = q›
thus ‹∃pa qa.
q = pa ∧ pqc = qa ∧
(∀x xa. pa ⟼x xa ⟶
(∃q'. qa ⇒^x q' ∧ ((xa = q ∧ q' = pqc ∨ xa = pqc ∧ q' = q ∨ xa = p ∧ q' = q)
∨ greatest_coupled_simulation xa q'))) ∧
(∃q'. qa ⟼* tau q' ∧
((q' = q ∧ pa = pqc ∨ q' = pqc ∧ pa = q ∨ q' = p ∧ pa = q)
∨ greatest_coupled_simulation q' pa))›
using `q ⊑cs pqc` step_tau_refl weak_sim_ruleformat tau_def
coupled_simulation_implies_weak_simulation[OF gcs_is_coupled_simulation]
unfolding gcs_eq_coupled_sim_by by fastforce
next
assume ‹q1 = q› ‹p1 = pqc›
thus ‹∃pa qa.
pqc = pa ∧ q = qa ∧
(∀x xa. pa ⟼x xa ⟶
(∃q'. qa ⇒^x q' ∧ ((xa = q ∧ q' = pqc ∨ xa = pqc ∧ q' = q ∨ xa = p ∧ q' = q)
∨ greatest_coupled_simulation xa q'))) ∧
(∃q'. qa ⟼* tau q' ∧
((q' = q ∧ pa = pqc ∨ q' = pqc ∧ pa = q ∨ q' = p ∧ pa = q)
∨ greatest_coupled_simulation q' pa))›
using R1_def ‹coupled_simulation R1› assms(2)
coupled_similarity_implies_gcs step_tau_refl by fastforce
next
assume ‹q1 = q› ‹p1 = p›
thus ‹∃pa qa.
p = pa ∧ q = qa ∧
(∀x xa. pa ⟼x xa ⟶ (∃q'. qa ⇒^x q' ∧ ((xa = q ∧ q' = pqc ∨ xa = pqc ∧ q' = q ∨ xa = p ∧ q' = q) ∨ greatest_coupled_simulation xa q'))) ∧
(∃q'. qa ⟼* tau q' ∧ ((q' = q ∧ pa = pqc ∨ q' = pqc ∧ pa = q ∨ q' = p ∧ pa = q) ∨ greatest_coupled_simulation q' pa))›
using `p ⊑cs q` weak_sim_ruleformat
coupled_simulation_implies_weak_simulation[OF gcs_is_coupled_simulation]
coupled_simulation_implies_coupling[OF gcs_is_coupled_simulation]
unfolding gcs_eq_coupled_sim_by
by (auto, metis+)
qed
qed
qed
lemma coupledsim_choice_2:
assumes
‹pqc ⊑cs q›
‹⋀ pq a . pqc ⟼a pq ⟷ (a = τ ∧ (pq = p ∨ pq = q))›
shows
‹p ⊑cs q›
proof -
have ‹pqc ⟼τ p› using assms(2) by blast
then obtain q' where ‹q ⟼* tau q'› ‹p ⊑cs q'›
using assms(1) tau_tau unfolding coupled_simulation_def by blast
then moreover have ‹q' ⊑cs q› using coupledsim_step_gla17 by blast
ultimately show ?thesis using coupledsim_trans tau_tau by blast
qed
lemma coupledsim_choice_join:
assumes
‹⋀ pq a . pqc ⟼a pq ⟷ (a = τ ∧ (pq = p ∨ pq = q))›
shows
‹p ⊑cs q ⟷ pqc ≡cs q›
using coupledsim_choice_1[OF _ assms] coupledsim_choice_2[OF _ assms] by blast
subsection ‹Coupled Delay Simulation›
text ‹‹⊑cs› can also be characterized in terms of coupled delay simulations, which are
conceptionally simpler than van Glabbeek's coupled simulation definition.›
text ‹In the greatest coupled simulation, ‹τ›-challenges can be answered by stuttering.›
lemma coupledsim_tau_challenge_trivial:
assumes
‹p ⊑cs q›
‹p ⟼* tau p'›
shows
‹p' ⊑cs q›
using assms coupledsim_trans coupledsim_step by blast
lemma coupled_similarity_s_delay_simulation:
‹delay_simulation (λ p q. p ⊑cs q)›
unfolding delay_simulation_def
proof safe
fix p q R p' a
assume assms:
‹coupled_simulation R›
‹R p q›
‹p ⟼a p'›
{
assume ‹tau a›
then show ‹p' ⊑cs q›
using assms coupledsim_tau_challenge_trivial steps_one_step by blast
} {
show ‹∃q'. p' ⊑cs q' ∧ q =⊳a q'›
proof -
obtain q''' where q'''_spec: ‹q ⇒^a q'''› ‹p' ⊑cs q'''›
using assms coupled_simulation_implies_weak_simulation weak_sim_ruleformat by metis
show ?thesis
proof (cases ‹tau a›)
case True
then have ‹q ⟼* tau q'''› using q'''_spec by blast
thus ?thesis using q'''_spec(2) True assms(1) steps.refl by blast
next
case False
then obtain q' q'' where q'q''_spec:
‹q ⟼* tau q'› ‹q' ⟼a q''› ‹q'' ⟼* tau q'''›
using q'''_spec by blast
hence ‹q''' ⊑cs q''› using coupledsim_step by blast
hence ‹p' ⊑cs q''› using q'''_spec(2) coupledsim_trans by blast
thus ?thesis using q'q''_spec(1,2) False by blast
qed
qed
}
qed
definition coupled_delay_simulation ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹coupled_delay_simulation R ≡
delay_simulation R ∧ coupling R›
lemma coupled_sim_by_eq_coupled_delay_simulation:
‹(p ⊑cs q) = (∃R. R p q ∧ coupled_delay_simulation R)›
unfolding coupled_delay_simulation_def
proof
assume ‹p ⊑cs q›
define R where ‹R ≡ coupled_simulated_by›
hence ‹R p q ∧ delay_simulation R ∧ coupling R›
using coupled_similarity_s_delay_simulation coupled_sim_by_is_coupled_sim
coupled_simulation_implies_coupling ‹p ⊑cs q› by blast
thus ‹∃R. R p q ∧ delay_simulation R ∧ coupling R› by blast
next
assume ‹∃R. R p q ∧ delay_simulation R ∧ coupling R›
then obtain R where ‹R p q› ‹delay_simulation R› ‹coupling R› by blast
hence ‹coupled_simulation R›
using delay_simulation_implies_weak_simulation coupled_simulation_weak_simulation by blast
thus ‹p ⊑cs q› using ‹R p q› by blast
qed
subsection ‹Relationship to Contrasimulation and Weak Simulation›
text ‹Coupled simulation is precisely the intersection of contrasimulation and weak simulation.›
lemma weak_sim_and_contrasim_implies_coupled_sim:
assumes
‹contrasimulation R›
‹weak_simulation R›
shows
‹coupled_simulation R›
unfolding coupled_simulation_weak_simulation
using contrasim_coupled assms by blast
lemma coupledsim_implies_contrasim:
assumes
‹coupled_simulation R›
shows
‹contrasimulation R›
proof -
have ‹contrasim_step R›
unfolding contrasim_step_def
proof (rule allI impI)+
fix p q p' a
assume
‹R p q ∧ p ⇒^a p'›
then obtain q' where q'_def: ‹R p' q'› ‹q ⇒^a q'›
using assms unfolding coupled_simulation_weak_premise by blast
then obtain q'' where q''_def: ‹R q'' p'› ‹q' ⟼* tau q''›
using assms unfolding coupled_simulation_weak_premise by blast
then have ‹q ⇒^a q''› using q'_def(2) steps_concat by blast
thus ‹∃q'. q ⇒^a q' ∧ R q' p'›
using q''_def(1) by blast
qed
thus ‹contrasimulation R› using contrasim_step_seq_coincide_for_sims
coupled_simulation_implies_weak_simulation[OF assms] by blast
qed
lemma coupled_simulation_iff_weak_sim_and_contrasim:
shows ‹coupled_simulation R ⟷ contrasimulation R ∧ weak_simulation R›
using weak_sim_and_contrasim_implies_coupled_sim
coupledsim_implies_contrasim coupled_simulation_weak_simulation by blast
subsection ‹‹τ›-Reachability (and Divergence)›
text ‹
Coupled similarity comes close to (weak) bisimilarity in two respects:
▪ If there are no ‹τ› transitions, coupled similarity coincides with bisimilarity.
▪ If there are only finite ‹τ› reachable portions, then coupled similarity contains a
bisimilarity on the ‹τ›-maximal states. (For this, ‹τ›-cycles have to be ruled out, which, as
we show, is no problem because their removal is transparent to coupled similarity.)
›
lemma taufree_coupledsim_symm:
assumes
‹⋀ p1 a p2 . (p1 ⟼a p2 ⟹ ¬ tau a)›
‹coupled_simulation R›
‹R p q›
shows ‹R q p›
using assms(1,3) coupledsim_implies_contrasim[OF assms(2)] contrasim_taufree_symm
by blast
lemma taufree_coupledsim_weak_bisim:
assumes
‹⋀ p1 a p2 . (p1 ⟼a p2 ⟹ ¬ tau a)›
‹coupled_simulation R›
shows ‹weak_bisimulation R›
using assms contrasim_taufree_symm symm_contrasim_is_weak_bisim coupledsim_implies_contrasim[OF assms(2)]
by blast
lemma coupledsim_stable_state_symm:
assumes
‹coupled_simulation R›
‹R p q›
‹stable_state q›
shows
‹R q p›
using assms steps_left unfolding coupled_simulation_def by metis
text ‹In finite systems, coupling is guaranteed to happen through ‹τ›-maximal states.›
lemma coupledsim_max_coupled:
assumes
‹p ⊑cs q›
‹⋀ r1 r2 . r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2›
‹⋀ r. finite {r'. r ⟼* tau r'}›
shows
‹∃ q' . q ⟼* tau q' ∧ q' ⊑cs p ∧ tau_max q'›
proof -
obtain q1 where q1_spec: ‹q ⟼* tau q1› ‹q1 ⊑cs p›
using assms(1) coupled_simulation_implies_coupling coupledsim_implies_contrasim by blast
then obtain q' where ‹q1 ⟼* tau q'› ‹(∀q''. q' ⟼* tau q'' ⟶ q' = q'')›
using tau_max_deadlock assms(2,3) by blast
then moreover have ‹q' ⊑cs p› ‹q ⟼* tau q'›
using q1_spec coupledsim_trans coupledsim_step steps_concat[of q1 tau q' q]
by blast+
ultimately show ?thesis by blast
qed
text ‹In the greatest coupled simulation, ‹a›-challenges can be answered by a weak move without
trailing ‹τ›-steps. (This property is what bridges the gap between weak and delay simulation for
coupled simulation.)›
lemma coupledsim_step_challenge_short_answer:
assumes
‹p ⊑cs q›
‹p ⟼a p'›
‹¬ tau a›
shows
‹∃ q' q1. p' ⊑cs q' ∧ q ⟼* tau q1 ∧ q1 ⟼a q'›
using assms
unfolding coupled_sim_by_eq_coupled_delay_simulation
coupled_delay_simulation_def delay_simulation_def by blast
text ‹If two states share the same outgoing edges with except for one ‹τ›-loop, then they cannot
be distinguished by coupled similarity.›
lemma coupledsim_tau_loop_ignorance:
assumes
‹⋀ a p'. p ⟼a p' ∨ p' = pp ∧ a = τ ⟷ pp ⟼a p'›
shows
‹pp ≡cs p›
proof -
define R where ‹R ≡ λ p1 q1. p1 = q1 ∨ p1 = pp ∧ q1 = p ∨ p1 = p ∧ q1 = pp›
have ‹coupled_simulation R›
unfolding coupled_simulation_def R_def
proof (safe)
fix pa q p' a
assume
‹q ⟼a p'›
thus ‹∃q'. (p' = q' ∨ p' = pp ∧ q' = p ∨ p' = p ∧ q' = pp) ∧ q ⇒^a q'›
using assms step_weak_step_tau by auto
next
fix pa q
show ‹∃q'. q ⟼* tau q' ∧ (q' = q ∨ q' = pp ∧ q = p ∨ q' = p ∧ q = pp)›
using steps.refl by blast
next
fix pa q p' a
assume
‹pp ⟼a p'›
thus ‹∃q'. (p' = q' ∨ p' = pp ∧ q' = p ∨ p' = p ∧ q' = pp) ∧ p ⇒^a q'›
using assms by (metis lts.steps.simps tau_def)
next
fix pa q
show ‹∃q'. p ⟼* tau q' ∧ (q' = pp ∨ q' = pp ∧ pp = p ∨ q' = p ∧ pp = pp)›
using steps.refl[of p tau] by blast
next
fix pa q p' a
assume
‹p ⟼a p'›
thus ‹∃q'. (p' = q' ∨ p' = pp ∧ q' = p ∨ p' = p ∧ q' = pp) ∧ pp ⇒^a q'›
using assms step_weak_step_tau by fastforce
next
fix pa q
show ‹∃q'. pp ⟼* tau q' ∧ (q' = p ∨ q' = pp ∧ p = p ∨ q' = p ∧ p = pp)›
using steps.refl[of pp tau] by blast
qed
moreover have ‹R p pp› ‹R pp p› unfolding R_def by auto
ultimately show ?thesis by blast
qed
subsection ‹On the Connection to Weak Bisimulation›
text ‹When one only considers steps leading to ‹τ›-maximal states in a system without infinite
‹τ›-reachable regions (e.g. a finite system), then ‹≡cs› on these steps is a bisimulation.›
text ‹This lemma yields a neat argument why one can use a signature refinement algorithm to
pre-select the tuples which come into question for further checking of coupled simulation
by contraposition.›
lemma coupledsim_eventual_symmetry:
assumes
contracted_cycles: ‹⋀ r1 r2 . r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2› and
finite_taus: ‹⋀ r. finite {r'. r ⟼* tau r'}› and
cs: ‹p ⊑cs q› and
step: ‹p ⇒^a p'› and
tau_max_p': ‹tau_max p'›
shows
‹∃ q'. tau_max q' ∧ q ⇒^a q' ∧ p' ≡cs q'›
proof-
obtain q' where q'_spec: ‹q ⇒^a q'› ‹p' ⊑cs q'›
using cs step unfolding coupled_simulation_weak_premise by blast
then obtain q'' where q''_spec: ‹q' ⟼* tau q''› ‹q'' ⊑cs p'›
using cs unfolding coupled_simulation_weak_simulation by blast
then obtain q_max where q_max_spec: ‹q'' ⟼* tau q_max› ‹tau_max q_max›
using tau_max_deadlock contracted_cycles finite_taus by force
hence ‹q_max ⊑cs p'› using q''_spec coupledsim_tau_challenge_trivial by blast
hence ‹q_max ≡cs p'› using tau_max_p' coupledsim_tau_max_eq by blast
moreover have ‹q ⇒^a q_max› using q_max_spec q'_spec q''_spec steps_concat by blast
ultimately show ?thesis using q_max_spec(2) by blast
qed
text ‹Even without the assumption that the left-hand-side step ‹p ⇒^a p'› ends in a ‹τ›-maximal state,
a situation resembling bismulation can be set up -- with the drawback that it only refers to
a ‹τ›-maximal sibling of ‹p'›.›
lemma coupledsim_eventuality_2:
assumes
contracted_cycles: ‹⋀ r1 r2 . r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2› and
finite_taus: ‹⋀ r. finite {r'. r ⟼* tau r'}› and
cbisim: ‹p ≡cs q› and
step: ‹p ⇒^a p'›
shows
‹∃ p'' q'. tau_max p'' ∧ tau_max q' ∧ p ⇒^a p'' ∧ q ⇒^a q' ∧ p'' ≡cs q'›
proof-
obtain q' where q'_spec: ‹q ⇒^a q'›
using cbisim step unfolding coupled_simulation_weak_premise by blast
then obtain q_max where q_max_spec: ‹q' ⟼* tau q_max› ‹tau_max q_max›
using tau_max_deadlock contracted_cycles finite_taus by force
hence ‹q ⇒^a q_max› using q'_spec steps_concat by blast
then obtain p'' where p''_spec: ‹p ⇒^a p''› ‹q_max ⊑cs p''›
using cbisim unfolding coupled_simulation_weak_premise by blast
then obtain p''' where p'''_spec: ‹p'' ⟼* tau p'''› ‹p''' ⊑cs q_max›
using cbisim unfolding coupled_simulation_weak_simulation by blast
then obtain p_max where p_max_spec: ‹p''' ⟼* tau p_max› ‹tau_max p_max›
using tau_max_deadlock contracted_cycles finite_taus by force
hence ‹p_max ⊑cs p'''› using coupledsim_step by blast
hence ‹p_max ⊑cs q_max› using p'''_spec coupledsim_trans by blast
hence ‹q_max ≡cs p_max› using coupledsim_tau_max_eq q_max_spec by blast
moreover have ‹p ⇒^a p_max›
using p''_spec(1) steps_concat[OF p_max_spec(1) p'''_spec(1)] steps_concat by blast
ultimately show ?thesis using p_max_spec(2) q_max_spec(2) `q ⇒^a q_max` by blast
qed
lemma coupledsim_eq_reducible_1:
assumes
contracted_cycles: ‹⋀ r1 r2 . r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2› and
finite_taus: ‹⋀ r. finite {r'. r ⟼* tau r'}› and
tau_shortcuts:
‹⋀r a r'. r ⟼* tau r' ⟹ ∃r''. tau_max r'' ∧ r ⟼τ r'' ∧ r' ⊑cs r''› and
sim_vis_p:
‹⋀p' a. ¬tau a ⟹ p ⇒^a p' ⟹ ∃p'' q'. q ⇒^a q' ∧ p' ⊑cs q'› and
sim_tau_max_p:
‹⋀p'. tau_max p' ⟹ p ⟼* tau p' ⟹ ∃q'. tau_max q' ∧ q ⟼* tau q' ∧ p' ≡cs q'›
shows
‹p ⊑cs q›
proof-
have
‹((∀a p'. p ⟼a p' ⟶ (∃q'. q ⇒^a q' ∧ p' ⊑cs q')) ∧
(∃q'. q ⟼* tau q' ∧ q' ⊑cs p))›
proof safe
fix a p'
assume
step: ‹p ⟼a p'›
thus ‹∃q'. q ⇒^a q' ∧ p' ⊑cs q'›
proof (cases ‹tau a›)
case True
then obtain p'' where p''_spec: ‹p ⟼τ p''› ‹tau_max p''› ‹p' ⊑cs p''›
using tau_shortcuts step tau_def steps_one_step[of p τ p']
by (metis (no_types, lifting))
then obtain q' where q'_spec: ‹q ⟼* tau q'› ‹p'' ≡cs q'›
using sim_tau_max_p steps_one_step[OF step, of tau, OF `tau a`]
steps_one_step[of p τ p''] tau_def
by metis
then show ?thesis using `tau a` p''_spec(3) using coupledsim_trans by blast
next
case False
then show ?thesis using sim_vis_p step_weak_step_tau[OF step] by blast
qed
next
obtain p_max where ‹p ⟼* tau p_max› ‹tau_max p_max›
using tau_max_deadlock contracted_cycles finite_taus by blast
then obtain q_max where ‹q ⟼* tau q_max› ‹q_max ⊑cs p_max›
using sim_tau_max_p[of p_max] by force
moreover have ‹p_max ⊑cs p› using `p ⟼* tau p_max` coupledsim_step by blast
ultimately show ‹∃q'. q ⟼* tau q' ∧ q' ⊑cs p›
using coupledsim_trans by blast
qed
thus ‹p ⊑cs q› using coupledsim_unfold[symmetric] by auto
qed
lemma coupledsim_eq_reducible_2:
assumes
cs: ‹p ⊑cs q› and
contracted_cycles: ‹⋀r1 r2 . r1 ⟼* tau r2 ∧ r2 ⟼* tau r1 ⟹ r1 = r2› and
finite_taus: ‹⋀r. finite {r'. r ⟼* tau r'}›
shows
sim_vis_p:
‹⋀p' a. ¬tau a ⟹ p ⇒^a p' ⟹ ∃q'. q ⇒^a q' ∧ p' ⊑cs q'› and
sim_tau_max_p:
‹⋀p'. tau_max p' ⟹ p ⟼* tau p' ⟹ ∃q'. tau_max q' ∧ q ⟼* tau q' ∧ p' ≡cs q'›
proof-
fix p' a
assume
‹¬ tau a›
‹p ⇒^a p'›
thus ‹∃q'. q ⇒^a q' ∧ p' ⊑cs q'›
using cs unfolding coupled_simulation_weak_premise by blast
next
fix p'
assume step:
‹p ⟼* tau p'›
‹tau_max p'›
hence ‹p ⇒^τ p'› by auto
hence ‹∃ q'. tau_max q' ∧ q ⇒^τ q' ∧ p' ≡cs q'›
using coupledsim_eventual_symmetry[OF _ finite_taus, of p q τ p']
contracted_cycles cs step(2) by blast
thus ‹∃ q'. tau_max q' ∧ q ⟼* tau q' ∧ p' ≡cs q'›
by auto
qed
subsection ‹Reduction Semantics Coupled Simulation›
text ‹The tradition to describe coupled simulation as special delay/weak simulation is quite
common for coupled simulations on reduction semantics as in @{cite "gp15" and "Fournet2005"},
of which @{cite "gp15"} can also be found in the AFP @{cite "Encodability_Process_Calculi-AFP"}.
The notions coincide (for systems just with ‹τ›-transitions).›
definition coupled_simulation_gp15 ::
‹('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹coupled_simulation_gp15 R ≡ ∀ p q p'. R p q ∧ (p ⟼* (λa. True) p') ⟶
(∃ q'. (q ⟼* (λa. True) q') ∧ R p' q') ∧
(∃ q'. (q ⟼* (λa. True) q') ∧ R q' p')›
lemma weak_bisim_implies_coupled_sim_gp15:
assumes
wbisim: ‹weak_bisimulation R› and
symmetry: ‹⋀ p q . R p q ⟹ R q p›
shows ‹coupled_simulation_gp15 R›
unfolding coupled_simulation_gp15_def proof safe
fix p q p'
assume Rpq: ‹R p q› ‹p ⟼* (λa. True) p'›
have always_tau: ‹⋀a. tau a ⟹ (λa. True) a› by simp
hence ‹∃q'. q ⟼* (λa. True) q' ∧ R p' q'›
using steps_retain_weak_bisim[OF wbisim Rpq] by auto
moreover hence ‹∃q'. q ⟼* (λa. True) q' ∧ R q' p'›
using symmetry by auto
ultimately show
‹(∃q'. q ⟼* (λa. True) q' ∧ R p' q')›
‹(∃q'. q ⟼* (λa. True) q' ∧ R q' p')› .
qed
lemma coupledsim_gla17_implies_gp15:
assumes
‹coupled_simulation R›
shows
‹coupled_simulation_gp15 R›
unfolding coupled_simulation_gp15_def
proof safe
fix p q p'
assume challenge:
‹R p q›
‹p ⟼*(λa. True)p'›
have tau_true: ‹⋀a. tau a ⟹ (λa. True) a› by simp
thus ‹∃q'. q ⟼* (λa. True) q' ∧ R p' q'›
using steps_retain_weak_sim assms challenge
unfolding coupled_simulation_weak_simulation by meson
then obtain q' where q'_def: ‹q ⟼* (λa. True) q'› ‹R p' q'› by blast
then obtain q'' where ‹q' ⟼* tau q''› ‹R q'' p'›
using assms unfolding coupled_simulation_weak_simulation by blast
moreover hence ‹q ⟼* (λa. True) q''›
using q'_def(1) steps_concat steps_spec tau_true by meson
ultimately show ‹∃q'. q ⟼* (λa. True) q' ∧ R q' p'› by blast
qed
lemma coupledsim_gp15_implies_gla17_on_tau_systems:
assumes
‹coupled_simulation_gp15 R›
‹⋀ a . tau a›
shows
‹coupled_simulation R›
unfolding coupled_simulation_def
proof safe
fix p q p' a
assume challenge:
‹R p q›
‹p ⟼a p'›
hence ‹p ⟼* (λa. True) p'› using steps_one_step by metis
then obtain q' where ‹q ⟼* (λa. True) q'› ‹R p' q'›
using challenge(1) assms(1) unfolding coupled_simulation_gp15_def by blast
hence ‹q ⇒^a q'› using assms(2) steps_concat steps_spec by meson
thus ‹∃q'. R p' q' ∧ q ⇒^a q'› using `R p' q'` by blast
next
fix p q
assume
‹R p q›
moreover have ‹p ⟼* (λa. True) p› using steps.refl by blast
ultimately have ‹∃q'. q ⟼* (λa. True) q' ∧ R q' p›
using assms(1) unfolding coupled_simulation_gp15_def by blast
thus ‹∃q'. q ⟼* tau q' ∧ R q' p› using assms(2) steps_spec by blast
qed
subsection ‹Coupled Simulation as Two Simulations›
text ‹Historically, coupled similarity has been defined in terms of @{emph ‹two›} weak simulations
coupled in some way @{cite "sangiorgi2012" and "ps1994"}.
We reproduce these (more well-known) formulations and show that they are equivalent to the
coupled (delay) simulations we are using.›
definition coupled_simulation_san12 ::
‹('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹coupled_simulation_san12 R1 R2 ≡
weak_simulation R1 ∧ weak_simulation (λ p q . R2 q p)
∧ (∀ p q . R1 p q ⟶ (∃ q' . q ⟼* tau q' ∧ R2 p q'))
∧ (∀ p q . R2 p q ⟶ (∃ p' . p ⟼* tau p' ∧ R1 p' q))›
lemma weak_bisim_implies_coupled_sim_san12:
assumes ‹weak_bisimulation R›
shows ‹coupled_simulation_san12 R R›
using assms weak_bisim_weak_sim steps.refl[of _ tau]
unfolding coupled_simulation_san12_def
by blast
lemma coupledsim_gla17_resembles_san12:
shows
‹coupled_simulation R1 =
coupled_simulation_san12 R1 (λ p q . R1 q p)›
unfolding coupled_simulation_weak_simulation coupled_simulation_san12_def by blast
lemma coupledsim_san12_impl_gla17:
assumes
‹coupled_simulation_san12 R1 R2›
shows
‹coupled_simulation (λ p q. R1 p q ∨ R2 q p)›
unfolding coupled_simulation_weak_simulation
proof safe
have ‹weak_simulation R1› ‹weak_simulation (λp q. R2 q p)›
using assms unfolding coupled_simulation_san12_def by auto
thus ‹weak_simulation (λp q. R1 p q ∨ R2 q p)›
using weak_sim_union_cl by blast
next
fix p q
assume
‹R1 p q›
hence ‹∃q'. q ⟼* tau q' ∧ R2 p q'›
using assms unfolding coupled_simulation_san12_def by auto
thus ‹∃q'. q ⟼* tau q' ∧ (R1 q' p ∨ R2 p q')› by blast
next
fix p q
assume
‹R2 q p›
hence ‹∃q'. q ⟼* tau q' ∧ R1 q' p›
using assms unfolding coupled_simulation_san12_def by auto
thus ‹∃q'. q ⟼* tau q' ∧ (R1 q' p ∨ R2 p q')› by blast
qed
subsection ‹S-coupled Simulation›
text ‹Originally coupled simulation was introduced as two weak simulations coupled at the stable
states. We give the definitions from @{cite "parrow1992" and "ps1994"} and a proof connecting
this notion to ``our'' coupled similarity in the absence of divergences following
@{cite "sangiorgi2012"}.›
definition coupled_simulation_p92 ::
‹('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹coupled_simulation_p92 R1 R2 ≡ ∀ p q .
(R1 p q ⟶
((∀ p' a. p ⟼a p' ⟶
(∃ q'. R1 p' q' ∧
(q ⇒^a q'))) ∧
(stable_state p ⟶ R2 p q))) ∧
(R2 p q ⟶
((∀ q' a. q ⟼a q' ⟶
(∃ p'. R2 p' q' ∧
(p ⇒^a p'))) ∧
(stable_state q ⟶ R1 p q)))›
lemma weak_bisim_implies_coupled_sim_p92:
assumes ‹weak_bisimulation R›
shows ‹coupled_simulation_p92 R R›
using assms unfolding weak_bisimulation_def coupled_simulation_p92_def by blast
lemma coupled_sim_p92_symm:
assumes ‹coupled_simulation_p92 R1 R2›
shows ‹coupled_simulation_p92 (λ p q. R2 q p) (λ p q. R1 q p)›
using assms unfolding coupled_simulation_p92_def by blast
definition s_coupled_simulation_san12 ::
‹('s ⇒ 's ⇒ bool) ⇒ ('s ⇒ 's ⇒ bool) ⇒ bool›
where
‹s_coupled_simulation_san12 R1 R2 ≡
weak_simulation R1 ∧ weak_simulation (λ p q . R2 q p)
∧ (∀ p q . R1 p q ⟶ stable_state p ⟶ R2 p q)
∧ (∀ p q . R2 p q ⟶ stable_state q ⟶ R1 p q)›
abbreviation s_coupled_simulated_by :: ‹'s ⇒ 's ⇒ bool› (‹_ ⊑scs _› [60, 60] 65)
where ‹s_coupled_simulated_by p q ≡
∃ R1 R2 . s_coupled_simulation_san12 R1 R2 ∧ R1 p q›
abbreviation s_coupled_similar :: ‹'s ⇒ 's ⇒ bool› (‹_ ≡scs _› [60, 60] 65)
where ‹s_coupled_similar p q ≡
∃ R1 R2 . s_coupled_simulation_san12 R1 R2 ∧ R1 p q ∧ R2 p q›
lemma s_coupled_sim_is_original_coupled:
‹s_coupled_simulation_san12 = coupled_simulation_p92›
unfolding coupled_simulation_p92_def
s_coupled_simulation_san12_def weak_simulation_def by blast
corollary weak_bisim_implies_s_coupled_sim:
assumes ‹weak_bisimulation R›
shows ‹s_coupled_simulation_san12 R R›
using assms s_coupled_sim_is_original_coupled weak_bisim_implies_coupled_sim_p92 by simp
corollary s_coupled_sim_symm:
assumes ‹s_coupled_simulation_san12 R1 R2›
shows ‹s_coupled_simulation_san12 (λ p q. R2 q p) (λ p q. R1 q p)›
using assms coupled_sim_p92_symm s_coupled_sim_is_original_coupled by simp
corollary s_coupled_sim_union_cl:
assumes
‹s_coupled_simulation_san12 RA1 RA2›
‹s_coupled_simulation_san12 RB1 RB2›
shows
‹s_coupled_simulation_san12 (λ p q. RA1 p q ∨ RB1 p q) (λ p q. RA2 p q ∨ RB2 p q)›
using assms weak_sim_union_cl unfolding s_coupled_simulation_san12_def by auto
corollary s_coupled_sim_symm_union:
assumes ‹s_coupled_simulation_san12 R1 R2›
shows ‹s_coupled_simulation_san12 (λ p q. R1 p q ∨ R2 q p) (λ p q. R2 p q ∨ R1 q p)›
using s_coupled_sim_union_cl[OF assms s_coupled_sim_symm[OF assms]] .
lemma s_coupledsim_stable_eq:
assumes
‹p ⊑scs q›
‹stable_state p›
shows ‹p ≡scs q›
proof -
obtain R1 R2 where
‹R1 p q›
‹weak_simulation R1›
‹weak_simulation (λp q. R2 q p)›
‹∀p q. R1 p q ⟶ stable_state p ⟶ R2 p q›
‹∀p q. R2 p q ⟶ stable_state q ⟶ R1 p q›
using assms(1) unfolding s_coupled_simulation_san12_def by blast
moreover hence ‹R2 p q› using assms(2) by blast
ultimately show ?thesis unfolding s_coupled_simulation_san12_def by blast
qed
lemma s_coupledsim_symm:
assumes
‹p ≡scs q›
shows
‹q ≡scs p›
using assms s_coupled_sim_symm by blast
lemma s_coupledsim_eq_parts:
assumes
‹p ≡scs q›
shows
‹p ⊑scs q›
‹q ⊑scs p›
using assms s_coupledsim_symm by metis+
lemma divergence_free_coupledsims_coincidence_1:
defines
‹R1 ≡ (λ p q . p ⊑cs q ∧ (stable_state p ⟶ stable_state q))› and
‹R2 ≡ (λ p q . q ⊑cs p ∧ (stable_state q ⟶ stable_state p))›
assumes
non_divergent_system: ‹⋀ p . ¬ divergent_state p›
shows
‹s_coupled_simulation_san12 R1 R2›
unfolding s_coupled_simulation_san12_def
proof safe
show ‹weak_simulation R1› unfolding weak_simulation_def
proof safe
fix p q p' a
assume sub_assms:
‹R1 p q›
‹p ⟼a p'›
then obtain q' where q'_def: ‹q ⇒^a q'› ‹p' ⊑cs q'›
using coupled_sim_by_is_coupled_sim unfolding R1_def coupled_simulation_def by blast
show ‹∃q'. R1 p' q' ∧ q ⇒^a q'›
proof (cases ‹stable_state p'›)
case True
obtain q'' where q''_def: ‹q' ⟼* tau q''› ‹q'' ⊑cs p'›
using coupled_sim_by_is_coupled_sim q'_def(2)
unfolding coupled_simulation_weak_simulation by blast
then obtain q''' where q'''_def: ‹q'' ⟼* tau q'''› ‹stable_state q'''›
using non_divergence_implies_eventual_stability non_divergent_system by blast
hence ‹q''' ⊑cs p'›
using coupledsim_step_gla17 coupledsim_trans[OF _ q''_def(2)] by blast
hence ‹p' ⊑cs q'''›
using `stable_state p'` coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm
by blast
moreover have ‹q ⇒^a q'''› using q'_def(1) q''_def(1) q'''_def(1) steps_concat by blast
ultimately show ?thesis using q'''_def(2) unfolding R1_def by blast
next
case False
then show ?thesis using q'_def unfolding R1_def by blast
qed
qed
then show ‹weak_simulation (λp q. R2 q p)› unfolding R1_def R2_def .
next
fix p q
assume
‹R1 p q›
‹stable_state p›
thus ‹R2 p q›
unfolding R1_def R2_def
using coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm by blast
next
fix p q
assume
‹R2 p q›
‹stable_state q›
thus ‹R1 p q›
unfolding R1_def R2_def
using coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm by blast
qed
lemma divergence_free_coupledsims_coincidence_2:
defines
‹R ≡ (λ p q . p ⊑scs q ∨ (∃ q' . q ⟼* tau q' ∧ p ≡scs q'))›
assumes
non_divergent_system: ‹⋀ p . ¬ divergent_state p›
shows
‹coupled_simulation R›
unfolding coupled_simulation_weak_simulation
proof safe
show ‹weak_simulation R›
unfolding weak_simulation_def
proof safe
fix p q p' a
assume sub_assms:
‹R p q›
‹p ⟼a p'›
thus ‹∃q'. R p' q' ∧ q ⇒^a q'›
unfolding R_def
proof (cases ‹p ⊑scs q›)
case True
then obtain q' where ‹p' ⊑scs q'› ‹q ⇒^a q'›
using s_coupled_simulation_san12_def sub_assms(2) weak_sim_ruleformat by metis
thus ‹∃q'. (p' ⊑scs q' ∨ (∃q'a. q' ⟼* tau q'a ∧ p' ≡scs q'a)) ∧ q ⇒^a q'›
by blast
next
case False
then obtain q' where ‹q ⟼* tau q'› ‹p ≡scs q'›
using sub_assms(1) unfolding R_def by blast
then obtain q'' where ‹q' ⇒^a q''› ‹p' ⊑scs q''›
using s_coupled_simulation_san12_def sub_assms(2) weak_sim_ruleformat by metis
hence ‹p' ⊑scs q'' ∧ q ⇒^a q''› using steps_concat `q ⟼* tau q'` by blast
thus ‹∃q'. (p' ⊑scs q' ∨ (∃q'a. q' ⟼* tau q'a ∧ p' ≡scs q'a)) ∧ q ⇒^a q'›
by blast
qed
qed
next
fix p q
assume
‹R p q›
thus ‹∃q'. q ⟼* tau q' ∧ R q' p› unfolding R_def
proof safe
fix R1 R2
assume sub_assms:
‹s_coupled_simulation_san12 R1 R2›
‹R1 p q›
thus ‹∃q'. q ⟼* tau q' ∧ (q' ⊑scs p ∨ (∃q'a. p ⟼* tau q'a ∧ q' ≡scs q'a))›
proof -
obtain p' where ‹stable_state p'› ‹p ⟼* tau p'›
using non_divergent_system non_divergence_implies_eventual_stability by blast
hence ‹p ⇒^τ p'› using tau_tau by blast
then obtain q' where ‹q ⟼* tau q'› ‹p' ⊑scs q'›
using s_coupled_simulation_san12_def weak_sim_weak_premise sub_assms tau_tau
by metis
moreover hence ‹p' ≡scs q'› using `stable_state p'` s_coupledsim_stable_eq by blast
ultimately show ?thesis using `p ⟼* tau p'` s_coupledsim_symm by blast
qed
qed (metis s_coupledsim_symm)
qed
text ‹While this proof follows @{cite "sangiorgi2012"}, we needed to deviate from them by also
requiring rootedness (shared stability) for the compared states.›
theorem divergence_free_coupledsims_coincidence:
assumes
non_divergent_system: ‹⋀ p . ¬ divergent_state p› and
stability_rooted: ‹stable_state p ⟷ stable_state q›
shows
‹(p ≡cs q) = (p ≡scs q)›
proof rule
assume ‹p ≡cs q›
hence ‹p ⊑cs q› ‹q ⊑cs p› by auto
thus ‹p ≡scs q›
using stability_rooted divergence_free_coupledsims_coincidence_1[OF non_divergent_system]
by blast
next
assume ‹p ≡scs q›
thus ‹p ≡cs q›
using stability_rooted divergence_free_coupledsims_coincidence_2[OF non_divergent_system]
s_coupledsim_eq_parts by blast
qed
end
text ‹The following example shows that a system might be related by s-coupled-simulation without
being connected by coupled-simulation.›