section ‹Coupled Similarity›
theory Coupled_Simulation
imports Weak_Relations
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, simp del: weak_step_tau2_def, safe)
fix x1 x2 R a xa
assume ih: ‹coupled_simulation R› ‹R x1 x2› ‹x1 ⟼a xa›
then obtain q' where ‹x2 ⇒^^ a q'› ‹R xa q'›
unfolding coupled_simulation_def weak_step_tau2_def by blast
thus ‹∃q'. x2 ⇒^^ a q' ∧ (xa ⊑cs q' ∨ greatest_coupled_simulation xa q')›
using ih by blast
next
fix x1 x2 R
assume ih: ‹coupled_simulation R› ‹R x1 x2›
then obtain q' where ‹x2 ⟼* tau q'› ‹R q' x1›
unfolding coupled_simulation_def by blast
thus ‹∃q'. x2 ⟼* tau q' ∧ (q' ⊑cs x1 ∨ greatest_coupled_simulation q' x1)›
using ih by blast
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, auto)
fix x1 x2 x xa
assume ih:
‹R x1 x2›
‹x1 ⟼x xa›
hence ‹x1 = q ∧ x2 = pqc ∨ x1 = pqc ∧ x2 = q ∨ x1 = p ∧ x2 = q› using R_def by auto
thus ‹∃q'. (tau x ⟶ x2 ⟼* tau q') ∧
(¬ tau x ⟶ (∃pq1. x2 ⟼* tau pq1 ∧
(∃pq2. pq1 ⟼x pq2 ∧ pq2 ⟼* tau q'))) ∧
(R xa q' ∨ greatest_coupled_simulation xa q')›
proof safe
assume ‹x1 = q› ‹x2 = pqc›
thus ‹∃q'.
(tau x ⟶ pqc ⟼* tau q') ∧
(¬tau x ⟶ (∃pq1. pqc ⟼* tau pq1 ∧
(∃pq2. pq1 ⟼x pq2 ∧ pq2 ⟼* tau q'))) ∧
(R xa q' ∨ greatest_coupled_simulation xa q')›
using ih `q ⊑cs pqc`
coupled_simulation_implies_weak_simulation[OF gcs_is_coupled_simulation]
unfolding gcs_eq_coupled_sim_by
by (metis (full_types) weak_sim_ruleformat)
next
assume ‹x1 = pqc› ‹x2 = q›
hence ‹x = τ ∧ (xa = q ∨ xa = p)› using ih(2) assms(2) by blast
thus ‹∃q'.
(tau x ⟶ q ⟼* tau q') ∧
(¬ tau x ⟶ (∃pq1. q ⟼* tau pq1 ∧
(∃pq2. pq1 ⟼x pq2 ∧ pq2 ⟼* tau q'))) ∧
(R xa q' ∨ greatest_coupled_simulation xa q')›
unfolding gcs_eq_coupled_sim_by[symmetric]
using steps.refl[of q tau] `p ⊑cs q` tau_tau
by auto
next
assume ‹x1 = p› ‹x2 = q›
thus ‹∃q'.
(tau x ⟶ q ⟼* tau q') ∧
(¬ tau x ⟶ (∃pq1. q ⟼* tau pq1 ∧
(∃pq2. pq1 ⟼x pq2 ∧ pq2 ⟼* tau q'))) ∧
(R xa q' ∨ greatest_coupled_simulation xa q')›
using ih `p ⊑cs q`
coupled_simulation_implies_weak_simulation[OF gcs_is_coupled_simulation]
unfolding gcs_eq_coupled_sim_by
by (metis (full_types) weak_sim_ruleformat)
qed
next
fix x1 x2
assume
‹R x1 x2›
hence ‹x1 = q ∧ x2 = pqc ∨ x1 = pqc ∧ x2 = q ∨ x1 = p ∧ x2 = q› using R_def by auto
thus ‹∃q'. x2 ⟼* tau q' ∧ (R q' x1 ∨ greatest_coupled_simulation q' x1)›
proof (auto)
show ‹∃q'. pqc ⟼* tau q' ∧ (R q' q ∨ greatest_coupled_simulation q' q)›
using ‹R pqc q› steps.simps by blast
next
show ‹∃q'. q ⟼* tau q' ∧ (R q' pqc ∨ greatest_coupled_simulation q' pqc)›
using ‹R1 q pqc› ‹coupled_simulation R1› coupled_similarity_implies_gcs steps.refl
by blast
next
show ‹∃q'. q ⟼* tau q' ∧ (R q' p ∨ greatest_coupled_simulation q' p)›
using assms(1) coupled_simulation_weak_simulation
lts_tau.coupled_similarity_implies_gcs by fastforce
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
‹contrasim R›
‹weak_simulation R›
shows
‹coupled_simulation R›
unfolding coupled_simulation_weak_simulation
using contrasim_implies_coupling assms by blast
lemma coupledsim_implies_contrasim:
assumes
‹coupled_simulation R›
shows
‹contrasim 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 ‹contrasim 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 ⟷ contrasim R ∧ weak_simulation R›
using weak_sim_and_contrasim_implies_coupled_sim
coupledsim_implies_contrasim coupled_simulation_weak_simulation by blast
text ‹If there is a sink every state can reach via tau steps, then weak simulation implies
(and thus coincides with) coupled simulation.›
lemma tau_sink_sim_coupledsim:
assumes
‹⋀ p . (p ⟼* tau sink)›
‹⋀ p . R sink p›
‹weak_simulation R›
shows
‹coupled_simulation R›
unfolding coupled_simulation_def
proof safe
show ‹ ⋀p q p' a. R p q ⟹ p ⟼a p' ⟹ ∃q'. R p' q' ∧ q ⇒^a q'›
using assms(3) unfolding weak_simulation_def by blast
next
fix p q
assume ‹R p q›
hence ‹q ⟼* tau sink ∧ R sink p›
using assms(1,2) by blast
thus ‹∃q'. q ⟼* tau q' ∧ R q' p› by blast
qed
subsection ‹‹τ›-Reachability (and Divergence)›
text ‹Coupled similarity comes close to (weak) bisimilarity in two respects:›
text ‹If there are no ‹τ› transitions, coupled similarity coincides with bisimilarity.›
text ‹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) taufree_contrasim_symm coupledsim_implies_contrasim[OF assms(2)]
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 taufree_contrasim_implies_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) contrasim_implies_coupling coupledsim_implies_contrasim by fastforce
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 described 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 (in 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.›
datatype ex_state = a0 | a1 | a2 | a3 | b0 | b1 | b2
locale ex_lts = lts_tau trans τ
for trans :: ‹ex_state ⇒ nat ⇒ ex_state ⇒ bool› and τ +
assumes
sys:
‹trans = (λ p act q .
1 = act ∧ (p = a0 ∧ q = a1
∨ p = a0 ∧ q = a2
∨ p = a2 ∧ q = a3
∨ p = b0 ∧ q = b1
∨ p = b1 ∧ q = b2) ∨
0 = act ∧ (p = a1 ∧ q = a1))›
‹τ = 0›
begin
lemma no_root_coupled_sim:
fixes R1 R2
assumes
coupled:
‹coupled_simulation_san12 R1 R2› and
root:
‹R1 a0 b0› ‹R2 a0 b0›
shows
False
proof -
have
R1sim:
‹weak_simulation R1› and
R1coupling:
‹∀p q. R1 p q ⟶ (∃q'. q ⟼* tau q' ∧ R2 p q')› and
R2sim:
‹weak_simulation (λp q. R2 q p)›
using coupled unfolding coupled_simulation_san12_def by auto
hence R1sim_rf:
‹⋀ p q. R1 p q ⟹
(∀p' a. p ⟼a p' ⟶
(∃q'. R1 p' q' ∧ (¬ tau a ⟶ q ⇒a q') ∧
(tau a ⟶ q ⟼* tau q')))›
unfolding weak_simulation_def by blast
have ‹a0 ⟼1 a1› using sys by auto
hence ‹∃q'. R1 a1 q' ∧ b0 ⇒1 q'›
using R1sim_rf[OF root(1), rule_format, of 1 a1] tau_def
by (auto simp add: sys)
then obtain q' where q': ‹R1 a1 q'› ‹b0 ⇒1 q'› by blast
have b0_quasi_stable: ‹∀ q' . b0 ⟼*tau q' ⟶ b0 = q'›
using steps_no_step[of b0 tau] tau_def by (auto simp add: sys)
have b0_only_b1: ‹∀ q' . b0 ⟼1 q' ⟶ q' = b1› by (auto simp add: sys)
have b1_quasi_stable: ‹∀ q' . b1 ⟼*tau q' ⟶ b1 = q'›
using steps_no_step[of b1 tau] tau_def by (auto simp add: sys)
have ‹∀ q' . b0 ⇒1 q' ⟶ q' = b1›
using b0_quasi_stable b0_only_b1 b1_quasi_stable by auto
hence ‹q' = b1› using q'(2) by blast
hence ‹R1 a1 b1› using q'(1) by simp
hence ‹R2 a1 b1›
using b1_quasi_stable R1coupling by auto
have b1_b2: ‹b1 ⟼1 b2›
by (auto simp add: sys)
hence a1_sim: ‹∃ q' . R2 q' b2 ∧ a1 ⇒1 q'›
using `R2 a1 b1` R2sim b1_b2
unfolding weak_simulation_def tau_def by (auto simp add: sys)
have a1_quasi_stable: ‹∀ q' . a1 ⟼*tau q' ⟶ a1 = q'›
using steps_loop[of a1] by (auto simp add: sys)
hence a1_stuck: ‹∀ q' . ¬ a1 ⇒1 q'›
by (auto simp add: sys)
show ?thesis using a1_sim a1_stuck by blast
qed
lemma root_s_coupled_sim:
defines
‹R1 ≡ λ a b .
a = a0 ∧ b = b0 ∨
a = a1 ∧ b = b1 ∨
a = a2 ∧ b = b1 ∨
a = a3 ∧ b = b2›
and
‹R2 ≡ λ a b .
a = a0 ∧ b = b0 ∨
a = a2 ∧ b = b1 ∨
a = a3 ∧ b = b2›
shows
coupled:
‹s_coupled_simulation_san12 R1 R2›
unfolding s_coupled_simulation_san12_def
proof safe
show ‹weak_simulation R1›
unfolding weak_simulation_def proof (clarify)
fix p q p' a
show ‹R1 p q ⟹ p ⟼a p' ⟹ ∃q'. R1 p' q' ∧ (q ⇒^a q')›
using step_tau_refl unfolding sys assms tau_def using sys(2) tau_def by (cases p, auto)
qed
next
show ‹weak_simulation (λp q. R2 q p)›
unfolding weak_simulation_def proof (clarify)
fix p q p' a
show ‹R2 q p ⟹ p ⟼a p' ⟹ ∃q'. R2 q' p' ∧ (q ⇒^a q')›
using steps.refl[of _ tau] tau_def unfolding assms sys
using sys(2) tau_def by (cases p, auto)
qed
next
fix p q
assume ‹R1 p q› ‹stable_state p›
thus ‹R2 p q› unfolding assms sys using sys(2) tau_def by auto
next
fix p q
assume ‹R2 p q› ‹stable_state q›
thus ‹R1 p q› unfolding assms sys using tau_def by auto
qed
end
end