1(* ========================================================================== *)
2(* FILE          : BisimulationUptoScript.sml                                 *)
3(* DESCRIPTION   : Bisimulation up to Strong, Weak (2 versions) and OBS_CONGR *)
4(*                                                                            *)
5(* THESIS        : A Formalization of Unique Solutions of Equations in        *)
6(*                 Process Algebra                                            *)
7(* AUTHOR        : (c) Chun Tian, University of Bologna                       *)
8(* DATE          : 2017                                                       *)
9(* ========================================================================== *)
10
11open HolKernel Parse boolLib bossLib;
12
13open relationTheory CCSLib CCSTheory;
14open StrongEQTheory StrongEQLib StrongLawsTheory;
15open WeakEQTheory WeakEQLib WeakLawsTheory;
16open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory;
17
18val _ = new_theory "BisimulationUpto";
19
20(******************************************************************************)
21(*                                                                            *)
22(*                    1. Bisimulation Upto STRONG_EQUIV                       *)
23(*                                                                            *)
24(******************************************************************************)
25
26(* Define the strong bisimulation relation up to STRONG_EQUIV *)
27val STRONG_BISIM_UPTO = new_definition (
28   "STRONG_BISIM_UPTO",
29  ``STRONG_BISIM_UPTO (Bsm :('a, 'b) simulation) =
30    !E E'.
31        Bsm E E' ==>
32        !u. (!E1. TRANS E u E1 ==>
33                  ?E2. TRANS E' u E2 /\ (STRONG_EQUIV O Bsm O STRONG_EQUIV) E1 E2) /\
34            (!E2. TRANS E' u E2 ==>
35                  ?E1. TRANS E u E1 /\ (STRONG_EQUIV O Bsm O STRONG_EQUIV) E1 E2)``);
36
37val IDENTITY_STRONG_BISIM_UPTO_lemma = store_thm (
38   "IDENTITY_STRONG_BISIM_UPTO_lemma",
39  ``!E. (STRONG_EQUIV O Id O STRONG_EQUIV) E E``,
40    GEN_TAC >> REWRITE_TAC [O_DEF]
41 >> NTAC 2 (Q.EXISTS_TAC `E` >> REWRITE_TAC [STRONG_EQUIV_REFL]));
42
43val IDENTITY_STRONG_BISIM_UPTO = store_thm (
44   "IDENTITY_STRONG_BISIM_UPTO", ``STRONG_BISIM_UPTO Id``,
45    PURE_ONCE_REWRITE_TAC [STRONG_BISIM_UPTO]
46 >> rpt STRIP_TAC (* 2 sub-goals *)
47 >| [ (* goal 1 *)
48      ASSUME_TAC (REWRITE_RULE [ASSUME ``E:('a, 'b) CCS = E'``]
49                               (ASSUME ``TRANS E u E1``)) \\
50      EXISTS_TAC ``E1 :('a, 'b) CCS`` \\
51      ASM_REWRITE_TAC [] \\
52      REWRITE_TAC [IDENTITY_STRONG_BISIM_UPTO_lemma],
53      (* goal 2 *)
54      PURE_ONCE_ASM_REWRITE_TAC [] \\
55      EXISTS_TAC ``E2 :('a, 'b) CCS`` \\
56      ASM_REWRITE_TAC [] \\
57      REWRITE_TAC [IDENTITY_STRONG_BISIM_UPTO_lemma] ]);
58
59val CONVERSE_STRONG_BISIM_UPTO_lemma = Q.prove (
60   `!Wbsm E E'. (STRONG_EQUIV O (inv Wbsm) O STRONG_EQUIV) E E' =
61                (STRONG_EQUIV O Wbsm O STRONG_EQUIV) E' E`,
62    rpt GEN_TAC
63 >> EQ_TAC (* 2 sub-goals here *)
64 >| [ (* goal 1 (of 2) *)
65      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
66      `STRONG_EQUIV y' E` by PROVE_TAC [STRONG_EQUIV_SYM] \\
67      `STRONG_EQUIV E' y` by PROVE_TAC [STRONG_EQUIV_SYM] \\
68      Q.EXISTS_TAC `y'` >> art [] \\
69      Q.EXISTS_TAC `y` >> art [],
70      (* goal 2 (of 2) *)
71      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
72      `STRONG_EQUIV E y` by PROVE_TAC [STRONG_EQUIV_SYM] \\
73      `STRONG_EQUIV y' E'` by PROVE_TAC [STRONG_EQUIV_SYM] \\
74      Q.EXISTS_TAC `y'` >> art [] \\
75      Q.EXISTS_TAC `y` >> art [] ]);
76
77val CONVERSE_STRONG_BISIM_UPTO = store_thm (
78   "CONVERSE_STRONG_BISIM_UPTO",
79  ``!Wbsm. STRONG_BISIM_UPTO Wbsm ==> STRONG_BISIM_UPTO (inv Wbsm)``,
80    GEN_TAC
81 >> PURE_ONCE_REWRITE_TAC [STRONG_BISIM_UPTO]
82 >> REWRITE_TAC [inv_DEF] >> BETA_TAC
83 >> rpt STRIP_TAC
84 >> RES_TAC (* 2 sub-goals here *)
85 >| [ (* goal 1 (of 2) *)
86      Q.EXISTS_TAC `E1'` >> art [] \\
87      REWRITE_TAC [CONVERSE_STRONG_BISIM_UPTO_lemma] >> art [],
88      (* goal 2 (of 2) *)
89      Q.EXISTS_TAC `E2'` >> art [] \\
90      REWRITE_TAC [CONVERSE_STRONG_BISIM_UPTO_lemma] >> art [] ]);
91
92val STRONG_BISIM_UPTO_LEMMA = store_thm (
93   "STRONG_BISIM_UPTO_LEMMA",
94  ``!Bsm. STRONG_BISIM_UPTO Bsm ==> STRONG_BISIM (STRONG_EQUIV O Bsm O STRONG_EQUIV)``,
95    GEN_TAC
96 >> REWRITE_TAC [STRONG_BISIM, O_DEF]
97 >> rpt STRIP_TAC (* 2 sub-goals here *)
98 >| [ (* goal 1 (of 2) *)
99      qpat_x_assum `STRONG_EQUIV E y'`
100        (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\
101      POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `u`)) \\
102      POP_ASSUM K_TAC \\
103      RES_TAC \\
104      qpat_x_assum `STRONG_BISIM_UPTO Bsm`
105        (STRIP_ASSUME_TAC o (REWRITE_RULE [STRONG_BISIM_UPTO])) \\
106      RES_TAC \\
107      NTAC 4 (POP_ASSUM K_TAC) \\
108      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
109      qpat_x_assum `STRONG_EQUIV y E'`
110        (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\
111      POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `u`)) \\
112      POP_ASSUM K_TAC \\
113      POP_ASSUM (STRIP_ASSUME_TAC o
114                 (fn th => MATCH_MP th (ASSUME ``TRANS y u E2'``))) \\
115(***
116                  E    ~   y'    Bsm    y    ~   E'
117                  |       /              \       |
118                  u      u                u      u
119                  |     /                  \     |
120                  E1 ~ E2 ~ y''' Bsm y'' ~ E2' ~ E2''
121 ***)
122      `STRONG_EQUIV E1 y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
123      `STRONG_EQUIV y'' E2''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
124      Q.EXISTS_TAC `E2''` >> art [] \\
125      Q.EXISTS_TAC `y''` >> art [] \\
126      Q.EXISTS_TAC `y'''` >> art [],
127      (* goal 2 (of 2) *)
128      qpat_x_assum `STRONG_EQUIV y E'`
129        (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\
130      POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `u`)) \\
131      qpat_x_assum `!E1. TRANS y u E1 ==> P` K_TAC \\
132      RES_TAC \\
133      qpat_x_assum `STRONG_BISIM_UPTO Bsm`
134        (STRIP_ASSUME_TAC o (REWRITE_RULE [STRONG_BISIM_UPTO])) \\
135      RES_TAC \\
136      NTAC 2 (POP_ASSUM K_TAC) \\
137      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
138      qpat_x_assum `STRONG_EQUIV E y'`
139        (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\
140      POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `u`)) \\
141      qpat_x_assum `!E1. TRANS E u E1 ==> P` K_TAC \\
142      POP_ASSUM (STRIP_ASSUME_TAC o
143                 (fn th => MATCH_MP th (ASSUME ``TRANS y' u E1'``))) \\
144(***
145               E    ~     y'     Bsm    y   ~   E'
146               |         /               \      |
147               u        u                 u     u
148               |       /                   \    |
149               E1'' ~ E1' ~ y''' Bsm y'' ~ E1 ~ E2
150 ***)
151      `STRONG_EQUIV E1'' y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
152      `STRONG_EQUIV y'' E2` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
153      Q.EXISTS_TAC `E1''` >> art [] \\
154      Q.EXISTS_TAC `y''` >> art [] \\
155      Q.EXISTS_TAC `y'''` >> art [] ]);
156
157(* To prove (STRONG_EQUIV P Q), we only have to find a weak bisimulation up to STRONG_EQUIV
158   which contains (P, Q) *)
159val STRONG_BISIM_UPTO_THM = store_thm (
160   "STRONG_BISIM_UPTO_THM",
161  ``!Bsm. STRONG_BISIM_UPTO Bsm ==> Bsm RSUBSET STRONG_EQUIV``,
162    rpt STRIP_TAC
163 >> IMP_RES_TAC STRONG_BISIM_UPTO_LEMMA
164 >> IMP_RES_TAC STRONG_BISIM_SUBSET_STRONG_EQUIV
165 >> Suff `Bsm RSUBSET (STRONG_EQUIV O Bsm O STRONG_EQUIV)`
166 >- ( DISCH_TAC \\
167      Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
168      >- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
169      RW_TAC std_ss [transitive_def] >> RES_TAC )
170 >> KILL_TAC
171 >> REWRITE_TAC [RSUBSET, O_DEF]
172 >> rpt STRIP_TAC
173 >> `STRONG_EQUIV x x /\ STRONG_EQUIV y y` by PROVE_TAC [STRONG_EQUIV_REFL]
174 >> Q.EXISTS_TAC `y` >> art []
175 >> Q.EXISTS_TAC `x` >> art []);
176
177val STRONG_EQUIV_BY_BISIM_UPTO = store_thm (
178   "STRONG_EQUIV_BY_BISIM_UPTO",
179  ``!Bsm P Q. STRONG_BISIM_UPTO Bsm /\ Bsm P Q ==> STRONG_EQUIV P Q``,
180    rpt STRIP_TAC
181 >> irule (REWRITE_RULE [RSUBSET] STRONG_BISIM_UPTO_THM)
182 >> Q.EXISTS_TAC `Bsm` >> art []);
183
184(******************************************************************************)
185(*                                                                            *)
186(*                     2. Bisimulation Upto WEAK_EQUIV                        *)
187(*                                                                            *)
188(******************************************************************************)
189
190(* NOTE: this is actually Proposition 5.12 (section 5.7) in the ERRATA (1990) of [1].
191
192   IMPORTANT: in HOL's big "O", the second argument to composition acts on the "input" first,
193         so we need to revert the order of (?a O Wbsm O ?b) when ?a and ?b are different.
194 *)
195val WEAK_BISIM_UPTO = new_definition (
196   "WEAK_BISIM_UPTO",
197  ``WEAK_BISIM_UPTO (Wbsm: ('a, 'b) simulation) =
198    !E E'. Wbsm E E' ==>
199        (!l.
200          (!E1. TRANS E  (label l) E1 ==>
201                ?E2. WEAK_TRANS E' (label l) E2 /\ (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2) /\
202          (!E2. TRANS E' (label l) E2 ==>
203                ?E1. WEAK_TRANS E  (label l) E1 /\ (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2)) /\
204        (!E1. TRANS E  tau E1 ==>
205              ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2) /\
206        (!E2. TRANS E' tau E2 ==>
207              ?E1. EPS E  E1 /\ (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2)``);
208
209(* Extracted above definition into smaller pieces for easier uses *)
210val WEAK_BISIM_UPTO_TRANS_label = store_thm (
211   "WEAK_BISIM_UPTO_TRANS_label",
212  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
213        !E E'. Wbsm E E' ==>
214               !l E1. TRANS E (label l) E1 ==>
215                      ?E2. WEAK_TRANS E' (label l) E2 /\
216                           (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2``,
217    PROVE_TAC [WEAK_BISIM_UPTO]);
218
219val WEAK_BISIM_UPTO_TRANS_label' = store_thm (
220   "WEAK_BISIM_UPTO_TRANS_label'",
221  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
222        !E E'. Wbsm E E' ==>
223               !l E2. TRANS E' (label l) E2 ==>
224                      ?E1. WEAK_TRANS E  (label l) E1 /\
225                           (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
226    PROVE_TAC [WEAK_BISIM_UPTO]);
227
228val WEAK_BISIM_UPTO_TRANS_tau = store_thm (
229   "WEAK_BISIM_UPTO_TRANS_tau",
230  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
231        !E E'. Wbsm E E' ==>
232               !E1. TRANS E tau E1 ==>
233                    ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2``,
234    PROVE_TAC [WEAK_BISIM_UPTO]);
235
236val WEAK_BISIM_UPTO_TRANS_tau' = store_thm (
237   "WEAK_BISIM_UPTO_TRANS_tau'",
238  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
239        !E E'. Wbsm E E' ==>
240               !E2. TRANS E' tau E2 ==>
241                    ?E1. EPS E  E1 /\ (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
242    PROVE_TAC [WEAK_BISIM_UPTO]);
243
244val IDENTITY_WEAK_BISIM_UPTO_lemma = store_thm (
245   "IDENTITY_WEAK_BISIM_UPTO_lemma",
246  ``!E. (WEAK_EQUIV O Id O STRONG_EQUIV) E E``,
247    GEN_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC
248 >> Q.EXISTS_TAC `E` >> REWRITE_TAC [WEAK_EQUIV_REFL]
249 >> Q.EXISTS_TAC `E` >> REWRITE_TAC [STRONG_EQUIV_REFL]);
250
251val IDENTITY_WEAK_BISIM_UPTO_lemma' = store_thm (
252   "IDENTITY_WEAK_BISIM_UPTO_lemma'",
253  ``!E. (STRONG_EQUIV O Id O WEAK_EQUIV) E E``,
254    GEN_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC
255 >> Q.EXISTS_TAC `E` >> REWRITE_TAC [STRONG_EQUIV_REFL]
256 >> Q.EXISTS_TAC `E` >> REWRITE_TAC [WEAK_EQUIV_REFL]);
257
258val IDENTITY_WEAK_BISIM_UPTO = store_thm (
259   "IDENTITY_WEAK_BISIM_UPTO", ``WEAK_BISIM_UPTO Id``,
260    PURE_ONCE_REWRITE_TAC [WEAK_BISIM_UPTO]
261 >> rpt STRIP_TAC (* 4 sub-goals here *)
262 >| [ (* goal 1 (of 4) *)
263      ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
264                               (ASSUME ``TRANS E (label l) E1``)) \\
265      IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
266      Q.EXISTS_TAC `E1` >> art [] \\
267      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma],
268      (* goal 2 (of 4) *)
269      IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
270      Q.EXISTS_TAC `E2` >> art [] \\
271      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma'],
272      (* goal 3 (of 4) *)
273      ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
274                               (ASSUME ``TRANS E tau E1``)) \\
275      IMP_RES_TAC ONE_TAU \\
276      Q.EXISTS_TAC `E1` >> art [] \\
277      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma],
278      (* goal 4 (of 4) *)
279      IMP_RES_TAC ONE_TAU \\
280      Q.EXISTS_TAC `E2` >> art [] \\
281      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma'] ]);
282
283val CONVERSE_WEAK_BISIM_UPTO_lemma = store_thm (
284   "CONVERSE_WEAK_BISIM_UPTO_lemma",
285  ``!Wbsm E E'. (WEAK_EQUIV O (inv Wbsm) O STRONG_EQUIV) E E' =
286                (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E' E``,
287    rpt GEN_TAC
288 >> EQ_TAC (* 2 sub-goals here *)
289 >| [ (* goal 1 (of 2) *)
290      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
291      `STRONG_EQUIV y' E` by PROVE_TAC [STRONG_EQUIV_SYM] \\
292      `WEAK_EQUIV E' y` by PROVE_TAC [WEAK_EQUIV_SYM] \\
293      Q.EXISTS_TAC `y'` >> art [] \\
294      Q.EXISTS_TAC `y` >> art [],
295      (* goal 2 (of 2) *)
296      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
297      `STRONG_EQUIV E y` by PROVE_TAC [STRONG_EQUIV_SYM] \\
298      `WEAK_EQUIV y' E'` by PROVE_TAC [WEAK_EQUIV_SYM] \\
299      Q.EXISTS_TAC `y'` >> art [] \\
300      Q.EXISTS_TAC `y` >> art [] ]);
301
302val CONVERSE_WEAK_BISIM_UPTO_lemma' = store_thm (
303   "CONVERSE_WEAK_BISIM_UPTO_lemma'",
304  ``!Wbsm E E'. (STRONG_EQUIV O (inv Wbsm) O WEAK_EQUIV) E E' =
305                (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E' E``,
306    rpt GEN_TAC
307 >> EQ_TAC (* 2 sub-goals here *)
308 >| [ (* goal 1 (of 2) *)
309      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
310      `STRONG_EQUIV E' y` by PROVE_TAC [STRONG_EQUIV_SYM] \\
311      `WEAK_EQUIV y' E` by PROVE_TAC [WEAK_EQUIV_SYM] \\
312      Q.EXISTS_TAC `y'` >> art [] \\
313      Q.EXISTS_TAC `y` >> art [],
314      (* goal 2 (of 2) *)
315      REWRITE_TAC [O_DEF, inv_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
316      `STRONG_EQUIV y' E'` by PROVE_TAC [STRONG_EQUIV_SYM] \\
317      `WEAK_EQUIV E y` by PROVE_TAC [WEAK_EQUIV_SYM] \\
318      Q.EXISTS_TAC `y'` >> art [] \\
319      Q.EXISTS_TAC `y` >> art [] ]);
320
321val CONVERSE_WEAK_BISIM_UPTO = store_thm (
322   "CONVERSE_WEAK_BISIM_UPTO",
323  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==> WEAK_BISIM_UPTO (inv Wbsm)``,
324    GEN_TAC
325 >> PURE_ONCE_REWRITE_TAC [WEAK_BISIM_UPTO]
326 >> rpt STRIP_TAC
327 >> fs [INVERSE_REL]
328 >> RES_TAC (* 4 sub-goals here *)
329 >| [ (* goal 1 (of 4) *)
330      Q.EXISTS_TAC `E1'` >> art [] \\
331      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma] >> art [],
332      (* goal 2 (of 4) *)
333      Q.EXISTS_TAC `E2'` >> art [] \\
334      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma'] >> art [],
335      (* goal 3 (of 4) *)
336      Q.EXISTS_TAC `E1'` >> art [] \\
337      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma] >> art [],
338      (* goal 4 (of 4) *)
339      Q.EXISTS_TAC `E2'` >> art [] \\
340      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma'] >> art [] ]);
341
342val WEAK_BISIM_UPTO_EPS = store_thm ((* NEW *)
343   "WEAK_BISIM_UPTO_EPS",
344  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
345        !E E'. Wbsm E E' ==>
346               !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2``,
347    rpt STRIP_TAC
348 >> PAT_X_ASSUM ``WEAK_BISIM_UPTO Wbsm`` MP_TAC
349 >> qpat_x_assum `Wbsm E E'` MP_TAC
350 >> POP_ASSUM MP_TAC
351 >> Q.SPEC_TAC (`E1`, `E1`)
352 >> Q.SPEC_TAC (`E`, `E`)
353 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
354 >> rpt STRIP_TAC (* 2 sub-goals here *)
355 >| [ (* goal 1 (of 2) *)
356      Q.EXISTS_TAC `E'` \\
357      RW_TAC std_ss [EPS_REFL] \\
358      REWRITE_TAC [O_DEF] >> BETA_TAC \\
359      Q.EXISTS_TAC `E'` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\
360      Q.EXISTS_TAC `E` >> art [STRONG_EQUIV_REFL],
361      (* goal 2 (of 2) *)
362      RES_TAC \\
363      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
364      STRIP_ASSUME_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR]
365                                          (ASSUME ``STRONG_EQUIV E1 y'``)) \\
366      RES_TAC \\
367      NTAC 2 (POP_ASSUM K_TAC) \\
368      STRIP_ASSUME_TAC (REWRITE_RULE [WEAK_BISIM_UPTO]
369                                     (ASSUME ``WEAK_BISIM_UPTO Wbsm``)) \\
370      POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [`y'`, `y`])) \\
371      RES_TAC \\
372      NTAC 7 (POP_ASSUM K_TAC) \\
373      qpat_x_assum `Wbsm y' y ==> X` K_TAC \\
374      qpat_x_assum `!l E1. TRANS y' (label l) E1 ==> P` K_TAC \\
375      qpat_x_assum `!l E2. TRANS y (label l) E2 ==> P` K_TAC \\
376      IMP_RES_TAC WEAK_EQUIV_EPS \\
377      Q.EXISTS_TAC `E2'''` \\
378      CONJ_TAC >- IMP_RES_TAC EPS_TRANS \\
379      qpat_x_assum `X E2' E2''` MP_TAC \\
380      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
381(* Induct case:
382      E                Wbsm                E'
383                                           ||
384      ...                                 eps
385                                           ||
386      E1   ~    y'     Wbsm      y    =~   E2
387      |        /                 \\        ||
388     tau     tau                 eps      eps
389      |      /                     \\      ||
390      E1' ~ E2' ~ y''' Wbsm y'' =~ E2'' =~ E2'''
391 *)
392      `WEAK_EQUIV y'' E2'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
393      `STRONG_EQUIV E1' y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
394      Q.EXISTS_TAC `y''` >> art [] \\
395      Q.EXISTS_TAC `y'''` >> art [] ]);
396
397val WEAK_BISIM_UPTO_EPS' = store_thm ((* NEW *)
398   "WEAK_BISIM_UPTO_EPS'",
399  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
400        !E E'. Wbsm E E' ==>
401               !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
402    GEN_TAC >> DISCH_TAC
403 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONVERSE_WEAK_BISIM_UPTO))
404 >> IMP_RES_TAC WEAK_BISIM_UPTO_EPS
405 >> POP_ASSUM MP_TAC
406 >> rpt STRIP_TAC
407 >> IMP_RES_TAC (GSYM INVERSE_REL)
408 >> RES_TAC
409 >> Q.EXISTS_TAC `E2'` >> art []
410 >> REWRITE_TAC [GSYM CONVERSE_WEAK_BISIM_UPTO_lemma] >> art []);
411
412(* Proof sketch:
413      E            Wbsm              E'
414      ||                             ||
415      eps                            eps
416      ||                             ||
417      E1' ~ y'     Wbsm     y  =~    E2'    (WEAK_BISIM_UPTO_EPS)
418      |     |               ||       ||
419      |     l               l        ||
420      l     |               ||       l
421      |  ~ E2'' (~ Wbsm =~) E2''' =~ ||
422      E2                             E2'''' (WEAK_BISIM_UPTO_TRANS_label)
423      || ~  y'''   Wbsm     y''   =~ ||
424      eps   ||              ||       eps
425      ||    eps             eps      ||
426      ||    ||              ||       ||
427      E1 ~ E2'5 (~ Wbsm =~) E2'6  =~ E2'7   (WEAK_BISIM_UPTO_EPS)
428 *)
429val WEAK_BISIM_UPTO_WEAK_TRANS_label = store_thm ((* NEW *)
430   "WEAK_BISIM_UPTO_WEAK_TRANS_label",
431  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
432        !E E'. Wbsm E E' ==>
433               !l E1. WEAK_TRANS E (label l) E1 ==>
434                      ?E2. WEAK_TRANS E' (label l) E2 /\
435                           (WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2``,
436    rpt STRIP_TAC
437 >> IMP_RES_TAC WEAK_TRANS
438 >> IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_EPS (* lemma 1 used here *)
439                          (ASSUME ``WEAK_BISIM_UPTO Wbsm``))
440 >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF]))
441 >> IMP_RES_TAC PROPERTY_STAR_LEFT
442 >> IMP_RES_TAC WEAK_BISIM_UPTO_TRANS_label
443 >> POP_ASSUM K_TAC
444 >> IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label
445 >> Know `(WEAK_EQUIV O Wbsm O STRONG_EQUIV) E2 E2''''`
446 >- ( qpat_x_assum `X E2'' E2'''` MP_TAC \\
447      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
448      `STRONG_EQUIV E2 y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
449      `WEAK_EQUIV y'' E2''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
450      Q.EXISTS_TAC `y''` >> art [] \\
451      Q.EXISTS_TAC `y'''` >> art [] )
452 >> DISCH_TAC
453 >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF]))
454 >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS
455                          (ASSUME ``STRONG_EQUIV E2 y'''``))
456 >> IMP_RES_TAC (Q.SPECL [`y'''`, `y''`]
457                         (MATCH_MP WEAK_BISIM_UPTO_EPS (* lemma 1 used here *)
458                                   (ASSUME ``WEAK_BISIM_UPTO Wbsm``)))
459 >> NTAC 3 (POP_ASSUM K_TAC)
460 >> IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS
461                          (ASSUME ``WEAK_EQUIV y'' E2''''``))
462 >> Know `(WEAK_EQUIV O Wbsm O STRONG_EQUIV) E1 E2'''''''`
463 >- ( qpat_x_assum `X E2''''' E2''''''` MP_TAC \\
464      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
465      `STRONG_EQUIV E1 y'''''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
466      `WEAK_EQUIV y'''' E2'''''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
467      Q.EXISTS_TAC `y''''` >> art [] \\
468      Q.EXISTS_TAC `y'''''` >> art [] )
469 >> DISCH_TAC
470 >> Q.EXISTS_TAC `E2'''''''`
471 >> art []
472 >> MATCH_MP_TAC EPS_WEAK_EPS
473 >> take [`E2'`, `E2''''`]
474 >> art []);
475
476val WEAK_BISIM_UPTO_WEAK_TRANS_label' = store_thm ((* NEW *)
477   "WEAK_BISIM_UPTO_WEAK_TRANS_label'",
478  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==>
479        !E E'. Wbsm E E' ==>
480               !l E2. WEAK_TRANS E' (label l) E2 ==>
481                      ?E1. WEAK_TRANS E (label l) E1 /\
482                           (STRONG_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
483    GEN_TAC >> DISCH_TAC
484 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONVERSE_WEAK_BISIM_UPTO))
485 >> IMP_RES_TAC WEAK_BISIM_UPTO_WEAK_TRANS_label
486 >> POP_ASSUM MP_TAC
487 >> rpt STRIP_TAC
488 >> IMP_RES_TAC (GSYM INVERSE_REL)
489 >> RES_TAC
490 >> Q.EXISTS_TAC `E2'` >> art []
491 >> REWRITE_TAC [GSYM CONVERSE_WEAK_BISIM_UPTO_lemma] >> art []);
492
493(* If S is a bisimulation up to WEAK_EQUIV, then (WEAK_EQUIV O S O WEAK_EQUIV) is
494   a weak bisimultion. *)
495val WEAK_BISIM_UPTO_LEMMA = store_thm (
496   "WEAK_BISIM_UPTO_LEMMA",
497  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==> WEAK_BISIM (WEAK_EQUIV O Wbsm O WEAK_EQUIV)``,
498    GEN_TAC
499 >> REWRITE_TAC [WEAK_BISIM, O_DEF]
500 >> rpt STRIP_TAC (* 4 sub-goals here *)
501 >| [ (* goal 1 (of 4) *)
502      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_label (ASSUME ``WEAK_EQUIV E y'``)) \\
503      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_WEAK_TRANS_label
504                            (ASSUME ``WEAK_BISIM_UPTO Wbsm``)) \\
505      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label
506                            (ASSUME ``WEAK_EQUIV y E'``)) \\
507      Q.EXISTS_TAC `E2''` >> art [] \\
508      qpat_x_assum `X E2 E2'` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
509(***
510               E    ~=   y'    Wbsm     y    ~=   E'
511               |        //              \\        ||
512              !l       l                 l        l
513               |      //                  \\      ||
514               E1 ~= E2 ~ y''' Wbsm y'' ~= E2' ~= E2''
515 ***)
516      `WEAK_EQUIV E2 y'''` by PROVE_TAC [STRONG_IMP_WEAK_EQUIV] \\
517      `WEAK_EQUIV E1 y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
518      `WEAK_EQUIV y'' E2''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
519      Q.EXISTS_TAC `y''` >> art [] \\
520      Q.EXISTS_TAC `y'''` >> art [],
521      (* goal 2 (of 4) *)
522      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_label' (ASSUME ``WEAK_EQUIV y E'``)) \\
523      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_WEAK_TRANS_label'
524                            (ASSUME ``WEAK_BISIM_UPTO Wbsm``)) \\
525      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label'
526                            (ASSUME ``WEAK_EQUIV E y'``)) \\
527      Q.EXISTS_TAC `E1''` >> art [] \\
528      qpat_x_assum `X E1' E1` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
529(***
530               E    ~=     y'      Wbsm    y   ~=   E'
531               ||         //               \\       |
532               l         l                  l       l
533               ||       //                   \\     |
534               E1'' ~= E1' ~= y''' Wbsm y'' ~ E1 ~= E2
535 ***)
536      `WEAK_EQUIV E1'' y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
537      `WEAK_EQUIV y'' E1` by PROVE_TAC [STRONG_IMP_WEAK_EQUIV] \\
538      `WEAK_EQUIV y'' E2` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
539      Q.EXISTS_TAC `y''` >> art [] \\
540      Q.EXISTS_TAC `y'''` >> art [],
541      (* goal 3 (of 4) *)
542      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau (ASSUME ``WEAK_EQUIV E y'``)) \\
543      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_EPS (ASSUME ``WEAK_BISIM_UPTO Wbsm``)) \\
544      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS (ASSUME ``WEAK_EQUIV y E'``)) \\
545      Q.EXISTS_TAC `E2''` >> art [] \\
546      qpat_x_assum `X E2 E2'` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
547(***
548               E    ~=   y'    Wbsm     y    ~=   E'
549               |        //              \\        ||
550              tau      eps               eps      eps
551               |      //                  \\      ||
552               E1 ~= E2 ~ y''' Wbsm y'' ~= E2' ~= E2''
553 ***)
554      `WEAK_EQUIV E2 y'''` by PROVE_TAC [STRONG_IMP_WEAK_EQUIV] \\
555      `WEAK_EQUIV E1 y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
556      `WEAK_EQUIV y'' E2''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
557      Q.EXISTS_TAC `y''` >> art [] \\
558      Q.EXISTS_TAC `y'''` >> art [],
559      (* goal 4 (of 4) *)
560      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau' (ASSUME ``WEAK_EQUIV y E'``)) \\
561      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_EPS' (ASSUME ``WEAK_BISIM_UPTO Wbsm``)) \\
562      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS' (ASSUME ``WEAK_EQUIV E y'``)) \\
563      Q.EXISTS_TAC `E1''` >> art [] \\
564      qpat_x_assum `X E1' E1` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
565(***
566               E    ~=     y'      Wbsm    y   ~=   E'
567               ||         //               \\       |
568               eps       eps                eps     tau
569               ||       //                   \\     |
570               E1'' ~= E1' ~= y''' Wbsm y'' ~ E1 ~= E2
571 ***)
572      `WEAK_EQUIV E1'' y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
573      `WEAK_EQUIV y'' E1` by PROVE_TAC [STRONG_IMP_WEAK_EQUIV] \\
574      `WEAK_EQUIV y'' E2` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
575      Q.EXISTS_TAC `y''` >> art [] \\
576      Q.EXISTS_TAC `y'''` >> art [] ]);
577
578(* To prove (WEAK_EQUIV P Q), we only have to find a weak bisimulation up to WEAK_EQUIV
579   which contains (P, Q) *)
580val WEAK_BISIM_UPTO_THM = store_thm (
581   "WEAK_BISIM_UPTO_THM",
582  ``!Wbsm. WEAK_BISIM_UPTO Wbsm ==> Wbsm RSUBSET WEAK_EQUIV``,
583    rpt STRIP_TAC
584 >> IMP_RES_TAC WEAK_BISIM_UPTO_LEMMA
585 >> IMP_RES_TAC WEAK_BISIM_SUBSET_WEAK_EQUIV
586 >> Suff `Wbsm RSUBSET (WEAK_EQUIV O Wbsm O WEAK_EQUIV)`
587 >- ( DISCH_TAC \\
588      Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
589      >- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
590      RW_TAC std_ss [transitive_def] >> RES_TAC )
591 >> KILL_TAC
592 >> REWRITE_TAC [RSUBSET, O_DEF]
593 >> rpt STRIP_TAC
594 >> `WEAK_EQUIV x x /\ WEAK_EQUIV y y` by PROVE_TAC [WEAK_EQUIV_REFL]
595 >> Q.EXISTS_TAC `y` >> art []
596 >> Q.EXISTS_TAC `x` >> art []);
597
598val WEAK_EQUIV_BY_BISIM_UPTO = store_thm (
599   "WEAK_EQUIV_BY_BISIM_UPTO",
600  ``!Bsm P Q. WEAK_BISIM_UPTO Bsm /\ Bsm P Q ==> WEAK_EQUIV P Q``,
601    rpt STRIP_TAC
602 >> irule (REWRITE_RULE [RSUBSET] WEAK_BISIM_UPTO_THM)
603 >> Q.EXISTS_TAC `Bsm` >> art []);
604
605(******************************************************************************)
606(*                                                                            *)
607(*            3. Bisimulation Upto WEAK_EQUIV (double-weak version)           *)
608(*                                                                            *)
609(******************************************************************************)
610
611(* NOTE: the (original) definition in Milner's 1989 book [1] is wrong, this is the
612         corrected Definition 5.8 in the ERRATA (1990) of [1]. *)
613val WEAK_BISIM_UPTO_ALT = new_definition (
614   "WEAK_BISIM_UPTO_ALT",
615  ``WEAK_BISIM_UPTO_ALT (Wbsm: ('a, 'b) simulation) =
616    !E E'. Wbsm E E' ==>
617        (!l.
618          (!E1. WEAK_TRANS E  (label l) E1 ==>
619                ?E2. WEAK_TRANS E' (label l) E2 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2) /\
620          (!E2. WEAK_TRANS E' (label l) E2 ==>
621                ?E1. WEAK_TRANS E  (label l) E1 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2)) /\
622        (!E1. WEAK_TRANS E  tau E1 ==>
623              ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2) /\
624        (!E2. WEAK_TRANS E' tau E2 ==>
625              ?E1. EPS E  E1 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2)``);
626
627(* Extracted above definition into smaller pieces for easier uses *)
628val WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label = store_thm (
629   "WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label",
630  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
631        !E E'. Wbsm E E' ==>
632               !l E1. WEAK_TRANS E (label l) E1 ==>
633                      ?E2. WEAK_TRANS E' (label l) E2 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
634    PROVE_TAC [WEAK_BISIM_UPTO_ALT]);
635
636val WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label' = store_thm (
637   "WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label'",
638  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
639        !E E'. Wbsm E E' ==>
640               !l E2. WEAK_TRANS E' (label l) E2 ==>
641                      ?E1. WEAK_TRANS E  (label l) E1 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
642    PROVE_TAC [WEAK_BISIM_UPTO_ALT]);
643
644val WEAK_BISIM_UPTO_ALT_WEAK_TRANS_tau = store_thm (
645   "WEAK_BISIM_UPTO_ALT_WEAK_TRANS_tau",
646  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
647        !E E'. Wbsm E E' ==>
648               !E1. WEAK_TRANS E tau E1 ==>
649                    ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
650    PROVE_TAC [WEAK_BISIM_UPTO_ALT]);
651
652val WEAK_BISIM_UPTO_ALT_WEAK_TRANS_tau' = store_thm (
653   "WEAK_BISIM_UPTO_ALT_WEAK_TRANS_tau'",
654  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
655        !E E'. Wbsm E E' ==>
656               !E2. WEAK_TRANS E' tau E2 ==>
657                    ?E1. EPS E  E1 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
658    PROVE_TAC [WEAK_BISIM_UPTO_ALT]);
659
660val WEAK_BISIM_UPTO_ALT_EPS = store_thm ((* NEW *)
661   "WEAK_BISIM_UPTO_ALT_EPS",
662  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
663        !E E'. Wbsm E E' ==>
664               !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
665    rpt STRIP_TAC
666 >> IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
667 >| [ (* goal 1 (of 2) *)
668      Q.EXISTS_TAC `E'` >> REWRITE_TAC [EPS_REFL] \\
669      REWRITE_TAC [O_DEF] >> BETA_TAC \\
670      Q.EXISTS_TAC `E'` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\
671      Q.EXISTS_TAC `E` >> art [WEAK_EQUIV_REFL],
672      (* goal 2 (of 2) *)
673      PROVE_TAC [WEAK_BISIM_UPTO_ALT] ]);
674
675val WEAK_BISIM_UPTO_ALT_EPS' = store_thm ((* NEW *)
676   "WEAK_BISIM_UPTO_ALT_EPS'",
677  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==>
678        !E E'. Wbsm E E' ==>
679               !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ (WEAK_EQUIV O Wbsm O WEAK_EQUIV) E1 E2``,
680    rpt STRIP_TAC
681 >> IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *)
682 >| [ (* goal 1 (of 2) *)
683      Q.EXISTS_TAC `E` >> REWRITE_TAC [EPS_REFL] \\
684      REWRITE_TAC [O_DEF] >> BETA_TAC \\
685      Q.EXISTS_TAC `E'` >> art [WEAK_EQUIV_REFL] \\
686      Q.EXISTS_TAC `E` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\
687      PROVE_TAC [],
688      (* goal 2 (of 2) *)
689      PROVE_TAC [WEAK_BISIM_UPTO_ALT] ]);
690
691(* If S is a bisimulation up to WEAK_EQUIV, then (WEAK_EQUIV O S O WEAK_EQUIV) is
692   a weak bisimultion. *)
693val WEAK_BISIM_UPTO_ALT_LEMMA = store_thm (
694   "WEAK_BISIM_UPTO_ALT_LEMMA",
695  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==> WEAK_BISIM (WEAK_EQUIV O Wbsm O WEAK_EQUIV)``,
696    GEN_TAC
697 >> REWRITE_TAC [WEAK_BISIM, O_DEF]
698 >> rpt STRIP_TAC (* 4 sub-goals here *)
699 >| [ (* goal 1 (of 4) *)
700      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_label (ASSUME ``WEAK_EQUIV E y'``)) \\
701      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label
702                            (ASSUME ``WEAK_BISIM_UPTO_ALT Wbsm``)) \\
703      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label
704                            (ASSUME ``WEAK_EQUIV y E'``)) \\
705      Q.EXISTS_TAC `E2''` >> art [] \\
706      qpat_x_assum `X E2 E2'` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
707(***
708               E    ~=   y'     Wbsm     y    ~=   E'
709               |        //               \\        ||
710              !l       l                  l        l
711               |      //                   \\      ||
712               E1 ~= E2 ~~ y''' Wbsm y'' ~= E2' ~= E2''
713 ***)
714      `WEAK_EQUIV E1 y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
715      `WEAK_EQUIV y'' E2''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
716      Q.EXISTS_TAC `y''` >> art [] \\
717      Q.EXISTS_TAC `y'''` >> art [],
718      (* goal 2 (of 4) *)
719      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_label' (ASSUME ``WEAK_EQUIV y E'``)) \\
720      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_ALT_WEAK_TRANS_label'
721                            (ASSUME ``WEAK_BISIM_UPTO_ALT Wbsm``)) \\
722      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label'
723                            (ASSUME ``WEAK_EQUIV E y'``)) \\
724      Q.EXISTS_TAC `E1''` >> art [] \\
725      qpat_x_assum `X E1' E1` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
726(***
727               E    ~=     y'      Wbsm    y   ~=   E'
728               ||         //               \\       |
729               l         l                  l       l
730               ||       //                   \\     |
731               E1'' ~= E1' ~= y''' Wbsm y'' ~ E1 ~= E2
732 ***)
733      `WEAK_EQUIV E1'' y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
734      `WEAK_EQUIV y'' E2` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
735      Q.EXISTS_TAC `y''` >> art [] \\
736      Q.EXISTS_TAC `y'''` >> art [],
737      (* goal 3 (of 4) *)
738      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau (ASSUME ``WEAK_EQUIV E y'``)) \\
739      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_ALT_EPS (ASSUME ``WEAK_BISIM_UPTO_ALT Wbsm``)) \\
740      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS (ASSUME ``WEAK_EQUIV y E'``)) \\
741      Q.EXISTS_TAC `E2''` >> art [] \\
742      qpat_x_assum `X E2 E2'` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
743(***
744               E    ~=   y'    Wbsm     y    ~=   E'
745               |        //              \\        ||
746              tau      eps               eps      eps
747               |      //                  \\      ||
748               E1 ~= E2 ~ y''' Wbsm y'' ~= E2' ~= E2''
749 ***)
750      `WEAK_EQUIV E1 y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
751      `WEAK_EQUIV y'' E2''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
752      Q.EXISTS_TAC `y''` >> art [] \\
753      Q.EXISTS_TAC `y'''` >> art [],
754      (* goal 4 (of 4) *)
755      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau' (ASSUME ``WEAK_EQUIV y E'``)) \\
756      IMP_RES_TAC (MATCH_MP WEAK_BISIM_UPTO_ALT_EPS' (ASSUME ``WEAK_BISIM_UPTO_ALT Wbsm``)) \\
757      IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS' (ASSUME ``WEAK_EQUIV E y'``)) \\
758      Q.EXISTS_TAC `E1''` >> art [] \\
759      qpat_x_assum `X E1' E1` (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
760(***
761               E    ~=     y'      Wbsm    y   ~=   E'
762               ||         //               \\       |
763               eps       eps                eps     tau
764               ||       //                   \\     |
765               E1'' ~= E1' ~= y''' Wbsm y'' ~ E1 ~= E2
766 ***)
767      `WEAK_EQUIV E1'' y'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
768      `WEAK_EQUIV y'' E2` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
769      Q.EXISTS_TAC `y''` >> art [] \\
770      Q.EXISTS_TAC `y'''` >> art [] ]);
771
772(* To prove (WEAK_EQUIV P Q), we only have to find a weak bisimulation up to WEAK_EQUIV
773   which contains (P, Q) *)
774val WEAK_BISIM_UPTO_ALT_THM = store_thm (
775   "WEAK_BISIM_UPTO_ALT_THM",
776  ``!Wbsm. WEAK_BISIM_UPTO_ALT Wbsm ==> Wbsm RSUBSET WEAK_EQUIV``,
777    rpt STRIP_TAC
778 >> IMP_RES_TAC WEAK_BISIM_UPTO_ALT_LEMMA
779 >> IMP_RES_TAC WEAK_BISIM_SUBSET_WEAK_EQUIV
780 >> Suff `Wbsm RSUBSET (WEAK_EQUIV O Wbsm O WEAK_EQUIV)`
781 >- ( DISCH_TAC \\
782      Know `transitive ((RSUBSET) :('a, 'b) simulation -> ('a, 'b) simulation -> bool)`
783      >- PROVE_TAC [RSUBSET_WeakOrder, WeakOrder] \\
784      RW_TAC std_ss [transitive_def] >> RES_TAC )
785 >> KILL_TAC
786 >> REWRITE_TAC [RSUBSET, O_DEF]
787 >> rpt STRIP_TAC
788 >> `WEAK_EQUIV x x /\ WEAK_EQUIV y y` by PROVE_TAC [WEAK_EQUIV_REFL]
789 >> Q.EXISTS_TAC `y` >> art []
790 >> Q.EXISTS_TAC `x` >> art []);
791
792val WEAK_EQUIV_BY_BISIM_UPTO_ALT = store_thm (
793   "WEAK_EQUIV_BY_BISIM_UPTO_ALT",
794  ``!Bsm P Q. WEAK_BISIM_UPTO_ALT Bsm /\ Bsm P Q ==> WEAK_EQUIV P Q``,
795    rpt STRIP_TAC
796 >> irule (REWRITE_RULE [RSUBSET] WEAK_BISIM_UPTO_ALT_THM)
797 >> Q.EXISTS_TAC `Bsm` >> art []);
798
799(******************************************************************************)
800(*                                                                            *)
801(*          4. Bisimulation upto WEAK_EQUIV, contained in OBS_CONGR           *)
802(*                                                                            *)
803(******************************************************************************)
804
805(* this work is now useless *)
806val OBS_BISIM_UPTO = new_definition (
807   "OBS_BISIM_UPTO",
808  ``OBS_BISIM_UPTO (Obsm: ('a, 'b) simulation) =
809    !E E'. Obsm E E' ==>
810      !u. (!E1. TRANS E  u E1 ==>
811                ?E2. WEAK_TRANS E' u E2 /\ (WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2) /\
812          (!E2. TRANS E' u E2 ==>
813                ?E1. WEAK_TRANS E  u E1 /\ (STRONG_EQUIV O Obsm O WEAK_EQUIV) E1 E2)``);
814
815val OBS_BISIM_UPTO_TRANS = store_thm (
816   "OBS_BISIM_UPTO_TRANS",
817  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
818        !E E'. Obsm E E' ==>
819               !u E1. TRANS E u E1 ==>
820                      ?E2. WEAK_TRANS E' u E2 /\ (WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2``,
821    PROVE_TAC [OBS_BISIM_UPTO]);
822
823val OBS_BISIM_UPTO_TRANS' = store_thm (
824   "OBS_BISIM_UPTO_TRANS'",
825  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
826        !E E'. Obsm E E' ==>
827               !u E2. TRANS E' u E2 ==>
828                      ?E1. WEAK_TRANS E  u E1 /\ (STRONG_EQUIV O Obsm O WEAK_EQUIV) E1 E2``,
829    PROVE_TAC [OBS_BISIM_UPTO]);
830
831val IDENTITY_OBS_BISIM_UPTO = store_thm (
832   "IDENTITY_OBS_BISIM_UPTO", ``OBS_BISIM_UPTO Id``,
833    PURE_ONCE_REWRITE_TAC [OBS_BISIM_UPTO]
834 >> rpt STRIP_TAC (* 2 sub-goals here *)
835 >| [ (* goal 1 (of 4) *)
836      ASSUME_TAC (REWRITE_RULE [ASSUME ``E :('a, 'b) CCS = E'``]
837                               (ASSUME ``TRANS E u E1``)) \\
838      IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
839      Q.EXISTS_TAC `E1` >> art [] \\
840      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma],
841      (* goal 2 (of 4) *)
842      IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\
843      Q.EXISTS_TAC `E2` >> art [] \\
844      REWRITE_TAC [IDENTITY_WEAK_BISIM_UPTO_lemma'] ]);
845
846val CONVERSE_OBS_BISIM_UPTO = store_thm (
847   "CONVERSE_OBS_BISIM_UPTO",
848  ``!Obsm. OBS_BISIM_UPTO Obsm ==> OBS_BISIM_UPTO (inv Obsm)``,
849    GEN_TAC
850 >> PURE_ONCE_REWRITE_TAC [OBS_BISIM_UPTO]
851 >> rpt STRIP_TAC
852 >> IMP_RES_TAC (GSYM INVERSE_REL)
853 >> RES_TAC (* 2 sub-goals here *)
854 >| [ (* goal 1 (of 2) *)
855      Q.EXISTS_TAC `E1'` >> art [] \\
856      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma] >> art [],
857      (* goal 2 (of 2) *)
858      Q.EXISTS_TAC `E2'` >> art [] \\
859      REWRITE_TAC [CONVERSE_WEAK_BISIM_UPTO_lemma'] >> art [] ]);
860
861val OBS_BISIM_UPTO_EPS = store_thm ((* NEW *)
862   "OBS_BISIM_UPTO_EPS",
863  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
864        !E E'. Obsm E E' ==>
865               !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ (WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2``,
866    rpt STRIP_TAC
867 >> PAT_X_ASSUM ``OBS_BISIM_UPTO Obsm`` MP_TAC
868 >> qpat_x_assum `Obsm E E'` MP_TAC
869 >> POP_ASSUM MP_TAC
870 >> Q.SPEC_TAC (`E1`, `E1`)
871 >> Q.SPEC_TAC (`E`, `E`)
872 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *)
873 >> rpt STRIP_TAC (* 2 sub-goals here *)
874 >| [ (* goal 1 (of 2) *)
875      Q.EXISTS_TAC `E'` \\
876      RW_TAC std_ss [EPS_REFL] \\
877      REWRITE_TAC [O_DEF] >> BETA_TAC \\
878      Q.EXISTS_TAC `E'` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\
879      Q.EXISTS_TAC `E` >> art [STRONG_EQUIV_REFL],
880      (* goal 2 (of 2) *)
881      RES_TAC \\
882      POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF])) \\
883      IMP_RES_TAC PROPERTY_STAR_LEFT \\
884      IMP_RES_TAC OBS_BISIM_UPTO_TRANS \\
885      IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_tau \\
886      Q.EXISTS_TAC `E2'''` \\
887      CONJ_TAC >- IMP_RES_TAC EPS_TRANS \\
888      qpat_x_assum `X E2' E2''` MP_TAC \\
889      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
890(* Induct case:
891      E                Obsm                E'
892                                           ||
893      ...                                 eps
894                                           ||
895      E1   ~    y'     Obsm      y    =~   E2
896      |        /                 \\        ||
897     tau     tau                 tau      eps
898      |      /                     \\      ||
899      E1' ~ E2' ~ y''' Obsm y'' =~ E2'' =~ E2'''
900 *)
901      `WEAK_EQUIV y'' E2'''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
902      `STRONG_EQUIV E1' y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
903      Q.EXISTS_TAC `y''` >> art [] \\
904      Q.EXISTS_TAC `y'''` >> art [] ]);
905
906val OBS_BISIM_UPTO_EPS' = store_thm ((* NEW *)
907   "OBS_BISIM_UPTO_EPS'",
908  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
909        !E E'. Obsm E E' ==>
910               !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ (STRONG_EQUIV O Obsm O WEAK_EQUIV) E1 E2``,
911    GEN_TAC >> DISCH_TAC
912 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONVERSE_OBS_BISIM_UPTO))
913 >> IMP_RES_TAC OBS_BISIM_UPTO_EPS
914 >> POP_ASSUM MP_TAC
915 >> rpt STRIP_TAC
916 >> IMP_RES_TAC INVERSE_REL
917 >> RES_TAC
918 >> Q.EXISTS_TAC `E2'` >> art []
919 >> REWRITE_TAC [GSYM CONVERSE_WEAK_BISIM_UPTO_lemma] >> art []);
920
921(* Proof sketch:
922      E            Obsm              E'
923      ||                             ||
924      eps                            eps
925      ||                             ||
926      E1' ~ y'     Obsm     y  =~    E2'    (WEAK_BISIM_UPTO_EPS)
927      |     |               ||       ||
928      |     l               l        ||
929      l     |               ||       l
930      |  ~ E2'' (~ Obsm =~) E2''' =~ ||
931      E2                             E2'''' (WEAK_BISIM_UPTO_TRANS_label)
932      || ~  y'''   Obsm     y''   =~ ||
933      eps   ||              ||       eps
934      ||    eps             eps      ||
935      ||    ||              ||       ||
936      E1 ~ E2'5 (~ Obsm =~) E2'6  =~ E2'7   (WEAK_BISIM_UPTO_EPS)
937 *)
938val OBS_BISIM_UPTO_WEAK_TRANS_label = store_thm ((* NEW *)
939   "OBS_BISIM_UPTO_WEAK_TRANS_label",
940  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
941        !E E'. Obsm E E' ==>
942               !l E1. WEAK_TRANS E (label l) E1 ==>
943                      ?E2. WEAK_TRANS E' (label l) E2 /\
944                           (WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2``,
945    rpt STRIP_TAC
946 >> IMP_RES_TAC WEAK_TRANS
947 >> IMP_RES_TAC (MATCH_MP OBS_BISIM_UPTO_EPS (* lemma 1 used here *)
948                          (ASSUME ``OBS_BISIM_UPTO Obsm``))
949 >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF]))
950 >> IMP_RES_TAC PROPERTY_STAR_LEFT
951 >> IMP_RES_TAC OBS_BISIM_UPTO_TRANS
952 >> POP_ASSUM K_TAC
953 >> IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label
954 >> Know `(WEAK_EQUIV O Obsm O STRONG_EQUIV) E2 E2''''`
955 >- ( qpat_x_assum `X E2'' E2'''` MP_TAC \\
956      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
957      `STRONG_EQUIV E2 y'''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
958      `WEAK_EQUIV y'' E2''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
959      Q.EXISTS_TAC `y''` >> art [] \\
960      Q.EXISTS_TAC `y'''` >> art [] )
961 >> DISCH_TAC
962 >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [O_DEF]))
963 >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS
964                          (ASSUME ``STRONG_EQUIV E2 y'''``))
965 >> IMP_RES_TAC (Q.SPECL [`y'''`, `y''`]
966                         (MATCH_MP OBS_BISIM_UPTO_EPS (* lemma 1 used here *)
967                                   (ASSUME ``OBS_BISIM_UPTO Obsm``)))
968 >> NTAC 3 (POP_ASSUM K_TAC)
969 >> IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS
970                          (ASSUME ``WEAK_EQUIV y'' E2''''``))
971 >> Know `(WEAK_EQUIV O Obsm O STRONG_EQUIV) E1 E2'''''''`
972 >- ( qpat_x_assum `X E2''''' E2''''''` MP_TAC \\
973      REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
974      `STRONG_EQUIV E1 y'''''` by PROVE_TAC [STRONG_EQUIV_TRANS] \\
975      `WEAK_EQUIV y'''' E2'''''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
976      Q.EXISTS_TAC `y''''` >> art [] \\
977      Q.EXISTS_TAC `y'''''` >> art [] )
978 >> DISCH_TAC
979 >> Q.EXISTS_TAC `E2'''''''`
980 >> art []
981 >> MATCH_MP_TAC EPS_WEAK_EPS
982 >> take [`E2'`, `E2''''`]
983 >> art []);
984
985val OBS_BISIM_UPTO_WEAK_TRANS_label' = store_thm ((* NEW *)
986   "OBS_BISIM_UPTO_WEAK_TRANS_label'",
987  ``!Obsm. OBS_BISIM_UPTO Obsm ==>
988        !E E'. Obsm E E' ==>
989               !l E2. WEAK_TRANS E' (label l) E2 ==>
990                      ?E1. WEAK_TRANS E (label l) E1 /\
991                           (STRONG_EQUIV O Obsm O WEAK_EQUIV) E1 E2``,
992    GEN_TAC >> DISCH_TAC
993 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONVERSE_OBS_BISIM_UPTO))
994 >> IMP_RES_TAC OBS_BISIM_UPTO_WEAK_TRANS_label
995 >> POP_ASSUM MP_TAC
996 >> rpt STRIP_TAC
997 >> IMP_RES_TAC INVERSE_REL
998 >> RES_TAC
999 >> Q.EXISTS_TAC `E2'` >> art []
1000 >> REWRITE_TAC [GSYM CONVERSE_WEAK_BISIM_UPTO_lemma] >> art []);
1001
1002(* To prove (OBS_CONGR P Q), we only have to find a `Obs` bisimulation up to WEAK_EQUIV
1003   which contains (P, Q) *)
1004val OBS_BISIM_UPTO_THM = store_thm (
1005   "OBS_BISIM_UPTO_THM",
1006  ``!Obsm. OBS_BISIM_UPTO Obsm ==> Obsm RSUBSET OBS_CONGR``,
1007    REWRITE_TAC [RSUBSET]
1008 >> rpt STRIP_TAC
1009 >> STRIP_ASSUME_TAC (REWRITE_RULE [OBS_BISIM_UPTO] (ASSUME ``OBS_BISIM_UPTO Obsm``))
1010 >> RES_TAC
1011 >> qpat_x_assum `!E E'. Obsm E E' ==> P` K_TAC
1012 >> REWRITE_TAC [OBS_CONGR]
1013 >> rpt STRIP_TAC (* 2 sub-goals here *)
1014 >| [ (* goal 1 (of 2) *)
1015      RES_TAC \\
1016      Q.EXISTS_TAC `E2` >> art [] \\
1017      irule (REWRITE_RULE [RSUBSET] WEAK_BISIM_UPTO_THM) \\
1018      Q.EXISTS_TAC `(WEAK_EQUIV O Obsm O STRONG_EQUIV)` >> art [] \\
1019      REWRITE_TAC [WEAK_BISIM_UPTO] >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1020      [ (* goal 1.1 (of 4) *)
1021        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1022        IMP_RES_TAC PROPERTY_STAR_LEFT \\
1023        qpat_x_assum `Obsm x y` K_TAC \\
1024        IMP_RES_TAC OBS_BISIM_UPTO_TRANS \\
1025        qpat_x_assum `WEAK_TRANS y u E2` K_TAC \\
1026        IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label \\
1027(***
1028        E    ~   y''    Obsm     y'   ~~   E'
1029        |        |               ||        ||
1030        l        l               l         l
1031        |        |               ||        ||
1032       !E1'  ~   E2' (~ Obsm ~~) E2'' ~~  E2'''
1033 ***)
1034        Q.EXISTS_TAC `E2'''` >> art [] \\
1035        NTAC 2 (ONCE_REWRITE_TAC [O_DEF]) \\
1036        Q.EXISTS_TAC `E2''` >> art [] \\
1037        Q.EXISTS_TAC `E2'` >> art [],
1038        (* goal 1.2 (of 4) *)
1039        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1040        IMP_RES_TAC WEAK_EQUIV_TRANS_label' \\
1041        qpat_x_assum `Obsm x y` K_TAC \\
1042        IMP_RES_TAC OBS_BISIM_UPTO_WEAK_TRANS_label' \\
1043        IMP_RES_TAC STRONG_EQUIV_WEAK_TRANS' \\
1044(***
1045        E    ~   y''          Obsm         y'   ~~   E'
1046        ||       ||                        ||        |
1047        l        l                         l         l
1048        ||       ||                        ||        |
1049        E1''' ~  E1'' ~ y'''' Obsm y''' ~~ E1'  ~~  !E2'
1050 ***)
1051        Q.EXISTS_TAC `E1'''` >> art [] \\
1052        qpat_x_assum `X E1'' E1'` MP_TAC \\
1053        REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
1054        IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\
1055        `WEAK_EQUIV E1''' y''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1056        `WEAK_EQUIV y''' E2'`  by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1057        Q.EXISTS_TAC `E2'` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1058        Q.EXISTS_TAC `y''''` >> art [] \\
1059        Q.EXISTS_TAC `y'''` >> art [] \\
1060        Q.EXISTS_TAC `y''''` >> art [STRONG_EQUIV_REFL],
1061        (* goal 1.3 (of 4) *)
1062        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1063        IMP_RES_TAC PROPERTY_STAR_LEFT \\
1064        qpat_x_assum `Obsm x y` K_TAC \\
1065        IMP_RES_TAC OBS_BISIM_UPTO_TRANS \\
1066        qpat_x_assum `WEAK_TRANS y u E2` K_TAC \\
1067        IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_tau \\
1068(***
1069        E    ~   y''    Obsm     y'   ~~   E'
1070        |        |               ||        ||
1071        tau     tau              tau       eps
1072        |        |               ||        ||
1073       !E1'  ~   E2' (~ Obsm ~~) E2'' ~~  E2'''
1074 ***)
1075        Q.EXISTS_TAC `E2'''` >> art [] \\
1076        NTAC 2 (ONCE_REWRITE_TAC [O_DEF]) \\
1077        Q.EXISTS_TAC `E2''` >> art [] \\
1078        Q.EXISTS_TAC `E2'` >> art [],
1079        (* goal 1.4 (of 4) *)
1080        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1081        IMP_RES_TAC WEAK_EQUIV_TRANS_tau' \\
1082        qpat_x_assum `Obsm x y` K_TAC \\
1083        IMP_RES_TAC OBS_BISIM_UPTO_EPS' \\
1084        IMP_RES_TAC STRONG_EQUIV_EPS' \\
1085(***
1086        E    ~   y''          Obsm         y'   ~~   E'
1087        ||       ||                        ||        |
1088        eps      eps                       eps      tau
1089        ||       ||                        ||        |
1090        E1''' ~  E1'' ~ y'''' Obsm y''' ~~ E1'  ~~  !E2'
1091 ***)
1092        Q.EXISTS_TAC `E1'''` >> art [] \\
1093        qpat_x_assum `X E1'' E1'` MP_TAC \\
1094        REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
1095        IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\
1096        `WEAK_EQUIV E1''' y''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1097        `WEAK_EQUIV y''' E2'`  by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1098        Q.EXISTS_TAC `E2'` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1099        Q.EXISTS_TAC `y''''` >> art [] \\
1100        Q.EXISTS_TAC `y'''` >> art [] \\
1101        Q.EXISTS_TAC `y''''` >> art [STRONG_EQUIV_REFL] ],
1102      (* goal 2 (of 2) *)
1103      RES_TAC \\
1104      Q.EXISTS_TAC `E1` >> art [] \\
1105      irule (REWRITE_RULE [RSUBSET] WEAK_BISIM_UPTO_THM) \\
1106      Q.EXISTS_TAC `(STRONG_EQUIV O Obsm O WEAK_EQUIV)` >> art [] \\
1107      REWRITE_TAC [WEAK_BISIM_UPTO] >> rpt STRIP_TAC >| (* 4 sub-goals here *)
1108      [ (* goal 2.1 (of 4) *)
1109        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1110        IMP_RES_TAC WEAK_EQUIV_TRANS_label \\
1111        qpat_x_assum `Obsm x y` K_TAC \\
1112        IMP_RES_TAC OBS_BISIM_UPTO_WEAK_TRANS_label \\
1113        qpat_x_assum `WEAK_TRANS x u E1` K_TAC \\
1114        IMP_RES_TAC STRONG_EQUIV_WEAK_TRANS \\
1115(***
1116        E    ~~  y''    Obsm     y'   ~    E'
1117        |        ||              ||        ||
1118        l        l               l         l
1119        |        ||              ||        ||
1120       !E1'  ~~  E2' (~ Obsm ~~) E2'' ~   E2'''
1121 ***)
1122        Q.EXISTS_TAC `E2'''` >> art [] \\
1123        qpat_x_assum `X E2' E2''` MP_TAC \\
1124        REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
1125        IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\
1126        `WEAK_EQUIV E1' y''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1127        `WEAK_EQUIV y''' E2'''`  by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1128        Q.EXISTS_TAC `y'''` >> art [] \\
1129        Q.EXISTS_TAC `E1'` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1130        Q.EXISTS_TAC `y'''` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1131        Q.EXISTS_TAC `y''''` >> art [],
1132        (* goal 2.2 (of 4) *)
1133        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1134        IMP_RES_TAC PROPERTY_STAR_RIGHT \\
1135        qpat_x_assum `Obsm x y` K_TAC \\
1136        IMP_RES_TAC OBS_BISIM_UPTO_TRANS' \\
1137        IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label' \\
1138(***
1139        E    ~~  y''          Obsm         y'   ~   E'
1140        ||       ||                        |        |
1141        l        l                         l        l
1142        ||       ||                        |        |
1143        E1''' ~~ E1'' ~ y'''' Obsm y''' ~~ E1'  ~  !E2'
1144 ***)
1145        Q.EXISTS_TAC `E1'''` >> art [] \\
1146        NTAC 2 (ONCE_REWRITE_TAC [O_DEF]) \\
1147        Q.EXISTS_TAC `E1'` >> art [] \\
1148        Q.EXISTS_TAC `E1''` >> art [],
1149        (* goal 2.3 (of 4) *)
1150        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1151        IMP_RES_TAC WEAK_EQUIV_TRANS_tau \\
1152        qpat_x_assum `Obsm x y` K_TAC \\
1153        IMP_RES_TAC OBS_BISIM_UPTO_EPS \\
1154        qpat_x_assum `WEAK_TRANS x u E1` K_TAC \\
1155        IMP_RES_TAC STRONG_EQUIV_EPS \\
1156(***
1157        E    ~~  y''    Obsm     y'   ~    E'
1158        |        ||              ||        ||
1159       tau       eps            eps        eps
1160        |        ||              ||        ||
1161       !E1'  ~~  E2' (~ Obsm ~~) E2'' ~   E2'''
1162 ***)
1163        Q.EXISTS_TAC `E2'''` >> art [] \\
1164        qpat_x_assum `X E2' E2''` MP_TAC \\
1165        REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\
1166        IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\
1167        `WEAK_EQUIV E1' y''''` by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1168        `WEAK_EQUIV y''' E2'''`  by PROVE_TAC [WEAK_EQUIV_TRANS] \\
1169        Q.EXISTS_TAC `y'''` >> art [] \\
1170        Q.EXISTS_TAC `E1'` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1171        Q.EXISTS_TAC `y'''` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\
1172        Q.EXISTS_TAC `y''''` >> art [],
1173        (* goal 2.4 (of 4) *)
1174        qpat_x_assum `X E E'` (STRIP_ASSUME_TAC o BETA_RULE o (REWRITE_RULE [O_DEF])) \\
1175        IMP_RES_TAC PROPERTY_STAR_RIGHT \\
1176        qpat_x_assum `Obsm x y` K_TAC \\
1177        IMP_RES_TAC OBS_BISIM_UPTO_TRANS' \\
1178        IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_tau' \\
1179(***
1180        E    ~~  y''          Obsm         y'   ~   E'
1181        ||       ||                        |        |
1182        eps      tau                       tau     tau
1183        ||       ||                        |        |
1184        E1''' ~~ E1'' ~ y'''' Obsm y''' ~~ E1'  ~  !E2'
1185 ***)
1186        Q.EXISTS_TAC `E1'''` >> art [] \\
1187        NTAC 2 (ONCE_REWRITE_TAC [O_DEF]) \\
1188        Q.EXISTS_TAC `E1'` >> art [] \\
1189        Q.EXISTS_TAC `E1''` >> art [] ] ]);
1190
1191val OBS_CONGR_BY_BISIM_UPTO = store_thm (
1192   "OBS_CONGR_BY_BISIM_UPTO",
1193  ``!Obsm P Q. OBS_BISIM_UPTO Obsm /\ Obsm P Q ==> OBS_CONGR P Q``,
1194    rpt STRIP_TAC
1195 >> irule (REWRITE_RULE [RSUBSET] OBS_BISIM_UPTO_THM)
1196 >> Q.EXISTS_TAC `Obsm` >> art []);
1197
1198(* Bibliography:
1199 *
1200 * [1] Milner, R.: Communication and concurrency. (1989).
1201.* [2] Gorrieri, R., Versari, C.: Introduction to Concurrency Theory. Springer, Cham (2015).
1202 * [3] Sangiorgi, D.: Introduction to Bisimulation and Coinduction. Cambridge University Press (2011).
1203 * [4] Sangiorgi, D., Rutten, J.: Advanced Topics in Bisimulation and Coinduction.
1204                                  Cambridge University Press (2011).
1205 *)
1206
1207val _ = export_theory ();
1208val _ = html_theory "BisimulationUpto";
1209
1210(* last updated: Aug 5, 2017 *)
1211