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; 9open CCSLib CCSTheory; 10open StrongEQTheory StrongLawsTheory; 11open WeakEQTheory WeakEQLib WeakLawsTheory; 12 13val _ = new_theory "ObsCongr"; 14val _ = temp_loose_equality (); 15 16(******************************************************************************) 17(* *) 18(* Operational definition of observation congruence for CCS *) 19(* and related properties *) 20(* *) 21(******************************************************************************) 22 23(* Define the observation congruence over CCS agents expressions. *) 24val OBS_CONGR = new_definition ("OBS_CONGR", 25 ``OBS_CONGR (E :('a, 'b) CCS) (E' :('a, 'b) CCS) = 26 (!(u :'b Action). 27 (!E1. TRANS E u E1 ==> 28 ?E2. WEAK_TRANS E' u E2 /\ WEAK_EQUIV E1 E2) /\ 29 (!E2. TRANS E' u E2 ==> 30 ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2))``); 31 32val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 33 fixity = Infix (NONASSOC, 450), 34 paren_style = OnlyIfNecessary, 35 pp_elements = [HardSpace 1, TOK (UTF8.chr 0x2248 ^ UTF8.chr 0x1D9C), 36 BreakSpace (1,0)], 37 term_name = "OBS_CONGR" } 38 39val _ = TeX_notation { hol = UTF8.chr 0x2248 ^ UTF8.chr 0x1D9C, 40 TeX = ("\\HOLTokenObsCongr", 1) }; 41 42val OBS_CONGR_TRANS_LEFT = store_thm ( 43 "OBS_CONGR_TRANS_LEFT", 44 ``!E E'. OBS_CONGR (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 45 !u E1. TRANS E u E1 ==> 46 ?E2. WEAK_TRANS E' u E2 /\ WEAK_EQUIV E1 E2``, 47 PROVE_TAC [OBS_CONGR]); 48 49val OBS_CONGR_TRANS_RIGHT = store_thm ( 50 "OBS_CONGR_TRANS_RIGHT", 51 ``!E E'. OBS_CONGR (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 52 !u E2. TRANS E' u E2 ==> 53 ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2``, 54 PROVE_TAC [OBS_CONGR]); 55 56(* Prove that observation congruence implies observation equivalence. *) 57val OBS_CONGR_IMP_WEAK_EQUIV = store_thm ( 58 "OBS_CONGR_IMP_WEAK_EQUIV", ``!E E'. OBS_CONGR E E' ==> WEAK_EQUIV E E'``, 59 REPEAT GEN_TAC 60 >> ONCE_REWRITE_TAC [OBS_CONGR, WEAK_PROPERTY_STAR] 61 >> REPEAT STRIP_TAC (* 4 sub-goals here, sharing initial & end tactical *) 62 >> RES_TAC 63 >| [ Q.EXISTS_TAC `E2`, 64 Q.EXISTS_TAC `E1`, 65 IMP_RES_TAC WEAK_TRANS_IMP_EPS >> Q.EXISTS_TAC `E2`, 66 IMP_RES_TAC WEAK_TRANS_IMP_EPS >> Q.EXISTS_TAC `E1` ] 67 >> ASM_REWRITE_TAC []); 68 69val WEAK_EQUIV_STABLE_IMP_CONGR = store_thm ( 70 "WEAK_EQUIV_STABLE_IMP_CONGR", 71 ``!E E'. WEAK_EQUIV E E' /\ STABLE E /\ STABLE E' ==> OBS_CONGR E E'``, 72 REPEAT GEN_TAC 73 >> REWRITE_TAC [STABLE, OBS_CONGR] 74 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 75 >| [ (* goal 1 (of 2) *) 76 RES_TAC \\ 77 IMP_RES_TAC Action_no_tau_is_Label \\ 78 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u :'b Action) = label x``] 79 (ASSUME ``TRANS E u E1``)) \\ 80 IMP_RES_TAC 81 (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 82 (ASSUME ``WEAK_EQUIV E E'``))) \\ 83 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 84 (* goal 2 (of 2) *) 85 RES_TAC THEN IMP_RES_TAC Action_no_tau_is_Label \\ 86 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u :'b Action) = label x``] 87 (ASSUME ``TRANS E' u E2``)) \\ 88 IMP_RES_TAC 89 (CONJUNCT1 (ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 90 (ASSUME ``WEAK_EQUIV E E'``))) \\ 91 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ]); 92 93(******************************************************************************) 94(* *) 95(* Observation congruence is an equivalence relation *) 96(* *) 97(******************************************************************************) 98 99(* Observation congruence is a reflexive relation. *) 100val OBS_CONGR_REFL = store_thm ( 101 "OBS_CONGR_REFL", ``!E. OBS_CONGR E E``, 102 GEN_TAC 103 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 104 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *) 105 >> IMP_RES_TAC TRANS_IMP_WEAK_TRANS 106 >| [ (* goal 1 (of 2) *) Q.EXISTS_TAC `E1`, 107 (* goal 2 (of 2) *) Q.EXISTS_TAC `E2` ] 108 >> ASM_REWRITE_TAC [WEAK_EQUIV_REFL]); 109 110(* Observation congruence is a symmetric relation. *) 111val OBS_CONGR_SYM = store_thm ( 112 "OBS_CONGR_SYM", ``!E E'. OBS_CONGR E E' ==> OBS_CONGR E' E``, 113 REPEAT GEN_TAC 114 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 115 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing begin & end tacticals *) 116 >> RES_TAC 117 >> IMP_RES_TAC WEAK_EQUIV_SYM 118 >| [ (* goal 1 (of 2) *) Q.EXISTS_TAC `E1'`, 119 (* goal 1 (of 2) *) Q.EXISTS_TAC `E2'` ] 120 >> ASM_REWRITE_TAC []); 121 122(* Syntactic equivalence implies observation congruence. *) 123val EQUAL_IMP_OBS_CONGR = store_thm ( 124 "EQUAL_IMP_OBS_CONGR", ``!E E'. (E = E') ==> OBS_CONGR E E'``, 125 REPEAT STRIP_TAC 126 >> PURE_ASM_REWRITE_TAC [OBS_CONGR_REFL]); 127 128val OBS_CONGR_EPS = store_thm ((* NEW *) 129 "OBS_CONGR_EPS", 130 ``!E E'. OBS_CONGR E E' ==> 131 (!E1. EPS E E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2)``, 132 rpt GEN_TAC 133 >> DISCH_TAC 134 >> MATCH_MP_TAC WEAK_EQUIV_EPS 135 >> IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV); 136 137(* Lemma: in any case, `WEAK_TRANS E u E1` implies at least one real transition, 138 it then leads to `WEAK_TRANS E' u E2` on the other side. 139 140 Case 1 (u = tau): | Case 2 (u = label L) 141============================================================ 142 !E ~~c !E' | !E ~~c !E' 143 || | || || | || || || || 144 || | || || | || eps eps || 145 || tau tau || | || || || || 146 || | || || | || \/ \/ || 147 || | || || | || ?E1' ~~ ?E2' (lemma 1) 148 || \/ \/ || | || | || || 149 tau ?E1' ~~ ?E2 tau | L L L L 150 || || || || | || | || || 151 || || || || | || \/ \/ || 152 || eps eps || | || ?E2 ~~ ?E2'' || 153 || || || || | || || || || 154 || || || || | || eps eps || 155 || || || || | || || || || 156 \/ \/ \/ \/ | \/ \/ \/ \/ 157 !E1 ~~ ?E2' | !E1 ~~ ?E2''' 158 *) 159val OBS_CONGR_WEAK_TRANS = store_thm ((* NEW *) 160 "OBS_CONGR_WEAK_TRANS", 161 ``!E E'. OBS_CONGR E E' ==> 162 (!u E1. WEAK_TRANS E u E1 ==> ?E2. WEAK_TRANS E' u E2 /\ WEAK_EQUIV E1 E2)``, 163 REPEAT STRIP_TAC 164 >> Cases_on `u` (* 2 sub-goals here *) 165 >| [ (* case 1 (of 2): u = tau *) 166 IMP_RES_TAC WEAK_TRANS_TAU_IMP_TRANS_TAU \\ 167 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E E'``)) \\ 168 IMP_RES_TAC (REWRITE_RULE [WEAK_EQUIV_IS_WEAK_BISIM] 169 (Q.SPECL [`WEAK_EQUIV`, `E2`] 170 (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E1' E1``)))) \\ 171 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 172 ASSUME_TAC (Q.SPEC `E'` EPS_REFL) \\ 173 IMP_RES_TAC EPS_WEAK_EPS, 174 (* case 2 (of 2): ~(u = tau) *) 175 IMP_RES_TAC WEAK_TRANS \\ 176 IMP_RES_TAC (MATCH_MP OBS_CONGR_EPS (* lemma 1 used here *) 177 (ASSUME ``OBS_CONGR E E'``)) \\ 178 IMP_RES_TAC (CONJUNCT1 179 (PURE_ONCE_REWRITE_RULE [WEAK_PROPERTY_STAR] 180 (ASSUME ``WEAK_EQUIV E1' E2'``))) \\ 181 IMP_RES_TAC (REWRITE_RULE [WEAK_EQUIV_IS_WEAK_BISIM] 182 (Q.SPECL [`WEAK_EQUIV`, `E2''`] 183 (MATCH_MP EPS_TRANS_AUX (ASSUME ``EPS E2 E1``)))) \\ 184 Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] \\ 185 IMP_RES_TAC EPS_WEAK_EPS ]); 186 187(* Observation congruence is a transitive relation. 188 189 +-------- ~~ ------+ ---> (sub-goal 1) 190 | | || 191 !E1 ~~ ?E2 ~~ ?E3 (lemma 2) || 192 /\ /\ /\ || 193 | || || || 194 !u u u \/ 195 | || || 196 E ~~c E' ~~c E'' ==> E ~~c E'' (goal) 197 || || | || | 198 || u u || | /\ 199 u || | u !u || 200 || \/ \/ || | || 201 || ?E1 ~~ !E2 || | || 202 \/ \/ \/ || 203 (lemma 2) ?E1' ~~ ?E2' ~~ !E3 || 204 | | || 205 +--------- ~~ --------+ ---> (sub-goal 2) 206 *) 207val OBS_CONGR_TRANS = store_thm ((* NEW *) 208 "OBS_CONGR_TRANS", 209 ``!E E' E''. OBS_CONGR E E' /\ OBS_CONGR E' E'' ==> OBS_CONGR E E''``, 210 REPEAT STRIP_TAC 211 >> REWRITE_TAC [OBS_CONGR] 212 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 213 >| [ (* goal 1 (of 2) *) 214 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E E'``)) \\ 215 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *) 216 (ASSUME ``OBS_CONGR E' E''``)) \\ 217 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 218 IMP_RES_TAC WEAK_EQUIV_TRANS, 219 (* goal 2 (of 2) *) 220 IMP_RES_TAC OBS_CONGR_SYM \\ 221 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E'' E'``)) \\ 222 IMP_RES_TAC (MATCH_MP OBS_CONGR_WEAK_TRANS (* lemma 2 used here *) 223 (ASSUME ``OBS_CONGR E' E``)) \\ 224 Q.EXISTS_TAC `E2''` >> ASM_REWRITE_TAC [] \\ 225 MATCH_MP_TAC WEAK_EQUIV_SYM \\ 226 IMP_RES_TAC WEAK_EQUIV_TRANS ]); 227 228val OBS_CONGR_equivalence = store_thm ((* NEW *) 229 "OBS_CONGR_equivalence", ``equivalence OBS_CONGR``, 230 REWRITE_TAC [equivalence_def] 231 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 232 >| [ (* goal 1 (of 3) *) 233 REWRITE_TAC [reflexive_def, OBS_CONGR_REFL], 234 (* goal 2 (of 3) *) 235 REWRITE_TAC [symmetric_def] \\ 236 REPEAT GEN_TAC \\ 237 EQ_TAC >> REWRITE_TAC [OBS_CONGR_SYM], 238 (* goal 3 (of 3) *) 239 REWRITE_TAC [transitive_def, OBS_CONGR_TRANS] ]); 240 241(******************************************************************************) 242(* *) 243(* Substitutive properties of observation congruence *) 244(* *) 245(******************************************************************************) 246 247(* Proposition 6 (Milner's book, page 154). *) 248val PROP6 = store_thm ("PROP6", 249 ``!E E'. WEAK_EQUIV E E' ==> !u. OBS_CONGR (prefix u E) (prefix u E')``, 250 REPEAT GEN_TAC 251 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 252 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 253 >| [ (* goal 1 (of 2) *) 254 IMP_RES_TAC TRANS_PREFIX \\ 255 Q.EXISTS_TAC `E'` \\ 256 ASM_REWRITE_TAC [WEAK_TRANS] \\ 257 EXISTS_TAC ``prefix (u :'b Action) E'`` \\ 258 Q.EXISTS_TAC `E'` \\ 259 ASM_REWRITE_TAC [EPS_REFL, PREFIX], 260 (* goal 2 (of 2) *) 261 IMP_RES_TAC TRANS_PREFIX \\ 262 Q.EXISTS_TAC `E` \\ 263 ASM_REWRITE_TAC [WEAK_TRANS] \\ 264 EXISTS_TAC ``prefix (u :'b Action) E`` \\ 265 Q.EXISTS_TAC `E` \\ 266 ASM_REWRITE_TAC [EPS_REFL, PREFIX] ]); 267 268(* Observation congruence is substitutive under the prefix operator. *) 269val OBS_CONGR_SUBST_PREFIX = store_thm ( 270 "OBS_CONGR_SUBST_PREFIX", 271 ``!E E'. OBS_CONGR E E' ==> !u. OBS_CONGR (prefix u E) (prefix u E')``, 272 REPEAT STRIP_TAC 273 >> IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV 274 >> IMP_RES_TAC PROP6 275 >> ASM_REWRITE_TAC []); 276 277(* Observation congruence is substitutive under binary summation. *) 278val OBS_CONGR_PRESD_BY_SUM = store_thm ( 279 "OBS_CONGR_PRESD_BY_SUM", 280 ``!E1 E1' E2 E2'. OBS_CONGR E1 E1' /\ OBS_CONGR E2 E2' ==> 281 OBS_CONGR (sum E1 E2) (sum E1' E2')``, 282 rpt STRIP_TAC 283 >> REWRITE_TAC [OBS_CONGR] 284 >> rpt STRIP_TAC (* 2 sub-goals here *) 285 >| [ (* goal 1 (of 2) *) 286 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 287 [ (* goal 1.1 (of 2) *) 288 IMP_RES_TAC OBS_CONGR_TRANS_LEFT \\ 289 Q.EXISTS_TAC `E2''` >> art [] \\ 290 MATCH_MP_TAC WEAK_SUM1 >> art [], 291 (* goal 1.2 (of 2) *) 292 IMP_RES_TAC OBS_CONGR_TRANS_LEFT \\ 293 Q.EXISTS_TAC `E2''` >> art [] \\ 294 MATCH_MP_TAC WEAK_SUM2 >> art [] ], 295 (* goal 2 (of 2) *) 296 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 297 [ (* goal 2.1 (of 2) *) 298 IMP_RES_TAC OBS_CONGR_TRANS_RIGHT \\ 299 Q.EXISTS_TAC `E1''` >> art [] \\ 300 MATCH_MP_TAC WEAK_SUM1 >> art [], 301 (* goal 2.2 (of 2) *) 302 IMP_RES_TAC OBS_CONGR_TRANS_RIGHT \\ 303 Q.EXISTS_TAC `E1''` >> art [] \\ 304 MATCH_MP_TAC WEAK_SUM2 >> art [] ] ]); 305 306(* Observation congruence is substitutive under binary summation on the left: 307 |- !E E'. OBS_CONGR E E' ==> !E''. OBS_CONGR (sum E'' E) (sum E'' E') 308 *) 309val OBS_CONGR_SUBST_SUM_L = save_thm ( 310 "OBS_CONGR_SUBST_SUM_L", 311 Q_GENL [`E`, `E'`] 312 (DISCH ``OBS_CONGR E E'`` 313 (Q.GEN `E''` 314 (MATCH_MP OBS_CONGR_PRESD_BY_SUM 315 (CONJ (Q.SPEC `E''` OBS_CONGR_REFL) 316 (ASSUME ``OBS_CONGR E E'``)))))); 317 318(* Observation congruence is substitutive under binary summation on the right: 319 |- !E E'. OBS_CONGR E E' ==> !E''. OBS_CONGR (sum E E'') (sum E' E'') 320 *) 321val OBS_CONGR_SUBST_SUM_R = save_thm ( 322 "OBS_CONGR_SUBST_SUM_R", 323 Q_GENL [`E`, `E'`] 324 (DISCH ``OBS_CONGR E E'`` 325 (Q.GEN `E''` 326 (MATCH_MP OBS_CONGR_PRESD_BY_SUM 327 (CONJ (ASSUME ``OBS_CONGR E E'``) 328 (Q.SPEC `E''` OBS_CONGR_REFL)))))); 329 330(* Observation congruence is preserved by parallel composition. *) 331val OBS_CONGR_PRESD_BY_PAR = store_thm ( 332 "OBS_CONGR_PRESD_BY_PAR", 333 ``!E1 E1' E2 E2'. OBS_CONGR E1 E1' /\ OBS_CONGR E2 E2' ==> 334 OBS_CONGR (par E1 E2) (par E1' E2')``, 335 REPEAT STRIP_TAC 336 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 337 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 338 >| [ (* goal 1 (of 2) *) 339 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 340 [ (* goal 1.1 (of 3) *) 341 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] 342 (ASSUME ``OBS_CONGR E1 E1'``)) \\ 343 ASSUME_TAC (CONJUNCT1 344 (Q.SPEC `E2'` 345 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E1' u E2''``)))) \\ 346 EXISTS_TAC ``par E2'' E2'`` \\ 347 ASM_REWRITE_TAC 348 [OE_TRANS (Q.SPEC `E2` 349 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 350 (ASSUME ``WEAK_EQUIV E1''' E2''``))) 351 (Q.SPEC `E2''` 352 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 353 (MATCH_MP OBS_CONGR_IMP_WEAK_EQUIV 354 (ASSUME ``OBS_CONGR E2 E2'``))))], 355 (* goal 1.2 (of 3) *) 356 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] 357 (ASSUME ``OBS_CONGR E2 E2'``)) \\ 358 ASSUME_TAC (CONJUNCT2 359 (Q.SPEC `E1'` 360 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E2' u E2''``)))) \\ 361 EXISTS_TAC ``par E1' E2''`` \\ 362 ASM_REWRITE_TAC 363 [OE_TRANS (Q.SPEC `E1'''` 364 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 365 (MATCH_MP OBS_CONGR_IMP_WEAK_EQUIV 366 (ASSUME ``OBS_CONGR E1 E1'``)))) 367 (Q.SPEC `E1'` 368 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 369 (ASSUME ``WEAK_EQUIV E1''' E2''``)))], 370 (* goal 1.3 (of 3) *) 371 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E1 E1'``)) \\ 372 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E2 E2'``)) \\ 373 EXISTS_TAC ``par E2''' E2''''`` \\ 374 ASM_REWRITE_TAC 375 [OE_TRANS (Q.SPEC `E2''` 376 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 377 (ASSUME ``WEAK_EQUIV E1''' E2'''``))) 378 (Q.SPEC `E2'''` 379 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 380 (ASSUME ``WEAK_EQUIV E2'' E2''''``)))] \\ 381 PURE_ONCE_REWRITE_TAC [WEAK_TRANS] \\ 382 STRIP_ASSUME_TAC 383 (REWRITE_RULE [WEAK_TRANS] 384 (ASSUME ``WEAK_TRANS E1' (label l) E2'''``)) \\ 385 STRIP_ASSUME_TAC 386 (REWRITE_RULE [WEAK_TRANS] 387 (ASSUME ``WEAK_TRANS E2' (label (COMPL l)) E2''''``)) \\ 388 EXISTS_TAC ``par E1'''' E1'''''`` \\ 389 EXISTS_TAC ``par E2''''' E2''''''`` \\ 390 REWRITE_TAC 391 [MATCH_MP EPS_PAR_PAR 392 (CONJ (ASSUME ``EPS E1' E1''''``) 393 (ASSUME ``EPS E2' E1'''''``)), 394 MATCH_MP EPS_PAR_PAR 395 (CONJ (ASSUME ``EPS E2''''' E2'''``) 396 (ASSUME ``EPS E2'''''' E2''''``))] \\ 397 MATCH_MP_TAC PAR3 \\ 398 EXISTS_TAC ``l: 'b Label`` >> ASM_REWRITE_TAC [] ], 399 (* goal 2 (of 2) *) 400 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 401 [ (* goal 2.1 (of 3) *) 402 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] (ASSUME ``OBS_CONGR E1 E1'``)) \\ 403 ASSUME_TAC (CONJUNCT1 404 (Q.SPEC `E2` 405 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E1 u E1'''``)))) \\ 406 EXISTS_TAC ``par E1''' E2`` \\ 407 ASM_REWRITE_TAC 408 [OE_TRANS (Q.SPEC `E2` 409 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 410 (ASSUME ``WEAK_EQUIV E1''' E1''``))) 411 (Q.SPEC `E1''` 412 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 413 (MATCH_MP OBS_CONGR_IMP_WEAK_EQUIV 414 (ASSUME ``OBS_CONGR E2 E2'``))))], 415 (* goal 2.2 (of 3) *) 416 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] 417 (ASSUME ``OBS_CONGR E2 E2'``)) \\ 418 ASSUME_TAC (CONJUNCT2 419 (Q.SPEC `E1` 420 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E2 u E1'''``)))) \\ 421 EXISTS_TAC ``par E1 E1'''`` \\ 422 ASM_REWRITE_TAC 423 [OE_TRANS (Q.SPEC `E1'''` 424 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 425 (MATCH_MP OBS_CONGR_IMP_WEAK_EQUIV 426 (ASSUME ``OBS_CONGR E1 E1'``)))) 427 (Q.SPEC `E1'` 428 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 429 (ASSUME ``WEAK_EQUIV E1''' E1''``)))], 430 (* goal 2.3 (of 3) *) 431 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] 432 (ASSUME ``OBS_CONGR E1 E1'``)) \\ 433 IMP_RES_TAC (REWRITE_RULE [OBS_CONGR] 434 (ASSUME ``OBS_CONGR E2 E2'``)) \\ 435 EXISTS_TAC ``par E1''' E1''''`` \\ 436 ASM_REWRITE_TAC 437 [OE_TRANS (Q.SPEC `E1''''` 438 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 439 (ASSUME ``WEAK_EQUIV E1''' E1''``))) 440 (Q.SPEC `E1''` 441 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 442 (ASSUME ``WEAK_EQUIV E1'''' E2'''``)))] \\ 443 PURE_ONCE_REWRITE_TAC [WEAK_TRANS] \\ 444 STRIP_ASSUME_TAC 445 (REWRITE_RULE [WEAK_TRANS] 446 (ASSUME ``WEAK_TRANS E1 (label l) E1'''``)) \\ 447 STRIP_ASSUME_TAC 448 (REWRITE_RULE [WEAK_TRANS] 449 (ASSUME ``WEAK_TRANS E2 (label (COMPL l)) E1''''``)) \\ 450 EXISTS_TAC ``par E1''''' E1''''''`` \\ 451 EXISTS_TAC ``par E2'''' E2'''''`` \\ 452 REWRITE_TAC 453 [MATCH_MP EPS_PAR_PAR 454 (CONJ (ASSUME ``EPS E1 E1'''''``) 455 (ASSUME ``EPS E2 E1''''''``)), 456 MATCH_MP EPS_PAR_PAR 457 (CONJ (ASSUME ``EPS E2'''' E1'''``) 458 (ASSUME ``EPS E2''''' E1''''``))] \\ 459 MATCH_MP_TAC PAR3 \\ 460 EXISTS_TAC ``l: 'b Label`` >> ASM_REWRITE_TAC [] ] ]); 461 462(* Observation congruence is substitutive under parallel operator on the left: 463 |- !E E'. OBS_CONGR E E' ==> (!E''. OBS_CONGR (par E'' E) (par E'' E')) 464 *) 465val OBS_CONGR_SUBST_PAR_L = save_thm ( 466 "OBS_CONGR_SUBST_PAR_L", 467 Q_GENL [`E`, `E'`] 468 (DISCH ``OBS_CONGR E E'`` 469 (Q.GEN `E''` 470 (MATCH_MP OBS_CONGR_PRESD_BY_PAR 471 (CONJ (Q.SPEC `E''` OBS_CONGR_REFL) 472 (ASSUME ``OBS_CONGR E E'``)))))); 473 474(* Observation congruence is substitutive under parallel operator on the right: 475 |- !E E'. OBS_CONGR E E' ==> (!E''. OBS_CONGR (par E E'') (par E' E'')) 476 *) 477val OBS_CONGR_SUBST_PAR_R = save_thm ( 478 "OBS_CONGR_SUBST_PAR_R", 479 Q_GENL [`E`, `E'`] 480 (DISCH ``OBS_CONGR E E'`` 481 (Q.GEN `E''` 482 (MATCH_MP OBS_CONGR_PRESD_BY_PAR 483 (CONJ (ASSUME ``OBS_CONGR E E'``) 484 (Q.SPEC `E''` OBS_CONGR_REFL)))))); 485 486(* Observation congruence is substitutive under the restriction operator. *) 487val OBS_CONGR_SUBST_RESTR = store_thm ( 488 "OBS_CONGR_SUBST_RESTR", 489 ``!E E'. OBS_CONGR E E' ==> !L. OBS_CONGR (restr L E) (restr L E')``, 490 REPEAT GEN_TAC 491 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 492 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 493 >| [ (* goal 1 (of 2) *) 494 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 495 [ (* goal 1.1 (of 2) *) 496 RES_TAC \\ 497 ASSUME_TAC 498 (MATCH_MP WEAK_RESTR_tau 499 (REWRITE_RULE [ASSUME ``(u :'b Action) = tau``] 500 (ASSUME ``WEAK_TRANS E' u E2``))) \\ 501 EXISTS_TAC ``restr (L :'b Label set) E2`` \\ 502 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [], 503 (* goal 1.2 (of 2) *) 504 RES_TAC \\ 505 ASSUME_TAC 506 (MATCH_MP WEAK_RESTR_label 507 (LIST_CONJ [ASSUME ``~((l :'b Label) IN L)``, 508 ASSUME ``~((COMPL (l :'b Label)) IN L)``, 509 REWRITE_RULE [ASSUME ``(u :'b Action) = label l``] 510 (ASSUME ``WEAK_TRANS E' u E2``)])) \\ 511 EXISTS_TAC ``restr (L :'b Label set) E2`` \\ 512 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [] ], 513 (* goal 2 (of 2) *) 514 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 515 [ (* goal 2.1 (of 2) *) 516 RES_TAC \\ 517 ASSUME_TAC 518 (MATCH_MP WEAK_RESTR_tau 519 (REWRITE_RULE [ASSUME ``(u :'b Action) = tau``] 520 (ASSUME ``WEAK_TRANS E u E1``))) \\ 521 EXISTS_TAC ``restr (L :'b Label set) E1`` \\ 522 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [], 523 (* goal 2.2 (of 2) *) 524 RES_TAC \\ 525 ASSUME_TAC 526 (MATCH_MP WEAK_RESTR_label 527 (LIST_CONJ [ASSUME ``~((l: 'b Label) IN L)``, 528 ASSUME ``~((COMPL (l :'b Label)) IN L)``, 529 REWRITE_RULE [ASSUME ``(u :'b Action) = label l``] 530 (ASSUME ``WEAK_TRANS E u E1``)])) \\ 531 EXISTS_TAC ``restr (L :'b Label set) E1`` \\ 532 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [] ] ]); 533 534(* Observation congruence is substitutive under the relabelling operator. *) 535val OBS_CONGR_SUBST_RELAB = store_thm ( 536 "OBS_CONGR_SUBST_RELAB", 537 ``!E E'. OBS_CONGR E E' ==> !rf. OBS_CONGR (relab E rf) (relab E' rf)``, 538 REPEAT GEN_TAC 539 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 540 >> REPEAT STRIP_TAC (* 2 sub-goals here, sharing start&end tacticals *) 541 >> IMP_RES_TAC TRANS_RELAB 542 >> RES_TAC 543 >| [ (* goal 1 (of 2) *) 544 ASSUME_TAC (MATCH_MP WEAK_RELAB_rf 545 (ASSUME ``WEAK_TRANS E' u' E2``)) \\ 546 EXISTS_TAC ``relab E2 rf``, 547 (* goal 2 (of 2) *) 548 ASSUME_TAC (MATCH_MP WEAK_RELAB_rf 549 (ASSUME ``WEAK_TRANS E u' E1``)) \\ 550 EXISTS_TAC ``relab E1 rf`` ] 551 >> IMP_RES_TAC WEAK_EQUIV_SUBST_RELAB 552 >> ASM_REWRITE_TAC []); 553 554(******************************************************************************) 555(* *) 556(* Relationship between strong equivalence and observation congruence *) 557(* *) 558(******************************************************************************) 559 560(* Prove that strong equivalence implies observation congruence. *) 561val STRONG_IMP_OBS_CONGR = store_thm ( 562 "STRONG_IMP_OBS_CONGR", ``!E E'. STRONG_EQUIV E E' ==> OBS_CONGR E E'``, 563 REPEAT GEN_TAC 564 >> PURE_ONCE_REWRITE_TAC [PROPERTY_STAR, OBS_CONGR] 565 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 566 >| [ (* goal 1 (of 2) *) 567 RES_TAC \\ 568 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 569 IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\ 570 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 571 (* goal 2 (of 2) *) 572 RES_TAC \\ 573 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 574 IMP_RES_TAC STRONG_IMP_WEAK_EQUIV \\ 575 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ]); 576 577(* `EPS E E1` implies zero or more tau transitions, and this leads to 578 zero or at least one tau transition on the other side, which implies 579 `EPS E' E2` in any case. 580 581 (Base case) | (Induct case) 582 ========================================== 583 !E ~~c !E' | !E ~~c !E' 584 | | | || || || 585 = = | eps eps || 586 | | | || || || 587 E ~~ ?E' | \/ \/ || 588 | E1 ~~ ?E2 eps 589 | | || || 590 | tau tau || 591 | | || || 592 | \/ \/ \/ 593 | E1' ~~ ?E2' 594 *) 595val OBS_CONGR_EPS = store_thm ((* NEW *) 596 "OBS_CONGR_EPS", 597 ``!E E'. OBS_CONGR E E' ==> 598 !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ WEAK_EQUIV E1 E2``, 599 REPEAT STRIP_TAC 600 >> PAT_X_ASSUM ``OBS_CONGR E E'`` MP_TAC 601 >> POP_ASSUM MP_TAC 602 >> Q.SPEC_TAC (`E1`, `E1`) 603 >> Q.SPEC_TAC (`E`, `E`) 604 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 605 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 606 >| [ (* goal 1 (of 2) *) 607 Q.EXISTS_TAC `E'` >> RW_TAC std_ss [EPS_REFL] \\ 608 IMP_RES_TAC OBS_CONGR_IMP_WEAK_EQUIV, 609 (* goal 2 (of 2) *) 610 RES_TAC \\ 611 IMP_RES_TAC WEAK_EQUIV_TRANS_tau \\ 612 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 613 IMP_RES_TAC EPS_TRANS ]); 614 615val OBS_CONGR_EPS' = store_thm ((* NEW *) 616 "OBS_CONGR_EPS'", 617 ``!E E'. OBS_CONGR E E' ==> 618 !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 619 rpt GEN_TAC >> DISCH_TAC 620 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP OBS_CONGR_SYM)) 621 >> IMP_RES_TAC OBS_CONGR_EPS 622 >> POP_ASSUM MP_TAC 623 >> rpt STRIP_TAC 624 >> RES_TAC 625 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 626 >> IMP_RES_TAC WEAK_EQUIV_SYM); 627 628val OBS_CONGR_WEAK_TRANS = store_thm ((* NEW *) 629 "OBS_CONGR_WEAK_TRANS", 630 ``!E E'. OBS_CONGR E E' ==> 631 !u E1. WEAK_TRANS E u E1 ==> ?E2. WEAK_TRANS E' u E2 /\ WEAK_EQUIV E1 E2``, 632 REPEAT STRIP_TAC 633 >> Cases_on `u` (* 2 sub-goals here *) 634 >| [ (* goal 1 (of 2) *) 635 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS_TAU])) \\ 636 IMP_RES_TAC OBS_CONGR_TRANS_LEFT \\ 637 IMP_RES_TAC WEAK_EQUIV_EPS \\ 638 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 639 MATCH_MP_TAC EPS_WEAK_EPS \\ 640 take [`E'`, `E2`] >> ASM_REWRITE_TAC [EPS_REFL], 641 (* goal 2 (of 2) *) 642 POP_ASSUM (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 643 IMP_RES_TAC OBS_CONGR_EPS \\ 644 IMP_RES_TAC WEAK_EQUIV_TRANS_label \\ 645 IMP_RES_TAC WEAK_EQUIV_EPS \\ 646 Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] \\ 647 MATCH_MP_TAC EPS_WEAK_EPS \\ 648 take [`E2'`, `E2''`] >> ASM_REWRITE_TAC [] ]); 649 650val OBS_CONGR_WEAK_TRANS' = store_thm ((* NEW *) 651 "OBS_CONGR_WEAK_TRANS'", 652 ``!E E'. OBS_CONGR E E' ==> 653 !u E2. WEAK_TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2``, 654 REPEAT GEN_TAC 655 >> DISCH_TAC 656 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP OBS_CONGR_SYM)) 657 >> IMP_RES_TAC OBS_CONGR_WEAK_TRANS 658 >> POP_ASSUM MP_TAC 659 >> rpt STRIP_TAC 660 >> RES_TAC 661 >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] 662 >> IMP_RES_TAC WEAK_EQUIV_SYM); 663 664(******************************************************************************) 665(* *) 666(* Proving OBS_CONGR by constructing a WEAK_BISIM ! *) 667(* *) 668(******************************************************************************) 669 670(* This beautiful result is learnt from Prof. Davide Sangiorgi *) 671val OBS_CONGR_BY_WEAK_BISIM = store_thm ( 672 "OBS_CONGR_BY_WEAK_BISIM", 673 ``!Wbsm. WEAK_BISIM Wbsm ==> 674 !E E'. 675 (!u. 676 (!E1. TRANS E u E1 ==> 677 (?E2. WEAK_TRANS E' u E2 /\ Wbsm E1 E2)) /\ 678 (!E2. TRANS E' u E2 ==> 679 (?E1. WEAK_TRANS E u E1 /\ Wbsm E1 E2))) ==> OBS_CONGR E E'``, 680 rpt STRIP_TAC 681 >> REWRITE_TAC [OBS_CONGR] 682 >> REWRITE_TAC [WEAK_EQUIV] 683 >> GEN_TAC 684 >> CONJ_TAC (* 2 sub-goals here *) 685 >| [ (* goal 1 (of 2) *) 686 rpt STRIP_TAC >> RES_TAC \\ 687 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 688 Q.EXISTS_TAC `Wbsm` >> ASM_REWRITE_TAC [], 689 (* goal 2 (of 2) *) 690 rpt STRIP_TAC >> RES_TAC \\ 691 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 692 Q.EXISTS_TAC `Wbsm` >> ASM_REWRITE_TAC [] ]); 693 694val _ = export_theory (); 695val _ = html_theory "ObsCongr"; 696 697(* last updated: Jun 20, 2017 *) 698