1(* ------------------------------------------------------------------------ *)
2(*  Bisimulations defined on general labeled transition ('a->'b->'a->bool)  *)
3(* ------------------------------------------------------------------------ *)
4
5open HolKernel Parse boolLib simpLib metisLib BasicProvers;
6open relationTheory;
7
8val _ = new_theory "bisimulation";
9
10(*---------------------------------------------------------------------------*)
11(*  (Strong) bisimulation                                                    *)
12(*---------------------------------------------------------------------------*)
13
14val BISIM_def = new_definition ("BISIM_def",
15  ``BISIM ts R = !p q.
16                    R p q ==> !l.
17                    (!p'. ts p l p' ==> ?q'. ts q l q' /\ R p' q') /\
18                    (!q'. ts q l q' ==> ?p'. ts p l p' /\ R p' q')``);
19
20(* (Strong) bisimilarity, see BISIM_REL_def for an alternative definition *)
21CoInductive BISIM_REL :
22    !p q. (!l.
23            (!p'. ts p l p' ==> ?q'. ts q l q' /\ (BISIM_REL ts) p' q') /\
24            (!q'. ts q l q' ==> ?p'. ts p l p' /\ (BISIM_REL ts) p' q'))
25      ==> (BISIM_REL ts) p q
26End
27
28Theorem BISIM_ID :
29    !ts. BISIM ts Id
30Proof
31    SRW_TAC[][BISIM_def]
32QED
33
34Theorem BISIM_INV :
35    !ts R. BISIM ts R ==> BISIM ts (inv R)
36Proof
37    SRW_TAC[][BISIM_def, inv_DEF] >> METIS_TAC []
38QED
39
40Theorem BISIM_O :
41    !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R' O R)
42Proof
43    rpt STRIP_TAC
44 >> PURE_ONCE_REWRITE_TAC [BISIM_def]
45 >> SRW_TAC[][O_DEF]
46 >> METIS_TAC[BISIM_def]
47QED
48
49Theorem BISIM_RUNION :
50    !ts R R'. BISIM ts R /\ BISIM ts R' ==> BISIM ts (R RUNION R')
51Proof
52    rpt GEN_TAC
53 >> PURE_ONCE_REWRITE_TAC [BISIM_def]
54 >> SRW_TAC[][RUNION]
55 >> METIS_TAC[]
56QED
57
58Theorem BISIM_REL_IS_BISIM :
59    !ts. BISIM ts (BISIM_REL ts)
60Proof
61    PURE_ONCE_REWRITE_TAC [BISIM_def]
62 >> rpt GEN_TAC >> DISCH_TAC
63 >> Q.SPEC_TAC (`l`, `l`)
64 >> PURE_ONCE_REWRITE_TAC [GSYM BISIM_REL_cases]
65 >> ASM_REWRITE_TAC []
66QED
67
68(* (Strong) bisimilarity, the original definition *)
69Theorem BISIM_REL_def :
70    !ts. BISIM_REL ts = \p q. ?R. BISIM ts R /\ R p q
71Proof
72    SRW_TAC[][FUN_EQ_THM]
73 >> EQ_TAC
74 >| [ (* goal 1 (of 2) *)
75      DISCH_TAC >> Q.EXISTS_TAC `BISIM_REL ts` \\
76      ASM_REWRITE_TAC [BISIM_REL_IS_BISIM],
77      (* goal 2 (of 2) *)
78      Q.SPEC_TAC (`q`, `q`) \\
79      Q.SPEC_TAC (`p`, `p`) \\
80      HO_MATCH_MP_TAC BISIM_REL_coind \\ (* co-induction used here! *)
81      PROVE_TAC [BISIM_def] ]
82QED
83
84Theorem BISIM_REL_IS_EQUIV_REL :
85    !ts. equivalence (BISIM_REL ts)
86Proof
87    SRW_TAC[][equivalence_def]
88 >- (SRW_TAC[][reflexive_def, BISIM_REL_def] \\
89     Q.EXISTS_TAC `Id` \\
90     REWRITE_TAC [BISIM_ID])
91 >- (SRW_TAC[][symmetric_def, BISIM_REL_def] \\
92     SRW_TAC[][EQ_IMP_THM] \\
93     Q.EXISTS_TAC `SC R` \\
94     FULL_SIMP_TAC (srw_ss ()) [BISIM_def, SC_DEF] \\
95     METIS_TAC[])
96 >- (SRW_TAC[][transitive_def, BISIM_REL_def] \\
97     Q.EXISTS_TAC `R' O R` \\
98     METIS_TAC [O_DEF, BISIM_O])
99QED
100
101
102(*---------------------------------------------------------------------------*)
103(*  Weak bisimulation                                                        *)
104(*---------------------------------------------------------------------------*)
105
106(* Empty transition: zero or more invisible actions *)
107val ETS_def = new_definition ("ETS_def", (* was: EPS *)
108  ``ETS ts tau = RTC (\x y. ts x tau y)``);
109
110(* Weak transition *)
111val WTS_def = new_definition ("WTS_def",
112  ``WTS ts tau =
113     \p l q. ?p' q'. (ETS ts tau) p p' /\ ts p' l q' /\ (ETS ts tau) q' q``);
114
115(* Weak bisimulation *)
116val WBISIM_def = new_definition ("WBISIM_def",
117  ``WBISIM ts tau R =
118     !p q. R p q ==>
119          (!l. l <> tau ==>
120            (!p'. ts p l p' ==> ?q'. (WTS ts tau) q l q' /\ R p' q') /\
121            (!q'. ts q l q' ==> ?p'. (WTS ts tau) p l p' /\ R p' q')) /\
122          (!p'. ts p tau p' ==> ?q'. (ETS ts tau) q   q' /\ R p' q') /\
123          (!q'. ts q tau q' ==> ?p'. (ETS ts tau) p   p' /\ R p' q')``);
124
125(* Weak bisimilarity, see WBISIM_REL_def for an alternative definition *)
126CoInductive WBISIM_REL :
127  !p q.
128    (!l. l <> tau ==>
129      (!p'. ts p l p' ==> ?q'. WTS ts tau q l q' /\ WBISIM_REL ts tau p' q') /\
130      (!q'. ts q l q' ==> ?p'. WTS ts tau p l p' /\ WBISIM_REL ts tau p' q')) /\
131    (!p'. ts p tau p' ==> ?q'. ETS ts tau q   q' /\ WBISIM_REL ts tau p' q') /\
132    (!q'. ts q tau q' ==> ?p'. ETS ts tau p   p' /\ WBISIM_REL ts tau p' q')
133   ==>
134    WBISIM_REL ts tau p q
135End
136
137Theorem TS_IMP_ETS :
138    !ts tau p q. ts p tau q ==> (ETS ts tau) p q
139Proof
140    SRW_TAC[][ETS_def]
141 >> MATCH_MP_TAC RTC_SINGLE
142 >> BETA_TAC >> ASM_REWRITE_TAC []
143QED
144
145Theorem ETS_REFL :
146    !ts tau p. (ETS ts tau) p p
147Proof
148    SRW_TAC[][ETS_def, RTC_REFL]
149QED
150
151Theorem TS_IMP_WTS :
152    !ts tau p l q. ts p l q ==> WTS ts tau p l q
153Proof
154    SRW_TAC[][WTS_def]
155 >> Q.EXISTS_TAC `p`
156 >> Q.EXISTS_TAC `q`
157 >> ASM_REWRITE_TAC [ETS_REFL]
158QED
159
160Theorem ETS_TRANS :
161    !ts tau x y z. (ETS ts tau) x y /\ (ETS ts tau) y z
162               ==> (ETS ts tau) x z
163Proof
164    SRW_TAC[][ETS_def]
165 >> MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)
166 >> Q.EXISTS_TAC `y`
167 >> ASM_REWRITE_TAC []
168QED
169
170val lemma1 = prove (
171  ``!R. (!p q.   ts p tau q ==> R p q) /\
172        (!p.     R p p) /\
173        (!p q r. R p q /\ R q r ==> R p r)
174    ==> !p q. (ETS ts tau) p q ==> R p q``,
175    GEN_TAC >> STRIP_TAC
176 >> REWRITE_TAC [ETS_def]
177 >> HO_MATCH_MP_TAC RTC_INDUCT
178 >> METIS_TAC []);
179
180Theorem ETS_WTS_ETS :
181    !ts tau p p1 l p2 p'.
182        (ETS ts tau) p p1 /\ (WTS ts tau) p1 l p2 /\ (ETS ts tau) p2 p'
183    ==> (WTS ts tau) p l p'
184Proof
185    SRW_TAC[][WTS_def]
186 >> Q.EXISTS_TAC `p''`
187 >> Q.EXISTS_TAC `q'`
188 >> ASM_REWRITE_TAC []
189 >> METIS_TAC [ETS_TRANS]
190QED
191
192Theorem WBISIM_INV :
193    !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R)
194Proof
195    SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC []
196QED
197
198Theorem lemma2[local]:
199  !p p'. (ETS ts tau) p p' ==>
200         !R q. WBISIM ts tau R /\ R p q ==> ?q'. (ETS ts tau) q q' /\ R p' q'
201Proof
202    HO_MATCH_MP_TAC lemma1
203 >> SRW_TAC[][]
204 >| [ (* goal 1 (of 3) *)
205      FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
206      RES_TAC >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [],
207      (* goal 2 (of 3) *)
208      FULL_SIMP_TAC (srw_ss()) [WBISIM_def] \\
209      RES_TAC >> Q.EXISTS_TAC `q` \\
210      ASM_REWRITE_TAC [ETS_def, RTC_REFL],
211      (* goal 3 (of 3) *)
212     `?q'. ETS ts tau q q' /\ R p' q'` by PROVE_TAC [] \\
213     `?q''. ETS ts tau q' q'' /\ R p'' q''` by PROVE_TAC [] \\
214      Q.EXISTS_TAC `q''` >> ASM_REWRITE_TAC [] \\
215      FULL_SIMP_TAC (srw_ss()) [ETS_def] \\
216      MATCH_MP_TAC (REWRITE_RULE [transitive_def] RTC_TRANSITIVE) \\
217      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] ]
218QED
219
220val lemma2' = prove (
221  ``!q q'. (ETS ts tau) q q' ==>
222           !R p. WBISIM ts tau R /\ R p q ==>
223                 ?p'. (ETS ts tau) p p' /\ R p' q'``,
224    rpt STRIP_TAC
225 >> MP_TAC (Q.SPECL [`q`, `q'`] lemma2) >> SRW_TAC[][]
226 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
227 >> IMP_RES_TAC WBISIM_INV
228 >> SRW_TAC[][]);
229
230(* p ==> p1 -l-> p2 ==> p'
231   R     R       R      R
232   q ==> q1 =l=> q2 ==> q'
233 *)
234val lemma3 = prove (
235  ``!p l p'. (WTS ts tau) p l p' /\ l <> tau ==>
236             !R q. WBISIM ts tau R /\ R p q ==>
237                   ?q'. (WTS ts tau) q l q' /\ R p' q'``,
238    rpt STRIP_TAC
239 >> `?p1 p2. (ETS ts tau) p p1 /\ ts p1 l p2 /\ (ETS ts tau) p2 p'`
240        by PROVE_TAC [WTS_def]
241 >> `?q1. (ETS ts tau) q q1 /\ R p1 q1` by PROVE_TAC [lemma2]
242 >> `?q2. (WTS ts tau) q1 l q2 /\ R p2 q2` by PROVE_TAC [WBISIM_def]
243 >> `?q'. (ETS ts tau) q2 q' /\ R p' q'` by PROVE_TAC [lemma2]
244 >> Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC []
245 >> MATCH_MP_TAC ETS_WTS_ETS
246 >> Q.EXISTS_TAC `q1`
247 >> Q.EXISTS_TAC `q2`
248 >> ASM_REWRITE_TAC []);
249
250val lemma3' = prove (
251  ``!q l q'. (WTS ts tau) q l q' /\ l <> tau ==>
252             !R p. WBISIM ts tau R /\ R p q ==>
253                   ?p'. (WTS ts tau) p l p' /\ R p' q'``,
254    rpt STRIP_TAC
255 >> MP_TAC (Q.SPECL [`q`, `l`, `q'`] lemma3) >> SRW_TAC[][]
256 >> POP_ASSUM (MP_TAC o (REWRITE_RULE [inv_DEF]) o (Q.SPECL [`inv R`, `p`]))
257 >> IMP_RES_TAC WBISIM_INV
258 >> SRW_TAC[][]);
259
260Theorem WBISIM_ID :
261    !ts tau. WBISIM ts tau Id
262Proof
263    SRW_TAC[][WBISIM_def]
264 >- (MATCH_MP_TAC TS_IMP_WTS >> ASM_REWRITE_TAC [])
265 >> MATCH_MP_TAC TS_IMP_ETS >> ASM_REWRITE_TAC []
266QED
267
268Theorem WBISIM_INV :
269    !ts tau R. WBISIM ts tau R ==> WBISIM ts tau (inv R)
270Proof
271    SRW_TAC[][WBISIM_def, inv_DEF] >> METIS_TAC []
272QED
273
274Theorem WBISIM_O :
275    !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
276                  WBISIM ts tau (R' O R)
277Proof
278    rpt STRIP_TAC
279 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
280 >> SRW_TAC[][O_DEF]
281 >| [ METIS_TAC [WBISIM_def, lemma3],
282      METIS_TAC [WBISIM_def, lemma3'],
283      METIS_TAC [WBISIM_def, lemma2],
284      METIS_TAC [WBISIM_def, lemma2'] ]
285QED
286
287Theorem WBISIM_RUNION :
288    !ts tau R R'. WBISIM ts tau R /\ WBISIM ts tau R' ==>
289                  WBISIM ts tau (R RUNION R')
290Proof
291    rpt GEN_TAC
292 >> PURE_ONCE_REWRITE_TAC [WBISIM_def]
293 >> REWRITE_TAC [RUNION] >> BETA_TAC
294 >> rpt STRIP_TAC
295 >> RES_TAC (* 8 sub-goals here, the same last tactic *)
296 >| [ Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
297      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
298      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'`,
299      Q.EXISTS_TAC `q'`, Q.EXISTS_TAC `p'` ]
300 >> ASM_REWRITE_TAC []
301QED
302
303Theorem WBISIM_REL_IS_WBISIM :
304    !ts tau. WBISIM ts tau (WBISIM_REL ts tau)
305Proof
306    PURE_ONCE_REWRITE_TAC [WBISIM_def]
307 >> rpt GEN_TAC >> DISCH_TAC
308 >> PURE_ONCE_REWRITE_TAC [GSYM WBISIM_REL_cases]
309 >> ASM_REWRITE_TAC []
310QED
311
312(* Weak bisimilarity, the original definition *)
313Theorem WBISIM_REL_def :
314    !ts tau. WBISIM_REL ts tau = \p q. ?R. WBISIM ts tau R /\ R p q
315Proof
316    SRW_TAC[][FUN_EQ_THM]
317 >> EQ_TAC
318 >| [ (* goal 1 (of 2) *)
319      DISCH_TAC >> Q.EXISTS_TAC `WBISIM_REL ts tau` \\
320      ASM_REWRITE_TAC [WBISIM_REL_IS_WBISIM],
321      (* goal 2 (of 2) *)
322      Q.SPEC_TAC (`q`, `q`) \\
323      Q.SPEC_TAC (`p`, `p`) \\
324      HO_MATCH_MP_TAC WBISIM_REL_coind \\ (* co-induction used here! *)
325      PROVE_TAC [WBISIM_def] ]
326QED
327
328Theorem WBISIM_REL_IS_EQUIV_REL :
329    !ts tau. equivalence (WBISIM_REL ts tau)
330Proof
331  SRW_TAC[][equivalence_def]
332  >- (SRW_TAC[][reflexive_def, WBISIM_REL_def] \\
333      Q.EXISTS_TAC `Id` \\
334      SRW_TAC[][WBISIM_def, WBISIM_ID])
335  >- (SRW_TAC[][symmetric_def, WBISIM_REL_def] \\
336      SRW_TAC[][EQ_IMP_THM] \\
337      Q.EXISTS_TAC `SC R` \\
338      FULL_SIMP_TAC (srw_ss ()) [WBISIM_def, SC_DEF] \\
339      METIS_TAC [])
340  >- (SRW_TAC[][transitive_def, WBISIM_REL_def] >>
341      Q.EXISTS_TAC `R' O R` \\
342      METIS_TAC [WBISIM_O, O_DEF])
343QED
344
345
346(*---------------------------------------------------------------------------*)
347(*  Relations between strong and weak bisimulations                          *)
348(*---------------------------------------------------------------------------*)
349
350Theorem BISIM_IMP_WBISIM :
351    !ts tau R. BISIM ts R ==> WBISIM ts tau R
352Proof
353    SRW_TAC[][WBISIM_def] (* 4 goals *)
354 >> IMP_RES_TAC BISIM_def
355 >| [ (* goal 1 (of 4) *)
356      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
357      MATCH_MP_TAC TS_IMP_WTS,
358      (* goal 2 (of 4) *)
359      Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
360      MATCH_MP_TAC TS_IMP_WTS,
361      (* goal 3 (of 4) *)
362      Q.EXISTS_TAC `q'` >> ASM_REWRITE_TAC [] \\
363      MATCH_MP_TAC TS_IMP_ETS,
364      (* goal 4 (of 4) *)
365      Q.EXISTS_TAC `p'` >> ASM_REWRITE_TAC [] \\
366      MATCH_MP_TAC TS_IMP_ETS ]
367 >> ASM_REWRITE_TAC []
368QED
369
370Theorem BISIM_REL_RSUBSET_WBISIM_REL :
371    !ts tau. (BISIM_REL ts) RSUBSET (WBISIM_REL ts tau)
372Proof
373    SRW_TAC[][RSUBSET, BISIM_REL_def, WBISIM_REL_def]
374 >> Q.EXISTS_TAC `R` >> ASM_REWRITE_TAC []
375 >> MATCH_MP_TAC BISIM_IMP_WBISIM
376 >> ASM_REWRITE_TAC []
377QED
378
379Theorem BISIM_REL_IMP_WBISIM_REL :
380    !ts tau p q. (BISIM_REL ts) p q ==> (WBISIM_REL ts tau) p q
381Proof
382    REWRITE_TAC [GSYM RSUBSET, BISIM_REL_RSUBSET_WBISIM_REL]
383QED
384
385val _ = export_theory ();
386