1(* ========================================================================== *) 2(* FILE : ContractionScript.sml *) 3(* DESCRIPTION : CONTRACTION and `contracts' relation *) 4(* *) 5(* THESIS : A Formalization of Unique Solutions of Equations in *) 6(* Process Algebra *) 7(* AUTHOR : (c) 2017 Chun Tian, University of Bologna, Italy *) 8(* (c) 2018 Chun Tian, Fondazione Bruno Kessler (FBK) *) 9(* DATE : 2017-2018 *) 10(* ========================================================================== *) 11 12open HolKernel Parse boolLib bossLib; 13 14open relationTheory combinTheory listTheory; 15open CCSLib CCSTheory; 16open StrongEQTheory StrongLawsTheory; 17open WeakEQTheory WeakEQLib WeakLawsTheory; 18open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory ObsCongrConv; 19open TraceTheory CongruenceTheory CoarsestCongrTheory; 20open ExpansionTheory; 21 22val _ = new_theory "Contraction"; 23val _ = temp_loose_equality (); 24 25(******************************************************************************) 26(* *) 27(* The bisimulation contraction relation *) 28(* *) 29(******************************************************************************) 30 31val CONTRACTION = new_definition ("CONTRACTION", 32 ``CONTRACTION (Con: ('a, 'b) simulation) = 33 !(E :('a, 'b) CCS) (E' :('a, 'b) CCS). Con E E' ==> 34 (!l. 35 (!E1. TRANS E (label l) E1 ==> 36 ?E2. TRANS E' (label l) E2 /\ Con E1 E2) /\ 37 (!E2. TRANS E' (label l) E2 ==> 38 ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2)) /\ 39 (!E1. TRANS E tau E1 ==> Con E1 E' \/ ?E2. TRANS E' tau E2 /\ Con E1 E2) /\ 40 (!E2. TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2)``); 41 42(* The identity relation is a CONTRACTION. *) 43val IDENTITY_CONTRACTION = store_thm ( 44 "IDENTITY_CONTRACTION", ``CONTRACTION Id``, 45 PURE_ONCE_REWRITE_TAC [CONTRACTION] 46 >> rpt STRIP_TAC >> rfs [] (* 2 sub-goals *) 47 >| [ (* goal 1 (of 2) *) 48 Q.EXISTS_TAC `E2` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\ 49 IMP_RES_TAC TRANS_IMP_WEAK_TRANS, 50 (* goal 2 (of 2) *) 51 Q.EXISTS_TAC `E2` >> REWRITE_TAC [WEAK_EQUIV_REFL] \\ 52 IMP_RES_TAC ONE_TAU ]); 53 54(* the proof is the same with EXPANSION_EPS *) 55val CONTRACTION_EPS = store_thm ( 56 "CONTRACTION_EPS", 57 ``!(Con: ('a, 'b) simulation). CONTRACTION Con ==> 58 !E E'. Con E E' ==> !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ Con E1 E2``, 59 REPEAT STRIP_TAC 60 >> qpat_x_assum `Con E E'` MP_TAC 61 >> POP_ASSUM MP_TAC 62 >> Q.SPEC_TAC (`E1`, `E1`) 63 >> Q.SPEC_TAC (`E`, `E`) 64 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 65 >> rpt STRIP_TAC (* 2 sub-goals here *) 66 >| [ (* goal 1 (of 2) *) 67 Q.EXISTS_TAC `E'` >> RW_TAC std_ss [EPS_REFL], 68 (* goal 2 (of 2) *) 69 RES_TAC \\ 70 IMP_RES_TAC 71 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 72 (ASSUME ``(Con :('a, 'b) simulation) E1 E2``)) 73 >- ( Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 74 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 75 IMP_RES_TAC ONE_TAU \\ 76 IMP_RES_TAC EPS_TRANS ]); 77 78val CONTRACTION_WEAK_TRANS_label' = store_thm ( 79 "CONTRACTION_WEAK_TRANS_label'", 80 ``!(Con: ('a, 'b) simulation). CONTRACTION Con ==> 81 !E E'. Con E E' ==> 82 !l E2. WEAK_TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 83 REPEAT STRIP_TAC 84 >> IMP_RES_TAC WEAK_TRANS_cases2 (* 2 sub-goals here *) 85 >| [ (* goal 1 (of 2) *) 86 IMP_RES_TAC 87 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 88 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 89 IMP_RES_TAC 90 (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label' (ASSUME ``WEAK_EQUIV E1 E''``)) \\ 91 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 92 MATCH_MP_TAC EPS_AND_WEAK_TRANS \\ 93 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 94 (* goal 2 (of 2) *) 95 IMP_RES_TAC 96 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 97 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 98 IMP_RES_TAC 99 (MATCH_MP WEAK_EQUIV_EPS' (ASSUME ``WEAK_EQUIV E1 E''``)) \\ 100 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 101 MATCH_MP_TAC WEAK_TRANS_AND_EPS \\ 102 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ]); 103 104val EXPANSION_IMP_CONTRACTION = store_thm ( 105 "EXPANSION_IMP_CONTRACTION", 106 ``!Con. EXPANSION Con ==> CONTRACTION Con``, 107 REPEAT STRIP_TAC 108 >> REWRITE_TAC [CONTRACTION] 109 >> rpt STRIP_TAC (* 4 sub-goals here *) 110 >| [ (* goal 1 (of 4) *) 111 IMP_RES_TAC 112 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Con``)) 113 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 114 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 115 (* goal 2 (of 4) *) 116 IMP_RES_TAC 117 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Con``)) 118 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 119 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 120 REWRITE_TAC [WEAK_EQUIV] \\ 121 Q.EXISTS_TAC `Con` >> ASM_REWRITE_TAC [] \\ 122 IMP_RES_TAC EXPANSION_IMP_WEAK_BISIM, 123 (* goal 3 (of 4) *) 124 IMP_RES_TAC 125 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Con``)) 126 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) (* 2 sub-goals here *) 127 >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] ) \\ 128 DISJ2_TAC \\ 129 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 130 (* goal 4 (of 4) *) 131 IMP_RES_TAC 132 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Con``)) 133 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 134 IMP_RES_TAC WEAK_TRANS_IMP_EPS \\ 135 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 136 REWRITE_TAC [WEAK_EQUIV] \\ 137 Q.EXISTS_TAC `Con` >> ASM_REWRITE_TAC [] \\ 138 IMP_RES_TAC EXPANSION_IMP_WEAK_BISIM ]); 139 140(* Bisimilarity contraction, written `P contracts (to) Q`, is the union of all 141 bisimulation contractions. Here we define it as a co-inductive relation. 142 143 "P contracts to Q" holds if "P is equivalent to Q" and, in addition, 144 "Q has the possibility of being as efficient as P". That is, Q is capable of 145 simulating P by performing less internal work. It is sufficient that Q has 146 one `efficient` path; Q could also have other paths, that are slower than 147 any path in P. 148 *) 149val (contracts_rules, contracts_coind, contracts_cases) = Hol_coreln ` 150 (!(E :('a, 'b) CCS) (E' :('a, 'b) CCS). 151 (!l. 152 (!E1. TRANS E (label l) E1 ==> 153 ?E2. TRANS E' (label l) E2 /\ $contracts E1 E2) /\ 154 (!E2. TRANS E' (label l) E2 ==> 155 ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2)) /\ 156 (!E1. TRANS E tau E1 ==> $contracts E1 E' \/ ?E2. TRANS E' tau E2 /\ $contracts E1 E2) /\ 157 (!E2. TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2) 158 ==> $contracts E E')`; 159 160val _ = set_fixity "contracts" (Infix (NONASSOC, 450)); 161 162val _ = Unicode.unicode_version { u = UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D47, tmnm = "contracts" }; 163val _ = TeX_notation { hol = UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D47, 164 TeX = ("\\HOLTokenContracts{}", 1) }; 165 166val contracts_is_CONTRACTION = store_thm ( 167 "contracts_is_CONTRACTION", ``CONTRACTION $contracts``, 168 PURE_ONCE_REWRITE_TAC [CONTRACTION] 169 >> REPEAT GEN_TAC 170 >> DISCH_TAC 171 >> PURE_ONCE_REWRITE_TAC [GSYM contracts_cases] 172 >> ASM_REWRITE_TAC []); 173 174(* the original definition now becomes a theorem *) 175val contracts_thm = store_thm ( 176 "contracts_thm", 177 ``!P Q. P contracts Q = ?Con. Con P Q /\ CONTRACTION Con``, 178 NTAC 2 GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 179 >| [ (* goal 1 (of 2) *) 180 DISCH_TAC \\ 181 EXISTS_TAC ``$contracts`` \\ 182 ASM_REWRITE_TAC [contracts_is_CONTRACTION], 183 (* goal 2 (of 2) *) 184 Q.SPEC_TAC (`Q`, `Q`) \\ 185 Q.SPEC_TAC (`P`, `P`) \\ 186 HO_MATCH_MP_TAC contracts_coind \\ (* co-induction used here! *) 187 METIS_TAC [CONTRACTION] ]); 188 189val CONTRACTION_SUBSET_contracts = store_thm ((* NEW *) 190 "CONTRACTION_SUBSET_contracts", 191 ``!Con. CONTRACTION Con ==> Con RSUBSET $contracts``, 192 PROVE_TAC [RSUBSET, contracts_thm]); 193 194(* "Half" theorems for `contracts` relation *) 195val contracts_TRANS_label = store_thm ( 196 "contracts_TRANS_label", 197 ``!E E'. E contracts E' ==> 198 !l E1. TRANS E (label l) E1 ==> ?E2. TRANS E' (label l) E2 /\ E1 contracts E2``, 199 PROVE_TAC [contracts_cases]); 200 201val contracts_TRANS_label' = store_thm ( 202 "contracts_TRANS_label'", 203 ``!E E'. E contracts E' ==> 204 !l E2. TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 205 PROVE_TAC [contracts_cases]); 206 207val contracts_TRANS_tau = store_thm ( 208 "contracts_TRANS_tau", 209 ``!E E'. E contracts E' ==> 210 !E1. TRANS E tau E1 ==> E1 contracts E' \/ ?E2. TRANS E' tau E2 /\ E1 contracts E2``, 211 PROVE_TAC [contracts_cases]); 212 213val contracts_TRANS_tau' = store_thm ( 214 "contracts_TRANS_tau'", 215 ``!E E'. E contracts E' ==> 216 !E2. TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 217 PROVE_TAC [contracts_cases]); 218 219(* The `contracts` relation is reflexive *) 220val contracts_reflexive = store_thm ( 221 "contracts_reflexive", ``reflexive $contracts``, 222 REWRITE_TAC [reflexive_def] 223 >> GEN_TAC 224 >> PURE_ONCE_REWRITE_TAC [contracts_thm] 225 >> Q.EXISTS_TAC `Id` 226 >> REWRITE_TAC [IDENTITY_CONTRACTION]); 227 228(* the version for easier use *) 229val contracts_REFL = save_thm ( 230 "contracts_REFL", REWRITE_RULE [reflexive_def] contracts_reflexive); 231 232(* `expands` implies `contracts` *) 233val expands_IMP_contracts = store_thm ( 234 "expands_IMP_contracts", ``!P Q. P expands Q ==> P contracts Q``, 235 REPEAT GEN_TAC 236 >> REWRITE_TAC [contracts_thm, expands_thm] 237 >> rpt STRIP_TAC 238 >> Q.EXISTS_TAC `Exp` 239 >> ASM_REWRITE_TAC [] 240 >> IMP_RES_TAC EXPANSION_IMP_CONTRACTION); 241 242(* NOTE: unlike in the EXPANSION cases, CONTRACTION_IMP_WEAK_BISIM doesn't hold, 243 To finish the proof, prof. Sangiorgi said "You do not prove Con itself is a weak 244 bisimulation, but rather that Con "union" weak bisimilarity is a weak bisimulation." 245 that is amazing ... 246 *) 247val contracts_IMP_WEAK_EQUIV = store_thm ( 248 "contracts_IMP_WEAK_EQUIV", 249 ``!P Q. P contracts Q ==> WEAK_EQUIV P Q``, 250 REPEAT GEN_TAC 251 >> REWRITE_TAC [WEAK_EQUIV, contracts_thm] 252 >> rpt STRIP_TAC 253 >> Q.EXISTS_TAC `Con RUNION WEAK_EQUIV` 254 >> REWRITE_TAC [RUNION] 255 >> CONJ_TAC >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] ) 256 >> REWRITE_TAC [WEAK_BISIM, RUNION] 257 >> rpt STRIP_TAC (* 8 sub-goals here *) 258 >| [ (* goal 1 (of 8) *) 259 IMP_RES_TAC 260 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 261 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 262 Q.EXISTS_TAC `E2` \\ 263 CONJ_TAC >- ( MATCH_MP_TAC TRANS_IMP_WEAK_TRANS >> ASM_REWRITE_TAC [] ) \\ 264 DISJ1_TAC >> ASM_REWRITE_TAC [], 265 (* goal 2 (of 8) *) 266 IMP_RES_TAC 267 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 268 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 269 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 270 (* goal 3 (of 8) *) 271 IMP_RES_TAC 272 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 273 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) (* 2 sub-goals here *) 274 >- ( Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [EPS_REFL] ) \\ 275 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 276 IMP_RES_TAC ONE_TAU, 277 (* goal 4 (of 8) *) 278 IMP_RES_TAC 279 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 280 (ASSUME ``(Con :('a, 'b) simulation) E E'``)) \\ 281 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 282 (* goal 5 (of 8) *) 283 IMP_RES_TAC WEAK_EQUIV_TRANS_label \\ 284 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 285 (* goal 6 (of 8) *) 286 IMP_RES_TAC WEAK_EQUIV_TRANS_label' \\ 287 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 288 (* goal 7 (of 8) *) 289 IMP_RES_TAC WEAK_EQUIV_TRANS_tau \\ 290 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 291 (* goal 8 (of 8) *) 292 IMP_RES_TAC WEAK_EQUIV_TRANS_tau' \\ 293 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ]); 294 295(* This proof depends on `contracts_IMP_WEAK_EQUIV`, that's why it's here *) 296val CONTRACTION_EPS' = store_thm ( 297 "CONTRACTION_EPS'", 298 ``!(Con: ('a, 'b) simulation). CONTRACTION Con ==> 299 !E E'. Con E E' ==> 300 !u E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 301 REPEAT STRIP_TAC 302 >> qpat_x_assum `Con E E'` MP_TAC 303 >> POP_ASSUM MP_TAC 304 >> Q.SPEC_TAC (`E2`, `E2`) 305 >> Q.SPEC_TAC (`E'`, `E'`) 306 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 307 >> rpt STRIP_TAC (* 2 sub-goals here *) 308 >| [ (* goal 1 (of 2) *) 309 Q.EXISTS_TAC `E` >> REWRITE_TAC [EPS_REFL] \\ 310 MATCH_MP_TAC contracts_IMP_WEAK_EQUIV \\ (* IMPORTANT! *) 311 REWRITE_TAC [contracts_thm] \\ 312 Q.EXISTS_TAC `Con` >> ASM_REWRITE_TAC [], 313 (* goal 2 (of 2) *) 314 RES_TAC \\ 315 IMP_RES_TAC 316 (MATCH_MP WEAK_EQUIV_TRANS_tau' (ASSUME ``WEAK_EQUIV E1 E2``)) \\ 317 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 318 IMP_RES_TAC EPS_TRANS ]); 319 320(* The composition of two CONTRACTIONs is still an CONTRACTION. *) 321val COMP_CONTRACTION = store_thm ( 322 "COMP_CONTRACTION", 323 ``!Con1 Con2. CONTRACTION Con1 /\ CONTRACTION Con2 ==> CONTRACTION (Con2 O Con1)``, 324 REPEAT STRIP_TAC 325 >> REWRITE_TAC [CONTRACTION, O_DEF] 326 >> BETA_TAC 327 >> REPEAT STRIP_TAC (* 4 sub-goals here *) 328 >| [ (* goal 1 (of 4) *) 329 IMP_RES_TAC 330 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con1``)) 331 (ASSUME ``(Con1 :('a, 'b) simulation) E y``)) \\ 332 IMP_RES_TAC 333 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con2``)) 334 (ASSUME ``(Con2 :('a, 'b) simulation) y E'``)) \\ 335 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 336 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 337 (* goal 2 (of 4) *) 338 IMP_RES_TAC 339 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con2``)) 340 (ASSUME ``(Con2 :('a, 'b) simulation) y E'``)) \\ 341 IMP_RES_TAC 342 (MATCH_MP (MATCH_MP CONTRACTION_WEAK_TRANS_label' (ASSUME ``CONTRACTION Con1``)) 343 (ASSUME ``(Con1 :('a, 'b) simulation) E y``)) \\ 344 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 345 IMP_RES_TAC WEAK_EQUIV_TRANS, 346 (* goal 3 (of 4) *) 347 IMP_RES_TAC 348 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con1``)) 349 (ASSUME ``(Con1 :('a, 'b) simulation) E y``)) (* 2 sub-goals here *) 350 >- ( DISJ1_TAC >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [] ) \\ 351 IMP_RES_TAC 352 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con2``)) 353 (ASSUME ``(Con2 :('a, 'b) simulation) y E'``)) (* 2 sub-goals here *) 354 >- ( DISJ1_TAC >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 355 DISJ2_TAC \\ 356 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 357 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 358 (* goal 4 (of 4) *) 359 IMP_RES_TAC 360 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con2``)) 361 (ASSUME ``(Con2 :('a, 'b) simulation) y E'``)) \\ 362 IMP_RES_TAC 363 (MATCH_MP (MATCH_MP CONTRACTION_EPS' (ASSUME ``CONTRACTION Con1``)) 364 (ASSUME ``(Con1 :('a, 'b) simulation) E y``)) \\ 365 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 366 IMP_RES_TAC WEAK_EQUIV_TRANS ]); 367 368(* The `contracts` relation is transitive 369 NOTE: it's not symmetric, because otherwise it becomes equivalence relation *) 370val contracts_transitive = store_thm ( 371 "contracts_transitive", ``transitive $contracts``, 372 REWRITE_TAC [transitive_def] 373 >> REPEAT GEN_TAC 374 >> PURE_ONCE_REWRITE_TAC [contracts_thm] 375 >> STRIP_TAC 376 >> Q.EXISTS_TAC `Con' O Con` 377 >> CONJ_TAC (* 2 sub-goals here *) 378 >| [ (* goal 1 (of 2) *) 379 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 380 Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [], 381 (* goal 2 (of 2) *) 382 IMP_RES_TAC COMP_CONTRACTION ]); 383 384(* the version for easier use *) 385val contracts_TRANS = save_thm ( 386 "contracts_TRANS", REWRITE_RULE [transitive_def] contracts_transitive); 387 388(* `contracts` is a pre-order *) 389val contracts_PreOrder = store_thm ( 390 "contracts_PreOrder", ``PreOrder $contracts``, 391 REWRITE_TAC [PreOrder, contracts_reflexive, contracts_transitive]); 392 393val contracts_WEAK_TRANS_label' = store_thm ( 394 "contracts_WEAK_TRANS_label'", 395 ``!E E'. E contracts E' ==> 396 !l E2. WEAK_TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 397 REWRITE_TAC [contracts_thm] 398 >> REPEAT STRIP_TAC 399 >> IMP_RES_TAC CONTRACTION_WEAK_TRANS_label' 400 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC []); 401 402val contracts_WEAK_TRANS_tau' = store_thm ( 403 "contracts_WEAK_TRANS_tau'", 404 ``!E E'. E contracts E' ==> 405 !l E2. WEAK_TRANS E' tau E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 406 REPEAT STRIP_TAC 407 >> IMP_RES_TAC WEAK_TRANS_TAU 408 >> IMP_RES_TAC contracts_TRANS_tau' 409 >> IMP_RES_TAC 410 (MATCH_MP WEAK_EQUIV_EPS' (ASSUME ``WEAK_EQUIV E1 E''``)) 411 >> Q.EXISTS_TAC `E1'` 412 >> ASM_REWRITE_TAC [] 413 >> IMP_RES_TAC EPS_TRANS); 414 415val contracts_EPS = store_thm ( 416 "contracts_EPS", 417 ``!E E'. E contracts E' ==> !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ E1 contracts E2``, 418 REWRITE_TAC [contracts_thm] 419 >> rpt STRIP_TAC 420 >> IMP_RES_TAC CONTRACTION_EPS 421 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] 422 >> Q.EXISTS_TAC `Con` >> ASM_REWRITE_TAC []); 423 424val contracts_EPS' = store_thm ( 425 "contracts_EPS'", 426 ``!E E'. E contracts E' ==> !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 427 REWRITE_TAC [contracts_thm] 428 >> rpt STRIP_TAC 429 >> IMP_RES_TAC CONTRACTION_EPS' 430 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC []); 431 432val contracts_WEAK_TRANS_label = store_thm ( 433 "contracts_WEAK_TRANS_label", 434 ``!E E'. E contracts E' ==> 435 !l E1. WEAK_TRANS E (label l) E1 ==> ?E2. WEAK_TRANS E' (label l) E2 /\ E1 contracts E2``, 436 REPEAT STRIP_TAC 437 >> IMP_RES_TAC WEAK_TRANS 438 >> IMP_RES_TAC (MATCH_MP contracts_EPS (ASSUME ``E contracts E'``)) 439 >> IMP_RES_TAC (MATCH_MP contracts_TRANS_label (ASSUME ``E1' contracts E2'``)) 440 >> IMP_RES_TAC (MATCH_MP contracts_EPS (ASSUME ``E2 contracts E2''``)) 441 >> Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] 442 >> REWRITE_TAC [WEAK_TRANS] 443 >> take [`E2'`, `E2''`] >> ASM_REWRITE_TAC []); 444 445val contracts_WEAK_TRANS_tau = store_thm ( 446 "contracts_WEAK_TRANS_tau", 447 ``!E E'. E contracts E' ==> 448 !E1. WEAK_TRANS E tau E1 ==> ?E2. EPS E' E2 /\ E1 contracts E2``, 449 REPEAT STRIP_TAC 450 >> IMP_RES_TAC WEAK_TRANS 451 >> IMP_RES_TAC (MATCH_MP contracts_EPS (ASSUME ``E contracts E'``)) 452 >> IMP_RES_TAC 453 (MATCH_MP contracts_TRANS_tau (ASSUME ``E1' contracts E2'``)) (* 2 sub-goals here *) 454 >| [ (* goal 1 (of 2) *) 455 IMP_RES_TAC (MATCH_MP contracts_EPS (ASSUME ``E2 contracts E2'``)) \\ 456 Q.EXISTS_TAC `E2''` >> ASM_REWRITE_TAC [] \\ 457 IMP_RES_TAC EPS_TRANS, 458 (* goal 2 (of 2) *) 459 IMP_RES_TAC (MATCH_MP contracts_EPS (ASSUME ``E2 contracts E2''``)) \\ 460 Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] \\ 461 IMP_RES_TAC ONE_TAU \\ 462 IMP_RES_TAC EPS_TRANS ]); 463 464(******************************************************************************) 465(* *) 466(* `contracts` is precongruence *) 467(* *) 468(******************************************************************************) 469 470val contracts_SUBST_PREFIX = store_thm ( 471 "contracts_SUBST_PREFIX", 472 ``!E E'. E contracts E' ==> !u. (prefix u E) contracts (prefix u E')``, 473 rpt GEN_TAC 474 >> PURE_ONCE_REWRITE_TAC [Q.SPECL [`prefix u E`, `prefix u E'`] contracts_cases] 475 >> rpt STRIP_TAC (* 4 sub-goals here *) 476 >| [ (* goal 1 (of 4) *) 477 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 478 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [PREFIX], 479 (* goal 2 (of 4) *) 480 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 481 Q.EXISTS_TAC `E` >> REWRITE_TAC [WEAK_PREFIX] \\ 482 IMP_RES_TAC contracts_IMP_WEAK_EQUIV, 483 (* goal 3 (of 4) *) 484 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 485 DISJ2_TAC \\ 486 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [PREFIX], 487 (* goal 4 (of 4) *) 488 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 489 Q.EXISTS_TAC `E` \\ 490 qpat_x_assum `tau = u` (REWRITE_TAC o wrap o SYM) \\ 491 CONJ_TAC >- ( MATCH_MP_TAC ONE_TAU >> REWRITE_TAC [PREFIX] ) \\ 492 IMP_RES_TAC contracts_IMP_WEAK_EQUIV ]); 493 494val contracts_PRESD_BY_GUARDED_SUM = store_thm ( 495 "contracts_PRESD_BY_GUARDED_SUM", 496 ``!E1 E1' E2 E2' a1 a2. 497 E1 contracts E1' /\ E2 contracts E2' ==> 498 (sum (prefix a1 E1) (prefix a2 E2)) contracts 499 (sum (prefix a1 E1') (prefix a2 E2'))``, 500 REPEAT STRIP_TAC 501 >> ONCE_REWRITE_TAC [contracts_cases] 502 >> rpt STRIP_TAC (* 4 sub-goals here *) 503 >| [ (* goal 1 (of 4) *) 504 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 505 [ (* goal 1.1 (of 2) *) 506 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 507 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 508 MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 509 (* goal 1.2 (of 2) *) 510 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 511 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 512 MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ], 513 (* goal 2 (of 4) *) 514 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 515 [ (* goal 2.1 (of 2) *) 516 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 517 Q.EXISTS_TAC `E1` \\ 518 CONJ_TAC >- ( MATCH_MP_TAC WEAK_SUM1 >> REWRITE_TAC [WEAK_PREFIX] ) \\ 519 IMP_RES_TAC contracts_IMP_WEAK_EQUIV, 520 (* goal 2.2 (of 2) *) 521 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 522 Q.EXISTS_TAC `E2` \\ 523 CONJ_TAC >- ( MATCH_MP_TAC WEAK_SUM2 >> REWRITE_TAC [WEAK_PREFIX] ) \\ 524 IMP_RES_TAC contracts_IMP_WEAK_EQUIV ], 525 (* goal 3 (of 4) *) 526 DISJ2_TAC >> IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 527 [ (* goal 3.1 (of 2) *) 528 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 529 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 530 MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 531 (* goal 3.2 (of 2) *) 532 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 533 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 534 MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ], 535 (* goal 4 (of 4) *) 536 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 537 [ (* goal 3.1 (of 2) *) 538 IMP_RES_TAC TRANS_PREFIX \\ 539 qpat_x_assum `tau = a1` (fs o wrap o SYM) \\ 540 Q.EXISTS_TAC `E1` \\ 541 Rev CONJ_TAC >- IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 542 MATCH_MP_TAC ONE_TAU \\ 543 MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 544 (* goal 3.2 (of 2) *) 545 IMP_RES_TAC TRANS_PREFIX \\ 546 qpat_x_assum `tau = a2` (fs o wrap o SYM) \\ 547 Q.EXISTS_TAC `E2` \\ 548 Rev CONJ_TAC >- IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 549 MATCH_MP_TAC ONE_TAU \\ 550 MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ] ]); 551 552val contracts_PRESD_BY_PAR = store_thm ( 553 "contracts_PRESD_BY_PAR", 554 ``!E1 E1' E2 E2'. 555 E1 contracts E1' /\ E2 contracts E2' ==> (par E1 E2) contracts (par E1' E2')``, 556 REPEAT STRIP_TAC 557 >> PURE_ONCE_REWRITE_TAC [contracts_thm] 558 >> Q.EXISTS_TAC `\x y. 559 ?F1 F1' F2 F2'. 560 (x = par F1 F2) /\ (y = par F1' F2') /\ 561 F1 contracts F1' /\ F2 contracts F2'` 562 >> BETA_TAC 563 >> CONJ_TAC >- ( take [`E1`, `E1'`, `E2`, `E2'`] >> ASM_REWRITE_TAC [] ) 564 >> PURE_ONCE_REWRITE_TAC [CONTRACTION] 565 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 566 >| [ (* goal 1 (of 4) *) 567 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 568 (ASSUME ``TRANS E (label l) E1''``)) \\ 569 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 570 [ (* goal 1.1 (of 3) *) 571 IMP_RES_TAC (MATCH_MP contracts_TRANS_label 572 (ASSUME ``F1 contracts F1'``)) \\ 573 EXISTS_TAC ``par E2'' F2'`` \\ 574 CONJ_TAC >| (* 2 sub-goals here *) 575 [ (* goal 1.1.1 (of 2) *) 576 ASM_REWRITE_TAC [] \\ 577 MATCH_MP_TAC PAR1 >> ASM_REWRITE_TAC [], 578 (* goal 1.1.2 (of 2) *) 579 take [`E1'''`, `E2''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ], 580 (* goal 1.2 (of 3) *) 581 IMP_RES_TAC (MATCH_MP contracts_TRANS_label 582 (ASSUME ``F2 contracts F2'``)) \\ 583 EXISTS_TAC ``par F1' E2''`` \\ 584 CONJ_TAC >| (* 2 sub-goals here *) 585 [ (* goal 1.2.1 (of 2) *) 586 ASM_REWRITE_TAC [] \\ 587 MATCH_MP_TAC PAR2 >> ASM_REWRITE_TAC [], 588 (* goal 1.2.2 (of 2) *) 589 take [`F1`, `F1'`, `E1'''`, `E2''`] >> ASM_REWRITE_TAC [] ], 590 (* goal 1.3 (of 3) *) 591 IMP_RES_TAC Action_distinct_label ], 592 (* goal 2 (of 4) *) 593 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 594 (ASSUME ``TRANS E' (label l) E2''``)) \\ 595 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 596 [ (* goal 2.1 (of 3) *) 597 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' 598 (ASSUME ``F1 contracts F1'``)) \\ 599 EXISTS_TAC ``par E1''' F2`` \\ 600 CONJ_TAC >| (* 2 sub-goals here *) 601 [ (* goal 2.1.1 (of 2) *) 602 ASM_REWRITE_TAC [] \\ 603 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 604 (* goal 2.1.2 (of 2) *) 605 ASM_REWRITE_TAC [] \\ 606 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_PAR \\ 607 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> ASM_REWRITE_TAC [] ], 608 (* goal 2.2 (of 3) *) 609 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' 610 (ASSUME ``F2 contracts F2'``)) \\ 611 EXISTS_TAC ``par F1 E1'''`` \\ 612 CONJ_TAC >| (* 2 sub-goals here *) 613 [ (* goal 2.2.1 (of 2) *) 614 ASM_REWRITE_TAC [] \\ 615 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 616 (* goal 2.2.2 (of 2) *) 617 ASM_REWRITE_TAC [] \\ 618 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_PAR \\ 619 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> ASM_REWRITE_TAC [] ], 620 (* goal 2.3 (of 3) *) 621 IMP_RES_TAC Action_distinct_label ], 622 (* goal 3 (of 4) *) 623 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 624 (ASSUME ``TRANS E tau E1''``)) \\ 625 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 626 [ (* goal 3.1 (of 3) *) 627 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau 628 (ASSUME ``F1 contracts F1'``)) >| (* 2 sub-goals here *) 629 [ (* goal 3.1.1 (of 2) *) 630 DISJ1_TAC >> take [`E1'''`, `F1'`, `F2`, `F2'`] >> ASM_REWRITE_TAC [], 631 (* goal 3.1.2 (of 2) *) 632 DISJ2_TAC \\ 633 EXISTS_TAC ``par E2'' F2'`` \\ 634 CONJ_TAC >| (* 2 sub-goals here *) 635 [ (* goal 3.1.2.1 (of 2) *) 636 ASM_REWRITE_TAC [] \\ 637 MATCH_MP_TAC PAR1 >> ASM_REWRITE_TAC [], 638 (* goal 3.1.2.2 (of 2) *) 639 take [`E1'''`, `E2''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ] ], 640 (* goal 3.2 (of 3) *) 641 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau 642 (ASSUME ``F2 contracts F2'``)) >| (* 2 sub-goals here *) 643 [ (* goal 3.2.1 (of 2) *) 644 DISJ1_TAC >> take [`F1`, `F1'`, `E1'''`, `F2'`] >> ASM_REWRITE_TAC [], 645 (* goal 3.2.2 (of 2) *) 646 DISJ2_TAC \\ 647 EXISTS_TAC ``par F1' E2''`` \\ 648 CONJ_TAC >| (* 2 sub-goals here *) 649 [ (* goal 3.2.2.1 (of 2) *) 650 ASM_REWRITE_TAC [] \\ 651 MATCH_MP_TAC PAR2 >> ASM_REWRITE_TAC [], 652 (* goal 3.2.2.2 (of 2) *) 653 take [`F1`, `F1'`, `E1'''`, `E2''`] >> ASM_REWRITE_TAC [] ] ], 654 (* goal 3.3 (of 3) *) 655 IMP_RES_TAC (MATCH_MP contracts_TRANS_label (ASSUME ``F1 contracts F1'``)) \\ 656 IMP_RES_TAC (MATCH_MP contracts_TRANS_label (ASSUME ``F2 contracts F2'``)) \\ 657 DISJ2_TAC \\ 658 EXISTS_TAC ``par E2''' E2''''`` \\ 659 CONJ_TAC >| (* 2 sub-goals here *) 660 [ (* goal 3.3.1 (of 2) *) 661 ONCE_ASM_REWRITE_TAC [] \\ 662 MATCH_MP_TAC PAR3 \\ 663 Q.EXISTS_TAC `l` >> ASM_REWRITE_TAC [], 664 (* goal 3.3.2 (of 2) *) 665 take [`E1'''`, `E2'''`, `E2''`, `E2''''`] >> ASM_REWRITE_TAC [] ] ], 666 (* goal 4 (of 4) *) 667 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 668 (ASSUME ``TRANS E' tau E2''``)) \\ 669 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 670 [ (* goal 4.1 (of 3) *) 671 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau' (ASSUME ``F1 contracts F1'``)) \\ 672 EXISTS_TAC ``par E1''' F2`` \\ 673 CONJ_TAC >| (* 2 sub-goals here *) 674 [ (* goal 4.1.1 (of 2) *) 675 ASM_REWRITE_TAC [] \\ 676 IMP_RES_TAC EPS_PAR >> ASM_REWRITE_TAC [], 677 (* goal 4.1.2 (of 2) *) 678 ASM_REWRITE_TAC [] \\ 679 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_PAR \\ 680 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> ASM_REWRITE_TAC [] ], 681 (* goal 4.2 (of 3) *) 682 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau' (ASSUME ``F2 contracts F2'``)) \\ 683 EXISTS_TAC ``par F1 E1'''`` \\ 684 CONJ_TAC >| (* 2 sub-goals here *) 685 [ (* goal 4.2.1 (of 2) *) 686 ASM_REWRITE_TAC [] \\ 687 IMP_RES_TAC EPS_PAR >> ASM_REWRITE_TAC [], 688 (* goal 4.2.2 (of 2) *) 689 ASM_REWRITE_TAC [] \\ 690 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_PAR \\ 691 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> ASM_REWRITE_TAC [] ], 692 (* goal 4.3 (of 3) *) 693 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' (ASSUME ``F1 contracts F1'``)) \\ 694 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' (ASSUME ``F2 contracts F2'``)) \\ 695 EXISTS_TAC ``par E1''' E1''''`` \\ 696 Rev CONJ_TAC 697 >- ( ASM_REWRITE_TAC [] \\ 698 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_PAR \\ 699 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> ASM_REWRITE_TAC [] ) \\ 700 ONCE_ASM_REWRITE_TAC [] \\ 701 MATCH_MP_TAC WEAK_TRANS_IMP_EPS \\ 702 REWRITE_TAC [WEAK_TRANS] \\ 703 STRIP_ASSUME_TAC 704 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS F1 (label l) E1'''``)) \\ 705 STRIP_ASSUME_TAC 706 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS F2 (label (COMPL l)) E1''''``)) \\ 707 EXISTS_TAC ``par E1''''' E1''''''`` \\ 708 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 709 (CONJ (ASSUME ``EPS F1 E1'''''``) 710 (ASSUME ``EPS F2 E1''''''``))] \\ 711 EXISTS_TAC ``par E2'''' E2'''''`` \\ 712 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 713 (CONJ (ASSUME ``EPS E2'''' E1'''``) 714 (ASSUME ``EPS E2''''' E1''''``))] \\ 715 MATCH_MP_TAC PAR3 \\ 716 Q.EXISTS_TAC `l` >> ASM_REWRITE_TAC [] ] ]); 717 718(* |- ���E E'. E contracts E' ��� ���E''. (E || E'') contracts (E' || E'') *) 719val contracts_SUBST_PAR_R = save_thm ( 720 "contracts_SUBST_PAR_R", 721 Q_GENL [`E`, `E'`] 722 (DISCH ``E contracts E'`` 723 (Q.GEN `E''` 724 (MATCH_MP contracts_PRESD_BY_PAR 725 (CONJ (ASSUME ``E contracts E'``) 726 (Q.SPEC `E''` contracts_REFL)))))); 727 728(* |- ���E E'. E contracts E' ��� ���E''. (E'' || E) contracts (E'' || E') *) 729val contracts_SUBST_PAR_L = save_thm ( 730 "contracts_SUBST_PAR_L", 731 Q_GENL [`E`, `E'`] 732 (DISCH ``E contracts E'`` 733 (Q.GEN `E''` 734 (MATCH_MP contracts_PRESD_BY_PAR 735 (CONJ (Q.SPEC `E''` contracts_REFL) 736 (ASSUME ``E contracts E'``)))))); 737 738val contracts_SUBST_RESTR = store_thm ( 739 "contracts_SUBST_RESTR", 740 ``!E E'. E contracts E' ==> !L. (restr L E) contracts (restr L E')``, 741 REPEAT STRIP_TAC 742 >> PURE_ONCE_REWRITE_TAC [contracts_thm] 743 >> Q.EXISTS_TAC `\x y. ?E1 E2 L'. (x = restr L' E1) /\ (y = restr L' E2) /\ E1 contracts E2` 744 >> BETA_TAC 745 >> CONJ_TAC >- ( take [`E`, `E'`, `L`] >> ASM_REWRITE_TAC [] ) 746 >> PURE_ONCE_REWRITE_TAC [CONTRACTION] 747 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 748 >| [ (* goal 1 (of 4) *) 749 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 750 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 751 IMP_RES_TAC TRANS_RESTR >- IMP_RES_TAC Action_distinct_label \\ 752 IMP_RES_TAC (MATCH_MP contracts_TRANS_label (ASSUME ``E1 contracts E2``)) \\ 753 Q.EXISTS_TAC `restr L' E2'` \\ 754 ASM_REWRITE_TAC 755 [MATCH_MP WEAK_RESTR_label 756 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 757 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 758 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 759 (ASSUME ``WEAK_TRANS E2 (label l) E2'``)])] \\ 760 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> Q.EXISTS_TAC `l'` >> rfs [Action_11] ) \\ 761 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [], 762 (* goal 2 (of 4) *) 763 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 764 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 765 IMP_RES_TAC TRANS_RESTR >- IMP_RES_TAC Action_distinct_label \\ 766 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' (ASSUME ``E1 contracts E2``)) \\ 767 Q.EXISTS_TAC `restr L' E1'` \\ 768 ASM_REWRITE_TAC 769 [MATCH_MP WEAK_RESTR_label 770 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 771 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 772 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 773 (ASSUME ``WEAK_TRANS E1 (label l) E1'``)])] \\ 774 MATCH_MP_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [], 775 (* goal 3 (of 4) *) 776 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 777 (ASSUME ``TRANS E'' tau E1'``)) \\ 778 Rev (IMP_RES_TAC TRANS_RESTR) >- IMP_RES_TAC Action_distinct \\ 779 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau (ASSUME ``E1 contracts E2``)) 780 >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] \\ 781 take [`E''''`, `E2`, `L'`] >> ASM_REWRITE_TAC [] ) \\ 782 DISJ2_TAC \\ 783 ONCE_ASM_REWRITE_TAC [] \\ 784 Q.EXISTS_TAC `restr L' E2'` \\ 785 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> fs [] ) \\ 786 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [], 787 (* goal 4 (of 4) *) 788 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 789 (ASSUME ``TRANS E''' tau E2'``)) \\ 790 Rev (IMP_RES_TAC TRANS_RESTR) >- IMP_RES_TAC Action_distinct \\ 791 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau' (ASSUME ``E1 contracts E2``)) \\ 792 Q.EXISTS_TAC `restr L' E1'` \\ 793 Rev CONJ_TAC 794 >- ( ASM_REWRITE_TAC [] \\ 795 MATCH_MP_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [] ) \\ 796 ONCE_ASM_REWRITE_TAC [] \\ 797 IMP_RES_TAC EPS_RESTR >> ASM_REWRITE_TAC [] ]); 798 799val contracts_SUBST_RELAB = store_thm ( 800 "contracts_SUBST_RELAB", 801 ``!E E'. E contracts E' ==> !rf. (relab E rf) contracts (relab E' rf)``, 802 REPEAT STRIP_TAC 803 >> PURE_ONCE_REWRITE_TAC [contracts_thm] 804 >> Q.EXISTS_TAC 805 `\x y. ?E1 E2 rf'. (x = relab E1 rf') /\ (y = relab E2 rf') /\ E1 contracts E2` 806 >> BETA_TAC 807 >> CONJ_TAC >- ( take [`E`, `E'`, `rf`] >> ASM_REWRITE_TAC [] ) 808 >> PURE_ONCE_REWRITE_TAC [CONTRACTION] 809 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 810 >| [ (* goal 1 (of 4) *) 811 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 812 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 813 IMP_RES_TAC TRANS_RELAB \\ 814 qpat_x_assum `label l = relabel rf' u'` (ASSUME_TAC o SYM) \\ 815 IMP_RES_TAC Relab_label \\ 816 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 817 (ASSUME ``TRANS E1 u' E''''``)) \\ 818 IMP_RES_TAC (MATCH_MP contracts_TRANS_label (ASSUME ``E1 contracts E2``)) \\ 819 EXISTS_TAC ``relab E2' rf'`` \\ 820 Rev CONJ_TAC 821 >- ( take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 822 ASM_REWRITE_TAC [] \\ 823 qpat_x_assum `relabel rf' u' = label l` (REWRITE_TAC o wrap o SYM) \\ 824 MATCH_MP_TAC RELABELING >> ASM_REWRITE_TAC [], 825 (* goal 2 (of 4) *) 826 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 827 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 828 IMP_RES_TAC TRANS_RELAB \\ 829 qpat_x_assum `label l = relabel rf' u'` (ASSUME_TAC o SYM) \\ 830 IMP_RES_TAC Relab_label \\ 831 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 832 (ASSUME ``TRANS E2 u' E''''``)) \\ 833 IMP_RES_TAC (MATCH_MP contracts_TRANS_label' (ASSUME ``E1 contracts E2``)) \\ 834 EXISTS_TAC ``relab E1' rf'`` \\ 835 Rev CONJ_TAC 836 >- ( ASM_REWRITE_TAC [] \\ 837 MATCH_MP_TAC WEAK_EQUIV_SUBST_RELAB >> ASM_REWRITE_TAC [] ) \\ 838 ASM_REWRITE_TAC [] \\ 839 IMP_RES_TAC WEAK_RELAB_rf >> PROVE_TAC [], 840 (* goal 3 (of 4) *) 841 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 842 (ASSUME ``TRANS E'' tau E1'``)) \\ 843 IMP_RES_TAC TRANS_RELAB \\ 844 qpat_x_assum `tau = relabel rf' u'` (ASSUME_TAC o SYM) \\ 845 IMP_RES_TAC Relab_tau \\ 846 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 847 (ASSUME ``TRANS E1 u' E''''``)) \\ 848 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau (ASSUME ``E1 contracts E2``)) 849 >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] \\ 850 take [`E''''`, `E2`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 851 DISJ2_TAC >> EXISTS_TAC ``relab E2' rf'`` \\ 852 Rev CONJ_TAC 853 >- ( take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 854 ASM_REWRITE_TAC [] \\ 855 qpat_x_assum `relabel rf' u' = tau` (REWRITE_TAC o wrap o SYM) \\ 856 MATCH_MP_TAC RELABELING >> ASM_REWRITE_TAC [], 857 (* goal 4 (of 4) *) 858 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 859 (ASSUME ``TRANS E''' tau E2'``)) \\ 860 IMP_RES_TAC TRANS_RELAB \\ 861 qpat_x_assum `tau = relabel rf' u'` (ASSUME_TAC o SYM) \\ 862 IMP_RES_TAC Relab_tau \\ 863 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 864 (ASSUME ``TRANS E2 u' E''''``)) \\ 865 IMP_RES_TAC (MATCH_MP contracts_TRANS_tau' (ASSUME ``E1 contracts E2``)) \\ 866 EXISTS_TAC ``relab E1' rf'`` \\ 867 Rev CONJ_TAC 868 >- ( ASM_REWRITE_TAC [] \\ 869 MATCH_MP_TAC WEAK_EQUIV_SUBST_RELAB >> ASM_REWRITE_TAC [] ) \\ 870 ASM_REWRITE_TAC [] \\ 871 qpat_x_assum `relabel rf' u' = tau` (REWRITE_TAC o wrap o SYM) \\ 872 IMP_RES_TAC EPS_RELAB_rf >> ASM_REWRITE_TAC [] ]); 873 874val contracts_SUBST_GCONTEXT = store_thm ( 875 "contracts_SUBST_GCONTEXT", 876 ``!P Q. P contracts Q ==> !E. GCONTEXT E ==> (E P) contracts (E Q)``, 877 rpt GEN_TAC >> DISCH_TAC 878 >> Induct_on `GCONTEXT` 879 >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 880 >- ASM_REWRITE_TAC [] 881 >- REWRITE_TAC [contracts_REFL] 882 >| [ (* goal 1 (of 5) *) 883 MATCH_MP_TAC contracts_SUBST_PREFIX >> ASM_REWRITE_TAC [], 884 (* goal 2 (of 5) *) 885 MATCH_MP_TAC contracts_PRESD_BY_GUARDED_SUM \\ 886 ASM_REWRITE_TAC [], 887 (* goal 3 (of 5) *) 888 IMP_RES_TAC contracts_PRESD_BY_PAR, 889 (* goal 4 (of 5) *) 890 MATCH_MP_TAC contracts_SUBST_RESTR >> ASM_REWRITE_TAC [], 891 (* goal 5 (of 5) *) 892 MATCH_MP_TAC contracts_SUBST_RELAB >> ASM_REWRITE_TAC [] ]); 893 894val contracts_precongruence = store_thm ( 895 "contracts_precongruence", ``precongruence1 $contracts``, 896 PROVE_TAC [precongruence1_def, contracts_PreOrder, contracts_SUBST_GCONTEXT]); 897 898(******************************************************************************) 899(* *) 900(* Trace, Weak transition and Contraction *) 901(* *) 902(******************************************************************************) 903 904val contracts_AND_TRACE1_lemma = Q.prove ( 905 `!E xs E1. TRACE E xs E1 ==> 906 !E'. E contracts E' ==> ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2`, 907 HO_MATCH_MP_TAC TRACE_strongind 908 >> rpt STRIP_TAC >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [TRACE_REFL] ) 909 >> Cases_on `h` (* 2 sub-goals here *) 910 >| [ (* goal 1 (of 2) *) 911 IMP_RES_TAC contracts_TRANS_tau >| (* 2 sub-goals here *) 912 [ (* goal 1.1 (of 2) *) 913 RES_TAC >> take [`xs'`, `E2`] >> ASM_REWRITE_TAC [], 914 (* goal 1.2 (of 2) *) 915 RES_TAC >> take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 916 MATCH_MP_TAC TRACE2 \\ 917 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ], 918 (* goal 2 (of 2) *) 919 IMP_RES_TAC contracts_TRANS_label \\ 920 RES_TAC \\ 921 take [`label x :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 922 MATCH_MP_TAC TRACE2 \\ 923 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ]); 924 925val contracts_AND_TRACE1 = store_thm ( 926 "contracts_AND_TRACE1", 927 ``!E E'. E contracts E' ==> 928 !xs E1. TRACE E xs E1 ==> ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2``, 929 NTAC 2 (rpt GEN_TAC >> DISCH_TAC) 930 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] contracts_AND_TRACE1_lemma) 931 >> RW_TAC std_ss []); 932 933val contracts_AND_TRACE2_lemma = Q.prove ( 934 `!E xs E1. TRACE E xs E1 ==> 935 !E'. E contracts E' ==> 936 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ (LENGTH xs' <= LENGTH xs)`, 937 HO_MATCH_MP_TAC TRACE_strongind 938 >> rpt STRIP_TAC 939 >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [TRACE_REFL] \\ 940 REWRITE_TAC [LENGTH] >> RW_TAC arith_ss [] ) 941 >> Cases_on `h` (* 2 sub-goals here *) 942 >| [ (* goal 1 (of 2) *) 943 IMP_RES_TAC contracts_TRANS_tau >| (* 2 sub-goals here *) 944 [ (* goal 1.1 (of 2) *) 945 RES_TAC >> take [`xs'`, `E2`] >> ASM_REWRITE_TAC [] \\ 946 REWRITE_TAC [LENGTH] >> RW_TAC arith_ss [], 947 (* goal 1.2 (of 2) *) 948 RES_TAC >> take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 949 CONJ_TAC >| (* 2 sub-goals here *) 950 [ (* goal 1.2.1 (of 2) *) 951 MATCH_MP_TAC TRACE2 \\ 952 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 953 (* goal 1.2.2 (of 2) *) 954 REWRITE_TAC [LENGTH] >> RW_TAC arith_ss [] ] ], 955 (* goal 2 (of 2) *) 956 IMP_RES_TAC contracts_TRANS_label \\ 957 RES_TAC \\ 958 take [`label x :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 959 CONJ_TAC >| (* 2 sub-goals here *) 960 [ (* goal 2.1 (of 2) *) 961 MATCH_MP_TAC TRACE2 \\ 962 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 963 (* goal 2.2 (of 2) *) 964 REWRITE_TAC [LENGTH] >> RW_TAC arith_ss [] ] ]); 965 966val contracts_AND_TRACE2 = store_thm ( 967 "contracts_AND_TRACE2", 968 ``!E E'. E contracts E' ==> 969 !xs E1. TRACE E xs E1 ==> 970 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ (LENGTH xs' <= LENGTH xs)``, 971 NTAC 2 (rpt GEN_TAC >> DISCH_TAC) 972 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] contracts_AND_TRACE2_lemma) 973 >> RW_TAC std_ss []); 974 975val contracts_AND_TRACE_tau_lemma = Q.prove ( 976 `!E xs E1. TRACE E xs E1 ==> NO_LABEL xs ==> 977 !E'. E contracts E' ==> 978 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 979 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'`, 980 HO_MATCH_MP_TAC TRACE_strongind 981 >> rpt STRIP_TAC 982 >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [] \\ 983 REWRITE_TAC [TRACE_REFL, LENGTH] >> RW_TAC arith_ss [] ) 984 >> IMP_RES_TAC NO_LABEL_cases 985 >> qpat_x_assum `NO_LABEL xs ==> X` 986 (ASSUME_TAC o (fn thm => MATCH_MP thm (ASSUME ``NO_LABEL (xs :'b Action list)``))) 987 >> Cases_on `h` >> FULL_SIMP_TAC std_ss [Action_distinct_label, LENGTH] 988 >> IMP_RES_TAC contracts_TRANS_tau >> RES_TAC (* 2 sub-goals here *) 989 >| [ (* goal 1 (of 2) *) 990 take [`xs'`, `E2`] >> ASM_REWRITE_TAC [] \\ 991 FULL_SIMP_TAC arith_ss [], 992 (* goal 2 (of 2) *) 993 take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 994 CONJ_TAC 995 >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 996 Rev CONJ_TAC 997 >- ( POP_ASSUM MP_TAC >> KILL_TAC \\ 998 REWRITE_TAC [NO_LABEL_def, MEM, Action_distinct_label] ) \\ 999 REWRITE_TAC [LENGTH] \\ 1000 FULL_SIMP_TAC arith_ss [] ]); 1001 1002val contracts_AND_TRACE_tau = store_thm ( 1003 "contracts_AND_TRACE_tau", 1004 ``!E E'. E contracts E' ==> 1005 !xs E1. TRACE E xs E1 /\ NO_LABEL xs ==> 1006 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 1007 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'``, 1008 NTAC 2 (rpt GEN_TAC >> STRIP_TAC) 1009 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] contracts_AND_TRACE_tau_lemma) 1010 >> RW_TAC std_ss []); 1011 1012(* the version shown in the paper using P and Q *) 1013val contracts_AND_TRACE_tau' = store_thm ( 1014 "contracts_AND_TRACE_tau'", 1015 ``!P Q. P contracts Q ==> 1016 !xs P'. TRACE P xs P' /\ NO_LABEL xs ==> 1017 ?xs' Q'. TRACE Q xs' Q' /\ P' contracts Q' /\ 1018 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'``, 1019 METIS_TAC [contracts_AND_TRACE_tau]); 1020 1021val contracts_AND_TRACE_label_lemma = Q.prove ( 1022 `!E xs E1. TRACE E xs E1 ==> !l. UNIQUE_LABEL (label l) xs ==> 1023 !E'. E contracts E' ==> 1024 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 1025 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'`, 1026 HO_MATCH_MP_TAC TRACE_strongind 1027 >> rpt STRIP_TAC 1028 >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [] \\ 1029 REWRITE_TAC [TRACE_REFL, LENGTH] >> RW_TAC arith_ss [] ) 1030 >> REWRITE_TAC [LENGTH] 1031 >> Cases_on `h` (* 2 sub-goals here *) 1032 >| [ (* goal 1 (of 2) *) 1033 IMP_RES_TAC contracts_TRANS_tau >| (* 2 sub-goals here *) 1034 [ (* goal 1.1 (of 2) *) 1035 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases1) \\ 1036 RES_TAC \\ 1037 take [`xs'`, `E2`] >> ASM_REWRITE_TAC [] \\ 1038 FULL_SIMP_TAC arith_ss [], 1039 (* goal 1.2 (of 2) *) 1040 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases1) \\ 1041 RES_TAC \\ 1042 take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 1043 CONJ_TAC >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 1044 CONJ_TAC >- ( FULL_SIMP_TAC arith_ss [LENGTH] ) \\ 1045 REWRITE_TAC [UNIQUE_LABEL_cases1] >> ASM_REWRITE_TAC [] ], 1046 (* goal 2 of 2 *) 1047 IMP_RES_TAC contracts_TRANS_label \\ 1048 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases2) \\ 1049 IMP_RES_TAC (MATCH_MP contracts_AND_TRACE_tau (ASSUME ``E' contracts E2``)) \\ 1050 NTAC 4 (POP_ASSUM K_TAC) \\ 1051 take [`label x :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 1052 CONJ_TAC >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 1053 CONJ_TAC >- ( FULL_SIMP_TAC arith_ss [LENGTH] ) \\ 1054 REWRITE_TAC [UNIQUE_LABEL_cases2] >> ASM_REWRITE_TAC [] ]); 1055 1056val contracts_AND_TRACE_label = store_thm ( 1057 "contracts_AND_TRACE_label", 1058 ``!E E'. E contracts E' ==> 1059 !xs l E1. TRACE E xs E1 /\ UNIQUE_LABEL (label l) xs ==> 1060 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 1061 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'``, 1062 NTAC 2 (rpt GEN_TAC >> STRIP_TAC) 1063 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] contracts_AND_TRACE_label_lemma) 1064 >> RW_TAC std_ss []); 1065 1066(* the version shown in the paper using P and Q *) 1067val contracts_AND_TRACE_label' = store_thm ( 1068 "contracts_AND_TRACE_label'", 1069 ``!P Q. P contracts Q ==> 1070 !xs l P'. TRACE P xs P' /\ UNIQUE_LABEL (label l) xs ==> 1071 ?xs' Q'. TRACE Q xs' Q' /\ P contracts Q /\ 1072 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'``, 1073 METIS_TAC [contracts_AND_TRACE_label]); 1074 1075(******************************************************************************) 1076(* *) 1077(* Bisimulation Upto `contracts` and context *) 1078(* *) 1079(******************************************************************************) 1080 1081(* 1082val BISIM_UPTO_contracts_and_C = new_definition ( 1083 "BISIM_UPTO_contracts_and_C", 1084 ``BISIM_UPTO_contracts_and_C (Wbsm: ('a, 'b) simulation) = 1085 !E E'. 1086 Wbsm E E' ==> 1087 (!l. 1088 (!E1. TRANS E (label l) E1 ==> 1089 ?E2. WEAK_TRANS E' (label l) E2 /\ 1090 (WEAK_EQUIV O (GCC Wbsm) O $contracts) E1 E2) /\ 1091 (!E2. TRANS E' (label l) E2 ==> 1092 ?E1. WEAK_TRANS E (label l) E1 /\ 1093 ($contracts O (GCC Wbsm) O WEAK_EQUIV) E1 E2)) /\ 1094 (!E1. TRANS E tau E1 ==> 1095 ?E2. EPS E' E2 /\ (WEAK_EQUIV O (GCC Wbsm) O $contracts) E1 E2) /\ 1096 (!E2. TRANS E' tau E2 ==> 1097 ?E1. EPS E E1 /\ ($contracts O (GCC Wbsm) O WEAK_EQUIV) E1 E2)``); 1098 *) 1099 1100(******************************************************************************) 1101(* *) 1102(* Observational contraction (OBS_contracts) *) 1103(* *) 1104(******************************************************************************) 1105 1106val OBS_contracts = new_definition ("OBS_contracts", 1107 ``OBS_contracts (E :('a, 'b) CCS) (E' :('a, 'b) CCS) = 1108 (!(u :'b Action). 1109 (!E1. TRANS E u E1 ==> 1110 ?E2. TRANS E' u E2 /\ E1 contracts E2) /\ 1111 (!E2. TRANS E' u E2 ==> 1112 ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2))``); 1113 1114val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 1115 fixity = Infix (NONASSOC, 450), 1116 paren_style = OnlyIfNecessary, 1117 pp_elements = [HardSpace 1, TOK (UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D9C), 1118 BreakSpace (1,0)], 1119 term_name = "OBS_contracts" }; 1120 1121val _ = TeX_notation { hol = (UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D9C), 1122 TeX = ("\\HOLTokenObsContracts", 1) }; 1123 1124(* This one is difficult because `standard technique` doesn't work *) 1125val OBS_contracts_BY_CONTRACTION = store_thm ( 1126 "OBS_contracts_BY_CONTRACTION", 1127 ``!Con. CONTRACTION Con ==> 1128 !E E'. 1129 (!u. 1130 (!E1. TRANS E u E1 ==> 1131 (?E2. TRANS E' u E2 /\ Con E1 E2)) /\ 1132 (!E2. TRANS E' u E2 ==> 1133 (?E1. WEAK_TRANS E u E1 /\ Con E1 E2))) ==> OBS_contracts E E'``, 1134 rpt STRIP_TAC 1135 >> REWRITE_TAC [OBS_contracts] 1136 >> REWRITE_TAC [contracts_thm] 1137 >> GEN_TAC 1138 >> CONJ_TAC (* 2 sub-goals here *) 1139 >- ( rpt STRIP_TAC >> RES_TAC \\ 1140 Q.EXISTS_TAC `E2` >> art [] \\ 1141 Q.EXISTS_TAC `Con` >> art [] ) 1142 >> rpt STRIP_TAC >> RES_TAC 1143 >> Q.EXISTS_TAC `E1` >> art [] 1144 >> REWRITE_TAC [WEAK_EQUIV] 1145 >> Q.EXISTS_TAC `Con RUNION WEAK_EQUIV` (* here !!! *) 1146 >> REWRITE_TAC [RUNION] 1147 >> CONJ_TAC >- ( DISJ1_TAC >> art [] ) 1148 >> REWRITE_TAC [WEAK_BISIM, RUNION] >> rpt STRIP_TAC (* 8 sub-goals here *) 1149 >| [ (* goal 1 (of 8) *) 1150 IMP_RES_TAC 1151 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 1152 (ASSUME ``(Con :('a, 'b) simulation) E'' E'''``)) \\ 1153 Q.EXISTS_TAC `E2'` \\ 1154 CONJ_TAC >- ( MATCH_MP_TAC TRANS_IMP_WEAK_TRANS >> art [] ) \\ 1155 DISJ1_TAC >> art [], 1156 (* goal 2 (of 8) *) 1157 IMP_RES_TAC 1158 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 1159 (ASSUME ``(Con :('a, 'b) simulation) E'' E'''``)) \\ 1160 Q.EXISTS_TAC `E1'` >> art [], 1161 (* goal 3 (of 8) *) 1162 IMP_RES_TAC 1163 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 1164 (ASSUME ``(Con :('a, 'b) simulation) E'' E'''``)) (* 2 sub-goals here *) 1165 >- ( Q.EXISTS_TAC `E'''` >> art [EPS_REFL] ) \\ 1166 Q.EXISTS_TAC `E2'` >> art [] \\ 1167 IMP_RES_TAC ONE_TAU, 1168 (* goal 4 (of 8) *) 1169 IMP_RES_TAC 1170 (MATCH_MP (REWRITE_RULE [CONTRACTION] (ASSUME ``CONTRACTION Con``)) 1171 (ASSUME ``(Con :('a, 'b) simulation) E'' E'''``)) \\ 1172 Q.EXISTS_TAC `E1'` >> art [], 1173 (* goal 5 (of 8) *) 1174 IMP_RES_TAC WEAK_EQUIV_TRANS_label \\ 1175 Q.EXISTS_TAC `E2'` >> art [], 1176 (* goal 6 (of 8) *) 1177 IMP_RES_TAC WEAK_EQUIV_TRANS_label' \\ 1178 Q.EXISTS_TAC `E1'` >> art [], 1179 (* goal 7 (of 8) *) 1180 IMP_RES_TAC WEAK_EQUIV_TRANS_tau \\ 1181 Q.EXISTS_TAC `E2'` >> art [], 1182 (* goal 8 (of 8) *) 1183 IMP_RES_TAC WEAK_EQUIV_TRANS_tau' \\ 1184 Q.EXISTS_TAC `E1'` >> art [] ]); 1185 1186val OBS_contracts_TRANS_LEFT = store_thm ( 1187 "OBS_contracts_TRANS_LEFT", 1188 ``!E E'. OBS_contracts (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 1189 !u E1. TRANS E u E1 ==> ?E2. TRANS E' u E2 /\ E1 contracts E2``, 1190 PROVE_TAC [OBS_contracts]); 1191 1192val OBS_contracts_TRANS_RIGHT = store_thm ( 1193 "OBS_contracts_TRANS_RIGHT", 1194 ``!E E'. OBS_contracts (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 1195 !u E2. TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2``, 1196 PROVE_TAC [OBS_contracts]); 1197 1198val OBS_contracts_IMP_contracts = store_thm ( 1199 "OBS_contracts_IMP_contracts", ``!E E'. OBS_contracts E E' ==> E contracts E'``, 1200 rpt STRIP_TAC 1201 >> ONCE_REWRITE_TAC [contracts_cases] 1202 >> rpt STRIP_TAC (* 4 sub-goals here *) 1203 >| [ (* goal 1 (of 4) *) 1204 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1205 Q.EXISTS_TAC `E2` >> art [], 1206 (* goal 2 (of 4) *) 1207 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1208 Q.EXISTS_TAC `E1` >> art [], 1209 (* goal 3 (of 4) *) 1210 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1211 DISJ2_TAC >> Q.EXISTS_TAC `E2` >> art [], 1212 (* goal 2 (of 4) *) 1213 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1214 Q.EXISTS_TAC `E1` >> art [] \\ 1215 MATCH_MP_TAC WEAK_TRANS_IMP_EPS >> art [] ]); 1216 1217val OBS_contracts_IMP_WEAK_EQUIV = store_thm ( 1218 "OBS_contracts_IMP_WEAK_EQUIV", ``!E E'. OBS_contracts E E' ==> WEAK_EQUIV E E'``, 1219 rpt STRIP_TAC 1220 >> IMP_RES_TAC OBS_contracts_IMP_contracts 1221 >> IMP_RES_TAC contracts_IMP_WEAK_EQUIV); 1222 1223(* Know relations: 1224 1. `expands` << `contracts` << WEAK_EQUIV 1225 2. `OBS_contracts` << `contracts` 1226 3. `OBS_contracts` << OBS_CONGR << WEAK_EQUIV *) 1227val OBS_contracts_IMP_OBS_CONGR = store_thm ( 1228 "OBS_contracts_IMP_OBS_CONGR", ``!E E'. OBS_contracts E E' ==> OBS_CONGR E E'``, 1229 rpt STRIP_TAC 1230 >> REWRITE_TAC [OBS_CONGR] 1231 >> rpt STRIP_TAC (* 2 sub-goals here *) 1232 >| [ (* goal 1 (of 2) *) 1233 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1234 Q.EXISTS_TAC `E2` \\ 1235 CONJ_TAC >- IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 1236 IMP_RES_TAC contracts_IMP_WEAK_EQUIV, 1237 (* goal 2 (of 2) *) 1238 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1239 Q.EXISTS_TAC `E1` >> art [] ]); 1240 1241(* another way to prove this *) 1242val OBS_contracts_IMP_WEAK_EQUIV' = store_thm ( 1243 "OBS_contracts_IMP_WEAK_EQUIV'", ``!E E'. OBS_contracts E E' ==> WEAK_EQUIV E E'``, 1244 rpt STRIP_TAC 1245 >> MATCH_MP_TAC OBS_CONGR_IMP_WEAK_EQUIV 1246 >> IMP_RES_TAC OBS_contracts_IMP_OBS_CONGR); 1247 1248val OBS_contracts_EPS' = store_thm ( 1249 "OBS_contracts_EPS'", 1250 ``!E E'. OBS_contracts (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 1251 !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 1252 rpt STRIP_TAC 1253 >> PAT_X_ASSUM ``OBS_contracts E E'`` MP_TAC 1254 >> POP_ASSUM MP_TAC 1255 >> Q.SPEC_TAC (`E2`, `E2`) 1256 >> Q.SPEC_TAC (`E'`, `E'`) 1257 >> HO_MATCH_MP_TAC EPS_strongind_right (* must use right induct here! *) 1258 >> rpt STRIP_TAC (* 2 sub-goals here *) 1259 >| [ (* goal 1 (of 2) *) 1260 Q.EXISTS_TAC `E` >> REWRITE_TAC [EPS_REFL] \\ 1261 IMP_RES_TAC OBS_contracts_IMP_WEAK_EQUIV, 1262 (* goal 2 (of 2) *) 1263 RES_TAC \\ 1264 IMP_RES_TAC WEAK_EQUIV_TRANS_tau' \\ 1265 Q.EXISTS_TAC `E1'` >> art [] \\ 1266 IMP_RES_TAC EPS_TRANS ]); 1267 1268val OBS_contracts_WEAK_TRANS' = store_thm ( 1269 "OBS_contracts_WEAK_TRANS'", 1270 ``!E E'. OBS_contracts (E :('a, 'b) CCS) (E' :('a, 'b) CCS) ==> 1271 !u E2. WEAK_TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ WEAK_EQUIV E1 E2``, 1272 rpt STRIP_TAC 1273 >> Cases_on `u` (* 2 sub-goals here *) 1274 >| [ (* case 1 (of 2): u = tau *) 1275 IMP_RES_TAC WEAK_TRANS_TAU_IMP_TRANS_TAU \\ 1276 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1277 IMP_RES_TAC WEAK_EQUIV_EPS' \\ 1278 Q.EXISTS_TAC `E1''` >> art [] \\ 1279 MATCH_MP_TAC WEAK_TRANS_AND_EPS \\ 1280 Q.EXISTS_TAC `E1'` >> art [], 1281 (* case 2 (of 2): ~(u = tau) *) 1282 IMP_RES_TAC WEAK_TRANS \\ 1283 IMP_RES_TAC OBS_contracts_EPS' \\ 1284 IMP_RES_TAC WEAK_EQUIV_TRANS_label' \\ 1285 IMP_RES_TAC WEAK_EQUIV_EPS' \\ 1286 Q.EXISTS_TAC `E1'''` >> art [] \\ 1287 IMP_RES_TAC EPS_WEAK_EPS ]); 1288 1289(******************************************************************************) 1290(* *) 1291(* OBS_contracts is PreOrder *) 1292(* *) 1293(******************************************************************************) 1294 1295val OBS_contracts_TRANS = store_thm ( 1296 "OBS_contracts_TRANS", 1297 ``!E E' E''. OBS_contracts E E' /\ OBS_contracts E' E'' ==> OBS_contracts E E''``, 1298 rpt STRIP_TAC 1299 >> REWRITE_TAC [OBS_contracts] 1300 >> rpt STRIP_TAC (* 2 sub-goals here *) 1301 >| [ (* goal 1 (of 2) *) 1302 IMP_RES_TAC (REWRITE_RULE [OBS_contracts] (ASSUME ``OBS_contracts E E'``)) \\ 1303 IMP_RES_TAC (REWRITE_RULE [OBS_contracts] (ASSUME ``OBS_contracts E' E''``)) \\ 1304 Q.EXISTS_TAC `E2'` >> art [] \\ 1305 IMP_RES_TAC contracts_TRANS, 1306 (* goal 2 (of 2) *) 1307 IMP_RES_TAC (REWRITE_RULE [OBS_contracts] (ASSUME ``OBS_contracts E' E''``)) \\ 1308 IMP_RES_TAC OBS_contracts_WEAK_TRANS' \\ 1309 Q.EXISTS_TAC `E1'` >> art [] \\ 1310 IMP_RES_TAC WEAK_EQUIV_TRANS ]); 1311 1312val OBS_contracts_REFL = store_thm ( 1313 "OBS_contracts_REFL", ``!E. OBS_contracts E E``, 1314 GEN_TAC 1315 >> REWRITE_TAC [OBS_contracts] 1316 >> rpt STRIP_TAC 1317 >- ( Q.EXISTS_TAC `E1` >> art [contracts_REFL] ) 1318 >> Q.EXISTS_TAC `E2` >> REWRITE_TAC [WEAK_EQUIV_REFL] 1319 >> IMP_RES_TAC TRANS_IMP_WEAK_TRANS); 1320 1321val OBS_contracts_PreOrder = store_thm ( 1322 "OBS_contracts_PreOrder", ``PreOrder OBS_contracts``, 1323 REWRITE_TAC [PreOrder, reflexive_def, transitive_def] 1324 >> CONJ_TAC >- REWRITE_TAC [OBS_contracts_REFL] 1325 >> rpt STRIP_TAC 1326 >> MATCH_MP_TAC OBS_contracts_TRANS 1327 >> Q.EXISTS_TAC `y` >> art []); 1328 1329(******************************************************************************) 1330(* *) 1331(* OBS_contracts is precongruence *) 1332(* *) 1333(******************************************************************************) 1334 1335(* Proposition 6 (Milner's book, page 154), the version for `contracts` *) 1336val contracts_PROP6 = store_thm ( 1337 "contracts_PROP6", 1338 ``!E E'. E contracts E' ==> !u. OBS_contracts (prefix u E) (prefix u E')``, 1339 rpt GEN_TAC 1340 >> PURE_ONCE_REWRITE_TAC [OBS_contracts] 1341 >> rpt STRIP_TAC (* 2 sub-goals here *) 1342 >| [ (* goal 1 (of 2) *) 1343 IMP_RES_TAC TRANS_PREFIX \\ 1344 Q.EXISTS_TAC `E'` >> art [] \\ 1345 REWRITE_TAC [PREFIX], 1346 (* goal 2 (of 2) *) 1347 IMP_RES_TAC TRANS_PREFIX \\ 1348 Q.EXISTS_TAC `E` >> art [] \\ 1349 CONJ_TAC >- REWRITE_TAC [WEAK_PREFIX] \\ 1350 IMP_RES_TAC contracts_IMP_WEAK_EQUIV ]); 1351 1352val OBS_contracts_SUBST_PREFIX = store_thm ( 1353 "OBS_contracts_SUBST_PREFIX", 1354 ``!E E'. OBS_contracts E E' ==> !u. OBS_contracts (prefix u E) (prefix u E')``, 1355 rpt STRIP_TAC 1356 >> IMP_RES_TAC OBS_contracts_IMP_contracts 1357 >> MATCH_MP_TAC contracts_PROP6 >> art []); 1358 1359val OBS_contracts_PRESD_BY_SUM = store_thm ( 1360 "OBS_contracts_PRESD_BY_SUM", 1361 ``!E1 E1' E2 E2'. OBS_contracts E1 E1' /\ OBS_contracts E2 E2' ==> 1362 OBS_contracts (sum E1 E2) (sum E1' E2')``, 1363 rpt GEN_TAC 1364 >> REWRITE_TAC [OBS_contracts] 1365 >> rpt STRIP_TAC (* 2 sub-goals here *) 1366 >| [ (* goal 1 (of 2) *) 1367 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 1368 [ (* goal 1.1 (of 2) *) 1369 RES_TAC >> Q.EXISTS_TAC `E2''` >> art [] \\ 1370 MATCH_MP_TAC SUM1 >> art [], 1371 (* goal 1.2 (of 2) *) 1372 RES_TAC >> Q.EXISTS_TAC `E2''` >> art [] \\ 1373 MATCH_MP_TAC SUM2 >> art [] ], 1374 (* goal 2 (of 2) *) 1375 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 1376 [ (* goal 2.1 (of 2) *) 1377 RES_TAC >> Q.EXISTS_TAC `E1''` >> art [] \\ 1378 MATCH_MP_TAC WEAK_SUM1 >> art [], 1379 (* goal 2.2 (of 2) *) 1380 RES_TAC >> Q.EXISTS_TAC `E1''` >> art [] \\ 1381 MATCH_MP_TAC WEAK_SUM2 >> art [] ] ]); 1382 1383(* |- !E E'. OBS_contracts E E' ==> !E''. OBS_contracts (sum E'' E) (sum E'' E') *) 1384val OBS_contracts_SUBST_SUM_L = save_thm ( 1385 "OBS_contracts_SUBST_SUM_L", 1386 Q_GENL [`E`, `E'`] 1387 (DISCH ``OBS_contracts E E'`` 1388 (Q.GEN `E''` 1389 (MATCH_MP OBS_contracts_PRESD_BY_SUM 1390 (CONJ (Q.SPEC `E''` OBS_contracts_REFL) 1391 (ASSUME ``OBS_contracts E E'``)))))); 1392 1393(* |- !E E'. OBS_contracts E E' ==> !E''. OBS_contracts (sum E E'') (sum E' E'') *) 1394val OBS_contracts_SUBST_SUM_R = save_thm ( 1395 "OBS_contracts_SUBST_SUM_R", 1396 Q_GENL [`E`, `E'`] 1397 (DISCH ``OBS_contracts E E'`` 1398 (Q.GEN `E''` 1399 (MATCH_MP OBS_contracts_PRESD_BY_SUM 1400 (CONJ (ASSUME ``OBS_contracts E E'``) 1401 (Q.SPEC `E''` OBS_contracts_REFL)))))); 1402 1403(* this belongs to ContractionLib.sml *) 1404fun C_TRANS thm1 thm2 = 1405 if (rhs_tm thm1 = lhs_tm thm2) then 1406 MATCH_MP contracts_TRANS (CONJ thm1 thm2) 1407 else 1408 failwith "transitivity of contraction not applicable"; 1409 1410(* Observation contracts is preserved by parallel composition. *) 1411val OBS_contracts_PRESD_BY_PAR = store_thm ( 1412 "OBS_contracts_PRESD_BY_PAR", 1413 ``!E1 E1' E2 E2'. OBS_contracts E1 E1' /\ OBS_contracts E2 E2' ==> 1414 OBS_contracts (par E1 E2) (par E1' E2')``, 1415 rpt STRIP_TAC 1416 >> REWRITE_TAC [OBS_contracts] 1417 >> rpt STRIP_TAC (* 2 sub-goals here *) 1418 >| [ (* goal 1 (of 2) *) 1419 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1420 [ (* goal 1.1 (of 3) *) 1421 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1422 ASSUME_TAC (Q.SPEC `E2'` 1423 (MATCH_MP PAR1 (ASSUME ``TRANS E1' u E2''``))) \\ 1424 EXISTS_TAC ``par E2'' E2'`` \\ 1425 ASM_REWRITE_TAC 1426 [C_TRANS (Q.SPEC `E2` 1427 (MATCH_MP contracts_SUBST_PAR_R 1428 (ASSUME ``E1''' contracts E2''``))) 1429 (Q.SPEC `E2''` 1430 (MATCH_MP contracts_SUBST_PAR_L 1431 (MATCH_MP OBS_contracts_IMP_contracts 1432 (ASSUME ``OBS_contracts E2 E2'``))))], 1433 (* goal 1.2 (of 3) *) 1434 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1435 ASSUME_TAC (Q.SPEC `E1'` 1436 (MATCH_MP PAR2 (ASSUME ``TRANS E2' u E2''``))) \\ 1437 EXISTS_TAC ``par E1' E2''`` \\ 1438 ASM_REWRITE_TAC 1439 [C_TRANS (Q.SPEC `E1'''` 1440 (MATCH_MP contracts_SUBST_PAR_R 1441 (MATCH_MP OBS_contracts_IMP_contracts 1442 (ASSUME ``OBS_contracts E1 E1'``)))) 1443 (Q.SPEC `E1'` 1444 (MATCH_MP contracts_SUBST_PAR_L 1445 (ASSUME ``E1''' contracts E2''``)))], 1446 (* goal 1.3 (of 3) *) 1447 IMP_RES_TAC (MATCH_MP OBS_contracts_TRANS_LEFT (ASSUME ``OBS_contracts E1 E1'``)) \\ 1448 IMP_RES_TAC (MATCH_MP OBS_contracts_TRANS_LEFT (ASSUME ``OBS_contracts E2 E2'``)) \\ 1449 EXISTS_TAC ``par E2''' E2''''`` \\ 1450 ASM_REWRITE_TAC 1451 [C_TRANS (Q.SPEC `E2''` 1452 (MATCH_MP contracts_SUBST_PAR_R 1453 (ASSUME ``E1''' contracts E2'''``))) 1454 (Q.SPEC `E2'''` 1455 (MATCH_MP contracts_SUBST_PAR_L 1456 (ASSUME ``E2'' contracts E2''''``)))] \\ 1457 MATCH_MP_TAC PAR3 \\ 1458 Q.EXISTS_TAC `l` >> art [] ], 1459 (* goal 2 (of 2) *) 1460 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1461 [ (* goal 2.1 (of 3) *) 1462 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1463 ASSUME_TAC (CONJUNCT1 1464 (Q.SPEC `E2` 1465 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E1 u E1'''``)))) \\ 1466 EXISTS_TAC ``par E1''' E2`` \\ 1467 ASM_REWRITE_TAC 1468 [OE_TRANS (Q.SPEC `E2` 1469 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 1470 (ASSUME ``WEAK_EQUIV E1''' E1''``))) 1471 (Q.SPEC `E1''` 1472 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 1473 (MATCH_MP OBS_contracts_IMP_WEAK_EQUIV 1474 (ASSUME ``OBS_contracts E2 E2'``))))], 1475 (* goal 2.2 (of 3) *) 1476 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1477 ASSUME_TAC (CONJUNCT2 1478 (Q.SPEC `E1` 1479 (MATCH_MP WEAK_PAR (ASSUME ``WEAK_TRANS E2 u E1'''``)))) \\ 1480 EXISTS_TAC ``par E1 E1'''`` \\ 1481 ASM_REWRITE_TAC 1482 [OE_TRANS (Q.SPEC `E1'''` 1483 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 1484 (MATCH_MP OBS_contracts_IMP_WEAK_EQUIV 1485 (ASSUME ``OBS_contracts E1 E1'``)))) 1486 (Q.SPEC `E1'` 1487 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 1488 (ASSUME ``WEAK_EQUIV E1''' E1''``)))], 1489 (* goal 2.3 (of 3) *) 1490 IMP_RES_TAC (MATCH_MP OBS_contracts_TRANS_RIGHT (ASSUME ``OBS_contracts E1 E1'``)) \\ 1491 IMP_RES_TAC (MATCH_MP OBS_contracts_TRANS_RIGHT (ASSUME ``OBS_contracts E2 E2'``)) \\ 1492 EXISTS_TAC ``par E1''' E1''''`` \\ 1493 ASM_REWRITE_TAC 1494 [OE_TRANS (Q.SPEC `E1''''` 1495 (MATCH_MP WEAK_EQUIV_SUBST_PAR_R 1496 (ASSUME ``WEAK_EQUIV E1''' E1''``))) 1497 (Q.SPEC `E1''` 1498 (MATCH_MP WEAK_EQUIV_SUBST_PAR_L 1499 (ASSUME ``WEAK_EQUIV E1'''' E2'''``)))] \\ 1500 PURE_ONCE_REWRITE_TAC [WEAK_TRANS] \\ 1501 STRIP_ASSUME_TAC 1502 (REWRITE_RULE [WEAK_TRANS] 1503 (ASSUME ``WEAK_TRANS E1 (label l) E1'''``)) \\ 1504 STRIP_ASSUME_TAC 1505 (REWRITE_RULE [WEAK_TRANS] 1506 (ASSUME ``WEAK_TRANS E2 (label (COMPL l)) E1''''``)) \\ 1507 EXISTS_TAC ``par E1''''' E1''''''`` \\ 1508 EXISTS_TAC ``par E2'''' E2'''''`` \\ 1509 REWRITE_TAC 1510 [MATCH_MP EPS_PAR_PAR 1511 (CONJ (ASSUME ``EPS E1 E1'''''``) 1512 (ASSUME ``EPS E2 E1''''''``)), 1513 MATCH_MP EPS_PAR_PAR 1514 (CONJ (ASSUME ``EPS E2'''' E1'''``) 1515 (ASSUME ``EPS E2''''' E1''''``))] \\ 1516 MATCH_MP_TAC PAR3 \\ 1517 Q.EXISTS_TAC `l` >> art [] ] ]); 1518 1519(* |- !E E'. OBS_contracts E E' ==> !E''. OBS_contracts (par E'' E) (par E'' E') *) 1520val OBS_contracts_SUBST_PAR_L = save_thm ( 1521 "OBS_contracts_SUBST_PAR_L", 1522 Q_GENL [`E`, `E'`] 1523 (DISCH ``OBS_contracts E E'`` 1524 (Q.GEN `E''` 1525 (MATCH_MP OBS_contracts_PRESD_BY_PAR 1526 (CONJ (Q.SPEC `E''` OBS_contracts_REFL) 1527 (ASSUME ``OBS_contracts E E'``)))))); 1528 1529(* |- !E E'. OBS_contracts E E' ==> !E''. OBS_contracts (par E E'') (par E' E'') *) 1530val OBS_contracts_SUBST_PAR_R = save_thm ( 1531 "OBS_contracts_SUBST_PAR_R", 1532 Q_GENL [`E`, `E'`] 1533 (DISCH ``OBS_contracts E E'`` 1534 (Q.GEN `E''` 1535 (MATCH_MP OBS_contracts_PRESD_BY_PAR 1536 (CONJ (ASSUME ``OBS_contracts E E'``) 1537 (Q.SPEC `E''` OBS_contracts_REFL)))))); 1538 1539val OBS_contracts_SUBST_RESTR = store_thm ( 1540 "OBS_contracts_SUBST_RESTR", 1541 ``!E E'. OBS_contracts E E' ==> !L. OBS_contracts (restr L E) (restr L E')``, 1542 rpt GEN_TAC 1543 >> PURE_ONCE_REWRITE_TAC [OBS_contracts] 1544 >> rpt STRIP_TAC (* 2 sub-goals here *) 1545 >| [ (* goal 1 (of 2) *) 1546 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1547 [ (* goal 1.1 (of 2) *) 1548 RES_TAC \\ 1549 Q.EXISTS_TAC `restr L E2` \\ 1550 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> art [] ) \\ 1551 IMP_RES_TAC contracts_SUBST_RESTR >> art [], 1552 (* goal 1.2 (of 2) *) 1553 RES_TAC \\ 1554 Q.EXISTS_TAC `restr L E2` >> art [] \\ 1555 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> Q.EXISTS_TAC `l` >> rfs [] ) \\ 1556 IMP_RES_TAC contracts_SUBST_RESTR >> art [] ], 1557 (* goal 2 (of 2) *) 1558 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1559 [ (* goal 2.1 (of 2) *) 1560 RES_TAC \\ 1561 ASSUME_TAC 1562 (MATCH_MP WEAK_RESTR_tau 1563 (REWRITE_RULE [ASSUME ``(u :'b Action) = tau``] 1564 (ASSUME ``WEAK_TRANS E u E1``))) \\ 1565 Q.EXISTS_TAC `restr L E1` \\ 1566 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> art [], 1567 (* goal 2.2 (of 2) *) 1568 RES_TAC \\ 1569 ASSUME_TAC 1570 (MATCH_MP WEAK_RESTR_label 1571 (LIST_CONJ [ASSUME ``~((l: 'b Label) IN L)``, 1572 ASSUME ``~((COMPL (l :'b Label)) IN L)``, 1573 REWRITE_RULE [ASSUME ``(u :'b Action) = label l``] 1574 (ASSUME ``WEAK_TRANS E u E1``)])) \\ 1575 Q.EXISTS_TAC `restr L E1` \\ 1576 IMP_RES_TAC WEAK_EQUIV_SUBST_RESTR >> art [] ] ]); 1577 1578(* Observation congruence is substitutive under the relabelling operator. *) 1579val OBS_contracts_SUBST_RELAB = store_thm ( 1580 "OBS_contracts_SUBST_RELAB", 1581 ``!E E'. OBS_contracts E E' ==> !rf. OBS_contracts (relab E rf) (relab E' rf)``, 1582 rpt GEN_TAC 1583 >> PURE_ONCE_REWRITE_TAC [OBS_contracts] 1584 >> rpt STRIP_TAC (* 2 sub-goals here, sharing start&end tacticals *) 1585 >> IMP_RES_TAC TRANS_RELAB 1586 >> RES_TAC 1587 >| [ (* goal 1 (of 2) *) 1588 Q.EXISTS_TAC `relab E2 rf` >> art [] \\ 1589 CONJ_TAC >- ( MATCH_MP_TAC RELABELING >> art [] ) \\ 1590 IMP_RES_TAC contracts_SUBST_RELAB >> art [], 1591 (* goal 2 (of 2) *) 1592 ASSUME_TAC (MATCH_MP WEAK_RELAB_rf 1593 (ASSUME ``WEAK_TRANS E u' E1``)) \\ 1594 Q.EXISTS_TAC `relab E1 rf` >> art [] \\ 1595 IMP_RES_TAC WEAK_EQUIV_SUBST_RELAB >> art [] ]); 1596 1597val OBS_contracts_SUBST_CONTEXT = store_thm ( 1598 "OBS_contracts_SUBST_CONTEXT", 1599 ``!P Q. OBS_contracts P Q ==> !E. CONTEXT E ==> OBS_contracts (E P) (E Q)``, 1600 rpt GEN_TAC >> DISCH_TAC 1601 >> Induct_on `CONTEXT` 1602 >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 1603 >- ASM_REWRITE_TAC [] 1604 >- REWRITE_TAC [OBS_contracts_REFL] 1605 >| [ (* goal 1 (of 5) *) 1606 MATCH_MP_TAC OBS_contracts_SUBST_PREFIX >> art [], 1607 (* goal 2 (of 5) *) 1608 MATCH_MP_TAC OBS_contracts_PRESD_BY_SUM >> art [], 1609 (* goal 3 (of 5) *) 1610 IMP_RES_TAC OBS_contracts_PRESD_BY_PAR, 1611 (* goal 4 (of 5) *) 1612 MATCH_MP_TAC OBS_contracts_SUBST_RESTR >> art [], 1613 (* goal 5 (of 5) *) 1614 MATCH_MP_TAC OBS_contracts_SUBST_RELAB >> art [] ]); 1615 1616val OBS_contracts_precongruence = store_thm ( 1617 "OBS_contracts_precongruence", ``precongruence OBS_contracts``, 1618 PROVE_TAC [precongruence_def, OBS_contracts_PreOrder, 1619 OBS_contracts_SUBST_CONTEXT]); 1620 1621(******************************************************************************) 1622(* *) 1623(* OBS_contracts and trace *) 1624(* *) 1625(******************************************************************************) 1626 1627val OBS_contracts_AND_TRACE_tau = store_thm ( 1628 "OBS_contracts_AND_TRACE_tau", 1629 ``!E E'. OBS_contracts E E' ==> 1630 !xs l E1. TRACE E xs E1 /\ NO_LABEL xs ==> 1631 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 1632 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'``, 1633 rpt STRIP_TAC 1634 >> IMP_RES_TAC TRACE_cases1 1635 >> Cases_on `xs` (* 2 sub-goals here *) 1636 >- ( take [`[]`, `E'`] >> REWRITE_TAC [TRACE_rule0] \\ 1637 fs [NULL] >> IMP_RES_TAC OBS_contracts_IMP_contracts ) 1638 >> fs [NULL] 1639 >> IMP_RES_TAC NO_LABEL_cases >> fs [] 1640 >> IMP_RES_TAC OBS_contracts_TRANS_LEFT 1641 >> MP_TAC (Q.SPECL [`t`, `E1`] 1642 (MATCH_MP (Q.SPECL [`u`, `E2`] contracts_AND_TRACE_tau) 1643 (ASSUME ``u contracts E2``))) 1644 >> RW_TAC std_ss [] 1645 >> take [`tau :: xs'`, `E2'`] >> art [] 1646 >> CONJ_TAC 1647 >- ( MATCH_MP_TAC TRACE_rule1 >> Q.EXISTS_TAC `E2` >> art [] ) 1648 >> RW_TAC arith_ss [LENGTH] 1649 >> REWRITE_TAC [NO_LABEL_cases] >> art []); 1650 1651val OBS_contracts_AND_TRACE_label = store_thm ( 1652 "OBS_contracts_AND_TRACE_label", 1653 ``!E E'. OBS_contracts E E' ==> 1654 !xs l E1. TRACE E xs E1 /\ UNIQUE_LABEL (label l) xs ==> 1655 ?xs' E2. TRACE E' xs' E2 /\ E1 contracts E2 /\ 1656 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'``, 1657 rpt STRIP_TAC 1658 >> IMP_RES_TAC TRACE_cases1 1659 >> Cases_on `xs` (* 2 sub-goals here *) 1660 >- ( take [`[]`, `E'`] >> REWRITE_TAC [TRACE_rule0] \\ 1661 fs [NULL] >> IMP_RES_TAC OBS_contracts_IMP_contracts ) 1662 >> Cases_on `h` (* 2 sub-goals here *) 1663 >| [ (* goal 1 (of 2) *) 1664 fs [UNIQUE_LABEL_cases1] \\ 1665 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1666 MP_TAC (Q.SPECL [`t`, `l`, `E1`] 1667 (MATCH_MP (Q.SPECL [`u`, `E2`] contracts_AND_TRACE_label) 1668 (ASSUME ``u contracts E2``))) \\ 1669 RW_TAC std_ss [] \\ 1670 take [`tau :: xs'`, `E2'`] >> art [] \\ 1671 CONJ_TAC >- ( MATCH_MP_TAC TRACE_rule1 >> Q.EXISTS_TAC `E2` >> art [] ) \\ 1672 RW_TAC arith_ss [LENGTH] \\ 1673 REWRITE_TAC [UNIQUE_LABEL_cases1] >> art [], 1674 (* goal 2 (of 2) *) 1675 fs [UNIQUE_LABEL_cases2] \\ 1676 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 1677 MP_TAC (Q.SPECL [`t`, `E1`] 1678 (MATCH_MP (Q.SPECL [`u`, `E2`] contracts_AND_TRACE_tau) 1679 (ASSUME ``u contracts E2``))) \\ 1680 RW_TAC std_ss [] \\ 1681 take [`label l :: xs'`, `E2'`] >> art [] \\ 1682 CONJ_TAC >- ( MATCH_MP_TAC TRACE_rule1 >> Q.EXISTS_TAC `E2` >> art [] ) \\ 1683 RW_TAC arith_ss [LENGTH] \\ 1684 REWRITE_TAC [UNIQUE_LABEL_cases2] >> art [] ]); 1685 1686val OBS_contracts_WEAK_TRANS_label' = store_thm ( 1687 "OBS_contracts_WEAK_TRANS_label'", 1688 ``!E E'. OBS_contracts E E' ==> 1689 !l E2. WEAK_TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ WEAK_EQUIV E1 E2``, 1690 rpt STRIP_TAC 1691 >> IMP_RES_TAC WEAK_TRANS_cases1 (* 2 sub-goals here *) 1692 >| [ (* goal 1 (of 2) *) 1693 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1694 IMP_RES_TAC WEAK_EQUIV_WEAK_TRANS_label' \\ 1695 Q.EXISTS_TAC `E1'` >> art [] \\ 1696 IMP_RES_TAC WEAK_TRANS_IMP_EPS \\ 1697 MATCH_MP_TAC EPS_AND_WEAK_TRANS \\ 1698 Q.EXISTS_TAC `E1` >> art [], 1699 (* goal 2 (of 2) *) 1700 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 1701 IMP_RES_TAC WEAK_EQUIV_EPS' \\ 1702 Q.EXISTS_TAC `E1'` >> art [] \\ 1703 MATCH_MP_TAC WEAK_TRANS_AND_EPS \\ 1704 Q.EXISTS_TAC `E1` >> art [] ]); 1705 1706val OBS_contracts_EPS' = store_thm ( 1707 "OBS_contracts_EPS'", 1708 ``!E E'. OBS_contracts E E' ==> !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ WEAK_EQUIV E1 E2``, 1709 rpt STRIP_TAC 1710 >> IMP_RES_TAC EPS_cases1 (* 2 sub-goals here *) 1711 >- ( Q.EXISTS_TAC `E` >> fs [EPS_REFL] \\ 1712 IMP_RES_TAC OBS_contracts_IMP_WEAK_EQUIV ) 1713 >> IMP_RES_TAC OBS_contracts_TRANS_RIGHT 1714 >> IMP_RES_TAC WEAK_EQUIV_EPS' 1715 >> Q.EXISTS_TAC `E1'` >> art [] 1716 >> IMP_RES_TAC WEAK_TRANS_IMP_EPS 1717 >> IMP_RES_TAC EPS_TRANS); 1718 1719(******************************************************************************) 1720(* *) 1721(* Is OBS_contracts coarsest precongruence contained in `contracts`? *) 1722(* *) 1723(******************************************************************************) 1724 1725(* (pre)congruence closure of `contracts` relation *) 1726val C_contracts = new_definition ( 1727 "C_contracts", ``C_contracts = CC $contracts``); 1728 1729(* |- C_contracts = (��g h. ���c. CONTEXT c ��� c g ������ c h) *) 1730val C_contracts_thm = save_thm ( 1731 "C_contracts_thm", REWRITE_RULE [CC_def] C_contracts); 1732 1733val C_contracts_precongruence = store_thm ( 1734 "C_contracts_precongruence", ``precongruence $C_contracts``, 1735 PROVE_TAC [C_contracts, CC_precongruence, contracts_PreOrder]); 1736 1737val OBS_contracts_IMP_C_contracts = store_thm ( 1738 "OBS_contracts_IMP_C_contracts", ``!p q. OBS_contracts p q ==> C_contracts p q``, 1739 REWRITE_TAC [C_contracts, GSYM RSUBSET] 1740 >> ASSUME_TAC OBS_contracts_precongruence 1741 >> `OBS_contracts RSUBSET $contracts` 1742 by PROVE_TAC [OBS_contracts_IMP_contracts, GSYM RSUBSET] 1743 >> MATCH_MP_TAC CC_is_coarsest' >> art []); 1744 1745val SUM_contracts = new_definition ("SUM_contracts", 1746 ``SUM_contracts = (\p q. !r. (sum p r) contracts (sum q r))``); 1747 1748val C_contracts_IMP_SUM_contracts = store_thm ( 1749 "C_contracts_IMP_SUM_contracts", 1750 ``!p q. C_contracts p q ==> SUM_contracts p q``, 1751 REWRITE_TAC [C_contracts, SUM_contracts, CC_def] 1752 >> BETA_TAC >> rpt STRIP_TAC 1753 >> POP_ASSUM MP_TAC 1754 >> Know `CONTEXT (\(t :('a, 'b) CCS). t) /\ CONTEXT (\t. r)` 1755 >- REWRITE_TAC [CONTEXT1, CONTEXT2] 1756 >> DISCH_TAC 1757 >> POP_ASSUM (ASSUME_TAC o (MATCH_MP CONTEXT4)) 1758 >> DISCH_TAC >> RES_TAC 1759 >> POP_ASSUM (MP_TAC o BETA_RULE) >> Rewr); 1760 1761val OBS_contracts_IMP_SUM_contracts = store_thm ( 1762 "OBS_contracts_IMP_SUM_contracts", 1763 ``!p q. OBS_contracts p q ==> SUM_contracts p q``, 1764 rpt STRIP_TAC 1765 >> MATCH_MP_TAC C_contracts_IMP_SUM_contracts 1766 >> IMP_RES_TAC OBS_contracts_IMP_C_contracts); 1767 1768(* OBS_contracts ==> C_contracts (coarsest) ==> SUM_contracts 1769 /\ || 1770 || || 1771 ++===================<<<====================++ *) 1772val SUM_contracts_IMP_OBS_contracts = store_thm ( 1773 "SUM_contracts_IMP_OBS_contracts", 1774 ``!p q. free_action p /\ free_action q ==> 1775 (SUM_contracts p q ==> OBS_contracts p q)``, 1776 REWRITE_TAC [SUM_contracts, free_action_def, OBS_contracts] 1777 >> BETA_TAC 1778 >> Rev (rpt STRIP_TAC) (* 2 sub-goals here *) 1779 >| [ (* goal 1 (of 2), same as goal 2 of COARSEST_CONGR_RL *) 1780 ASSUME_TAC (Q.SPEC `prefix (label a') nil` 1781 (ASSUME ``!r. (sum p r) contracts (sum q r)``)) \\ 1782 IMP_RES_TAC SUM1 \\ 1783 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a') nil`)) \\ 1784 Cases_on `u` >| (* 2 sub-goals here *) 1785 [ (* goal 1.1 (of 2) *) 1786 STRIP_ASSUME_TAC (MATCH_MP contracts_TRANS_tau' 1787 (ASSUME ``$contracts (sum p (prefix (label a') nil)) 1788 (sum q (prefix (label a') nil))``)) \\ 1789 RES_TAC \\ 1790 IMP_RES_TAC EPS_cases1 >| (* 2 sub-goals here *) 1791 [ (* goal 1.1.1 (of 2) *) 1792 `TRANS E1 (label a') nil` by RW_TAC std_ss [SUM2, PREFIX] \\ 1793 STRIP_ASSUME_TAC (MATCH_MP WEAK_EQUIV_TRANS_label 1794 (ASSUME ``WEAK_EQUIV E1 E2``)) \\ 1795 RES_TAC \\ 1796 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 1797 RES_TAC, (* initial assumption of `q` is used here *) 1798 (* goal 1.1.2 (of 2) *) 1799 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau u`` 1800 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1801 [ (* goal 1.1.2.1 (of 4) *) 1802 Q.EXISTS_TAC `E1` >> art [] \\ 1803 REWRITE_TAC [WEAK_TRANS] \\ 1804 take [`p`, `u`] >> art [EPS_REFL], 1805 (* goal 1.1.2.2 (of 4) *) 1806 IMP_RES_TAC TRANS_PREFIX \\ 1807 RW_TAC std_ss [Action_distinct] ] ], 1808 (* goal 1.2 (of 2) *) 1809 STRIP_ASSUME_TAC (MATCH_MP contracts_TRANS_label' 1810 (ASSUME ``$contracts (sum p (prefix (label a') nil)) 1811 (sum q (prefix (label a') nil))``)) \\ 1812 RES_TAC \\ 1813 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 1814 [ (* goal 1.2.1 (of 2) *) 1815 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) tau E'`` 1816 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1817 [ (* goal 1.2.1.1 (of 2) *) 1818 Q.EXISTS_TAC `E1` >> art [] \\ 1819 IMP_RES_TAC TRANS_TAU_AND_WEAK, 1820 (* goal 1.2.1.2 (of 2) *) 1821 IMP_RES_TAC TRANS_PREFIX \\ 1822 RW_TAC std_ss [Action_distinct] ], 1823 (* goal 1.2.2 (of 2) *) 1824 PAT_X_ASSUM ``TRANS (sum p (prefix (label a') nil)) (label L) E'`` 1825 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1826 [ (* goal 1.2.2.1 (of 2) *) 1827 Q.EXISTS_TAC `E1` >> art [] \\ 1828 REWRITE_TAC [WEAK_TRANS] \\ 1829 take [`p`, `E'`] >> art [EPS_REFL], 1830 (* goal 1.2.2.2 (of 2) *) 1831 IMP_RES_TAC TRANS_PREFIX \\ 1832 PAT_X_ASSUM ``label L = label a'`` (ASSUME_TAC o (REWRITE_RULE [Action_11])) \\ 1833 `TRANS q (label a') E2` by RW_TAC std_ss [] \\ 1834 POP_ASSUM (ASSUME_TAC o (MATCH_MP TRANS_IMP_WEAK_TRANS)) \\ 1835 RES_TAC ] ] ], (* initial assumption of `q` is used here *) 1836 (* goal 2 (of 2) *) 1837 ASSUME_TAC (Q.SPEC `prefix (label a) nil` 1838 (ASSUME ``!r. (sum p r) contracts (sum q r)``)) \\ 1839 IMP_RES_TAC SUM1 \\ 1840 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) nil`)) \\ 1841 Cases_on `u` >| (* 2 sub-goals here *) 1842 [ (* goal 2.1 (of 2) *) 1843 STRIP_ASSUME_TAC (MATCH_MP contracts_TRANS_tau 1844 (ASSUME ``$contracts (sum p (prefix (label a) nil)) 1845 (sum q (prefix (label a) nil))``)) \\ 1846 RES_TAC >| (* 2 sub-goals here *) 1847 [ (* goal 2.1.1 (of 2) *) 1848 Q.ABBREV_TAC `E2 = q + label a..nil` \\ 1849 `TRANS E2 (label a) nil` by PROVE_TAC [SUM2, PREFIX] \\ 1850 STRIP_ASSUME_TAC (MATCH_MP contracts_TRANS_label' 1851 (ASSUME ``E1 contracts E2``)) \\ 1852 RES_TAC \\ 1853 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 1854 RES_TAC, (* initial assumption of `p` is used here *) 1855 (* goal 2.1.2 (of 2) *) 1856 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) tau E2`` 1857 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1858 [ (* goal 2.1.2.1 (of 4) *) 1859 Q.EXISTS_TAC `E2` >> art [], 1860 (* goal 2.1.2.2 (of 4) *) 1861 IMP_RES_TAC TRANS_PREFIX \\ 1862 RW_TAC std_ss [Action_distinct] ] ], 1863 (* goal 2.2 (of 2) *) 1864 STRIP_ASSUME_TAC (MATCH_MP contracts_TRANS_label 1865 (ASSUME ``$contracts (sum p (prefix (label a) nil)) 1866 (sum q (prefix (label a) nil))``)) \\ 1867 RES_TAC \\ 1868 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) nil)) (label x) E2`` 1869 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1870 [ (* goal 2.2.2.1 (of 2) *) 1871 Q.EXISTS_TAC `E2` >> art [], 1872 (* goal 2.2.2.2 (of 2) *) 1873 IMP_RES_TAC TRANS_PREFIX \\ 1874 PAT_X_ASSUM ``label x = label a`` 1875 (ASSUME_TAC o (REWRITE_RULE [Action_11])) \\ 1876 `TRANS p (label a) E1` by RW_TAC std_ss [] \\ 1877 POP_ASSUM (ASSUME_TAC o (MATCH_MP TRANS_IMP_WEAK_TRANS)) \\ 1878 RES_TAC ] ] ]); (* initial assumption of `p` is used here *) 1879 1880val COARSEST_PRECONGR_RL = save_thm ( 1881 "COARSEST_PRECONGR_RL", 1882 BETA_RULE (REWRITE_RULE [SUM_contracts] SUM_contracts_IMP_OBS_contracts)); 1883 1884(* Assuming p & q have free actions, OBS_contracts is the coarsest precongruence 1885 contained in `contracts`! *) 1886val COARSEST_PRECONGR_THM = store_thm ( 1887 "COARSEST_PRECONGR_THM", 1888 ``!p q. free_action p /\ free_action q ==> (OBS_contracts p q = SUM_contracts p q)``, 1889 rpt STRIP_TAC 1890 >> EQ_TAC 1891 >- REWRITE_TAC [OBS_contracts_IMP_SUM_contracts] 1892 >> MATCH_MP_TAC SUM_contracts_IMP_OBS_contracts >> art []); 1893 1894(* |- ���p q. free_action p ��� free_action q ��� (p ������ q ��� ���r. p + r ������ q + r) *) 1895val COARSEST_PRECONGR_THM' = save_thm ( 1896 "COARSEST_PRECONGR_THM'", BETA_RULE (REWRITE_RULE [SUM_contracts] COARSEST_PRECONGR_THM)); 1897 1898(******************************************************************************) 1899(* *) 1900(* Coarsest precongruence contained in `contracts` (full, EXPRESS/SOS 2018) *) 1901(* *) 1902(******************************************************************************) 1903 1904(* |- `���p q. p ������ q ��� ���r. p + r ������ q + r` *) 1905val COARSEST_PRECONGR_LR = save_thm ((* NEW *) 1906 "COARSEST_PRECONGR_LR", 1907 BETA_RULE (REWRITE_RULE [SUM_contracts] OBS_contracts_IMP_SUM_contracts)); 1908(* or prove directly by: 1909 REPEAT STRIP_TAC 1910 >> MATCH_MP_TAC OBS_contracts_IMP_contracts 1911 >> RW_TAC std_ss [OBS_contracts_SUBST_SUM_R] *) 1912 1913(* This is the OBS_contracts version of PROP3_COMMON *) 1914val COARSEST_PRECONGR_LEMMA = store_thm ((* NEW *) 1915 "COARSEST_PRECONGR_LEMMA", 1916 ``!p q. (?k. STABLE k /\ 1917 (!p' u. WEAK_TRANS p u p' ==> ~(WEAK_EQUIV p' k)) /\ 1918 (!q' u. WEAK_TRANS q u q' ==> ~(WEAK_EQUIV q' k))) ==> 1919 (!r. (sum p r) contracts (sum q r)) ==> OBS_contracts p q``, 1920 rpt STRIP_TAC 1921 >> PAT_X_ASSUM ``!r. (sum p r) contracts (sum q r)`` 1922 (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) 1923 >> REWRITE_TAC [OBS_contracts] 1924 >> rpt STRIP_TAC (* 2 sub-goals here *) 1925 >| [ (* goal 1 (of 2) *) 1926 IMP_RES_TAC SUM1 \\ 1927 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\ 1928 PAT_X_ASSUM ``$contracts (sum p (prefix (label a) k)) (sum q (prefix (label a) k))`` 1929 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [contracts_cases])) \\ 1930 Cases_on `u` >| (* 2 sub-goals here *) 1931 [ (* goal 1.1 (of 2) *) 1932 RES_TAC >| (* 2 sub-goals here *) 1933 [ (* goal 1.1.1 (of 2) *) 1934 Q.ABBREV_TAC `E2 = sum q (prefix (label a) k)` \\ 1935 `TRANS E2 (label a) k` by PROVE_TAC [PREFIX, SUM2] \\ 1936 IMP_RES_TAC contracts_TRANS_label' \\ 1937 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 1938 PROVE_TAC [], 1939 (* goal 1.1.2 (of 2) *) 1940 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) tau E2`` 1941 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1942 [ (* goal 1.1.2.1 (of 2) *) 1943 Q.EXISTS_TAC `E2` >> art [], 1944 (* goal 1.1.2.2 (of 2) *) 1945 IMP_RES_TAC TRANS_PREFIX \\ 1946 RW_TAC std_ss [Action_distinct_label] ] ], 1947 (* goal 1.2 (of 2) *) 1948 Cases_on `x = a` >| (* 2 sub-goals here *) 1949 [ (* goal 1.2.1 (of 2) *) 1950 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1951 Q.EXISTS_TAC `E2` >> art [] \\ 1952 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label a) E2`` 1953 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) \\ 1954 IMP_RES_TAC TRANS_PREFIX \\ 1955 `WEAK_EQUIV E1 k` by PROVE_TAC [contracts_IMP_WEAK_EQUIV] \\ 1956 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 1957 RES_TAC, 1958 (* goal 1.2.2 (of 2) *) 1959 RES_TAC \\ 1960 Q.EXISTS_TAC `E2` >> art [] \\ 1961 PAT_X_ASSUM ``TRANS (sum q (prefix (label a) k)) (label x) E2`` 1962 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) \\ 1963 IMP_RES_TAC TRANS_PREFIX \\ 1964 RW_TAC std_ss [Action_11] ] ], 1965 (* goal 2 (of 2), almost symmetric with goal 1 *) 1966 IMP_RES_TAC SUM1 \\ 1967 POP_ASSUM (ASSUME_TAC o (Q.SPEC `prefix (label a) k`)) \\ 1968 PAT_X_ASSUM ``$contracts (sum p (prefix (label a) k)) (sum h (prefix (label a) k))`` 1969 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [contracts_cases])) \\ 1970 Cases_on `u` >| (* 2 sub-goals here *) 1971 [ (* goal 2.1 (of 2) *) 1972 RES_TAC \\ 1973 PAT_X_ASSUM ``EPS (sum p (prefix (label a) k)) E1`` 1974 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [EPS_cases1])) >| (* 2 sub-goals here *) 1975 [ (* goal 2.1.1 (of 2) *) 1976 `TRANS E1 (label a) k` by PROVE_TAC [PREFIX, SUM2] \\ 1977 IMP_RES_TAC WEAK_EQUIV_TRANS_label \\ 1978 IMP_RES_TAC TRANS_TAU_AND_WEAK \\ 1979 `WEAK_EQUIV E2' k` by PROVE_TAC [WEAK_EQUIV_SYM] \\ (* one extra step *) 1980 PROVE_TAC [], 1981 (* goal 2.1.2 (of 2) *) 1982 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau u`` 1983 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1984 [ (* goal 2.1.2.1 (of 2) *) 1985 Q.EXISTS_TAC `E1` >> art [] \\ 1986 IMP_RES_TAC TRANS_AND_EPS, 1987 (* goal 2.1.2.2 (of 2) *) 1988 IMP_RES_TAC TRANS_PREFIX \\ 1989 RW_TAC std_ss [Action_distinct_label] ] ], 1990 (* goal 2.2 (of 2) *) 1991 Cases_on `x = a` >| (* 2 sub-goals here *) 1992 [ (* goal 2.2.1 (of 2) *) 1993 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1994 Q.EXISTS_TAC `E1` >> art [] \\ 1995 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 1996 [ (* goal 2.2.1.1 (of 2) *) 1997 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'`` 1998 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 1999 [ (* goal 2.2.1.1.1 (of 2) *) 2000 IMP_RES_TAC TRANS_TAU_AND_WEAK, 2001 (* goal 2.2.1.1.2 (of 2) *) 2002 IMP_RES_TAC TRANS_PREFIX \\ 2003 RW_TAC std_ss [Action_distinct] ], 2004 (* goal 2.2.1.2 (of 2) *) 2005 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label a) E'`` 2006 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 2007 [ (* goal 2.2.1.2.1 (of 2) *) 2008 IMP_RES_TAC TRANS_AND_EPS, 2009 (* goal 2.2.1.2.2 (of 2) *) 2010 IMP_RES_TAC TRANS_PREFIX \\ 2011 `WEAK_EQUIV E2 k` by PROVE_TAC [EPS_STABLE', WEAK_EQUIV_SYM] \\ 2012 IMP_RES_TAC TRANS_IMP_WEAK_TRANS \\ 2013 RES_TAC ] ], 2014 (* goal 2.2.2 (of 2) *) 2015 RES_TAC \\ 2016 Q.EXISTS_TAC `E1` >> art [] \\ 2017 IMP_RES_TAC WEAK_TRANS_cases1 >| (* 2 sub-goals here *) 2018 [ (* goal 2.2.2.1 (of 2) *) 2019 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) tau E'`` 2020 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 2021 [ (* goal 2.2.2.1.1 (of 2) *) 2022 IMP_RES_TAC TRANS_TAU_AND_WEAK, 2023 (* goal 2.2.2.1.2 (of 2) *) 2024 IMP_RES_TAC TRANS_PREFIX \\ 2025 RW_TAC std_ss [Action_distinct] ], 2026 (* goal 2.2.2.2 (of 2) *) 2027 PAT_X_ASSUM ``TRANS (sum p (prefix (label a) k)) (label x) E'`` 2028 (STRIP_ASSUME_TAC o (MATCH_MP TRANS_SUM)) >| (* 2 sub-goals here *) 2029 [ (* goal 2.2.2.2.1 (of 2) *) 2030 IMP_RES_TAC TRANS_AND_EPS, 2031 (* goal 2.2.2.2.2 (of 2) *) 2032 IMP_RES_TAC TRANS_PREFIX \\ 2033 RW_TAC std_ss [Action_11] ] ] ] ] ]); 2034 2035(* The finite-state version of COARSEST_PRECONGR_THM; i. e. 2036 The contraction version of COARSEST_CONGR_FINITE (van Glabbeek scenario) *) 2037val COARSEST_PRECONGR_FINITE = store_thm ((* NEW *) 2038 "COARSEST_PRECONGR_FINITE", 2039 ``!p q. finite_state p /\ finite_state q ==> 2040 (OBS_contracts p q = !r. (sum p r) contracts (sum q r))``, 2041 rpt STRIP_TAC 2042 >> EQ_TAC >- REWRITE_TAC [COARSEST_PRECONGR_LR] 2043 >> MP_TAC (Q.SPECL [`p`, `q`] KLOP_LEMMA_FINITE) (* in CoarsestCongrTheory *) 2044 >> RW_TAC std_ss [COARSEST_PRECONGR_LEMMA]); 2045 2046(* Another version with SUM_contracts used *) 2047val COARSEST_PRECONGR_FINITE' = store_thm ( 2048 "COARSEST_PRECONGR_FINITE'", 2049 ``!p q. finite_state p /\ finite_state q ==> (OBS_contracts p q = SUM_contracts p q)``, 2050 rpt STRIP_TAC 2051 >> EQ_TAC >- REWRITE_TAC [OBS_contracts_IMP_SUM_contracts] 2052 >> REWRITE_TAC [SUM_contracts] 2053 >> BETA_TAC >> rpt STRIP_TAC 2054 >> MP_TAC COARSEST_PRECONGR_FINITE 2055 >> RW_TAC std_ss []); 2056 2057(* Bibliography: 2058 * 2059 * [1] Sangiorgi, D.: Equations, contractions, and unique solutions. ACM SIGPLAN Notices. (2015). 2060 * [2] R.J. van Glabbeek, ���A characterisation of weak bisimulation congruence���, in Processes, 2061 * Terms and Cycles: Steps on the Road to Infinity, Essays dedicated to Jan Willem Klop, on the 2062 * occasion of his 60th birthday, LNCS 3838, 26-39. Springer-Verlag, 2005. 2063 *) 2064 2065val _ = export_theory (); 2066val _ = html_theory "Contraction"; 2067 2068(* last updated: Oct 14, 2017 *) 2069