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