bisimulationScript.sml
1(* ------------------------------------------------------------------------ *)
2(* Bisimulations defined on general labeled transition ('a->'b->'a->bool) *)
3(* ------------------------------------------------------------------------ *)
4Theory bisimulation[bare]
5Ancestors
6 relation
7Libs
8 HolKernel Parse boolLib simpLib metisLib BasicProvers
9
10
11(*---------------------------------------------------------------------------*)
12(* (Strong) bisimulation *)
13(*---------------------------------------------------------------------------*)
14
15val BISIM_def = new_definition ("BISIM_def",
16 ``BISIM ts R = !p q.
17 R p q ==> !l.
18 (!p'. ts p l p' ==> ?q'. ts q l q' /\ R p' q') /\
19 (!q'. ts q l q' ==> ?p'. ts p l p' /\ R p' q')``);
20
21(* (Strong) bisimilarity, see BISIM_REL_def for an alternative definition *)
22CoInductive BISIM_REL :
23 !p q. (!l.
24 (!p'. ts p l p' ==> ?q'. ts q l q' /\ (BISIM_REL ts) p' q') /\
25 (!q'. ts q l q' ==> ?p'. ts p l p' /\ (BISIM_REL ts) p' q'))
26 ==> (BISIM_REL ts) p q
27End
28
29Theorem BISIM_ID :
30 !ts. BISIM ts Id
31Proof
32 SRW_TAC[][BISIM_def]
33QED
34
35Theorem BISIM_INV :
36 !ts R. BISIM ts R ==> BISIM ts (inv R)
37Proof
38 SRW_TAC[][BISIM_def, inv_DEF] >> METIS_TAC []
39QED
40
41Theorem BISIM_O :
42 !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R' O R)
43Proof
44 rpt STRIP_TAC
45 >> PURE_ONCE_REWRITE_TAC [BISIM_def]
46 >> SRW_TAC[][O_DEF]
47 >> METIS_TAC[BISIM_def]
48QED
49
50Theorem BISIM_RUNION :
51 !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R RUNION R')
52Proof
53 rpt GEN_TAC
54 >> PURE_ONCE_REWRITE_TAC [BISIM_def]
55 >> SRW_TAC[][RUNION]
56 >> METIS_TAC[]
57QED
58
59Theorem BISIM_REL_IS_BISIM :
60 !ts. BISIM ts (BISIM_REL ts)
61Proof
62 PURE_ONCE_REWRITE_TAC [BISIM_def]
63 >> rpt GEN_TAC >> DISCH_TAC
64 >> Q.SPEC_TAC (`l`, `l`)
65 >> PURE_ONCE_REWRITE_TAC [GSYM BISIM_REL_cases]
66 >> ASM_REWRITE_TAC []
67QED
68
69(* (Strong) bisimilarity, the original definition *)
70Theorem BISIM_REL_def :
71 !ts. BISIM_REL ts = \p q. ?R. BISIM ts R /\ R p q
72Proof
73 SRW_TAC[][FUN_EQ_THM]
74 >> EQ_TAC
75 >| [ (* goal 1 (of 2) *)
76 DISCH_TAC >> Q.EXISTS_TAC `BISIM_REL ts` \\
77 ASM_REWRITE_TAC [BISIM_REL_IS_BISIM],
78 (* goal 2 (of 2) *)
79 Q.SPEC_TAC (`q`, `q`) \\
80 Q.SPEC_TAC (`p`, `p`) \\
81 HO_MATCH_MP_TAC BISIM_REL_coind \\ (* co-induction used here! *)
82 PROVE_TAC [BISIM_def] ]
83QED
84
85Theorem BISIM_REL_sym:
86 symmetric (BISIM_REL ts)
87Proof
88 SRW_TAC[][symmetric_def, BISIM_REL_def]
89 >> METIS_TAC[BISIM_INV, inv_DEF]
90QED
91
92Theorem BISIM_REL_IS_EQUIV_REL :
93 !ts. equivalence (BISIM_REL ts)
94Proof
95 SRW_TAC[][equivalence_def]
96 >- (SRW_TAC[][reflexive_def, BISIM_REL_def] \\
97 Q.EXISTS_TAC `Id` \\
98 REWRITE_TAC [BISIM_ID])
99 >- (SRW_TAC[][symmetric_def, BISIM_REL_def] \\
100 SRW_TAC[][EQ_IMP_THM] \\
101 Q.EXISTS_TAC `SC R` \\
102 FULL_SIMP_TAC (srw_ss ()) [BISIM_def, SC_DEF] \\
103 METIS_TAC[])
104 >- (SRW_TAC[][transitive_def, BISIM_REL_def] \\
105 Q.EXISTS_TAC `R' O R` \\
106 METIS_TAC [O_DEF, BISIM_O])
107QED
108
109Theorem BISIM_REL_EQUIV_rules =
110 BISIM_REL_IS_EQUIV_REL
111 |> SIMP_RULE bool_ss
112 [equivalence_def, reflexive_def, symmetric_def, transitive_def];
113
114Theorem BISIM_REL_ts:
115 ∀ts.
116 (∀p q l p'. BISIM_REL ts p q ∧ ts p l p'
117 ==> ∃q'. ts q l q' ∧ BISIM_REL ts p' q') ∧
118 (∀p q l q'. BISIM_REL ts p q ∧ ts q l q'
119 ==> ∃p'. ts p l p' ∧ BISIM_REL ts p' q')
120Proof
121 SRW_TAC[][BISIM_REL_def]
122 >> METIS_TAC[BISIM_def]
123QED
124
125Theorem BISIM_REL_strong_thm:
126 ∀ts.
127 BISIM_REL ts p0 q0 <=> ∃R. R p0 q0 ∧
128 (∀p q. R p q ⇒
129 ∀l. (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q')) ∧
130 (∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ (R p' q' ∨ BISIM_REL ts p' q')))
131Proof
132 SRW_TAC[][EQ_IMP_THM]
133 >- (Q.EXISTS_TAC `BISIM_REL ts`
134 >> SRW_TAC[][BISIM_REL_def, BISIM_def]
135 >> METIS_TAC[])
136 >> SRW_TAC[][BISIM_REL_def, BISIM_def]
137 >> Q.EXISTS_TAC `λp q. R p q ∨ BISIM_REL ts p q`
138 >> METIS_TAC[BISIM_REL_def, BISIM_def]
139QED
140
141Theorem BISIM_REL_strong_coind:
142 ∀ts R.
143 (∀p q. R p q ⇒
144 ∀l. (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q')) ∧
145 (∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ (R p' q' ∨ BISIM_REL ts p' q')))
146 ==> ∀p0 q0. R p0 q0 ==> BISIM_REL ts p0 q0
147Proof
148 SRW_TAC[][EQ_IMP_THM] >> SRW_TAC[][Once BISIM_REL_strong_thm]
149 >> Q.EXISTS_TAC `R` >> SRW_TAC[][]
150 >> METIS_TAC[]
151QED
152
153Theorem BISIM_REL_sym_thm:
154 ∀ts R.
155 BISIM_REL ts p0 q0 <=> ∃R. symmetric R ∧ R p0 q0 ∧
156 (∀p q. R p q ⇒ ∀l p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q')
157Proof
158 SRW_TAC[][EQ_IMP_THM, symmetric_def, BISIM_REL_def]
159 >| [Q.EXISTS_TAC `λp q. R p q ∨ R q p`, SRW_TAC[][]]
160 >> METIS_TAC[BISIM_INV, BISIM_def]
161QED
162
163Theorem BISIM_REL_sym_coind:
164 ∀ts R. symmetric R ∧
165 (∀p q. R p q ⇒ ∀l p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q')
166 ==> ∀p0 q0. R p0 q0 ==> BISIM_REL ts p0 q0
167Proof
168 SRW_TAC[][EQ_IMP_THM] >> SRW_TAC[][Once BISIM_REL_sym_thm]
169 >> Q.EXISTS_TAC `R` >> SRW_TAC[][]
170 >> METIS_TAC[]
171QED
172
173Theorem BISIM_REL_sym_strong_thm:
174 ∀ts R.
175 BISIM_REL ts p0 q0 <=> ∃R. symmetric R ∧ R p0 q0 ∧
176 (∀p q. R p q ⇒ ∀l p'. ts p l p'
177 ==> ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q'))
178Proof
179 SRW_TAC[][EQ_IMP_THM]
180 >- METIS_TAC[BISIM_REL_sym_thm]
181 >> PURE_ONCE_REWRITE_TAC[BISIM_REL_strong_thm]
182 >> Q.EXISTS_TAC `λp q. R p q ∨ R q p`
183 >> METIS_TAC[symmetric_def, BISIM_REL_EQUIV_rules]
184QED
185
186Theorem BISIM_REL_sym_strong_coind:
187 ∀ts R. symmetric R ∧
188 (∀p q. R p q ==> ∀l p'. ts p l p'
189 ==> ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q'))
190 ==> ∀p0 q0. R p0 q0 ==> BISIM_REL ts p0 q0
191Proof
192 SRW_TAC[][EQ_IMP_THM] >> SRW_TAC[][Once BISIM_REL_sym_strong_thm]
193 >> Q.EXISTS_TAC `R` >> SRW_TAC[][]
194 >> METIS_TAC[]
195QED
196
197(*---------------------------------------------------------------------------*)
198(* Weak bisimulation *)
199(*---------------------------------------------------------------------------*)
200
201(* Empty transition: zero or more invisible actions *)
202val ETS_def = new_definition ("ETS_def", (* was: EPS *)
203 ``ETS ts tau = RTC (\x y. ts x tau y)``);
204
205(* Weak transition *)
206val WTS_def = new_definition ("WTS_def",
207 ``WTS ts tau =
208 \p l q. ?p' q'. (ETS ts tau) p p' /\ ts p' l q' /\ (ETS ts tau) q' q``);
209
210(* Weak bisimulation *)
211val WBISIM_def = new_definition ("WBISIM_def",
212 ``WBISIM ts tau R =
213 !p q. R p q ==>
214 (!l. l <> tau ==>
215 (!p'. ts p l p' ==> ?q'. (WTS ts tau) q l q' /\ R p' q') /\
216 (!q'. ts q l q' ==> ?p'. (WTS ts tau) p l p' /\ R p' q')) /\
217 (!p'. ts p tau p' ==> ?q'. (ETS ts tau) q q' /\ R p' q') /\
218 (!q'. ts q tau q' ==> ?p'. (ETS ts tau) p p' /\ R p' q')``);
219
220(* Weak bisimilarity, see WBISIM_REL_def for an alternative definition *)
221CoInductive WBISIM_REL :
222 !p q.
223 (!l. l <> tau ==>
224 (!p'. ts p l p' ==> ?q'. WTS ts tau q l q' /\ WBISIM_REL ts tau p' q') /\
225 (!q'. ts q l q' ==> ?p'. WTS ts tau p l p' /\ WBISIM_REL ts tau p' q')) /\
226 (!p'. ts p tau p' ==> ?q'. ETS ts tau q q' /\ WBISIM_REL ts tau p' q') /\
227 (!q'. ts q tau q' ==> ?p'. ETS ts tau p p' /\ WBISIM_REL ts tau p' q')
228 ==>
229 WBISIM_REL ts tau p q
230End
231
232Theorem TS_IMP_ETS :
233 !ts tau p q. ts p tau q ==> (ETS ts tau) p q
234Proof
235 SRW_TAC[][ETS_def]
236 >> MATCH_MP_TAC RTC_SINGLE
237 >> BETA_TAC >> ASM_REWRITE_TAC []
238QED
239
240Theorem ETS_REFL :
241 !ts tau p. (ETS ts tau) p p
242Proof
243 SRW_TAC[][ETS_def, RTC_REFL]
244QED
245
246Theorem TS_IMP_WTS :
247 !ts tau p l q. ts p l q ==> WTS ts tau p l q
248Proof
249 SRW_TAC[][WTS_def]
250 >> Q.EXISTS_TAC `p`
251 >> Q.EXISTS_TAC `q`
252 >> ASM_REWRITE_TAC [ETS_REFL]
253QED
254
255Theorem ETS_TRANS :
256 !ts tau x y z. (ETS ts tau) x y /\ (ETS ts tau) y z
257 ==> (ETS ts tau) x z
258Proof
259 SRW_TAC[][ETS_def]
260 >> MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)
261 >> Q.EXISTS_TAC `y`
262 >> ASM_REWRITE_TAC []
263QED
264
265Theorem ETS_CASES:
266 ∀ts tau p p'. ETS ts tau p p' <=> p = p' ∨ ∃u. ts p tau u ∧ ETS ts tau u p'
267Proof
268 SRW_TAC[][ETS_def, Once RTC_CASES1]
269QED
270
271Theorem ETS_INDUCT[rule_induction]:
272 ∀ts tau P. (∀p. P p p) ∧ (
273 (∀p p' q. ts p tau p' ∧ P p' q ⇒ P p q) ∨
274 (∀p q' q. P p q' ∧ ts q' tau q ⇒ P p q)
275 ) ⇒ ∀p0 q0. ETS ts tau p0 q0 ⇒ P p0 q0
276Proof
277 STRIP_TAC >> STRIP_TAC >> GEN_TAC >> STRIP_TAC
278 >> REWRITE_TAC [ETS_def]
279 >| [HO_MATCH_MP_TAC RTC_INDUCT, HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1]
280 >> METIS_TAC []
281QED
282
283Theorem lemma1[local]:
284 !R. (!p q. ts p tau q ==> R p q) /\
285 (!p. R p p) /\
286 (!p q r. R p q /\ R q r ==> R p r)
287 ==> !p q. (ETS ts tau) p q ==> R p q
288Proof
289 GEN_TAC >> STRIP_TAC
290 >> REWRITE_TAC [ETS_def]
291 >> HO_MATCH_MP_TAC RTC_INDUCT
292 >> METIS_TAC []
293QED
294
295Theorem ETS_WTS_ETS :
296 !ts tau p p1 l p2 p'.
297 (ETS ts tau) p p1 /\ (WTS ts tau) p1 l p2 /\ (ETS ts tau) p2 p'
298 ==> (WTS ts tau) p l p'
299Proof
300 SRW_TAC[][WTS_def]
301 >> Q.EXISTS_TAC `p''`
302 >> Q.EXISTS_TAC `q'`
303 >> ASM_REWRITE_TAC []
304 >> METIS_TAC [ETS_TRANS]
305QED
306
307Theorem WBISIM_INV :
308 !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R)
309Proof
310 SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC []
311QED
312
313Theorem lemma2[local]:
314 !p p'. (ETS ts tau) p p' ==>
315 !R q. WBISIM ts tau R /\ R p q ==> ?q'. (ETS ts tau) q q' /\ R p' q'
316Proof
317 HO_MATCH_MP_TAC lemma1
318 >> SRW_TAC[][]
319 >| [ (* goal 1 (of 3) *)
320 FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
321 RES_TAC >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [],
322 (* goal 2 (of 3) *)
323 FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
324 RES_TAC >> Q.EXISTS_TAC `q` \\
325 ASM_REWRITE_TAC [ETS_def, RTC_REFL],
326 (* goal 3 (of 3) *)
327 `?q'. ETS ts tau q q' /\ R p' q'` by PROVE_TAC [] \\
328 `?q''. ETS ts tau q' q'' /\ R p'' q''` by PROVE_TAC [] \\
329 Q.EXISTS_TAC `q''` >> ASM_REWRITE_TAC [] \\
330 FULL_SIMP_TAC (srw_ss()) [ETS_def] \\
331 MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) \\
332 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] ]
333QED
334
335Theorem lemma2'[local]:
336 !q q'. (ETS ts tau) q q' ==>
337 !R p. WBISIM ts tau R /\ R p q ==>
338 ?p'. (ETS ts tau) p p' /\ R p' q'
339Proof
340 rpt STRIP_TAC
341 >> MP_TAC (Q.SPECL [`q`, `q'`] lemma2) >> SRW_TAC[][]
342 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
343 >> IMP_RES_TAC WBISIM_INV
344 >> SRW_TAC[][]
345QED
346
347(* p ==> p1 -l-> p2 ==> p'
348 R R R R
349 q ==> q1 =l=> q2 ==> q'
350 *)
351Theorem lemma3[local]:
352 !p l p'. (WTS ts tau) p l p' /\ l <> tau ==>
353 !R q. WBISIM ts tau R /\ R p q ==>
354 ?q'. (WTS ts tau) q l q' /\ R p' q'
355Proof
356 rpt STRIP_TAC
357 >> `?p1 p2. (ETS ts tau) p p1 /\ ts p1 l p2 /\ (ETS ts tau) p2 p'`
358 by PROVE_TAC [WTS_def]
359 >> `?q1. (ETS ts tau) q q1 /\ R p1 q1` by PROVE_TAC [lemma2]
360 >> `?q2. (WTS ts tau) q1 l q2 /\ R p2 q2` by PROVE_TAC [WBISIM_def]
361 >> `?q'. (ETS ts tau) q2 q' /\ R p' q'` by PROVE_TAC [lemma2]
362 >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC []
363 >> MATCH_MP_TAC ETS_WTS_ETS
364 >> Q.EXISTS_TAC `q1`
365 >> Q.EXISTS_TAC `q2`
366 >> ASM_REWRITE_TAC []
367QED
368
369Theorem lemma3'[local]:
370 !q l q'. (WTS ts tau) q l q' /\ l <> tau ==>
371 !R p. WBISIM ts tau R /\ R p q ==>
372 ?p'. (WTS ts tau) p l p' /\ R p' q'
373Proof
374 rpt STRIP_TAC
375 >> MP_TAC (Q.SPECL [`q`, `l`, `q'`] lemma3) >> SRW_TAC[][]
376 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
377 >> IMP_RES_TAC WBISIM_INV
378 >> SRW_TAC[][]
379QED
380
381Theorem WBISIM_ID :
382 !ts tau. WBISIM ts tau Id
383Proof
384 SRW_TAC[][WBISIM_def]
385 >- (MATCH_MP_TAC TS_IMP_WTS >> ASM_REWRITE_TAC [])
386 >> MATCH_MP_TAC TS_IMP_ETS >> ASM_REWRITE_TAC []
387QED
388
389Theorem WBISIM_O :
390 !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
391 WBISIM ts tau (R' O R)
392Proof
393 rpt STRIP_TAC
394 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
395 >> SRW_TAC[][O_DEF]
396 >| [ METIS_TAC [WBISIM_def, lemma3],
397 METIS_TAC [WBISIM_def, lemma3'],
398 METIS_TAC [WBISIM_def, lemma2],
399 METIS_TAC [WBISIM_def, lemma2'] ]
400QED
401
402Theorem WBISIM_RUNION :
403 !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
404 WBISIM ts tau (R RUNION R')
405Proof
406 rpt GEN_TAC
407 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
408 >> REWRITE_TAC [RUNION] >> BETA_TAC
409 >> rpt STRIP_TAC
410 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
411 >| [ Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
412 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
413 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
414 Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'` ]
415 >> ASM_REWRITE_TAC []
416QED
417
418Theorem WBISIM_REL_IS_WBISIM :
419 !ts tau. WBISIM ts tau (WBISIM_REL ts tau)
420Proof
421 PURE_ONCE_REWRITE_TAC [WBISIM_def]
422 >> rpt GEN_TAC >> DISCH_TAC
423 >> PURE_ONCE_REWRITE_TAC [GSYM WBISIM_REL_cases]
424 >> ASM_REWRITE_TAC []
425QED
426
427(* Weak bisimilarity, the original definition *)
428Theorem WBISIM_REL_def :
429 !ts tau. WBISIM_REL ts tau = \p q. ?R. WBISIM ts tau R /\ R p q
430Proof
431 SRW_TAC[][FUN_EQ_THM]
432 >> EQ_TAC
433 >| [ (* goal 1 (of 2) *)
434 DISCH_TAC >> Q.EXISTS_TAC `WBISIM_REL ts tau` \\
435 ASM_REWRITE_TAC [WBISIM_REL_IS_WBISIM],
436 (* goal 2 (of 2) *)
437 Q.SPEC_TAC (`q`, `q`) \\
438 Q.SPEC_TAC (`p`, `p`) \\
439 HO_MATCH_MP_TAC WBISIM_REL_coind \\ (* co-induction used here! *)
440 PROVE_TAC [WBISIM_def] ]
441QED
442
443Theorem WBISIM_REL_IS_EQUIV_REL :
444 !ts tau. equivalence (WBISIM_REL ts tau)
445Proof
446 SRW_TAC[][equivalence_def]
447 >- (SRW_TAC[][reflexive_def, WBISIM_REL_def] \\
448 Q.EXISTS_TAC `Id` \\
449 SRW_TAC[][WBISIM_def, WBISIM_ID])
450 >- (SRW_TAC[][symmetric_def, WBISIM_REL_def] \\
451 SRW_TAC[][EQ_IMP_THM] \\
452 Q.EXISTS_TAC `SC R` \\
453 FULL_SIMP_TAC (srw_ss ()) [WBISIM_def, SC_DEF] \\
454 METIS_TAC [])
455 >- (SRW_TAC[][transitive_def, WBISIM_REL_def]
456>> Q.EXISTS_TAC `R' O R` \\
457 METIS_TAC [WBISIM_O, O_DEF])
458QED
459
460Theorem WBISIM_REL_EQUIV_rules =
461 WBISIM_REL_IS_EQUIV_REL
462 |> SIMP_RULE bool_ss
463 [equivalence_def, reflexive_def, symmetric_def, transitive_def];
464
465Theorem WBISIM_REL_ts:
466 ∀ts tau.
467 (∀p q l p'. WBISIM_REL ts tau p q ∧ ts p l p' ∧ l ≠ tau
468 ==> ∃q'. WTS ts tau q l q' ∧ WBISIM_REL ts tau p' q') ∧
469 (∀p q l q'. WBISIM_REL ts tau p q ∧ ts q l q' ∧ l ≠ tau
470 ==> ∃p'. WTS ts tau p l p' ∧ WBISIM_REL ts tau p' q') ∧
471 (∀p q p'. WBISIM_REL ts tau p q ∧ ts p tau p'
472 ==> ∃q'. ETS ts tau q q' ∧ WBISIM_REL ts tau p' q') ∧
473 (∀p q q'. WBISIM_REL ts tau p q ∧ ts q tau q'
474 ==> ∃p'. ETS ts tau p p' ∧ WBISIM_REL ts tau p' q')
475Proof
476 SRW_TAC[][WBISIM_REL_def]
477 >> METIS_TAC[WBISIM_def]
478QED
479
480(*---------------------------------------------------------------------------*)
481(* Relations between strong and weak bisimulations *)
482(*---------------------------------------------------------------------------*)
483
484Theorem BISIM_IMP_WBISIM :
485 !ts tau R. BISIM ts R ==> WBISIM ts tau R
486Proof
487 SRW_TAC[][WBISIM_def] (* 4 goals *)
488 >> IMP_RES_TAC BISIM_def
489 >| [ (* goal 1 (of 4) *)
490 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
491 MATCH_MP_TAC TS_IMP_WTS,
492 (* goal 2 (of 4) *)
493 Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
494 MATCH_MP_TAC TS_IMP_WTS,
495 (* goal 3 (of 4) *)
496 Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
497 MATCH_MP_TAC TS_IMP_ETS,
498 (* goal 4 (of 4) *)
499 Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
500 MATCH_MP_TAC TS_IMP_ETS ]
501 >> ASM_REWRITE_TAC []
502QED
503
504Theorem BISIM_REL_RSUBSET_WBISIM_REL :
505 !ts tau. (BISIM_REL ts) RSUBSET (WBISIM_REL ts tau)
506Proof
507 SRW_TAC[][RSUBSET, BISIM_REL_def, WBISIM_REL_def]
508 >> Q.EXISTS_TAC `R` >> ASM_REWRITE_TAC []
509 >> MATCH_MP_TAC BISIM_IMP_WBISIM
510 >> ASM_REWRITE_TAC []
511QED
512
513Theorem BISIM_REL_IMP_WBISIM_REL :
514 !ts tau p q. (BISIM_REL ts) p q ==> (WBISIM_REL ts tau) p q
515Proof
516 REWRITE_TAC [GSYM RSUBSET, BISIM_REL_RSUBSET_WBISIM_REL]
517QED