1(* ========================================================================== *) 2(* FILE : ExpansionScript.sml *) 3(* DESCRIPTION : EXPANSION and `expands' relation *) 4(* *) 5(* THESIS : A Formalization of Unique Solutions of Equations in *) 6(* Process Algebra *) 7(* AUTHOR : (c) Chun Tian, University of Bologna *) 8(* DATE : 2017 *) 9(* ========================================================================== *) 10 11open HolKernel Parse boolLib bossLib; 12 13open relationTheory listTheory; 14open CCSLib CCSTheory; 15open StrongEQTheory StrongLawsTheory; 16open WeakEQTheory WeakLawsTheory; 17open CongruenceTheory TraceTheory; 18 19val _ = new_theory "Expansion"; 20val _ = temp_loose_equality (); 21 22(******************************************************************************) 23(* *) 24(* The expansion relation *) 25(* *) 26(******************************************************************************) 27 28(* The definitin is confirmed with [1], [2] and [3] *) 29val EXPANSION = new_definition ("EXPANSION", 30 ``EXPANSION (Exp: ('a, 'b) simulation) = 31 !(E :('a, 'b) CCS) (E' :('a, 'b) CCS). Exp E E' ==> 32 (!l. 33 (!E1. TRANS E (label l) E1 ==> 34 ?E2. TRANS E' (label l) E2 /\ Exp E1 E2) /\ 35 (!E2. TRANS E' (label l) E2 ==> 36 ?E1. WEAK_TRANS E (label l) E1 /\ Exp E1 E2)) /\ 37 (!E1. TRANS E tau E1 ==> Exp E1 E' \/ ?E2. TRANS E' tau E2 /\ Exp E1 E2) /\ 38 (!E2. TRANS E' tau E2 ==> ?E1. WEAK_TRANS E tau E1 /\ Exp E1 E2)``); 39 40(* alternative definition *) 41val EXPANSION_ALT = store_thm ( 42 "EXPANSION_ALT", 43 ``EXPANSION (Exp: ('a, 'b) simulation) = 44 !(E :('a, 'b) CCS) (E' :('a, 'b) CCS). Exp E E' ==> 45 (!l E1. TRANS E (label l) E1 ==> ?E2. TRANS E' (label l) E2 /\ Exp E1 E2) /\ 46 (! E1. TRANS E tau E1 ==> Exp E1 E' \/ ?E2. TRANS E' tau E2 /\ Exp E1 E2) /\ 47 (!u E2. TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ Exp E1 E2)``, 48 EQ_TAC (* 2 sub-goals here *) 49 >| [ (* goal 1 (of 2) *) 50 REWRITE_TAC [EXPANSION] \\ 51 REPEAT STRIP_TAC >| (* 3 sub-goals here *) 52 [ (* goal 1 (of 3) *) 53 RES_TAC >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 54 (* goal 2 (of 3) *) 55 RES_TAC >| (* 2 sub-goals here *) 56 [ (* goal 2.1 (of 2) *) 57 DISJ1_TAC >> ASM_REWRITE_TAC [], 58 (* goal 2.2 (of 2) *) 59 DISJ2_TAC \\ 60 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ], 61 (* goal 3 (of 3) *) 62 Cases_on `u` \\ (* 2 sub-goals sharing the same tacticals *) 63 RES_TAC >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ], 64 (* goal 2 (of 2) *) 65 REWRITE_TAC [EXPANSION] \\ 66 REPEAT STRIP_TAC >> RES_TAC >| (* 5 sub-goals here *) 67 [ Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 68 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 69 DISJ1_TAC >> ASM_REWRITE_TAC [], 70 DISJ2_TAC >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 71 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ] ]); 72 73(* The identity relation is a EXPANSION. *) 74val IDENTITY_EXPANSION = store_thm ( 75 "IDENTITY_EXPANSION", ``EXPANSION Id``, 76 PURE_ONCE_REWRITE_TAC [EXPANSION_ALT] 77 >> rpt STRIP_TAC >> rfs [] 78 >> IMP_RES_TAC TRANS_IMP_WEAK_TRANS); 79 80val EXPANSION_EPS = store_thm ( 81 "EXPANSION_EPS", 82 ``!(Exp: ('a, 'b) simulation). EXPANSION Exp ==> 83 !E E'. Exp E E' ==> !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ Exp E1 E2``, 84 REPEAT STRIP_TAC 85 >> qpat_x_assum `Exp E E'` MP_TAC 86 >> POP_ASSUM MP_TAC 87 >> Q.SPEC_TAC (`E1`, `E1`) 88 >> Q.SPEC_TAC (`E`, `E`) 89 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 90 >> rpt STRIP_TAC (* 2 sub-goals here *) 91 >| [ (* goal 1 (of 2) *) 92 Q.EXISTS_TAC `E'` >> RW_TAC std_ss [EPS_REFL], 93 (* goal 2 (of 2) *) 94 RES_TAC \\ 95 IMP_RES_TAC 96 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Exp``)) 97 (ASSUME ``(Exp :('a, 'b) simulation) E1 E2``)) 98 >- ( Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 99 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 100 IMP_RES_TAC ONE_TAU \\ 101 IMP_RES_TAC EPS_TRANS ]); 102 103val EXPANSION_EPS' = store_thm ( 104 "EXPANSION_EPS'", 105 ``!(Exp: ('a, 'b) simulation). EXPANSION Exp ==> 106 !E E'. Exp E E' ==> !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ Exp E1 E2``, 107 REPEAT STRIP_TAC 108 >> qpat_x_assum `Exp E E'` MP_TAC 109 >> POP_ASSUM MP_TAC 110 >> Q.SPEC_TAC (`E2`, `E2`) 111 >> Q.SPEC_TAC (`E'`, `E'`) 112 >> HO_MATCH_MP_TAC EPS_ind_right (* must use right induct here! *) 113 >> rpt STRIP_TAC (* 2 sub-goals here *) 114 >| [ (* goal 1 (of 2) *) 115 Q.EXISTS_TAC `E` >> RW_TAC std_ss [EPS_REFL], 116 (* goal 2 (of 2) *) 117 RES_TAC \\ 118 IMP_RES_TAC 119 (MATCH_MP (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp``)) 120 (ASSUME ``(Exp :('a, 'b) simulation) E1 E2``)) \\ 121 `WEAK_TRANS E tau E1'` by PROVE_TAC [EPS_AND_WEAK_TRANS] \\ 122 `EPS E E1'` by PROVE_TAC [WEAK_TRANS_IMP_EPS] \\ 123 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] ]); 124 125(* NOTE: EXPANSION_WEAK_TRANS doens't hold *) 126val EXPANSION_WEAK_TRANS' = store_thm ( 127 "EXPANSION_WEAK_TRANS'", 128 ``!(Exp: ('a, 'b) simulation). EXPANSION Exp ==> 129 !E E'. Exp E E' ==> 130 !u E2. WEAK_TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ Exp E1 E2``, 131 REPEAT STRIP_TAC 132 >> IMP_RES_TAC WEAK_TRANS 133 >> IMP_RES_TAC 134 (MATCH_MP (MATCH_MP EXPANSION_EPS' (ASSUME ``EXPANSION Exp``)) 135 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) 136 >> IMP_RES_TAC 137 (MATCH_MP (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp``)) 138 (ASSUME ``(Exp :('a, 'b) simulation) E1' E1``)) 139 >> IMP_RES_TAC 140 (MATCH_MP (MATCH_MP EXPANSION_EPS' (ASSUME ``EXPANSION Exp``)) 141 (ASSUME ``(Exp :('a, 'b) simulation) E1'' E2'``)) 142 >> Q.EXISTS_TAC `E1'''` 143 >> ASM_REWRITE_TAC [] 144 >> MATCH_MP_TAC EPS_WEAK_EPS 145 >> take [`E1'`, `E1''`] 146 >> ASM_REWRITE_TAC []); 147 148(* The composition of two EXPANSIONs is an EXPANSION. *) 149val COMP_EXPANSION = store_thm ( 150 "COMP_EXPANSION", 151 ``!Exp1 Exp2. EXPANSION Exp1 /\ EXPANSION Exp2 ==> EXPANSION (Exp2 O Exp1)``, 152 REPEAT STRIP_TAC 153 >> REWRITE_TAC [EXPANSION_ALT, O_DEF] 154 >> BETA_TAC 155 >> REPEAT STRIP_TAC (* 3 sub-goals here *) 156 >| [ (* goal 1 (of 3) *) 157 IMP_RES_TAC 158 (MATCH_MP 159 (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp1``)) 160 (ASSUME ``(Exp1 :('a, 'b) simulation) E y``)) \\ 161 IMP_RES_TAC 162 (MATCH_MP 163 (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp2``)) 164 (ASSUME ``(Exp2 :('a, 'b) simulation) y E'``)) \\ 165 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 166 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 167 (* goal 2 (of 3) *) 168 IMP_RES_TAC 169 (MATCH_MP 170 (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp1``)) 171 (ASSUME ``(Exp1 :('a, 'b) simulation) E y``)) (* 2 sub-goals here *) 172 >- ( DISJ1_TAC >> Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [] ) \\ 173 IMP_RES_TAC 174 (MATCH_MP 175 (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp2``)) 176 (ASSUME ``(Exp2 :('a, 'b) simulation) y E'``)) (* 2 sub-goals here *) 177 >- ( DISJ1_TAC >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 178 DISJ2_TAC >> Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 179 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 180 (* goal 2 (of 3) *) 181 IMP_RES_TAC 182 (MATCH_MP (REWRITE_RULE [EXPANSION_ALT] (ASSUME ``EXPANSION Exp2``)) 183 (ASSUME ``(Exp2 :('a, 'b) simulation) y E'``)) \\ 184 IMP_RES_TAC 185 (MATCH_MP (MATCH_MP EXPANSION_WEAK_TRANS' (ASSUME ``EXPANSION Exp1``)) 186 (ASSUME ``(Exp1 :('a, 'b) simulation) E y``)) \\ 187 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 188 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] ]); 189 190val STRONG_BISIM_IMP_EXPANSION = store_thm ( 191 "STRONG_BISIM_IMP_EXPANSION", ``!Exp. STRONG_BISIM Exp ==> EXPANSION Exp``, 192 REPEAT STRIP_TAC 193 >> REWRITE_TAC [EXPANSION] 194 >> rpt STRIP_TAC (* 4 sub-goals here *) 195 >| [ (* goal 1 (of 4) *) 196 IMP_RES_TAC 197 (MATCH_MP (REWRITE_RULE [STRONG_BISIM] (ASSUME ``STRONG_BISIM Exp``)) 198 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 199 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 200 (* goal 2 (of 4) *) 201 IMP_RES_TAC 202 (MATCH_MP (REWRITE_RULE [STRONG_BISIM] (ASSUME ``STRONG_BISIM Exp``)) 203 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 204 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 205 IMP_RES_TAC TRANS_IMP_WEAK_TRANS, 206 (* goal 3 (of 4) *) 207 IMP_RES_TAC 208 (MATCH_MP (REWRITE_RULE [STRONG_BISIM] (ASSUME ``STRONG_BISIM Exp``)) 209 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 210 DISJ2_TAC \\ 211 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [], 212 (* goal 4 (of 4) *) 213 IMP_RES_TAC 214 (MATCH_MP (REWRITE_RULE [STRONG_BISIM] (ASSUME ``STRONG_BISIM Exp``)) 215 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 216 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 217 IMP_RES_TAC TRANS_IMP_WEAK_TRANS ]); 218 219val EXPANSION_IMP_WEAK_BISIM = store_thm ( 220 "EXPANSION_IMP_WEAK_BISIM", 221 ``!Exp. EXPANSION Exp ==> WEAK_BISIM Exp``, 222 REPEAT STRIP_TAC 223 >> REWRITE_TAC [WEAK_BISIM] 224 >> rpt STRIP_TAC (* 4 sub-goals here *) 225 >| [ (* goal 1 (of 4) *) 226 IMP_RES_TAC 227 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Exp``)) 228 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 229 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 230 IMP_RES_TAC TRANS_IMP_WEAK_TRANS, 231 (* goal 2 (of 4) *) 232 IMP_RES_TAC 233 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Exp``)) 234 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 235 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 236 (* goal 3 (of 4) *) 237 IMP_RES_TAC 238 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Exp``)) 239 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) (* 2 sub-goals here *) 240 >- ( Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [EPS_REFL] ) \\ 241 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 242 IMP_RES_TAC ONE_TAU, 243 (* goal 4 (of 4) *) 244 IMP_RES_TAC 245 (MATCH_MP (REWRITE_RULE [EXPANSION] (ASSUME ``EXPANSION Exp``)) 246 (ASSUME ``(Exp :('a, 'b) simulation) E E'``)) \\ 247 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 248 IMP_RES_TAC WEAK_TRANS_IMP_EPS ]); 249 250(* `P expands Q` if P R Q for some expansion R, re-defined by co-induction 251 * it means "P is at least as fast as Q", or more generally "Q uses at least as much 252 * resources as P". 253 *) 254val (expands_rules, expands_coind, expands_cases) = Hol_coreln ` 255 (!(E :('a, 'b) CCS) (E' :('a, 'b) CCS). 256 (!l. 257 (!E1. TRANS E (label l) E1 ==> 258 ?E2. TRANS E' (label l) E2 /\ $expands E1 E2) /\ 259 (!E2. TRANS E' (label l) E2 ==> 260 ?E1. WEAK_TRANS E (label l) E1 /\ $expands E1 E2)) /\ 261 (!E1. TRANS E tau E1 ==> $expands E1 E' \/ ?E2. TRANS E' tau E2 /\ $expands E1 E2) /\ 262 (!E2. TRANS E' tau E2 ==> ?E1. WEAK_TRANS E tau E1 /\ $expands E1 E2) 263 ==> $expands E E')`; 264 265val _ = set_fixity "expands" (Infixl 500); 266val _ = Unicode.unicode_version { u = UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D49, tmnm = "expands" }; 267val _ = TeX_notation { hol = UTF8.chr 0x2AB0 ^ UTF8.chr 0x1D49, 268 TeX = ("\\HOLTokenExpands{}", 1) }; 269 270(* a shorter version of `expands_cases` with only 3 branches *) 271val expands_cases' = store_thm ( 272 "expands_cases'", 273 ``!E E'. E expands E' = 274 (!l E1. TRANS E (label l) E1 ==> ?E2. TRANS E' (label l) E2 /\ E1 expands E2) /\ 275 (! E1. TRANS E tau E1 ==> E1 expands E' \/ (?E2. TRANS E' tau E2 /\ E1 expands E2)) /\ 276 (!u E2. TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ E1 expands E2)``, 277 rpt GEN_TAC 278 >> EQ_TAC (* 2 sub-goals here *) 279 >| [ (* goal 1 (of 2) *) 280 DISCH_TAC >> POP_ASSUM (MP_TAC o (ONCE_REWRITE_RULE [expands_cases])) \\ 281 fs [] >> rpt STRIP_TAC \\ 282 Cases_on `u` >> RES_TAC \\ (* 2 sub-goals here, same tacticals *) 283 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [], 284 (* goal 2 (of 2) *) 285 DISCH_TAC \\ 286 MATCH_MP_TAC expands_rules \\ 287 POP_ASSUM MP_TAC >> fs [] ]); 288 289val expands_is_EXPANSION = store_thm ( 290 "expands_is_EXPANSION", ``EXPANSION $expands``, 291 PURE_ONCE_REWRITE_TAC [EXPANSION] 292 >> REPEAT GEN_TAC 293 >> DISCH_TAC 294 >> PURE_ONCE_REWRITE_TAC [GSYM expands_cases] 295 >> ASM_REWRITE_TAC []); 296 297(* the original definition now becomes a theorem *) 298val expands_thm = store_thm ( 299 "expands_thm", 300 ``!P Q. P expands Q = ?Exp. Exp P Q /\ EXPANSION Exp``, 301 NTAC 2 GEN_TAC >> EQ_TAC (* 2 sub-goals here *) 302 >| [ (* goal 1 (of 2) *) 303 DISCH_TAC \\ 304 EXISTS_TAC ``$expands`` \\ 305 ASM_REWRITE_TAC [expands_is_EXPANSION], 306 (* goal 2 (of 2) *) 307 Q.SPEC_TAC (`Q`, `Q`) \\ 308 Q.SPEC_TAC (`P`, `P`) \\ 309 HO_MATCH_MP_TAC expands_coind \\ (* co-induction used here! *) 310 METIS_TAC [EXPANSION] ]); 311 312val EXPANSION_SUBSET_expands = store_thm ((* NEW *) 313 "EXPANSION_SUBSET_expands", 314 ``!Exp. EXPANSION Exp ==> Exp RSUBSET $expands``, 315 PROVE_TAC [RSUBSET, expands_thm]); 316 317(* "Half" theorems for `expands` relation *) 318val expands_TRANS_label = store_thm ( 319 "expands_TRANS_label", 320 ``!E E'. E expands E' ==> 321 !l E1. TRANS E (label l) E1 ==> ?E2. TRANS E' (label l) E2 /\ E1 expands E2``, 322 PROVE_TAC [expands_cases]); 323 324val expands_TRANS_label' = store_thm ( 325 "expands_TRANS_label'", 326 ``!E E'. E expands E' ==> 327 !l E2. TRANS E' (label l) E2 ==> ?E1. WEAK_TRANS E (label l) E1 /\ E1 expands E2``, 328 PROVE_TAC [expands_cases]); 329 330val expands_TRANS_tau = store_thm ( 331 "expands_TRANS_tau", 332 ``!E E'. E expands E' ==> 333 !E1. TRANS E tau E1 ==> E1 expands E' \/ ?E2. TRANS E' tau E2 /\ E1 expands E2``, 334 PROVE_TAC [expands_cases]); 335 336val expands_TRANS_tau' = store_thm ( 337 "expands_TRANS_tau'", 338 ``!E E'. E expands E' ==> 339 !E2. TRANS E' tau E2 ==> ?E1. WEAK_TRANS E tau E1 /\ E1 expands E2``, 340 PROVE_TAC [expands_cases]); 341 342val expands_TRANS_action' = store_thm ( 343 "expands_TRANS_action'", 344 ``!E E'. E expands E' ==> 345 !u E2. TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ E1 expands E2``, 346 rpt STRIP_TAC 347 >> Cases_on `u` 348 >- PROVE_TAC [expands_TRANS_tau'] 349 >> PROVE_TAC [expands_TRANS_label']); 350 351(* The `expands` relation is reflexive *) 352val expands_reflexive = store_thm ( 353 "expands_reflexive", ``reflexive $expands``, 354 REWRITE_TAC [reflexive_def] 355 >> GEN_TAC 356 >> PURE_ONCE_REWRITE_TAC [expands_thm] 357 >> Q.EXISTS_TAC `Id` 358 >> REWRITE_TAC [IDENTITY_EXPANSION]); 359 360(* the version for easier use *) 361val expands_REFL = save_thm ( 362 "expands_REFL", REWRITE_RULE [reflexive_def] expands_reflexive); 363 364(* Syntactic equivalence implies expands. *) 365val EQ_IMP_expands = store_thm ( 366 "EQ_IMP_expands", ``!E E'. (E = E') ==> E expands E'``, 367 REPEAT STRIP_TAC 368 >> PURE_ASM_REWRITE_TAC [expands_REFL]); 369 370(* `expands` is a transitive relation. *) 371val expands_transitive = store_thm ( 372 "expands_transitive", ``transitive $expands``, 373 REWRITE_TAC [transitive_def] 374 >> REPEAT GEN_TAC 375 >> PURE_ONCE_REWRITE_TAC [expands_thm] 376 >> STRIP_TAC 377 >> Q.EXISTS_TAC `Exp' O Exp` 378 >> CONJ_TAC (* 2 sub-goals here *) 379 >| [ (* goal 1 (of 2) *) 380 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 381 Q.EXISTS_TAC `y` >> ASM_REWRITE_TAC [], 382 (* goal 2 (of 2) *) 383 IMP_RES_TAC COMP_EXPANSION ]); 384 385(* the version for easier use *) 386val expands_TRANS = save_thm ( 387 "expands_TRANS", REWRITE_RULE [transitive_def] expands_transitive); 388 389(* `expands` is a pre-order *) 390val expands_PreOrder = store_thm ( 391 "expands_PreOrder", ``PreOrder $expands``, 392 REWRITE_TAC [PreOrder, expands_reflexive, expands_transitive]); 393 394val STRONG_EQUIV_IMP_expands = store_thm ( 395 "STRONG_EQUIV_IMP_expands", ``!P Q. STRONG_EQUIV P Q ==> P expands Q``, 396 REPEAT GEN_TAC 397 >> REWRITE_TAC [expands_thm, STRONG_EQUIV] 398 >> rpt STRIP_TAC 399 >> Q.EXISTS_TAC `Bsm` >> ASM_REWRITE_TAC [] 400 >> IMP_RES_TAC STRONG_BISIM_IMP_EXPANSION); 401 402val expands_IMP_WEAK_EQUIV = store_thm ( 403 "expands_IMP_WEAK_EQUIV", ``!P Q. P expands Q ==> WEAK_EQUIV P Q``, 404 REPEAT GEN_TAC 405 >> REWRITE_TAC [expands_thm, WEAK_EQUIV] 406 >> rpt STRIP_TAC 407 >> Q.EXISTS_TAC `Exp` >> ASM_REWRITE_TAC [] 408 >> IMP_RES_TAC EXPANSION_IMP_WEAK_BISIM); 409 410val expands_EPS = store_thm ( 411 "expands_EPS", 412 ``!E E'. E expands E' ==> !E1. EPS E E1 ==> ?E2. EPS E' E2 /\ E1 expands E2``, 413 REWRITE_TAC [expands_thm] 414 >> rpt STRIP_TAC 415 >> IMP_RES_TAC EXPANSION_EPS 416 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] 417 >> Q.EXISTS_TAC `Exp` >> ASM_REWRITE_TAC []); 418 419val expands_EPS' = store_thm ( 420 "expands_EPS'", 421 ``!E E'. E expands E' ==> !E2. EPS E' E2 ==> ?E1. EPS E E1 /\ E1 expands E2``, 422 REWRITE_TAC [expands_thm] 423 >> rpt STRIP_TAC 424 >> IMP_RES_TAC EXPANSION_EPS' 425 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] 426 >> Q.EXISTS_TAC `Exp` >> ASM_REWRITE_TAC []); 427 428val expands_WEAK_TRANS' = store_thm ( 429 "expands_WEAK_TRANS'", 430 ``!E E'. E expands E' ==> 431 !u E2. WEAK_TRANS E' u E2 ==> ?E1. WEAK_TRANS E u E1 /\ E1 expands E2``, 432 REWRITE_TAC [expands_thm] 433 >> rpt STRIP_TAC 434 >> IMP_RES_TAC EXPANSION_WEAK_TRANS' 435 >> Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] 436 >> Q.EXISTS_TAC `Exp` >> ASM_REWRITE_TAC []); 437 438val expands_WEAK_TRANS_label = store_thm ( 439 "expands_WEAK_TRANS_label", 440 ``!E E'. E expands E' ==> 441 !l E1. WEAK_TRANS E (label l) E1 ==> ?E2. WEAK_TRANS E' (label l) E2 /\ E1 expands E2``, 442 rpt STRIP_TAC 443 >> IMP_RES_TAC WEAK_TRANS 444 >> IMP_RES_TAC (MATCH_MP expands_EPS (ASSUME ``E expands E'``)) 445 >> IMP_RES_TAC (MATCH_MP expands_TRANS_label (ASSUME ``E1' expands E2'``)) 446 >> IMP_RES_TAC (MATCH_MP expands_EPS (ASSUME ``E2 expands E2''``)) 447 >> Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] 448 >> REWRITE_TAC [WEAK_TRANS] 449 >> take [`E2'`, `E2''`] >> ASM_REWRITE_TAC []); 450 451val expands_WEAK_TRANS_tau = store_thm ( 452 "expands_WEAK_TRANS_tau", 453 ``!E E'. E expands E' ==> 454 !E1. WEAK_TRANS E tau E1 ==> ?E2. EPS E' E2 /\ E1 expands E2``, 455 rpt STRIP_TAC 456 >> IMP_RES_TAC WEAK_TRANS 457 >> IMP_RES_TAC (MATCH_MP expands_EPS (ASSUME ``E expands E'``)) 458 >> IMP_RES_TAC 459 (MATCH_MP expands_TRANS_tau (ASSUME ``E1' expands E2'``)) (* 2 sub-goals here *) 460 >| [ (* goal 1 (of 2) *) 461 IMP_RES_TAC (MATCH_MP expands_EPS (ASSUME ``E2 expands E2'``)) \\ 462 Q.EXISTS_TAC `E2''` >> ASM_REWRITE_TAC [] \\ 463 IMP_RES_TAC EPS_TRANS, 464 (* goal 2 (of 2) *) 465 IMP_RES_TAC (MATCH_MP expands_EPS (ASSUME ``E2 expands E2''``)) \\ 466 Q.EXISTS_TAC `E2'''` >> ASM_REWRITE_TAC [] \\ 467 IMP_RES_TAC ONE_TAU \\ 468 IMP_RES_TAC EPS_TRANS ]); 469 470(******************************************************************************) 471(* *) 472(* `expands` is precongruence *) 473(* *) 474(******************************************************************************) 475 476val expands_SUBST_PREFIX = store_thm ( 477 "expands_SUBST_PREFIX", 478 ``!E E'. E expands E' ==> !u. (prefix u E) expands (prefix u E')``, 479 rpt GEN_TAC 480 >> PURE_ONCE_REWRITE_TAC [Q.SPECL [`prefix u E`, `prefix u E'`] expands_cases'] 481 >> rpt STRIP_TAC (* 3 sub-goals here *) 482 >| [ (* goal 1 (of 3) *) 483 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 484 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [PREFIX], 485 (* goal 2 (of 3) *) 486 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 487 DISJ2_TAC \\ 488 Q.EXISTS_TAC `E'` >> ASM_REWRITE_TAC [PREFIX], 489 (* goal 3 (of 3) *) 490 IMP_RES_TAC TRANS_PREFIX >> ASM_REWRITE_TAC [] \\ 491 Q.EXISTS_TAC `E` >> ASM_REWRITE_TAC [WEAK_PREFIX] ]); 492 493val expands_PRESD_BY_GUARDED_SUM = store_thm ( 494 "expands_PRESD_BY_GUARDED_SUM", 495 ``!E1 E1' E2 E2' a1 a2. E1 expands E1' /\ E2 expands E2' ==> 496 (sum (prefix a1 E1) (prefix a2 E2)) expands (sum (prefix a1 E1') (prefix a2 E2'))``, 497 rpt STRIP_TAC 498 >> ONCE_REWRITE_TAC [expands_cases'] 499 >> rpt STRIP_TAC (* 3 sub-goals here *) 500 >| [ (* goal 1 (of 3) *) 501 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 502 [ (* goal 1.1 (of 2) *) 503 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 504 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 505 MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 506 (* goal 1.2 (of 2) *) 507 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 508 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 509 MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ], 510 (* goal 2 (of 3) *) 511 DISJ2_TAC >> IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 512 [ (* goal 2.1 (of 2) *) 513 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 514 Q.EXISTS_TAC `E1'` >> ASM_REWRITE_TAC [] \\ 515 MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 516 (* goal 2.2 (of 2) *) 517 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 518 Q.EXISTS_TAC `E2'` >> ASM_REWRITE_TAC [] \\ 519 MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ], 520 (* goal 3 (of 3) *) 521 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 522 [ (* goal 3.1 (of 2) *) 523 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 524 Q.EXISTS_TAC `E1` >> ASM_REWRITE_TAC [] \\ 525 MATCH_MP_TAC WEAK_SUM1 >> REWRITE_TAC [WEAK_PREFIX], 526 (* goal 3.2 (of 2) *) 527 IMP_RES_TAC TRANS_PREFIX >> fs [] \\ 528 Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] \\ 529 MATCH_MP_TAC WEAK_SUM2 >> REWRITE_TAC [WEAK_PREFIX] ] ]); 530 531val expands_PRESD_BY_PAR = store_thm ( 532 "expands_PRESD_BY_PAR", 533 ``!E1 E1' E2 E2'. 534 E1 expands E1' /\ E2 expands E2' ==> (par E1 E2) expands (par E1' E2')``, 535 rpt STRIP_TAC 536 >> PURE_ONCE_REWRITE_TAC [expands_thm] 537 >> Q.EXISTS_TAC `\x y. 538 ?F1 F1' F2 F2'. 539 (x = par F1 F2) /\ (y = par F1' F2') /\ 540 F1 expands F1' /\ F2 expands F2'` 541 >> BETA_TAC 542 >> CONJ_TAC >- ( take [`E1`, `E1'`, `E2`, `E2'`] >> ASM_REWRITE_TAC [] ) 543 >> PURE_ONCE_REWRITE_TAC [EXPANSION] (* cannot use EXPANSION_ALT here *) 544 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 545 >| [ (* goal 1 (of 4) *) 546 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 547 (ASSUME ``TRANS E (label l) E1''``)) \\ 548 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 549 [ (* goal 1.1 (of 3) *) 550 IMP_RES_TAC (MATCH_MP expands_TRANS_label 551 (ASSUME ``F1 expands F1'``)) \\ 552 EXISTS_TAC ``par E2'' F2'`` \\ 553 CONJ_TAC >| (* 2 sub-goals here *) 554 [ (* goal 1.1.1 (of 2) *) 555 ASM_REWRITE_TAC [] \\ 556 MATCH_MP_TAC PAR1 >> ASM_REWRITE_TAC [], 557 (* goal 1.1.2 (of 2) *) 558 take [`E1'''`, `E2''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ], 559 (* goal 1.2 (of 3) *) 560 IMP_RES_TAC (MATCH_MP expands_TRANS_label 561 (ASSUME ``F2 expands F2'``)) \\ 562 EXISTS_TAC ``par F1' E2''`` \\ 563 CONJ_TAC >| (* 2 sub-goals here *) 564 [ (* goal 1.2.1 (of 2) *) 565 ASM_REWRITE_TAC [] \\ 566 MATCH_MP_TAC PAR2 >> ASM_REWRITE_TAC [], 567 (* goal 1.2.2 (of 2) *) 568 take [`F1`, `F1'`, `E1'''`, `E2''`] >> ASM_REWRITE_TAC [] ], 569 (* goal 1.3 (of 3) *) 570 IMP_RES_TAC Action_distinct_label ], 571 (* goal 2 (of 4) *) 572 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 573 (ASSUME ``TRANS E' (label l) E2''``)) \\ 574 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 575 [ (* goal 2.1 (of 3) *) 576 IMP_RES_TAC (MATCH_MP expands_TRANS_label' 577 (ASSUME ``F1 expands F1'``)) \\ 578 EXISTS_TAC ``par E1''' F2`` \\ 579 CONJ_TAC >| (* 2 sub-goals here *) 580 [ (* goal 2.1.1 (of 2) *) 581 ASM_REWRITE_TAC [] \\ 582 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 583 (* goal 2.1.2 (of 2) *) 584 take [`E1'''`, `E1''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ], 585 (* goal 2.2 (of 3) *) 586 IMP_RES_TAC (MATCH_MP expands_TRANS_label' 587 (ASSUME ``F2 expands F2'``)) \\ 588 EXISTS_TAC ``par F1 E1'''`` \\ 589 CONJ_TAC >| (* 2 sub-goals here *) 590 [ (* goal 2.2.1 (of 2) *) 591 ASM_REWRITE_TAC [] \\ 592 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 593 (* goal 2.2.2 (of 2) *) 594 take [`F1`, `F1'`, `E1'''`, `E1''`] >> ASM_REWRITE_TAC [] ], 595 (* goal 2.3 (of 3) *) 596 IMP_RES_TAC Action_distinct_label ], 597 (* goal 3 (of 4) *) 598 ASSUME_TAC (REWRITE_RULE [ASSUME ``E = par F1 F2``] 599 (ASSUME ``TRANS E tau E1''``)) \\ 600 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 601 [ (* goal 3.1 (of 3) *) 602 IMP_RES_TAC (MATCH_MP expands_TRANS_tau 603 (ASSUME ``F1 expands F1'``)) >| (* 2 sub-goals here *) 604 [ (* goal 3.1.1 (of 2) *) 605 DISJ1_TAC >> take [`E1'''`, `F1'`, `F2`, `F2'`] >> ASM_REWRITE_TAC [], 606 (* goal 3.1.2 (of 2) *) 607 DISJ2_TAC \\ 608 EXISTS_TAC ``par E2'' F2'`` \\ 609 CONJ_TAC >| (* 2 sub-goals here *) 610 [ (* goal 3.1.2.1 (of 2) *) 611 ASM_REWRITE_TAC [] \\ 612 MATCH_MP_TAC PAR1 >> ASM_REWRITE_TAC [], 613 (* goal 3.1.2.2 (of 2) *) 614 take [`E1'''`, `E2''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ] ], 615 (* goal 3.2 (of 3) *) 616 IMP_RES_TAC (MATCH_MP expands_TRANS_tau 617 (ASSUME ``F2 expands F2'``)) >| (* 2 sub-goals here *) 618 [ (* goal 3.2.1 (of 2) *) 619 DISJ1_TAC >> take [`F1`, `F1'`, `E1'''`, `F2'`] >> ASM_REWRITE_TAC [], 620 (* goal 3.2.2 (of 2) *) 621 DISJ2_TAC \\ 622 EXISTS_TAC ``par F1' E2''`` \\ 623 CONJ_TAC >| (* 2 sub-goals here *) 624 [ (* goal 3.2.2.1 (of 2) *) 625 ASM_REWRITE_TAC [] \\ 626 MATCH_MP_TAC PAR2 >> ASM_REWRITE_TAC [], 627 (* goal 3.2.2.2 (of 2) *) 628 take [`F1`, `F1'`, `E1'''`, `E2''`] >> ASM_REWRITE_TAC [] ] ], 629 (* goal 3.3 (of 3) *) 630 IMP_RES_TAC (MATCH_MP expands_TRANS_label (ASSUME ``F1 expands F1'``)) \\ 631 IMP_RES_TAC (MATCH_MP expands_TRANS_label (ASSUME ``F2 expands F2'``)) \\ 632 DISJ2_TAC \\ 633 EXISTS_TAC ``par E2''' E2''''`` \\ 634 CONJ_TAC >| (* 2 sub-goals here *) 635 [ (* goal 3.3.1 (of 2) *) 636 ONCE_ASM_REWRITE_TAC [] \\ 637 MATCH_MP_TAC PAR3 \\ 638 Q.EXISTS_TAC `l` >> ASM_REWRITE_TAC [], 639 (* goal 3.3.2 (of 2) *) 640 take [`E1'''`, `E2'''`, `E2''`, `E2''''`] >> ASM_REWRITE_TAC [] ] ], 641 (* goal 4 (of 4) *) 642 ASSUME_TAC (REWRITE_RULE [ASSUME ``E' = par F1' F2'``] 643 (ASSUME ``TRANS E' tau E2''``)) \\ 644 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 645 [ (* goal 4.1 (of 3) *) 646 IMP_RES_TAC (MATCH_MP expands_TRANS_tau' (ASSUME ``F1 expands F1'``)) \\ 647 EXISTS_TAC ``par E1''' F2`` \\ 648 CONJ_TAC >| (* 2 sub-goals here *) 649 [ (* goal 4.1.1 (of 2) *) 650 ASM_REWRITE_TAC [] \\ 651 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 652 (* goal 4.1.2 (of 2) *) 653 take [`E1'''`, `E1''`, `F2`, `F2'`] >> ASM_REWRITE_TAC [] ], 654 (* goal 4.2 (of 3) *) 655 IMP_RES_TAC (MATCH_MP expands_TRANS_tau' (ASSUME ``F2 expands F2'``)) \\ 656 EXISTS_TAC ``par F1 E1'''`` \\ 657 CONJ_TAC >| (* 2 sub-goals here *) 658 [ (* goal 4.2.1 (of 2) *) 659 ASM_REWRITE_TAC [] \\ 660 IMP_RES_TAC WEAK_PAR >> ASM_REWRITE_TAC [], 661 (* goal 4.2.2 (of 2) *) 662 take [`F1`, `F1'`, `E1'''`, `E1''`] >> ASM_REWRITE_TAC [] ], 663 (* goal 4.3 (of 3) *) 664 IMP_RES_TAC (MATCH_MP expands_TRANS_label' (ASSUME ``F1 expands F1'``)) \\ 665 IMP_RES_TAC (MATCH_MP expands_TRANS_label' (ASSUME ``F2 expands F2'``)) \\ 666 EXISTS_TAC ``par E1''' E1''''`` \\ 667 Rev CONJ_TAC 668 >- ( take [`E1'''`, `E1''`, `E1''''`, `E2'''`] >> ASM_REWRITE_TAC [] ) \\ 669 ONCE_ASM_REWRITE_TAC [] \\ 670 REWRITE_TAC [WEAK_TRANS] \\ 671 STRIP_ASSUME_TAC 672 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS F1 (label l) E1'''``)) \\ 673 STRIP_ASSUME_TAC 674 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS F2 (label (COMPL l)) E1''''``)) \\ 675 EXISTS_TAC ``par E1''''' E1''''''`` \\ 676 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 677 (CONJ (ASSUME ``EPS F1 E1'''''``) 678 (ASSUME ``EPS F2 E1''''''``))] \\ 679 EXISTS_TAC ``par E2'''' E2'''''`` \\ 680 REWRITE_TAC [MATCH_MP EPS_PAR_PAR 681 (CONJ (ASSUME ``EPS E2'''' E1'''``) 682 (ASSUME ``EPS E2''''' E1''''``))] \\ 683 MATCH_MP_TAC PAR3 \\ 684 Q.EXISTS_TAC `l` >> ASM_REWRITE_TAC [] ] ]); 685 686val expands_SUBST_RESTR = store_thm ( 687 "expands_SUBST_RESTR", 688 ``!E E'. E expands E' ==> !L. (restr L E) expands (restr L E')``, 689 REPEAT STRIP_TAC 690 >> PURE_ONCE_REWRITE_TAC [expands_thm] 691 >> Q.EXISTS_TAC `\x y. ?E1 E2 L'. (x = restr L' E1) /\ (y = restr L' E2) /\ E1 expands E2` 692 >> BETA_TAC 693 >> CONJ_TAC >- ( take [`E`, `E'`, `L`] >> ASM_REWRITE_TAC [] ) 694 >> PURE_ONCE_REWRITE_TAC [EXPANSION] 695 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 696 >| [ (* goal 1 (of 4) *) 697 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 698 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 699 IMP_RES_TAC TRANS_RESTR >- IMP_RES_TAC Action_distinct_label \\ 700 IMP_RES_TAC (MATCH_MP expands_TRANS_label (ASSUME ``E1 expands E2``)) \\ 701 Q.EXISTS_TAC `restr L' E2'` \\ 702 ASM_REWRITE_TAC 703 [MATCH_MP WEAK_RESTR_label 704 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 705 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 706 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 707 (ASSUME ``WEAK_TRANS E2 (label l) E2'``)])] \\ 708 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> Q.EXISTS_TAC `l'` >> rfs [Action_11] ) \\ 709 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [], 710 (* goal 2 (of 4) *) 711 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 712 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 713 IMP_RES_TAC TRANS_RESTR >- IMP_RES_TAC Action_distinct_label \\ 714 IMP_RES_TAC (MATCH_MP expands_TRANS_label' (ASSUME ``E1 expands E2``)) \\ 715 Q.EXISTS_TAC `restr L' E1'` \\ 716 ASM_REWRITE_TAC 717 [MATCH_MP WEAK_RESTR_label 718 (LIST_CONJ [ASSUME ``~((l': 'b Label) IN L')``, 719 ASSUME ``~((COMPL (l': 'b Label)) IN L')``, 720 REWRITE_RULE [ASSUME ``label (l :'b Label) = label l'``] 721 (ASSUME ``WEAK_TRANS E1 (label l) E1'``)])] \\ 722 take [`E1'`, `E''''`, `L'`] >> ASM_REWRITE_TAC [], 723 (* goal 3 (of 4) *) 724 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = restr L' E1``] 725 (ASSUME ``TRANS E'' tau E1'``)) \\ 726 Rev (IMP_RES_TAC TRANS_RESTR) >- IMP_RES_TAC Action_distinct \\ 727 IMP_RES_TAC (MATCH_MP expands_TRANS_tau (ASSUME ``E1 expands E2``)) 728 >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] \\ 729 take [`E''''`, `E2`, `L'`] >> ASM_REWRITE_TAC [] ) \\ 730 DISJ2_TAC \\ 731 ONCE_ASM_REWRITE_TAC [] \\ 732 Q.EXISTS_TAC `restr L' E2'` \\ 733 CONJ_TAC >- ( MATCH_MP_TAC RESTR >> fs [] ) \\ 734 take [`E''''`, `E2'`, `L'`] >> ASM_REWRITE_TAC [], 735 (* goal 4 (of 4) *) 736 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = restr L' E2``] 737 (ASSUME ``TRANS E''' tau E2'``)) \\ 738 Rev (IMP_RES_TAC TRANS_RESTR) >- IMP_RES_TAC Action_distinct \\ 739 IMP_RES_TAC (MATCH_MP expands_TRANS_tau' (ASSUME ``E1 expands E2``)) \\ 740 Q.EXISTS_TAC `restr L' E1'` \\ 741 Rev CONJ_TAC 742 >- ( take [`E1'`, `E''''`, `L'`] >> ASM_REWRITE_TAC [] ) \\ 743 ONCE_ASM_REWRITE_TAC [] \\ 744 REWRITE_TAC [WEAK_TRANS] \\ 745 STRIP_ASSUME_TAC 746 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS E1 tau E1'``)) \\ 747 take [`restr L' E1''`, `restr L' E2''`] \\ 748 IMP_RES_TAC EPS_RESTR >> fs [] \\ 749 MATCH_MP_TAC RESTR >> fs [] ]); 750 751val expands_SUBST_RELAB = store_thm ( 752 "expands_SUBST_RELAB", 753 ``!E E'. E expands E' ==> !rf. (relab E rf) expands (relab E' rf)``, 754 REPEAT STRIP_TAC 755 >> PURE_ONCE_REWRITE_TAC [expands_thm] 756 >> Q.EXISTS_TAC 757 `\x y. ?E1 E2 rf'. (x = relab E1 rf') /\ (y = relab E2 rf') /\ E1 expands E2` 758 >> BETA_TAC 759 >> CONJ_TAC >- ( take [`E`, `E'`, `rf`] >> ASM_REWRITE_TAC [] ) 760 >> PURE_ONCE_REWRITE_TAC [EXPANSION] 761 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 762 >| [ (* goal 1 (of 4) *) 763 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 764 (ASSUME ``TRANS E'' (label l) E1'``)) \\ 765 IMP_RES_TAC TRANS_RELAB \\ 766 qpat_x_assum `label l = relabel rf' u'` (ASSUME_TAC o SYM) \\ 767 IMP_RES_TAC Relab_label \\ 768 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 769 (ASSUME ``TRANS E1 u' E''''``)) \\ 770 IMP_RES_TAC (MATCH_MP expands_TRANS_label (ASSUME ``E1 expands E2``)) \\ 771 EXISTS_TAC ``relab E2' rf'`` \\ 772 Rev CONJ_TAC 773 >- ( take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 774 ASM_REWRITE_TAC [] \\ 775 qpat_x_assum `relabel rf' u' = label l` (REWRITE_TAC o wrap o SYM) \\ 776 MATCH_MP_TAC RELABELING >> ASM_REWRITE_TAC [], 777 (* goal 2 (of 4) *) 778 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 779 (ASSUME ``TRANS E''' (label l) E2'``)) \\ 780 IMP_RES_TAC TRANS_RELAB \\ 781 qpat_x_assum `label l = relabel rf' u'` (ASSUME_TAC o SYM) \\ 782 IMP_RES_TAC Relab_label \\ 783 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = label l'``] 784 (ASSUME ``TRANS E2 u' E''''``)) \\ 785 IMP_RES_TAC (MATCH_MP expands_TRANS_label' (ASSUME ``E1 expands E2``)) \\ 786 EXISTS_TAC ``relab E1' rf'`` \\ 787 Rev CONJ_TAC 788 >- ( take [`E1'`, `E''''`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 789 ASM_REWRITE_TAC [] \\ 790 IMP_RES_TAC WEAK_RELAB_rf >> PROVE_TAC [], 791 (* goal 3 (of 4) *) 792 ASSUME_TAC (REWRITE_RULE [ASSUME ``E'' = relab E1 rf'``] 793 (ASSUME ``TRANS E'' tau E1'``)) \\ 794 IMP_RES_TAC TRANS_RELAB \\ 795 qpat_x_assum `tau = relabel rf' u'` (ASSUME_TAC o SYM) \\ 796 IMP_RES_TAC Relab_tau \\ 797 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 798 (ASSUME ``TRANS E1 u' E''''``)) \\ 799 IMP_RES_TAC (MATCH_MP expands_TRANS_tau (ASSUME ``E1 expands E2``)) 800 >- ( DISJ1_TAC >> ASM_REWRITE_TAC [] \\ 801 take [`E''''`, `E2`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 802 DISJ2_TAC >> EXISTS_TAC ``relab E2' rf'`` \\ 803 Rev CONJ_TAC 804 >- ( take [`E''''`, `E2'`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 805 ASM_REWRITE_TAC [] \\ 806 qpat_x_assum `relabel rf' u' = tau` (REWRITE_TAC o wrap o SYM) \\ 807 MATCH_MP_TAC RELABELING >> ASM_REWRITE_TAC [], 808 (* goal 4 (of 4) *) 809 ASSUME_TAC (REWRITE_RULE [ASSUME ``E''' = relab E2 rf'``] 810 (ASSUME ``TRANS E''' tau E2'``)) \\ 811 IMP_RES_TAC TRANS_RELAB \\ 812 qpat_x_assum `tau = relabel rf' u'` (ASSUME_TAC o SYM) \\ 813 IMP_RES_TAC Relab_tau \\ 814 ASSUME_TAC (REWRITE_RULE [ASSUME ``(u' :'b Action) = tau``] 815 (ASSUME ``TRANS E2 u' E''''``)) \\ 816 IMP_RES_TAC (MATCH_MP expands_TRANS_tau' (ASSUME ``E1 expands E2``)) \\ 817 EXISTS_TAC ``relab E1' rf'`` \\ 818 Rev CONJ_TAC 819 >- ( take [`E1'`, `E''''`, `rf'`] >> ASM_REWRITE_TAC [] ) \\ 820 ASM_REWRITE_TAC [] \\ 821 qpat_x_assum `relabel rf' u' = tau` (REWRITE_TAC o wrap o SYM) \\ 822 REWRITE_TAC [WEAK_TRANS] \\ 823 STRIP_ASSUME_TAC 824 (REWRITE_RULE [WEAK_TRANS] (ASSUME ``WEAK_TRANS E1 tau E1'``)) \\ 825 take [`relab E1'' rf'`, `relab E2'' rf'`] \\ 826 IMP_RES_TAC EPS_RELAB_rf >> fs [] \\ 827 MATCH_MP_TAC RELABELING >> ASM_REWRITE_TAC [] ]); 828 829val expands_SUBST_GCONTEXT = store_thm ( 830 "expands_SUBST_GCONTEXT", 831 ``!P Q. P expands Q ==> !E. GCONTEXT E ==> (E P) expands (E Q)``, 832 rpt GEN_TAC >> DISCH_TAC 833 >> Induct_on `GCONTEXT` 834 >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 835 >- ASM_REWRITE_TAC [] 836 >- REWRITE_TAC [expands_REFL] 837 >| [ (* goal 1 (of 5) *) 838 MATCH_MP_TAC expands_SUBST_PREFIX >> ASM_REWRITE_TAC [], 839 (* goal 2 (of 5) *) 840 MATCH_MP_TAC expands_PRESD_BY_GUARDED_SUM \\ 841 ASM_REWRITE_TAC [], 842 (* goal 3 (of 5) *) 843 IMP_RES_TAC expands_PRESD_BY_PAR, 844 (* goal 4 (of 5) *) 845 MATCH_MP_TAC expands_SUBST_RESTR >> ASM_REWRITE_TAC [], 846 (* goal 5 (of 5) *) 847 MATCH_MP_TAC expands_SUBST_RELAB >> ASM_REWRITE_TAC [] ]); 848 849val expands_precongruence = store_thm ( 850 "expands_precongruence", ``precongruence1 $expands``, 851 PROVE_TAC [precongruence1_def, expands_PreOrder, expands_SUBST_GCONTEXT]); 852 853(******************************************************************************) 854(* *) 855(* Trace, Weak transition and Expansion *) 856(* *) 857(******************************************************************************) 858 859val expands_AND_TRACE_tau_lemma = Q.prove ( 860 `!E xs E1. TRACE E xs E1 ==> NO_LABEL xs ==> 861 !E'. E expands E' ==> 862 ?xs' E2. TRACE E' xs' E2 /\ E1 expands E2 /\ 863 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'`, 864 HO_MATCH_MP_TAC TRACE_strongind 865 >> rpt STRIP_TAC 866 >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [] \\ 867 REWRITE_TAC [TRACE_REFL, LENGTH] >> RW_TAC arith_ss [] ) 868 >> IMP_RES_TAC NO_LABEL_cases 869 >> qpat_x_assum `NO_LABEL xs ==> X` 870 (ASSUME_TAC o (fn thm => MATCH_MP thm (ASSUME ``NO_LABEL (xs :'b Action list)``))) 871 >> Cases_on `h` >> FULL_SIMP_TAC std_ss [Action_distinct_label, LENGTH] 872 >> IMP_RES_TAC expands_TRANS_tau >> RES_TAC (* 2 sub-goals here *) 873 >| [ (* goal 1 (of 2) *) 874 take [`xs'`, `E2`] >> ASM_REWRITE_TAC [] \\ 875 FULL_SIMP_TAC arith_ss [], 876 (* goal 2 (of 2) *) 877 take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 878 CONJ_TAC 879 >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 880 Rev CONJ_TAC 881 >- ( POP_ASSUM MP_TAC >> KILL_TAC \\ 882 REWRITE_TAC [NO_LABEL_def, MEM, Action_distinct_label] ) \\ 883 REWRITE_TAC [LENGTH] \\ 884 FULL_SIMP_TAC arith_ss [] ]); 885 886val expands_AND_TRACE_tau = store_thm ( 887 "expands_AND_TRACE_tau", 888 ``!E E'. E expands E' ==> 889 !xs l E1. TRACE E xs E1 /\ NO_LABEL xs ==> 890 ?xs' E2. TRACE E' xs' E2 /\ E1 expands E2 /\ 891 (LENGTH xs' <= LENGTH xs) /\ NO_LABEL xs'``, 892 NTAC 2 (rpt GEN_TAC >> STRIP_TAC) 893 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] expands_AND_TRACE_tau_lemma) 894 >> RW_TAC std_ss []); 895 896val expands_AND_TRACE_label_lemma = Q.prove ( 897 `!E xs E1. TRACE E xs E1 ==> !l. UNIQUE_LABEL (label l) xs ==> 898 !E'. E expands E' ==> 899 ?xs' E2. TRACE E' xs' E2 /\ E1 expands E2 /\ 900 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'`, 901 HO_MATCH_MP_TAC TRACE_strongind 902 >> rpt STRIP_TAC 903 >- ( take [`[]`, `E'`] >> ASM_REWRITE_TAC [] \\ 904 REWRITE_TAC [TRACE_REFL, LENGTH] >> RW_TAC arith_ss [] ) 905 >> REWRITE_TAC [LENGTH] 906 >> Cases_on `h` (* 2 sub-goals here *) 907 >| [ (* goal 1 (of 2) *) 908 IMP_RES_TAC expands_TRANS_tau >| (* 2 sub-goals here *) 909 [ (* goal 1.1 (of 2) *) 910 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases1) \\ 911 RES_TAC \\ 912 take [`xs'`, `E2`] >> ASM_REWRITE_TAC [] \\ 913 FULL_SIMP_TAC arith_ss [], 914 (* goal 1.2 (of 2) *) 915 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases1) \\ 916 RES_TAC \\ 917 take [`tau :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 918 CONJ_TAC >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 919 CONJ_TAC >- ( FULL_SIMP_TAC arith_ss [LENGTH] ) \\ 920 REWRITE_TAC [UNIQUE_LABEL_cases1] >> ASM_REWRITE_TAC [] ], 921 (* goal 2 of 2 *) 922 IMP_RES_TAC expands_TRANS_label \\ 923 IMP_RES_TAC (EQ_IMP_LR UNIQUE_LABEL_cases2) \\ 924 IMP_RES_TAC (MATCH_MP expands_AND_TRACE_tau (ASSUME ``E' expands E2``)) \\ 925 NTAC 4 (POP_ASSUM K_TAC) \\ 926 take [`label x :: xs'`, `E2'`] >> ASM_REWRITE_TAC [] \\ 927 CONJ_TAC >- ( MATCH_MP_TAC TRACE2 >> Q.EXISTS_TAC `E2` >> ASM_REWRITE_TAC [] ) \\ 928 CONJ_TAC >- ( FULL_SIMP_TAC arith_ss [LENGTH] ) \\ 929 REWRITE_TAC [UNIQUE_LABEL_cases2] >> ASM_REWRITE_TAC [] ]); 930 931val expands_AND_TRACE_label = store_thm ( 932 "expands_AND_TRACE_label", 933 ``!E E'. E expands E' ==> 934 !xs l E1. TRACE E xs E1 /\ UNIQUE_LABEL (label l) xs ==> 935 ?xs' E2. TRACE E' xs' E2 /\ E1 expands E2 /\ 936 (LENGTH xs' <= LENGTH xs) /\ UNIQUE_LABEL (label l) xs'``, 937 NTAC 2 (rpt GEN_TAC >> STRIP_TAC) 938 >> MP_TAC (Q.SPECL [`E`, `xs`, `E1`] expands_AND_TRACE_label_lemma) 939 >> RW_TAC std_ss []); 940 941(******************************************************************************) 942(* *) 943(* Bisimulation Upto `expands` and context *) 944(* *) 945(******************************************************************************) 946 947(* 948val BISIM_UPTO_expands_and_C = new_definition ( 949 "BISIM_UPTO_expands_and_C", 950 ``BISIM_UPTO_expands_and_C (Wbsm: ('a, 'b) simulation) = 951 !E E'. 952 Wbsm E E' ==> 953 (!l. 954 (!E1. TRANS E (label l) E1 ==> 955 ?E2. WEAK_TRANS E' (label l) E2 /\ 956 (WEAK_EQUIV O (GCC Wbsm) O $expands) E1 E2) /\ 957 (!E2. TRANS E' (label l) E2 ==> 958 ?E1. WEAK_TRANS E (label l) E1 /\ 959 ($expands O (GCC Wbsm) O WEAK_EQUIV) E1 E2)) /\ 960 (!E1. TRANS E tau E1 ==> 961 ?E2. EPS E' E2 /\ (WEAK_EQUIV O (GCC Wbsm) O $expands) E1 E2) /\ 962 (!E2. TRANS E' tau E2 ==> 963 ?E1. EPS E E1 /\ ($expands O (GCC Wbsm) O WEAK_EQUIV) E1 E2)``); 964 *) 965 966(* Bibliography: 967 * 968 * [1] Sangiorgi, D.: Equations, contractions, and unique solutions. ACM SIGPLAN Notices. (2015). 969 * [2] Arun-Kumar, S., Hennessy, M.: An efficiency preorder for processes. Acta Informatica. 29, 737���760 (1992). 970 * [3] Sangiorgi, D., Milner, R.: The problem of ���Weak Bisimulation up to.��� CONCUR'92. (1992). 971 *) 972 973val _ = export_theory (); 974val _ = html_theory "Expansion"; 975 976(* last updated: Sep 28, 2017 *) 977