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 pairTheory relationTheory bisimulationTheory listTheory; 10open CCSLib CCSTheory; 11 12val _ = new_theory "StrongEQ"; 13val _ = temp_loose_equality (); 14 15(******************************************************************************) 16(* *) 17(* Operational definition of strong equivalence for CCS (strong_sem.ml) *) 18(* *) 19(******************************************************************************) 20 21(* Type abbreviations *) 22val _ = type_abbrev_pp ("simulation", ``:('a, 'b) CCS -> ('a, 'b) CCS -> bool``); 23 24(* new definition based on relationTheory.BISIM *) 25val STRONG_BISIM_def = Define 26 `STRONG_BISIM (R :('a, 'b) simulation) = BISIM TRANS R`; 27 28(* original definition of STRONG_BISIM, now becomes a theorem *) 29Theorem STRONG_BISIM : 30 STRONG_BISIM (Bsm :('a, 'b) simulation) = 31 !E E'. Bsm E E' ==> 32 !u. 33 (!E1. TRANS E u E1 ==> 34 ?E2. TRANS E' u E2 /\ Bsm E1 E2) /\ 35 (!E2. TRANS E' u E2 ==> 36 ?E1. TRANS E u E1 /\ Bsm E1 E2) 37Proof 38 RW_TAC std_ss [STRONG_BISIM_def, BISIM_def] 39 >> METIS_TAC [] 40QED 41 42(* The identity relation is a strong bisimulation. *) 43Theorem IDENTITY_STRONG_BISIM : 44 STRONG_BISIM Id 45Proof 46 REWRITE_TAC [STRONG_BISIM_def, BISIM_ID] 47QED 48 49(* The converse of a strong bisimulation is a strong bisimulation. *) 50Theorem CONVERSE_STRONG_BISIM : 51 !Bsm. STRONG_BISIM Bsm ==> STRONG_BISIM (inv Bsm) 52Proof 53 REWRITE_TAC [STRONG_BISIM_def, BISIM_INV] 54QED 55 56(* The composition of two strong bisimulations is a strong bisimulation. *) 57Theorem COMP_STRONG_BISIM : 58 !Bsm1 Bsm2. STRONG_BISIM Bsm1 /\ STRONG_BISIM Bsm2 ==> 59 STRONG_BISIM (Bsm2 O Bsm1) 60Proof 61 REWRITE_TAC [STRONG_BISIM_def, BISIM_O] 62QED 63 64(* The union of two strong bisimulations is a strong bisimulation. *) 65Theorem UNION_STRONG_BISIM : 66 !Bsm1 Bsm2. STRONG_BISIM Bsm1 /\ STRONG_BISIM Bsm2 ==> 67 STRONG_BISIM (Bsm1 RUNION Bsm2) 68Proof 69 REWRITE_TAC [STRONG_BISIM_def, BISIM_RUNION] 70QED 71 72(* The (strong) bisimilarity, now based on BISIM_REL *) 73val STRONG_EQUIV_def = Define `STRONG_EQUIV = BISIM_REL TRANS`; 74 75val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 76 fixity = Infix (NONASSOC, 450), 77 paren_style = OnlyIfNecessary, 78 pp_elements = [HardSpace 1, TOK (UTF8.chr 0x223C), BreakSpace (1,0)], 79 term_name = "STRONG_EQUIV" }; 80 81val _ = TeX_notation { hol = UTF8.chr 0x223C, 82 TeX = ("\\HOLTokenStrongEQ", 1) }; 83 84(* |- !p q. 85 (!l. 86 (!p'. p --l-> p' ==> ?q'. q --l-> q' /\ STRONG_EQUIV p' q') /\ 87 !q'. q --l-> q' ==> ?p'. p --l-> p' /\ STRONG_EQUIV p' q') ==> 88 STRONG_EQUIV p q 89 *) 90val STRONG_EQUIV_rules = save_thm 91 ("STRONG_EQUIV_rules", 92 REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_rules)); 93 94(* |- !BISIM_REL'. 95 (!a0 a1. 96 BISIM_REL' a0 a1 ==> 97 !l. 98 (!p'. a0 --l-> p' ==> ?q'. a1 --l-> q' /\ BISIM_REL' p' q') /\ 99 !q'. a1 --l-> q' ==> ?p'. a0 --l-> p' /\ BISIM_REL' p' q') ==> 100 !a0 a1. BISIM_REL' a0 a1 ==> STRONG_EQUIV a0 a1 101 *) 102val STRONG_EQUIV_coind = save_thm 103 ("STRONG_EQUIV_coind", 104 REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_coind)); 105 106(* |- !a0 a1. 107 STRONG_EQUIV a0 a1 <=> 108 !l. 109 (!p'. a0 --l-> p' ==> ?q'. a1 --l-> q' /\ STRONG_EQUIV p' q') /\ 110 !q'. a1 --l-> q' ==> ?p'. a0 --l-> p' /\ STRONG_EQUIV p' q' 111 *) 112val STRONG_EQUIV_cases = save_thm 113 ("STRONG_EQUIV_cases", 114 REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_cases)); 115 116Theorem STRONG_EQUIV_IS_STRONG_BISIM : 117 STRONG_BISIM STRONG_EQUIV 118Proof 119 REWRITE_TAC [STRONG_BISIM_def, STRONG_EQUIV_def, BISIM_REL_IS_BISIM] 120QED 121 122(* Alternative definition of STRONG_EQUIV *) 123Theorem STRONG_EQUIV : 124 !E E'. STRONG_EQUIV E E' = ?Bsm. Bsm E E' /\ STRONG_BISIM Bsm 125Proof 126 METIS_TAC [STRONG_EQUIV_def, STRONG_BISIM_def, BISIM_REL_def] 127QED 128 129Theorem STRONG_EQUIV_equivalence : 130 equivalence STRONG_EQUIV 131Proof 132 REWRITE_TAC [STRONG_EQUIV_def, BISIM_REL_IS_EQUIV_REL] 133QED 134 135Theorem STRONG_EQUIV_REFL : 136 !E. STRONG_EQUIV E E 137Proof 138 PROVE_TAC [REWRITE_RULE [equivalence_def, reflexive_def] 139 STRONG_EQUIV_equivalence] 140QED 141 142Theorem STRONG_EQUIV_SYM : 143 !E E'. STRONG_EQUIV E E' ==> STRONG_EQUIV E' E 144Proof 145 PROVE_TAC [REWRITE_RULE [equivalence_def, symmetric_def] 146 STRONG_EQUIV_equivalence] 147QED 148 149Theorem STRONG_EQUIV_TRANS : 150 !E E' E''. STRONG_EQUIV E E' /\ STRONG_EQUIV E' E'' ==> STRONG_EQUIV E E'' 151Proof 152 PROVE_TAC [REWRITE_RULE [equivalence_def, transitive_def] 153 STRONG_EQUIV_equivalence] 154QED 155 156val STRONG_BISIM_SUBSET_STRONG_EQUIV = store_thm ( 157 "STRONG_BISIM_SUBSET_STRONG_EQUIV", 158 ``!Bsm. STRONG_BISIM Bsm ==> Bsm RSUBSET STRONG_EQUIV``, 159 PROVE_TAC [RSUBSET, STRONG_EQUIV]); 160 161(* Syntactic equivalence implies strong equivalence. *) 162val EQUAL_IMP_STRONG_EQUIV = store_thm ( 163 "EQUAL_IMP_STRONG_EQUIV", ``!E E'. (E = E') ==> STRONG_EQUIV E E'``, 164 REPEAT STRIP_TAC 165 >> PURE_ASM_REWRITE_TAC [STRONG_EQUIV_REFL]); 166 167(* Prop. 4, page 91: strong equivalence satisfies property [*] *) 168Theorem PROPERTY_STAR : 169 !E E'. STRONG_EQUIV E E' <=> 170 !u. (!E1. TRANS E u E1 ==> ?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2) /\ 171 (!E2. TRANS E' u E2 ==> ?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2) 172Proof 173 METIS_TAC [STRONG_EQUIV_cases] 174QED 175 176(* Half versions of PROPERTY_STAR *) 177val PROPERTY_STAR_LEFT = store_thm ( 178 "PROPERTY_STAR_LEFT", 179 ``!E E'. STRONG_EQUIV E E' ==> 180 !u E1. TRANS E u E1 ==> ?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2``, 181 PROVE_TAC [PROPERTY_STAR]); 182 183val PROPERTY_STAR_RIGHT = store_thm ( 184 "PROPERTY_STAR_RIGHT", 185 ``!E E'. STRONG_EQUIV E E' ==> 186 !u E2. TRANS E' u E2 ==> ?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2``, 187 PROVE_TAC [PROPERTY_STAR]); 188 189(* Strong equivalence is substitutive under prefix operator. *) 190val STRONG_EQUIV_SUBST_PREFIX = store_thm ( 191 "STRONG_EQUIV_SUBST_PREFIX", 192 ``!E E'. 193 STRONG_EQUIV E E' ==> !u. STRONG_EQUIV (prefix u E) (prefix u E')``, 194 REPEAT GEN_TAC 195 >> PURE_ONCE_REWRITE_TAC 196 [SPECL [``prefix (u :'b Action) E``, ``prefix (u :'b Action) E'``] PROPERTY_STAR] 197 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 198 >| [ EXISTS_TAC ``E' :('a, 'b) CCS``, 199 EXISTS_TAC ``E :('a, 'b) CCS``] 200 >> IMP_RES_TAC TRANS_PREFIX 201 >> ASM_REWRITE_TAC [PREFIX]); 202 203(* Strong equivalence is preserved by binary summation. *) 204val STRONG_EQUIV_PRESD_BY_SUM = store_thm ( 205 "STRONG_EQUIV_PRESD_BY_SUM", 206 ``!E1 E1' E2 E2'. 207 STRONG_EQUIV E1 E1' /\ STRONG_EQUIV E2 E2' ==> 208 STRONG_EQUIV (sum E1 E2) (sum E1' E2')``, 209 REPEAT GEN_TAC 210 >> PURE_ONCE_REWRITE_TAC [PROPERTY_STAR] 211 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 212 >| [ (* goal 1 *) 213 IMP_RES_TAC TRANS_SUM \\ (* 2 sub-goals here *) 214 RES_TAC \\ 215 EXISTS_TAC ``E2'' :('a, 'b) CCS`` \\ 216 ASM_REWRITE_TAC [] 217 >| [ MATCH_MP_TAC SUM1, MATCH_MP_TAC SUM2 ] \\ 218 ASM_REWRITE_TAC [], 219 (* goal 2 *) 220 IMP_RES_TAC TRANS_SUM \\ (* 2 sub-goals here *) 221 RES_TAC \\ 222 EXISTS_TAC ``E1'' :('a, 'b) CCS`` \\ 223 ASM_REWRITE_TAC [] 224 >| [ MATCH_MP_TAC SUM1, MATCH_MP_TAC SUM2] \\ 225 ASM_REWRITE_TAC [] ]); 226 227(* Strong equivalence is substitutive under summation operator on the right. 228 |- !E E'. STRONG_EQUIV E E' ==> (!E''. STRONG_EQUIV (sum E E'') (sum E' E'')) 229 *) 230val STRONG_EQUIV_SUBST_SUM_R = save_thm ( 231 "STRONG_EQUIV_SUBST_SUM_R", 232 (GEN_ALL o 233 DISCH_ALL o 234 GEN_ALL o 235 UNDISCH o 236 (REWRITE_RULE [STRONG_EQUIV_REFL]) o 237 DISCH_ALL) 238 (MATCH_MP STRONG_EQUIV_PRESD_BY_SUM 239 (CONJ (ASSUME ``STRONG_EQUIV E E'``) 240 (ASSUME ``STRONG_EQUIV E'' E''``)))); 241 242(* Strong equivalence is substitutive under summation operator on the left. 243 |- !E E'. STRONG_EQUIV E E' ==> (!E''. STRONG_EQUIV (sum E'' E) (sum E'' E')) 244 *) 245val STRONG_EQUIV_SUBST_SUM_L = save_thm ( 246 "STRONG_EQUIV_SUBST_SUM_L", 247 (GEN_ALL o 248 DISCH_ALL o 249 GEN_ALL o 250 UNDISCH o 251 (REWRITE_RULE [STRONG_EQUIV_REFL]) o 252 DISCH_ALL) 253 (MATCH_MP STRONG_EQUIV_PRESD_BY_SUM 254 (CONJ (ASSUME ``STRONG_EQUIV E'' E''``) 255 (ASSUME ``STRONG_EQUIV E E'``)))); 256 257(* Strong equivalence is preserved by parallel composition. *) 258val STRONG_EQUIV_PRESD_BY_PAR = store_thm ( 259 "STRONG_EQUIV_PRESD_BY_PAR", 260 ``!E1 E1' E2 E2'. 261 STRONG_EQUIV E1 E1' /\ STRONG_EQUIV E2 E2' ==> 262 STRONG_EQUIV (par E1 E2) (par E1' E2')``, 263 REPEAT STRIP_TAC 264 >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV] 265 >> EXISTS_TAC 266 ``\x y. 267 (?F1 F2 F3 F4. 268 (x = par F1 F3) /\ (y = par F2 F4) /\ 269 STRONG_EQUIV F1 F2 /\ STRONG_EQUIV F3 F4)`` 270 >> CONJ_TAC (* 2 sub-goals here *) 271 >| [ (* goal 1 (of 2) *) 272 BETA_TAC \\ 273 take [`E1`, `E1'`, `E2`, `E2'`] \\ 274 ASM_REWRITE_TAC [], 275 (* goal 2 (of 2) *) 276 PURE_ONCE_REWRITE_TAC [STRONG_BISIM] \\ 277 BETA_TAC \\ 278 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 279 [ (* goal 2.1 (of 2) *) 280 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F3``] 281 (ASSUME ``TRANS E u E1''``)) \\ 282 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 283 [ (* goal 2.1.1 (of 3) *) 284 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 285 (ASSUME ``STRONG_EQUIV F1 F2``)) \\ 286 EXISTS_TAC ``par E2'' F4`` \\ 287 ASM_REWRITE_TAC [] \\ 288 CONJ_TAC >| (* 2 sub-goals here *) 289 [ (* goal 2.1.1.1 (of 2) *) 290 MATCH_MP_TAC PAR1 \\ 291 PURE_ONCE_ASM_REWRITE_TAC [], 292 (* goal 2.1.1.2 (of 2) *) 293 take [`E1'''`, `E2''`, `F3`, `F4`] \\ 294 ASM_REWRITE_TAC [] ], 295 (* goal 2.1.2 (of 3) *) 296 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 297 (ASSUME ``STRONG_EQUIV F3 F4``)) \\ 298 EXISTS_TAC ``par F2 E2''`` \\ 299 ASM_REWRITE_TAC [] \\ 300 CONJ_TAC >| (* 2 sub-goals here *) 301 [ (* goal 2.1.2.1 (of 2) *) 302 MATCH_MP_TAC PAR2 >> PURE_ONCE_ASM_REWRITE_TAC [], 303 (* goal 2.1.2.2 (of 2) *) 304 take [`F1`, `F2`, `E1'''`, `E2''`] \\ 305 ASM_REWRITE_TAC [] ], 306 (* goal 2.1.3 (of 3) *) 307 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 308 (ASSUME ``STRONG_EQUIV F1 F2``)) \\ 309 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 310 (ASSUME ``STRONG_EQUIV F3 F4``)) \\ 311 EXISTS_TAC ``par E2''' E2''''`` \\ 312 ASM_REWRITE_TAC [] \\ 313 CONJ_TAC >| (* 2 sub-goals here *) 314 [ (* goal 2.1.3.1 (of 2) *) 315 MATCH_MP_TAC PAR3 \\ 316 EXISTS_TAC ``l: 'b Label`` \\ 317 ASM_REWRITE_TAC [], 318 (* goal 2.1.3.2 (of 2) *) 319 take [`E1'''`, `E2'''`, `E2''`, `E2''''`] \\ 320 ASM_REWRITE_TAC [] ] ], 321 (* goal 2.2 (of 2) *) 322 ASSUME_TAC 323 (REWRITE_RULE [ASSUME ``E' = par F2 F4``] 324 (ASSUME ``TRANS E' u E2''``)) \\ 325 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 326 [ (* goal 2.2.1 (of 3) *) 327 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 328 (ASSUME ``STRONG_EQUIV F1 F2``)) \\ 329 EXISTS_TAC ``par E1''' F3`` \\ 330 ASM_REWRITE_TAC [] \\ 331 CONJ_TAC >| (* 2 sub-goals here *) 332 [ (* goal 2.2.1.1 (of 2) *) 333 MATCH_MP_TAC PAR1 \\ 334 PURE_ONCE_ASM_REWRITE_TAC [], 335 (* goal 2.2.1.2 (of 2) *) 336 take [`E1'''`, `E1''`, `F3`, `F4`] \\ 337 ASM_REWRITE_TAC [] ], 338 (* goal 2.2.2 (of 3) *) 339 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 340 (ASSUME ``STRONG_EQUIV F3 F4``)) \\ 341 EXISTS_TAC ``par F1 E1'''`` \\ 342 ASM_REWRITE_TAC [] \\ 343 CONJ_TAC >| (* 2 sub-goals here *) 344 [ (* goal 2.2.2.1 (of 2) *) 345 MATCH_MP_TAC PAR2 \\ 346 PURE_ONCE_ASM_REWRITE_TAC [], 347 (* goal 2.2.2.2 (of 2) *) 348 take [`F1`, `F2`, `E1'''`, `E1''`] \\ 349 ASM_REWRITE_TAC [] ], 350 (* goal 2.2.3 (of 3) *) 351 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 352 (ASSUME ``STRONG_EQUIV F1 F2``)) \\ 353 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 354 (ASSUME ``STRONG_EQUIV F3 F4``)) \\ 355 EXISTS_TAC ``par E1''' E1''''`` \\ 356 ASM_REWRITE_TAC [] \\ 357 CONJ_TAC >| (* 2 sub-goals here *) 358 [ (* goal 2.2.3.1 (of 2) *) 359 MATCH_MP_TAC PAR3 \\ 360 EXISTS_TAC ``l: 'b Label`` \\ 361 ASM_REWRITE_TAC [], 362 (* goal 2.2.3.2 (of 2) *) 363 take [`E1'''`, `E1''`, `E1''''`, `E2'''`] \\ 364 ASM_REWRITE_TAC [] ] ] ] ]); 365 366(* Strong equivalence is substitutive under parallel operator on the right: 367 |- !E E'. STRONG_EQUIV E E' ==> (!E''. STRONG_EQUIV (par E E'') (par E' E'')) 368 *) 369val STRONG_EQUIV_SUBST_PAR_R = save_thm ( 370 "STRONG_EQUIV_SUBST_PAR_R", 371 Q.GENL [`E`, `E'`] 372 (DISCH_ALL 373 (GEN_ALL 374 (UNDISCH 375 (REWRITE_RULE [STRONG_EQUIV_REFL] 376 (DISCH_ALL 377 (MATCH_MP STRONG_EQUIV_PRESD_BY_PAR 378 (CONJ (ASSUME ``STRONG_EQUIV E E'``) 379 (ASSUME ``STRONG_EQUIV E'' E''``))))))))); 380 381(* Strong equivalence is substitutive under parallel operator on the left: 382 |- !E E'. STRONG_EQUIV E E' ==> (!E''. STRONG_EQUIV (par E'' E) (par E'' E')) 383 *) 384val STRONG_EQUIV_SUBST_PAR_L = save_thm ( 385 "STRONG_EQUIV_SUBST_PAR_L", 386 Q.GENL [`E`, `E'`] 387 (DISCH_ALL 388 (GEN_ALL 389 (UNDISCH 390 (REWRITE_RULE [STRONG_EQUIV_REFL] 391 (DISCH_ALL 392 (MATCH_MP STRONG_EQUIV_PRESD_BY_PAR 393 (CONJ (ASSUME ``STRONG_EQUIV E'' E''``) 394 (ASSUME ``STRONG_EQUIV E E'``))))))))); 395 396(* Strong equivalence is substitutive under restriction operator. *) 397val STRONG_EQUIV_SUBST_RESTR = store_thm ( 398 "STRONG_EQUIV_SUBST_RESTR", 399 ``!E E'. 400 STRONG_EQUIV E E' ==> 401 (!L. STRONG_EQUIV (restr L E) (restr L E'))``, 402 REPEAT STRIP_TAC 403 >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV] 404 >> EXISTS_TAC ``\x y. ?E1 E2 L'. (x = restr L' E1) /\ (y = restr L' E2) /\ 405 STRONG_EQUIV E1 E2`` 406 >> CONJ_TAC (* 2 sub-goals here *) 407 >| [ (* goal 1 (of 2) *) 408 BETA_TAC \\ 409 take [`E`, `E'`, `L`] \\ 410 ASM_REWRITE_TAC [], 411 (* goal 2 (of 2) *) 412 PURE_ONCE_REWRITE_TAC [STRONG_BISIM] \\ 413 BETA_TAC \\ 414 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 415 [ (* goal 2.1 (of 2) *) 416 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 417 (ASSUME ``TRANS E'' u E1'``)) \\ 418 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 419 [ (* goal 2.1.1 (of 2) *) 420 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 421 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 422 EXISTS_TAC ``restr (L' :'b Label set) E2'`` \\ 423 CONJ_TAC >| (* 2 sub-goals here *) 424 [ (* goal 2.1.1.1 (of 2) *) 425 ASM_REWRITE_TAC [] \\ 426 MATCH_MP_TAC RESTR \\ 427 REWRITE_TAC [REWRITE_RULE [ASSUME ``(u :'b Action) = tau``] 428 (ASSUME ``TRANS E2 u E2'``)], 429 (* goal 2.1.1.2 (of 2) *) 430 take [`E''''`, `E2'`, `L'`] \\ 431 ASM_REWRITE_TAC [] ], 432 (* goal 2.1.2 (of 2) *) 433 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 434 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 435 EXISTS_TAC ``restr (L' :'b Label set) E2'`` \\ 436 CONJ_TAC >| (* 2 sub-goals here *) 437 [ (* goal 2.1.2.1 (of 2) *) 438 ASM_REWRITE_TAC [] \\ 439 MATCH_MP_TAC RESTR \\ 440 EXISTS_TAC ``l: 'b Label`` \\ 441 ASM_REWRITE_TAC [REWRITE_RULE [ASSUME ``(u :'b Action) = label l``] 442 (ASSUME ``TRANS E2 u E2'``)], 443 (* goal 2.1.2.2 (of 2) *) 444 take [`E''''`, `E2'`, `L'`] \\ 445 ASM_REWRITE_TAC [] ] ], 446 (* goal 2.2 (of 2) *) 447 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 448 (ASSUME ``TRANS E''' u E2'``)) \\ 449 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 450 [ (* goal 2.2.1 (of 2) *) 451 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 452 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 453 EXISTS_TAC ``restr (L' :'b Label set) E1'`` \\ 454 CONJ_TAC >| (* 2 sub-goals here *) 455 [ (* goal 2.2.1.1 (of 2) *) 456 ASM_REWRITE_TAC [] \\ 457 MATCH_MP_TAC RESTR \\ 458 REWRITE_TAC [REWRITE_RULE [ASSUME ``(u :'b Action) = tau``] 459 (ASSUME ``TRANS E1 u E1'``)], 460 (* goal 2.2.1.2 (of 2) *) 461 take [`E1'`, `E''''`, `L'`] \\ 462 ASM_REWRITE_TAC [] ], 463 (* goal 2.2.2 (of 2) *) 464 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 465 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 466 EXISTS_TAC ``restr (L' :'b Label set) E1'`` \\ 467 CONJ_TAC >| (* 2 sub-goals here *) 468 [ (* goal 2.2.2.1 (of 2) *) 469 ASM_REWRITE_TAC [] \\ 470 MATCH_MP_TAC RESTR \\ 471 EXISTS_TAC ``l: 'b Label`` \\ 472 ASM_REWRITE_TAC [REWRITE_RULE [ASSUME ``(u :'b Action) = label l``] 473 (ASSUME ``TRANS E1 u E1'``)], 474 (* goal 2.2.2.2 (of 2) *) 475 take [`E1'`, `E''''`, `L'`] \\ 476 ASM_REWRITE_TAC [] ] ] ] ]); 477 478(* Strong equivalence is substitutive under relabelling operator. *) 479val STRONG_EQUIV_SUBST_RELAB = store_thm ( 480 "STRONG_EQUIV_SUBST_RELAB", 481 ``!E E'. 482 STRONG_EQUIV E E' ==> 483 (!rf. STRONG_EQUIV (relab E rf) (relab E' rf))``, 484 REPEAT STRIP_TAC 485 >> PURE_ONCE_REWRITE_TAC [STRONG_EQUIV] 486 >> EXISTS_TAC ``\x y. ?E1 E2 rf'. (x = relab E1 rf') /\ (y = relab E2 rf') /\ 487 STRONG_EQUIV E1 E2`` 488 >> CONJ_TAC (* 2 sub-goals here *) 489 >| [ (* goal 1 (of 2) *) 490 BETA_TAC \\ 491 take [`E`, `E'`, `rf`] \\ 492 ASM_REWRITE_TAC [], 493 (* goal 2 (of 2) *) 494 PURE_ONCE_REWRITE_TAC [STRONG_BISIM] \\ 495 BETA_TAC \\ 496 REPEAT STRIP_TAC >| (* 2 sub-goals here *) 497 [ (* goal 2.1 (of 2) *) 498 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 499 (ASSUME ``TRANS E'' u E1'``)) \\ 500 IMP_RES_TAC TRANS_RELAB \\ 501 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 502 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 503 EXISTS_TAC ``relab E2' rf'`` \\ 504 CONJ_TAC >| (* 2 sub-goals here *) 505 [ (* goal 2.1.1 (of 2) *) 506 ASM_REWRITE_TAC [] \\ 507 MATCH_MP_TAC RELABELING \\ 508 PURE_ONCE_ASM_REWRITE_TAC [], 509 (* goal 2.1.2 (of 2) *) 510 take [`E''''`, `E2'`, `rf'`] \\ 511 ASM_REWRITE_TAC [] ], 512 (* goal 2.2 (of 2) *) 513 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 514 (ASSUME ``TRANS E''' u E2'``)) \\ 515 IMP_RES_TAC TRANS_RELAB \\ 516 IMP_RES_TAC (ONCE_REWRITE_RULE [PROPERTY_STAR] 517 (ASSUME ``STRONG_EQUIV E1 E2``)) \\ 518 EXISTS_TAC ``relab E1' rf'`` \\ 519 CONJ_TAC >| (* 2 sub-goals here *) 520 [ (* goal 2.2.1 (of 2) *) 521 ASM_REWRITE_TAC [] \\ 522 MATCH_MP_TAC RELABELING \\ 523 PURE_ONCE_ASM_REWRITE_TAC [], 524 (* goal 2.2.2 (of 2) *) 525 take [`E1'`, `E''''`, `rf'`] \\ 526 ASM_REWRITE_TAC [] ] ] ]); 527 528val _ = export_theory (); 529val _ = html_theory "StrongEQ"; 530