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_strong_thm:
93  BISIM_REL ts p0 q0 <=> ∃R. R p0 q0 ∧
94    (∀p q. R p q ⇒
95      ∀l. (∀p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q')) ∧
96           (∀q'. ts q l q' ⇒ ∃p'. ts p l p' ∧ (R p' q' ∨ BISIM_REL ts p' q')))
97Proof
98  SRW_TAC[][EQ_IMP_THM]
99  >- (Q.EXISTS_TAC `BISIM_REL ts`
100      >> SRW_TAC[][BISIM_REL_def, BISIM_def]
101      >> METIS_TAC[])
102  >> SRW_TAC[][BISIM_REL_def, BISIM_def]
103  >> Q.EXISTS_TAC `λp q. R p q ∨ BISIM_REL ts p q`
104  >> METIS_TAC[BISIM_REL_def, BISIM_def]
105QED
106
107Theorem BISIM_REL_sym_thm:
108  BISIM_REL ts p0 q0 <=> ∃R. symmetric R ∧ R p0 q0 ∧
109    (∀p q. R p q ⇒ ∀l p'. ts p l p' ⇒ ∃q'. ts q l q' ∧ R p' q')
110Proof
111  SRW_TAC[][EQ_IMP_THM, symmetric_def, BISIM_REL_def]
112  >| [Q.EXISTS_TAC `λp q. R p q ∨ R q p`, SRW_TAC[][]]
113  >> METIS_TAC[BISIM_INV, BISIM_def]
114QED
115
116Theorem BISIM_REL_sym_strong_thm:
117  BISIM_REL ts p0 q0 <=>
118    ∃R. symmetric R ∧ R p0 q0 ∧
119        (∀p q. R p q ⇒
120               ∀l p'. ts p l p' ⇒
121                      ∃q'. ts q l q' ∧ (R p' q' ∨ BISIM_REL ts p' q'))
122Proof
123  SRW_TAC[][EQ_IMP_THM]
124  >- METIS_TAC[BISIM_REL_sym_thm]
125  >> PURE_ONCE_REWRITE_TAC[BISIM_REL_strong_thm]
126  >> Q.EXISTS_TAC `λp q. R p q ∨ R q p`
127  >> METIS_TAC[symmetric_def, BISIM_REL_sym]
128QED
129
130Theorem BISIM_REL_IS_EQUIV_REL :
131    !ts. equivalence (BISIM_REL ts)
132Proof
133    SRW_TAC[][equivalence_def]
134 >- (SRW_TAC[][reflexive_def, BISIM_REL_def] \\
135     Q.EXISTS_TAC `Id` \\
136     REWRITE_TAC [BISIM_ID])
137 >- (SRW_TAC[][symmetric_def, BISIM_REL_def] \\
138     SRW_TAC[][EQ_IMP_THM] \\
139     Q.EXISTS_TAC `SC R` \\
140     FULL_SIMP_TAC (srw_ss ()) [BISIM_def, SC_DEF] \\
141     METIS_TAC[])
142 >- (SRW_TAC[][transitive_def, BISIM_REL_def] \\
143     Q.EXISTS_TAC `R' O R` \\
144     METIS_TAC [O_DEF, BISIM_O])
145QED
146
147
148(*---------------------------------------------------------------------------*)
149(*  Weak bisimulation                                                        *)
150(*---------------------------------------------------------------------------*)
151
152(* Empty transition: zero or more invisible actions *)
153val ETS_def = new_definition ("ETS_def", (* was: EPS *)
154  ``ETS ts tau = RTC (\x y. ts x tau y)``);
155
156(* Weak transition *)
157val WTS_def = new_definition ("WTS_def",
158  ``WTS ts tau =
159     \p l q. ?p' q'. (ETS ts tau) p p' /\ ts p' l q' /\ (ETS ts tau) q' q``);
160
161(* Weak bisimulation *)
162val WBISIM_def = new_definition ("WBISIM_def",
163  ``WBISIM ts tau R =
164     !p q. R p q ==>
165          (!l. l <> tau ==>
166            (!p'. ts p l p' ==> ?q'. (WTS ts tau) q l q' /\ R p' q') /\
167            (!q'. ts q l q' ==> ?p'. (WTS ts tau) p l p' /\ R p' q')) /\
168          (!p'. ts p tau p' ==> ?q'. (ETS ts tau) q   q' /\ R p' q') /\
169          (!q'. ts q tau q' ==> ?p'. (ETS ts tau) p   p' /\ R p' q')``);
170
171(* Weak bisimilarity, see WBISIM_REL_def for an alternative definition *)
172CoInductive WBISIM_REL :
173  !p q.
174    (!l. l <> tau ==>
175      (!p'. ts p l p' ==> ?q'. WTS ts tau q l q' /\ WBISIM_REL ts tau p' q') /\
176      (!q'. ts q l q' ==> ?p'. WTS ts tau p l p' /\ WBISIM_REL ts tau p' q')) /\
177    (!p'. ts p tau p' ==> ?q'. ETS ts tau q   q' /\ WBISIM_REL ts tau p' q') /\
178    (!q'. ts q tau q' ==> ?p'. ETS ts tau p   p' /\ WBISIM_REL ts tau p' q')
179   ==>
180    WBISIM_REL ts tau p q
181End
182
183Theorem TS_IMP_ETS :
184    !ts tau p q. ts p tau q ==> (ETS ts tau) p q
185Proof
186    SRW_TAC[][ETS_def]
187 >> MATCH_MP_TAC RTC_SINGLE
188 >> BETA_TAC >> ASM_REWRITE_TAC []
189QED
190
191Theorem ETS_REFL :
192    !ts tau p. (ETS ts tau) p p
193Proof
194    SRW_TAC[][ETS_def, RTC_REFL]
195QED
196
197Theorem TS_IMP_WTS :
198    !ts tau p l q. ts p l q ==> WTS ts tau p l q
199Proof
200    SRW_TAC[][WTS_def]
201 >> Q.EXISTS_TAC `p`
202 >> Q.EXISTS_TAC `q`
203 >> ASM_REWRITE_TAC [ETS_REFL]
204QED
205
206Theorem ETS_TRANS :
207    !ts tau x y z. (ETS ts tau) x y /\ (ETS ts tau) y z
208               ==> (ETS ts tau) x z
209Proof
210    SRW_TAC[][ETS_def]
211 >> MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)
212 >> Q.EXISTS_TAC `y`
213 >> ASM_REWRITE_TAC []
214QED
215
216Theorem lemma1[local]:
217    !R. (!p q.   ts p tau q ==> R p q) /\
218        (!p.     R p p) /\
219        (!p q r. R p q /\ R q r ==> R p r)
220    ==> !p q. (ETS ts tau) p q ==> R p q
221Proof
222    GEN_TAC >> STRIP_TAC
223 >> REWRITE_TAC [ETS_def]
224 >> HO_MATCH_MP_TAC RTC_INDUCT
225 >> METIS_TAC []
226QED
227
228Theorem ETS_WTS_ETS :
229    !ts tau p p1 l p2 p'.
230        (ETS ts tau) p p1 /\ (WTS ts tau) p1 l p2 /\ (ETS ts tau) p2 p'
231    ==> (WTS ts tau) p l p'
232Proof
233    SRW_TAC[][WTS_def]
234 >> Q.EXISTS_TAC `p''`
235 >> Q.EXISTS_TAC `q'`
236 >> ASM_REWRITE_TAC []
237 >> METIS_TAC [ETS_TRANS]
238QED
239
240Theorem WBISIM_INV :
241    !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R)
242Proof
243    SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC []
244QED
245
246Theorem lemma2[local]:
247  !p p'. (ETS ts tau) p p' ==>
248         !R q. WBISIM ts tau R /\ R p q ==> ?q'. (ETS ts tau) q q' /\ R p' q'
249Proof
250    HO_MATCH_MP_TAC lemma1
251 >> SRW_TAC[][]
252 >| [ (* goal 1 (of 3) *)
253      FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
254      RES_TAC >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [],
255      (* goal 2 (of 3) *)
256      FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
257      RES_TAC >> Q.EXISTS_TAC `q` \\
258      ASM_REWRITE_TAC [ETS_def, RTC_REFL],
259      (* goal 3 (of 3) *)
260     `?q'. ETS ts tau q q' /\ R p' q'` by PROVE_TAC [] \\
261     `?q''. ETS ts tau q' q'' /\ R p'' q''` by PROVE_TAC [] \\
262      Q.EXISTS_TAC `q''` >> ASM_REWRITE_TAC [] \\
263      FULL_SIMP_TAC (srw_ss()) [ETS_def] \\
264      MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) \\
265      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] ]
266QED
267
268Theorem lemma2'[local]:
269    !q q'. (ETS ts tau) q q' ==>
270           !R p. WBISIM ts tau R /\ R p q ==>
271                 ?p'. (ETS ts tau) p p' /\ R p' q'
272Proof
273    rpt STRIP_TAC
274 >> MP_TAC (Q.SPECL [`q`, `q'`] lemma2) >> SRW_TAC[][]
275 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
276 >> IMP_RES_TAC WBISIM_INV
277 >> SRW_TAC[][]
278QED
279
280(* p ==> p1 -l-> p2 ==> p'
281   R     R       R      R
282   q ==> q1 =l=> q2 ==> q'
283 *)
284Theorem lemma3[local]:
285    !p l p'. (WTS ts tau) p l p' /\ l <> tau ==>
286             !R q. WBISIM ts tau R /\ R p q ==>
287                   ?q'. (WTS ts tau) q l q' /\ R p' q'
288Proof
289    rpt STRIP_TAC
290 >> `?p1 p2. (ETS ts tau) p p1 /\ ts p1 l p2 /\ (ETS ts tau) p2 p'`
291        by PROVE_TAC [WTS_def]
292 >> `?q1. (ETS ts tau) q q1 /\ R p1 q1` by PROVE_TAC [lemma2]
293 >> `?q2. (WTS ts tau) q1 l q2 /\ R p2 q2` by PROVE_TAC [WBISIM_def]
294 >> `?q'. (ETS ts tau) q2 q' /\ R p' q'` by PROVE_TAC [lemma2]
295 >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC []
296 >> MATCH_MP_TAC ETS_WTS_ETS
297 >> Q.EXISTS_TAC `q1`
298 >> Q.EXISTS_TAC `q2`
299 >> ASM_REWRITE_TAC []
300QED
301
302Theorem lemma3'[local]:
303    !q l q'. (WTS ts tau) q l q' /\ l <> tau ==>
304             !R p. WBISIM ts tau R /\ R p q ==>
305                   ?p'. (WTS ts tau) p l p' /\ R p' q'
306Proof
307    rpt STRIP_TAC
308 >> MP_TAC (Q.SPECL [`q`, `l`, `q'`] lemma3) >> SRW_TAC[][]
309 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
310 >> IMP_RES_TAC WBISIM_INV
311 >> SRW_TAC[][]
312QED
313
314Theorem WBISIM_ID :
315    !ts tau. WBISIM ts tau Id
316Proof
317    SRW_TAC[][WBISIM_def]
318 >- (MATCH_MP_TAC TS_IMP_WTS >> ASM_REWRITE_TAC [])
319 >> MATCH_MP_TAC TS_IMP_ETS >> ASM_REWRITE_TAC []
320QED
321
322Theorem WBISIM_O :
323    !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
324                  WBISIM ts tau (R' O R)
325Proof
326    rpt STRIP_TAC
327 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
328 >> SRW_TAC[][O_DEF]
329 >| [ METIS_TAC [WBISIM_def, lemma3],
330      METIS_TAC [WBISIM_def, lemma3'],
331      METIS_TAC [WBISIM_def, lemma2],
332      METIS_TAC [WBISIM_def, lemma2'] ]
333QED
334
335Theorem WBISIM_RUNION :
336    !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
337                  WBISIM ts tau (R RUNION R')
338Proof
339    rpt GEN_TAC
340 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
341 >> REWRITE_TAC [RUNION] >> BETA_TAC
342 >> rpt STRIP_TAC
343 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
344 >| [ Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
345      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
346      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
347      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'` ]
348 >> ASM_REWRITE_TAC []
349QED
350
351Theorem WBISIM_REL_IS_WBISIM :
352    !ts tau. WBISIM ts tau (WBISIM_REL ts tau)
353Proof
354    PURE_ONCE_REWRITE_TAC [WBISIM_def]
355 >> rpt GEN_TAC >> DISCH_TAC
356 >> PURE_ONCE_REWRITE_TAC [GSYM WBISIM_REL_cases]
357 >> ASM_REWRITE_TAC []
358QED
359
360(* Weak bisimilarity, the original definition *)
361Theorem WBISIM_REL_def :
362    !ts tau. WBISIM_REL ts tau = \p q. ?R. WBISIM ts tau R /\ R p q
363Proof
364    SRW_TAC[][FUN_EQ_THM]
365 >> EQ_TAC
366 >| [ (* goal 1 (of 2) *)
367      DISCH_TAC >> Q.EXISTS_TAC `WBISIM_REL ts tau` \\
368      ASM_REWRITE_TAC [WBISIM_REL_IS_WBISIM],
369      (* goal 2 (of 2) *)
370      Q.SPEC_TAC (`q`, `q`) \\
371      Q.SPEC_TAC (`p`, `p`) \\
372      HO_MATCH_MP_TAC WBISIM_REL_coind \\ (* co-induction used here! *)
373      PROVE_TAC [WBISIM_def] ]
374QED
375
376Theorem WBISIM_REL_IS_EQUIV_REL :
377    !ts tau. equivalence (WBISIM_REL ts tau)
378Proof
379  SRW_TAC[][equivalence_def]
380  >- (SRW_TAC[][reflexive_def, WBISIM_REL_def] \\
381      Q.EXISTS_TAC `Id` \\
382      SRW_TAC[][WBISIM_def, WBISIM_ID])
383  >- (SRW_TAC[][symmetric_def, WBISIM_REL_def] \\
384      SRW_TAC[][EQ_IMP_THM] \\
385      Q.EXISTS_TAC `SC R` \\
386      FULL_SIMP_TAC (srw_ss ()) [WBISIM_def, SC_DEF] \\
387      METIS_TAC [])
388  >- (SRW_TAC[][transitive_def, WBISIM_REL_def]
389>> Q.EXISTS_TAC `R' O R` \\
390      METIS_TAC [WBISIM_O, O_DEF])
391QED
392
393
394(*---------------------------------------------------------------------------*)
395(*  Relations between strong and weak bisimulations                          *)
396(*---------------------------------------------------------------------------*)
397
398Theorem BISIM_IMP_WBISIM :
399    !ts tau R. BISIM ts R ==> WBISIM ts tau R
400Proof
401    SRW_TAC[][WBISIM_def] (* 4 goals *)
402 >> IMP_RES_TAC BISIM_def
403 >| [ (* goal 1 (of 4) *)
404      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
405      MATCH_MP_TAC TS_IMP_WTS,
406      (* goal 2 (of 4) *)
407      Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
408      MATCH_MP_TAC TS_IMP_WTS,
409      (* goal 3 (of 4) *)
410      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
411      MATCH_MP_TAC TS_IMP_ETS,
412      (* goal 4 (of 4) *)
413      Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
414      MATCH_MP_TAC TS_IMP_ETS ]
415 >> ASM_REWRITE_TAC []
416QED
417
418Theorem BISIM_REL_RSUBSET_WBISIM_REL :
419    !ts tau. (BISIM_REL ts) RSUBSET (WBISIM_REL ts tau)
420Proof
421    SRW_TAC[][RSUBSET, BISIM_REL_def, WBISIM_REL_def]
422 >> Q.EXISTS_TAC `R` >> ASM_REWRITE_TAC []
423 >> MATCH_MP_TAC BISIM_IMP_WBISIM
424 >> ASM_REWRITE_TAC []
425QED
426
427Theorem BISIM_REL_IMP_WBISIM_REL :
428    !ts tau p q. (BISIM_REL ts) p q ==> (WBISIM_REL ts tau) p q
429Proof
430    REWRITE_TAC [GSYM RSUBSET, BISIM_REL_RSUBSET_WBISIM_REL]
431QED
432
433