1274955Ssvnmir(* 2274955Ssvnmir * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3353358Sdim * Copyright 2016-2017 University of Bologna, Italy (Author: Chun Tian) 4353358Sdim * Copyright 2018-2019 Fondazione Bruno Kessler, Italy (Author: Chun Tian) 5353358Sdim *) 6274955Ssvnmir 7274955Ssvnmiropen HolKernel Parse boolLib bossLib; 8314564Sdim 9314564Sdimopen pred_setTheory pairTheory relationTheory bisimulationTheory listTheory; 10314564Sdimopen CCSLib CCSTheory; 11274955Ssvnmir 12274955Ssvnmirval _ = new_theory "StrongEQ"; 13274955Ssvnmirval _ = temp_loose_equality (); 14274955Ssvnmir 15321369Sdim(******************************************************************************) 16274955Ssvnmir(* *) 17321369Sdim(* Operational definition of strong equivalence for CCS (strong_sem.ml) *) 18280031Sdim(* *) 19274955Ssvnmir(******************************************************************************) 20274955Ssvnmir 21314564Sdim(* Type abbreviations *) 22327952Sdimval _ = type_abbrev_pp ("simulation", ``:('a, 'b) CCS -> ('a, 'b) CCS -> bool``); 23327952Sdim 24274955Ssvnmir(* new definition based on relationTheory.BISIM *) 25274955Ssvnmirval STRONG_BISIM_def = Define 26274955Ssvnmir `STRONG_BISIM (R :('a, 'b) simulation) = BISIM TRANS R`; 27274955Ssvnmir 28274955Ssvnmir(* original definition of STRONG_BISIM, now becomes a theorem *) 29274955SsvnmirTheorem STRONG_BISIM : 30274955Ssvnmir STRONG_BISIM (Bsm :('a, 'b) simulation) = 31274955Ssvnmir !E E'. Bsm E E' ==> 32296417Sdim !u. 33296417Sdim (!E1. TRANS E u E1 ==> 34274955Ssvnmir ?E2. TRANS E' u E2 /\ Bsm E1 E2) /\ 35274955Ssvnmir (!E2. TRANS E' u E2 ==> 36274955Ssvnmir ?E1. TRANS E u E1 /\ Bsm E1 E2) 37274955SsvnmirProof 38314564Sdim RW_TAC std_ss [STRONG_BISIM_def, BISIM_def] 39314564Sdim >> METIS_TAC [] 40314564SdimQED 41314564Sdim 42274955Ssvnmir(* The identity relation is a strong bisimulation. *) 43274955SsvnmirTheorem IDENTITY_STRONG_BISIM : 44314564Sdim STRONG_BISIM Id 45296417SdimProof 46296417Sdim REWRITE_TAC [STRONG_BISIM_def, BISIM_ID] 47296417SdimQED 48274955Ssvnmir 49280031Sdim(* The converse of a strong bisimulation is a strong bisimulation. *) 50274955SsvnmirTheorem CONVERSE_STRONG_BISIM : 51314564Sdim !Bsm. STRONG_BISIM Bsm ==> STRONG_BISIM (inv Bsm) 52309124SdimProof 53280031Sdim REWRITE_TAC [STRONG_BISIM_def, BISIM_INV] 54274955SsvnmirQED 55274955Ssvnmir 56274955Ssvnmir(* The composition of two strong bisimulations is a strong bisimulation. *) 57274955SsvnmirTheorem COMP_STRONG_BISIM : 58274955Ssvnmir !Bsm1 Bsm2. STRONG_BISIM Bsm1 /\ STRONG_BISIM Bsm2 ==> 59274955Ssvnmir STRONG_BISIM (Bsm2 O Bsm1) 60274955SsvnmirProof 61296417Sdim REWRITE_TAC [STRONG_BISIM_def, BISIM_O] 62296417SdimQED 63296417Sdim 64314564Sdim(* The union of two strong bisimulations is a strong bisimulation. *) 65314564SdimTheorem UNION_STRONG_BISIM : 66314564Sdim !Bsm1 Bsm2. STRONG_BISIM Bsm1 /\ STRONG_BISIM Bsm2 ==> 67274955Ssvnmir STRONG_BISIM (Bsm1 RUNION Bsm2) 68274955SsvnmirProof 69274955Ssvnmir REWRITE_TAC [STRONG_BISIM_def, BISIM_RUNION] 70274955SsvnmirQED 71353358Sdim 72353358Sdim(* The (strong) bisimilarity, now based on BISIM_REL *) 73353358Sdimval STRONG_EQUIV_def = Define `STRONG_EQUIV = BISIM_REL TRANS`; 74353358Sdim 75353358Sdimval _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 76353358Sdim fixity = Infix (NONASSOC, 450), 77353358Sdim paren_style = OnlyIfNecessary, 78353358Sdim pp_elements = [HardSpace 1, TOK (UTF8.chr 0x223C), BreakSpace (1,0)], 79353358Sdim term_name = "STRONG_EQUIV" }; 80353358Sdim 81353358Sdimval _ = TeX_notation { hol = UTF8.chr 0x223C, 82353358Sdim TeX = ("\\HOLTokenStrongEQ", 1) }; 83353358Sdim 84353358Sdim(* |- !p q. 85353358Sdim (!l. 86353358Sdim (!p'. p --l-> p' ==> ?q'. q --l-> q' /\ STRONG_EQUIV p' q') /\ 87353358Sdim !q'. q --l-> q' ==> ?p'. p --l-> p' /\ STRONG_EQUIV p' q') ==> 88353358Sdim STRONG_EQUIV p q 89353358Sdim *) 90353358Sdimval STRONG_EQUIV_rules = save_thm 91353358Sdim ("STRONG_EQUIV_rules", 92353358Sdim REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_rules)); 93353358Sdim 94353358Sdim(* |- !BISIM_REL'. 95353358Sdim (!a0 a1. 96353358Sdim BISIM_REL' a0 a1 ==> 97353358Sdim !l. 98353358Sdim (!p'. a0 --l-> p' ==> ?q'. a1 --l-> q' /\ BISIM_REL' p' q') /\ 99353358Sdim !q'. a1 --l-> q' ==> ?p'. a0 --l-> p' /\ BISIM_REL' p' q') ==> 100353358Sdim !a0 a1. BISIM_REL' a0 a1 ==> STRONG_EQUIV a0 a1 101353358Sdim *) 102353358Sdimval STRONG_EQUIV_coind = save_thm 103353358Sdim ("STRONG_EQUIV_coind", 104353358Sdim REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_coind)); 105353358Sdim 106353358Sdim(* |- !a0 a1. 107353358Sdim STRONG_EQUIV a0 a1 <=> 108353358Sdim !l. 109353358Sdim (!p'. a0 --l-> p' ==> ?q'. a1 --l-> q' /\ STRONG_EQUIV p' q') /\ 110353358Sdim !q'. a1 --l-> q' ==> ?p'. a0 --l-> p' /\ STRONG_EQUIV p' q' 111353358Sdim *) 112327952Sdimval STRONG_EQUIV_cases = save_thm 113327952Sdim ("STRONG_EQUIV_cases", 114327952Sdim REWRITE_RULE [SYM STRONG_EQUIV_def] (Q.ISPEC `TRANS` BISIM_REL_cases)); 115327952Sdim 116314564SdimTheorem STRONG_EQUIV_IS_STRONG_BISIM : 117274955Ssvnmir STRONG_BISIM STRONG_EQUIV 118314564SdimProof 119274955Ssvnmir REWRITE_TAC [STRONG_BISIM_def, STRONG_EQUIV_def, BISIM_REL_IS_BISIM] 120274955SsvnmirQED 121274955Ssvnmir 122274955Ssvnmir(* Alternative definition of STRONG_EQUIV *) 123274955SsvnmirTheorem STRONG_EQUIV : 124341825Sdim !E E'. STRONG_EQUIV E E' = ?Bsm. Bsm E E' /\ STRONG_BISIM Bsm 125274955SsvnmirProof 126274955Ssvnmir METIS_TAC [STRONG_EQUIV_def, STRONG_BISIM_def, BISIM_REL_def] 127309124SdimQED 128309124Sdim 129309124SdimTheorem STRONG_EQUIV_equivalence : 130341825Sdim equivalence STRONG_EQUIV 131341825SdimProof 132341825Sdim REWRITE_TAC [STRONG_EQUIV_def, BISIM_REL_IS_EQUIV_REL] 133309124SdimQED 134309124Sdim 135327952SdimTheorem STRONG_EQUIV_REFL : 136353358Sdim !E. STRONG_EQUIV E E 137353358SdimProof 138327952Sdim PROVE_TAC [REWRITE_RULE [equivalence_def, reflexive_def] 139321369Sdim STRONG_EQUIV_equivalence] 140327952SdimQED 141314564Sdim 142314564SdimTheorem STRONG_EQUIV_SYM : 143314564Sdim !E E'. STRONG_EQUIV E E' ==> STRONG_EQUIV E' E 144314564SdimProof 145314564Sdim PROVE_TAC [REWRITE_RULE [equivalence_def, symmetric_def] 146314564Sdim STRONG_EQUIV_equivalence] 147314564SdimQED 148360784Sdim 149360784SdimTheorem STRONG_EQUIV_TRANS : 150314564Sdim !E E' E''. STRONG_EQUIV E E' /\ STRONG_EQUIV E' E'' ==> STRONG_EQUIV E E'' 151314564SdimProof 152314564Sdim PROVE_TAC [REWRITE_RULE [equivalence_def, transitive_def] 153341825Sdim STRONG_EQUIV_equivalence] 154341825SdimQED 155314564Sdim 156314564Sdimval STRONG_BISIM_SUBSET_STRONG_EQUIV = store_thm ( 157341825Sdim "STRONG_BISIM_SUBSET_STRONG_EQUIV", 158314564Sdim ``!Bsm. STRONG_BISIM Bsm ==> Bsm RSUBSET STRONG_EQUIV``, 159274955Ssvnmir PROVE_TAC [RSUBSET, STRONG_EQUIV]); 160314564Sdim 161314564Sdim(* Syntactic equivalence implies strong equivalence. *) 162314564Sdimval EQUAL_IMP_STRONG_EQUIV = store_thm ( 163341825Sdim "EQUAL_IMP_STRONG_EQUIV", ``!E E'. (E = E') ==> STRONG_EQUIV E E'``, 164314564Sdim REPEAT STRIP_TAC 165314564Sdim >> PURE_ASM_REWRITE_TAC [STRONG_EQUIV_REFL]); 166314564Sdim 167314564Sdim(* Prop. 4, page 91: strong equivalence satisfies property [*] *) 168314564SdimTheorem PROPERTY_STAR : 169314564Sdim !E E'. STRONG_EQUIV E E' <=> 170341825Sdim !u. (!E1. TRANS E u E1 ==> ?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2) /\ 171314564Sdim (!E2. TRANS E' u E2 ==> ?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2) 172314564SdimProof 173341825Sdim METIS_TAC [STRONG_EQUIV_cases] 174314564SdimQED 175314564Sdim 176341825Sdim(* Half versions of PROPERTY_STAR *) 177314564Sdimval PROPERTY_STAR_LEFT = store_thm ( 178314564Sdim "PROPERTY_STAR_LEFT", 179314564Sdim ``!E E'. STRONG_EQUIV E E' ==> 180314564Sdim !u E1. TRANS E u E1 ==> ?E2. TRANS E' u E2 /\ STRONG_EQUIV E1 E2``, 181274955Ssvnmir PROVE_TAC [PROPERTY_STAR]); 182274955Ssvnmir 183274955Ssvnmirval PROPERTY_STAR_RIGHT = store_thm ( 184274955Ssvnmir "PROPERTY_STAR_RIGHT", 185274955Ssvnmir ``!E E'. STRONG_EQUIV E E' ==> 186274955Ssvnmir !u E2. TRANS E' u E2 ==> ?E1. TRANS E u E1 /\ STRONG_EQUIV E1 E2``, 187274955Ssvnmir PROVE_TAC [PROPERTY_STAR]); 188327952Sdim 189309124Sdim(* Strong equivalence is substitutive under prefix operator. *) 190309124Sdimval STRONG_EQUIV_SUBST_PREFIX = store_thm ( 191314564Sdim "STRONG_EQUIV_SUBST_PREFIX", 192314564Sdim ``!E E'. 193314564Sdim STRONG_EQUIV E E' ==> !u. STRONG_EQUIV (prefix u E) (prefix u E')``, 194341825Sdim REPEAT GEN_TAC 195314564Sdim >> PURE_ONCE_REWRITE_TAC 196274955Ssvnmir [SPECL [``prefix (u :'b Action) E``, ``prefix (u :'b Action) E'``] PROPERTY_STAR] 197314564Sdim >> REPEAT STRIP_TAC (* 2 sub-goals here *) 198274955Ssvnmir >| [ EXISTS_TAC ``E' :('a, 'b) CCS``, 199274955Ssvnmir EXISTS_TAC ``E :('a, 'b) CCS``] 200274955Ssvnmir >> IMP_RES_TAC TRANS_PREFIX 201274955Ssvnmir >> ASM_REWRITE_TAC [PREFIX]); 202274955Ssvnmir 203274955Ssvnmir(* 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