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 CCSLib CCSTheory; 9open StrongEQTheory StrongEQLib StrongLawsTheory; 10open WeakEQTheory WeakEQLib WeakLawsTheory; 11open ObsCongrTheory ObsCongrLib; 12 13val _ = new_theory "ObsCongrLaws"; 14 15(******************************************************************************) 16(* *) 17(* Basic laws of observation congruence for binary summation *) 18(* through strong equivalence *) 19(* *) 20(******************************************************************************) 21 22(* Prove OBS_SUM_IDENT_R: |- !E. OBS_CONGR (sum E nil) E *) 23val OBS_SUM_IDENT_R = save_thm ( 24 "OBS_SUM_IDENT_R", 25 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_IDENT_R); 26 27(* Prove OBS_SUM_IDENT_L: |- !E. OBS_CONGR (sum nil E) E *) 28val OBS_SUM_IDENT_L = save_thm ( 29 "OBS_SUM_IDENT_L", 30 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_IDENT_L); 31 32(* Prove OBS_SUM_IDEMP: |- !E. OBS_CONGR (sum E E) E *) 33val OBS_SUM_IDEMP = save_thm ( 34 "OBS_SUM_IDEMP", 35 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_IDEMP); 36 37(* Prove OBS_SUM_COMM: |- !E E'. OBS_CONGR (sum E E') (sum E' E) *) 38val OBS_SUM_COMM = save_thm ( 39 "OBS_SUM_COMM", 40 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_COMM); 41 42(* Prove OBS_SUM_ASSOC_R: 43 |- !E E' E''. OBS_CONGR (sum (sum E E') E'') (sum E (sum E' E'')) 44 *) 45val OBS_SUM_ASSOC_R = save_thm ( 46 "OBS_SUM_ASSOC_R", 47 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_ASSOC_R); 48 49(* Prove OBS_SUM_ASSOC_L: 50 |- !E E' E''. OBS_CONGR (sum E (sum E' E'')) (sum (sum E E') E'') 51 *) 52val OBS_SUM_ASSOC_L = save_thm ( 53 "OBS_SUM_ASSOC_L", 54 STRONG_IMP_OBS_CONGR_RULE STRONG_SUM_ASSOC_L); 55 56(******************************************************************************) 57(* *) 58(* Basic laws of observation congruence for the parallel *) 59(* operator through strong equivalence *) 60(* *) 61(******************************************************************************) 62 63(* Prove OBS_PAR_IDENT_R: |- !E. OBS_CONGR (par E nil) E *) 64val OBS_PAR_IDENT_R = save_thm ( 65 "OBS_PAR_IDENT_R", 66 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_IDENT_R); 67 68(* Prove OBS_PAR_IDENT_L: |- !E. OBS_CONGR (par nil E) E *) 69val OBS_PAR_IDENT_L = save_thm ( 70 "OBS_PAR_IDENT_L", 71 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_IDENT_L); 72 73(* Prove OBS_PAR_COMM: |- !E E'. OBS_CONGR (par E E') (par E' E) *) 74val OBS_PAR_COMM = save_thm ( 75 "OBS_PAR_COMM", 76 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_COMM); 77 78(* Prove OBS_PAR_ASSOC: 79 |- !E E' E''. OBS_CONGR (par (par E E') E'') (par E (par E' E'')) 80 *) 81val OBS_PAR_ASSOC = save_thm ( 82 "OBS_PAR_ASSOC", 83 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_ASSOC); 84 85(* Prove OBS_PAR_PREF_TAU: 86 |- !u E E'. 87 OBS_CONGR (par (prefix u E) (prefix tau E')) 88 (sum (prefix u (par E (prefix tau E'))) 89 (prefix tau (par (prefix u E) E'))) 90 *) 91val OBS_PAR_PREF_TAU = save_thm ( 92 "OBS_PAR_PREF_TAU", 93 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_PREF_TAU); 94 95(* Prove OBS_PAR_TAU_PREF: 96 |- !E u E'. 97 OBS_CONGR (par (prefix tau E) (prefix u E')) 98 (sum (prefix tau (par E (prefix u E'))) 99 (prefix u (par (prefix tau E) E'))) 100 *) 101val OBS_PAR_TAU_PREF = save_thm ( 102 "OBS_PAR_TAU_PREF", 103 STRONG_IMP_OBS_CONGR_RULE STRONG_PAR_TAU_PREF); 104 105(* Prove OBS_PAR_TAU_TAU: 106 |- !E E'. 107 OBS_CONGR (par (prefix tau E) (prefix tau E')) 108 (sum (prefix tau (par E (prefix tau E'))) 109 (prefix tau (par (prefix tau E) E'))) 110 *) 111val OBS_PAR_TAU_TAU = save_thm ( 112 "OBS_PAR_TAU_TAU", Q.SPEC `tau` OBS_PAR_PREF_TAU); 113 114(* Prove OBS_PAR_PREF_NO_SYNCR: 115 |- !l l'. 116 ~(l = COMPL l') ==> 117 (!E E'. 118 OBS_CONGR (par (prefix (label l) E) (prefix (label l') E')) 119 (sum (prefix (label l) (par E (prefix (label l') E'))) 120 (prefix (label l') (par (prefix (label l) E) E')))) 121 *) 122val OBS_PAR_PREF_NO_SYNCR = save_thm ( 123 "OBS_PAR_PREF_NO_SYNCR", 124 STRIP_FORALL_RULE ((DISCH ``~((l :'b Label) = COMPL l')``) o 125 (STRIP_FORALL_RULE (MATCH_MP STRONG_IMP_OBS_CONGR)) o 126 UNDISCH) 127 STRONG_PAR_PREF_NO_SYNCR); 128 129(* Prove OBS_PAR_PREF_SYNCR: 130 |- !l l'. 131 (l = COMPL l') ==> 132 (!E E'. 133 OBS_CONGR (par (prefix (label l) E) (prefix (label l') E')) 134 (sum 135 (sum (prefix (label l) (par E (prefix (label l') E'))) 136 (prefix (label l') (par (prefix (label l) E) E'))) 137 (prefix tau (par E E')))) 138 *) 139val OBS_PAR_PREF_SYNCR = save_thm ( 140 "OBS_PAR_PREF_SYNCR", 141 STRIP_FORALL_RULE ((DISCH ``((l :'b Label) = COMPL l')``) o 142 (STRIP_FORALL_RULE (MATCH_MP STRONG_IMP_OBS_CONGR)) o 143 UNDISCH) 144 STRONG_PAR_PREF_SYNCR); 145 146(* The expansion law for observation congruence: 147 |- !f n f' m. 148 (!i. i <= n ==> Is_Prefix (f i)) /\ (!j. j <= m ==> Is_Prefix (f' j)) 149 ==> 150 OBS_CONGR 151 (par (SIGMA f n) (SIGMA f' m)) 152 (sum 153 (sum 154 (SIGMA (\i. prefix (PREF_ACT (f i)) (par (PREF_PROC (f i)) (SIGMA f' m))) n) 155 (SIGMA (\j. prefix (PREF_ACT (f' j)) (par (SIGMA f n) (PREF_PROC (f' j)))) m)) 156 (ALL_SYNC f n f' m)) 157 *) 158val OBS_EXPANSION_LAW = save_thm ( 159 "OBS_EXPANSION_LAW", 160 STRIP_FORALL_RULE (DISCH_ALL o (MATCH_MP STRONG_IMP_OBS_CONGR) o UNDISCH) 161 STRONG_EXPANSION_LAW); 162 163(******************************************************************************) 164(* *) 165(* Basic laws of observation congruence for the restriction *) 166(* operator through strong equivalence *) 167(* *) 168(******************************************************************************) 169 170(* Prove OBS_RESTR_NIL: |- !L. OBS_CONGR (restr L nil) nil *) 171val OBS_RESTR_NIL = save_thm ( 172 "OBS_RESTR_NIL", 173 STRONG_IMP_OBS_CONGR_RULE STRONG_RESTR_NIL); 174 175(* Prove OBS_RESTR_SUM: 176 |- !E E' L. OBS_CONGR (restr L (sum E E')) (sum (restr L E) (restr L E')) 177 *) 178val OBS_RESTR_SUM = save_thm ( 179 "OBS_RESTR_SUM", 180 STRONG_IMP_OBS_CONGR_RULE STRONG_RESTR_SUM); 181 182(* Prove OBS_RESTR_PREFIX_TAU: 183 |- !E L. OBS_CONGR (restr (prefix tau E) L) (prefix tau (restr E L)) 184 *) 185val OBS_RESTR_PREFIX_TAU = save_thm ( 186 "OBS_RESTR_PREFIX_TAU", 187 STRONG_IMP_OBS_CONGR_RULE STRONG_RESTR_PREFIX_TAU); 188 189(* Prove OBS_RESTR_PR_LAB_NIL: 190 |- !l L. 191 l IN L \/ (COMPL l) IN L ==> 192 (!E. OBS_CONGR (restr L (prefix (label l) E)) nil) 193 *) 194val OBS_RESTR_PR_LAB_NIL = save_thm ( 195 "OBS_RESTR_PR_LAB_NIL", 196 ((Q_GENL [`l`, `L`]) o 197 (DISCH ``(l :'b Label) IN L \/ (COMPL l) IN L``) o 198 (Q.GEN `E`) o 199 UNDISCH) 200 (IMP_TRANS 201 (DISCH ``(l :'b Label) IN L \/ (COMPL l) IN L`` 202 (Q.SPEC `E` 203 (UNDISCH 204 (Q.SPECL [`l`, `L`] STRONG_RESTR_PR_LAB_NIL)))) 205 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, ``nil``] 206 STRONG_IMP_OBS_CONGR))); 207 208(* Prove OBS_RESTR_PREFIX_LABEL: 209 |- !l L. 210 ~l IN L /\ ~(COMPL l) IN L ==> 211 (!E. OBS_CONGR (restr (prefix (label l) E) L) (prefix (label l) (restr E L))) 212 *) 213val OBS_RESTR_PREFIX_LABEL = save_thm ( 214 "OBS_RESTR_PREFIX_LABEL", 215 ((Q_GENL [`l`, `L`]) o 216 (DISCH ``~((l :'b Label) IN L) /\ ~((COMPL l) IN L)``) o 217 (Q.GEN `E`) o 218 UNDISCH) 219 (IMP_TRANS 220 (DISCH ``~((l :'b Label) IN L) /\ ~((COMPL l) IN L)`` 221 (Q.SPEC `E` 222 (UNDISCH 223 (Q.SPECL [`l`, `L`] STRONG_RESTR_PREFIX_LABEL)))) 224 (SPECL [``restr (L :'b Label set) (prefix (label l) E)``, 225 ``prefix (label (l :'b Label)) (restr L E)``] 226 STRONG_IMP_OBS_CONGR))); 227 228(******************************************************************************) 229(* *) 230(* Basic laws of observation congruence for the recursion *) 231(* operator through strong equivalence *) 232(* *) 233(******************************************************************************) 234 235(* The unfolding law: 236 OBS_UNFOLDING: |- !X E. OBS_CONGR (rec X E) (CCS_Subst E (rec X E) X) 237 *) 238val OBS_UNFOLDING = save_thm ( 239 "OBS_UNFOLDING", 240 STRONG_IMP_OBS_CONGR_RULE STRONG_UNFOLDING); 241 242(* Prove the theorem OBS_PREF_REC_EQUIV: 243 |- !u s v. 244 OBS_CONGR 245 (prefix u (rec s (prefix v (prefix u (var s))))) 246 (rec s (prefix u (prefix v (var s)))) 247 *) 248val OBS_PREF_REC_EQUIV = save_thm ( 249 "OBS_PREF_REC_EQUIV", 250 STRONG_IMP_OBS_CONGR_RULE STRONG_PREF_REC_EQUIV); 251 252(******************************************************************************) 253(* *) 254(* Basic laws of observation congruence for the relabelling *) 255(* operator through strong equivalence *) 256(* *) 257(******************************************************************************) 258 259(* Prove OBS_RELAB_NIL: |- !rf. OBS_CONGR (relab nil rf) nil *) 260val OBS_RELAB_NIL = save_thm ( 261 "OBS_RELAB_NIL", 262 STRONG_IMP_OBS_CONGR_RULE STRONG_RELAB_NIL); 263 264(* Prove OBS_RELAB_SUM: 265 |- !E E' rf. OBS_CONGR (relab (sum E E') rf) (sum (relab E rf) (relab E' rf)) 266 *) 267val OBS_RELAB_SUM = save_thm ( 268 "OBS_RELAB_SUM", 269 STRONG_IMP_OBS_CONGR_RULE STRONG_RELAB_SUM); 270 271(* Prove OBS_RELAB_PREFIX: 272 |- !u E labl. 273 OBS_CONGR (relab (prefix u E) (RELAB labl)) 274 (prefix (relabel (RELAB labl) u) (relab E (RELAB labl))) 275 *) 276val OBS_RELAB_PREFIX = save_thm ( 277 "OBS_RELAB_PREFIX", 278 STRONG_IMP_OBS_CONGR_RULE STRONG_RELAB_PREFIX); 279 280(******************************************************************************) 281(* *) 282(* tau-laws for observation congruence (and the same tau-laws *) 283(* for observation equivalence derived through the congruence) *) 284(* *) 285(******************************************************************************) 286 287(* Prove TAU1: 288 |- !u E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E) 289 *) 290val TAU1 = store_thm ("TAU1", 291 ``!(u :'b Action) E. OBS_CONGR (prefix u (prefix tau E)) (prefix u E)``, 292 REPEAT GEN_TAC 293 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 294 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 295 >| [ (* goal 1 (of 2) *) 296 IMP_RES_TAC TRANS_PREFIX \\ 297 Q.EXISTS_TAC `E` \\ 298 ASM_REWRITE_TAC [WEAK_TRANS, TAU_WEAK] \\ 299 EXISTS_TAC ``prefix (u :'b Action) E`` \\ 300 Q.EXISTS_TAC `E` \\ 301 ASM_REWRITE_TAC [EPS_REFL, PREFIX], 302 (* goal 2 (of 2) *) 303 IMP_RES_TAC TRANS_PREFIX \\ 304 EXISTS_TAC ``prefix (tau :'b Action) E2`` \\ 305 ASM_REWRITE_TAC [WEAK_TRANS, TAU_WEAK] \\ 306 EXISTS_TAC ``prefix (u :'b Action) (prefix tau E2)`` \\ 307 EXISTS_TAC ``prefix (tau :'b Action) E2`` \\ 308 ASM_REWRITE_TAC [EPS_REFL, PREFIX] ]); 309 310(* Prove WEAK_TAU1: 311 |- !u E. WEAK_EQUIV (prefix u (prefix tau E)) (prefix u E) 312 *) 313val WEAK_TAU1 = save_thm ("WEAK_TAU1", 314 OBS_CONGR_IMP_WEAK_EQUIV_RULE TAU1); 315 316(* Prove TAU2: 317 |- !E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E) 318 *) 319val TAU2 = store_thm ("TAU2", 320 ``!E. OBS_CONGR (sum E (prefix tau E)) (prefix tau E)``, 321 GEN_TAC 322 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 323 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 324 >| [ (* goal 1 (of 2) *) 325 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 326 [ (* goal 1.1 (of 2) *) 327 Q.EXISTS_TAC `E1` \\ 328 REWRITE_TAC [WEAK_TRANS, WEAK_EQUIV_REFL] \\ 329 take [`E`, `E1`] \\ 330 ASM_REWRITE_TAC [EPS_REFL] \\ 331 MATCH_MP_TAC ONE_TAU \\ 332 ASM_REWRITE_TAC [PREFIX], 333 (* goal 1.2 (of 2) *) 334 IMP_RES_TAC TRANS_PREFIX \\ 335 Q.EXISTS_TAC `E1` \\ 336 REWRITE_TAC [WEAK_EQUIV_REFL] \\ 337 IMP_RES_TAC TRANS_IMP_WEAK_TRANS ], 338 (* goal 2 (of 2) *) 339 IMP_RES_TAC TRANS_PREFIX \\ 340 Q.EXISTS_TAC `E2` \\ 341 REWRITE_TAC [WEAK_TRANS, WEAK_EQUIV_REFL] \\ 342 take [`sum E (prefix tau E)`, `E2`] \\ 343 REWRITE_TAC [EPS_REFL] \\ 344 MATCH_MP_TAC SUM2 \\ 345 PURE_ONCE_ASM_REWRITE_TAC [] ]); 346 347(* Prove WEAK_TAU2: 348 |- !E. WEAK_EQUIV (sum E (prefix tau E)) (prefix tau E) 349 *) 350val WEAK_TAU2 = save_thm ("WEAK_TAU2", 351 OBS_CONGR_IMP_WEAK_EQUIV_RULE TAU2); 352 353(* Prove TAU3: 354 |- !u E E'. 355 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E')) 356 (prefix u (sum E (prefix tau E'))) 357 *) 358val TAU3 = store_thm ("TAU3", 359 ``!(u :'b Action) E E'. 360 OBS_CONGR (sum (prefix u (sum E (prefix tau E'))) (prefix u E')) 361 (prefix u (sum E (prefix tau E')))``, 362 REPEAT GEN_TAC 363 >> PURE_ONCE_REWRITE_TAC [OBS_CONGR] 364 >> REPEAT STRIP_TAC (* 2 sub-goals here *) 365 >| [ (* goal 1 (of 2) *) 366 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 367 [ (* goal 1.1 (of 2) *) 368 IMP_RES_TAC TRANS_PREFIX \\ 369 Q.EXISTS_TAC `E1` \\ 370 REWRITE_TAC [WEAK_EQUIV_REFL] \\ 371 IMP_RES_TAC TRANS_IMP_WEAK_TRANS, 372 (* goal 1.2 (of 2) *) 373 IMP_RES_TAC TRANS_PREFIX \\ 374 Q.EXISTS_TAC `E1` \\ 375 ASM_REWRITE_TAC [WEAK_TRANS, WEAK_EQUIV_REFL] \\ 376 take [`prefix (u :'b Action) (sum E (prefix tau E'))`, 377 `sum E (prefix tau E')`] \\ 378 REWRITE_TAC [EPS_REFL, PREFIX] \\ 379 MATCH_MP_TAC ONE_TAU \\ 380 MATCH_MP_TAC SUM2 \\ 381 ASM_REWRITE_TAC [PREFIX] ], 382 (* goal 2 (of 2) *) 383 IMP_RES_TAC TRANS_PREFIX \\ 384 Q.EXISTS_TAC `E2` \\ 385 REWRITE_TAC [WEAK_TRANS, WEAK_EQUIV_REFL] \\ 386 take [`sum (prefix u (sum E (prefix tau E'))) (prefix u E')`, `E2`] \\ 387 REWRITE_TAC [EPS_REFL] \\ 388 MATCH_MP_TAC SUM1 \\ 389 PURE_ONCE_ASM_REWRITE_TAC [] ]); 390 391(* Prove WEAK_TAU3: 392 |- !u E E'. 393 WEAK_EQUIV (sum (prefix u (sum E (prefix tau E'))) (prefix u E')) 394 (prefix u (sum E (prefix tau E'))) 395 *) 396val WEAK_TAU3 = save_thm ("WEAK_TAU3", 397 OBS_CONGR_IMP_WEAK_EQUIV_RULE TAU3); 398 399val _ = export_theory (); 400val _ = html_theory "ObsCongrLaws"; 401 402(* last updated: Jun 20, 2017 *) 403