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.›