This GitLab instance reached the end of its service life. It won't be possible to create new users or projects.

Please read the deprecation notice for more information concerning the deprecation timeline

Visit migration.git.tu-berlin.de (internal network only) to import your old projects to the new GitLab platform 📥

Coupled_Simulation.thy 61.1 KB
Newer Older
benkeks committed
1
section \<open>Coupled Similarity\<close>
2 3 4 5 6 7 8 9 10 11

theory Coupled_Simulation
  imports Weak_Relations
begin

context lts_tau
begin

subsection \<open>Van Glabbeeks's Coupled Simulation\<close>
  
benkeks committed
12 13
text \<open>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.\<close>
14

benkeks committed
15 16
definition coupled_simulation ::
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
17
where
benkeks committed
18 19 20 21 22 23 24 25
  \<open>coupled_simulation R  \<equiv> \<forall> p q . 
    R p q \<longrightarrow> 
      (\<forall> p' a. p \<longmapsto>a p' \<longrightarrow> 
        (\<exists> q'. R p' q' \<and> q \<Rightarrow>^a q')) \<and>
      (\<exists> q'. q \<longmapsto>*tau q' \<and> R q' p)\<close>

abbreviation coupled_simulated_by :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<sqsubseteq>cs  _" [60, 60] 65)
  where \<open>coupled_simulated_by p q \<equiv> \<exists> R . coupled_simulation R \<and> R p q\<close>
26
    
benkeks committed
27 28
abbreviation coupled_similar :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<equiv>cs  _" [60, 60] 65)
  where \<open>coupled_similar p q \<equiv> p \<sqsubseteq>cs q \<and> q \<sqsubseteq>cs p\<close>
29

benkeks committed
30
text \<open>We call \<open>\<sqsubseteq>cs\<close> "coupled simulation preorder" and \<open>\<equiv>cs\<close> coupled similarity.\<close>
31

benkeks committed
32
subsection \<open>Position between Weak Simulation and Weak Bisimulation\<close>
33

benkeks committed
34 35
text \<open>Coupled simulations are special weak simulations, and symmetric weak bisimulations also
  are coupled simulations.\<close>
36 37

lemma coupled_simulation_weak_simulation:
benkeks committed
38 39
  \<open>coupled_simulation R =
    (weak_simulation R \<and> (\<forall> p q . R p q \<longrightarrow> (\<exists> q'. q \<longmapsto>*tau q' \<and> R q' p)))\<close>
40 41 42
  unfolding coupled_simulation_def weak_simulation_def by blast

corollary coupled_simulation_implies_weak_simulation:
benkeks committed
43 44
  assumes \<open>coupled_simulation R\<close>
  shows \<open>weak_simulation R\<close>
45 46 47 48
  using assms unfolding coupled_simulation_weak_simulation ..

corollary coupledsim_enabled_subs:
  assumes
benkeks committed
49 50 51 52
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>weak_enabled p a\<close>
    \<open>\<not> tau a\<close>
  shows \<open>weak_enabled q a\<close>
53 54 55 56
  using assms weak_sim_enabled_subs coupled_simulation_implies_weak_simulation by blast

lemma coupled_simulation_implies_coupling:
  assumes
benkeks committed
57 58
    \<open>coupled_simulation R\<close>
    \<open>R p q\<close>
59
  shows
benkeks committed
60
    \<open>\<exists> q'. q \<longmapsto>*tau q' \<and> R q' p\<close>
61 62 63 64
  using assms unfolding coupled_simulation_weak_simulation by blast

lemma weak_bisim_implies_coupled_sim_gla17:
  assumes
benkeks committed
65 66
    wbisim:   \<open>weak_bisimulation R\<close> and
    symmetry: \<open>\<And> p q . R p q \<Longrightarrow> R q p\<close>
benkeks committed
67
    \<comment>\<open>symmetry is needed here, which is alright because bisimilarity is symmetric.\<close>
benkeks committed
68
  shows \<open>coupled_simulation R\<close>
69 70
unfolding coupled_simulation_def proof safe
  fix p q p' a
benkeks committed
71 72
  assume \<open>R p q\<close> \<open>p \<longmapsto>a  p'\<close>
  thus \<open>\<exists>q'. R p' q' \<and> (q \<Rightarrow>^a  q')\<close>
73 74 75
    using wbisim unfolding weak_bisimulation_def by simp
next
  fix p q 
benkeks committed
76 77
  assume \<open>R p q\<close>
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R q' p\<close> 
78 79 80 81 82
    using symmetry steps.refl[of q tau] by auto
qed

subsection \<open>Coupled Simulation and Silent Steps\<close>

benkeks committed
83 84 85
text \<open>Coupled simulation shares important patterns with weak simulation when it comes to the
  treatment of silent steps.\<close>

86
lemma coupledsim_step_gla17:
benkeks committed
87
  \<open>coupled_simulation (\<lambda> p1 q1 . q1 \<longmapsto>* tau p1)\<close>
88 89 90 91 92
  unfolding coupled_simulation_def
  using lts.steps.simps by metis

corollary coupledsim_step:
  assumes
benkeks committed
93
    \<open>p \<longmapsto>* tau  q\<close>
94
  shows
benkeks committed
95
    \<open>q \<sqsubseteq>cs p\<close>
96 97 98 99 100
  using assms coupledsim_step_gla17 by auto

text \<open>A direct implication of this is that states on a tau loop are coupled similar.\<close>
corollary strongly_tau_connected_coupled_similar:
  assumes
benkeks committed
101 102 103
    \<open>p \<longmapsto>* tau  q\<close>
    \<open>q \<longmapsto>* tau  p\<close>
  shows \<open>p \<equiv>cs q\<close>
104 105 106 107
  using assms coupledsim_step by auto

lemma silent_steps_retain_coupled_simulation:
assumes 
benkeks committed
108 109 110 111 112
  \<open>coupled_simulation R\<close>
  \<open>R p q\<close>
  \<open>p \<longmapsto>* A  p'\<close>
  \<open>A = tau\<close>
shows \<open>\<exists> q' . q \<longmapsto>* A q' \<and> R p' q'\<close>
113 114
  using assms(1,3,2,4) steps_retain_weak_sim
  unfolding coupled_simulation_weak_simulation by blast
benkeks committed
115

116
lemma coupled_simulation_weak_premise:
benkeks committed
117 118 119 120 121 122
  \<open>coupled_simulation R =
   (\<forall> p q . R p q \<longrightarrow>
      (\<forall> p' a. p \<Rightarrow>^a p' \<longrightarrow>
        (\<exists> q'. R p' q' \<and> q \<Rightarrow>^a q')) \<and>
      (\<exists> q'. q \<longmapsto>*tau q' \<and> R q' p))\<close>
  unfolding coupled_simulation_weak_simulation weak_sim_weak_premise by blast
123 124

subsection \<open>Closure, Preorder and Symmetry Properties\<close>
benkeks committed
125 126 127 128

text \<open>The coupled simulation preorder \<open>\<sqsubseteq>cs\<close> @{emph \<open>is\<close>} a preoder and symmetric at the
  stable states.\<close>

129 130
lemma coupledsim_union:
  assumes
benkeks committed
131 132
    \<open>coupled_simulation R1\<close>
    \<open>coupled_simulation R2\<close>
133
  shows
benkeks committed
134
    \<open>coupled_simulation (\<lambda> p q . R1 p q \<or> R2 p q)\<close>
135 136 137
  using assms unfolding coupled_simulation_def by (blast)  
  
lemma coupledsim_refl:
benkeks committed
138
  \<open>p \<sqsubseteq>cs p\<close>
139 140 141 142
  using coupledsim_step steps.refl by auto
    
lemma coupledsim_trans:
  assumes
benkeks committed
143 144
    \<open>p \<sqsubseteq>cs pq\<close>
    \<open>pq \<sqsubseteq>cs q\<close>
145
  shows
benkeks committed
146
    \<open>p \<sqsubseteq>cs q\<close>
147
proof -
benkeks committed
148
  obtain R1 where R1_def: \<open>coupled_simulation R1\<close> \<open>R1 p pq\<close>
149
    using assms(1) by blast
benkeks committed
150
  obtain R2 where R2_def: \<open>coupled_simulation R2\<close> \<open>R2 pq q\<close>
151
    using assms(2) by blast
benkeks committed
152 153
  define R where R_def: \<open>R \<equiv> \<lambda> p q . \<exists> pq . (R1 p pq \<and> R2 pq q) \<or> (R2 p pq \<and> R1 pq q)\<close>
  have \<open>weak_simulation R\<close> \<open>R p q\<close>
154 155 156 157 158
    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
benkeks committed
159
  moreover have \<open>(\<forall> p q . R p q \<longrightarrow> (\<exists> q'. q \<longmapsto>*tau q' \<and> R q' p))\<close>
160 161 162
    unfolding R_def
  proof safe
    fix p q pq
benkeks committed
163 164
    assume r1r2: \<open>R1 p pq\<close> \<open>R2 pq q\<close>
    then obtain pq' where \<open>R1 pq' p\<close> \<open>pq \<longmapsto>* tau  pq'\<close>
165
      using r1r2 R1_def(1) unfolding coupled_simulation_weak_premise by blast
benkeks committed
166
    then moreover obtain q' where \<open>R2 pq' q'\<close> \<open>q \<longmapsto>* tau q'\<close>
167 168
      using r1r2 R2_def(1) weak_step_tau_tau[OF `pq \<longmapsto>* tau  pq'`] tau_tau
      unfolding coupled_simulation_weak_premise by blast
benkeks committed
169
    then moreover obtain q'' where \<open>R2 q'' pq'\<close> \<open>q' \<longmapsto>* tau  q''\<close>
170
      using R2_def(1) unfolding coupled_simulation_weak_premise by blast
benkeks committed
171
    ultimately show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (\<exists>pq. R1 q' pq \<and> R2 pq p \<or> R2 q' pq \<and> R1 pq p)\<close>
172
      using steps_concat by blast
benkeks committed
173
  next \<comment>\<open>analogous with R2 and R1 swapped\<close>
174
    fix p q pq
benkeks committed
175 176
    assume r2r1: \<open>R2 p pq\<close> \<open>R1 pq q\<close>
    then obtain pq' where \<open>R2 pq' p\<close> \<open>pq \<longmapsto>* tau  pq'\<close>
177
      using r2r1 R2_def(1) unfolding coupled_simulation_weak_premise by blast
benkeks committed
178
    then moreover obtain q' where \<open>R1 pq' q'\<close> \<open>q \<longmapsto>* tau q'\<close>
179 180
      using r2r1 R1_def(1) weak_step_tau_tau[OF `pq \<longmapsto>* tau  pq'`] tau_tau
      unfolding coupled_simulation_weak_premise by blast
benkeks committed
181
    then moreover obtain q'' where \<open>R1 q'' pq'\<close> \<open>q' \<longmapsto>* tau  q''\<close>
182
      using R1_def(1) unfolding coupled_simulation_weak_premise by blast
benkeks committed
183
    ultimately show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (\<exists>pq. R1 q' pq \<and> R2 pq p \<or> R2 q' pq \<and> R1 pq p)\<close>
184 185
      using steps_concat by blast
  qed
benkeks committed
186
  ultimately have \<open>R p q\<close> \<open>coupled_simulation R\<close>
187 188 189 190
    using coupled_simulation_weak_simulation by auto
  thus ?thesis by blast
qed

benkeks committed
191 192 193
interpretation preorder \<open>\<lambda> p q. p \<sqsubseteq>cs q\<close> \<open>\<lambda> p q. p \<sqsubseteq>cs q \<and> \<not>(q \<sqsubseteq>cs p)\<close>
  by (standard, blast, fact coupledsim_refl, fact coupledsim_trans)

194
lemma coupled_similarity_equivalence:
benkeks committed
195
  \<open>equivp (\<lambda> p q. p \<equiv>cs q)\<close>
196
proof (rule equivpI)
benkeks committed
197 198
  show \<open>reflp coupled_similar\<close>
    unfolding reflp_def by blast
199
next
benkeks committed
200
  show \<open>symp coupled_similar\<close>
201 202
    unfolding symp_def by blast
next
benkeks committed
203
  show \<open>transp coupled_similar\<close>
204 205 206 207 208
    unfolding transp_def using coupledsim_trans by meson
qed

lemma coupledsim_tau_max_eq:
  assumes
benkeks committed
209 210 211
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>tau_max q\<close>
  shows  \<open>p \<equiv>cs q\<close> 
212 213 214 215
  using assms using coupled_simulation_weak_simulation coupling_tau_max_symm by metis

corollary coupledsim_stable_eq:
  assumes
benkeks committed
216 217 218
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>stable_state q\<close>
  shows  \<open>p \<equiv>cs q\<close> 
219 220 221 222
  using assms using coupled_simulation_weak_simulation coupling_stability_symm by metis

subsection \<open>Coinductive Coupled Simulation Preorder\<close>

benkeks committed
223 224 225 226
text \<open>\<open>\<sqsubseteq>cs\<close> can also be characterized coinductively. \<open>\<sqsubseteq>cs\<close> is the greatest
  coupled simulation.\<close>

coinductive greatest_coupled_simulation :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close>
227
  where gcs:
benkeks committed
228
    \<open>\<lbrakk>\<And> a p' . p \<longmapsto>a p' \<Longrightarrow> \<exists>q'. q \<Rightarrow>^^ a q' \<and> greatest_coupled_simulation p' q'; 
229
      \<exists> q' . q \<longmapsto>* tau q' \<and> greatest_coupled_simulation q' p\<rbrakk>
benkeks committed
230
  \<Longrightarrow> greatest_coupled_simulation p q\<close>
231 232

lemma gcs_implies_gws:
benkeks committed
233 234
  assumes \<open>greatest_coupled_simulation p q\<close>
  shows \<open>greatest_weak_simulation p q\<close>
235 236 237
  using assms by (metis greatest_coupled_simulation.cases greatest_weak_simulation.coinduct)

lemma gcs_is_coupled_simulation:
benkeks committed
238
  shows \<open>coupled_simulation greatest_coupled_simulation\<close>
239 240
  unfolding coupled_simulation_def
proof safe
benkeks committed
241
  \<comment>\<open>identical to ws\<close>
242 243
  fix p q p' a
  assume ih:
benkeks committed
244 245 246
    \<open>greatest_coupled_simulation p q\<close>
    \<open>p \<longmapsto>a  p'\<close>
  hence \<open>(\<forall>x xa. p \<longmapsto>x xa \<longrightarrow> (\<exists>q'. q \<Rightarrow>^^ x  q' \<and> greatest_coupled_simulation xa q'))\<close>
247
    by (meson greatest_coupled_simulation.simps)
benkeks committed
248 249
  then obtain q' where \<open>q \<Rightarrow>^^ a  q' \<and> greatest_coupled_simulation p' q'\<close> using ih by blast
  thus \<open>\<exists>q'. greatest_coupled_simulation p' q' \<and> q \<Rightarrow>^a  q'\<close>
250 251 252 253
    unfolding weak_step_tau2_def by blast
next
  fix p q
  assume
benkeks committed
254 255
    \<open>greatest_coupled_simulation p q\<close>
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> greatest_coupled_simulation q' p\<close>
256 257 258 259
    by (meson greatest_coupled_simulation.simps)
qed

lemma coupled_similarity_implies_gcs:
benkeks committed
260 261
  assumes \<open>p \<sqsubseteq>cs q\<close>
  shows \<open>greatest_coupled_simulation p q\<close>
262 263 264
  using assms
proof (coinduct, simp del: weak_step_tau2_def, safe)
  fix x1 x2 R a xa
benkeks committed
265 266
  assume ih: \<open>coupled_simulation R\<close> \<open>R x1 x2\<close> \<open>x1 \<longmapsto>a  xa\<close>
  then obtain q' where \<open>x2 \<Rightarrow>^^ a  q'\<close> \<open>R xa q'\<close>
267
    unfolding coupled_simulation_def weak_step_tau2_def by blast
benkeks committed
268
  thus \<open>\<exists>q'. x2 \<Rightarrow>^^ a  q' \<and> (xa \<sqsubseteq>cs  q' \<or> greatest_coupled_simulation xa q')\<close>
269 270 271
    using ih by blast
next
  fix x1 x2 R
benkeks committed
272 273
  assume ih: \<open>coupled_simulation R\<close> \<open>R x1 x2\<close>
  then obtain q' where \<open>x2 \<longmapsto>* tau  q'\<close> \<open>R q' x1\<close>
274
    unfolding coupled_simulation_def by blast
benkeks committed
275
  thus \<open>\<exists>q'. x2 \<longmapsto>* tau  q' \<and> (q' \<sqsubseteq>cs  x1 \<or> greatest_coupled_simulation q' x1)\<close>
276 277 278 279
    using ih by blast
qed

lemma gcs_eq_coupled_sim_by:
benkeks committed
280
  shows \<open>p \<sqsubseteq>cs q = greatest_coupled_simulation p q\<close>
281 282 283 284
  using coupled_similarity_implies_gcs gcs_is_coupled_simulation by blast

lemma coupled_sim_by_is_coupled_sim:
  shows
benkeks committed
285
    \<open>coupled_simulation (\<lambda> p q . p \<sqsubseteq>cs q)\<close>
286 287 288
  unfolding gcs_eq_coupled_sim_by using gcs_is_coupled_simulation .

lemma coupledsim_unfold:
benkeks committed
289 290 291
  shows \<open>p \<sqsubseteq>cs q =
    ((\<forall>a p'. p \<longmapsto>a  p' \<longrightarrow> (\<exists>q'. q \<Rightarrow>^a  q' \<and> p' \<sqsubseteq>cs q')) \<and>
       (\<exists>q'. q \<longmapsto>* tau  q' \<and> q' \<sqsubseteq>cs p))\<close>
292 293 294 295 296
  unfolding gcs_eq_coupled_sim_by weak_step_tau2_def[symmetric]
  by (metis lts_tau.greatest_coupled_simulation.simps)

subsection \<open>Coupled Simulation Join\<close>

benkeks committed
297 298 299 300
text \<open>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 \<open>\<sqsubseteq>cs\<close> taking \<open>\<equiv>cs\<close>
  as equality.\<close>

301 302
lemma coupledsim_choice_1:
  assumes 
benkeks committed
303 304
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>\<And> pq a . pqc \<longmapsto>a pq \<longleftrightarrow> (a = \<tau> \<and> (pq = p \<or> pq = q))\<close>
305
  shows
benkeks committed
306 307
    \<open>pqc \<sqsubseteq>cs q\<close>
    \<open>q \<sqsubseteq>cs pqc\<close>
308
proof -
benkeks committed
309 310
  define R1 where \<open>R1 \<equiv> (\<lambda>p1 q1. q1 \<longmapsto>* tau  p1)\<close>
  have \<open>R1 q pqc\<close>
311
    using assms(2) steps_one_step R1_def by simp
benkeks committed
312
  moreover have \<open>coupled_simulation R1\<close>
313
    unfolding R1_def using coupledsim_step_gla17 .
benkeks committed
314
  ultimately show q_pqc: \<open>q \<sqsubseteq>cs pqc\<close> by blast
benkeks committed
315
\<comment>\<open>next case\<close>
benkeks committed
316 317 318
  define R where \<open>R \<equiv> \<lambda> p0 q0 . p0 = q \<and> q0 = pqc \<or> p0 = pqc \<and> q0 = q \<or> p0 = p \<and> q0 = q\<close>
  hence \<open>R pqc q\<close> by blast
  thus \<open>pqc \<sqsubseteq>cs  q\<close>
319 320 321 322
    unfolding gcs_eq_coupled_sim_by
  proof (coinduct, auto)
    fix x1 x2 x xa
    assume ih:
benkeks committed
323 324 325 326 327 328 329
      \<open>R x1 x2\<close>
      \<open>x1 \<longmapsto>x  xa\<close>
    hence \<open>x1 = q \<and> x2 = pqc \<or> x1 = pqc \<and> x2 = q \<or> x1 = p \<and> x2 = q\<close> using R_def by auto
    thus \<open>\<exists>q'. (tau x \<longrightarrow> x2 \<longmapsto>* tau  q') \<and>
      (\<not> tau x \<longrightarrow> (\<exists>pq1. x2 \<longmapsto>* tau  pq1 \<and>
        (\<exists>pq2. pq1 \<longmapsto>x  pq2 \<and> pq2 \<longmapsto>* tau  q'))) \<and>
      (R xa q' \<or> greatest_coupled_simulation xa q')\<close>
330
    proof safe
benkeks committed
331 332 333 334 335 336
      assume \<open>x1 = q\<close> \<open>x2 = pqc\<close>
      thus \<open>\<exists>q'.
        (tau x \<longrightarrow> pqc \<longmapsto>* tau  q') \<and>
        (\<not>tau x \<longrightarrow> (\<exists>pq1. pqc \<longmapsto>* tau  pq1 \<and>
          (\<exists>pq2. pq1 \<longmapsto>x  pq2 \<and> pq2 \<longmapsto>* tau  q'))) \<and>
        (R xa q' \<or> greatest_coupled_simulation xa q')\<close> 
337 338 339 340 341
        using ih `q \<sqsubseteq>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
benkeks committed
342 343 344 345 346 347 348
      assume \<open>x1 = pqc\<close> \<open>x2 = q\<close>
      hence \<open>x = \<tau> \<and> (xa = q \<or> xa = p)\<close> using ih(2) assms(2) by blast
      thus \<open>\<exists>q'.
        (tau x \<longrightarrow> q \<longmapsto>* tau  q') \<and>
        (\<not> tau x \<longrightarrow> (\<exists>pq1. q \<longmapsto>* tau  pq1 \<and>
          (\<exists>pq2. pq1 \<longmapsto>x  pq2 \<and> pq2 \<longmapsto>* tau  q'))) \<and>
        (R xa q' \<or> greatest_coupled_simulation xa q')\<close>
349
        unfolding gcs_eq_coupled_sim_by[symmetric] 
benkeks committed
350
        using steps.refl[of q tau] `p \<sqsubseteq>cs q` tau_tau
351 352
        by auto
    next
benkeks committed
353 354 355 356 357 358
      assume \<open>x1 = p\<close> \<open>x2 = q\<close>
      thus \<open>\<exists>q'.
         (tau x \<longrightarrow> q \<longmapsto>* tau  q') \<and>
         (\<not> tau x \<longrightarrow> (\<exists>pq1. q \<longmapsto>* tau  pq1 \<and>
            (\<exists>pq2. pq1 \<longmapsto>x  pq2 \<and> pq2 \<longmapsto>* tau  q'))) \<and>
         (R xa q' \<or> greatest_coupled_simulation xa q')\<close>
359 360 361 362 363 364 365 366
        using ih `p \<sqsubseteq>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
benkeks committed
367 368 369
      \<open>R x1 x2\<close>
    hence \<open>x1 = q \<and> x2 = pqc \<or> x1 = pqc \<and> x2 = q \<or> x1 = p \<and> x2 = q\<close> using R_def by auto
    thus \<open>\<exists>q'. x2 \<longmapsto>* tau  q' \<and> (R q' x1 \<or> greatest_coupled_simulation q' x1)\<close>
370
    proof (auto)
benkeks committed
371
      show \<open>\<exists>q'. pqc \<longmapsto>* tau  q' \<and> (R q' q \<or> greatest_coupled_simulation q' q)\<close>
372 373
        using \<open>R pqc q\<close> steps.simps by blast
    next
benkeks committed
374 375 376
      show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (R q' pqc \<or> greatest_coupled_simulation q' pqc)\<close>
        using \<open>R1 q pqc\<close> \<open>coupled_simulation R1\<close> coupled_similarity_implies_gcs steps.refl
        by blast
377
    next
benkeks committed
378
      show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (R q' p \<or> greatest_coupled_simulation q' p)\<close>
379 380 381 382 383 384 385 386
        using assms(1) coupled_simulation_weak_simulation
          lts_tau.coupled_similarity_implies_gcs by fastforce
    qed
  qed
qed

lemma coupledsim_choice_2:
  assumes 
benkeks committed
387 388
    \<open>pqc \<sqsubseteq>cs q\<close> 
    \<open>\<And> pq a . pqc \<longmapsto>a pq \<longleftrightarrow> (a = \<tau> \<and> (pq = p \<or> pq = q))\<close>
389
  shows
benkeks committed
390
    \<open>p \<sqsubseteq>cs q\<close>
391
proof -
benkeks committed
392 393
  have \<open>pqc \<longmapsto>\<tau> p\<close> using assms(2) by blast
  then obtain q' where \<open>q \<longmapsto>* tau q'\<close> \<open>p \<sqsubseteq>cs q'\<close>
394
    using assms(1) tau_tau unfolding coupled_simulation_def by blast
benkeks committed
395
  then moreover have \<open>q' \<sqsubseteq>cs q\<close> using coupledsim_step_gla17 by blast
396 397 398 399 400
  ultimately show ?thesis using coupledsim_trans tau_tau by blast
qed

lemma coupledsim_choice_join:
  assumes 
benkeks committed
401
    \<open>\<And> pq a . pqc \<longmapsto>a pq \<longleftrightarrow> (a = \<tau> \<and> (pq = p \<or> pq = q))\<close>
402
  shows
benkeks committed
403
    \<open>p \<sqsubseteq>cs q \<longleftrightarrow> pqc \<equiv>cs q\<close>
404 405
  using  coupledsim_choice_1[OF _ assms] coupledsim_choice_2[OF _ assms] by blast

benkeks committed
406 407 408 409
subsection \<open>Coupled Delay Simulation\<close>

text \<open>\<open>\<sqsubseteq>cs\<close> can also be characterized in terms of coupled delay simulations, which are
 conceptionally simpler than van Glabbeek's coupled simulation definition.\<close>
410

benkeks committed
411 412 413 414 415 416 417 418 419 420 421
text \<open>In the greatest coupled simulation, \<open>\<tau>\<close>-challenges can be answered by stuttering.\<close>
lemma coupledsim_tau_challenge_trivial:
  assumes 
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>p \<longmapsto>* tau p'\<close>
  shows
    \<open>p' \<sqsubseteq>cs q\<close>
  using assms coupledsim_trans coupledsim_step by blast

lemma coupled_similarity_s_delay_simulation:
  \<open>delay_simulation (\<lambda> p q. p \<sqsubseteq>cs q)\<close>
422 423 424 425
  unfolding delay_simulation_def
proof safe
  fix p q R p' a
  assume assms:
benkeks committed
426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451
    \<open>coupled_simulation R\<close>
    \<open>R p q\<close>
    \<open>p \<longmapsto>a p'\<close>
  {
    assume \<open>tau a\<close>
    then show \<open>p' \<sqsubseteq>cs  q\<close>
      using assms coupledsim_tau_challenge_trivial steps_one_step by blast
  } {
    show \<open>\<exists>q'. p' \<sqsubseteq>cs  q' \<and> q =\<rhd>a  q'\<close>
    proof -
      obtain q''' where q'''_spec: \<open>q \<Rightarrow>^a q'''\<close> \<open>p' \<sqsubseteq>cs q'''\<close>
        using assms coupled_simulation_implies_weak_simulation weak_sim_ruleformat by metis
      show ?thesis
      proof (cases \<open>tau a\<close>)
        case True
        then have \<open>q \<longmapsto>* tau q'''\<close> 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:
            \<open>q \<longmapsto>* tau q'\<close> \<open>q' \<longmapsto>a q''\<close> \<open>q'' \<longmapsto>* tau q'''\<close>
          using q'''_spec by blast
        hence \<open>q''' \<sqsubseteq>cs q''\<close> using coupledsim_step by blast
        hence \<open>p' \<sqsubseteq>cs q''\<close> using q'''_spec(2) coupledsim_trans by blast
        thus ?thesis using q'q''_spec(1,2) False by blast
      qed
452
    qed
benkeks committed
453
  }
454 455
qed

456
definition coupled_delay_simulation ::
benkeks committed
457
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
458
  where
benkeks committed
459 460
  \<open>coupled_delay_simulation R  \<equiv>
    delay_simulation R \<and> coupling R\<close>
461

benkeks committed
462 463
lemma coupled_sim_by_eq_coupled_delay_simulation:
  \<open>(p \<sqsubseteq>cs q) = (\<exists>R. R p q \<and> coupled_delay_simulation R)\<close>
464
  unfolding coupled_delay_simulation_def
465
proof
benkeks committed
466 467 468 469
  assume \<open>p \<sqsubseteq>cs q\<close>
  define R where \<open>R \<equiv> coupled_simulated_by\<close>
  hence \<open>R p q \<and> delay_simulation R \<and> coupling R\<close>
    using coupled_similarity_s_delay_simulation coupled_sim_by_is_coupled_sim
470
        coupled_simulation_implies_coupling \<open>p \<sqsubseteq>cs q\<close> by blast
benkeks committed
471
  thus \<open>\<exists>R. R p q \<and> delay_simulation R \<and> coupling R\<close> by blast
472
next
benkeks committed
473 474 475
  assume \<open>\<exists>R. R p q \<and> delay_simulation R \<and> coupling R\<close>
  then obtain R where \<open>R p q\<close> \<open>delay_simulation R\<close> \<open>coupling R\<close> by blast
  hence \<open>coupled_simulation R\<close>
476
    using delay_simulation_implies_weak_simulation coupled_simulation_weak_simulation by blast
benkeks committed
477 478 479 480 481 482
  thus \<open>p \<sqsubseteq>cs q\<close> using \<open>R p q\<close> by blast
qed

subsection \<open>Relationship to Contrasimulation and Weak Simulation\<close>

text \<open>Coupled simulation is precisely the intersection of contrasimulation and weak simulation.\<close>
483 484 485

lemma weak_sim_and_contrasim_implies_coupled_sim:
  assumes
benkeks committed
486 487
    \<open>contrasim R\<close>
    \<open>weak_simulation R\<close>
488
  shows
benkeks committed
489
    \<open>coupled_simulation R\<close>
490 491 492 493 494
  unfolding coupled_simulation_weak_simulation
  using contrasim_implies_coupling assms by blast

lemma coupledsim_implies_contrasim:
  assumes
benkeks committed
495
    \<open>coupled_simulation R\<close>
496
  shows 
benkeks committed
497
    \<open>contrasim R\<close>
498
proof -
benkeks committed
499
  have \<open>contrasim_step R\<close>
500 501 502 503
  unfolding contrasim_step_def
  proof (rule allI impI)+
    fix p q p' a
    assume
benkeks committed
504 505
      \<open>R p q \<and> p \<Rightarrow>^a  p'\<close>
    then obtain q' where q'_def: \<open>R p' q'\<close> \<open>q \<Rightarrow>^a  q'\<close>
506
      using assms unfolding coupled_simulation_weak_premise by blast
benkeks committed
507
    then obtain q'' where q''_def: \<open>R q'' p'\<close> \<open>q' \<longmapsto>* tau  q''\<close>
508
      using assms unfolding coupled_simulation_weak_premise by blast
benkeks committed
509 510
    then have \<open>q \<Rightarrow>^a  q''\<close> using q'_def(2) steps_concat by blast
    thus \<open>\<exists>q'. q \<Rightarrow>^a  q' \<and> R q' p'\<close>
511 512
      using q''_def(1) by blast
  qed
benkeks committed
513
  thus \<open>contrasim R\<close> using contrasim_step_seq_coincide_for_sims
514 515 516 517
      coupled_simulation_implies_weak_simulation[OF assms] by blast 
qed

lemma coupled_simulation_iff_weak_sim_and_contrasim:
benkeks committed
518
  shows \<open>coupled_simulation R \<longleftrightarrow> contrasim R \<and> weak_simulation R\<close>
519 520 521 522 523 524 525
  using weak_sim_and_contrasim_implies_coupled_sim
    coupledsim_implies_contrasim coupled_simulation_weak_simulation by blast

text \<open>If there is a sink every state can reach via tau steps, then weak simulation implies
  (and thus coincides with) coupled simulation.\<close>
lemma tau_sink_sim_coupledsim:
  assumes
benkeks committed
526 527 528
    \<open>\<And> p . (p \<longmapsto>* tau sink)\<close>
    \<open>\<And> p . R sink p\<close>
    \<open>weak_simulation R\<close>
529
  shows
benkeks committed
530
    \<open>coupled_simulation R\<close>
531 532
  unfolding coupled_simulation_def
proof safe
benkeks committed
533
  show \<open> \<And>p q p' a. R p q \<Longrightarrow> p \<longmapsto>a  p' \<Longrightarrow> \<exists>q'. R p' q' \<and> q \<Rightarrow>^a  q'\<close>
534 535 536
    using assms(3) unfolding weak_simulation_def by blast
next
  fix p q
benkeks committed
537 538
  assume \<open>R p q\<close>
  hence \<open>q \<longmapsto>* tau sink \<and> R sink p\<close>
539
    using assms(1,2) by blast
benkeks committed
540
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R q' p\<close> by blast
541 542
qed

benkeks committed
543 544 545 546 547 548 549 550 551
subsection \<open>\<open>\<tau>\<close>-Reachability (and Divergence)\<close>

text \<open>Coupled similarity comes close to (weak) bisimilarity in two respects:\<close>

text \<open>If there are no \<open>\<tau>\<close> transitions, coupled similarity coincides with bisimilarity.\<close>

text \<open>If there are only finite \<open>\<tau>\<close> reachable portions, then coupled similarity contains a
  bisimilarity on the \<open>\<tau>\<close>-maximal states. (For this,  \<open>\<tau>\<close>-cycles have to be ruled out, which, as
  we show, is no problem because their removal is transparent to coupled similarity.) \<close>
552 553 554

lemma taufree_coupledsim_symm:
  assumes
benkeks committed
555 556 557 558 559 560
    \<open>\<And> p1 a p2 . (p1 \<longmapsto>a p2 \<Longrightarrow> \<not> tau a)\<close>
    \<open>coupled_simulation R\<close>
    \<open>R p q\<close>
  shows \<open>R q p\<close>
  using assms(1,3) taufree_contrasim_symm coupledsim_implies_contrasim[OF assms(2)]
  by blast
561 562 563

lemma taufree_coupledsim_weak_bisim:
  assumes
benkeks committed
564 565 566 567 568
    \<open>\<And> p1 a p2 . (p1 \<longmapsto>a p2 \<Longrightarrow> \<not> tau a)\<close>
    \<open>coupled_simulation R\<close>
  shows \<open>weak_bisimulation R\<close>
  using assms taufree_contrasim_implies_weak_bisim coupledsim_implies_contrasim[OF assms(2)]
  by blast
569 570 571

lemma coupledsim_stable_state_symm:
  assumes
benkeks committed
572 573 574
    \<open>coupled_simulation R\<close>
    \<open>R p q\<close>
    \<open>stable_state q\<close>
575
  shows
benkeks committed
576
    \<open>R q p\<close>
577 578
  using assms steps_left unfolding coupled_simulation_def by metis

benkeks committed
579
text \<open>In finite systems, coupling is guaranteed to happen through \<open>\<tau>\<close>-maximal states.\<close>
580 581
lemma coupledsim_max_coupled:
  assumes 
benkeks committed
582 583 584
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>\<And> r1 r2 . r1 \<longmapsto>* tau r2 \<and> r2 \<longmapsto>* tau r1 \<Longrightarrow> r1 = r2\<close> \<comment>\<open>contracted tau cycles\<close>
    \<open>\<And> r. finite {r'. r \<longmapsto>* tau r'}\<close>
585
  shows
benkeks committed
586
    \<open>\<exists> q' . q \<longmapsto>* tau q' \<and> q' \<sqsubseteq>cs p \<and> tau_max q'\<close>
587
proof -
benkeks committed
588
  obtain q1 where q1_spec: \<open>q \<longmapsto>* tau q1\<close> \<open>q1 \<sqsubseteq>cs p\<close> 
589
    using assms(1) contrasim_implies_coupling coupledsim_implies_contrasim by fastforce
benkeks committed
590
  then obtain q' where \<open>q1 \<longmapsto>* tau q'\<close> \<open>(\<forall>q''. q' \<longmapsto>* tau q'' \<longrightarrow> q' = q'')\<close>
591
    using tau_max_deadlock assms(2,3) by blast
benkeks committed
592
  then moreover have \<open>q' \<sqsubseteq>cs p\<close> \<open>q \<longmapsto>* tau q'\<close>
593 594 595 596 597
    using q1_spec coupledsim_trans coupledsim_step steps_concat[of q1 tau q' q]
    by blast+
  ultimately show ?thesis by blast
qed

benkeks committed
598 599 600
text \<open>In the greatest coupled simulation, \<open>a\<close>-challenges can be answered by a weak move without
  trailing \<open>\<tau>\<close>-steps. (This property is what bridges the gap between weak and delay simulation for 
  coupled simulation.)\<close>
601 602
lemma coupledsim_step_challenge_short_answer:
  assumes 
benkeks committed
603 604 605
    \<open>p \<sqsubseteq>cs q\<close>
    \<open>p \<longmapsto>a p'\<close>
    \<open>\<not> tau a\<close>
606
  shows
benkeks committed
607 608 609 610
    \<open>\<exists> q' q1. p' \<sqsubseteq>cs q' \<and> q \<longmapsto>* tau q1 \<and> q1 \<longmapsto>a q'\<close>
  using assms
  unfolding coupled_sim_by_eq_coupled_delay_simulation
    coupled_delay_simulation_def delay_simulation_def by blast
611

benkeks committed
612
text \<open>If two states share the same outgoing edges with except for one \<open>\<tau>\<close>-loop, then they cannot
613 614 615
  be distinguished by coupled similarity.\<close>
lemma coupledsim_tau_loop_ignorance:
  assumes
benkeks committed
616
    \<open>\<And> a p'. p \<longmapsto>a p' \<or> p' = pp \<and> a = \<tau> \<longleftrightarrow> pp \<longmapsto>a p'\<close>
617
  shows
benkeks committed
618
    \<open>pp \<equiv>cs p\<close>
619
proof -
benkeks committed
620 621
  define R where \<open>R \<equiv> \<lambda> p1 q1. p1 = q1 \<or> p1 = pp \<and> q1 = p \<or> p1 = p \<and> q1 = pp\<close>
  have \<open>coupled_simulation R\<close>
622 623 624 625
    unfolding coupled_simulation_def R_def
  proof (safe)
    fix pa q p' a
    assume
benkeks committed
626 627
      \<open>q \<longmapsto>a  p'\<close>
    thus \<open>\<exists>q'. (p' = q' \<or> p' = pp \<and> q' = p \<or> p' = p \<and> q' = pp) \<and> q \<Rightarrow>^a  q'\<close>
628 629 630
      using assms step_weak_step_tau by auto
  next
    fix pa q
benkeks committed
631
    show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (q' = q \<or> q' = pp \<and> q = p \<or> q' = p \<and> q = pp)\<close>
632 633 634 635
      using steps.refl by blast
  next
    fix pa q p' a
    assume
benkeks committed
636 637
      \<open>pp \<longmapsto>a  p'\<close>
    thus \<open>\<exists>q'. (p' = q' \<or> p' = pp \<and> q' = p \<or> p' = p \<and> q' = pp) \<and> p \<Rightarrow>^a  q'\<close>
638 639 640
      using assms by (metis lts.steps.simps tau_def)
  next
    fix pa q
benkeks committed
641
    show \<open>\<exists>q'. p \<longmapsto>* tau  q' \<and> (q' = pp \<or> q' = pp \<and> pp = p \<or> q' = p \<and> pp = pp)\<close>
642 643 644 645
      using steps.refl[of p tau] by blast
  next
    fix pa q p' a
    assume
benkeks committed
646 647
      \<open>p \<longmapsto>a  p'\<close>
    thus \<open>\<exists>q'. (p' = q' \<or> p' = pp \<and> q' = p \<or> p' = p \<and> q' = pp) \<and> pp \<Rightarrow>^a  q'\<close>
648 649 650
      using assms step_weak_step_tau by fastforce
  next
    fix pa q
benkeks committed
651
    show \<open>\<exists>q'. pp \<longmapsto>* tau  q' \<and> (q' = p \<or> q' = pp \<and> p = p \<or> q' = p \<and> p = pp)\<close>
652 653
      using steps.refl[of pp tau] by blast
  qed
benkeks committed
654
  moreover have \<open>R p pp\<close> \<open>R pp p\<close> unfolding R_def by auto
655 656 657
  ultimately show ?thesis by blast
qed

benkeks committed
658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717
subsection \<open>On the Connection to Weak Bisimulation\<close>

text \<open>When one only considers steps leading to \<open>\<tau>\<close>-maximal states in a system without infinite
  \<open>\<tau>\<close>-reachable regions (e.g. a finite system), then \<open>\<equiv>cs\<close> on these steps is a bisimulation.\<close>

text \<open>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.\<close>
lemma coupledsim_eventual_symmetry:
  assumes
    contracted_cycles: \<open>\<And> r1 r2 . r1 \<longmapsto>* tau r2 \<and> r2 \<longmapsto>* tau r1 \<Longrightarrow> r1 = r2\<close> and
    finite_taus: \<open>\<And> r. finite {r'. r \<longmapsto>* tau r'}\<close> and
    cs: \<open>p \<sqsubseteq>cs q\<close> and
    step: \<open>p \<Rightarrow>^a p'\<close> and
    tau_max_p': \<open>tau_max p'\<close>
  shows
    \<open>\<exists> q'. tau_max q' \<and> q \<Rightarrow>^a q' \<and> p' \<equiv>cs q'\<close>
proof-
  obtain q' where q'_spec: \<open>q \<Rightarrow>^a q'\<close> \<open>p' \<sqsubseteq>cs q'\<close>
    using cs step unfolding coupled_simulation_weak_premise by blast
  then obtain q'' where q''_spec: \<open>q' \<longmapsto>* tau q''\<close> \<open>q'' \<sqsubseteq>cs p'\<close>
    using cs unfolding coupled_simulation_weak_simulation by blast
  then obtain q_max where q_max_spec: \<open>q'' \<longmapsto>* tau q_max\<close> \<open>tau_max q_max\<close> 
    using tau_max_deadlock contracted_cycles finite_taus by force
  hence \<open>q_max \<sqsubseteq>cs p'\<close> using q''_spec coupledsim_tau_challenge_trivial by blast
  hence \<open>q_max \<equiv>cs p'\<close> using tau_max_p' coupledsim_tau_max_eq by blast
  moreover have \<open>q \<Rightarrow>^a q_max\<close> using q_max_spec q'_spec q''_spec steps_concat by blast
  ultimately show ?thesis using q_max_spec(2) by blast
qed

text \<open>Even without the assumption that the left-hand-side step \<open>p \<Rightarrow>^a p'\<close> ends in a \<open>\<tau>\<close>-maximal state,
a situation resembling bismulation can be set up -- with the drawback that it only refers to
a \<open>\<tau>\<close>-maximal sibling of \<open>p'\<close>.\<close>
lemma coupledsim_eventuality_2:
  assumes
    contracted_cycles: \<open>\<And> r1 r2 . r1 \<longmapsto>* tau r2 \<and> r2 \<longmapsto>* tau r1 \<Longrightarrow> r1 = r2\<close> and
    finite_taus: \<open>\<And> r. finite {r'. r \<longmapsto>* tau r'}\<close> and
    cbisim: \<open>p \<equiv>cs q\<close> and
    step: \<open>p \<Rightarrow>^a p'\<close>
  shows
    \<open>\<exists> p'' q'. tau_max p'' \<and> tau_max q' \<and> p \<Rightarrow>^a p'' \<and> q \<Rightarrow>^a q' \<and> p'' \<equiv>cs q'\<close>
proof-
  obtain q' where q'_spec: \<open>q \<Rightarrow>^a q'\<close>
    using cbisim step unfolding coupled_simulation_weak_premise by blast
  then obtain q_max where q_max_spec: \<open>q' \<longmapsto>* tau q_max\<close> \<open>tau_max q_max\<close>
    using tau_max_deadlock contracted_cycles finite_taus by force
  hence \<open>q \<Rightarrow>^a q_max\<close> using q'_spec steps_concat by blast
  then obtain p'' where p''_spec: \<open>p \<Rightarrow>^a p''\<close> \<open>q_max \<sqsubseteq>cs p''\<close>
    using cbisim unfolding coupled_simulation_weak_premise by blast
  then obtain p''' where p'''_spec: \<open>p'' \<longmapsto>* tau p'''\<close> \<open>p''' \<sqsubseteq>cs q_max\<close>
    using cbisim unfolding coupled_simulation_weak_simulation  by blast
  then obtain p_max where p_max_spec: \<open>p''' \<longmapsto>* tau p_max\<close> \<open>tau_max p_max\<close>
    using tau_max_deadlock contracted_cycles finite_taus by force
  hence \<open>p_max \<sqsubseteq>cs p'''\<close> using coupledsim_step by blast
  hence \<open>p_max \<sqsubseteq>cs q_max\<close> using p'''_spec coupledsim_trans by blast
  hence \<open>q_max \<equiv>cs p_max\<close> using coupledsim_tau_max_eq q_max_spec by blast
  moreover have  \<open>p \<Rightarrow>^a p_max\<close>
    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 \<Rightarrow>^a q_max` by blast
qed
718 719 720

lemma coupledsim_eq_reducible_1:
  assumes
benkeks committed
721 722 723 724
    contracted_cycles: \<open>\<And> r1 r2 . r1 \<longmapsto>* tau r2 \<and> r2 \<longmapsto>* tau r1 \<Longrightarrow> r1 = r2\<close> and
    finite_taus: \<open>\<And> r. finite {r'. r \<longmapsto>* tau r'}\<close> and
    tau_shortcuts:
      \<open>\<And>r a r'. r \<longmapsto>* tau r' \<Longrightarrow> \<exists>r''. tau_max r'' \<and> r \<longmapsto>\<tau> r'' \<and> r' \<sqsubseteq>cs r''\<close>  and
725
    sim_vis_p:
benkeks committed
726
      \<open>\<And>p' a. \<not>tau a \<Longrightarrow> p \<Rightarrow>^a p' \<Longrightarrow> \<exists>p'' q'. q \<Rightarrow>^a q' \<and> p' \<sqsubseteq>cs q'\<close> and
727
    sim_tau_max_p:
benkeks committed
728
      \<open>\<And>p'. tau_max p' \<Longrightarrow> p \<longmapsto>* tau p' \<Longrightarrow> \<exists>q'. tau_max q' \<and> q \<longmapsto>* tau q' \<and> p' \<equiv>cs q'\<close>
729
  shows
benkeks committed
730
    \<open>p \<sqsubseteq>cs q\<close>
731 732
proof-
  have
benkeks committed
733 734
    \<open>((\<forall>a p'. p \<longmapsto>a  p' \<longrightarrow> (\<exists>q'. q \<Rightarrow>^a  q' \<and> p' \<sqsubseteq>cs q')) \<and>
    (\<exists>q'. q \<longmapsto>* tau  q' \<and> q' \<sqsubseteq>cs p))\<close>
735 736 737
  proof safe
    fix a p'
    assume
benkeks committed
738 739 740
      step: \<open>p \<longmapsto>a  p'\<close>
    thus \<open>\<exists>q'. q \<Rightarrow>^a  q' \<and> p' \<sqsubseteq>cs  q'\<close>
    proof (cases \<open>tau a\<close>)
741
      case True
benkeks committed
742 743
      then obtain p'' where p''_spec: \<open>p \<longmapsto>\<tau> p''\<close> \<open>tau_max p''\<close> \<open>p' \<sqsubseteq>cs p''\<close>
        using tau_shortcuts step tau_def steps_one_step[of p \<tau> p']
744
        by (metis (no_types, lifting))
benkeks committed
745
      then obtain q' where q'_spec: \<open>q \<longmapsto>* tau q'\<close> \<open>p'' \<equiv>cs q'\<close>
746 747 748 749 750 751 752 753 754
        using sim_tau_max_p steps_one_step[OF step, of tau, OF `tau a`]
          steps_one_step[of p \<tau> 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
benkeks committed
755
    obtain p_max where \<open>p \<longmapsto>* tau p_max\<close> \<open>tau_max p_max\<close>
756
      using tau_max_deadlock contracted_cycles finite_taus by blast
benkeks committed
757
    then obtain q_max where \<open>q \<longmapsto>* tau  q_max\<close> \<open>q_max \<sqsubseteq>cs p_max\<close>
758
      using sim_tau_max_p[of p_max] by force
benkeks committed
759 760
    moreover have \<open>p_max \<sqsubseteq>cs  p\<close> using `p \<longmapsto>* tau p_max` coupledsim_step by blast
    ultimately show \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> q' \<sqsubseteq>cs  p\<close>
761 762
      using coupledsim_trans by blast
  qed
benkeks committed
763
  thus \<open>p \<sqsubseteq>cs q\<close> using coupledsim_unfold[symmetric] by auto
764 765 766 767
qed

lemma coupledsim_eq_reducible_2:
  assumes
benkeks committed
768 769 770
    cs: \<open>p \<sqsubseteq>cs q\<close> and
    contracted_cycles: \<open>\<And>r1 r2 . r1 \<longmapsto>* tau r2 \<and> r2 \<longmapsto>* tau r1 \<Longrightarrow> r1 = r2\<close> and
    finite_taus: \<open>\<And>r. finite {r'. r \<longmapsto>* tau r'}\<close>
771 772
  shows
    sim_vis_p:
benkeks committed
773
      \<open>\<And>p' a. \<not>tau a \<Longrightarrow> p \<Rightarrow>^a p' \<Longrightarrow> \<exists>q'. q \<Rightarrow>^a q' \<and> p' \<sqsubseteq>cs q'\<close> and
774
    sim_tau_max_p:
benkeks committed
775
      \<open>\<And>p'. tau_max p' \<Longrightarrow> p \<longmapsto>* tau p' \<Longrightarrow> \<exists>q'. tau_max q' \<and> q \<longmapsto>* tau q' \<and> p' \<equiv>cs q'\<close>
776 777 778
proof-
  fix p' a
  assume
benkeks committed
779 780 781
    \<open>\<not> tau a\<close>
    \<open>p \<Rightarrow>^a  p'\<close>
  thus \<open>\<exists>q'. q \<Rightarrow>^a  q' \<and> p' \<sqsubseteq>cs  q'\<close>
782 783 784 785
    using cs unfolding coupled_simulation_weak_premise by blast
next
  fix p'
  assume step:
benkeks committed
786 787 788 789
    \<open>p \<longmapsto>* tau p'\<close>
    \<open>tau_max p'\<close>
  hence \<open>p \<Rightarrow>^\<tau>  p'\<close>  by auto
  hence \<open>\<exists> q'. tau_max q' \<and> q \<Rightarrow>^\<tau> q' \<and> p' \<equiv>cs q'\<close>
790 791
    using coupledsim_eventual_symmetry[OF _ finite_taus, of p q \<tau> p']
      contracted_cycles cs step(2) by blast
benkeks committed
792
  thus \<open>\<exists> q'. tau_max q' \<and> q \<longmapsto>* tau q' \<and> p' \<equiv>cs q'\<close>
793 794 795
    by auto
qed

benkeks committed
796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851
subsection \<open>Reduction Semantics Coupled Simulation\<close>

text \<open>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 \<open>\<tau>\<close>-transitions).\<close>

definition coupled_simulation_gp15 ::
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>coupled_simulation_gp15 R \<equiv> \<forall> p q p'. R p q \<and> (p \<longmapsto>* (\<lambda>a. True) p') \<longrightarrow>
    (\<exists> q'. (q \<longmapsto>* (\<lambda>a. True) q') \<and> R p' q') \<and>
    (\<exists> q'. (q \<longmapsto>* (\<lambda>a. True) q') \<and> R q' p')\<close>

lemma weak_bisim_implies_coupled_sim_gp15:
  assumes
    wbisim: \<open>weak_bisimulation R\<close> and 
    symmetry: \<open>\<And> p q . R p q \<Longrightarrow> R q p\<close>
  shows \<open>coupled_simulation_gp15 R\<close>
unfolding coupled_simulation_gp15_def proof safe
  fix p q p'
  assume Rpq: \<open>R p q\<close> \<open>p \<longmapsto>* (\<lambda>a. True)  p'\<close>
  have always_tau: \<open>\<And>a. tau a \<Longrightarrow> (\<lambda>a. True) a\<close> by simp
  hence \<open>\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R p' q'\<close>
    using steps_retain_weak_bisim[OF wbisim Rpq] by auto
  moreover hence \<open>\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R q' p'\<close>
    using symmetry by auto
  ultimately show
    \<open>(\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R p' q')\<close>
    \<open>(\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R q' p')\<close> .
qed

lemma coupledsim_gla17_implies_gp15:
  assumes
    \<open>coupled_simulation R\<close>
  shows 
    \<open>coupled_simulation_gp15 R\<close>
  unfolding coupled_simulation_gp15_def
proof safe
  fix p q p'
  assume challenge:
    \<open>R p q\<close>
    \<open>p \<longmapsto>*(\<lambda>a. True)p'\<close>
  have tau_true: \<open>\<And>a. tau a \<Longrightarrow> (\<lambda>a. True) a\<close> by simp
  thus \<open>\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R p' q'\<close>
    using steps_retain_weak_sim assms challenge
    unfolding coupled_simulation_weak_simulation by meson
  then obtain q' where q'_def: \<open>q \<longmapsto>* (\<lambda>a. True)  q'\<close> \<open>R p' q'\<close> by blast
  then obtain q'' where \<open>q' \<longmapsto>* tau  q''\<close> \<open>R q'' p'\<close>
    using assms unfolding coupled_simulation_weak_simulation by blast
  moreover hence \<open>q \<longmapsto>* (\<lambda>a. True)  q''\<close>
    using q'_def(1) steps_concat steps_spec tau_true by meson
  ultimately show \<open>\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R q' p'\<close> by blast
qed

lemma coupledsim_gp15_implies_gla17_on_tau_systems:
852
  assumes
benkeks committed
853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902
    \<open>coupled_simulation_gp15 R\<close>
    \<open>\<And> a . tau a\<close>
  shows 
    \<open>coupled_simulation R\<close>
  unfolding coupled_simulation_def
proof safe
  fix p q p' a
  assume challenge:
    \<open>R p q\<close>
    \<open>p \<longmapsto>a  p'\<close>
  hence \<open>p \<longmapsto>* (\<lambda>a. True)  p'\<close> using steps_one_step by metis
  then obtain q' where \<open>q \<longmapsto>* (\<lambda>a. True)  q'\<close> \<open>R p' q'\<close>
    using challenge(1) assms(1) unfolding coupled_simulation_gp15_def by blast
  hence \<open>q \<Rightarrow>^a  q'\<close> using assms(2) steps_concat steps_spec by meson
  thus \<open>\<exists>q'. R p' q' \<and> q \<Rightarrow>^a  q'\<close> using `R p' q'` by blast
next
  fix p q
  assume
    \<open>R p q\<close>
  moreover have \<open>p \<longmapsto>* (\<lambda>a. True) p\<close> using steps.refl by blast
  ultimately have \<open>\<exists>q'. q \<longmapsto>* (\<lambda>a. True)  q' \<and> R q' p\<close>
    using assms(1) unfolding coupled_simulation_gp15_def by blast
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R q' p\<close> using assms(2) steps_spec by blast
qed


subsection \<open>Coupled Simulation as Two Simulations\<close>

text \<open>Historically, coupled similarity has been defined in terms of @{emph \<open>two\<close>} 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.\<close>

\<comment>\<open>From @{cite "sangiorgi2012"}\<close>
definition coupled_simulation_san12 :: 
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>coupled_simulation_san12 R1 R2 \<equiv>
    weak_simulation R1 \<and> weak_simulation (\<lambda> p q . R2 q p)
  \<and> (\<forall> p q . R1 p q \<longrightarrow> (\<exists> q' . q \<longmapsto>* tau q' \<and> R2 p q'))
  \<and> (\<forall> p q . R2 p q \<longrightarrow> (\<exists> p' . p \<longmapsto>* tau p' \<and> R1 p' q))\<close>
  
lemma weak_bisim_implies_coupled_sim_san12:
  assumes \<open>weak_bisimulation R\<close>
  shows \<open>coupled_simulation_san12 R R\<close>
  using assms weak_bisim_weak_sim steps.refl[of _ tau]
  unfolding coupled_simulation_san12_def
  by blast

lemma coupledsim_gla17_resembles_san12:
903
  shows
benkeks committed
904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026
    \<open>coupled_simulation R1 =
    coupled_simulation_san12 R1 (\<lambda> p q . R1 q p)\<close>
  unfolding coupled_simulation_weak_simulation coupled_simulation_san12_def by blast

lemma coupledsim_san12_impl_gla17:
  assumes
    \<open>coupled_simulation_san12 R1 R2\<close>
  shows
    \<open>coupled_simulation (\<lambda> p q. R1 p q \<or> R2 q p)\<close>
  unfolding coupled_simulation_weak_simulation
proof safe
  have \<open>weak_simulation R1\<close> \<open>weak_simulation (\<lambda>p q. R2 q p)\<close>
    using assms unfolding coupled_simulation_san12_def by auto
  thus \<open>weak_simulation (\<lambda>p q. R1 p q \<or> R2 q p)\<close>
    using weak_sim_union_cl by blast
next
  fix p q
  assume
    \<open>R1 p q\<close>
  hence \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R2 p q'\<close>
    using assms unfolding coupled_simulation_san12_def by auto
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (R1 q' p \<or> R2 p q')\<close> by blast
next
  fix p q
  assume
    \<open>R2 q p\<close>
  hence \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R1 q' p\<close>
    using assms unfolding coupled_simulation_san12_def by auto
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (R1 q' p \<or> R2 p q')\<close> by blast
qed

subsection \<open>S-coupled Simulation\<close>

text \<open>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"}.\<close>

\<comment>\<open>From @{cite "parrow1992"}\<close>
definition coupled_simulation_p92 :: 
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>coupled_simulation_p92 R1 R2 \<equiv> \<forall> p q . 
    (R1 p q \<longrightarrow> 
      ((\<forall> p' a. p \<longmapsto>a p' \<longrightarrow> 
        (\<exists> q'. R1 p' q' \<and> 
          (q \<Rightarrow>^a q'))) \<and>
      (stable_state p \<longrightarrow> R2 p q))) \<and>
    (R2 p q \<longrightarrow> 
      ((\<forall> q' a. q \<longmapsto>a q' \<longrightarrow>
        (\<exists> p'. R2 p' q' \<and> 
          (p \<Rightarrow>^a p'))) \<and>
      (stable_state q \<longrightarrow> R1 p q)))\<close>

lemma weak_bisim_implies_coupled_sim_p92:
  assumes \<open>weak_bisimulation R\<close>
  shows \<open>coupled_simulation_p92 R R\<close>
using assms unfolding weak_bisimulation_def coupled_simulation_p92_def by blast
  
lemma coupled_sim_p92_symm:
  assumes \<open>coupled_simulation_p92 R1 R2\<close>
  shows \<open>coupled_simulation_p92 (\<lambda> p q. R2 q p) (\<lambda> p q. R1 q p)\<close>
using assms unfolding coupled_simulation_p92_def by blast
  
definition s_coupled_simulation_san12 :: 
  \<open>('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool\<close>
where
  \<open>s_coupled_simulation_san12 R1 R2 \<equiv>
    weak_simulation R1 \<and> weak_simulation (\<lambda> p q . R2 q p)
  \<and> (\<forall> p q . R1 p q \<longrightarrow> stable_state p \<longrightarrow> R2 p q)
  \<and> (\<forall> p q . R2 p q \<longrightarrow> stable_state q \<longrightarrow> R1 p q)\<close>

abbreviation s_coupled_simulated_by :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<sqsubseteq>scs  _" [60, 60] 65)
  where \<open>s_coupled_simulated_by p q \<equiv>
    \<exists> R1 R2 . s_coupled_simulation_san12 R1 R2 \<and> R1 p q\<close>
    
abbreviation s_coupled_similar :: \<open>'s \<Rightarrow> 's \<Rightarrow> bool\<close> ("_ \<equiv>scs  _" [60, 60] 65)
  where \<open>s_coupled_similar p q \<equiv>
    \<exists> R1 R2 . s_coupled_simulation_san12 R1 R2 \<and> R1 p q \<and> R2 p q\<close>

lemma s_coupled_sim_is_original_coupled:
  \<open>s_coupled_simulation_san12 = coupled_simulation_p92\<close>
unfolding coupled_simulation_p92_def
  s_coupled_simulation_san12_def weak_simulation_def by blast
 
corollary weak_bisim_implies_s_coupled_sim:
  assumes \<open>weak_bisimulation R\<close>
  shows \<open>s_coupled_simulation_san12 R R\<close>
  using assms s_coupled_sim_is_original_coupled weak_bisim_implies_coupled_sim_p92 by simp
   
corollary s_coupled_sim_symm:
  assumes \<open>s_coupled_simulation_san12 R1 R2\<close>
  shows \<open>s_coupled_simulation_san12 (\<lambda> p q. R2 q p) (\<lambda> p q. R1 q p)\<close>
  using assms coupled_sim_p92_symm s_coupled_sim_is_original_coupled by simp
   
corollary s_coupled_sim_union_cl:
  assumes
    \<open>s_coupled_simulation_san12 RA1 RA2\<close>
    \<open>s_coupled_simulation_san12 RB1 RB2\<close>
  shows
    \<open>s_coupled_simulation_san12 (\<lambda> p q. RA1 p q \<or> RB1 p q) (\<lambda> p q. RA2 p q \<or> RB2 p q)\<close>
  using assms weak_sim_union_cl unfolding s_coupled_simulation_san12_def by auto
    
corollary s_coupled_sim_symm_union:
  assumes \<open>s_coupled_simulation_san12 R1 R2\<close>
  shows \<open>s_coupled_simulation_san12 (\<lambda> p q. R1 p q \<or> R2 q p) (\<lambda> p q. R2 p q \<or> R1 q p)\<close>
  using s_coupled_sim_union_cl[OF assms s_coupled_sim_symm[OF assms]] .

lemma s_coupledsim_stable_eq:
  assumes
    \<open>p \<sqsubseteq>scs q\<close>
    \<open>stable_state p\<close>
  shows  \<open>p \<equiv>scs q\<close> 
proof -
  obtain R1 R2 where
      \<open>R1 p q\<close>
      \<open>weak_simulation R1\<close>
      \<open>weak_simulation (\<lambda>p q. R2 q p)\<close>
      \<open>\<forall>p q. R1 p q \<longrightarrow> stable_state p \<longrightarrow> R2 p q\<close>
      \<open>\<forall>p q. R2 p q \<longrightarrow> stable_state q \<longrightarrow> R1 p q\<close>
    using assms(1)  unfolding s_coupled_simulation_san12_def by blast
  moreover hence \<open>R2 p q\<close> using assms(2) by blast
  ultimately show ?thesis unfolding s_coupled_simulation_san12_def by blast
1027 1028
qed

benkeks committed
1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042
lemma s_coupledsim_symm:
  assumes
    \<open>p \<equiv>scs q\<close> 
  shows 
    \<open>q \<equiv>scs p\<close> 
  using assms s_coupled_sim_symm by blast

lemma s_coupledsim_eq_parts:
  assumes
    \<open>p \<equiv>scs q\<close>
  shows
    \<open>p \<sqsubseteq>scs q\<close>
    \<open>q \<sqsubseteq>scs p\<close>
  using assms s_coupledsim_symm by metis+
1043

benkeks committed
1044
\<comment>\<open>From @{cite "sangiorgi2012"}, p.~226\<close>
1045 1046
lemma divergence_free_coupledsims_coincidence_1:
  defines 
benkeks committed
1047 1048
    \<open>R1 \<equiv> (\<lambda> p q . p \<sqsubseteq>cs q \<and> (stable_state p \<longrightarrow> stable_state q))\<close> and
    \<open>R2 \<equiv> (\<lambda> p q . q \<sqsubseteq>cs p \<and> (stable_state q \<longrightarrow> stable_state p))\<close>
1049
  assumes
benkeks committed
1050
    non_divergent_system: \<open>\<And> p . \<not> divergent_state p\<close>
1051
  shows
benkeks committed
1052 1053
    \<open>s_coupled_simulation_san12 R1 R2\<close>
  unfolding s_coupled_simulation_san12_def
1054
proof safe
benkeks committed
1055
  show \<open>weak_simulation R1\<close> unfolding weak_simulation_def
1056 1057 1058
  proof safe
    fix p q p' a
    assume sub_assms:
benkeks committed
1059 1060 1061
      \<open>R1 p q\<close>
      \<open>p \<longmapsto>a  p'\<close>
    then obtain q' where q'_def: \<open>q \<Rightarrow>^a q'\<close> \<open>p' \<sqsubseteq>cs q'\<close>
1062
      using coupled_sim_by_is_coupled_sim unfolding R1_def coupled_simulation_def by blast
benkeks committed
1063 1064
    show \<open>\<exists>q'. R1 p' q' \<and> q \<Rightarrow>^a  q'\<close>
    proof (cases \<open>stable_state p'\<close>)
1065
      case True
benkeks committed
1066
      obtain  q'' where q''_def: \<open>q' \<longmapsto>* tau q''\<close> \<open>q'' \<sqsubseteq>cs  p'\<close>
1067 1068
        using coupled_sim_by_is_coupled_sim q'_def(2)
        unfolding coupled_simulation_weak_simulation by blast
benkeks committed
1069
      then obtain q''' where q'''_def: \<open>q'' \<longmapsto>* tau q'''\<close> \<open>stable_state q'''\<close>
1070
        using non_divergence_implies_eventual_stability non_divergent_system by blast
benkeks committed
1071 1072 1073 1074 1075 1076
      hence \<open>q''' \<sqsubseteq>cs p'\<close>
        using coupledsim_step_gla17 coupledsim_trans[OF _ q''_def(2)] by blast
      hence \<open>p' \<sqsubseteq>cs q'''\<close>
        using `stable_state p'` coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm
        by blast
      moreover have \<open>q \<Rightarrow>^a q'''\<close> using q'_def(1) q''_def(1) q'''_def(1) steps_concat by blast
1077 1078 1079 1080 1081 1082
      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
benkeks committed
1083
  \<comment>\<open>analogous to previous case\<close>
benkeks committed
1084
  then show \<open>weak_simulation (\<lambda>p q. R2 q p)\<close> unfolding R1_def R2_def .
1085 1086 1087
next
  fix p q
  assume
benkeks committed
1088 1089 1090
    \<open>R1 p q\<close>
    \<open>stable_state p\<close>
  thus \<open>R2 p q\<close>
1091 1092
    unfolding R1_def R2_def 
    using coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm by blast
benkeks committed
1093
next \<comment>\<open>analogous\<close>
1094 1095
  fix p q
  assume
benkeks committed
1096 1097 1098
    \<open>R2 p q\<close>
    \<open>stable_state q\<close>
  thus \<open>R1 p q\<close>
1099 1100 1101 1102
    unfolding R1_def R2_def 
    using coupled_sim_by_is_coupled_sim coupledsim_stable_state_symm by blast
qed

benkeks committed
1103
\<comment>\<open>From @{cite "sangiorgi2012"}, p.~227\<close>
1104 1105
lemma divergence_free_coupledsims_coincidence_2:
  defines 
benkeks committed
1106
    \<open>R \<equiv> (\<lambda> p q . p \<sqsubseteq>scs q \<or> (\<exists> q' . q \<longmapsto>* tau q' \<and> p \<equiv>scs q'))\<close>
1107
  assumes
benkeks committed
1108
    non_divergent_system: \<open>\<And> p . \<not> divergent_state p\<close>
1109
  shows
benkeks committed
1110
    \<open>coupled_simulation R\<close>
1111 1112
  unfolding coupled_simulation_weak_simulation
proof safe
benkeks committed
1113
  show \<open>weak_simulation R\<close> 
1114 1115 1116 1117
    unfolding weak_simulation_def
  proof safe
    fix p q p' a
    assume sub_assms:
benkeks committed
1118 1119 1120
      \<open>R p q\<close>
      \<open>p \<longmapsto>a  p'\<close>
    thus \<open>\<exists>q'. R p' q' \<and> q \<Rightarrow>^a  q'\<close>
1121
      unfolding R_def
benkeks committed
1122
    proof (cases \<open>p \<sqsubseteq>scs q\<close>)
1123
      case True
benkeks committed
1124 1125 1126 1127
      then obtain q' where \<open>p' \<sqsubseteq>scs  q'\<close> \<open>q \<Rightarrow>^a  q'\<close>
        using s_coupled_simulation_san12_def sub_assms(2) weak_sim_ruleformat by metis
      thus \<open>\<exists>q'. (p' \<sqsubseteq>scs  q' \<or> (\<exists>q'a. q' \<longmapsto>* tau  q'a \<and> p' \<equiv>scs  q'a)) \<and> q \<Rightarrow>^a  q'\<close>
        by blast
1128 1129
    next
      case False
benkeks committed
1130 1131 1132 1133 1134 1135 1136
      then obtain q' where \<open>q \<longmapsto>* tau  q'\<close> \<open>p \<equiv>scs  q'\<close>
          using sub_assms(1) unfolding R_def by blast
      then obtain q'' where \<open>q' \<Rightarrow>^a  q''\<close> \<open>p' \<sqsubseteq>scs  q''\<close> 
        using s_coupled_simulation_san12_def sub_assms(2) weak_sim_ruleformat by metis
      hence \<open>p' \<sqsubseteq>scs  q'' \<and> q \<Rightarrow>^a  q''\<close> using steps_concat `q \<longmapsto>* tau  q'` by blast
      thus \<open>\<exists>q'. (p' \<sqsubseteq>scs  q' \<or> (\<exists>q'a. q' \<longmapsto>* tau  q'a \<and> p' \<equiv>scs  q'a)) \<and> q \<Rightarrow>^a  q'\<close>
        by blast
1137 1138 1139 1140 1141
    qed
  qed
next
  fix p q
  assume
benkeks committed
1142 1143
    \<open>R p q\<close>
  thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> R q' p\<close> unfolding R_def
1144 1145 1146
  proof safe
    fix R1 R2
    assume sub_assms:
benkeks committed
1147 1148 1149
      \<open>s_coupled_simulation_san12 R1 R2\<close>
      \<open>R1 p q\<close>
    thus \<open>\<exists>q'. q \<longmapsto>* tau  q' \<and> (q' \<sqsubseteq>scs  p \<or> (\<exists>q'a. p \<longmapsto>* tau  q'a \<and> q' \<equiv>scs  q'a))\<close>
1150
    proof -
benkeks committed
1151
      \<comment>\<open>dropped a superfluous case distinction from @cite{sangiorgi2012}\<close>
benkeks committed
1152
      obtain p' where \<open>stable_state p'\<close> \<open>p \<longmapsto>* tau p'\<close>
1153
        using non_divergent_system non_divergence_implies_eventual_stability by blast
benkeks committed
1154 1155 1156
      hence \<open>p \<Rightarrow>^\<tau>  p'\<close> using tau_tau by blast
      then obtain q' where \<open>q \<longmapsto>* tau q'\<close> \<open>p' \<sqsubseteq>scs q'\<close>
        using s_coupled_simulation_san12_def weak_sim_weak_premise sub_assms tau_tau
1157
        by metis
benkeks committed
1158
      moreover hence \<open>p' \<equiv>scs q'\<close> using `stable_state p'` s_coupledsim_stable_eq by blast
1159 1160 1161 1162 1163
      ultimately show ?thesis using `p \<longmapsto>* tau p'` s_coupledsim_symm by blast
    qed
  qed (metis s_coupledsim_symm)
qed

benkeks committed
1164 1165
text \<open>While this proof follows @{cite "sangiorgi2012"}, we needed to deviate from them by also
  requiring rootedness (shared stability) for the compared states.\<close>
1166 1167
theorem divergence_free_coupledsims_coincidence:
  assumes
benkeks committed
1168 1169
    non_divergent_system: \<open>\<And> p . \<not> divergent_state p\<close> and
    stability_rooted: \<open>stable_state p \<longleftrightarrow> stable_state q\<close>
1170
  shows
benkeks committed
1171
    \<open>(p \<equiv>cs q) = (p \<equiv>scs q)\<close>
1172
proof rule
benkeks committed
1173 1174 1175 1176 1177
  assume \<open>p \<equiv>cs q\<close>
  hence \<open>p \<sqsubseteq>cs q\<close> \<open>q \<sqsubseteq>cs p\<close> by auto
  thus \<open>p \<equiv>scs q\<close>
    using stability_rooted divergence_free_coupledsims_coincidence_1[OF non_divergent_system]
    by blast
1178
next
benkeks committed
1179 1180 1181
  assume \<open>p \<equiv>scs q\<close>
  thus \<open>p \<equiv>cs q\<close>
    using stability_rooted divergence_free_coupledsims_coincidence_2[OF non_divergent_system]
1182 1183 1184
      s_coupledsim_eq_parts by blast
qed

benkeks committed
1185
end \<comment>\<open>context @{locale lts_tau}\<close>
benkeks committed
1186
 
1187 1188
text \<open>The following example shows that a system might be related by s-coupled-simulation without
  being connected by coupled-simulation.\<close>
benkeks committed
1189

1190 1191 1192
datatype ex_state = a0 | a1 | a2 | a3 | b0 | b1 | b2 
  
locale ex_lts = lts_tau trans \<tau>
benkeks committed
1193
  for trans :: \<open>ex_state \<Rightarrow> nat \<Rightarrow> ex_state \<Rightarrow> bool\<close> and \<tau> +
1194 1195
  assumes
    sys:
benkeks committed
1196
  \<open>trans = (\<lambda> p act q .
1197 1198 1199 1200 1201
     1 = act \<and> (p = a0 \<and> q = a1 
              \<or> p = a0 \<and> q = a2 
              \<or> p = a2 \<and> q = a3 
              \<or> p = b0 \<and> q = b1 
              \<or> p = b1 \<and> q = b2) \<or>
benkeks committed
1202 1203
     0 = act \<and> (p = a1 \<and> q = a1))\<close>
   \<open>\<tau> = 0\<close>
1204 1205 1206 1207 1208 1209
begin 
  
lemma no_root_coupled_sim:
  fixes R1 R2
  assumes
    coupled:
benkeks committed
1210
      \<open>coupled_simulation_san12 R1 R2\<close> and
1211
    root:
benkeks committed
1212
      \<open>R1 a0 b0\<close> \<open>R2 a0 b0\<close>
1213 1214 1215 1216 1217
  shows
    False
proof -
  have
    R1sim: 
benkeks committed
1218
      \<open>weak_simulation R1\<close> and
1219
    R1coupling:
benkeks committed
1220
      \<open>\<forall>p q. R1 p q \<longrightarrow> (\<exists>q'. q \<longmapsto>* tau  q' \<and> R2 p q')\<close> and
1221
    R2sim: 
benkeks committed
1222 1223
      \<open>weak_simulation (\<lambda>p q. R2 q p)\<close>
    using coupled unfolding coupled_simulation_san12_def by auto
1224
  hence R1sim_rf:
benkeks committed
1225 1226 1227 1228
      \<open>\<And> p q. R1 p q \<Longrightarrow>
        (\<forall>p' a. p \<longmapsto>a  p' \<longrightarrow>
          (\<exists>q'. R1 p' q' \<and> (\<not> tau a \<longrightarrow> q \<Rightarrow>a  q') \<and>
          (tau a \<longrightarrow> q \<longmapsto>* tau  q')))\<close>
1229
    unfolding weak_simulation_def by blast
benkeks committed
1230 1231 1232 1233 1234 1235
  have \<open>a0 \<longmapsto>1 a1\<close> using sys by auto
  hence \<open>\<exists>q'. R1 a1 q' \<and> b0 \<Rightarrow>1 q'\<close>
    using R1sim_rf[OF root(1), rule_format, of 1 a1] tau_def
    by (auto simp add: sys)
  then obtain q' where q': \<open>R1 a1 q'\<close> \<open>b0 \<Rightarrow>1 q'\<close> by blast
  have b0_quasi_stable: \<open>\<forall> q' . b0 \<longmapsto>*tau q' \<longrightarrow> b0 = q'\<close>
1236
    using steps_no_step[of b0 tau] tau_def by (auto simp add: sys)
benkeks committed
1237 1238
  have b0_only_b1: \<open>\<forall> q' . b0 \<longmapsto>1 q' \<longrightarrow> q' = b1\<close> by (auto simp add: sys)
  have b1_quasi_stable: \<open>\<forall> q' . b1 \<longmapsto>*tau q' \<longrightarrow> b1 = q'\<close>
1239
    using steps_no_step[of b1 tau] tau_def by (auto simp add: sys)
benkeks committed
1240 1241 1242 1243 1244
  have \<open>\<forall> q' . b0 \<Rightarrow>1 q' \<longrightarrow> q' = b1\<close>
    using b0_quasi_stable b0_only_b1 b1_quasi_stable by auto
  hence \<open>q' = b1\<close> using q'(2) by blast
  hence \<open>R1 a1 b1\<close> using q'(1) by simp
  hence \<open>R2 a1 b1\<close>
1245
    using b1_quasi_stable R1coupling by auto
benkeks committed
1246
  have b1_b2: \<open>b1 \<longmapsto>1 b2\<close>
1247
    by (auto simp add: sys)
benkeks committed
1248 1249 1250 1251
  hence a1_sim: \<open>\<exists> q' . R2 q' b2 \<and> a1 \<Rightarrow>1  q'\<close>
    using `R2 a1 b1` R2sim b1_b2
    unfolding weak_simulation_def tau_def by (auto simp add: sys)
  have a1_quasi_stable: \<open>\<forall> q' . a1 \<longmapsto>*tau q' \<longrightarrow> a1 = q'\<close>
1252
    using steps_loop[of a1] by (auto simp add: sys)
benkeks committed
1253
  hence a1_stuck: \<open>\<forall> q' . \<not> a1 \<Rightarrow>1 q'\<close>
1254 1255 1256 1257 1258 1259
    by (auto simp add: sys)
  show ?thesis using a1_sim  a1_stuck by blast
qed

lemma root_s_coupled_sim:
  defines
benkeks committed
1260
    \<open>R1 \<equiv> \<lambda> a b .
1261 1262 1263
      a = a0 \<and> b = b0 \<or>
      a = a1 \<and> b = b1 \<or>
      a = a2 \<and> b = b1 \<or>
benkeks committed
1264
      a = a3 \<and> b = b2\<close>
1265
  and
benkeks committed
1266
    \<open>R2 \<equiv> \<lambda> a b .
1267 1268
      a = a0 \<and> b = b0 \<or>
      a = a2 \<and> b = b1 \<or>
benkeks committed
1269
      a = a3 \<and> b = b2\<close>
1270 1271
  shows
    coupled:
benkeks committed
1272 1273
      \<open>s_coupled_simulation_san12 R1 R2\<close>
  unfolding s_coupled_simulation_san12_def
1274
proof safe
benkeks committed
1275
  show \<open>weak_simulation R1\<close>
1276 1277
    unfolding weak_simulation_def proof (clarify)
    fix p q p' a
benkeks committed
1278
    show \<open>R1 p q \<Longrightarrow> p \<longmapsto>a  p' \<Longrightarrow> \<exists>q'. R1 p' q' \<and> (q \<Rightarrow>^a  q')\<close> 
1279 1280 1281
      using step_tau_refl unfolding sys assms tau_def using sys(2) tau_def by (cases p, auto)
  qed
next
benkeks committed
1282
  show \<open>weak_simulation (\<lambda>p q. R2 q p)\<close>
1283 1284
    unfolding weak_simulation_def proof (clarify)
    fix p q p' a
benkeks committed
1285 1286 1287
    show \<open>R2 q p \<Longrightarrow> p \<longmapsto>a  p' \<Longrightarrow> \<exists>q'. R2 q' p' \<and> (q \<Rightarrow>^a  q')\<close> 
      using steps.refl[of _ tau] tau_def unfolding assms sys
      using sys(2) tau_def by (cases p, auto)
1288
  qed
benkeks committed
1289
next
1290
  fix p q
benkeks committed
1291 1292
  assume \<open>R1 p q\<close> \<open>stable_state p\<close>
  thus \<open>R2 p q\<close> unfolding assms sys using sys(2) tau_def by auto
1293 1294
next
  fix p q
benkeks committed
1295 1296
  assume \<open>R2 p q\<close> \<open>stable_state q\<close>
  thus \<open>R1 p q\<close> unfolding assms sys using tau_def by auto
1297 1298
qed

benkeks committed
1299
end \<comment>\<open>@{locale ex_lts}// example lts\<close>
benkeks committed
1300

1301
end