1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna, Italy (Author: Chun Tian) 4 * Copyright 2018-2019 Fondazione Bruno Kessler, Italy (Author: Chun Tian) 5 *) 6 7open HolKernel Parse boolLib bossLib; 8 9open pred_setTheory relationTheory bisimulationTheory listTheory IndDefRules; 10open CCSLib CCSTheory StrongEQTheory; 11 12val _ = new_theory "WeakEQ"; 13val _ = temp_loose_equality (); 14 15(******************************************************************************) 16(* *) 17(* Operational definition of obs. equiv. for CCS and related properties *) 18(* *) 19(******************************************************************************) 20 21(* new definition for the epsilon transition relation. *) 22val EPS_defn = ``\E E'. TRANS E tau E'``; 23val EPS_def = Define `EPS = RTC ^EPS_defn`; 24 25val _ = set_mapped_fixity { fixity = Infix (NONASSOC, 450), 26 tok = ("=" ^ (UTF8.chr 0x03B5) ^ "=>"), term_name = "EPS" }; 27val _ = TeX_notation { hol = ("=" ^ (UTF8.chr 0x03B5) ^ "=>"), 28 TeX = ("\\HOLTokenEPS", 1) }; 29 30Theorem EPS_ETS : 31 EPS = ETS TRANS tau 32Proof 33 REWRITE_TAC [ETS_def, EPS_def] 34QED 35 36Theorem ONE_TAU : 37 !E E'. TRANS E tau E' ==> EPS E E' 38Proof 39 RW_TAC std_ss [EPS_ETS] 40 >> MATCH_MP_TAC TS_IMP_ETS >> art [] 41QED 42 43Theorem EPS_REFL : 44 !E. EPS E E 45Proof 46 REWRITE_TAC [EPS_ETS, ETS_REFL] 47QED 48 49local 50 val trans = (REWRITE_RULE [GSYM EPS_def]) o BETA_RULE o (ISPEC EPS_defn); 51in 52 53(* !x y z. EPS x y /\ EPS y z ==> EPS x z 54 *) 55val EPS_TRANS = save_thm ((* NEW *) 56 "EPS_TRANS", trans (REWRITE_RULE [transitive_def] RTC_TRANSITIVE)); 57 58(* !P. 59 (!x. P x x) /\ (!x y z. x --'t-> y /\ P y z ==> P x z) ==> 60 !x y. EPS x y ==> P x y 61 *) 62val EPS_ind = save_thm ((* NEW *) 63 "EPS_ind", trans RTC_INDUCT); 64 65(* !P. 66 (!x. P x x) /\ (!x y z. x --'t-> y /\ EPS y z /\ P y z ==> P x z) ==> 67 !x y. EPS x y ==> P x y 68 *) 69val EPS_strongind = save_thm ((* NEW *) 70 "EPS_strongind", trans RTC_STRONG_INDUCT); 71 72(* !P. 73 (!x. P x x) /\ (!x y z. P x y /\ y --'t-> z ==> P x z) ==> 74 !x y. EPS x y ==> P x y 75 *) 76val EPS_ind_right = save_thm ((* NEW *) 77 "EPS_ind_right", trans RTC_INDUCT_RIGHT1); 78 79(* !P. 80 (!x. P x x) /\ (!x y z. P x y /\ EPS x y /\ y --'t-> z ==> P x z) ==> 81 !x y. EPS x y ==> P x y 82 *) 83val EPS_strongind_right = save_thm ((* NEW *) 84 "EPS_strongind_right", trans RTC_STRONG_INDUCT_RIGHT1); 85 86(* !x y. EPS x y <=> (x = y) \/ ?u. x --'t-> u /\ EPS u y 87 *) 88val EPS_cases1 = save_thm ((* NEW *) 89 "EPS_cases1", trans RTC_CASES1); 90 91(* !x y. EPS x y <=> (x = y) \/ ?u. EPS x u /\ u --'t-> y 92 *) 93val EPS_cases2 = save_thm ((* NEW *) 94 "EPS_cases2", trans RTC_CASES2); 95 96end; (* local *) 97 98(* A slightly different version of EPS induction theorem *) 99val EPS_INDUCT = store_thm ((* NEW *) 100 "EPS_INDUCT", ``!P. (!E E'. TRANS E tau E' ==> P E E') /\ 101 (!E. P E E) /\ 102 (!E E1 E'. P E E1 /\ P E1 E' ==> P E E') ==> 103 !x y. EPS x y ==> P x y``, 104 GEN_TAC >> STRIP_TAC 105 >> HO_MATCH_MP_TAC EPS_ind 106 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 107 >| [ (* goal 1 (of 2) *) 108 ASM_REWRITE_TAC [], 109 (* goal 2 (of 2) *) 110 NTAC 2 RES_TAC]); 111 112val EPS_INDUCT_TAC = RULE_INDUCT_THEN EPS_INDUCT ASSUME_TAC ASSUME_TAC; 113 114(* This cases theorem is not the same with any theorem in relationTheory *) 115val EPS_cases = store_thm ((* NEW *) 116 "EPS_cases", 117 ``!E E'. EPS E E' = TRANS E tau E' \/ (E = E') \/ ?E1. EPS E E1 /\ EPS E1 E'``, 118 REPEAT GEN_TAC 119 >> EQ_TAC (* 2 sub-goals here *) 120 >| [ (* goal 1 (of 2) *) 121 Q.SPEC_TAC (`E'`, `E'`) \\ 122 Q.SPEC_TAC (`E`, `E`) \\ 123 HO_MATCH_MP_TAC EPS_strongind (* must be strong *) \\ 124 REPEAT STRIP_TAC >- RW_TAC std_ss [] \\ (* 4 sub-goals here, first is easy *) 125 NTAC 2 DISJ2_TAC \\ (* then the rest 3 goals share the same tacticals *) 126 Q.EXISTS_TAC `E'` \\ 127 IMP_RES_TAC ONE_TAU \\ 128 ASM_REWRITE_TAC [], 129 (* goal 2 (of 2) *) 130 REPEAT STRIP_TAC >| (* 3 sub-goals here *) 131 [ IMP_RES_TAC ONE_TAU, 132 ASM_REWRITE_TAC [EPS_REFL], 133 IMP_RES_TAC EPS_TRANS ] ]); 134 135(******************************************************************************) 136(* *) 137(* Weak transition *) 138(* *) 139(******************************************************************************) 140 141(* Define the weak transition relation (double arrow transition). *) 142val WEAK_TRANS = new_definition ("WEAK_TRANS", 143 ``WEAK_TRANS E u E' = ?E1 E2. EPS E E1 /\ TRANS E1 u E2 /\ EPS E2 E'``); 144 145val _ = 146 add_rule { term_name = "WEAK_TRANS", fixity = Infix (NONASSOC, 450), 147 pp_elements = [ BreakSpace(1,0), TOK "==", HardSpace 0, TM, HardSpace 0, 148 TOK "=>", BreakSpace(1,0) ], 149 paren_style = OnlyIfNecessary, 150 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)) }; 151 152val _ = TeX_notation { hol = "==", TeX = ("\\HOLTokenWeakTransBegin", 1) }; 153val _ = TeX_notation { hol = "=>", TeX = ("\\HOLTokenWeakTransEnd", 1) }; 154 155Theorem WEAK_TRANS_WTS : 156 WEAK_TRANS = WTS TRANS tau 157Proof 158 ASM_SIMP_TAC std_ss [WTS_def, WEAK_TRANS, FUN_EQ_THM, EPS_ETS] 159QED 160 161(* A transition is a particular weak transition. *) 162Theorem TRANS_IMP_WEAK_TRANS : 163 !E u E'. TRANS E u E' ==> WEAK_TRANS E u E' 164Proof 165 RW_TAC std_ss [WEAK_TRANS_WTS] 166 >> MATCH_MP_TAC TS_IMP_WTS >> art [] 167QED 168 169(* A weak transition on tau implies the epsilon relation. *) 170val WEAK_TRANS_IMP_EPS = store_thm ( 171 "WEAK_TRANS_IMP_EPS", ``!E E'. WEAK_TRANS E tau E' ==> EPS E E'``, 172 PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 173 >> REPEAT STRIP_TAC 174 >> MATCH_MP_TAC EPS_TRANS 175 >> Q.EXISTS_TAC `E1` 176 >> ASM_REWRITE_TAC [] 177 >> MATCH_MP_TAC EPS_TRANS 178 >> Q.EXISTS_TAC `E2` 179 >> ASM_REWRITE_TAC [] 180 >> MATCH_MP_TAC ONE_TAU 181 >> ASM_REWRITE_TAC []); 182 183val TRANS_TAU_IMP_EPS = store_thm ((* NEW *) 184 "TRANS_TAU_IMP_EPS", ``!E E'. TRANS E tau E' ==> EPS E E'``, 185 REPEAT STRIP_TAC 186 >> IMP_RES_TAC TRANS_IMP_WEAK_TRANS 187 >> IMP_RES_TAC WEAK_TRANS_IMP_EPS); 188 189(* A weak transition on tau implies at least one transition on tau *) 190val WEAK_TRANS_TAU_IMP_TRANS_TAU = store_thm ((* NEW *) 191 "WEAK_TRANS_TAU_IMP_TRANS_TAU", 192 ``!E E'. WEAK_TRANS E tau E' ==> ?E1. TRANS E tau E1 /\ EPS E1 E'``, 193 REWRITE_TAC [WEAK_TRANS] 194 >> REPEAT STRIP_TAC 195 >> NTAC 3 (POP_ASSUM MP_TAC) 196 >> Q.SPEC_TAC (`E1`, `E1`) 197 >> Q.SPEC_TAC (`E`, `E`) 198 >> HO_MATCH_MP_TAC EPS_strongind (* must be strong *) 199 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 200 >| [ (* goal 1 (of 2) *) 201 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 202 (* goal 2 (of 2) *) 203 Q.EXISTS_TAC `E''` >> ASM_REWRITE_TAC [] \\ 204 IMP_RES_TAC ONE_TAU \\ 205 IMP_RES_TAC EPS_TRANS ]); 206 207val TAU_PREFIX_EPS = store_thm ((* NEW *) 208 "TAU_PREFIX_EPS", ``!E E'. EPS E E' ==> EPS (prefix tau E) E'``, 209 REPEAT STRIP_TAC 210 >> ONCE_REWRITE_TAC [EPS_cases1] 211 >> DISJ2_TAC 212 >> Q.EXISTS_TAC `E` 213 >> ASM_REWRITE_TAC [PREFIX]); 214 215val TAU_PREFIX_WEAK_TRANS = store_thm ((* NEW *) 216 "TAU_PREFIX_WEAK_TRANS", 217 ``!E u E'. WEAK_TRANS E u E' ==> WEAK_TRANS (prefix tau E) u E'``, 218 REPEAT STRIP_TAC 219 >> Cases_on `u` (* 2 sub-goals here *) 220 >| [ (* goal 1 (of 2) *) 221 IMP_RES_TAC WEAK_TRANS_IMP_EPS \\ 222 REWRITE_TAC [WEAK_TRANS] \\ 223 take [`prefix tau E`, `E`] \\ 224 ASM_REWRITE_TAC [EPS_REFL, PREFIX], 225 (* goal 2 (of 2) *) 226 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 227 REWRITE_TAC [WEAK_TRANS] \\ 228 take [`E1`, `E2`] >> ASM_REWRITE_TAC [] \\ 229 IMP_RES_TAC TAU_PREFIX_EPS ]); 230 231val EPS_WEAK_EPS = store_thm ( 232 "EPS_WEAK_EPS", 233 ``!E E1 u E2 E'. 234 EPS E E1 /\ WEAK_TRANS E1 u E2 /\ EPS E2 E' ==> WEAK_TRANS E u E'``, 235 REPEAT GEN_TAC 236 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 237 >> STRIP_TAC 238 >> Q.EXISTS_TAC `E1'` 239 >> Q.EXISTS_TAC `E2'` 240 >> ASM_REWRITE_TAC 241 [MATCH_MP EPS_TRANS 242 (CONJ (ASSUME ``EPS E E1``) (ASSUME ``EPS E1 E1'``)), 243 MATCH_MP EPS_TRANS 244 (CONJ (ASSUME ``EPS E2' E2``) (ASSUME ``EPS E2 E'``))]); 245 246val EPS_AND_WEAK_TRANS = store_thm ((* NEW *) 247 "EPS_AND_WEAK_TRANS", 248 ``!E E1 u E2. 249 EPS E E1 /\ WEAK_TRANS E1 u E2 ==> WEAK_TRANS E u E2``, 250 REPEAT GEN_TAC 251 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 252 >> STRIP_TAC 253 >> Q.EXISTS_TAC `E1'` 254 >> Q.EXISTS_TAC `E2'` 255 >> ASM_REWRITE_TAC [] 256 >> IMP_RES_TAC EPS_TRANS); 257 258val WEAK_TRANS_AND_EPS = store_thm ((* NEW *) 259 "WEAK_TRANS_AND_EPS", 260 ``!E1 u E2 E'. 261 WEAK_TRANS E1 u E2 /\ EPS E2 E' ==> WEAK_TRANS E1 u E'``, 262 REPEAT GEN_TAC 263 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 264 >> STRIP_TAC 265 >> Q.EXISTS_TAC `E1'` 266 >> Q.EXISTS_TAC `E2'` 267 >> ASM_REWRITE_TAC [] 268 >> IMP_RES_TAC EPS_TRANS); 269 270val TRANS_TAU_AND_WEAK = store_thm ((* NEW *) 271 "TRANS_TAU_AND_WEAK", 272 ``!E E1 u E'. TRANS E tau E1 /\ WEAK_TRANS E1 u E' ==> WEAK_TRANS E u E'``, 273 REPEAT STRIP_TAC 274 >> IMP_RES_TAC TRANS_IMP_WEAK_TRANS 275 >> IMP_RES_TAC WEAK_TRANS_IMP_EPS 276 >> MATCH_MP_TAC EPS_WEAK_EPS 277 >> take [`E1`, `E'`] 278 >> ASM_REWRITE_TAC [EPS_REFL]); 279 280val TRANS_AND_EPS = store_thm ((* NEW *) 281 "TRANS_AND_EPS", ``!E u E1 E'. TRANS E u E1 /\ EPS E1 E' ==> WEAK_TRANS E u E'``, 282 REPEAT STRIP_TAC 283 >> REWRITE_TAC [WEAK_TRANS] 284 >> take [`E`, `E1`] 285 >> ASM_REWRITE_TAC [EPS_REFL]); 286 287val EPS_IMP_WEAK_TRANS = store_thm ( 288 "EPS_IMP_WEAK_TRANS", 289 ``!E E'. EPS E E' ==> (E = E') \/ WEAK_TRANS E tau E'``, 290 REPEAT GEN_TAC 291 >> ONCE_REWRITE_TAC [EPS_cases1] 292 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 293 >| [ (* goal 1 (of 2) *) 294 DISJ1_TAC >> ASM_REWRITE_TAC [], 295 (* goal 2 (of 2) *) 296 DISJ2_TAC \\ 297 REWRITE_TAC [WEAK_TRANS] \\ 298 take [`E`, `u`] \\ 299 ASM_REWRITE_TAC [EPS_REFL] ]); 300 301(* The two possible cases for the 1st step in WEAK_TRANS, 302 NOTE: when (u = tau), after the first step it could be either EPS or WEAK_TRANS *) 303val WEAK_TRANS_cases1 = store_thm ((* NEW *) 304 "WEAK_TRANS_cases1", 305 ``!E u E1. WEAK_TRANS E u E1 ==> (?E'. TRANS E tau E' /\ WEAK_TRANS E' u E1) \/ 306 (?E'. TRANS E u E' /\ EPS E' E1)``, 307 REPEAT STRIP_TAC 308 >> POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) 309 >> PAT_X_ASSUM ``TRANS E1' u E2`` MP_TAC 310 >> PAT_X_ASSUM ``EPS E E1'`` MP_TAC 311 >> Q.SPEC_TAC (`E1'`, `E1'`) 312 >> Q.SPEC_TAC (`E`, `E`) 313 >> HO_MATCH_MP_TAC EPS_strongind (* must be strong *) 314 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 315 >| [ (* goal 1 (of 2) *) 316 DISJ2_TAC \\ 317 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 318 (* goal 2 (of 2) *) 319 DISJ1_TAC \\ 320 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] \\ 321 REWRITE_TAC [WEAK_TRANS] \\ 322 take [`E1'`, `E2`] >> ASM_REWRITE_TAC [] ]); 323 324(* The two possible cases for the 1st step in ``WEAK_TRANS _ (label _) _`` *) 325val WEAK_TRANS_cases2 = store_thm ((* NEW *) 326 "WEAK_TRANS_cases2", 327 ``!E l E1. WEAK_TRANS E (label l) E1 ==> (?E'. TRANS E tau E' /\ WEAK_TRANS E' (label l) E1) \/ 328 (?E'. TRANS E (label l) E' /\ EPS E' E1)``, 329 REPEAT STRIP_TAC 330 >> IMP_RES_TAC WEAK_TRANS_cases1 331 >| [ DISJ1_TAC >> Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [], 332 DISJ2_TAC >> Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] ]); 333 334val WEAK_TRANS_TAU = store_thm ((* NEW *) 335 "WEAK_TRANS_TAU", 336 ``!E E1. WEAK_TRANS E tau E1 = ?E'. TRANS E tau E' /\ EPS E' E1``, 337 REPEAT GEN_TAC 338 >> EQ_TAC (* 2 sub-goals here *) 339 >| [ (* goal 1 (of 2) *) 340 STRIP_TAC \\ 341 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 342 [ (* goal 1.1 (of 2) *) 343 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] \\ 344 MATCH_MP_TAC WEAK_TRANS_IMP_EPS \\ 345 ASM_REWRITE_TAC [], 346 (* goal 1.2 (of 2) *) 347 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] ], 348 (* goal 2 (of 2) *) 349 REPEAT STRIP_TAC \\ 350 REWRITE_TAC [WEAK_TRANS] \\ 351 take [`E`, `E'`] >> ASM_REWRITE_TAC [EPS_REFL] ]); 352 353(* The weak version of RREFIX *) 354val WEAK_PREFIX = store_thm ((* NEW *) 355 "WEAK_PREFIX", ``!E u. WEAK_TRANS (prefix u E) u E``, 356 rpt GEN_TAC 357 >> MATCH_MP_TAC TRANS_IMP_WEAK_TRANS 358 >> REWRITE_TAC [PREFIX]); 359 360(* The weak version of SUM1 *) 361val WEAK_SUM1 = store_thm ((* NEW *) 362 "WEAK_SUM1", ``!E u E1 E'. WEAK_TRANS E u E1 ==> WEAK_TRANS (sum E E') u E1``, 363 REPEAT STRIP_TAC 364 >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *) 365 >| [ (* goal 1 (of 2) *) 366 IMP_RES_TAC SUM1 \\ 367 POP_ASSUM (ASSUME_TAC o (Q.SPEC `E'`)) \\ 368 POP_ASSUM (ASSUME_TAC o (MATCH_MP ONE_TAU)) \\ 369 ASSUME_TAC (Q.SPEC `E1` EPS_REFL) \\ 370 IMP_RES_TAC EPS_WEAK_EPS, 371 (* goal 2 (of 2) *) 372 IMP_RES_TAC SUM1 \\ 373 POP_ASSUM (ASSUME_TAC o (Q.SPEC `E'`)) \\ 374 REWRITE_TAC [WEAK_TRANS] \\ 375 take [`E + E'`, `E''`] \\ 376 ASM_REWRITE_TAC [EPS_REFL] ]); 377 378(* The weak version of SUM2 *) 379val WEAK_SUM2 = store_thm ((* NEW *) 380 "WEAK_SUM2", ``!E u E1 E'. WEAK_TRANS E u E1 ==> WEAK_TRANS (sum E' E) u E1``, 381 REPEAT STRIP_TAC 382 >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *) 383 >| [ (* goal 1 (of 2) *) 384 IMP_RES_TAC SUM2 \\ 385 POP_ASSUM (ASSUME_TAC o (Q.SPEC `E'`)) \\ 386 POP_ASSUM (ASSUME_TAC o (MATCH_MP ONE_TAU)) \\ 387 ASSUME_TAC (Q.SPEC `E1` EPS_REFL) \\ 388 IMP_RES_TAC EPS_WEAK_EPS, 389 (* goal 2 (of 2) *) 390 IMP_RES_TAC SUM2 \\ 391 POP_ASSUM (ASSUME_TAC o (Q.SPEC `E'`)) \\ 392 REWRITE_TAC [WEAK_TRANS] \\ 393 take [`E' + E`, `E''`] \\ 394 ASM_REWRITE_TAC [EPS_REFL] ]); 395 396(******************************************************************************) 397(* *) 398(* Weak bisimulation relation *) 399(* *) 400(******************************************************************************) 401 402val WEAK_BISIM_def = Define 403 `WEAK_BISIM (R :('a, 'b) simulation) = WBISIM TRANS tau R`; 404 405Theorem WEAK_BISIM : 406 WEAK_BISIM (Wbsm: ('a, 'b) simulation) = 407 !E E'. Wbsm E E' ==> 408 (!l. 409 (!E1. TRANS E (label l) E1 ==> 410 (?E2. WEAK_TRANS E' (label l) E2 /\ Wbsm E1 E2)) /\ 411 (!E2. TRANS E' (label l) E2 ==> 412 (?E1. WEAK_TRANS E (label l) E1 /\ Wbsm E1 E2))) /\ 413 (!E1. TRANS E tau E1 ==> (?E2. EPS E' E2 /\ Wbsm E1 E2)) /\ 414 (!E2. TRANS E' tau E2 ==> (?E1. EPS E E1 /\ Wbsm E1 E2)) 415Proof 416 RW_TAC bool_ss [WEAK_BISIM_def, WBISIM_def, SYM EPS_ETS, SYM WEAK_TRANS_WTS] 417 >> EQ_TAC >> RW_TAC std_ss [] 418 >- METIS_TAC [Action_distinct_label] 419 >- METIS_TAC [Action_distinct_label] 420 >- METIS_TAC [] 421 >- METIS_TAC [] 422 >- (Cases_on `l` >> fs [] >> METIS_TAC []) 423 >- (Cases_on `l` >> fs [] >> METIS_TAC []) 424 >- METIS_TAC [] 425 >> METIS_TAC [] 426QED 427 428Theorem IDENTITY_WEAK_BISIM : 429 WEAK_BISIM Id 430Proof 431 REWRITE_TAC [WEAK_BISIM_def, WBISIM_ID] 432QED 433 434Theorem CONVERSE_WEAK_BISIM : 435 !Wbsm. WEAK_BISIM Wbsm ==> WEAK_BISIM (inv Wbsm) 436Proof 437 REWRITE_TAC [WEAK_BISIM_def, WBISIM_INV] 438QED 439 440(******************************************************************************) 441(* *) 442(* Some auxiliary results for proving that the composition of two weak *) 443(* bisimulations is a weak bisimulation. *) 444(* *) 445(******************************************************************************) 446 447(* Different formulation of case 1 in Milner's proof. *) 448val EPS_TRANS_AUX = store_thm ( 449 "EPS_TRANS_AUX", 450 ``!E E1. EPS E E1 ==> 451 !Wbsm E'. WEAK_BISIM Wbsm /\ Wbsm E E' ==> ?E2. EPS E' E2 /\ Wbsm E1 E2``, 452 EPS_INDUCT_TAC (* 3 sub-goals here *) 453 >| [ (* goal 1 (of 3) *) 454 REPEAT STRIP_TAC \\ 455 IMP_RES_TAC 456 (CONJUNCT2 457 (MATCH_MP (EQ_MP (SPEC_ALL WEAK_BISIM) (ASSUME ``WEAK_BISIM Wbsm``)) 458 (ASSUME ``(Wbsm: ('a, 'b) simulation) E E''``))) \\ 459 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 460 (* goal 2 (of 3) *) 461 REPEAT STRIP_TAC \\ 462 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [EPS_REFL], 463 (* goal 3 (of 3) *) 464 REPEAT STRIP_TAC \\ 465 STRIP_ASSUME_TAC 466 (MATCH_MP (ASSUME ``!Wbsm E'. WEAK_BISIM Wbsm /\ Wbsm E E' ==> 467 (?E2. EPS E' E2 /\ Wbsm E1 E2)``) 468 (CONJ (ASSUME ``WEAK_BISIM Wbsm``) 469 (ASSUME ``(Wbsm: ('a, 'b) simulation) E E''``))) \\ 470 STRIP_ASSUME_TAC 471 (MATCH_MP (ASSUME ``!Wbsm E''. WEAK_BISIM Wbsm /\ Wbsm E1 E'' ==> 472 (?E2. EPS E'' E2 /\ Wbsm E' E2)``) 473 (CONJ (ASSUME ``WEAK_BISIM Wbsm``) 474 (ASSUME ``(Wbsm: ('a, 'b) simulation) E1 E2``))) \\ 475 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 476 MATCH_MP_TAC EPS_TRANS \\ 477 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ]); 478 479(* Symmetric auxiliary result for EPS. *) 480val INVERSE_REL = store_thm ( 481 "INVERSE_REL", ``!(R: 'a -> 'a -> bool) x y. (inv R) x y = R y x``, 482 rpt STRIP_TAC >> REWRITE_TAC [inv_DEF]); 483 484val EPS_TRANS_AUX_SYM = store_thm ( 485 "EPS_TRANS_AUX_SYM", 486 ``!E' E1. 487 EPS E' E1 ==> 488 !Wbsm E. WEAK_BISIM Wbsm /\ Wbsm E E' ==> (?E2. EPS E E2 /\ Wbsm E2 E1)``, 489 rpt STRIP_TAC 490 >> IMP_RES_TAC (GSYM INVERSE_REL) 491 >> IMP_RES_TAC CONVERSE_WEAK_BISIM 492 >> IMP_RES_TAC 493 (Q.SPEC `inv Wbsm` (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E' E1``))) 494 >> ASSUME_TAC 495 (REWRITE_RULE [INVERSE_REL] 496 (ASSUME ``(inv (Wbsm :('a, 'b) simulation)) E1 E2'``)) 497 >> Q.EXISTS_TAC `E2'` >> art []); 498 499(* Auxiliary result for WEAK_TRANS. *) 500val WEAK_TRANS_AUX = store_thm ( 501 "WEAK_TRANS_AUX", 502 ``!E l E1. WEAK_TRANS E (label l) E1 ==> 503 !Wbsm E'. WEAK_BISIM Wbsm /\ Wbsm E E' ==> 504 (?E2. WEAK_TRANS E' (label l) E2 /\ Wbsm E1 E2)``, 505 REPEAT STRIP_TAC 506 >> STRIP_ASSUME_TAC (REWRITE_RULE [WEAK_TRANS] 507 (ASSUME ``WEAK_TRANS E (label l) E1``)) 508 >> STRIP_ASSUME_TAC 509 (MATCH_MP (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E E1'``)) 510 (CONJ (ASSUME ``WEAK_BISIM Wbsm``) 511 (ASSUME ``(Wbsm: ('a, 'b) simulation) E E'``))) 512 >> IMP_RES_TAC 513 (MATCH_MP (EQ_MP (SPEC_ALL WEAK_BISIM) (ASSUME ``WEAK_BISIM Wbsm``)) 514 (ASSUME ``(Wbsm: ('a, 'b) simulation) E1' E2'``)) 515 >> STRIP_ASSUME_TAC 516 (MATCH_MP (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E2 E1``)) 517 (CONJ (ASSUME ``WEAK_BISIM Wbsm``) 518 (ASSUME ``(Wbsm: ('a, 'b) simulation) E2 E2''``))) 519 >> ASSUME_TAC 520 (MATCH_MP EPS_WEAK_EPS 521 (LIST_CONJ [ASSUME ``EPS E' E2'``, 522 ASSUME ``WEAK_TRANS E2' (label l) E2''``, 523 ASSUME ``EPS E2'' E2'''``])) 524 >> EXISTS_TAC ``E2''' :('a, 'b) CCS`` 525 >> ASM_REWRITE_TAC []); 526 527(* Symmetric auxiliary result for WEAK_TRANS. *) 528val WEAK_TRANS_AUX_SYM = store_thm ( 529 "WEAK_TRANS_AUX_SYM", 530 ``!E' l E1. 531 WEAK_TRANS E' (label l) E1 ==> 532 !Wbsm E. WEAK_BISIM Wbsm /\ Wbsm E E' ==> 533 (?E2. WEAK_TRANS E (label l) E2 /\ Wbsm E2 E1)``, 534 rpt STRIP_TAC 535 >> IMP_RES_TAC (GSYM INVERSE_REL) 536 >> IMP_RES_TAC CONVERSE_WEAK_BISIM 537 >> IMP_RES_TAC 538 (Q.SPEC `inv Wbsm` 539 (MATCH_MP WEAK_TRANS_AUX (ASSUME ``WEAK_TRANS E' (label l) E1``))) 540 >> ASSUME_TAC 541 (REWRITE_RULE [INVERSE_REL] 542 (ASSUME ``(inv (Wbsm: ('a, 'b) simulation)) E1 E2'``)) 543 >> EXISTS_TAC ``E2' :('a, 'b) CCS`` >> art []); 544 545(* The composition of two weak bisimulations is a weak bisimulation. *) 546Theorem COMP_WEAK_BISIM : 547 !Wbsm1 Wbsm2. WEAK_BISIM Wbsm1 /\ WEAK_BISIM Wbsm2 ==> WEAK_BISIM (Wbsm2 O Wbsm1) 548Proof 549 REWRITE_TAC [WEAK_BISIM_def, WBISIM_O] 550QED 551 552(* The union of two weak bisimulations is a weak bisimulation. *) 553Theorem UNION_WEAK_BISIM : 554 !Wbsm1 Wbsm2. WEAK_BISIM Wbsm1 /\ WEAK_BISIM Wbsm2 ==> 555 WEAK_BISIM (Wbsm1 RUNION Wbsm2) 556Proof 557 REWRITE_TAC [WEAK_BISIM_def, WBISIM_RUNION] 558QED 559 560(* Define the weak equivalence relation for CCS processes. 561 562 Obsevations on new definition: 563 1. WEAK_EQUIV_cases ==> WEAK_EQUIV_rules (by EQ_IMP_LR) 564 2. WEAK_EQUIV_cases is the same as WEAK_PROPERTY_STAR 565 3. WEAK_EQUIV_coind is new (the co-inductive principle) 566 *) 567CoInductive WEAK_EQUIV : 568 !(E :('a, 'b) CCS) (E' :('a, 'b) CCS). 569 (!l. 570 (!E1. TRANS E (label l) E1 ==> 571 ?E2. WEAK_TRANS E' (label l) E2 /\ WEAK_EQUIV E1 E2) /\ 572 (!E2. TRANS E' (label l) E2 ==> 573 ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2)) /\ 574 (!E1. TRANS E tau E1 ==> (?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2)) /\ 575 (!E2. TRANS E' tau E2 ==> (?E1. EPS E E1 /\ WEAK_EQUIV E1 E2)) 576 ==> WEAK_EQUIV E E' 577End 578 579val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 580 fixity = Infix (NONASSOC, 450), 581 paren_style = OnlyIfNecessary, 582 pp_elements = [HardSpace 1, TOK (UTF8.chr 0x2248), BreakSpace (1,0)], 583 term_name = "WEAK_EQUIV" }; 584 585val _ = TeX_notation { hol = UTF8.chr 0x2248, 586 TeX = ("\\HOLTokenWeakEQ", 1) }; 587 588(* "Weak bisimilarity is a weak bisimulation" *) 589val WEAK_EQUIV_IS_WEAK_BISIM = store_thm ( 590 "WEAK_EQUIV_IS_WEAK_BISIM", ``WEAK_BISIM WEAK_EQUIV``, 591 PURE_ONCE_REWRITE_TAC [WEAK_BISIM] 592 >> REPEAT GEN_TAC 593 >> DISCH_TAC 594 >> PURE_ONCE_REWRITE_TAC [GSYM WEAK_EQUIV_cases] 595 >> ASM_REWRITE_TAC []); 596 597(* Alternative definition of WEAK_EQUIV, similar with STRONG_EQUIV. *) 598val WEAK_EQUIV = store_thm ((* NEW *) 599 "WEAK_EQUIV", 600 ``!E E'. WEAK_EQUIV E E' = ?Wbsm. Wbsm E E' /\ WEAK_BISIM Wbsm``, 601 REPEAT GEN_TAC 602 >> EQ_TAC (* 2 sub-goals here *) 603 >| [ (* goal 1 (of 2) *) 604 DISCH_TAC \\ 605 EXISTS_TAC ``WEAK_EQUIV`` \\ 606 ASM_REWRITE_TAC [WEAK_EQUIV_IS_WEAK_BISIM], 607 (* goal 2 (of 2) *) 608 Q.SPEC_TAC (`E'`, `E'`) \\ 609 Q.SPEC_TAC (`E`, `E`) \\ 610 HO_MATCH_MP_TAC WEAK_EQUIV_coind \\ (* co-induction used here! *) 611 PROVE_TAC [WEAK_BISIM] ]); 612 613Theorem WEAK_EQUIV_IS_WBISIM_REL : 614 WEAK_EQUIV = WBISIM_REL TRANS tau 615Proof 616 RW_TAC std_ss [FUN_EQ_THM, WBISIM_REL_def, WEAK_EQUIV, WEAK_BISIM_def] 617 >> EQ_TAC >> RW_TAC std_ss [] 618 >| [ Q.EXISTS_TAC `Wbsm` >> art [], 619 Q.EXISTS_TAC `R` >> art [] ] 620QED 621 622Theorem WEAK_EQUIV_equivalence : 623 equivalence WEAK_EQUIV 624Proof 625 REWRITE_TAC [WEAK_EQUIV_IS_WBISIM_REL, WBISIM_REL_IS_EQUIV_REL] 626QED 627 628Theorem WEAK_EQUIV_REFL : 629 !E. WEAK_EQUIV E E 630Proof 631 PROVE_TAC [REWRITE_RULE [equivalence_def, reflexive_def] 632 WEAK_EQUIV_equivalence] 633QED 634 635Theorem WEAK_EQUIV_SYM : 636 !E E'. WEAK_EQUIV E E' ==> WEAK_EQUIV E' E 637Proof 638 PROVE_TAC [REWRITE_RULE [equivalence_def, symmetric_def] 639 WEAK_EQUIV_equivalence] 640QED 641 642Theorem WEAK_EQUIV_TRANS : 643 !E E' E''. WEAK_EQUIV E E' /\ WEAK_EQUIV E' E'' ==> WEAK_EQUIV E E'' 644Proof 645 PROVE_TAC [REWRITE_RULE [equivalence_def, transitive_def] 646 WEAK_EQUIV_equivalence] 647QED 648 649val WEAK_BISIM_SUBSET_WEAK_EQUIV = store_thm ((* NEW *) 650 "WEAK_BISIM_SUBSET_WEAK_EQUIV", 651 ``!Wbsm. WEAK_BISIM Wbsm ==> Wbsm RSUBSET WEAK_EQUIV``, 652 PROVE_TAC [RSUBSET, WEAK_EQUIV]); 653 654val WEAK_EQUIV_SYM' = store_thm ((* NEW *) 655 "WEAK_EQUIV_SYM'", 656 ``!E E'. WEAK_EQUIV E E' <=> WEAK_EQUIV E' E``, 657 REPEAT STRIP_TAC 658 >> EQ_TAC 659 >> REWRITE_TAC [WEAK_EQUIV_SYM]); 660 661(* Syntactic equivalence implies observation equivalence. *) 662val EQUAL_IMP_WEAK_EQUIV = store_thm ( 663 "EQUAL_IMP_WEAK_EQUIV", ``!E E'. (E = E') ==> WEAK_EQUIV E E'``, 664 REPEAT STRIP_TAC 665 >> PURE_ASM_REWRITE_TAC [WEAK_EQUIV_REFL]); 666 667(* Observation equivalence satisfies the property [*] *) 668val WEAK_PROPERTY_STAR = save_thm ((* NEW *) 669 "WEAK_PROPERTY_STAR", WEAK_EQUIV_cases); 670 671(* Half versions of WEAK_PROPERTY_STAR *) 672val WEAK_EQUIV_TRANS_label = store_thm ( 673 "WEAK_EQUIV_TRANS_label", 674 ``!E E'. WEAK_EQUIV E E' ==> 675 !l E1. TRANS E (label l) E1 ==> ?E2. WEAK_TRANS E' (label l) E2 /\ WEAK_EQUIV E1 E2``, 676 PROVE_TAC [WEAK_PROPERTY_STAR]); 677 678val WEAK_EQUIV_TRANS_label' = store_thm ( 679 "WEAK_EQUIV_TRANS_label'", 680 ``!E E'. WEAK_EQUIV E E' ==> 681 !l E2. TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 682 PROVE_TAC [WEAK_PROPERTY_STAR]); 683 684val WEAK_EQUIV_TRANS_tau = store_thm ( 685 "WEAK_EQUIV_TRANS_tau", 686 ``!E E'. WEAK_EQUIV E E' ==> !E1. TRANS E tau E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2``, 687 PROVE_TAC [WEAK_PROPERTY_STAR]); 688 689val WEAK_EQUIV_TRANS_tau' = store_thm ( 690 "WEAK_EQUIV_TRANS_tau'", 691 ``!E E'. WEAK_EQUIV E E' ==> !E2. TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 692 PROVE_TAC [WEAK_PROPERTY_STAR]); 693 694(* Observation equivalence is substitutive under prefix operator. *) 695val WEAK_EQUIV_SUBST_PREFIX = store_thm ( 696 "WEAK_EQUIV_SUBST_PREFIX", 697 ``!E E'. WEAK_EQUIV E E' ==> !u. WEAK_EQUIV (prefix u E) (prefix u E')``, 698 REPEAT GEN_TAC 699 >> PURE_ONCE_REWRITE_TAC [SPECL [``prefix (u :'b Action) E``, 700 ``prefix (u :'b Action) E'``] WEAK_PROPERTY_STAR] 701 >> REPEAT STRIP_TAC (* 4 sub-goals here *) 702 >| [ (* goal 1 (of 4) *) 703 IMP_RES_TAC TRANS_PREFIX \\ 704 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [WEAK_TRANS] \\ 705 EXISTS_TAC ``prefix (u :'b Action) E'`` \\ 706 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [EPS_REFL, PREFIX], 707 (* goal 2 (of 4) *) 708 IMP_RES_TAC TRANS_PREFIX \\ 709 Q.EXISTS_TAC `E` >> ASM_REWRITE_TAC [WEAK_TRANS] \\ 710 EXISTS_TAC ``prefix (u :'b Action) E`` \\ 711 Q.EXISTS_TAC `E` >> ASM_REWRITE_TAC [EPS_REFL, PREFIX], 712 (* goal 3 (of 4) *) 713 IMP_RES_TAC TRANS_PREFIX \\ 714 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [] \\ 715 MATCH_MP_TAC ONE_TAU >> ASM_REWRITE_TAC [PREFIX], 716 (* goal 4 (of 4) *) 717 IMP_RES_TAC TRANS_PREFIX \\ 718 Q.EXISTS_TAC `E` >> ASM_REWRITE_TAC [] \\ 719 MATCH_MP_TAC ONE_TAU >> ASM_REWRITE_TAC [PREFIX] ]); 720 721(* Definition of stable agent (tau-derivative do not exist). *) 722val _ = hide "STABLE"; (* conflicted with sortingTheory *) 723 724val STABLE = new_definition ("STABLE", 725 ``STABLE (E :('a, 'b) CCS) = (!u E'. TRANS E u E' ==> ~(u = tau))``); 726 727(* Alternative definition using P, Q, p, q as process variables *) 728val STABLE' = store_thm ( 729 "STABLE'", ``STABLE p = (!u p'. TRANS p u p' ==> ~(u = tau))``, 730 PROVE_TAC [STABLE]); 731 732val STABLE_NO_TRANS_TAU = store_thm ( 733 "STABLE_NO_TRANS_TAU", ``!E. STABLE E ==> !E'. ~(TRANS E tau E')``, 734 REPEAT GEN_TAC 735 >> REWRITE_TAC [STABLE] 736 >> RW_TAC std_ss []); 737 738(* Every process is either stable or not *) 739val STABLE_cases = store_thm ( 740 "STABLE_cases", ``!E. STABLE E \/ ~(STABLE E)``, 741 PROVE_TAC [STABLE]); 742 743(* Properties of stable agents with respect to the epsilon and weak transition 744 relations. *) 745val EPS_STABLE = store_thm ("EPS_STABLE", 746 ``!E E'. EPS E E' ==> (STABLE E ==> (E' = E))``, 747 EPS_INDUCT_TAC (* 3 sub-goals here *) 748 >| [ (* goal 1 (of 3) *) 749 REWRITE_TAC [STABLE] >> DISCH_TAC \\ 750 CHECK_ASSUME_TAC 751 (REWRITE_RULE [] 752 (MATCH_MP (ASSUME ``!(u: 'b Action) E'. TRANS E u E' ==> ~(u = tau)``) 753 (ASSUME ``TRANS E tau E'``))), 754 (* goal 2 (of 3) *) 755 REWRITE_TAC [], 756 (* goal 3 (of 3) *) 757 DISCH_TAC >> RES_TAC \\ 758 REWRITE_TAC 759 [MATCH_MP (REWRITE_RULE [ASSUME ``E1 = E: ('a, 'b) CCS``] 760 (ASSUME ``STABLE E1 ==> (E' = E1)``)) 761 (ASSUME ``STABLE E``)] ]); 762 763val EPS_STABLE' = store_thm ( 764 "EPS_STABLE'", ``!E E'. EPS E E' /\ STABLE E ==> (E' = E)``, 765 PROVE_TAC [EPS_STABLE]); 766 767val WEAK_TRANS_STABLE = store_thm ( 768 "WEAK_TRANS_STABLE", 769 ``!E l E'. WEAK_TRANS E (label l) E' /\ STABLE E ==> 770 (?E''. TRANS E (label l) E'' /\ EPS E'' E')``, 771 REPEAT GEN_TAC 772 >> REWRITE_TAC [WEAK_TRANS] 773 >> STRIP_TAC 774 >> ASSUME_TAC 775 (MATCH_MP 776 (MATCH_MP EPS_STABLE (ASSUME ``EPS E E1``)) 777 (ASSUME ``STABLE E``)) 778 >> ASSUME_TAC (REWRITE_RULE [ASSUME ``E1 = E: ('a, 'b) CCS``] 779 (ASSUME ``TRANS E1 (label l) E2``)) 780 >> Q.EXISTS_TAC `E2` 781 >> ASM_REWRITE_TAC []); 782 783val STABLE_NO_WEAK_TRANS_TAU = store_thm ( 784 "STABLE_NO_WEAK_TRANS_TAU", 785 ``!E. STABLE E ==> !E'. ~(WEAK_TRANS E tau E')``, 786 REPEAT STRIP_TAC 787 >> PAT_X_ASSUM ``STABLE E`` (ASSUME_TAC o (REWRITE_RULE [STABLE])) 788 >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *) 789 >> PROVE_TAC []); 790 791(* Observation equivalence of stable agents is preserved by binary summation. *) 792val WEAK_EQUIV_PRESD_BY_SUM = store_thm ( 793 "WEAK_EQUIV_PRESD_BY_SUM", 794 ``!E1 E1' E2 E2'. 795 WEAK_EQUIV E1 E1' /\ STABLE E1 /\ STABLE E1' /\ 796 WEAK_EQUIV E2 E2' /\ STABLE E2 /\ STABLE E2' ==> 797 WEAK_EQUIV (sum E1 E2) (sum E1' E2')``, 798 REPEAT GEN_TAC 799 >> PURE_ONCE_REWRITE_TAC [WEAK_PROPERTY_STAR] 800 >> REPEAT STRIP_TAC (* 4 sub-goals here *) 801 >| [ (* goal 1 (of 4) *) 802 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 803 [ (* goal 1.1 (of 2) *) 804 RES_TAC >> Q.EXISTS_TAC `E2''` \\ 805 ASM_REWRITE_TAC [WEAK_TRANS] \\ 806 EXISTS_TAC ``sum E1' E2'`` \\ 807 REWRITE_TAC [EPS_REFL] \\ 808 STRIP_ASSUME_TAC (MATCH_MP WEAK_TRANS_STABLE 809 (CONJ (ASSUME ``WEAK_TRANS E1' (label l) E2''``) 810 (ASSUME ``STABLE E1'``))) \\ 811 Q.EXISTS_TAC `E''` >> ASM_REWRITE_TAC [] \\ 812 MATCH_MP_TAC SUM1 >> ASM_REWRITE_TAC [], 813 (* goal 2 (of 4) *) 814 RES_TAC >> Q.EXISTS_TAC `E2''` \\ 815 ASM_REWRITE_TAC [WEAK_TRANS] \\ 816 EXISTS_TAC ``sum E1' E2'`` \\ 817 REWRITE_TAC [EPS_REFL] \\ 818 STRIP_ASSUME_TAC (MATCH_MP WEAK_TRANS_STABLE 819 (CONJ (ASSUME ``WEAK_TRANS E2' (label l) E2''``) 820 (ASSUME ``STABLE E2'``))) \\ 821 Q.EXISTS_TAC `E''` >> ASM_REWRITE_TAC [] \\ 822 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ], 823 (* goal 2 (of 4) *) 824 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 825 [ (* goal 2.1 (of 2) *) 826 RES_TAC >> Q.EXISTS_TAC `E1''` \\ 827 ASM_REWRITE_TAC [WEAK_TRANS] \\ 828 EXISTS_TAC ``sum E1 E2`` >> REWRITE_TAC [EPS_REFL] \\ 829 STRIP_ASSUME_TAC (MATCH_MP WEAK_TRANS_STABLE 830 (CONJ (ASSUME ``WEAK_TRANS E1 (label l) E1''``) 831 (ASSUME ``STABLE E1``))) \\ 832 Q.EXISTS_TAC `E''` >> ASM_REWRITE_TAC [] \\ 833 MATCH_MP_TAC SUM1 >> ASM_REWRITE_TAC [], 834 (* goal 2.2 (of 2) *) 835 RES_TAC >> Q.EXISTS_TAC `E1''` \\ 836 ASM_REWRITE_TAC [WEAK_TRANS] \\ 837 EXISTS_TAC ``sum E1 E2`` >> REWRITE_TAC [EPS_REFL] \\ 838 STRIP_ASSUME_TAC (MATCH_MP WEAK_TRANS_STABLE 839 (CONJ (ASSUME ``WEAK_TRANS E2 (label l) E1''``) 840 (ASSUME ``STABLE E2``))) \\ 841 Q.EXISTS_TAC `E''` >> ASM_REWRITE_TAC [] \\ 842 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ], 843 (* goal 3 (of 4) *) 844 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 845 [ (* goal 3.1 (of 2) *) 846 CHECK_ASSUME_TAC 847 (REWRITE_RULE [] 848 (MATCH_MP (EQ_MP (Q.SPEC `E1` STABLE) (ASSUME ``STABLE E1``)) 849 (ASSUME ``TRANS E1 tau E1''``))), 850 (* goal 3.2 (of 2) *) 851 CHECK_ASSUME_TAC 852 (REWRITE_RULE [] 853 (MATCH_MP (EQ_MP (Q.SPEC `E2` STABLE) (ASSUME ``STABLE E2``)) 854 (ASSUME ``TRANS E2 tau E1''``))) ], 855 (* goal 4 (of 4) *) 856 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 857 [ (* goal 4.1 (of 2) *) 858 CHECK_ASSUME_TAC 859 (REWRITE_RULE [] 860 (MATCH_MP (EQ_MP (Q.SPEC `E1'` STABLE) (ASSUME ``STABLE E1'``)) 861 (ASSUME ``TRANS E1' tau E2''``))), 862 (* goal 4.2 (of 2) *) 863 CHECK_ASSUME_TAC 864 (REWRITE_RULE [] 865 (MATCH_MP (EQ_MP (Q.SPEC `E2'` STABLE) (ASSUME ``STABLE E2'``)) 866 (ASSUME ``TRANS E2' tau E2''``))) ] ]); 867 868(* Observation equivalence of stable agents is substitutive under binary 869 summation on the right. *) 870val WEAK_EQUIV_SUBST_SUM_R = store_thm ( 871 "WEAK_EQUIV_SUBST_SUM_R", 872 ``!E E'. WEAK_EQUIV E E' /\ STABLE E /\ STABLE E' ==> 873 !E''. WEAK_EQUIV (sum E E'') (sum E' E'')``, 874 REPEAT GEN_TAC 875 >> PURE_ONCE_REWRITE_TAC [WEAK_PROPERTY_STAR] 876 >> REPEAT STRIP_TAC (* 4 sub-goals here *) 877 >| [ (* goal 1 (of 4) *) 878 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 879 [ (* goal 1.1 (of 2) *) 880 RES_TAC >> Q.EXISTS_TAC `E2` \\ 881 ASM_REWRITE_TAC [WEAK_TRANS] \\ 882 EXISTS_TAC ``sum E' E''`` \\ 883 REWRITE_TAC [EPS_REFL] \\ 884 STRIP_ASSUME_TAC 885 (MATCH_MP WEAK_TRANS_STABLE 886 (CONJ (ASSUME ``WEAK_TRANS E' (label l) E2``) 887 (ASSUME ``STABLE E'``))) \\ 888 Q.EXISTS_TAC `E'''` >> ASM_REWRITE_TAC [] \\ 889 MATCH_MP_TAC SUM1 >> ASM_REWRITE_TAC [], 890 (* goal 1.2 (of 2) *) 891 Q.EXISTS_TAC `E1` \\ 892 REWRITE_TAC [WEAK_EQUIV_REFL, WEAK_TRANS] \\ 893 EXISTS_TAC ``sum E' E''`` \\ 894 Q.EXISTS_TAC `E1` \\ 895 REWRITE_TAC [EPS_REFL] \\ 896 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ], 897 (* goal 2 (of 4) *) 898 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 899 [ (* goal 2.1 (of 2) *) 900 RES_TAC >> Q.EXISTS_TAC `E1` \\ 901 ASM_REWRITE_TAC [WEAK_TRANS] \\ 902 EXISTS_TAC ``sum E E''`` \\ 903 REWRITE_TAC [EPS_REFL] \\ 904 STRIP_ASSUME_TAC 905 (MATCH_MP WEAK_TRANS_STABLE 906 (CONJ (ASSUME ``WEAK_TRANS E (label l) E1``) 907 (ASSUME ``STABLE E``))) \\ 908 Q.EXISTS_TAC `E'''` >> ASM_REWRITE_TAC [] \\ 909 MATCH_MP_TAC SUM1 >> ASM_REWRITE_TAC [], 910 (* goal 2.2 (of 2) *) 911 Q.EXISTS_TAC `E2` \\ 912 REWRITE_TAC [WEAK_EQUIV_REFL, WEAK_TRANS] \\ 913 EXISTS_TAC ``sum E E''`` \\ 914 Q.EXISTS_TAC `E2` \\ 915 REWRITE_TAC [EPS_REFL] \\ 916 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ], 917 (* goal 3 (of 4) *) 918 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 919 [ (* goal 3.1 (of 2) *) 920 CHECK_ASSUME_TAC 921 (REWRITE_RULE [] 922 (MATCH_MP (EQ_MP (Q.SPEC `E` STABLE) (ASSUME ``STABLE E``)) 923 (ASSUME ``TRANS E tau E1``))), 924 (* goal 3.2 (of 2) *) 925 Q.EXISTS_TAC `E1` \\ 926 REWRITE_TAC [WEAK_EQUIV_REFL] \\ 927 PURE_ONCE_REWRITE_TAC [EPS_cases] \\ 928 DISJ1_TAC \\ 929 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ], 930 (* goal 4 (of 4) *) 931 IMP_RES_TAC TRANS_SUM >| 932 [ (* goal 4.1 (of 2) *) 933 CHECK_ASSUME_TAC 934 (REWRITE_RULE [] 935 (MATCH_MP (EQ_MP (Q.SPEC `E'` STABLE) (ASSUME ``STABLE E'``)) 936 (ASSUME ``TRANS E' tau E2``))), 937 (* goal 4.2 (of 2) *) 938 Q.EXISTS_TAC `E2` \\ 939 REWRITE_TAC [WEAK_EQUIV_REFL] \\ 940 PURE_ONCE_REWRITE_TAC [EPS_cases] \\ 941 DISJ1_TAC \\ 942 MATCH_MP_TAC SUM2 >> ASM_REWRITE_TAC [] ] ]); 943 944(* Observation equivalence is substitutive under guarded binary summation *) 945val WEAK_EQUIV_PRESD_BY_GUARDED_SUM = store_thm ( 946 "WEAK_EQUIV_PRESD_BY_GUARDED_SUM", 947 ``!E1 E1' E2 E2' a1 a2. 948 WEAK_EQUIV E1 E1' /\ WEAK_EQUIV E2 E2' ==> 949 WEAK_EQUIV (sum (prefix a1 E1) (prefix a2 E2)) 950 (sum (prefix a1 E1') (prefix a2 E2'))``, 951 rpt STRIP_TAC 952 >> ONCE_REWRITE_TAC [WEAK_PROPERTY_STAR] 953 >> rpt STRIP_TAC (* 4 sub-goals here *) 954 >| [ (* goal 1 (of 4) *) 955 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 956 [ (* goal 1.1 (of 2) *) 957 IMP_RES_TAC TRANS_PREFIX \\ 958 FULL_SIMP_TAC std_ss [] \\ 959 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 960 MATCH_MP_TAC WEAK_SUM1 \\ 961 MATCH_MP_TAC TRANS_IMP_WEAK_TRANS \\ 962 REWRITE_TAC [PREFIX], 963 (* goal 1.2 (of 2) *) 964 IMP_RES_TAC TRANS_PREFIX \\ 965 FULL_SIMP_TAC std_ss [] \\ 966 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 967 MATCH_MP_TAC WEAK_SUM2 \\ 968 MATCH_MP_TAC TRANS_IMP_WEAK_TRANS \\ 969 REWRITE_TAC [PREFIX] ], 970 (* goal 2 (of 4) *) 971 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 972 [ (* goal 2.1 (of 2) *) 973 IMP_RES_TAC TRANS_PREFIX \\ 974 FULL_SIMP_TAC std_ss [] \\ 975 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 976 MATCH_MP_TAC WEAK_SUM1 \\ 977 MATCH_MP_TAC TRANS_IMP_WEAK_TRANS \\ 978 REWRITE_TAC [PREFIX], 979 (* goal 2.2 (of 2) *) 980 IMP_RES_TAC TRANS_PREFIX \\ 981 FULL_SIMP_TAC std_ss [] \\ 982 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 983 MATCH_MP_TAC WEAK_SUM2 \\ 984 MATCH_MP_TAC TRANS_IMP_WEAK_TRANS \\ 985 REWRITE_TAC [PREFIX] ], 986 (* goal 3 (of 4) *) 987 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 988 [ (* goal 3.1 (of 2) *) 989 IMP_RES_TAC TRANS_PREFIX \\ 990 qpat_x_assum `tau = a1` (ASSUME_TAC o SYM) \\ 991 FULL_SIMP_TAC std_ss [] \\ 992 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 993 MATCH_MP_TAC ONE_TAU \\ 994 MATCH_MP_TAC SUM1 \\ 995 REWRITE_TAC [PREFIX], 996 (* goal 3.2 (of 2) *) 997 IMP_RES_TAC TRANS_PREFIX \\ 998 qpat_x_assum `tau = a2` (ASSUME_TAC o SYM) \\ 999 FULL_SIMP_TAC std_ss [] \\ 1000 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 1001 MATCH_MP_TAC ONE_TAU \\ 1002 MATCH_MP_TAC SUM2 \\ 1003 REWRITE_TAC [PREFIX] ], 1004 (* goal 4 (of 4) *) 1005 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 1006 [ (* goal 4.1 (of 2) *) 1007 IMP_RES_TAC TRANS_PREFIX \\ 1008 qpat_x_assum `tau = a1` (ASSUME_TAC o SYM) \\ 1009 FULL_SIMP_TAC std_ss [] \\ 1010 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 1011 MATCH_MP_TAC ONE_TAU \\ 1012 MATCH_MP_TAC SUM1 \\ 1013 REWRITE_TAC [PREFIX], 1014 (* goal 3.2 (of 2) *) 1015 IMP_RES_TAC TRANS_PREFIX \\ 1016 qpat_x_assum `tau = a2` (ASSUME_TAC o SYM) \\ 1017 FULL_SIMP_TAC std_ss [] \\ 1018 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 1019 MATCH_MP_TAC ONE_TAU \\ 1020 MATCH_MP_TAC SUM2 \\ 1021 REWRITE_TAC [PREFIX] ] ]); 1022 1023(* The epsilon relation is preserved by the parallel operator. *) 1024val EPS_PAR = store_thm ("EPS_PAR", 1025 ``!E E'. EPS E E' ==> 1026 !E''. EPS (par E E'') (par E' E'') /\ EPS (par E'' E) (par E'' E')``, 1027 EPS_INDUCT_TAC (* 3 sub-goals here *) 1028 >| [ (* goal 1 (of 3) *) 1029 GEN_TAC \\ 1030 CONJ_TAC >| (* 2 sub-goals here *) 1031 [ (* goal 1.1 (of 2) *) 1032 IMP_RES_TAC PAR1 \\ 1033 ASSUME_TAC 1034 (Q.SPEC `E''` 1035 (ASSUME ``!E''. TRANS (par E E'') tau (par E' E'')``)) \\ 1036 IMP_RES_TAC ONE_TAU, 1037 (* goal 1.2 (of 2) *) 1038 IMP_RES_TAC PAR2 \\ 1039 ASSUME_TAC 1040 (Q.SPEC `E''` 1041 (ASSUME ``!E''. TRANS (par E'' E) tau (par E'' E')``)) \\ 1042 IMP_RES_TAC ONE_TAU ], 1043 (* goal 2 (of 3) *) 1044 REWRITE_TAC [EPS_REFL], 1045 (* goal 3 (of 3) *) 1046 GEN_TAC \\ 1047 CONJUNCTS_THEN ASSUME_TAC 1048 (Q.SPEC `E''` 1049 (ASSUME ``!E''. EPS (par E E'') (par E1 E'') /\ 1050 EPS (par E'' E) (par E'' E1)``)) \\ 1051 CONJUNCTS_THEN ASSUME_TAC 1052 (Q.SPEC `E''` 1053 (ASSUME ``!E''. EPS (par E1 E'') (par E' E'') /\ 1054 EPS (par E'' E1) (par E'' E')``)) \\ 1055 IMP_RES_TAC EPS_TRANS \\ 1056 ASM_REWRITE_TAC [] ]); 1057 1058val EPS_PAR_PAR = store_thm ( 1059 "EPS_PAR_PAR", 1060 ``!E1 E2 F1 F2. 1061 EPS E1 E2 /\ EPS F1 F2 ==> EPS (par E1 F1) (par E2 F2)``, 1062 REPEAT STRIP_TAC 1063 >> MATCH_MP_TAC EPS_TRANS 1064 >> EXISTS_TAC ``par E2 F1`` 1065 >> IMP_RES_TAC EPS_PAR 1066 >> ASM_REWRITE_TAC []); 1067 1068(* The relation WEAK_TRANS is preserved by the parallel operator. *) 1069val WEAK_PAR = store_thm ("WEAK_PAR", 1070 ``!E u E'. WEAK_TRANS E u E' ==> 1071 !E''. WEAK_TRANS (par E E'') u (par E' E'') /\ 1072 WEAK_TRANS (par E'' E) u (par E'' E')``, 1073 REPEAT GEN_TAC 1074 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 1075 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1076 >| [ (* goal 1 (of 2) *) 1077 IMP_RES_TAC EPS_PAR \\ 1078 EXISTS_TAC ``par E1 E''`` \\ 1079 EXISTS_TAC ``par E2 E''`` \\ 1080 ASM_REWRITE_TAC [] \\ 1081 MATCH_MP_TAC PAR1 >> ASM_REWRITE_TAC [], 1082 (* goal 2 (of 2) *) 1083 IMP_RES_TAC EPS_PAR \\ 1084 EXISTS_TAC ``par E'' E1`` \\ 1085 EXISTS_TAC ``par E'' E2`` \\ 1086 ASM_REWRITE_TAC [] \\ 1087 MATCH_MP_TAC PAR2 >> ASM_REWRITE_TAC [] ]); 1088 1089(* Observation equivalence is preserved by parallel operator. *) 1090val WEAK_EQUIV_PRESD_BY_PAR = store_thm ( 1091 "WEAK_EQUIV_PRESD_BY_PAR", 1092 ``!E1 E1' E2 E2'. 1093 WEAK_EQUIV E1 E1' /\ WEAK_EQUIV E2 E2' ==> 1094 WEAK_EQUIV (par E1 E2) (par E1' E2')``, 1095 REPEAT STRIP_TAC 1096 >> PURE_ONCE_REWRITE_TAC [WEAK_EQUIV] 1097 >> EXISTS_TAC ``\x y. 1098 (?F1 F1' F2 F2'. 1099 (x = par F1 F2) /\ (y = par F1' F2') /\ 1100 WEAK_EQUIV F1 F1' /\ WEAK_EQUIV F2 F2')`` 1101 >> CONJ_TAC (* 2 sub-goals here *) 1102 >| [ (* goal 1 (of 2) *) 1103 BETA_TAC \\ 1104 take [`E1`, `E1'`, `E2`, `E2'`] >> ASM_REWRITE_TAC [], 1105 (* goal 2 (of 2) *) 1106 PURE_ONCE_REWRITE_TAC [WEAK_BISIM] \\ 1107 BETA_TAC \\ 1108 REPEAT STRIP_TAC >| (* 4 sub-goals here *) 1109 [ (* goal 1 (of 4) *) 1110 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 1111 (ASSUME ``TRANS E (label l) E1''``)) \\ 1112 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1113 [ (* goal 1.1 (of 3) *) 1114 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1115 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1116 EXISTS_TAC ``par E2'' F2'`` \\ 1117 CONJ_TAC >| (* 2 sub-goals here *) 1118 [ (* goal 1.1.1 (of 2) *) 1119 ASM_REWRITE_TAC [] \\ 1120 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 1121 (* goal 1.1.2 (of 2) *) 1122 take [`E1'''`, `E2''`, `F2`, `F2'`] \\ 1123 ASM_REWRITE_TAC [] ], 1124 (* goal 1.2 (of 3) *) 1125 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1126 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1127 EXISTS_TAC ``par F1' E2''`` \\ 1128 CONJ_TAC >| (* 2 sub-goals here *) 1129 [ (* goal 1.2.1 (of 2) *) 1130 ASM_REWRITE_TAC [] \\ 1131 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 1132 (* goal 1.2.2 (of 2) *) 1133 take [`F1`, `F1'`, `E1'''`, `E2''`] \\ 1134 ASM_REWRITE_TAC [] ], 1135 (* goal 1.3 (of 3) *) 1136 IMP_RES_TAC Action_distinct_label ], 1137 (* goal 2 (of 4) *) 1138 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 1139 (ASSUME ``TRANS E' (label l) E2''``)) \\ 1140 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1141 [ (* goal 2.1 (of 3) *) 1142 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1143 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1144 EXISTS_TAC ``par E1''' F2`` \\ 1145 CONJ_TAC >| (* 2 sub-goals here *) 1146 [ (* goal 2.1.1 (of 2) *) 1147 ASM_REWRITE_TAC [] \\ 1148 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 1149 (* goal 2.1.2 (of 2) *) 1150 take [`E1'''`, `E1''`, `F2`, `F2'`] \\ 1151 ASM_REWRITE_TAC [] ], 1152 (* goal 2.2 (of 3) *) 1153 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1154 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1155 EXISTS_TAC ``par F1 E1'''`` \\ 1156 CONJ_TAC >| (* 2 sub-goals here *) 1157 [ (* goal 2.2.1 (of 2) *) 1158 ASM_REWRITE_TAC [] \\ 1159 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 1160 (* goal 2.2.2 (of 2) *) 1161 take [`F1`, `F1'`, `E1'''`, `E1''`] \\ 1162 ASM_REWRITE_TAC [] ], 1163 (* goal 2.3 (of 3) *) 1164 IMP_RES_TAC Action_distinct_label ], 1165 (* goal 3 (of 4) *) 1166 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 1167 (ASSUME ``TRANS E tau E1''``)) \\ 1168 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1169 [ (* goal 3.1 (of 3) *) 1170 IMP_RES_TAC 1171 (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1172 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1173 EXISTS_TAC ``par E2'' F2'`` \\ 1174 CONJ_TAC >| (* 2 sub-goals here *) 1175 [ (* goal 3.1.1 (of 2) *) 1176 ASM_REWRITE_TAC [] \\ 1177 IMP_RES_TAC EPS_PAR \\ ASM_REWRITE_TAC [], 1178 (* goal 3.1.2 (of 2) *) 1179 take [`E1'''`, `E2''`, `F2`, `F2'`] \\ 1180 ASM_REWRITE_TAC [] ], 1181 (* goal 3.2 (of 3) *) 1182 IMP_RES_TAC 1183 (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1184 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1185 EXISTS_TAC ``par F1' E2''`` \\ 1186 CONJ_TAC >| (* 2 sub-goals here *) 1187 [ (* goal 3.2.1 (of 2) *) 1188 ASM_REWRITE_TAC [] \\ 1189 IMP_RES_TAC EPS_PAR >> ASM_REWRITE_TAC [], 1190 (* goal 3.2.2 (of 2) *) 1191 take [`F1`, `F1'`, `E1'''`, `E2''`] \\ 1192 ASM_REWRITE_TAC [] ], 1193 (* goal 3.3 (of 3) *) 1194 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1195 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1196 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1197 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1198 EXISTS_TAC ``par E2''' E2''''`` \\ 1199 CONJ_TAC >| (* 2 sub-goals here *) 1200 [ (* goal 3.3.1 (of 2) *) 1201 ASM_REWRITE_TAC [] \\ 1202 MATCH_MP_TAC EPS_TRANS \\ 1203 STRIP_ASSUME_TAC 1204 (REWRITE_RULE [WEAK_TRANS] 1205 (ASSUME ``WEAK_TRANS F1' (label l) E2'''``)) \\ 1206 STRIP_ASSUME_TAC 1207 (REWRITE_RULE [WEAK_TRANS] 1208 (ASSUME ``WEAK_TRANS F2' (label (COMPL l)) E2''''``)) \\ 1209 EXISTS_TAC ``par E1'''' E1'''''`` \\ 1210 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 1211 (CONJ (ASSUME ``EPS F1' E1''''``) 1212 (ASSUME ``EPS F2' E1'''''``))] \\ 1213 MATCH_MP_TAC EPS_TRANS \\ 1214 EXISTS_TAC ``par E2''''' E2''''''`` \\ 1215 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 1216 (CONJ (ASSUME ``EPS E2''''' E2'''``) 1217 (ASSUME ``EPS E2'''''' E2''''``))] \\ 1218 MATCH_MP_TAC ONE_TAU \\ 1219 MATCH_MP_TAC PAR3 \\ 1220 EXISTS_TAC ``l: 'b Label`` \\ 1221 ASM_REWRITE_TAC [], 1222 (* goal 3.3.2 (of 2) *) 1223 take [`E1'''`, `E2'''`, `E2''`, `E2''''`] \\ 1224 ASM_REWRITE_TAC [] ] ], 1225 (* goal 4 (of 4) *) 1226 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 1227 (ASSUME ``TRANS E' tau E2''``)) \\ 1228 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1229 [ (* goal 4.1 (of 3) *) 1230 IMP_RES_TAC (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1231 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1232 EXISTS_TAC ``par E1''' F2`` \\ 1233 CONJ_TAC >| (* 2 sub-goals here *) 1234 [ (* goal 4.1.1 (of 2) *) 1235 IMP_RES_TAC EPS_PAR >> ASM_REWRITE_TAC [], 1236 (* goal 4.1.2 (of 2) *) 1237 take [`E1'''`, `E1''`, `F2`, `F2'`] \\ 1238 ASM_REWRITE_TAC [] ], 1239 (* goal 4.2 (of 3) *) 1240 IMP_RES_TAC (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1241 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1242 EXISTS_TAC ``par F1 E1'''`` \\ 1243 CONJ_TAC >| (* 2 sub-goals here *) 1244 [ (* goal 4.2.1 (of 2) *) 1245 IMP_RES_TAC EPS_PAR >> ASM_REWRITE_TAC [], 1246 (* goal 4.2.2 (of 2) *) 1247 take [`F1`, `F1'`, `E1'''`, `E1''`] \\ 1248 ASM_REWRITE_TAC [] ], 1249 (* goal 4.3 (of 3) *) 1250 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1251 (ASSUME ``WEAK_EQUIV F1 F1'``))) \\ 1252 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1253 (ASSUME ``WEAK_EQUIV F2 F2'``))) \\ 1254 EXISTS_TAC ``par E1''' E1''''`` \\ 1255 CONJ_TAC >| (* 2 sub-goals here *) 1256 [ (* goal 4.3.1 (of 2) *) 1257 ASM_REWRITE_TAC [] \\ 1258 MATCH_MP_TAC EPS_TRANS \\ 1259 STRIP_ASSUME_TAC 1260 (REWRITE_RULE [WEAK_TRANS] 1261 (ASSUME ``WEAK_TRANS F1 (label l) E1'''``)) \\ 1262 STRIP_ASSUME_TAC 1263 (REWRITE_RULE [WEAK_TRANS] 1264 (ASSUME ``WEAK_TRANS F2 (label (COMPL l)) E1''''``)) \\ 1265 EXISTS_TAC ``par E1''''' E1''''''`` \\ 1266 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 1267 (CONJ (ASSUME ``EPS F1 E1'''''``) 1268 (ASSUME ``EPS F2 E1''''''``))] \\ 1269 MATCH_MP_TAC EPS_TRANS \\ 1270 EXISTS_TAC ``par E2'''' E2'''''`` \\ 1271 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 1272 (CONJ (ASSUME ``EPS E2'''' E1'''``) 1273 (ASSUME ``EPS E2''''' E1''''``))] \\ 1274 MATCH_MP_TAC ONE_TAU \\ 1275 MATCH_MP_TAC PAR3 \\ 1276 EXISTS_TAC ``l: 'b Label`` \\ 1277 ASM_REWRITE_TAC [], 1278 (* goal 4.3.2 (of 2) *) 1279 take [`E1'''`, `E1''`, `E1''''`, `E2'''`] \\ 1280 ASM_REWRITE_TAC [] ] ] ] ]); 1281 1282(* Observation equivalence is substitutive under parallel operator on the right: 1283 !E E'. WEAK_EQUIV E E' ==> !E''. WEAK_EQUIV (E || E'') (E' || E'') 1284 *) 1285val WEAK_EQUIV_SUBST_PAR_R = save_thm ( 1286 "WEAK_EQUIV_SUBST_PAR_R", 1287 Q.GENL [`E`, `E'`] 1288 (DISCH ``WEAK_EQUIV E E'`` 1289 (Q.GEN `E''` 1290 (MATCH_MP WEAK_EQUIV_PRESD_BY_PAR 1291 (CONJ (ASSUME ``WEAK_EQUIV E E'``) 1292 (Q.SPEC `E''` WEAK_EQUIV_REFL)))))); 1293 1294(* Observation equivalence is substitutive under parallel operator on the left:k 1295 !E E'. WEAK_EQUIV E E' ==> !E''. WEAK_EQUIV (E'' || E) (E'' || E') 1296 *) 1297val WEAK_EQUIV_SUBST_PAR_L = save_thm ( 1298 "WEAK_EQUIV_SUBST_PAR_L", 1299 Q.GENL [`E`, `E'`] 1300 (DISCH ``WEAK_EQUIV E E'`` 1301 (Q.GEN `E''` 1302 (MATCH_MP WEAK_EQUIV_PRESD_BY_PAR 1303 (CONJ (Q.SPEC `E''` WEAK_EQUIV_REFL) 1304 (ASSUME ``WEAK_EQUIV E E'``)))))); 1305 1306(* The epsilon relation is preserved by the restriction operator. *) 1307val EPS_RESTR = store_thm ( 1308 "EPS_RESTR", 1309 ``!E E'. EPS E E' ==> !L. EPS (restr L E) (restr L E')``, 1310 EPS_INDUCT_TAC (* 3 sub-goals here *) 1311 >| [ (* goal 1 (of 3) *) 1312 GEN_TAC \\ 1313 IMP_RES_TAC 1314 (REWRITE_RULE [] (Q.SPECL [`E`, `tau`, `E'`] RESTR)) \\ 1315 ASSUME_TAC 1316 (Q.SPEC `L` (ASSUME ``!L :('b Label) set. 1317 TRANS (restr L E) tau (restr L E')``)) \\ 1318 IMP_RES_TAC ONE_TAU, 1319 (* goal 2 (of 3) *) 1320 REWRITE_TAC [EPS_REFL], 1321 (* goal 3 (of 3) *) 1322 GEN_TAC \\ 1323 ASSUME_TAC 1324 (Q.SPEC `L` (ASSUME ``!L :('b Label) set. EPS (restr L E) (restr L E1)``)) \\ 1325 ASSUME_TAC 1326 (Q.SPEC `L` (ASSUME ``!L :('b Label) set. EPS (restr L E1) (restr L E')``)) \\ 1327 IMP_RES_TAC EPS_TRANS ]); 1328 1329(* The relation WEAK_TRANS is preserved by the restriction operator. *) 1330val WEAK_RESTR_label = store_thm ( 1331 "WEAK_RESTR_label", 1332 ``!(l :'b Label) L E E'. 1333 ~(l IN L) /\ ~((COMPL l) IN L) /\ WEAK_TRANS E (label l) E' ==> 1334 WEAK_TRANS (restr L E) (label l) (restr L E')``, 1335 REPEAT GEN_TAC 1336 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 1337 >> STRIP_TAC 1338 >> EXISTS_TAC ``restr (L :'b Label set) E1`` 1339 >> EXISTS_TAC ``restr (L :'b Label set) E2`` 1340 >> IMP_RES_TAC EPS_RESTR 1341 >> ASM_REWRITE_TAC [] 1342 >> MATCH_MP_TAC RESTR 1343 >> EXISTS_TAC ``l: 'b Label`` 1344 >> ASM_REWRITE_TAC []); 1345 1346val WEAK_RESTR_tau = store_thm ( 1347 "WEAK_RESTR_tau", 1348 ``!E E'. WEAK_TRANS E tau E' ==> 1349 !L. WEAK_TRANS (restr L E) tau (restr L E')``, 1350 REPEAT GEN_TAC 1351 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 1352 >> STRIP_TAC 1353 >> GEN_TAC 1354 >> EXISTS_TAC ``restr (L :'b Label set) E1`` 1355 >> EXISTS_TAC ``restr (L :'b Label set) E2`` 1356 >> IMP_RES_TAC EPS_RESTR 1357 >> ASM_REWRITE_TAC [] 1358 >> MATCH_MP_TAC RESTR 1359 >> ASM_REWRITE_TAC []); 1360 1361(* Observation equivalence is substitutive under restriction operator. *) 1362val WEAK_EQUIV_SUBST_RESTR = store_thm ( 1363 "WEAK_EQUIV_SUBST_RESTR", 1364 ``!E E'. WEAK_EQUIV E E' ==> !L. WEAK_EQUIV (restr L E) (restr L E')``, 1365 REPEAT STRIP_TAC 1366 >> PURE_ONCE_REWRITE_TAC [WEAK_EQUIV] 1367 >> EXISTS_TAC ``\x y. ?E1 E2 L'. (x = restr L' E1) /\ (y = restr L' E2) /\ 1368 WEAK_EQUIV E1 E2`` 1369 >> CONJ_TAC (* 2 sub-goals here *) 1370 >| [ (* goal 1 (of 2) *) 1371 BETA_TAC \\ 1372 take [`E`, `E'`, `L`] >> ASM_REWRITE_TAC [], 1373 (* goal 2 (of 2) *) 1374 PURE_ONCE_REWRITE_TAC [WEAK_BISIM] \\ 1375 BETA_TAC \\ 1376 REPEAT STRIP_TAC >| (* 4 sub-goals here *) 1377 [ (* goal 2.1 (of 4) *) 1378 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 1379 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 1380 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1381 [ (* goal 2.1.1 (of 2) *) 1382 IMP_RES_TAC Action_distinct_label, 1383 (* goal 2.1.2 (of 2) *) 1384 IMP_RES_TAC 1385 (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1386 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1387 EXISTS_TAC ``restr (L' :'b Label set) E2'`` \\ 1388 ASM_REWRITE_TAC 1389 [MATCH_MP WEAK_RESTR_label 1390 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 1391 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 1392 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 1393 (ASSUME ``WEAK_TRANS E2 (label l) E2'``)])] \\ 1394 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [] ], 1395 (* goal 2.2 (of 4) *) 1396 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 1397 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 1398 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1399 [ (* goal 2.2.1 (of 2) *) 1400 IMP_RES_TAC Action_distinct_label, 1401 (* goal 2.2.2 (of 2) *) 1402 IMP_RES_TAC 1403 (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1404 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1405 EXISTS_TAC ``restr (L' :'b Label set) E1'`` \\ 1406 ASM_REWRITE_TAC 1407 [MATCH_MP WEAK_RESTR_label 1408 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 1409 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 1410 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 1411 (ASSUME ``WEAK_TRANS E1 (label l) E1'``)])] \\ 1412 take [`E1'`, `E''''`, `L'`] >> ASM_REWRITE_TAC [] ], 1413 (* goal 2.3 (of 4) *) 1414 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 1415 (ASSUME ``TRANS E'' tau E1'``)) \\ 1416 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1417 [ (* goal 2.3.1 (of 2) *) 1418 IMP_RES_TAC 1419 (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1420 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1421 EXISTS_TAC ``restr (L' :'b Label set) E2'`` \\ 1422 IMP_RES_TAC EPS_RESTR >> ASM_REWRITE_TAC [] \\ 1423 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [], 1424 (* goal 2.3.2 (of 2) *) 1425 IMP_RES_TAC Action_distinct ], 1426 (* goal 2.4 (of 4) *) 1427 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 1428 (ASSUME ``TRANS E''' tau E2'``)) \\ 1429 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1430 [ (* goal 2.4.1 (of 2) *) 1431 IMP_RES_TAC 1432 (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1433 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1434 EXISTS_TAC ``restr (L' :'b Label set) E1'`` \\ 1435 IMP_RES_TAC EPS_RESTR >> ASM_REWRITE_TAC [] \\ 1436 take [`E1'`, `E''''`, `L'`] >> ASM_REWRITE_TAC [], 1437 (* goal 2.4.2 (of 2) *) 1438 IMP_RES_TAC Action_distinct ] ] ]); 1439 1440(* The epsilon relation is preserved by the relabelling operator. *) 1441val EPS_RELAB = store_thm ("EPS_RELAB", 1442 ``!E E'. EPS E E' ==> 1443 !labl. EPS (relab E (RELAB labl)) (relab E' (RELAB labl))``, 1444 EPS_INDUCT_TAC (* 3 sub-goals here *) 1445 >| [ (* goal 1 (of 3) *) 1446 GEN_TAC \\ 1447 IMP_RES_TAC 1448 (REWRITE_RULE [relabel_def] 1449 (Q.SPECL [`E`, `tau`, `E'`] RELABELING)) \\ 1450 ASSUME_TAC 1451 (SPEC ``RELAB (labl :('b Label # 'b Label) list)`` 1452 (ASSUME ``!rf :'b Relabeling. 1453 TRANS (relab E rf) tau (relab E' rf)``)) \\ 1454 IMP_RES_TAC ONE_TAU, 1455 (* goal 2 (of 3) *) 1456 REWRITE_TAC [EPS_REFL], 1457 (* goal 3 (of 3) *) 1458 GEN_TAC \\ 1459 PAT_X_ASSUM ``!labl :('b Label # 'b Label) list. 1460 EPS (relab E (RELAB labl)) (relab E1 (RELAB labl))`` 1461 (ASSUME_TAC o (SPEC ``labl :('b Label # 'b Label) list``)) \\ 1462 PAT_X_ASSUM ``!labl :('b Label # 'b Label) list. 1463 EPS (relab E1 (RELAB labl)) (relab E' (RELAB labl))`` 1464 (ASSUME_TAC o (SPEC ``labl :('b Label # 'b Label) list``)) \\ 1465 IMP_RES_TAC EPS_TRANS ]); 1466 1467val EPS_RELAB_rf = store_thm ( 1468 "EPS_RELAB_rf", 1469 ``!E E'. EPS E E' ==> !(rf :'b Relabeling). EPS (relab E rf) (relab E' rf)``, 1470 EPS_INDUCT_TAC (* 3 sub-goals here *) 1471 >| [ (* goal 1 (of 3) *) 1472 GEN_TAC \\ 1473 IMP_RES_TAC 1474 (REWRITE_RULE [relabel_def] 1475 (Q.SPECL [`E`, `tau`, `E'`] RELABELING)) \\ 1476 ASSUME_TAC 1477 (Q.SPEC `rf` 1478 (ASSUME ``!rf :'b Relabeling. 1479 TRANS (relab E rf) tau (relab E' rf)``)) \\ 1480 IMP_RES_TAC ONE_TAU, 1481 (* goal 2 (of 3) *) 1482 REWRITE_TAC [EPS_REFL], 1483 (* goal 3 (of 3) *) 1484 GEN_TAC \\ 1485 PAT_X_ASSUM ``!rf :'b Relabeling. EPS (relab E rf) (relab E1 rf)`` 1486 (ASSUME_TAC o (Q.SPEC `rf`)) \\ 1487 PAT_X_ASSUM ``!rf :'b Relabeling. EPS (relab E1 rf) (relab E' rf)`` 1488 (ASSUME_TAC o (Q.SPEC `rf`)) \\ 1489 IMP_RES_TAC EPS_TRANS ]); 1490 1491(* The relation WEAK_TRANS is preserved by the relabelling operator. *) 1492val WEAK_RELAB = store_thm ("WEAK_RELAB", 1493 ``!E u E'. 1494 WEAK_TRANS E u E' ==> 1495 !(labl :('b Label # 'b Label) list). 1496 WEAK_TRANS (relab E (RELAB labl)) 1497 (relabel (RELAB labl) u) 1498 (relab E' (RELAB labl))``, 1499 REPEAT GEN_TAC 1500 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 1501 >> REPEAT STRIP_TAC 1502 >> IMP_RES_TAC EPS_RELAB 1503 >> EXISTS_TAC ``relab E1 (RELAB labl)`` 1504 >> EXISTS_TAC ``relab E2 (RELAB labl)`` 1505 >> ASM_REWRITE_TAC [] 1506 >> MATCH_MP_TAC RELABELING 1507 >> ASM_REWRITE_TAC []); 1508 1509val WEAK_RELAB_rf = store_thm ( 1510 "WEAK_RELAB_rf", 1511 ``!E u E'. 1512 WEAK_TRANS E u E' ==> 1513 !(rf :'b Relabeling). WEAK_TRANS (relab E rf) (relabel rf u) (relab E' rf)``, 1514 REPEAT GEN_TAC 1515 >> PURE_ONCE_REWRITE_TAC [WEAK_TRANS] 1516 >> REPEAT STRIP_TAC 1517 >> IMP_RES_TAC EPS_RELAB_rf 1518 >> EXISTS_TAC ``relab E1 rf`` 1519 >> EXISTS_TAC ``relab E2 rf`` 1520 >> ASM_REWRITE_TAC [] 1521 >> MATCH_MP_TAC RELABELING 1522 >> ASM_REWRITE_TAC []); 1523 1524(* Observation equivalence is substitutive under relabelling operator. *) 1525val WEAK_EQUIV_SUBST_RELAB = store_thm ( 1526 "WEAK_EQUIV_SUBST_RELAB", 1527 ``!E E'. WEAK_EQUIV E E' ==> !rf. WEAK_EQUIV (relab E rf) (relab E' rf)``, 1528 REPEAT STRIP_TAC 1529 >> PURE_ONCE_REWRITE_TAC [WEAK_EQUIV] 1530 >> EXISTS_TAC ``\x y. ?E1 E2 rf'. (x = relab E1 rf') /\ (y = relab E2 rf') /\ 1531 WEAK_EQUIV E1 E2`` 1532 >> CONJ_TAC (* 2 sub-goals here *) 1533 >| [ (* goal 1 (of 2) *) 1534 BETA_TAC \\ 1535 take [`E`, `E'`, `rf`] >> ASM_REWRITE_TAC [], 1536 (* goal 2 (of 2) *) 1537 PURE_ONCE_REWRITE_TAC [WEAK_BISIM] \\ 1538 BETA_TAC \\ 1539 REPEAT STRIP_TAC >| (* 4 sub-goals here *) 1540 [ (* goal 2.1 (of 4) *) 1541 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 1542 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 1543 IMP_RES_TAC TRANS_RELAB \\ 1544 PAT_X_ASSUM ``label (l :'b Label) = relabel rf' u'`` (ASSUME_TAC o SYM) \\ 1545 IMP_RES_TAC Relab_label \\ 1546 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 1547 (ASSUME ``TRANS E1 u' E''''``)) \\ 1548 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1549 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1550 EXISTS_TAC ``relab E2' rf'`` \\ 1551 CONJ_TAC >| (* 2 sub-goals here *) 1552 [ (* goal 2.1.1 (of 2) *) 1553 ASM_REWRITE_TAC [] \\ 1554 IMP_RES_TAC WEAK_RELAB_rf \\ 1555 PROVE_TAC [], 1556 (* goal 2.1.2 (of 2) *) 1557 take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ], 1558 (* goal 2.2 (of 4) *) 1559 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 1560 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 1561 IMP_RES_TAC TRANS_RELAB \\ 1562 PAT_X_ASSUM ``label (l :'b Label) = relabel rf' u'`` (ASSUME_TAC o SYM) \\ 1563 IMP_RES_TAC Relab_label \\ 1564 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 1565 (ASSUME ``TRANS E2 u' E''''``)) \\ 1566 IMP_RES_TAC (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1567 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1568 EXISTS_TAC ``relab E1' rf'`` \\ 1569 CONJ_TAC >| (* 2 sub-goals here *) 1570 [ (* goal 2.2.1 (of 2) *) 1571 ASM_REWRITE_TAC [] \\ 1572 IMP_RES_TAC WEAK_RELAB_rf \\ 1573 PROVE_TAC [], 1574 (* goal 2.2.2 (of 2) *) 1575 take [`E1'`, `E''''`, `rf'`] >> ASM_REWRITE_TAC [] ], 1576 (* goal 2.3 (of 4) *) 1577 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 1578 (ASSUME ``TRANS E'' tau E1'``)) \\ 1579 IMP_RES_TAC TRANS_RELAB \\ 1580 PAT_X_ASSUM ``(tau :'b Action) = relabel rf' u'`` (ASSUME_TAC o SYM) \\ 1581 IMP_RES_TAC Relab_tau \\ 1582 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 1583 (ASSUME ``TRANS E1 u' E''''``)) \\ 1584 IMP_RES_TAC (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1585 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1586 EXISTS_TAC ``relab E2' rf'`` \\ 1587 CONJ_TAC >| (* 2 sub-goals here *) 1588 [ (* goal 2.3.1 (of 2) *) 1589 ASM_REWRITE_TAC [] \\ 1590 IMP_RES_TAC EPS_RELAB_rf \\ 1591 ASM_REWRITE_TAC [], 1592 (* goal 2.3.2 (of 2) *) 1593 take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ], 1594 (* goal 2.4 (of 4) *) 1595 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 1596 (ASSUME ``TRANS E''' tau E2'``)) \\ 1597 IMP_RES_TAC TRANS_RELAB \\ 1598 PAT_X_ASSUM ``(tau :'b Action) = relabel rf' u'`` (ASSUME_TAC o SYM) \\ 1599 IMP_RES_TAC Relab_tau \\ 1600 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 1601 (ASSUME ``TRANS E2 u' E''''``)) \\ 1602 IMP_RES_TAC (CONJUNCT2 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1603 (ASSUME ``WEAK_EQUIV E1 E2``))) \\ 1604 EXISTS_TAC ``relab E1' rf'`` \\ 1605 CONJ_TAC >| (* 2 sub-goals here *) 1606 [ (* goal 2.4.1 (of 2) *) 1607 ASM_REWRITE_TAC [] \\ 1608 IMP_RES_TAC EPS_RELAB_rf \\ 1609 ASM_REWRITE_TAC [], 1610 (* goal 2.4.2 (of 2) *) 1611 take [`E1'`, `E''''`, `rf'`] \\ 1612 ASM_REWRITE_TAC [] ] ] ]); 1613 1614(******************************************************************************) 1615(* *) 1616(* Relationship between strong bisimulation (strong equiv.) *) 1617(* and weak bisimulation (observation equivalence) *) 1618(* *) 1619(******************************************************************************) 1620 1621(* A strong bisimulation is a particular weak bisimulation. *) 1622Theorem STRONG_IMP_WEAK_BISIM : 1623 !Bsm. STRONG_BISIM Bsm ==> WEAK_BISIM Bsm 1624Proof 1625 REWRITE_TAC [STRONG_BISIM_def, WEAK_BISIM_def, BISIM_IMP_WBISIM] 1626QED 1627 1628(* Strong equivalence implies weak/observation equivalence. *) 1629Theorem STRONG_IMP_WEAK_EQUIV : 1630 !E E'. STRONG_EQUIV E E' ==> WEAK_EQUIV E E' 1631Proof 1632 REWRITE_TAC [STRONG_EQUIV_def, WEAK_EQUIV_IS_WBISIM_REL, 1633 BISIM_REL_IMP_WBISIM_REL] 1634QED 1635 1636(******************************************************************************) 1637(* *) 1638(* Alternative half-definitions of WEAK_EQUIV using all WEAK_TRANS and EPS *) 1639(* *) 1640(******************************************************************************) 1641 1642(* `EPS E E1` implies zero or more tau transitions, and this leads to 1643 zero or at least one tau transition on the other side, which implies 1644 `EPS E' E2` in any case. 1645 1646 (Base case) | (Induct case) 1647 ========================================== 1648 !E ~~ !E' | !E ~~ !E' 1649 | | | || || || 1650 = = | eps eps || 1651 | | | || || || 1652 E ~~ ?E' | \/ \/ || 1653 | E1 ~~ ?E2 eps 1654 | | || || 1655 | tau eps || 1656 | | || || 1657 | \/ \/ \/ 1658 | E1' ~~ ?E2' 1659 *) 1660val WEAK_EQUIV_EPS = store_thm ((* NEW *) 1661 "WEAK_EQUIV_EPS", 1662 ``!E E'. WEAK_EQUIV E E' ==> 1663 !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2``, 1664 REPEAT STRIP_TAC 1665 >> PAT_X_ASSUM ``WEAK_EQUIV E E'`` MP_TAC 1666 >> POP_ASSUM MP_TAC 1667 >> Q.SPEC_TAC (`E1`, `E1`) 1668 >> Q.SPEC_TAC (`E`, `E`) 1669 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 1670 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1671 >| [ (* goal 1 (of 2) *) 1672 Q.EXISTS_TAC `E'` \\ 1673 RW_TAC std_ss [EPS_REFL], 1674 (* goal 2 (of 2) *) 1675 RES_TAC \\ 1676 IMP_RES_TAC (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1677 (ASSUME ``WEAK_EQUIV E1 E2``)) \\ 1678 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 1679 IMP_RES_TAC EPS_TRANS ]); 1680 1681val WEAK_EQUIV_EPS' = store_thm ((* NEW *) 1682 "WEAK_EQUIV_EPS'", 1683 ``!E E'. WEAK_EQUIV E E' ==> 1684 !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 1685 rpt GEN_TAC >> DISCH_TAC 1686 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP WEAK_EQUIV_SYM)) 1687 >> IMP_RES_TAC WEAK_EQUIV_EPS 1688 >> POP_ASSUM MP_TAC 1689 >> rpt STRIP_TAC 1690 >> RES_TAC 1691 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1692 >> IMP_RES_TAC WEAK_EQUIV_SYM); 1693 1694val WEAK_EQUIV_WEAK_TRANS_label = store_thm ((* NEW *) 1695 "WEAK_EQUIV_WEAK_TRANS_label", 1696 ``!E E'. WEAK_EQUIV E E' ==> 1697 !l E1. WEAK_TRANS E (label l) E1 ==> ?E2. WEAK_TRANS E' (label l) E2 /\ WEAK_EQUIV E1 E2``, 1698 REPEAT STRIP_TAC 1699 >> IMP_RES_TAC WEAK_TRANS 1700 >> IMP_RES_TAC (MATCH_MP WEAK_EQUIV_EPS (* lemma 1 used here *) 1701 (ASSUME ``WEAK_EQUIV E E'``)) 1702 >> IMP_RES_TAC (CONJUNCT1 1703 (PURE_ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 1704 (ASSUME ``WEAK_EQUIV E1' E2'``))) 1705 >> IMP_RES_TAC (REWRITE_RULE [WEAK_EQUIV_IS_WEAK_BISIM] 1706 (Q.SPECL [`WEAK_EQUIV`, `E2''`] 1707 (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E2 E1``)))) 1708 >> Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] 1709 >> IMP_RES_TAC EPS_WEAK_EPS); 1710 1711val WEAK_EQUIV_WEAK_TRANS_label' = store_thm ((* NEW *) 1712 "WEAK_EQUIV_WEAK_TRANS_label'", 1713 ``!E E'. WEAK_EQUIV E E' ==> 1714 !l E2. WEAK_TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 1715 rpt GEN_TAC >> DISCH_TAC 1716 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP WEAK_EQUIV_SYM)) 1717 >> IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label 1718 >> POP_ASSUM MP_TAC 1719 >> rpt STRIP_TAC 1720 >> RES_TAC 1721 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1722 >> IMP_RES_TAC WEAK_EQUIV_SYM); 1723 1724val WEAK_EQUIV_WEAK_TRANS_tau = store_thm ((* NEW *) 1725 "WEAK_EQUIV_WEAK_TRANS_tau", 1726 ``!E E'. WEAK_EQUIV E E' ==> 1727 !E1. WEAK_TRANS E tau E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2``, 1728 REPEAT STRIP_TAC 1729 >> IMP_RES_TAC WEAK_TRANS_TAU_IMP_TRANS_TAU 1730 >> IMP_RES_TAC (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] (ASSUME ``WEAK_EQUIV E E'``)) 1731 >> IMP_RES_TAC (REWRITE_RULE [WEAK_EQUIV_IS_WEAK_BISIM] 1732 (Q.SPECL [`WEAK_EQUIV`, `E2`] 1733 (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E1' E1``)))) 1734 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1735 >> IMP_RES_TAC EPS_TRANS); 1736 1737val WEAK_EQUIV_WEAK_TRANS_tau' = store_thm ((* NEW *) 1738 "WEAK_EQUIV_WEAK_TRANS_tau'", 1739 ``!E E'. WEAK_EQUIV E E' ==> 1740 !E2. WEAK_TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 1741 rpt GEN_TAC >> DISCH_TAC 1742 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP WEAK_EQUIV_SYM)) 1743 >> IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_tau 1744 >> POP_ASSUM MP_TAC 1745 >> rpt STRIP_TAC 1746 >> RES_TAC 1747 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1748 >> IMP_RES_TAC WEAK_EQUIV_SYM); 1749 1750(* A similar results for STRONG_EQUIV, needed sometimes *) 1751val STRONG_EQUIV_EPS = store_thm ((* NEW *) 1752 "STRONG_EQUIV_EPS", 1753 ``!E E'. STRONG_EQUIV E E' ==> 1754 !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ STRONG_EQUIV E1 E2``, 1755 REPEAT STRIP_TAC 1756 >> PAT_X_ASSUM ``STRONG_EQUIV E E'`` MP_TAC 1757 >> POP_ASSUM MP_TAC 1758 >> Q.SPEC_TAC (`E1`, `E1`) 1759 >> Q.SPEC_TAC (`E`, `E`) 1760 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 1761 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 1762 >| [ (* goal 1 (of 2) *) 1763 Q.EXISTS_TAC `E'` \\ 1764 RW_TAC std_ss [EPS_REFL], 1765 (* goal 2 (of 2) *) 1766 RES_TAC \\ 1767 IMP_RES_TAC (MATCH_MP PROPERTY_STAR_LEFT 1768 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 1769 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 1770 IMP_RES_TAC ONE_TAU \\ 1771 IMP_RES_TAC EPS_TRANS ]); 1772 1773val STRONG_EQUIV_EPS' = store_thm ((* NEW *) 1774 "STRONG_EQUIV_EPS'", 1775 ``!E E'. STRONG_EQUIV E E' ==> 1776 !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ STRONG_EQUIV E1 E2``, 1777 rpt GEN_TAC >> DISCH_TAC 1778 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP STRONG_EQUIV_SYM)) 1779 >> IMP_RES_TAC STRONG_EQUIV_EPS 1780 >> POP_ASSUM MP_TAC 1781 >> rpt STRIP_TAC 1782 >> RES_TAC 1783 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1784 >> IMP_RES_TAC STRONG_EQUIV_SYM); 1785 1786val STRONG_EQUIV_WEAK_TRANS = store_thm ((* NEW *) 1787 "STRONG_EQUIV_WEAK_TRANS", 1788 ``!E E'. STRONG_EQUIV E E' ==> 1789 !u E1. WEAK_TRANS E u E1 ==> ?E2. WEAK_TRANS E' u E2 /\ STRONG_EQUIV E1 E2``, 1790 REPEAT STRIP_TAC 1791 >> IMP_RES_TAC WEAK_TRANS 1792 >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS (* lemma 1 used here *) 1793 (ASSUME ``STRONG_EQUIV E E'``)) 1794 >> IMP_RES_TAC PROPERTY_STAR_LEFT 1795 >> POP_ASSUM K_TAC 1796 >> IMP_RES_TAC (MATCH_MP STRONG_EQUIV_EPS (* lemma 1 used here *) 1797 (ASSUME ``STRONG_EQUIV E2 E2''``)) 1798 >> Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] 1799 >> REWRITE_TAC [WEAK_TRANS] 1800 >> take [`E2'`, `E2''`] >> ASM_REWRITE_TAC []); 1801 1802val STRONG_EQUIV_WEAK_TRANS' = store_thm ((* NEW *) 1803 "STRONG_EQUIV_WEAK_TRANS'", 1804 ``!E E'. STRONG_EQUIV E E' ==> 1805 !u E2. WEAK_TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ STRONG_EQUIV E1 E2``, 1806 rpt GEN_TAC >> DISCH_TAC 1807 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP STRONG_EQUIV_SYM)) 1808 >> IMP_RES_TAC STRONG_EQUIV_WEAK_TRANS 1809 >> POP_ASSUM MP_TAC 1810 >> rpt STRIP_TAC 1811 >> RES_TAC 1812 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 1813 >> IMP_RES_TAC STRONG_EQUIV_SYM); 1814 1815val _ = export_theory (); 1816val _ = html_theory "WeakEQ"; 1817