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