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