1(* ========================================================================== *) 2(* FILE : UniqueSolutionsScript.sml *) 3(* DESCRIPTION : Milner and Sangiorgi's "Unique Solutions of Equations" *) 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 pred_setTheory relationTheory pairTheory sumTheory listTheory; 15open prim_recTheory arithmeticTheory combinTheory; 16 17open CCSLib CCSTheory TraceTheory StrongEQTheory WeakEQTheory ObsCongrTheory 18 BisimulationUptoTheory CongruenceTheory ExpansionTheory ContractionTheory; 19 20val _ = new_theory "UniqueSolutions"; 21val _ = temp_loose_equality (); 22 23(******************************************************************************) 24(* *) 25(* 1. Milner's unique solutions theorem for STRONG_EQUIV *) 26(* *) 27(******************************************************************************) 28 29(* Lemma 4.13 in Milner's book [1]: 30 If the variable X is weakly guarded in E, and E{P/X} --a-> P', then P' takes the form 31 E'{P/X} (for some expression E'), and moreover, for any Q, E{Q/X} --a-> E'{Q/X}. 32 *) 33val STRONG_UNIQUE_SOLUTION_LEMMA = store_thm ( 34 "STRONG_UNIQUE_SOLUTION_LEMMA", 35 ``!E. WG E ==> 36 !P a P'. TRANS (E P) a P' ==> 37 ?E'. CONTEXT E' /\ (P' = E' P) /\ !Q. TRANS (E Q) a (E' Q)``, 38 Induct_on `WG` >> BETA_TAC 39 >> COUNT_TAC (rpt STRIP_TAC) (* 6 sub-goals here *) 40 >| [ (* goal 1 (of 6) *) 41 Q.EXISTS_TAC `\t. P'` >> SIMP_TAC std_ss [CONTEXT2] >> art [], 42 (* goal 2 (of 6) *) 43 IMP_RES_TAC TRANS_PREFIX >> art [] \\ 44 Q.EXISTS_TAC `e` >> art [PREFIX], 45 (* goal 3 (of 6) *) 46 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 47 [ (* goal 3.1 (of 2) *) 48 RES_TAC \\ 49 Q.EXISTS_TAC `E''` >> art [] \\ 50 GEN_TAC >> MATCH_MP_TAC SUM1 >> art [], 51 (* goal 3.2 (of 2) *) 52 RES_TAC \\ 53 Q.EXISTS_TAC `E''` >> art [] \\ 54 GEN_TAC >> MATCH_MP_TAC SUM2 >> art [] ], 55 (* goal 4 (of 6) *) 56 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 57 [ (* goal 4.1 (of 3) *) 58 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 59 Q.EXISTS_TAC `\t. par (E'' t) (E' t)` \\ 60 BETA_TAC >> REWRITE_TAC [] \\ 61 CONJ_TAC >| (* 2 sub-goals here *) 62 [ (* goal 4.1.1 (of 2) *) 63 MATCH_MP_TAC CONTEXT5 >> art [] \\ 64 IMP_RES_TAC WG_IMP_CONTEXT, 65 (* goal 4.1.2 (of 2) *) 66 GEN_TAC >> MATCH_MP_TAC PAR1 >> art [] ], 67 (* goal 4.2 (of 3) *) 68 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 69 Q.EXISTS_TAC `\t. par (E t) (E'' t)` \\ 70 BETA_TAC >> REWRITE_TAC [] \\ 71 CONJ_TAC >| (* 2 sub-goals here *) 72 [ (* goal 4.2.1 (of 2) *) 73 MATCH_MP_TAC CONTEXT5 >> art [] \\ 74 IMP_RES_TAC WG_IMP_CONTEXT, 75 (* goal 4.2.2 (of 2) *) 76 GEN_TAC >> MATCH_MP_TAC PAR2 >> art [] ], 77 (* goal 4.3 (of 3) *) 78 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 79 Q.EXISTS_TAC `\t. par (E''' t) (E'' t)` \\ 80 BETA_TAC >> REWRITE_TAC [] \\ 81 CONJ_TAC >| (* 2 sub-goals here *) 82 [ (* goal 4.3.1 (of 2) *) 83 MATCH_MP_TAC CONTEXT5 >> art [], 84 (* goal 4.3.2 (of 2) *) 85 GEN_TAC >> MATCH_MP_TAC PAR3 \\ 86 Q.EXISTS_TAC `l` >> art [] ] ], 87 (* goal 5 (of 6) *) 88 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 89 [ (* goal 5.1 (of 2) *) 90 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 91 Q.EXISTS_TAC `\t. restr L (E' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 92 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT6 >> art [] ) \\ 93 GEN_TAC >> MATCH_MP_TAC RESTR \\ 94 FULL_SIMP_TAC std_ss [] \\ 95 PROVE_TAC [], 96 (* goal 5.2 (of 2) *) 97 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 98 Q.EXISTS_TAC `\t. restr L (E' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 99 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT6 >> art [] ) \\ 100 GEN_TAC >> MATCH_MP_TAC RESTR \\ 101 Q.EXISTS_TAC `l` >> FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 102 PROVE_TAC [] ], 103 (* goal 6 (of 6) *) 104 IMP_RES_TAC TRANS_RELAB \\ 105 RES_TAC >> FULL_SIMP_TAC std_ss [] \\ 106 Q.EXISTS_TAC `\t. relab (E' t) rf` >> BETA_TAC >> REWRITE_TAC [] \\ 107 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT7 >> art [] ) \\ 108 GEN_TAC >> MATCH_MP_TAC RELABELING >> art [] ]); 109 110(* Proposition 4.14 in Milner's book [1] (uni-variate version): 111 Let the expression E contains at most the variable X, and let X be 112 weakly guarded in E, then: 113 If P ~ E{P/X} and Q ~ E{Q/X} then P ~ Q. 114 *) 115Theorem STRONG_UNIQUE_SOLUTION : 116 !E P Q. WG E /\ STRONG_EQUIV P (E P) /\ STRONG_EQUIV Q (E Q) ==> STRONG_EQUIV P Q 117Proof 118 rpt STRIP_TAC 119 >> irule (REWRITE_RULE [RSUBSET] STRONG_BISIM_UPTO_THM) 120 >> Q.EXISTS_TAC `\x y. (x = y) \/ (?G. CONTEXT G /\ (x = G P) /\ (y = G Q))` 121 >> BETA_TAC >> reverse CONJ_TAC 122 >- ( DISJ2_TAC >> Q.EXISTS_TAC `\x. x` >> BETA_TAC \\ 123 KILL_TAC >> RW_TAC std_ss [CONTEXT1] ) 124 >> REWRITE_TAC [STRONG_BISIM_UPTO] 125 >> fix [`P'`, `Q'`] 126 >> BETA_TAC >> STRIP_TAC (* 2 sub-goals here *) 127 >- (POP_ASSUM MP_TAC >> RW_TAC std_ss [] >| (* 2 sub-goals here *) 128 [ (* goal 1 (of 2) *) 129 Q.EXISTS_TAC `E1` >> art [O_DEF] \\ 130 Q.EXISTS_TAC `E1` >> art [STRONG_EQUIV_REFL] \\ 131 Q.EXISTS_TAC `E1` >> art [STRONG_EQUIV_REFL] \\ 132 BETA_TAC >> DISJ1_TAC >> REWRITE_TAC [], 133 (* goal 2 (of 2) *) 134 Q.EXISTS_TAC `E2` >> art [O_DEF] \\ 135 Q.EXISTS_TAC `E2` >> art [STRONG_EQUIV_REFL] \\ 136 Q.EXISTS_TAC `E2` >> art [STRONG_EQUIV_REFL] \\ 137 BETA_TAC >> DISJ1_TAC >> REWRITE_TAC [] ]) 138 (* preparing for induction *) 139 >> NTAC 2 POP_ORW 140 >> POP_ASSUM MP_TAC 141 >> Q.SPEC_TAC (`G`, `G`) 142 >> Induct_on `CONTEXT` >> BETA_TAC 143 >> CONJ_TAC (* case 1: "var" *) 144 >- (rpt STRIP_TAC >| (* 2 subgoals *) 145 [ (* goal 1 (of 2) *) 146 Q.PAT_X_ASSUM `STRONG_EQUIV P (E P)` 147 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\ 148 RES_TAC \\ 149 IMP_RES_TAC STRONG_UNIQUE_SOLUTION_LEMMA \\ (* lemma used here *) 150 FULL_SIMP_TAC std_ss [] \\ 151 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 152 Q.PAT_X_ASSUM `STRONG_EQUIV Q (E Q)` 153 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\ 154 RES_TAC >> Q.EXISTS_TAC `E1'` >> art [] \\ 155 REWRITE_TAC [O_DEF] \\ 156 `STRONG_EQUIV (E' Q) E1'` by PROVE_TAC [STRONG_EQUIV_SYM] \\ 157 Q.EXISTS_TAC `E' Q` >> art [] \\ 158 Q.EXISTS_TAC `E' P` >> art [] \\ 159 BETA_TAC >> DISJ2_TAC \\ 160 Q.EXISTS_TAC `E'` >> art [], 161 (* goal 2 (of 2) *) 162 Q.PAT_X_ASSUM `STRONG_EQUIV Q (E Q)` 163 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\ 164 RES_TAC \\ 165 IMP_RES_TAC STRONG_UNIQUE_SOLUTION_LEMMA \\ (* lemma used here *) 166 FULL_SIMP_TAC std_ss [] \\ 167 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 168 Q.PAT_X_ASSUM `STRONG_EQUIV P (E P)` 169 (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [PROPERTY_STAR])) \\ 170 RES_TAC >> Q.EXISTS_TAC `E1` >> art [] \\ 171 REWRITE_TAC [O_DEF] \\ 172 `STRONG_EQUIV (E' P) E1` by PROVE_TAC [STRONG_EQUIV_SYM] \\ 173 `STRONG_EQUIV (E' Q) E2` by PROVE_TAC [STRONG_EQUIV_SYM] \\ 174 Q.EXISTS_TAC `E' Q` >> art [] \\ 175 Q.EXISTS_TAC `E' P` >> art [] \\ 176 BETA_TAC >> DISJ2_TAC \\ 177 Q.EXISTS_TAC `E'` >> art [] ]) 178 >> CONJ_TAC (* case 2: "no var" *) 179 >- (rpt STRIP_TAC >| (* 2 subgoals *) 180 [ (* goal 1 (of 2) *) 181 Q.EXISTS_TAC `E1` >> art [] \\ 182 REWRITE_TAC [O_DEF] \\ 183 Q.EXISTS_TAC `E1` >> art [STRONG_EQUIV_REFL] \\ 184 Q.EXISTS_TAC `E1` >> art [STRONG_EQUIV_REFL] \\ 185 BETA_TAC >> DISJ1_TAC >> RW_TAC std_ss [], 186 (* goal 2 (of 2) *) 187 Q.EXISTS_TAC `E2` >> art [] \\ 188 REWRITE_TAC [O_DEF] \\ 189 Q.EXISTS_TAC `E2` >> art [STRONG_EQUIV_REFL] \\ 190 Q.EXISTS_TAC `E2` >> art [STRONG_EQUIV_REFL] \\ 191 BETA_TAC >> DISJ1_TAC >> RW_TAC std_ss [] ]) 192 >> CONJ_TAC (* case 3: prefix *) 193 >- (Q.X_GEN_TAC `a` >> rpt STRIP_TAC >| (* 2 subgoals *) 194 [ (* goal 1 (of 2) *) 195 IMP_RES_TAC TRANS_PREFIX \\ 196 FULL_SIMP_TAC std_ss [] \\ 197 NTAC 2 (POP_ASSUM K_TAC) \\ 198 Q.EXISTS_TAC `G Q` >> REWRITE_TAC [PREFIX] \\ 199 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 200 Q.EXISTS_TAC `G Q` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\ 201 Q.EXISTS_TAC `G P` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\ 202 DISJ2_TAC >> Q.EXISTS_TAC `G` >> art [], 203 (* goal 2 (of 2) *) 204 IMP_RES_TAC TRANS_PREFIX \\ 205 FULL_SIMP_TAC std_ss [] \\ 206 NTAC 2 (POP_ASSUM K_TAC) \\ 207 Q.EXISTS_TAC `G P` >> REWRITE_TAC [PREFIX] \\ 208 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 209 Q.EXISTS_TAC `G Q` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\ 210 Q.EXISTS_TAC `G P` >> REWRITE_TAC [STRONG_EQUIV_REFL] \\ 211 DISJ2_TAC >> Q.EXISTS_TAC `G` >> art [] ]) 212 >> CONJ_TAC (* case 4: sum *) 213 >- (RW_TAC std_ss [TRANS_SUM_EQ] >| (* 4 subgoals *) 214 [ RES_TAC >> Q.EXISTS_TAC `E2` >> rw [], 215 RES_TAC >> Q.EXISTS_TAC `E2` >> rw [], 216 RES_TAC >> Q.EXISTS_TAC `E1` >> rw [], 217 RES_TAC >> Q.EXISTS_TAC `E1` >> rw [] ]) 218 >> CONJ_TAC (* case 5: par *) 219 >- (RW_TAC std_ss [TRANS_PAR_EQ] >| (* 6 subgoals *) 220 [ (* goal 1 (of 6) *) 221 RES_TAC >> Q.EXISTS_TAC `E2 || G' Q` \\ 222 CONJ_TAC >- (DISJ1_TAC >> Q.EXISTS_TAC `E2` >> art []) \\ 223 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 sub-goals here *) 224 [ (* goal 1.1 (of 2) *) 225 rename1 `STRONG_EQUIV E1' y` \\ 226 Q.EXISTS_TAC `y || G' Q` \\ 227 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 228 art [STRONG_EQUIV_REFL]) \\ 229 Q.EXISTS_TAC `y || G' P` \\ 230 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 231 art [STRONG_EQUIV_REFL]) \\ 232 DISJ2_TAC \\ 233 Q.EXISTS_TAC `\t. y || G' t` >> BETA_TAC >> REWRITE_TAC [] \\ 234 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 235 Know `CONTEXT (\t. (\z. y) t || G' t)` 236 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 237 (* goal 1.2 (of 2) *) 238 Q.EXISTS_TAC `G'' Q || G' Q` \\ 239 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 240 art [STRONG_EQUIV_REFL]) \\ 241 Q.EXISTS_TAC `G'' P || G' P` \\ 242 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 243 art [STRONG_EQUIV_REFL]) \\ 244 DISJ2_TAC \\ 245 Q.EXISTS_TAC `\t. G'' t || G' t` >> BETA_TAC >> REWRITE_TAC [] \\ 246 MATCH_MP_TAC CONTEXT5 >> art [] ], 247 (* goal 2 (of 6) *) 248 RES_TAC >> Q.EXISTS_TAC `G Q || E2` \\ 249 CONJ_TAC >- (NDISJ_TAC 1 >> Q.EXISTS_TAC `E2` >> art []) \\ 250 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 sub-goals here *) 251 [ (* goal 2.1 (of 2) *) 252 rename1 `STRONG_EQUIV E1' y` \\ 253 Q.EXISTS_TAC `G Q || y` \\ 254 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 255 art [STRONG_EQUIV_REFL]) \\ 256 Q.EXISTS_TAC `G P || y` \\ 257 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 258 art [STRONG_EQUIV_REFL]) \\ 259 DISJ2_TAC \\ 260 Q.EXISTS_TAC `\t. G t || y` >> BETA_TAC >> REWRITE_TAC [] \\ 261 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 262 Know `CONTEXT (\t. G t || (\z. y) t)` 263 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 264 (* goal 2.2 (of 2) *) 265 Q.EXISTS_TAC `G Q || G'' Q` \\ 266 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 267 art [STRONG_EQUIV_REFL]) \\ 268 Q.EXISTS_TAC `G P || G'' P` \\ 269 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 270 art [STRONG_EQUIV_REFL]) \\ 271 DISJ2_TAC \\ 272 Q.EXISTS_TAC `\t. G t || G'' t` >> BETA_TAC >> REWRITE_TAC [] \\ 273 MATCH_MP_TAC CONTEXT5 >> art [] ], 274 (* goal 3 (of 6) *) 275 RES_TAC >> Q.EXISTS_TAC `E2'' || E2'` \\ 276 CONJ_TAC >- (NDISJ_TAC 2 >> take [`E2''`, `E2'`, `l`] >> art []) \\ 277 Q.PAT_X_ASSUM `X E2 E2'` MP_TAC \\ 278 Q.PAT_X_ASSUM `X E1' E2''` MP_TAC \\ 279 RW_TAC std_ss [O_DEF] >| (* 4 sub-goals here *) 280 [ (* goal 3.1 (of 4) *) 281 rename1 `STRONG_EQUIV E1' x` \\ 282 rename1 `STRONG_EQUIV E2 y` \\ 283 Q.EXISTS_TAC `x || y` \\ 284 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 285 Q.EXISTS_TAC `x || y` \\ 286 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 287 DISJ1_TAC >> REWRITE_TAC [], 288 (* goal 3.2 (of 4) *) 289 rename1 `STRONG_EQUIV E1' y` \\ 290 Q.EXISTS_TAC `y || G'' Q` \\ 291 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 292 Q.EXISTS_TAC `y || G'' P` \\ 293 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 294 DISJ2_TAC \\ 295 Q.EXISTS_TAC `\t. y || G'' t` >> BETA_TAC >> REWRITE_TAC [] \\ 296 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 297 Know `CONTEXT (\t. (\z. y) t || G'' t)` 298 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 299 (* goal 3.3 (of 4) *) 300 rename1 `STRONG_EQUIV E2 y` \\ 301 Q.EXISTS_TAC `G'' Q || y` \\ 302 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 303 Q.EXISTS_TAC `G'' P || y` \\ 304 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 305 DISJ2_TAC \\ 306 Q.EXISTS_TAC `\t. G'' t || y` >> BETA_TAC >> REWRITE_TAC [] \\ 307 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 308 Know `CONTEXT (\t. G'' t || (\z. y) t)` 309 >- (MATCH_MP_TAC CONTEXT5 >> art []) \\ 310 BETA_TAC >> REWRITE_TAC [], 311 (* goal 3.4 (of 4) *) 312 Q.EXISTS_TAC `G'' Q || G''' Q` \\ 313 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 314 Q.EXISTS_TAC `G'' P || G''' P` \\ 315 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 316 DISJ2_TAC \\ 317 Q.EXISTS_TAC `\t. G'' t || G''' t` >> BETA_TAC >> REWRITE_TAC [] \\ 318 MATCH_MP_TAC CONTEXT5 >> art [] ], 319 (* goal 4 (of 6) *) 320 RES_TAC >> Q.EXISTS_TAC `E1' || G' P` \\ 321 CONJ_TAC >- (DISJ1_TAC >> Q.EXISTS_TAC `E1'` >> art []) \\ 322 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 sub-goals here *) 323 [ (* goal 4.1 (of 2) *) 324 rename1 `STRONG_EQUIV E1' y` \\ 325 Q.EXISTS_TAC `y || G' Q` \\ 326 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 327 art [STRONG_EQUIV_REFL]) \\ 328 Q.EXISTS_TAC `y || G' P` \\ 329 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 330 art [STRONG_EQUIV_REFL]) \\ 331 DISJ2_TAC \\ 332 Q.EXISTS_TAC `\t. y || G' t` >> BETA_TAC >> REWRITE_TAC [] \\ 333 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 334 Know `CONTEXT (\t. (\z. y) t || G' t)` 335 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 336 (* goal 4.2 (of 2) *) 337 Q.EXISTS_TAC `G'' Q || G' Q` \\ 338 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 339 art [STRONG_EQUIV_REFL]) \\ 340 Q.EXISTS_TAC `G'' P || G' P` \\ 341 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 342 art [STRONG_EQUIV_REFL]) \\ 343 DISJ2_TAC \\ 344 Q.EXISTS_TAC `\t. G'' t || G' t` >> BETA_TAC >> REWRITE_TAC [] \\ 345 MATCH_MP_TAC CONTEXT5 >> art [] ], 346 (* goal 5 (of 6) *) 347 RES_TAC >> Q.EXISTS_TAC `G P || E1'` \\ 348 CONJ_TAC >- (NDISJ_TAC 1 >> Q.EXISTS_TAC `E1'` >> art []) \\ 349 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 sub-goals here *) 350 [ (* goal 5.1 (of 2) *) 351 rename1 `STRONG_EQUIV E1' y` \\ 352 Q.EXISTS_TAC `G Q || y` \\ 353 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 354 art [STRONG_EQUIV_REFL]) \\ 355 Q.EXISTS_TAC `G P || y` \\ 356 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 357 art [STRONG_EQUIV_REFL]) \\ 358 DISJ2_TAC \\ 359 Q.EXISTS_TAC `\t. G t || y` >> BETA_TAC >> REWRITE_TAC [] \\ 360 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 361 Know `CONTEXT (\t. G t || (\z. y) t)` 362 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 363 (* goal 5.2 (of 2) *) 364 Q.EXISTS_TAC `G Q || G'' Q` \\ 365 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 366 art [STRONG_EQUIV_REFL]) \\ 367 Q.EXISTS_TAC `G P || G'' P` \\ 368 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR \\ 369 art [STRONG_EQUIV_REFL]) \\ 370 DISJ2_TAC \\ 371 Q.EXISTS_TAC `\t. G t || G'' t` >> BETA_TAC >> REWRITE_TAC [] \\ 372 MATCH_MP_TAC CONTEXT5 >> art [] ], 373 (* goal 6 (of 6) *) 374 RES_TAC >> Q.EXISTS_TAC `E1'' || E1'` \\ 375 CONJ_TAC >- (NDISJ_TAC 2 >> take [`E1''`, `E1'`, `l`] >> art []) \\ 376 Q.PAT_X_ASSUM `R E1'' E1` MP_TAC \\ 377 Q.PAT_X_ASSUM `R E1' E2'` MP_TAC \\ 378 RW_TAC std_ss [O_DEF] >| (* 4 sub-goals here *) 379 [ (* goal 6.1 (of 4) *) 380 rename1 `STRONG_EQUIV E1' x` \\ 381 rename1 `STRONG_EQUIV y E1` \\ 382 Q.EXISTS_TAC `y || x` \\ 383 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 384 Q.EXISTS_TAC `y || x` \\ 385 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 386 DISJ1_TAC >> REWRITE_TAC [], 387 (* goal 6.2 (of 4) *) 388 rename1 `STRONG_EQUIV E1' y` \\ 389 Q.EXISTS_TAC `G'' Q || y` \\ 390 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 391 Q.EXISTS_TAC `G'' P || y` \\ 392 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 393 DISJ2_TAC \\ 394 Q.EXISTS_TAC `\t. G'' t || y` >> BETA_TAC >> REWRITE_TAC [] \\ 395 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 396 Know `CONTEXT (\t. G'' t || (\z. y) t)` 397 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 398 (* goal 6.3 (of 4) *) 399 rename1 `STRONG_EQUIV y E1` \\ 400 Q.EXISTS_TAC `y || G'' Q` \\ 401 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 402 Q.EXISTS_TAC `y || G'' P` \\ 403 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 404 DISJ2_TAC \\ 405 Q.EXISTS_TAC `\t. y || G'' t` >> BETA_TAC >> REWRITE_TAC [] \\ 406 `CONTEXT (\z. y)` by REWRITE_TAC [CONTEXT2] \\ 407 Know `CONTEXT (\t. (\z. y) t || G'' t)` 408 >- (MATCH_MP_TAC CONTEXT5 >> art []) >> rw [], 409 (* goal 6.4 (of 4) *) 410 Q.EXISTS_TAC `G''' Q || G'' Q` \\ 411 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 412 Q.EXISTS_TAC `G''' P || G'' P` \\ 413 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_PRESD_BY_PAR >> art []) \\ 414 DISJ2_TAC \\ 415 Q.EXISTS_TAC `\t. G''' t || G'' t` >> BETA_TAC >> REWRITE_TAC [] \\ 416 MATCH_MP_TAC CONTEXT5 >> art [] ] ]) 417 >> CONJ_TAC (* case 6: restr *) 418 >- (RW_TAC std_ss [TRANS_RESTR_EQ] >| (* 4 subgoals *) 419 [ (* goal 1 (of 4) *) 420 RES_TAC >> Q.EXISTS_TAC `restr L E2` \\ 421 CONJ_TAC >- (Q.EXISTS_TAC `E2` >> art []) \\ 422 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 subgoals *) 423 [ (* goal 1.1 (of 2) *) 424 rename1 `STRONG_EQUIV y E2` \\ 425 Q.EXISTS_TAC `restr L y` \\ 426 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 427 Q.EXISTS_TAC `restr L y` \\ 428 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 429 DISJ1_TAC >> REWRITE_TAC [], 430 (* goal 1.2 (of 2) *) 431 Q.EXISTS_TAC `restr L (G' Q)` \\ 432 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 433 Q.EXISTS_TAC `restr L (G' P)` \\ 434 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 435 DISJ2_TAC \\ 436 Q.EXISTS_TAC `\t. restr L (G' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 437 MATCH_MP_TAC CONTEXT6 >> art [] ], 438 (* goal 2 (of 4) *) 439 RES_TAC >> Q.EXISTS_TAC `restr L E2` \\ 440 CONJ_TAC >- (Q.EXISTS_TAC `E2` >> art []) \\ 441 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 sub-goals here *) 442 [ (* goal 2.1 (of 2) *) 443 rename1 `STRONG_EQUIV y E2` \\ 444 Q.EXISTS_TAC `restr L y` \\ 445 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 446 Q.EXISTS_TAC `restr L y` \\ 447 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 448 DISJ1_TAC >> REWRITE_TAC [], 449 (* goal 11.2.2 (of 2) *) 450 Q.EXISTS_TAC `restr L (G' Q)` \\ 451 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 452 Q.EXISTS_TAC `restr L (G' P)` \\ 453 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 454 DISJ2_TAC \\ 455 Q.EXISTS_TAC `\t. restr L (G' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 456 MATCH_MP_TAC CONTEXT6 >> art [] ], 457 (* goal 3 (of 4) *) 458 RES_TAC >> Q.EXISTS_TAC `restr L E1` \\ 459 CONJ_TAC >- (Q.EXISTS_TAC `E1` >> art []) \\ 460 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 subgoals *) 461 [ (* goal 3.1 (of 2) *) 462 rename1 `STRONG_EQUIV E1 y` \\ 463 Q.EXISTS_TAC `restr L y` \\ 464 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 465 Q.EXISTS_TAC `restr L y` \\ 466 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 467 DISJ1_TAC >> REWRITE_TAC [], 468 (* goal 3.2 (of 2) *) 469 Q.EXISTS_TAC `restr L (G' Q)` \\ 470 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 471 Q.EXISTS_TAC `restr L (G' P)` \\ 472 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 473 DISJ2_TAC \\ 474 Q.EXISTS_TAC `\t. restr L (G' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 475 MATCH_MP_TAC CONTEXT6 >> art [] ], 476 (* goal 4 (of 4) *) 477 RES_TAC >> Q.EXISTS_TAC `restr L E1` \\ 478 CONJ_TAC >- (Q.EXISTS_TAC `E1` >> art []) \\ 479 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 subgoals *) 480 [ (* goal 4.1 (of 2) *) 481 rename1 `STRONG_EQUIV E1 y` \\ 482 Q.EXISTS_TAC `restr L y` \\ 483 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 484 Q.EXISTS_TAC `restr L y` \\ 485 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 486 DISJ1_TAC >> REWRITE_TAC [], 487 (* goal 4.2 (of 2) *) 488 Q.EXISTS_TAC `restr L (G' Q)` \\ 489 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 490 Q.EXISTS_TAC `restr L (G' P)` \\ 491 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> art []) \\ 492 DISJ2_TAC \\ 493 Q.EXISTS_TAC `\t. restr L (G' t)` >> BETA_TAC >> REWRITE_TAC [] \\ 494 MATCH_MP_TAC CONTEXT6 >> art [] ] ]) 495 (* final case: relab *) 496 >> RW_TAC std_ss [TRANS_RELAB_EQ] (* 2 subgoals *) 497 >| [ (* goal 1 (of 2) *) 498 RES_TAC >> Q.EXISTS_TAC `relab E2 rf` \\ 499 rename1 `TRANS (G Q) u E2` \\ 500 CONJ_TAC >- (take [`u`, `E2`] >> art []) \\ 501 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| (* 2 subgoals *) 502 [ (* goal 13.1 (of 2) *) 503 rename1 `STRONG_EQUIV y E2` \\ 504 Q.EXISTS_TAC `relab y rf` \\ 505 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art [] ) \\ 506 Q.EXISTS_TAC `relab y rf` \\ 507 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 508 DISJ1_TAC >> REWRITE_TAC [], 509 (* goal 13.2 (of 2) *) 510 Q.EXISTS_TAC `relab (G' Q) rf` \\ 511 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 512 Q.EXISTS_TAC `relab (G' P) rf` \\ 513 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 514 DISJ2_TAC \\ 515 Q.EXISTS_TAC `\t. relab (G' t) rf` >> BETA_TAC >> REWRITE_TAC [] \\ 516 MATCH_MP_TAC CONTEXT7 >> art [] ], 517 (* goal 2 (of 2) *) 518 RES_TAC >> Q.EXISTS_TAC `relab E1 rf` \\ 519 rename1 `TRANS (G P) u E1` \\ 520 CONJ_TAC >- (take [`u`, `E1`] >> art []) \\ 521 POP_ASSUM MP_TAC >> RW_TAC std_ss [O_DEF] >| 522 [ (* goal 14.1 (of 2) *) 523 rename1 `STRONG_EQUIV E1 y` \\ 524 Q.EXISTS_TAC `relab y rf` \\ 525 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 526 Q.EXISTS_TAC `relab y rf` \\ 527 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 528 DISJ1_TAC >> REWRITE_TAC [], 529 (* goal 14.2 (of 2) *) 530 Q.EXISTS_TAC `relab (G' Q) rf` \\ 531 reverse CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 532 Q.EXISTS_TAC `relab (G' P) rf` \\ 533 CONJ_TAC >- (MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> art []) \\ 534 DISJ2_TAC \\ 535 Q.EXISTS_TAC `\t. relab (G' t) rf` >> BETA_TAC >> REWRITE_TAC [] \\ 536 MATCH_MP_TAC CONTEXT7 >> art [] ] ] 537QED 538 539(******************************************************************************) 540(* *) 541(* 2. Milner's unique solutions theorem for WEAK_EQUIV *) 542(* *) 543(******************************************************************************) 544 545(* Lemma 7.12 in Milner's book [1]: 546 If the variable X is guarded and sequential in G, and G{P/X} --a-> P', then there is 547 an expression H such that G --a--> H, P' = H{P/X} and, for any Q, G{Q/X} --a-> H{Q/X}. 548 Moreover H is sequential, and if a = tau then H is also guarded. 549 *) 550val WEAK_UNIQUE_SOLUTION_LEMMA = store_thm ( 551 "WEAK_UNIQUE_SOLUTION_LEMMA", 552 ``!G. SG G /\ GSEQ G ==> 553 !P a P'. TRANS (G P) a P' ==> 554 ?H. GSEQ H /\ ((a = tau) ==> SG H) /\ 555 (P' = H P) /\ !Q. TRANS (G Q) a (H Q)``, 556 HO_MATCH_MP_TAC SG_GSEQ_strong_induction 557 >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 558 >| [ (* goal 1 (of 7) *) 559 Q.EXISTS_TAC `\t. P'` >> BETA_TAC \\ 560 ASM_SIMP_TAC std_ss [GSEQ2] \\ 561 DISCH_TAC \\ 562 REWRITE_TAC [SG1], 563 (* goal 2 (of 7), `a = tau` used here! *) 564 IMP_RES_TAC TRANS_PREFIX \\ 565 FULL_SIMP_TAC std_ss [] \\ 566 NTAC 2 (POP_ASSUM K_TAC) \\ 567 Q.EXISTS_TAC `G` >> art [] \\ 568 SIMP_TAC std_ss [Action_distinct_label] \\ 569 REWRITE_TAC [PREFIX], 570 (* goal 3 (of 7) *) 571 IMP_RES_TAC TRANS_PREFIX \\ 572 FULL_SIMP_TAC std_ss [] \\ 573 NTAC 3 (POP_ASSUM K_TAC) \\ 574 Q.EXISTS_TAC `G` \\ 575 ASM_SIMP_TAC std_ss [PREFIX], 576 (* goal 4 (of 7) *) 577 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 578 [ (* goal 4.1 (of 2) *) 579 IMP_RES_TAC TRANS_PREFIX \\ 580 FULL_SIMP_TAC std_ss [] \\ 581 Q.EXISTS_TAC `G` >> art [] \\ 582 GEN_TAC >> MATCH_MP_TAC SUM1 \\ 583 REWRITE_TAC [PREFIX], 584 (* goal 4.2 (of 2) *) 585 IMP_RES_TAC TRANS_PREFIX \\ 586 FULL_SIMP_TAC std_ss [] \\ 587 Q.EXISTS_TAC `G'` >> art [] \\ 588 GEN_TAC >> MATCH_MP_TAC SUM2 \\ 589 REWRITE_TAC [PREFIX] ], 590 (* goal 5 (of 7) *) 591 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 592 [ (* goal 4.1 (of 2) *) 593 IMP_RES_TAC TRANS_PREFIX \\ 594 FULL_SIMP_TAC std_ss [] \\ 595 Q.EXISTS_TAC `G` >> art [] \\ 596 GEN_TAC >> MATCH_MP_TAC SUM1 \\ 597 REWRITE_TAC [PREFIX], 598 (* goal 4.2 (of 2) *) 599 IMP_RES_TAC TRANS_PREFIX \\ 600 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 601 Q.EXISTS_TAC `e2` >> art [] \\ 602 GEN_TAC >> MATCH_MP_TAC SUM2 \\ 603 REWRITE_TAC [PREFIX] ], 604 (* goal 6 (of 7) *) 605 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 606 [ (* goal 4.1 (of 2) *) 607 IMP_RES_TAC TRANS_PREFIX \\ 608 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 609 Q.EXISTS_TAC `e1` >> art [] \\ 610 GEN_TAC >> MATCH_MP_TAC SUM1 \\ 611 REWRITE_TAC [PREFIX], 612 (* goal 4.2 (of 2) *) 613 IMP_RES_TAC TRANS_PREFIX \\ 614 FULL_SIMP_TAC std_ss [] \\ 615 Q.EXISTS_TAC `G` >> art [] \\ 616 GEN_TAC >> MATCH_MP_TAC SUM2 \\ 617 REWRITE_TAC [PREFIX] ], 618 (* goal 7 (of 7) *) 619 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 620 [ (* goal 4.1 (of 2) *) 621 IMP_RES_TAC TRANS_PREFIX \\ 622 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 623 Q.EXISTS_TAC `e1` >> art [] \\ 624 GEN_TAC >> MATCH_MP_TAC SUM1 \\ 625 REWRITE_TAC [PREFIX], 626 (* goal 4.2 (of 2) *) 627 IMP_RES_TAC TRANS_PREFIX \\ 628 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 629 Q.EXISTS_TAC `e2` >> art [] \\ 630 GEN_TAC >> MATCH_MP_TAC SUM2 \\ 631 REWRITE_TAC [PREFIX] ] ]); 632 633(* The EPS version of WEAK_UNIQUE_SOLUTION_LEMMA. 634 NOTE: the WEAK_TRANS version cannot be derived, because of the missing of SG in the middle. 635 *) 636val WEAK_UNIQUE_SOLUTION_LEMMA_EPS = store_thm ( 637 "WEAK_UNIQUE_SOLUTION_LEMMA_EPS", 638 ``!G. SG G /\ GSEQ G ==> 639 !P P'. EPS (G P) P' ==> 640 ?H. SG H /\ GSEQ H /\ (P' = H P) /\ !Q. EPS (G Q) (H Q)``, 641 rpt STRIP_TAC 642 >> Q.ABBREV_TAC `GP = G P` 643 >> POP_ASSUM MP_TAC 644 >> Q.SPEC_TAC (`P`, `P`) 645 >> POP_ASSUM MP_TAC 646 >> Q.SPEC_TAC (`P'`, `P'`) 647 >> Q.SPEC_TAC (`GP`, `GP`) 648 >> HO_MATCH_MP_TAC EPS_strongind_right 649 >> rpt STRIP_TAC (* 2 sub-goals here *) 650 >- ( Q.EXISTS_TAC `G` >> art [] \\ 651 Q.UNABBREV_TAC `GP` >> art [EPS_REFL] ) 652 >> RES_TAC 653 >> Q.UNABBREV_TAC `GP` 654 >> Q.PAT_X_ASSUM `!P''. Abbrev (G P = G P'') ==> X` K_TAC 655 >> FULL_SIMP_TAC std_ss [] 656 >> IMP_RES_TAC (Q.SPEC `H` WEAK_UNIQUE_SOLUTION_LEMMA) (* lemma used here *) 657 >> FULL_SIMP_TAC std_ss [] 658 >> Q.EXISTS_TAC `H''` 659 >> art [EQ_SYM] 660 >> GEN_TAC 661 >> `EPS (G Q) (H Q) /\ EPS (H Q) (H'' Q)` by PROVE_TAC [ONE_TAU] 662 >> IMP_RES_TAC EPS_TRANS); 663 664val GSEQ_EPS_lemma = Q.prove ( 665 `!E P Q R H. SG E /\ GSEQ E /\ WEAK_EQUIV P (E P) /\ WEAK_EQUIV Q (E Q) /\ GSEQ H /\ 666 (R = \x y. ?H. GSEQ H /\ (x = H P) /\ (y = H Q)) 667 ==> (!P'. EPS (H P) P' ==> ?Q'. EPS (H Q) Q' /\ (WEAK_EQUIV O R O WEAK_EQUIV) P' Q') /\ 668 (!Q'. EPS (H Q) Q' ==> ?P'. EPS (H P) P' /\ (WEAK_EQUIV O R O WEAK_EQUIV) P' Q')`, 669 (* proof *) 670 rpt GEN_TAC >> STRIP_TAC 671 >> `WEAK_EQUIV (H P) ((H o E) P) /\ WEAK_EQUIV (H Q) ((H o E) Q)` 672 by PROVE_TAC [WEAK_EQUIV_SUBST_GSEQ, o_DEF] 673 >> `SG (H o E) /\ GSEQ (H o E)` by PROVE_TAC [SG_GSEQ_combin] 674 >> rpt STRIP_TAC (* 2 sub-goals here *) 675 >| [ (* goal 1 (of 2) *) 676 IMP_RES_TAC (Q.SPECL [`H P`, `(H o E) P`] WEAK_EQUIV_EPS) \\ 677 MP_TAC (Q.SPEC `(H :('a, 'b) context) o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 678 RW_TAC bool_ss [] >> POP_ASSUM (MP_TAC o (Q.SPECL [`P`, `E2`])) \\ 679 RW_TAC bool_ss [] \\ 680 POP_ASSUM (ASSUME_TAC o BETA_RULE o (Q.SPEC `Q`)) \\ 681 MP_TAC (Q.SPECL [`(H :('a, 'b) context) Q`, 682 `((H :('a, 'b) context) o (E :('a, 'b) context)) Q`] 683 WEAK_EQUIV_EPS') >> RW_TAC bool_ss [] \\ 684 POP_ASSUM (MP_TAC o (Q.SPEC `(H' :('a, 'b) context) Q`)) \\ 685 RW_TAC bool_ss [] \\ 686 Q.EXISTS_TAC `E1` >> art [] \\ 687 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 688 `WEAK_EQUIV (H' Q) E1` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 689 Q.EXISTS_TAC `H' Q` >> art [] \\ 690 Q.EXISTS_TAC `H' P` >> art [] \\ 691 Q.EXISTS_TAC `H'` >> art [], 692 (* goal 2 (of 2) *) 693 IMP_RES_TAC (Q.SPECL [`H Q`, `(H o E) Q`] WEAK_EQUIV_EPS) \\ 694 MP_TAC (Q.SPEC `(H :('a, 'b) context) o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 695 RW_TAC bool_ss [] >> POP_ASSUM (MP_TAC o (Q.SPECL [`Q`, `E2`])) \\ 696 RW_TAC bool_ss [] \\ 697 POP_ASSUM (ASSUME_TAC o BETA_RULE o (Q.SPEC `P`)) \\ 698 MP_TAC (Q.SPECL [`(H :('a, 'b) context) P`, 699 `((H :('a, 'b) context) o (E :('a, 'b) context)) P`] 700 WEAK_EQUIV_EPS') >> RW_TAC bool_ss [] \\ 701 POP_ASSUM (MP_TAC o (Q.SPEC `(H' :('a, 'b) context) P`)) \\ 702 RW_TAC bool_ss [] \\ 703 Q.EXISTS_TAC `E1` >> art [] \\ 704 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 705 `WEAK_EQUIV (H' Q) Q'` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 706 Q.EXISTS_TAC `H' Q` >> art [] \\ 707 Q.EXISTS_TAC `H' P` >> art [] \\ 708 Q.EXISTS_TAC `H'` >> art [] ]); 709 710(* Proposition 7.13 in Milner's book [1]: 711 Let the expression E contains at most the variable X, and let X be guarded and sequential 712 in E, then: 713 If P = E{P/X} and Q = E{Q/X} then P = Q. (here "=" means WEAK_EQUIV) 714 *) 715Theorem WEAK_UNIQUE_SOLUTION : 716 !E P Q. SG E /\ GSEQ E /\ WEAK_EQUIV P (E P) /\ WEAK_EQUIV Q (E Q) 717 ==> WEAK_EQUIV P Q 718Proof 719 rpt STRIP_TAC 720 >> irule (REWRITE_RULE [RSUBSET] WEAK_BISIM_UPTO_ALT_THM) 721 >> Q.EXISTS_TAC `\x y. ?H. GSEQ H /\ (x = H P) /\ (y = H Q)` 722 >> BETA_TAC 723 >> reverse CONJ_TAC 724 >- (Q.EXISTS_TAC `\t. t` >> BETA_TAC >> REWRITE_TAC [GSEQ1]) 725 >> REWRITE_TAC [WEAK_BISIM_UPTO_ALT] 726 >> fix [`P'`, `Q'`] 727 >> BETA_TAC >> STRIP_TAC >> art [] 728 >> NTAC 2 (POP_ASSUM K_TAC) 729 >> Q.ABBREV_TAC `R = \x y. ?H. GSEQ H /\ (x = H P) /\ (y = H Q)` 730 >> `WEAK_EQUIV (H P) ((H o E) P) /\ WEAK_EQUIV (H Q) ((H o E) Q)` 731 by PROVE_TAC [WEAK_EQUIV_SUBST_GSEQ, o_DEF] 732 >> `SG (H o E) /\ GSEQ (H o E)` by PROVE_TAC [SG_GSEQ_combin] 733 >> rpt STRIP_TAC (* 4 sub-goals here *) 734 >| [ (* goal 1 (of 4) *) 735 `?E3. WEAK_TRANS ((H o E) P) (label l) E3 /\ WEAK_EQUIV E1 E3` 736 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label] \\ 737 Q.PAT_X_ASSUM `WEAK_TRANS ((H o E) P) (label l) E3` 738 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 739 IMP_RES_TAC (Q.SPEC `H o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 740 NTAC 4 (POP_ASSUM K_TAC) \\ 741 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 742 `TRANS (H' P) (label l) E2` by PROVE_TAC [] \\ 743 IMP_RES_TAC (Q.SPEC `H'` WEAK_UNIQUE_SOLUTION_LEMMA) \\ 744 NTAC 7 (POP_ASSUM K_TAC) \\ 745 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 746 `EPS (H'' P) E3` by PROVE_TAC [] \\ 747 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H''`] GSEQ_EPS_lemma) \\ 748 RW_TAC std_ss [] >> POP_ASSUM K_TAC \\ 749 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 750 `WEAK_TRANS ((H o E) Q) (label l) Q'` by PROVE_TAC [WEAK_TRANS] \\ 751 `?Q3. WEAK_TRANS (H Q) (label l) Q3 /\ WEAK_EQUIV Q3 Q'` 752 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label'] \\ 753 Q.EXISTS_TAC `Q3` >> art [] \\ 754 Q.PAT_X_ASSUM `X E3 Q'` MP_TAC \\ 755 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 756 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 757 Q.UNABBREV_TAC `R` >> BETA_TAC >> rpt STRIP_TAC \\ 758 `WEAK_EQUIV y Q3` by PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM] \\ 759 Q.EXISTS_TAC `y` >> art [] \\ 760 `WEAK_EQUIV E1 y'` by PROVE_TAC [WEAK_EQUIV_TRANS] \\ 761 Q.EXISTS_TAC `y'` >> art [] \\ 762 Q.EXISTS_TAC `H'''` >> art [], 763(* 764 (case 4) (case 1) 765 H P ======== eps =====> P3 H P ================= l ==============> E1 766 | | | | 767 ~~ ~~ ~~ ~~ 768 | | | | 769 H(E(P)) ==== eps =====> H' P H(E(P)) ==eps=> E1' --l-> E2 ==eps=> E3 ~~ y' 770 | (H' P) (H'' P) | 771 R R 772 | | 773 H(E(Q)) ==== eps =====> E3 = H' Q H(E(Q)) ==eps=> H' Q --l-> H'' Q ==eps=> Q' ~~ y 774 | | | | 775 ~~ ~~ ~~ ~~ 776 | | | | 777 H Q ======== tau =====> E2 H Q ================== l ==============> Q3 778 *) 779 (* goal 2 (of 4) *) 780 `?E3. WEAK_TRANS ((H o E) Q) (label l) E3 /\ WEAK_EQUIV E2 E3` 781 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label] \\ 782 Q.PAT_X_ASSUM `WEAK_TRANS ((H o E) Q) (label l) E3` 783 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 784 IMP_RES_TAC (Q.SPEC `H o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 785 NTAC 4 (POP_ASSUM K_TAC) \\ 786 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 787 `TRANS (H' Q) (label l) E2'` by PROVE_TAC [] \\ 788 IMP_RES_TAC (Q.SPEC `H'` WEAK_UNIQUE_SOLUTION_LEMMA) \\ 789 NTAC 7 (POP_ASSUM K_TAC) \\ 790 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 791 `EPS (H'' Q) E3` by PROVE_TAC [] \\ 792 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H''`] GSEQ_EPS_lemma) \\ 793 RW_TAC std_ss [] \\ 794 Q.PAT_X_ASSUM `!P'. EPS (H'' P) P' ==> X` K_TAC \\ 795 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 796 `WEAK_TRANS ((H o E) P) (label l) P'` by PROVE_TAC [WEAK_TRANS] \\ 797 `?P3. WEAK_TRANS (H P) (label l) P3 /\ WEAK_EQUIV P3 P'` 798 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label'] \\ 799 Q.EXISTS_TAC `P3` >> art [] \\ 800 Q.PAT_X_ASSUM `X P' E3` MP_TAC \\ 801 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 802 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 803 Q.UNABBREV_TAC `R` >> BETA_TAC >> rpt STRIP_TAC \\ 804 `WEAK_EQUIV y E2` by PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM] \\ 805 Q.EXISTS_TAC `y` >> art [] \\ 806 `WEAK_EQUIV P3 y'` by PROVE_TAC [WEAK_EQUIV_TRANS] \\ 807 Q.EXISTS_TAC `y'` >> art [] \\ 808 Q.EXISTS_TAC `H'''` >> art [], 809(* 810 (case 3) (case 2) 811 H P ======== tau =====> E1 H P ================== l ==============> P3 812 | | | | 813 ~~ ~~ ~~ ~~ 814 | | | | 815 H(E(P)) ==== eps =====> E3 = H' P H(E(P)) ==eps=> H' P --l-> H'' P ==eps==> P' ~~ y' 816 | | 817 R R 818 | (H' Q) (H'' Q) | 819 H(E(Q)) ==== eps =====> H' Q H(E(Q)) ==eps=> E1' --l-> E2' ==eps==> E3 ~~ y 820 | | | | 821 ~~ ~~ ~~ ~~ 822 | | | | 823 H Q ======== eps =====> Q3 H Q ================== l ==============> E2 824 *) 825 (* goal 3 (of 4) *) 826 `?E3. EPS ((H o E) P) E3 /\ WEAK_EQUIV E1 E3` by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_tau] \\ 827 IMP_RES_TAC (Q.SPEC `H o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 828 NTAC 4 (POP_ASSUM K_TAC) \\ 829 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 830 `?Q3. EPS (H Q) Q3 /\ WEAK_EQUIV Q3 (H' Q)` by PROVE_TAC [WEAK_EQUIV_EPS'] \\ 831 Q.EXISTS_TAC `Q3` >> art [] \\ 832 Q.UNABBREV_TAC `R` >> REWRITE_TAC [O_DEF] >> BETA_TAC \\ 833 `WEAK_EQUIV (H' Q) Q3` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 834 Q.EXISTS_TAC `H' Q` >> art [] \\ 835 Q.EXISTS_TAC `E3` >> art [] \\ 836 Q.EXISTS_TAC `H'` >> art [], 837 (* goal 4 (of 4) *) 838 `?E3. EPS ((H o E) Q) E3 /\ WEAK_EQUIV E2 E3` by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_tau] \\ 839 IMP_RES_TAC (Q.SPEC `H o E` WEAK_UNIQUE_SOLUTION_LEMMA_EPS) \\ 840 NTAC 4 (POP_ASSUM K_TAC) \\ 841 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 842 `?P3. EPS (H P) P3 /\ WEAK_EQUIV P3 (H' P)` by PROVE_TAC [WEAK_EQUIV_EPS'] \\ 843 Q.EXISTS_TAC `P3` >> art [] \\ 844 Q.UNABBREV_TAC `R` >> REWRITE_TAC [O_DEF] >> BETA_TAC \\ 845 `WEAK_EQUIV E3 E2` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 846 Q.EXISTS_TAC `E3` >> art [] \\ 847 Q.EXISTS_TAC `H' P` >> art [] \\ 848 Q.EXISTS_TAC `H'` >> art [] ] 849QED 850 851(******************************************************************************) 852(* *) 853(* 3. Milner's unique solutions theorem for OBS_CONGR *) 854(* *) 855(******************************************************************************) 856 857val OBS_UNIQUE_SOLUTION_LEMMA = store_thm ( 858 "OBS_UNIQUE_SOLUTION_LEMMA", 859 ``!G. SG G /\ SEQ G ==> 860 !P a P'. TRANS (G P) a P' ==> 861 ?H. SEQ H /\ ((a = tau) ==> SG H) /\ 862 (P' = H P) /\ !Q. TRANS (G Q) a (H Q)``, 863 HO_MATCH_MP_TAC SG_SEQ_strong_induction 864 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 865 >| [ (* goal 1 (of 4) *) 866 Q.EXISTS_TAC `\t. P'` >> BETA_TAC \\ 867 ASM_SIMP_TAC std_ss [SEQ2] \\ 868 DISCH_TAC \\ 869 REWRITE_TAC [SG1], 870 (* goal 2 (of 4), `a = tau` used here! *) 871 IMP_RES_TAC TRANS_PREFIX \\ 872 FULL_SIMP_TAC std_ss [] \\ 873 NTAC 2 (POP_ASSUM K_TAC) \\ 874 Q.EXISTS_TAC `G` >> art [] \\ 875 SIMP_TAC std_ss [Action_distinct_label] \\ 876 REWRITE_TAC [PREFIX], 877 (* goal 3 (of 4) *) 878 IMP_RES_TAC TRANS_PREFIX \\ 879 FULL_SIMP_TAC std_ss [] \\ 880 NTAC 3 (POP_ASSUM K_TAC) \\ 881 Q.EXISTS_TAC `G` \\ 882 ASM_SIMP_TAC std_ss [PREFIX], 883 (* goal 4 (of 4) *) 884 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 885 [ (* goal 4.1 (of 2) *) 886 RES_TAC >> Q.EXISTS_TAC `H` >> art [] \\ 887 GEN_TAC >> MATCH_MP_TAC SUM1 >> art [], 888 (* goal 4.2 (of 2) *) 889 RES_TAC >> Q.EXISTS_TAC `H` >> art [] \\ 890 GEN_TAC >> MATCH_MP_TAC SUM2 >> art [] ] ]); 891 892(* The EPS version of OBS_UNIQUE_SOLUTION_LEMMA. 893 NOTE: the WEAK_TRANS version cannot be derived, because of the missing of SG in the middle. 894 *) 895val OBS_UNIQUE_SOLUTION_LEMMA_EPS = store_thm ( 896 "OBS_UNIQUE_SOLUTION_LEMMA_EPS", 897 ``!G. SG G /\ SEQ G ==> 898 !P P'. EPS (G P) P' ==> 899 ?H. SG H /\ SEQ H /\ (P' = H P) /\ !Q. EPS (G Q) (H Q)``, 900 rpt STRIP_TAC 901 >> Q.ABBREV_TAC `GP = G P` 902 >> POP_ASSUM MP_TAC 903 >> Q.SPEC_TAC (`P`, `P`) 904 >> POP_ASSUM MP_TAC 905 >> Q.SPEC_TAC (`P'`, `P'`) 906 >> Q.SPEC_TAC (`GP`, `GP`) 907 >> HO_MATCH_MP_TAC EPS_strongind_right 908 >> rpt STRIP_TAC (* 2 sub-goals here *) 909 >- ( Q.EXISTS_TAC `G` >> art [] \\ 910 Q.UNABBREV_TAC `GP` >> art [EPS_REFL] ) 911 >> RES_TAC 912 >> Q.UNABBREV_TAC `GP` 913 >> Q.PAT_X_ASSUM `!P''. Abbrev (G P = G P'') ==> X` K_TAC 914 >> FULL_SIMP_TAC std_ss [] 915 >> IMP_RES_TAC (Q.SPEC `H` OBS_UNIQUE_SOLUTION_LEMMA) (* lemma used here *) 916 >> FULL_SIMP_TAC std_ss [] 917 >> Q.EXISTS_TAC `H''` 918 >> art [EQ_SYM] 919 >> GEN_TAC 920 >> `EPS (G Q) (H Q) /\ EPS (H Q) (H'' Q)` by PROVE_TAC [ONE_TAU] 921 >> IMP_RES_TAC EPS_TRANS); 922 923(* This lemma may apply at the final stage, it doesn't require (SG H), just (SEQ H) *) 924val SEQ_EPS_lemma = Q.prove ( 925 `!E P Q R H. SG E /\ SEQ E /\ OBS_CONGR P (E P) /\ OBS_CONGR Q (E Q) /\ SEQ H /\ 926 (R = \x y. ?H. SEQ H /\ (WEAK_EQUIV x (H P)) /\ (WEAK_EQUIV y (H Q))) 927 ==> (!P'. EPS (H P) P' ==> ?Q'. EPS (H Q) Q' /\ (WEAK_EQUIV O R O WEAK_EQUIV) P' Q') /\ 928 (!Q'. EPS (H Q) Q' ==> ?P'. EPS (H P) P' /\ (WEAK_EQUIV O R O WEAK_EQUIV) P' Q')`, 929 rpt GEN_TAC >> STRIP_TAC 930 >> `OBS_CONGR (H P) ((H o E) P) /\ OBS_CONGR (H Q) ((H o E) Q)` 931 by PROVE_TAC [OBS_CONGR_SUBST_SEQ, o_DEF] 932 >> `SG (H o E) /\ SEQ (H o E)` by PROVE_TAC [SG_SEQ_combin] 933 >> rpt STRIP_TAC (* 2 sub-goals here *) 934 >| [ (* goal 1 (of 2) *) 935 IMP_RES_TAC (Q.SPECL [`H P`, `(H o E) P`] OBS_CONGR_EPS) \\ 936 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 937 NTAC 4 (POP_ASSUM K_TAC) \\ 938 POP_ASSUM (ASSUME_TAC o BETA_RULE o (Q.SPEC `Q`)) \\ 939 IMP_RES_TAC (Q.SPECL [`H Q`, `(H o E) Q`] OBS_CONGR_EPS') \\ 940 NTAC 2 (POP_ASSUM K_TAC) \\ 941 Q.EXISTS_TAC `E1` >> art [] \\ 942 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 943 `WEAK_EQUIV (H' Q) E1` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 944 Q.EXISTS_TAC `H' Q` >> art [] \\ 945 Q.EXISTS_TAC `E2` >> art [] \\ 946 Q.EXISTS_TAC `H'` >> art [WEAK_EQUIV_REFL], 947 (* goal 2 (of 2) *) 948 IMP_RES_TAC (Q.SPECL [`H Q`, `(H o E) Q`] OBS_CONGR_EPS) \\ 949 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 950 NTAC 4 (POP_ASSUM K_TAC) \\ 951 POP_ASSUM (ASSUME_TAC o BETA_RULE o (Q.SPEC `P`)) \\ 952 IMP_RES_TAC (Q.SPECL [`H P`, `(H o E) P`] OBS_CONGR_EPS') \\ 953 Q.EXISTS_TAC `E1'` >> art [] \\ 954 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 955 `WEAK_EQUIV E2 Q'` by PROVE_TAC [WEAK_EQUIV_SYM] \\ 956 PROVE_TAC [WEAK_EQUIV_REFL] ]); 957 958(* Proposition 7.13 in Milner's book [1]: 959 Let the expression E contains at most the variable X, and let X be 960 guarded and sequential in E, then: 961 962 If P = E{P/X} and Q = E{Q/X} then P = Q. (here "=" means OBS_CONGR) 963 964 This proof doesn't use "bisimulation up to" at all, instead it 965 constructed a bisimulation directly and then verify it against 966 OBS_CONGR_BY_WEAK_BISIM. 967 *) 968Theorem OBS_UNIQUE_SOLUTION : 969 !E P Q. SG E /\ SEQ E /\ OBS_CONGR P (E P) /\ OBS_CONGR Q (E Q) 970 ==> OBS_CONGR P Q 971Proof 972 rpt STRIP_TAC 973 >> irule OBS_CONGR_BY_WEAK_BISIM 974 >> Q.EXISTS_TAC `\x y. ?H. SEQ H /\ WEAK_EQUIV x (H P) /\ WEAK_EQUIV y (H Q)` 975 >> reverse CONJ_TAC (* 2 sub-goals here *) 976 >| [ (* goal 1 (of 2) *) 977 REWRITE_TAC [WEAK_BISIM] \\ 978 fix [`P'`, `Q'`] \\ 979 STRIP_TAC >> POP_ASSUM (MP_TAC o (BETA_RULE)) \\ 980 STRIP_TAC \\ 981 Q.ABBREV_TAC `R = \x y. ?H. SEQ H /\ WEAK_EQUIV x (H P) /\ WEAK_EQUIV y (H Q)` \\ 982 `OBS_CONGR (H P) ((H o E) P) /\ OBS_CONGR (H Q) ((H o E) Q)` 983 by PROVE_TAC [OBS_CONGR_SUBST_SEQ, o_DEF] \\ 984 `SG (H o E) /\ SEQ (H o E)` by PROVE_TAC [SG_SEQ_combin] \\ 985 rpt STRIP_TAC >| (* 4 sub-goals here *) 986 [ (* goal 1 (of 4) *) 987 `?E2. WEAK_TRANS (H P) (label l) E2 /\ WEAK_EQUIV E1 E2` 988 by PROVE_TAC [WEAK_EQUIV_TRANS_label] \\ 989 `?E3. WEAK_TRANS ((H o E) P) (label l) E3 /\ WEAK_EQUIV E2 E3` 990 by PROVE_TAC [OBS_CONGR_WEAK_TRANS] \\ 991 Q.PAT_X_ASSUM `WEAK_TRANS ((H o E) P) (label l) E3` 992 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 993 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 994 NTAC 4 (POP_ASSUM K_TAC) \\ 995 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 996 `TRANS (H' P) (label l) E2'` by PROVE_TAC [] \\ 997 IMP_RES_TAC (Q.SPEC `H'` OBS_UNIQUE_SOLUTION_LEMMA) \\ 998 NTAC 7 (POP_ASSUM K_TAC) \\ 999 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1000 `EPS (H'' P) E3` by PROVE_TAC [] \\ 1001 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H''`] SEQ_EPS_lemma) \\ 1002 RW_TAC std_ss [] >> POP_ASSUM K_TAC \\ 1003 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1004 `WEAK_TRANS ((H o E) Q) (label l) Q''` by PROVE_TAC [WEAK_TRANS] \\ 1005 `?Q3. WEAK_TRANS (H Q) (label l) Q3 /\ WEAK_EQUIV Q3 Q''` 1006 by PROVE_TAC [OBS_CONGR_WEAK_TRANS'] \\ 1007 `?Q4. WEAK_TRANS Q' (label l) Q4 /\ WEAK_EQUIV Q4 Q3` 1008 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label'] \\ 1009 Q.EXISTS_TAC `Q4` >> art [] \\ 1010 Q.PAT_X_ASSUM `X E3 Q''` MP_TAC \\ 1011 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1012 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 1013 Q.UNABBREV_TAC `R` >> BETA_TAC >> rpt STRIP_TAC \\ 1014 PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM], 1015(* 1016 (goal 1.4) (goal 1.1) 1017 P' ======== tau =====> P4 P' ----------------- l --------------> E1 1018 | | | | 1019 ~~ ~~ ~~ ~~ 1020 | | | | 1021 H P ======== eps =====> P3 H P ================= l ==============> E2 1022 | | | | 1023 ~~ ~~ ~~c ~~ 1024 | | | | 1025 H(E(P)) ==== eps =====> H' P H(E(P)) ==eps=> E1' --l-> E2' ==eps=> E3 ~~ y' ~~ H''' P 1026 | (H' P) (H'' P) | 1027 R R 1028 | | 1029 H(E(Q)) ==== eps =====> E3 = H' Q H(E(Q)) ==eps=> H' Q --l-> H'' Q ==eps=> Q'' ~~ y ~~ H''' Q 1030 | | | | 1031 ~~ ~~ ~~c ~~ 1032 | | | | 1033 H Q ======== eps =====> E1 H Q ================== l ==============> Q3 1034 | | | | 1035 ~~ ~~ ~~ ~~ 1036 | | | | 1037 Q' -------- eps -----> E2 Q' ================== l ==============> Q4 1038 *) 1039 (* goal 2 (of 4) *) 1040 `?E1. WEAK_TRANS (H Q) (label l) E1 /\ WEAK_EQUIV E2 E1` 1041 by PROVE_TAC [WEAK_EQUIV_TRANS_label] \\ 1042 `?E3. WEAK_TRANS ((H o E) Q) (label l) E3 /\ WEAK_EQUIV E1 E3` 1043 by PROVE_TAC [OBS_CONGR_WEAK_TRANS] \\ 1044 Q.PAT_X_ASSUM `WEAK_TRANS ((H o E) Q) (label l) E3` 1045 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 1046 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 1047 NTAC 4 (POP_ASSUM K_TAC) \\ 1048 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 1049 `TRANS (H' Q) (label l) E2'` by PROVE_TAC [] \\ 1050 IMP_RES_TAC (Q.SPEC `H'` OBS_UNIQUE_SOLUTION_LEMMA) \\ 1051 NTAC 7 (POP_ASSUM K_TAC) \\ 1052 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 1053 `EPS (H'' Q) E3` by PROVE_TAC [] \\ 1054 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H''`] SEQ_EPS_lemma) \\ 1055 RW_TAC std_ss [] \\ 1056 Q.PAT_X_ASSUM `!P'. EPS (H'' P) P' ==> X` K_TAC \\ 1057 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1058 `WEAK_TRANS ((H o E) P) (label l) P''` by PROVE_TAC [WEAK_TRANS] \\ 1059 `?P3. WEAK_TRANS (H P) (label l) P3 /\ WEAK_EQUIV P3 P''` 1060 by PROVE_TAC [OBS_CONGR_WEAK_TRANS'] \\ 1061 `?P4. WEAK_TRANS P' (label l) P4 /\ WEAK_EQUIV P4 P3` 1062 by PROVE_TAC [WEAK_EQUIV_WEAK_TRANS_label'] \\ 1063 Q.EXISTS_TAC `P4` >> art [] \\ 1064 Q.PAT_X_ASSUM `X P'' E3` MP_TAC \\ 1065 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1066 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 1067 Q.UNABBREV_TAC `R` >> BETA_TAC >> 1068 PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM], 1069(* 1070 (goal 1.3) (goal 1.2) 1071 P' -------- tau -----> E1 P' ================= l ==============> P4 1072 | | | | 1073 ~~ ~~ ~~ ~~ 1074 | | | | 1075 H P ======== eps =====> E2 H P ================= l ==============> P3 1076 | | | | 1077 ~~c ~~ ~~c ~~ 1078 | | | | 1079 H(E(P)) ==== eps =====> E3 = H' P H(E(P)) ==eps=> H' P --l-> H'' P ==eps=> P'' ~~ y' ~~ H''' P 1080 | | 1081 R R 1082 | (H' Q) (H'' Q) | 1083 H(E(Q)) ==== eps =====> H' Q H(E(Q)) ==eps=> E1' --l-> E2' ==eps=> E3 ~~ y ~~ H''' Q 1084 | | | | 1085 ~~c ~~ ~~c ~~ 1086 | | | | 1087 H Q ======== eps =====> Q3 H Q ================= l ==============> E1 1088 | | | | 1089 ~~c ~~ ~~ ~~ 1090 | | | | 1091 Q' ======== eps =====> Q4 Q' ----------------- l --------------> E2 1092 *) 1093 (* goal 3 (of 4) *) 1094 `?E2. EPS (H P) E2 /\ WEAK_EQUIV E1 E2` by PROVE_TAC [WEAK_EQUIV_TRANS_tau] \\ 1095 `?E3. EPS ((H o E) P) E3 /\ WEAK_EQUIV E2 E3` by PROVE_TAC [OBS_CONGR_EPS] \\ 1096 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 1097 NTAC 4 (POP_ASSUM K_TAC) \\ 1098 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1099 `?Q3. EPS (H Q) Q3 /\ WEAK_EQUIV Q3 (H' Q)` by PROVE_TAC [OBS_CONGR_EPS'] \\ 1100 `?Q4. EPS Q' Q4 /\ WEAK_EQUIV Q4 Q3` by PROVE_TAC [WEAK_EQUIV_EPS'] \\ 1101 Q.EXISTS_TAC `Q4` >> art [] \\ 1102 Q.UNABBREV_TAC `R` >> BETA_TAC \\ 1103 PROVE_TAC [WEAK_EQUIV_TRANS], 1104 (* goal 4 (of 4) *) 1105 `?E1. EPS (H Q) E1 /\ WEAK_EQUIV E2 E1` by PROVE_TAC [WEAK_EQUIV_TRANS_tau] \\ 1106 `?E3. EPS ((H o E) Q) E3 /\ WEAK_EQUIV E1 E3` by PROVE_TAC [OBS_CONGR_EPS] \\ 1107 IMP_RES_TAC (Q.SPEC `H o E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 1108 NTAC 4 (POP_ASSUM K_TAC) \\ 1109 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 1110 `?P3. EPS (H P) P3 /\ WEAK_EQUIV P3 (H' P)` by PROVE_TAC [OBS_CONGR_EPS'] \\ 1111 `?P4. EPS P' P4 /\ WEAK_EQUIV P4 P3` by PROVE_TAC [WEAK_EQUIV_EPS'] \\ 1112 Q.EXISTS_TAC `P4` >> art [] \\ 1113 Q.UNABBREV_TAC `R` >> BETA_TAC \\ 1114 PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM] ], 1115 (* goal 2 (of 2) *) 1116 Q.ABBREV_TAC `R = \x y. ?H. SEQ H /\ WEAK_EQUIV x (H P) /\ WEAK_EQUIV y (H Q)` \\ 1117 rpt STRIP_TAC >| (* 2 sub-goals here *) 1118 [ (* goal 2.1 (of 2) *) 1119 `?E2. WEAK_TRANS (E P) u E2 /\ WEAK_EQUIV E1 E2` 1120 by PROVE_TAC [OBS_CONGR_TRANS_LEFT] \\ 1121 Q.PAT_X_ASSUM `WEAK_TRANS (E P) u E2` 1122 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 1123 IMP_RES_TAC (Q.SPEC `E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 1124 NTAC 4 (POP_ASSUM K_TAC) \\ 1125 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1126 `TRANS (H P) u E2'` by PROVE_TAC [] \\ 1127 IMP_RES_TAC (Q.SPEC `H` OBS_UNIQUE_SOLUTION_LEMMA) \\ 1128 NTAC 5 (POP_ASSUM K_TAC) \\ 1129 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1130 `EPS (H' P) E2` by PROVE_TAC [] \\ 1131 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H'`] SEQ_EPS_lemma) \\ 1132 RW_TAC std_ss [] >> POP_ASSUM K_TAC \\ 1133 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1134 `WEAK_TRANS (E Q) u Q'` by PROVE_TAC [WEAK_TRANS] \\ 1135 `?Q''. WEAK_TRANS Q u Q'' /\ WEAK_EQUIV Q'' Q'` 1136 by PROVE_TAC [OBS_CONGR_WEAK_TRANS'] \\ 1137 Q.EXISTS_TAC `Q''` >> art [] \\ 1138 Q.PAT_X_ASSUM `X E2 Q'` MP_TAC \\ 1139 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1140 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 1141 Q.UNABBREV_TAC `R` >> BETA_TAC >> rpt STRIP_TAC \\ 1142 PROVE_TAC [WEAK_EQUIV_TRANS, WEAK_EQUIV_SYM], 1143(* 1144 (goal 2.1) 1145 P ------------------- u --------------> E1 1146 | | 1147 ~~c ~~ 1148 | | 1149 E(P) ====eps==> E1' ---u-> E2' ==eps==> E2 ~~ y' ~~ H'' P 1150 (H P) (H' P) | 1151 R 1152 | 1153 E(Q) ====eps==> H Q ---u-> H' Q ==eps==> Q' ~~ y ~~ H'' Q 1154 | | 1155 ~~c ~~ 1156 | | 1157 Q =================== u ==============> Q'' 1158 *) 1159 (* goal 2.2 (of 2) *) 1160 `?E1. WEAK_TRANS (E Q) u E1 /\ WEAK_EQUIV E2 E1` 1161 by PROVE_TAC [OBS_CONGR_TRANS_LEFT] \\ 1162 Q.PAT_X_ASSUM `WEAK_TRANS (E Q) u E1` 1163 (STRIP_ASSUME_TAC o (REWRITE_RULE [WEAK_TRANS])) \\ 1164 IMP_RES_TAC (Q.SPEC `E` OBS_UNIQUE_SOLUTION_LEMMA_EPS) \\ 1165 NTAC 4 (POP_ASSUM K_TAC) \\ 1166 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 1167 `TRANS (H Q) u E2'` by PROVE_TAC [] \\ 1168 IMP_RES_TAC (Q.SPEC `H` OBS_UNIQUE_SOLUTION_LEMMA) \\ 1169 NTAC 5 (POP_ASSUM K_TAC) \\ 1170 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 1171 `EPS (H' Q) E1` by PROVE_TAC [] \\ 1172 MP_TAC (Q.SPECL [`E`, `P`, `Q`, `R`, `H'`] SEQ_EPS_lemma) \\ 1173 RW_TAC std_ss [] \\ 1174 Q.PAT_X_ASSUM `!P'. EPS (H' P) P' ==> X` K_TAC \\ 1175 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1176 `WEAK_TRANS (E P) u P'` by PROVE_TAC [WEAK_TRANS] \\ 1177 `?P''. WEAK_TRANS P u P'' /\ WEAK_EQUIV P'' P'` 1178 by PROVE_TAC [OBS_CONGR_WEAK_TRANS'] \\ 1179 Q.EXISTS_TAC `P''` >> art [] \\ 1180 Q.PAT_X_ASSUM `X P' E1` MP_TAC \\ 1181 REWRITE_TAC [O_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1182 Q.PAT_X_ASSUM `R y' y` MP_TAC \\ 1183 Q.UNABBREV_TAC `R` >> BETA_TAC >> rpt STRIP_TAC \\ 1184 PROVE_TAC [WEAK_EQUIV_SYM, WEAK_EQUIV_TRANS] ] ] 1185(* 1186 (goal 2.2) 1187 P ------------------- u --------------> P'' 1188 | | 1189 ~~c ~~ 1190 | | 1191 E(P) ====eps==> H P ---u-> H' P ==eps==> P' ~~ y' ~~ H'' P 1192 | 1193 R 1194 (H Q) (H' Q) | 1195 E(Q) ====eps==> E1' ---u-> E2' ===eps==> E1 ~~ y ~~ H'' Q 1196 | | 1197 ~~c ~~ 1198 | | 1199 Q ------------------- u --------------> E2 1200 *) 1201QED 1202 1203(******************************************************************************) 1204(* *) 1205(* 4. Unique solutions of contractions *) 1206(* *) 1207(******************************************************************************) 1208 1209(* NOTE: the lemma works for any precongruence relation *) 1210val unfolding_lemma1 = store_thm ( 1211 "unfolding_lemma1", 1212 ``!E C P. GCONTEXT E /\ GCONTEXT C /\ P contracts (E P) ==> 1213 !n. (C P) contracts (C o (FUNPOW E n)) P``, 1214 rpt STRIP_TAC 1215 >> REWRITE_TAC [o_DEF] 1216 >> BETA_TAC 1217 >> irule contracts_SUBST_GCONTEXT >> art [] 1218 >> Q.SPEC_TAC (`n`, `n`) 1219 >> Induct >- REWRITE_TAC [FUNPOW, contracts_REFL] 1220 >> REWRITE_TAC [FUNPOW_SUC] 1221 >> Q.ABBREV_TAC `Q = FUNPOW E n P` 1222 >> PROVE_TAC [contracts_SUBST_GCONTEXT, contracts_TRANS]); 1223 1224(* These can be merged to HOL's arithmeticTheory (not used here any more). 1225 The word "LEFT" or "RIGHT" indicate the position of `FUNPOW` w.r.t `o`. 1226 *) 1227Theorem FUNPOW_SUC_RIGHT : 1228 !f n. FUNPOW f (SUC n) = f o (FUNPOW f n) 1229Proof 1230 RW_TAC std_ss [o_DEF, FUNPOW_SUC, FUN_EQ_THM] 1231QED 1232 1233Theorem FUNPOW_SUC_LEFT : 1234 !f n. FUNPOW f (SUC n) = (FUNPOW f n) o f 1235Proof 1236 rpt GEN_TAC 1237 >> REWRITE_TAC [FUN_EQ_THM, o_DEF] >> BETA_TAC 1238 >> GEN_TAC 1239 >> `FUNPOW f (n + 1) x = FUNPOW f n (FUNPOW f 1 x)` by PROVE_TAC [FUNPOW_ADD] 1240 >> FULL_SIMP_TAC arith_ss [FUNPOW_1, ADD1] 1241QED 1242 1243(* A single transition from WGS E[P] will not touch the variable P *) 1244val unfolding_lemma2 = store_thm ( 1245 "unfolding_lemma2", 1246 ``!E. WGS E ==> !P u P'. TRANS (E P) u P' ==> 1247 ?C'. GCONTEXT C' /\ (P' = C' P) /\ !Q. TRANS (E Q) u (C' Q)``, 1248 HO_MATCH_MP_TAC WGS_strongind 1249 >> BETA_TAC >> REWRITE_TAC [ETA_AX] 1250 >> rpt STRIP_TAC (* 6 sub-goals here *) 1251 >| [ (* goal 1 (of 6) *) 1252 Q.EXISTS_TAC `\t. P'` >> art [GCONTEXT2], 1253 (* goal 2 (of 6) *) 1254 IMP_RES_TAC TRANS_PREFIX \\ 1255 Q.EXISTS_TAC `e` >> art [] \\ 1256 GEN_TAC >> REWRITE_TAC [PREFIX], 1257 (* goal 3 (of 6) *) 1258 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 1259 [ (* goal 3.1 (of 2) *) 1260 IMP_RES_TAC TRANS_PREFIX \\ 1261 Q.EXISTS_TAC `e1` >> art [] \\ 1262 GEN_TAC >> MATCH_MP_TAC SUM1 >> REWRITE_TAC [PREFIX], 1263 (* goal 3.2 (of 2) *) 1264 IMP_RES_TAC TRANS_PREFIX \\ 1265 Q.EXISTS_TAC `e2` >> art [] \\ 1266 GEN_TAC >> MATCH_MP_TAC SUM2 >> REWRITE_TAC [PREFIX] ], 1267 (* goal 4 (of 6) *) 1268 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1269 [ (* goal 4.1 (of 3) *) 1270 RES_TAC \\ 1271 Q.EXISTS_TAC `\t. par (C' t) (E' t)` >> BETA_TAC \\ 1272 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT5 >> art [] \\ 1273 MATCH_MP_TAC WGS_IMP_GCONTEXT >> art [] ) \\ 1274 FULL_SIMP_TAC std_ss [] \\ 1275 GEN_TAC >> MATCH_MP_TAC PAR1 >> art [], 1276 (* goal 4.2 (of 3) *) 1277 RES_TAC \\ 1278 Q.EXISTS_TAC `\t. par (E t) (C' t)` >> BETA_TAC \\ 1279 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT5 >> art [] \\ 1280 MATCH_MP_TAC WGS_IMP_GCONTEXT >> art [] ) \\ 1281 FULL_SIMP_TAC std_ss [] \\ 1282 GEN_TAC >> MATCH_MP_TAC PAR2 >> art [], 1283 (* goal 4.3 (of 3) *) 1284 RES_TAC \\ 1285 Q.EXISTS_TAC `\t. par (C'' t) (C' t)` >> BETA_TAC \\ 1286 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT5 >> art [] ) \\ 1287 FULL_SIMP_TAC std_ss [] \\ 1288 GEN_TAC >> MATCH_MP_TAC PAR3 \\ 1289 Q.EXISTS_TAC `l` >> art [] ], 1290 (* goal 5 (of 6) *) 1291 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1292 [ (* goal 5.1 (of 2) *) 1293 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1294 Q.EXISTS_TAC `\t. restr L (C' t)` >> BETA_TAC \\ 1295 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT6 >> art [] ) \\ 1296 art [] \\ 1297 GEN_TAC >> MATCH_MP_TAC RESTR >> art [], 1298 (* goal 5.2 (of 2) *) 1299 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1300 Q.EXISTS_TAC `\t. restr L (C' t)` >> BETA_TAC \\ 1301 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT6 >> art [] ) \\ 1302 art [] \\ 1303 GEN_TAC >> MATCH_MP_TAC RESTR >> art [] \\ 1304 Q.EXISTS_TAC `l` >> art [] ], 1305 (* goal 6 (of 6) *) 1306 IMP_RES_TAC TRANS_RELAB >> RES_TAC \\ 1307 Q.EXISTS_TAC `\t. relab (C' t) rf` >> BETA_TAC \\ 1308 CONJ_TAC >- ( MATCH_MP_TAC GCONTEXT7 >> art [] ) \\ 1309 art [] \\ 1310 GEN_TAC >> MATCH_MP_TAC RELABELING >> art [] ]); 1311 1312(* In this proof, we combine C and E into a single WGS and call previous lemma *) 1313val unfolding_lemma3 = store_thm ( 1314 "unfolding_lemma3", 1315 ``!C E. GCONTEXT C /\ WGS E ==> 1316 !P x P'. TRANS (C (E P)) x P' ==> 1317 ?C'. GCONTEXT C' /\ (P' = C' P) /\ !Q. TRANS (C (E Q)) x (C' Q)``, 1318 rpt STRIP_TAC 1319 >> IMP_RES_TAC GCONTEXT_WGS_combin 1320 >> Know `C (E P) = (C o E) P` >- SIMP_TAC std_ss [o_DEF] 1321 >> DISCH_TAC 1322 >> Q.PAT_X_ASSUM `TRANS (C (E P)) x P'` MP_TAC 1323 >> art [] >> DISCH_TAC 1324 >> IMP_RES_TAC unfolding_lemma2 1325 >> POP_ASSUM K_TAC 1326 >> Q.EXISTS_TAC `C'` >> art [] 1327 >> GEN_TAC >> POP_ASSUM MP_TAC 1328 >> KILL_TAC 1329 >> REWRITE_TAC [o_DEF] >> BETA_TAC 1330 >> RW_TAC std_ss []); 1331 1332(* NOTE: the lemma works for not only WGS but any weakly guarded expressions *) 1333val unfolding_lemma4 = store_thm ( 1334 "unfolding_lemma4", 1335 ``!C E n xs P' P. GCONTEXT C /\ WGS E /\ 1336 TRACE ((C o FUNPOW E n) P) xs P' /\ (LENGTH xs <= n) ==> 1337 ?C'. GCONTEXT C' /\ (P' = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs (C' Q)``, 1338 NTAC 2 GEN_TAC 1339 >> Induct_on `n` 1340 >- (RW_TAC std_ss [o_DEF, FUNPOW_0] \\ 1341 Q.EXISTS_TAC `C` >> fs [TRACE_NIL]) 1342 >> rpt STRIP_TAC 1343 >> Q.PAT_X_ASSUM `TRACE X xs P'` MP_TAC 1344 >> Know `!P. (C o (FUNPOW E (SUC n))) P = (C o (FUNPOW E n)) (E P)` 1345 >- RW_TAC std_ss [o_DEF, FUNPOW] >> Rewr 1346 >> DISCH_TAC 1347 >> IMP_RES_TAC TRACE_cases2 1348 >> Cases_on `xs` 1349 >- (REV_FULL_SIMP_TAC std_ss [NULL] \\ 1350 `LENGTH (epsilon :'b Action list) <= n` by FULL_SIMP_TAC arith_ss [LENGTH] \\ 1351 Q.PAT_X_ASSUM `!xs P' P. X ==> X'` 1352 (MP_TAC o (Q.SPECL [`[] :'b Action list`, `P'`, `(E :('a, 'b) context) P`])) \\ 1353 RW_TAC std_ss [] \\ 1354 Q.EXISTS_TAC `C' o E` >> art [] \\ 1355 CONJ_TAC >- (IMP_RES_TAC WGS_IMP_GCONTEXT \\ 1356 MATCH_MP_TAC GCONTEXT_combin >> art []) \\ 1357 CONJ_TAC >- (KILL_TAC >> REWRITE_TAC [o_DEF] >> RW_TAC std_ss []) \\ 1358 GEN_TAC >> ASM_SIMP_TAC std_ss [o_DEF]) 1359 >> FULL_SIMP_TAC list_ss [] 1360 >> `LENGTH (FRONT (h::t)) <= n` by PROVE_TAC [LENGTH_FRONT_CONS] 1361 >> Q.ABBREV_TAC `xs = FRONT (h::t)` 1362 >> Q.ABBREV_TAC `x = LAST (h::t)` 1363 >> Q.PAT_X_ASSUM `!xs P'' P'''. X ==> X'` 1364 (MP_TAC o (Q.SPECL [`xs`, `u`, `(E :('a, 'b) context) P`])) 1365 >> RW_TAC std_ss [] 1366 >> MP_TAC (Q.SPECL [`C'`, `E`] unfolding_lemma3) 1367 >> RW_TAC bool_ss [] 1368 >> POP_ASSUM (MP_TAC o (Q.SPECL [`P`, `x`, `P'`])) 1369 >> RW_TAC bool_ss [] 1370 >> Q.EXISTS_TAC `C''` >> art [] 1371 >> GEN_TAC 1372 >> ONCE_REWRITE_TAC [TRACE_cases2] 1373 >> REWRITE_TAC [NULL] 1374 >> Q.EXISTS_TAC `C' (E Q)` 1375 >> Q.UNABBREV_TAC `x` >> art [] 1376 >> Q.UNABBREV_TAC `xs` >> art []); 1377 1378(* Lemma 3.9 of [2] *) 1379val UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA = store_thm ( 1380 "UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA", 1381 ``!(P :('a, 'b) CCS) (Q :('a, 'b) CCS). 1382 (?E. WGS E /\ P contracts (E P) /\ Q contracts (E Q)) ==> 1383 !(C :('a, 'b) context). GCONTEXT C ==> 1384 (!l R. WEAK_TRANS (C P) (label l) R ==> 1385 ?C'. GCONTEXT C' /\ R contracts (C' P) /\ 1386 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C Q) (C' Q)) /\ 1387 (!R. WEAK_TRANS (C P) tau R ==> 1388 ?C'. GCONTEXT C' /\ R contracts (C' P) /\ 1389 (WEAK_EQUIV O EPS) (C Q) (C' Q))``, 1390 NTAC 5 STRIP_TAC 1391 (* Part 1: construct C'' which is a GCONTEXT *) 1392 >> IMP_RES_TAC WGS_IMP_GCONTEXT 1393 >> Q.ABBREV_TAC `C'' = \n. C o (FUNPOW E n)` 1394 >> Know `!n. GCONTEXT (C'' n)` 1395 >- (Q.UNABBREV_TAC `C''` >> BETA_TAC \\ 1396 Induct_on `n` >- art [o_DEF, FUNPOW, ETA_THM] \\ 1397 REWRITE_TAC [FUNPOW_SUC_LEFT, o_ASSOC] \\ 1398 MATCH_MP_TAC GCONTEXT_combin >> art []) >> DISCH_TAC 1399 (* Part 2: property of C'' on P and Q *) 1400 >> `!n. (C P) contracts (C'' n P)` 1401 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [unfolding_lemma1]) 1402 >> `!n. (C Q) contracts (C'' n Q)` 1403 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [unfolding_lemma1]) 1404 (* Part 3 *) 1405 >> rpt STRIP_TAC (* 2 sub-goals here *) 1406 >| [ (* goal 1 (of 2) *) 1407 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 1408 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 1409 `(C P) contracts (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 1410 POP_ASSUM (IMP_RES_TAC o (MATCH_MP contracts_AND_TRACE_label)) \\ 1411 NTAC 4 (POP_ASSUM K_TAC) \\ 1412 Q.ABBREV_TAC `n = LENGTH us` \\ 1413 Q.UNABBREV_TAC `C''` \\ 1414 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 1415 Know `?C'. GCONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 1416 >- ( MATCH_MP_TAC unfolding_lemma4 >> art [] ) \\ 1417 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1418 `(C Q) contracts ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 1419 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 1420 Q.EXISTS_TAC `C'` >> art [] \\ 1421 Know `WEAK_TRANS (C (FUNPOW E n Q)) (label l) (C' Q)` 1422 >- ( REWRITE_TAC [WEAK_TRANS_AND_TRACE, Action_distinct_label] \\ 1423 Q.EXISTS_TAC `xs'` >> art [] \\ 1424 MATCH_MP_TAC UNIQUE_LABEL_NOT_NULL \\ 1425 Q.EXISTS_TAC `label l` >> art [] ) >> DISCH_TAC \\ 1426 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 1427 IMP_RES_TAC contracts_WEAK_TRANS_label' \\ 1428 Q.EXISTS_TAC `E1` >> art [], 1429 (* goal 2 (of 2) *) 1430 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 1431 FULL_SIMP_TAC std_ss [] \\ 1432 `(C P) contracts (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 1433 POP_ASSUM (IMP_RES_TAC o (MATCH_MP contracts_AND_TRACE_tau)) \\ (* diff here *) 1434 NTAC 4 (POP_ASSUM K_TAC) \\ 1435 Q.ABBREV_TAC `n = LENGTH us` \\ 1436 Q.UNABBREV_TAC `C''` \\ 1437 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 1438 Know `?C'. GCONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 1439 >- ( MATCH_MP_TAC unfolding_lemma4 >> art [] ) \\ 1440 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1441 `(C Q) contracts ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 1442 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 1443 Q.EXISTS_TAC `C'` >> art [] \\ 1444 Know `EPS (C (FUNPOW E n Q)) (C' Q)` (* diff here *) 1445 >- ( REWRITE_TAC [EPS_AND_TRACE] \\ 1446 Q.EXISTS_TAC `xs'` >> art [] ) >> DISCH_TAC \\ 1447 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 1448 IMP_RES_TAC contracts_EPS' \\ 1449 Q.EXISTS_TAC `E1` >> art [] ]); 1450 1451(* Theorem 3.10 of [2], the proof relies on above lemma, and "contracts_IMP_WEAK_EQUIV", 1452 the definition of contraction is not used. 1453 *) 1454Theorem UNIQUE_SOLUTION_OF_CONTRACTIONS : 1455 !E P Q. WGS E /\ P contracts (E P) /\ Q contracts (E Q) ==> WEAK_EQUIV P Q 1456Proof 1457 rpt STRIP_TAC 1458 >> REWRITE_TAC [WEAK_EQUIV] 1459 >> Q.EXISTS_TAC `\R S. ?C. GCONTEXT C /\ WEAK_EQUIV R (C P) /\ WEAK_EQUIV S (C Q)` 1460 >> BETA_TAC >> CONJ_TAC 1461 >- (Q.EXISTS_TAC `E` \\ 1462 CONJ_TAC >- IMP_RES_TAC WGS_IMP_GCONTEXT \\ 1463 IMP_RES_TAC contracts_IMP_WEAK_EQUIV >> art []) 1464 >> REWRITE_TAC [WEAK_BISIM] 1465 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 1466 >| [ (* goal 1 (of 4) *) 1467 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1468 (ASSUME_TAC o (Q.SPECL [`l`, `E1`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 1469 RES_TAC \\ 1470 Q.PAT_X_ASSUM `TRANS E' (label l) E1 ==> X` K_TAC \\ 1471 ASSUME_TAC (Q.SPECL [`P`, `Q`] UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA) \\ 1472 `!l R. WEAK_TRANS (C P) (label l) R ==> 1473 ?C'. GCONTEXT C' /\ R contracts (C' P) /\ 1474 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C Q) (C' Q)` 1475 by METIS_TAC [] \\ 1476 Q.PAT_X_ASSUM `(?E. WGS E /\ P contracts (E P) /\ Q contracts (E Q)) ==> X` K_TAC \\ 1477 RES_TAC \\ 1478 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1479 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1480 (ASSUME_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 1481 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C P) (label l) R ==> X` K_TAC \\ 1482 RES_TAC \\ 1483 Q.PAT_X_ASSUM `WEAK_TRANS (C Q) (label l) y ==> X` K_TAC \\ 1484 Q.EXISTS_TAC `E1'` >> art [] \\ 1485 Q.EXISTS_TAC `C'` >> art [] \\ 1486 `WEAK_EQUIV E1' (C' Q)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1487 `WEAK_EQUIV E2 (C' P)` by PROVE_TAC [contracts_IMP_WEAK_EQUIV] \\ 1488 PROVE_TAC [WEAK_EQUIV_TRANS], 1489 (* goal 2 (of 4) *) 1490 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1491 (ASSUME_TAC o (Q.SPECL [`l`, `E2`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 1492 RES_TAC \\ 1493 Q.PAT_X_ASSUM `TRANS E'' (label l) E2 ==> X` K_TAC \\ 1494 ASSUME_TAC (Q.SPECL [`Q`, `P`] UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA) \\ 1495 `!l R. WEAK_TRANS (C Q) (label l) R ==> 1496 ?C'. GCONTEXT C' /\ R contracts (C' Q) /\ 1497 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C P) (C' P)` 1498 by METIS_TAC [] \\ 1499 Q.PAT_X_ASSUM `(?E. WGS E /\ Q contracts (E Q) /\ P contracts (E P)) ==> X` K_TAC \\ 1500 RES_TAC \\ 1501 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1502 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1503 (ASSUME_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 1504 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C Q) (label l) R ==> X` K_TAC \\ 1505 RES_TAC \\ 1506 Q.PAT_X_ASSUM `WEAK_TRANS (C P) (label l) y ==> X` K_TAC \\ 1507 Q.EXISTS_TAC `E1` >> art [] \\ 1508 Q.EXISTS_TAC `C'` >> art [] \\ 1509 `WEAK_EQUIV E1 (C' P)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1510 `WEAK_EQUIV E2' (C' Q)` by PROVE_TAC [contracts_IMP_WEAK_EQUIV] \\ 1511 PROVE_TAC [WEAK_EQUIV_TRANS], 1512 (* goal 3 (of 4) *) 1513 IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau 1514 (ASSUME ``WEAK_EQUIV E' ((C :('a, 'b) context) P)``)) \\ 1515 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 1516 >- ( Q.EXISTS_TAC `E''` >> REWRITE_TAC [EPS_REFL] \\ 1517 Q.EXISTS_TAC `C` >> art [] ) \\ 1518 ASSUME_TAC (Q.SPECL [`P`, `Q`] UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA) \\ 1519 `!R. WEAK_TRANS (C P) tau R ==> 1520 ?C'. GCONTEXT C' /\ R contracts (C' P) /\ 1521 (WEAK_EQUIV O EPS) (C Q) (C' Q)` by METIS_TAC [] \\ 1522 Q.PAT_X_ASSUM `(?E. WGS E /\ P contracts (E P) /\ Q contracts (E Q)) ==> X` K_TAC \\ 1523 RES_TAC \\ 1524 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1525 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1526 (ASSUME_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 1527 Q.PAT_X_ASSUM `!R. WEAK_TRANS (C P) tau R ==> X` K_TAC \\ 1528 RES_TAC \\ 1529 Q.PAT_X_ASSUM `EPS (C Q) y ==> X` K_TAC \\ 1530 Q.EXISTS_TAC `E1'` >> art [] \\ 1531 Q.EXISTS_TAC `C'` >> art [] \\ 1532 `WEAK_EQUIV E1' (C' Q)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1533 `WEAK_EQUIV E2 (C' P)` by PROVE_TAC [contracts_IMP_WEAK_EQUIV] \\ 1534 PROVE_TAC [WEAK_EQUIV_TRANS], 1535 (* goal 4 (of 4) *) 1536 IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau 1537 (ASSUME ``WEAK_EQUIV E'' ((C :('a, 'b) context) Q)``)) \\ 1538 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 1539 >- ( Q.EXISTS_TAC `E'` >> REWRITE_TAC [EPS_REFL] \\ 1540 Q.EXISTS_TAC `C` >> art [] ) \\ 1541 ASSUME_TAC (Q.SPECL [`Q`, `P`] UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA) \\ 1542 `!R. WEAK_TRANS (C Q) tau R ==> 1543 ?C'. GCONTEXT C' /\ R contracts (C' Q) /\ 1544 (WEAK_EQUIV O EPS) (C P) (C' P)` by METIS_TAC [] \\ 1545 Q.PAT_X_ASSUM `(?E. WGS E /\ Q contracts (E Q) /\ P contracts (E P)) ==> X` K_TAC \\ 1546 RES_TAC \\ 1547 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1548 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1549 (ASSUME_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 1550 Q.PAT_X_ASSUM `!R. WEAK_TRANS (C Q) tau R ==> X` K_TAC \\ 1551 RES_TAC \\ 1552 Q.PAT_X_ASSUM `EPS (C P) y ==> X` K_TAC \\ 1553 Q.EXISTS_TAC `E1` >> art [] \\ 1554 Q.EXISTS_TAC `C'` >> art [] \\ 1555 `WEAK_EQUIV E1 (C' P)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1556 `WEAK_EQUIV E2' (C' Q)` by PROVE_TAC [contracts_IMP_WEAK_EQUIV] \\ 1557 PROVE_TAC [WEAK_EQUIV_TRANS] ] 1558QED 1559 1560(******************************************************************************) 1561(* *) 1562(* 5. Unique solutions of expansions *) 1563(* *) 1564(******************************************************************************) 1565 1566(* NOTE: the lemma works for any precongruence relation *) 1567val unfolding_lemma1' = store_thm ( 1568 "unfolding_lemma1'", 1569 ``!E C P. GCONTEXT E /\ GCONTEXT C /\ P expands (E P) ==> 1570 !n. (C P) expands (C o (FUNPOW E n)) P``, 1571 rpt STRIP_TAC 1572 >> REWRITE_TAC [o_DEF] 1573 >> BETA_TAC 1574 >> irule expands_SUBST_GCONTEXT >> art [] 1575 >> Q.SPEC_TAC (`n`, `n`) 1576 >> Induct >- REWRITE_TAC [FUNPOW, expands_REFL] 1577 >> REWRITE_TAC [FUNPOW_SUC] 1578 >> Q.ABBREV_TAC `Q = FUNPOW E n P` 1579 >> `(E P) expands (E Q)` by PROVE_TAC [expands_SUBST_GCONTEXT] 1580 >> IMP_RES_TAC expands_TRANS); 1581 1582(* The proof has only minor differences with UNIQUE_SOLUTION_OF_CONTRACTIONS_LEMMA *) 1583val UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA = store_thm ( 1584 "UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA", 1585 ``!(P :('a, 'b) CCS) (Q :('a, 'b) CCS). 1586 (?E. WGS E /\ P expands (E P) /\ Q expands (E Q)) ==> 1587 !(C :('a, 'b) context). GCONTEXT C ==> 1588 (!l R. WEAK_TRANS (C P) (label l) R ==> 1589 ?C'. GCONTEXT C' /\ R expands (C' P) /\ 1590 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C Q) (C' Q)) /\ 1591 (!R. WEAK_TRANS (C P) tau R ==> 1592 ?C'. GCONTEXT C' /\ R expands (C' P) /\ 1593 (WEAK_EQUIV O EPS) (C Q) (C' Q))``, 1594 NTAC 5 STRIP_TAC 1595 (* Part 1: construct C'' which is a GCONTEXT *) 1596 >> IMP_RES_TAC WGS_IMP_GCONTEXT 1597 >> Q.ABBREV_TAC `C'' = \n. C o (FUNPOW E n)` 1598 >> Know `!n. GCONTEXT (C'' n)` 1599 >- (Q.UNABBREV_TAC `C''` >> BETA_TAC \\ 1600 Induct_on `n` >- art [o_DEF, FUNPOW, ETA_THM] \\ 1601 REWRITE_TAC [FUNPOW_SUC_LEFT, o_ASSOC] \\ 1602 MATCH_MP_TAC GCONTEXT_combin >> art []) >> DISCH_TAC 1603 (* Part 2: property of C'' on P and Q *) 1604 >> `!n. (C P) expands (C'' n P)` 1605 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [unfolding_lemma1']) 1606 >> `!n. (C Q) expands (C'' n Q)` 1607 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [unfolding_lemma1']) 1608 (* Part 3 *) 1609 >> rpt STRIP_TAC (* 2 sub-goals here *) 1610 >| [ (* goal 1 (of 2) *) 1611 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 1612 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 1613 `(C P) expands (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 1614 POP_ASSUM (IMP_RES_TAC o (MATCH_MP expands_AND_TRACE_label)) \\ 1615 NTAC 4 (POP_ASSUM K_TAC) \\ 1616 Q.ABBREV_TAC `n = LENGTH us` \\ 1617 Q.UNABBREV_TAC `C''` \\ 1618 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 1619 Know `?C'. GCONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 1620 >- ( MATCH_MP_TAC unfolding_lemma4 >> art [] ) \\ 1621 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1622 `(C Q) expands ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 1623 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 1624 Q.EXISTS_TAC `C'` >> art [] \\ 1625 Know `WEAK_TRANS (C (FUNPOW E n Q)) (label l) (C' Q)` 1626 >- ( REWRITE_TAC [WEAK_TRANS_AND_TRACE, Action_distinct_label] \\ 1627 Q.EXISTS_TAC `xs'` >> art [] \\ 1628 MATCH_MP_TAC UNIQUE_LABEL_NOT_NULL \\ 1629 Q.EXISTS_TAC `label l` >> art [] ) >> DISCH_TAC \\ 1630 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 1631 IMP_RES_TAC expands_WEAK_TRANS' \\ 1632 Q.EXISTS_TAC `E1` >> art [] \\ 1633 MATCH_MP_TAC expands_IMP_WEAK_EQUIV >> art [], (* extra steps *) 1634 (* goal 2 (of 2) *) 1635 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 1636 FULL_SIMP_TAC std_ss [] \\ 1637 `(C P) expands (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 1638 POP_ASSUM (IMP_RES_TAC o (MATCH_MP expands_AND_TRACE_tau)) \\ (* diff here *) 1639 NTAC 4 (POP_ASSUM K_TAC) \\ 1640 Q.ABBREV_TAC `n = LENGTH us` \\ 1641 Q.UNABBREV_TAC `C''` \\ 1642 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 1643 Know `?C'. GCONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 1644 >- ( MATCH_MP_TAC unfolding_lemma4 >> art [] ) \\ 1645 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1646 `(C Q) expands ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 1647 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 1648 Q.EXISTS_TAC `C'` >> art [] \\ 1649 Know `EPS (C (FUNPOW E n Q)) (C' Q)` (* diff here *) 1650 >- ( REWRITE_TAC [EPS_AND_TRACE] \\ 1651 Q.EXISTS_TAC `xs'` >> art [] ) >> DISCH_TAC \\ 1652 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 1653 IMP_RES_TAC expands_EPS' \\ 1654 Q.EXISTS_TAC `E1` >> art [] \\ 1655 MATCH_MP_TAC expands_IMP_WEAK_EQUIV >> art [] ]); (* extra steps *) 1656 1657(* The proof is essentially the same with UNIQUE_SOLUTION_OF_CONTRACTIONS *) 1658Theorem UNIQUE_SOLUTION_OF_EXPANSIONS : 1659 !E P Q. WGS E /\ P expands (E P) /\ Q expands (E Q) ==> WEAK_EQUIV P Q 1660Proof 1661 rpt STRIP_TAC 1662 >> REWRITE_TAC [WEAK_EQUIV] 1663 >> Q.EXISTS_TAC `\R S. ?C. GCONTEXT C /\ WEAK_EQUIV R (C P) /\ WEAK_EQUIV S (C Q)` 1664 >> BETA_TAC >> CONJ_TAC 1665 >- (Q.EXISTS_TAC `E` \\ 1666 CONJ_TAC >- IMP_RES_TAC WGS_IMP_GCONTEXT \\ 1667 IMP_RES_TAC expands_IMP_WEAK_EQUIV >> art []) 1668 >> REWRITE_TAC [WEAK_BISIM] 1669 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 1670 >| [ (* goal 1 (of 4) *) 1671 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1672 (ASSUME_TAC o (Q.SPECL [`l`, `E1`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 1673 RES_TAC \\ 1674 Q.PAT_X_ASSUM `TRANS E' (label l) E1 ==> X` K_TAC \\ 1675 ASSUME_TAC (Q.SPECL [`P`, `Q`] UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA) \\ 1676 `!l R. WEAK_TRANS (C P) (label l) R ==> 1677 ?C'. GCONTEXT C' /\ R expands (C' P) /\ 1678 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C Q) (C' Q)` 1679 by METIS_TAC [] \\ 1680 Q.PAT_X_ASSUM `(?E. WGS E /\ P expands (E P) /\ Q expands (E Q)) ==> X` K_TAC \\ 1681 RES_TAC \\ 1682 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1683 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1684 (ASSUME_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 1685 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C P) (label l) R ==> X` K_TAC \\ 1686 RES_TAC \\ 1687 Q.PAT_X_ASSUM `WEAK_TRANS (C Q) (label l) y ==> X` K_TAC \\ 1688 Q.EXISTS_TAC `E1'` >> art [] \\ 1689 Q.EXISTS_TAC `C'` >> art [] \\ 1690 `WEAK_EQUIV E1' (C' Q)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1691 `WEAK_EQUIV E2 (C' P)` by PROVE_TAC [expands_IMP_WEAK_EQUIV] \\ 1692 PROVE_TAC [WEAK_EQUIV_TRANS], 1693 (* goal 2 (of 4) *) 1694 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1695 (ASSUME_TAC o (Q.SPECL [`l`, `E2`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 1696 RES_TAC \\ 1697 Q.PAT_X_ASSUM `TRANS E'' (label l) E2 ==> X` K_TAC \\ 1698 ASSUME_TAC (Q.SPECL [`Q`, `P`] UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA) \\ 1699 `!l R. WEAK_TRANS (C Q) (label l) R ==> 1700 ?C'. GCONTEXT C' /\ R expands (C' Q) /\ 1701 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C P) (C' P)` 1702 by METIS_TAC [] \\ 1703 Q.PAT_X_ASSUM `(?E. WGS E /\ Q expands (E Q) /\ P expands (E P)) ==> X` K_TAC \\ 1704 RES_TAC \\ 1705 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1706 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1707 (ASSUME_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 1708 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C Q) (label l) R ==> X` K_TAC \\ 1709 RES_TAC \\ 1710 Q.PAT_X_ASSUM `WEAK_TRANS (C P) (label l) y ==> X` K_TAC \\ 1711 Q.EXISTS_TAC `E1` >> art [] \\ 1712 Q.EXISTS_TAC `C'` >> art [] \\ 1713 `WEAK_EQUIV E1 (C' P)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1714 `WEAK_EQUIV E2' (C' Q)` by PROVE_TAC [expands_IMP_WEAK_EQUIV] \\ 1715 PROVE_TAC [WEAK_EQUIV_TRANS], 1716 (* goal 3 (of 4) *) 1717 IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau 1718 (ASSUME ``WEAK_EQUIV E' ((C :('a, 'b) context) P)``)) \\ 1719 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 1720 >- ( Q.EXISTS_TAC `E''` >> REWRITE_TAC [EPS_REFL] \\ 1721 Q.EXISTS_TAC `C` >> art [] ) \\ 1722 ASSUME_TAC (Q.SPECL [`P`, `Q`] UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA) \\ 1723 `!R. WEAK_TRANS (C P) tau R ==> 1724 ?C'. GCONTEXT C' /\ R expands (C' P) /\ 1725 (WEAK_EQUIV O EPS) (C Q) (C' Q)` by METIS_TAC [] \\ 1726 Q.PAT_X_ASSUM `(?E. WGS E /\ P expands (E P) /\ Q expands (E Q)) ==> X` K_TAC \\ 1727 RES_TAC \\ 1728 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1729 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 1730 (ASSUME_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 1731 Q.PAT_X_ASSUM `!R. WEAK_TRANS (C P) tau R ==> X` K_TAC \\ 1732 RES_TAC \\ 1733 Q.PAT_X_ASSUM `EPS (C Q) y ==> X` K_TAC \\ 1734 Q.EXISTS_TAC `E1'` >> art [] \\ 1735 Q.EXISTS_TAC `C'` >> art [] \\ 1736 `WEAK_EQUIV E1' (C' Q)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1737 `WEAK_EQUIV E2 (C' P)` by PROVE_TAC [expands_IMP_WEAK_EQUIV] \\ 1738 PROVE_TAC [WEAK_EQUIV_TRANS], 1739 (* goal 4 (of 4) *) 1740 IMP_RES_TAC (MATCH_MP WEAK_EQUIV_TRANS_tau 1741 (ASSUME ``WEAK_EQUIV E'' ((C :('a, 'b) context) Q)``)) \\ 1742 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 1743 >- ( Q.EXISTS_TAC `E'` >> REWRITE_TAC [EPS_REFL] \\ 1744 Q.EXISTS_TAC `C` >> art [] ) \\ 1745 ASSUME_TAC (Q.SPECL [`Q`, `P`] UNIQUE_SOLUTION_OF_EXPANSIONS_LEMMA) \\ 1746 `!R. WEAK_TRANS (C Q) tau R ==> 1747 ?C'. GCONTEXT C' /\ R expands (C' Q) /\ 1748 (WEAK_EQUIV O EPS) (C P) (C' P)` by METIS_TAC [] \\ 1749 Q.PAT_X_ASSUM `(?E. WGS E /\ Q expands (E Q) /\ P expands (E P)) ==> X` K_TAC \\ 1750 RES_TAC \\ 1751 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 1752 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 1753 (ASSUME_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 1754 Q.PAT_X_ASSUM `!R. WEAK_TRANS (C Q) tau R ==> X` K_TAC \\ 1755 RES_TAC \\ 1756 Q.PAT_X_ASSUM `EPS (C P) y ==> X` K_TAC \\ 1757 Q.EXISTS_TAC `E1` >> art [] \\ 1758 Q.EXISTS_TAC `C'` >> art [] \\ 1759 `WEAK_EQUIV E1 (C' P)` by PROVE_TAC [WEAK_EQUIV_TRANS] >> art [] \\ 1760 `WEAK_EQUIV E2' (C' Q)` by PROVE_TAC [expands_IMP_WEAK_EQUIV] \\ 1761 PROVE_TAC [WEAK_EQUIV_TRANS] ] 1762QED 1763 1764(* Another way to prove above theorem using UNIQUE_SOLUTION_OF_CONTRACTIONS, this method 1765 works for any relation coarser than `contracts`, partial-ordering and precogruence of 1766 `expands` are not needed. *) 1767val UNIQUE_SOLUTION_OF_EXPANSIONS' = store_thm ( 1768 "UNIQUE_SOLUTION_OF_EXPANSIONS'", 1769 ``!E. WGS E ==> 1770 !P Q. P expands (E P) /\ Q expands (E Q) ==> WEAK_EQUIV P Q``, 1771 rpt STRIP_TAC 1772 >> IMP_RES_TAC expands_IMP_contracts 1773 >> irule UNIQUE_SOLUTION_OF_CONTRACTIONS 1774 >> Q.EXISTS_TAC `E` >> art []); 1775 1776(******************************************************************************) 1777(* *) 1778(* 6. Unique solutions of observational contractions *) 1779(* *) 1780(******************************************************************************) 1781 1782(* NOTE: the lemma works for any precongruence relation *) 1783Theorem OBS_unfolding_lemma1 : 1784 !E C P. CONTEXT E /\ CONTEXT C /\ OBS_contracts P (E P) ==> 1785 !n. OBS_contracts (C P) ((C o (FUNPOW E n)) P) 1786Proof 1787 rpt STRIP_TAC 1788 >> REWRITE_TAC [o_DEF] 1789 >> BETA_TAC 1790 >> irule OBS_contracts_SUBST_CONTEXT >> art [] 1791 >> Q.SPEC_TAC (`n`, `n`) 1792 >> Induct >- REWRITE_TAC [FUNPOW, OBS_contracts_REFL] 1793 >> REWRITE_TAC [FUNPOW_SUC] 1794 >> Q.ABBREV_TAC `Q = FUNPOW E n P` 1795 >> `OBS_contracts (E P) (E Q)` by PROVE_TAC [OBS_contracts_SUBST_CONTEXT] 1796 >> IMP_RES_TAC OBS_contracts_TRANS 1797QED 1798 1799(* A single transition from WG E[P] will not touch the variable P *) 1800Theorem OBS_unfolding_lemma2 : 1801 !E. WG E ==> 1802 !P u P'. TRANS (E P) u P' ==> 1803 ?C'. CONTEXT C' /\ (P' = C' P) /\ !Q. TRANS (E Q) u (C' Q) 1804Proof 1805 HO_MATCH_MP_TAC WG_strongind 1806 >> BETA_TAC >> REWRITE_TAC [ETA_AX] 1807 >> reverse (rpt STRIP_TAC 1808 >- (Q.EXISTS_TAC `\t. P'` >> art [CONTEXT2]) 1809 >- (IMP_RES_TAC TRANS_PREFIX \\ 1810 Q.EXISTS_TAC `e` >> art [] \\ 1811 GEN_TAC >> REWRITE_TAC [PREFIX])) (* 4 goals left *) 1812 >| [ (* goal 1 (of 4) *) 1813 IMP_RES_TAC TRANS_RELAB >> RES_TAC \\ 1814 Q.EXISTS_TAC `\t. relab (C' t) rf` >> BETA_TAC \\ 1815 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT7 >> art [] ) \\ 1816 art [] \\ 1817 GEN_TAC >> MATCH_MP_TAC RELABELING >> art [], 1818 (* goal 2 (of 4) *) 1819 IMP_RES_TAC TRANS_RESTR >| (* 2 sub-goals here *) 1820 [ (* goal 2.1 (of 2) *) 1821 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1822 Q.EXISTS_TAC `\t. restr L (C' t)` >> BETA_TAC \\ 1823 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT6 >> art [] ) \\ 1824 art [] \\ 1825 GEN_TAC >> MATCH_MP_TAC RESTR >> art [], 1826 (* goal 2.2 (of 2) *) 1827 FULL_SIMP_TAC std_ss [] >> RES_TAC \\ 1828 Q.EXISTS_TAC `\t. restr L (C' t)` >> BETA_TAC \\ 1829 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT6 >> art [] ) \\ 1830 art [] \\ 1831 GEN_TAC >> MATCH_MP_TAC RESTR >> art [] \\ 1832 Q.EXISTS_TAC `l` >> art [] ], 1833 (* goal 3 (of 4) *) 1834 IMP_RES_TAC TRANS_PAR >| (* 3 sub-goals here *) 1835 [ (* goal 3.1 (of 3) *) 1836 RES_TAC \\ 1837 Q.EXISTS_TAC `\t. par (C' t) (E' t)` >> BETA_TAC \\ 1838 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT5 >> art [] \\ 1839 MATCH_MP_TAC WG_IMP_CONTEXT >> art [] ) \\ 1840 FULL_SIMP_TAC std_ss [] \\ 1841 GEN_TAC >> MATCH_MP_TAC PAR1 >> art [], 1842 (* goal 3.2 (of 3) *) 1843 RES_TAC \\ 1844 Q.EXISTS_TAC `\t. par (E t) (C' t)` >> BETA_TAC \\ 1845 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT5 >> art [] \\ 1846 MATCH_MP_TAC WG_IMP_CONTEXT >> art [] ) \\ 1847 FULL_SIMP_TAC std_ss [] \\ 1848 GEN_TAC >> MATCH_MP_TAC PAR2 >> art [], 1849 (* goal 3.3 (of 3) *) 1850 RES_TAC \\ 1851 Q.EXISTS_TAC `\t. par (C'' t) (C' t)` >> BETA_TAC \\ 1852 CONJ_TAC >- ( MATCH_MP_TAC CONTEXT5 >> art [] ) \\ 1853 FULL_SIMP_TAC std_ss [] \\ 1854 GEN_TAC >> MATCH_MP_TAC PAR3 \\ 1855 Q.EXISTS_TAC `l` >> art [] ], 1856 (* goal 4 (of 4) *) 1857 IMP_RES_TAC TRANS_SUM >| (* 2 sub-goals here *) 1858 [ (* goal 4.1 (of 2) *) 1859 Q.PAT_X_ASSUM `!P u P'. TRANS (E P) u P' ==> X` MP_TAC \\ 1860 Q.PAT_X_ASSUM `TRANS (sum (E P) (E' P)) u P'` MP_TAC \\ 1861 POP_ASSUM MP_TAC \\ 1862 Q.PAT_X_ASSUM `WG E` MP_TAC \\ 1863 Q.SPEC_TAC (`E`, `E`) \\ 1864 HO_MATCH_MP_TAC WG_strongind \\ 1865 BETA_TAC >> REWRITE_TAC [ETA_AX] >> rpt STRIP_TAC (* 6 sub-goals here *) 1866 >- ( RES_TAC >> POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `P`)) \\ 1867 Q.EXISTS_TAC `C'` >> art [] \\ 1868 GEN_TAC >> MATCH_MP_TAC SUM1 >> art [] ) \\ 1869 RES_TAC >> Q.EXISTS_TAC `C'` >> art [] \\ 1870 GEN_TAC >> MATCH_MP_TAC SUM1 >> art [], 1871 (* goal 4.2 (of 2) *) 1872 Q.PAT_X_ASSUM `!P u P'. TRANS (E' P) u P' ==> X` MP_TAC \\ 1873 Q.PAT_X_ASSUM `TRANS (sum (E P) (E' P)) u P'` MP_TAC \\ 1874 POP_ASSUM MP_TAC \\ 1875 Q.PAT_X_ASSUM `WG E'` MP_TAC \\ 1876 Q.SPEC_TAC (`E'`, `E'`) \\ 1877 HO_MATCH_MP_TAC WG_strongind \\ 1878 BETA_TAC >> REWRITE_TAC [ETA_AX] >> rpt STRIP_TAC (* 6 sub-goals here *) 1879 >- ( RES_TAC >> POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPEC `P`)) \\ 1880 Q.EXISTS_TAC `C'` >> art [] \\ 1881 GEN_TAC >> MATCH_MP_TAC SUM2 >> art [] ) \\ 1882 RES_TAC >> Q.EXISTS_TAC `C'` >> art [] \\ 1883 GEN_TAC >> MATCH_MP_TAC SUM2 >> art [] ] ] 1884QED 1885 1886(* In this proof, we combine C and E into a single WG and call previous lemma *) 1887Theorem OBS_unfolding_lemma3 : 1888 !C E. CONTEXT C /\ WG E ==> 1889 !P x P'. TRANS (C (E P)) x P' ==> 1890 ?C'. CONTEXT C' /\ (P' = C' P) /\ !Q. TRANS (C (E Q)) x (C' Q) 1891Proof 1892 rpt STRIP_TAC 1893 >> IMP_RES_TAC CONTEXT_WG_combin 1894 >> Know `C (E P) = (C o E) P` >- SIMP_TAC std_ss [o_DEF] 1895 >> DISCH_TAC 1896 >> Q.PAT_X_ASSUM `TRANS (C (E P)) x P'` MP_TAC 1897 >> art [] >> DISCH_TAC 1898 >> IMP_RES_TAC OBS_unfolding_lemma2 1899 >> POP_ASSUM K_TAC 1900 >> Q.EXISTS_TAC `C'` >> art [] 1901 >> GEN_TAC >> POP_ASSUM MP_TAC 1902 >> KILL_TAC 1903 >> REWRITE_TAC [o_DEF] >> BETA_TAC 1904 >> RW_TAC std_ss [] 1905QED 1906 1907Theorem OBS_unfolding_lemma4 : 1908 !C E n xs P' P. CONTEXT C /\ WG E /\ 1909 TRACE ((C o FUNPOW E n) P) xs P' /\ (LENGTH xs <= n) ==> 1910 ?C'. CONTEXT C' /\ (P' = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs (C' Q) 1911Proof 1912 NTAC 2 GEN_TAC 1913 >> Induct_on `n` 1914 >- (RW_TAC std_ss [o_DEF, FUNPOW_0] \\ 1915 Q.EXISTS_TAC `C` >> fs [TRACE_NIL]) 1916 >> rpt STRIP_TAC 1917 >> Q.PAT_X_ASSUM `TRACE X xs P'` MP_TAC 1918 >> Know `!P. (C o (FUNPOW E (SUC n))) P = (C o (FUNPOW E n)) (E P)` 1919 >- RW_TAC std_ss [o_DEF, FUNPOW] >> Rewr 1920 >> DISCH_TAC 1921 >> IMP_RES_TAC TRACE_cases2 1922 >> Cases_on `xs` 1923 >- (REV_FULL_SIMP_TAC std_ss [NULL] \\ 1924 `LENGTH (epsilon :'b Action list) <= n` by FULL_SIMP_TAC arith_ss [LENGTH] \\ 1925 Q.PAT_X_ASSUM `!xs P' P. X ==> X'` 1926 (MP_TAC o (Q.SPECL [`[] :'b Action list`, `P'`, `(E :('a, 'b) context) P`])) \\ 1927 RW_TAC std_ss [] \\ 1928 Q.EXISTS_TAC `C' o E` >> art [] \\ 1929 CONJ_TAC >- (IMP_RES_TAC WG_IMP_CONTEXT \\ 1930 MATCH_MP_TAC CONTEXT_combin >> art []) \\ 1931 CONJ_TAC >- (KILL_TAC >> REWRITE_TAC [o_DEF] >> RW_TAC std_ss []) \\ 1932 GEN_TAC >> ASM_SIMP_TAC std_ss [o_DEF]) 1933 >> FULL_SIMP_TAC list_ss [] 1934 >> `LENGTH (FRONT (h::t)) <= n` by PROVE_TAC [LENGTH_FRONT_CONS] 1935 >> Q.ABBREV_TAC `xs = FRONT (h::t)` 1936 >> Q.ABBREV_TAC `x = LAST (h::t)` 1937 >> Q.PAT_X_ASSUM `!xs P'' P'''. X ==> X'` 1938 (MP_TAC o (Q.SPECL [`xs`, `u`, `(E :('a, 'b) context) P`])) 1939 >> RW_TAC std_ss [] 1940 >> MP_TAC (Q.SPECL [`C'`, `E`] OBS_unfolding_lemma3) 1941 >> RW_TAC bool_ss [] 1942 >> POP_ASSUM (MP_TAC o (Q.SPECL [`P`, `x`, `P'`])) 1943 >> RW_TAC bool_ss [] 1944 >> Q.EXISTS_TAC `C''` >> art [] 1945 >> GEN_TAC >> ONCE_REWRITE_TAC [TRACE_cases2] 1946 >> REWRITE_TAC [NULL] 1947 >> Q.EXISTS_TAC `C' (E Q)` 1948 >> Q.UNABBREV_TAC `x` >> art [] 1949 >> Q.UNABBREV_TAC `xs` >> art [] 1950QED 1951 1952(* Lemma 3.9 of [2] *) 1953val UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA = store_thm ( 1954 "UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA", 1955 ``!(P :('a, 'b) CCS) (Q :('a, 'b) CCS) E. 1956 WG E /\ OBS_contracts P (E P) /\ OBS_contracts Q (E Q) ==> 1957 !(C :('a, 'b) context). CONTEXT C ==> 1958 (!l R. WEAK_TRANS (C P) (label l) R ==> 1959 ?C'. CONTEXT C' /\ R contracts (C' P) /\ 1960 (WEAK_EQUIV O (\x y. WEAK_TRANS x (label l) y)) (C Q) (C' Q)) /\ 1961 (!R. WEAK_TRANS (C P) tau R ==> 1962 ?C'. CONTEXT C' /\ R contracts (C' P) /\ 1963 (WEAK_EQUIV O EPS) (C Q) (C' Q))``, 1964 NTAC 6 STRIP_TAC 1965 (* Part 1: construct C'' which is a CONTEXT *) 1966 >> IMP_RES_TAC WG_IMP_CONTEXT 1967 >> Q.ABBREV_TAC `C'' = \n. C o (FUNPOW E n)` 1968 >> Know `!n. CONTEXT (C'' n)` 1969 >- (Q.UNABBREV_TAC `C''` >> BETA_TAC \\ 1970 Induct_on `n` >- art [o_DEF, FUNPOW, ETA_THM] \\ 1971 REWRITE_TAC [FUNPOW_SUC_LEFT, o_ASSOC] \\ 1972 MATCH_MP_TAC CONTEXT_combin >> art []) >> DISCH_TAC 1973 (* Part 2: property of C'' on P and Q *) 1974 >> `!n. OBS_contracts (C P) (C'' n P)` 1975 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [OBS_unfolding_lemma1]) 1976 >> `!n. OBS_contracts (C Q) (C'' n Q)` 1977 by (Q.UNABBREV_TAC `C''` >> BETA_TAC >> PROVE_TAC [OBS_unfolding_lemma1]) 1978 (* Part 3 *) 1979 >> rpt STRIP_TAC (* 2 sub-goals here *) 1980 >| [ (* goal 1 (of 2) *) 1981 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 1982 FULL_SIMP_TAC std_ss [Action_distinct_label] \\ 1983 `OBS_contracts (C P) (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 1984 POP_ASSUM (IMP_RES_TAC o (MATCH_MP OBS_contracts_AND_TRACE_label)) \\ 1985 NTAC 4 (POP_ASSUM K_TAC) \\ 1986 Q.ABBREV_TAC `n = LENGTH us` \\ 1987 Q.UNABBREV_TAC `C''` \\ 1988 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 1989 Know `?C'. CONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 1990 >- (MATCH_MP_TAC OBS_unfolding_lemma4 >> art []) \\ 1991 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 1992 `OBS_contracts (C Q) ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 1993 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 1994 Q.EXISTS_TAC `C'` >> art [] \\ 1995 Know `WEAK_TRANS (C (FUNPOW E n Q)) (label l) (C' Q)` 1996 >- (REWRITE_TAC [WEAK_TRANS_AND_TRACE, Action_distinct_label] \\ 1997 Q.EXISTS_TAC `xs'` >> art [] \\ 1998 MATCH_MP_TAC UNIQUE_LABEL_NOT_NULL \\ 1999 Q.EXISTS_TAC `label l` >> art []) >> DISCH_TAC \\ 2000 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 2001 IMP_RES_TAC OBS_contracts_WEAK_TRANS_label' \\ 2002 Q.EXISTS_TAC `E1` >> art [], 2003 (* goal 2 (of 2) *) 2004 IMP_RES_TAC WEAK_TRANS_AND_TRACE \\ 2005 FULL_SIMP_TAC std_ss [] \\ 2006 `OBS_contracts (C P) (C'' (LENGTH us) P)` by PROVE_TAC [] \\ 2007 POP_ASSUM (IMP_RES_TAC o (MATCH_MP OBS_contracts_AND_TRACE_tau)) \\ (* diff here *) 2008 NTAC 4 (POP_ASSUM K_TAC) \\ 2009 Q.ABBREV_TAC `n = LENGTH us` \\ 2010 Q.UNABBREV_TAC `C''` \\ 2011 Q.PAT_X_ASSUM `TRACE X xs' E2` (ASSUME_TAC o BETA_RULE) \\ 2012 Know `?C'. CONTEXT C' /\ (E2 = C' P) /\ !Q. TRACE ((C o FUNPOW E n) Q) xs' (C' Q)` 2013 >- (MATCH_MP_TAC OBS_unfolding_lemma4 >> art []) \\ 2014 STRIP_TAC >> POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 2015 `OBS_contracts (C Q) ((C o FUNPOW E n) Q)` by PROVE_TAC [] \\ 2016 FULL_SIMP_TAC std_ss [] \\ (* to replace E2 *) 2017 Q.EXISTS_TAC `C'` >> art [] \\ 2018 Know `EPS (C (FUNPOW E n Q)) (C' Q)` (* diff here *) 2019 >- (REWRITE_TAC [EPS_AND_TRACE] \\ 2020 Q.EXISTS_TAC `xs'` >> art []) >> DISCH_TAC \\ 2021 REWRITE_TAC [O_DEF] >> BETA_TAC \\ 2022 IMP_RES_TAC OBS_contracts_EPS' \\ 2023 Q.EXISTS_TAC `E1` >> art [] ]); 2024 2025(* Shared lemma for UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS and 2026 UNIQUE_SOLUTION_OF_ROOTED_CONTRACTIONS *) 2027val shared_lemma = Q.prove ( 2028 `WG E /\ OBS_contracts P (E P) /\ OBS_contracts Q (E Q) ==> 2029 WEAK_BISIM (\R S. ?C. CONTEXT C /\ 2030 WEAK_EQUIV R (C P) /\ WEAK_EQUIV S (C Q))`, 2031 STRIP_TAC 2032 >> REWRITE_TAC [WEAK_BISIM] 2033 >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 2034 >| [ (* goal 1 (of 4) *) 2035 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 2036 (MP_TAC o (Q.SPECL [`l`, `E1`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 2037 RW_TAC std_ss [] \\ 2038 MP_TAC (Q.SPECL [`P`, `Q`, `E`] UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA) \\ 2039 RW_TAC std_ss [] \\ 2040 POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\ 2041 POP_ASSUM K_TAC \\ 2042 POP_ASSUM (MP_TAC o (Q.SPECL [`l`, `E2`])) >> RW_TAC std_ss [] \\ 2043 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 2044 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 2045 (MP_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 2046 RW_TAC std_ss [] \\ 2047 Q.EXISTS_TAC `E1'` >> art [] \\ 2048 Q.EXISTS_TAC `C'` >> art [] \\ 2049 reverse CONJ_TAC >- PROVE_TAC [WEAK_EQUIV_TRANS] \\ 2050 IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 2051 PROVE_TAC [WEAK_EQUIV_TRANS], 2052 (* goal 2 (of 4) *) 2053 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 2054 (MP_TAC o (Q.SPECL [`l`, `E2`]) o (MATCH_MP WEAK_EQUIV_TRANS_label)) \\ 2055 RW_TAC std_ss [] \\ 2056 MP_TAC (Q.SPECL [`Q`, `P`, `E`] UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA) \\ 2057 RW_TAC std_ss [] \\ 2058 POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\ 2059 POP_ASSUM K_TAC \\ 2060 POP_ASSUM (MP_TAC o (Q.SPECL [`l`, `E2'`])) >> RW_TAC std_ss [] \\ 2061 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 2062 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 2063 (MP_TAC o (Q.SPECL [`l`, `y`]) o (MATCH_MP WEAK_EQUIV_WEAK_TRANS_label')) \\ 2064 RW_TAC std_ss [] \\ 2065 Q.EXISTS_TAC `E1` >> art [] \\ 2066 Q.EXISTS_TAC `C'` >> art [] \\ 2067 CONJ_TAC >- PROVE_TAC [WEAK_EQUIV_TRANS] \\ 2068 IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 2069 PROVE_TAC [WEAK_EQUIV_TRANS], 2070 (* goal 3 (of 4) *) 2071 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 2072 (MP_TAC o (Q.SPEC `E1`) o (MATCH_MP WEAK_EQUIV_TRANS_tau)) \\ 2073 RW_TAC std_ss [] \\ 2074 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 2075 >- (Q.EXISTS_TAC `E''` >> REWRITE_TAC [EPS_REFL] \\ 2076 Q.EXISTS_TAC `C` >> art []) \\ 2077 Q.PAT_X_ASSUM `EPS _ E2` K_TAC \\ 2078 MP_TAC (Q.SPECL [`P`, `Q`, `E`] UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA) \\ 2079 RW_TAC std_ss [] \\ 2080 POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\ 2081 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C P) (label l) R ==> X` K_TAC \\ 2082 POP_ASSUM (MP_TAC o (Q.SPEC `E2`)) >> RW_TAC std_ss [] \\ 2083 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 2084 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 2085 (MP_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 2086 RW_TAC std_ss [] \\ 2087 Q.EXISTS_TAC `E1'` >> art [] \\ 2088 Q.EXISTS_TAC `C'` >> art [] \\ 2089 reverse CONJ_TAC >- PROVE_TAC [WEAK_EQUIV_TRANS] \\ 2090 IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 2091 PROVE_TAC [WEAK_EQUIV_TRANS], 2092 (* goal 4 (of 4) *) 2093 Q.PAT_X_ASSUM `WEAK_EQUIV E'' (C Q)` 2094 (MP_TAC o (Q.SPEC `E2`) o (MATCH_MP WEAK_EQUIV_TRANS_tau)) \\ 2095 RW_TAC std_ss [] \\ 2096 IMP_RES_TAC EPS_IMP_WEAK_TRANS (* 2 sub-goals here *) 2097 >- (Q.EXISTS_TAC `E'` >> REWRITE_TAC [EPS_REFL] \\ 2098 Q.EXISTS_TAC `C` >> art []) \\ 2099 Q.PAT_X_ASSUM `EPS _ E2'` K_TAC \\ 2100 MP_TAC (Q.SPECL [`Q`, `P`, `E`] UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS_LEMMA) \\ 2101 RW_TAC std_ss [] \\ 2102 POP_ASSUM (MP_TAC o (Q.SPEC `C`)) >> RW_TAC std_ss [] \\ 2103 Q.PAT_X_ASSUM `!l R. WEAK_TRANS (C Q) (label l) R ==> X` K_TAC \\ 2104 POP_ASSUM (MP_TAC o (Q.SPEC `E2'`)) >> RW_TAC std_ss [] \\ 2105 POP_ASSUM MP_TAC >> REWRITE_TAC [O_DEF] >> BETA_TAC >> STRIP_TAC \\ 2106 Q.PAT_X_ASSUM `WEAK_EQUIV E' (C P)` 2107 (MP_TAC o (Q.SPEC `y`) o (MATCH_MP WEAK_EQUIV_EPS')) \\ 2108 RW_TAC std_ss [] \\ 2109 Q.EXISTS_TAC `E1` >> art [] \\ 2110 Q.EXISTS_TAC `C'` >> art [] \\ 2111 CONJ_TAC >- PROVE_TAC [WEAK_EQUIV_TRANS] \\ 2112 IMP_RES_TAC contracts_IMP_WEAK_EQUIV \\ 2113 PROVE_TAC [WEAK_EQUIV_TRANS] ]); 2114 2115Theorem UNIQUE_SOLUTION_OF_OBS_CONTRACTIONS : 2116 !E P Q. WG E /\ OBS_contracts P (E P) /\ OBS_contracts Q (E Q) ==> WEAK_EQUIV P Q 2117Proof 2118 rpt STRIP_TAC 2119 >> REWRITE_TAC [WEAK_EQUIV] 2120 >> Q.EXISTS_TAC `\R S. ?C. CONTEXT C /\ WEAK_EQUIV R (C P) /\ WEAK_EQUIV S (C Q)` 2121 >> BETA_TAC >> CONJ_TAC 2122 >- (Q.EXISTS_TAC `E` \\ 2123 CONJ_TAC >- IMP_RES_TAC WG_IMP_CONTEXT \\ 2124 IMP_RES_TAC OBS_contracts_IMP_WEAK_EQUIV >> art []) 2125 >> MATCH_MP_TAC shared_lemma >> art [] 2126QED 2127 2128(******************************************************************************) 2129(* *) 2130(* 7. Unique solutions of rooted contractions (EXPRESS/SOS 2018) *) 2131(* *) 2132(******************************************************************************) 2133 2134(* This is a stronger version of previous theorem: conclusion is `OBS_CONGR P Q` 2135 OBS_CONGR_BY_WEAK_BISIM and STRONG_UNIQUE_SOLUTION_LEMMA must be used here. 2136 *) 2137Theorem UNIQUE_SOLUTION_OF_ROOTED_CONTRACTIONS : 2138 !E P Q. WG E /\ OBS_contracts P (E P) /\ OBS_contracts Q (E Q) ==> OBS_CONGR P Q 2139Proof 2140 rpt STRIP_TAC 2141 >> irule OBS_CONGR_BY_WEAK_BISIM 2142 >> Q.EXISTS_TAC `\R S. ?C. CONTEXT C /\ WEAK_EQUIV R (C P) /\ WEAK_EQUIV S (C Q)` 2143 >> BETA_TAC >> CONJ_TAC 2144 >- (rpt STRIP_TAC >| (* 2 subgoals *) 2145 [ (* goal 1 (of 2) *) 2146 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 2147 IMP_RES_TAC STRONG_UNIQUE_SOLUTION_LEMMA \\ 2148 POP_ASSUM (ASSUME_TAC o (Q.SPEC `Q`)) \\ 2149 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 2150 Q.EXISTS_TAC `E1'` >> art [] \\ 2151 Q.EXISTS_TAC `E'` >> art [] \\ 2152 fs [contracts_IMP_WEAK_EQUIV], 2153 (* goal 2 (of 2) *) 2154 IMP_RES_TAC OBS_contracts_TRANS_LEFT \\ 2155 IMP_RES_TAC STRONG_UNIQUE_SOLUTION_LEMMA \\ 2156 POP_ASSUM (ASSUME_TAC o (Q.SPEC `P`)) \\ 2157 IMP_RES_TAC OBS_contracts_TRANS_RIGHT \\ 2158 Q.EXISTS_TAC `E1'` >> art [] \\ 2159 Q.EXISTS_TAC `E'` >> art [] \\ 2160 fs [contracts_IMP_WEAK_EQUIV] ]) 2161 >> MATCH_MP_TAC shared_lemma >> art [] 2162QED 2163 2164(* Bibliography: 2165 * 2166 * [1] Milner, R.: Communication and concurrency. (1989). 2167 * [2] Sangiorgi, D.: Equations, contractions, and unique solutions. ACM SIGPLAN Notices. (2015). 2168 *) 2169 2170val _ = export_theory (); 2171val _ = print_theory_to_file "-" "UniqueSolutionsTheory.lst"; 2172val _ = html_theory "UniqueSolutions"; 2173