1(* ========================================================================== *) 2(* FILE : CongruenceScript.sml *) 3(* DESCRIPTION : The theory of congruence and guarded contexts *) 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 combinTheory arithmeticTheory; 15open CCSLib CCSTheory; 16open StrongEQTheory StrongLawsTheory WeakEQTheory WeakLawsTheory; 17open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory ObsCongrConv; 18open BisimulationUptoTheory; 19 20val _ = new_theory "Congruence"; 21val _ = temp_loose_equality (); 22 23(******************************************************************************) 24(* *) 25(* STRONG_EQ is preserved by recursive definition *) 26(* *) 27(******************************************************************************) 28 29(* moved to MultivariateScript.sml *) 30 31(******************************************************************************) 32(* *) 33(* one-hole contexts and multi-hole contexts *) 34(* *) 35(******************************************************************************) 36 37val _ = type_abbrev_pp ("context", ``:('a, 'b) CCS -> ('a, 'b) CCS``); 38 39Definition IS_CONST_def : 40 IS_CONST (e :('a, 'b) context) <=> !t1 t2. e t1 = e t2 41End 42 43Theorem IS_CONST_alt : 44 !e. IS_CONST e <=> ?p. !t. (e t = p) 45Proof 46 RW_TAC std_ss [IS_CONST_def] 47 >> METIS_TAC [] 48QED 49 50(* ONE HOLE CONTEXT (unused) *) 51Inductive OH_CONTEXT : 52 ( OH_CONTEXT (\t. t)) /\ (* OH_CONTEXT1 *) 53 (!a c. OH_CONTEXT c ==> OH_CONTEXT (\t. prefix a (c t))) /\ (* OH_CONTEXT2 *) 54 (!x c. OH_CONTEXT c ==> OH_CONTEXT (\t. sum (c t) x)) /\ (* OH_CONTEXT3 *) 55 (!x c. OH_CONTEXT c ==> OH_CONTEXT (\t. sum x (c t))) /\ (* OH_CONTEXT4 *) 56 (!x c. OH_CONTEXT c ==> OH_CONTEXT (\t. par (c t) x)) /\ (* OH_CONTEXT5 *) 57 (!x c. OH_CONTEXT c ==> OH_CONTEXT (\t. par x (c t))) /\ (* OH_CONTEXT6 *) 58 (!L c. OH_CONTEXT c ==> OH_CONTEXT (\t. restr L (c t))) /\ (* OH_CONTEXT7 *) 59 (!rf c. OH_CONTEXT c ==> OH_CONTEXT (\t. relab (c t) rf)) (* OH_CONTEXT8 *) 60End 61 62val [OH_CONTEXT1, OH_CONTEXT2, OH_CONTEXT3, OH_CONTEXT4, OH_CONTEXT5, OH_CONTEXT6, 63 OH_CONTEXT7, OH_CONTEXT8] = 64 map save_thm 65 (combine (["OH_CONTEXT1", "OH_CONTEXT2", "OH_CONTEXT3", "OH_CONTEXT4", 66 "OH_CONTEXT5", "OH_CONTEXT6", "OH_CONTEXT7", "OH_CONTEXT8"], 67 CONJUNCTS OH_CONTEXT_rules)); 68 69val OH_CONTEXT_combin = store_thm ( 70 "OH_CONTEXT_combin", ``!c1 c2. OH_CONTEXT c1 /\ OH_CONTEXT c2 ==> OH_CONTEXT (c1 o c2)``, 71 REPEAT STRIP_TAC 72 >> NTAC 2 (POP_ASSUM MP_TAC) 73 >> Q.SPEC_TAC (`c1`, `c`) 74 >> HO_MATCH_MP_TAC OH_CONTEXT_ind 75 >> REWRITE_TAC [o_DEF] 76 >> BETA_TAC 77 >> REWRITE_TAC [ETA_AX] 78 >> REPEAT STRIP_TAC (* 7 sub-goals here *) 79 >| [ FULL_SIMP_TAC std_ss [OH_CONTEXT2], 80 FULL_SIMP_TAC std_ss [OH_CONTEXT3], 81 FULL_SIMP_TAC std_ss [OH_CONTEXT4], 82 FULL_SIMP_TAC std_ss [OH_CONTEXT5], 83 FULL_SIMP_TAC std_ss [OH_CONTEXT6], 84 FULL_SIMP_TAC std_ss [OH_CONTEXT7], 85 FULL_SIMP_TAC std_ss [OH_CONTEXT8] ]); 86 87(* Multi-hole (or non-hole) contexts (Univariate CCS equations) *) 88Inductive CONTEXT : 89 ( CONTEXT (\t. t)) /\ (* CONTEXT1 *) 90 (!p. CONTEXT (\t. p)) /\ (* CONTEXT2 *) 91 (!a e. CONTEXT e ==> CONTEXT (\t. prefix a (e t))) /\ (* CONTEXT3 *) 92 (!e1 e2. CONTEXT e1 /\ CONTEXT e2 93 ==> CONTEXT (\t. sum (e1 t) (e2 t))) /\ (* CONTEXT4 *) 94 (!e1 e2. CONTEXT e1 /\ CONTEXT e2 95 ==> CONTEXT (\t. par (e1 t) (e2 t))) /\ (* CONTEXT5 *) 96 (!L e. CONTEXT e ==> CONTEXT (\t. restr L (e t))) /\ (* CONTEXT6 *) 97 (!rf e. CONTEXT e ==> CONTEXT (\t. relab (e t) rf)) (* CONTEXT7 *) 98End 99 100val [CONTEXT1, CONTEXT2, CONTEXT3, CONTEXT4, CONTEXT5, CONTEXT6, CONTEXT7] = 101 map save_thm 102 (combine (["CONTEXT1", "CONTEXT2", "CONTEXT3", "CONTEXT4", "CONTEXT5", 103 "CONTEXT6", "CONTEXT7"], 104 CONJUNCTS CONTEXT_rules)); 105 106val CONTEXT3a = store_thm ( 107 "CONTEXT3a", 108 ``!a :'b Action. CONTEXT (\t. prefix a t)``, 109 ASSUME_TAC CONTEXT1 110 >> IMP_RES_TAC CONTEXT3 111 >> POP_ASSUM MP_TAC 112 >> BETA_TAC >> REWRITE_TAC []); 113 114Theorem CONTEXT_CONST : 115 !e. IS_CONST e ==> CONTEXT e 116Proof 117 RW_TAC std_ss [IS_CONST_def] 118 >> Know `e = (\t. e nil)` >- fs [FUN_EQ_THM] 119 >> Rewr' >> REWRITE_TAC [CONTEXT2] 120QED 121 122Theorem NO_CONTEXT8 : 123 !e X. ~IS_CONST e ==> ~CONTEXT (\t. rec X (e t)) 124Proof 125 rpt GEN_TAC >> ONCE_REWRITE_TAC [CONTEXT_cases] 126 >> fs [FUN_EQ_THM, IS_CONST_def] 127 >> rpt STRIP_TAC 128 >- (Q.EXISTS_TAC `nil` >> rw []) 129 >> Cases_on `p` >> fs [FUN_EQ_THM] 130 >> METIS_TAC [] 131QED 132 133Theorem CONTEXT8_IMP_CONST : 134 !e X. CONTEXT (\t. rec X (e t)) ==> IS_CONST e 135Proof 136 METIS_TAC [NO_CONTEXT8] 137QED 138 139Theorem CONTEXT3_backward : 140 !e u. CONTEXT (\t. prefix u (e t)) ==> CONTEXT e 141Proof 142 rpt STRIP_TAC 143 >> POP_ASSUM (STRIP_ASSUME_TAC o 144 (ONCE_REWRITE_RULE [CONTEXT_cases])) 145 >> fs [FUN_EQ_THM] (* 3 subgoals left *) 146 >| [ (* goal 1 (of 3) *) 147 POP_ASSUM (MP_TAC o (Q.SPEC `nil`)) >> rw [], 148 (* goal 2 (of 3) *) 149 Cases_on `p` (* 8 sub-goals here *) 150 >- PROVE_TAC [CCS_distinct] 151 >- PROVE_TAC [CCS_distinct] 152 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 153 rename1 `!t. (u = o') /\ (e t = C')` \\ 154 `(e = \t. C')` by PROVE_TAC [] >> art [CONTEXT2]) 155 >> PROVE_TAC [CCS_distinct], 156 (* goal 3 (of 3) *) 157 METIS_TAC [] ] 158QED 159 160Theorem CONTEXT4_backward : 161 !e e'. CONTEXT (\t. sum (e t) (e' t)) ==> CONTEXT e /\ CONTEXT e' 162Proof 163 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 164 ( POP_ASSUM (STRIP_ASSUME_TAC o 165 (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *) 166 >> fs [FUN_EQ_THM] (* 3 subgoals left *) 167 >| [ (* goal 1 (of 3) *) 168 POP_ASSUM (MP_TAC o (Q.SPEC `nil`)) \\ 169 SIMP_TAC std_ss [CCS_distinct], 170 (* goal 2 (of 3) *) 171 Cases_on `p` (* 8 sub-goals here *) 172 >- PROVE_TAC [CCS_distinct] 173 >- PROVE_TAC [CCS_distinct] 174 >- PROVE_TAC [CCS_distinct] 175 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 176 rename1 `!t. (e t = C') /\ (e' t = C0)` \\ 177 `(e = \t. C') /\ (e' = \t. C0)` by PROVE_TAC [] \\ 178 ASM_REWRITE_TAC [CONTEXT2]) 179 >> PROVE_TAC [CCS_distinct], 180 (* goal 3 (of 3) *) 181 METIS_TAC [] ] ) 182QED 183 184Theorem CONTEXT5_backward : 185 !e e'. CONTEXT (\t. par (e t) (e' t)) ==> CONTEXT e /\ CONTEXT e' 186Proof 187 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 188 ( POP_ASSUM (STRIP_ASSUME_TAC o 189 (ONCE_REWRITE_RULE [CONTEXT_cases])) (* 7 sub-goals here *) 190 >> fs [FUN_EQ_THM] (* 3 subgoals left *) 191 >| [ (* goal 1 (of 3) *) 192 POP_ASSUM (MP_TAC o (Q.SPEC `nil`)) \\ 193 SIMP_TAC std_ss [CCS_distinct], 194 (* goal 2 (of 3) *) 195 Cases_on `p` (* 8 sub-goals here *) 196 >- PROVE_TAC [CCS_distinct] 197 >- PROVE_TAC [CCS_distinct] 198 >- PROVE_TAC [CCS_distinct] 199 >- PROVE_TAC [CCS_distinct] 200 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 201 rename1 `!t. (e t = C') /\ (e' t = C0)` \\ 202 `(e = \t. C') /\ (e' = \t. C0)` by PROVE_TAC [] \\ 203 ASM_REWRITE_TAC [CONTEXT2]) 204 >> PROVE_TAC [CCS_distinct], 205 (* goal 3 (of 3) *) 206 METIS_TAC [] ] ) 207QED 208 209Theorem CONTEXT6_backward : 210 !e L. CONTEXT (\t. restr L (e t)) ==> CONTEXT e 211Proof 212 rpt STRIP_TAC 213 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [CONTEXT_cases])) 214 >> fs [FUN_EQ_THM] (* 3 subgoals left *) 215 >| [ (* goal 1 (of 3) *) 216 POP_ASSUM (MP_TAC o (Q.SPEC `nil`)) \\ 217 SIMP_TAC std_ss [CCS_distinct], 218 (* goal 2 (of 3) *) 219 Cases_on `p` (* 8 sub-goals here *) 220 >- PROVE_TAC [CCS_distinct] 221 >- PROVE_TAC [CCS_distinct] 222 >- PROVE_TAC [CCS_distinct] 223 >- PROVE_TAC [CCS_distinct] 224 >- PROVE_TAC [CCS_distinct] 225 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 226 rename1 `!t. (L = f) /\ (e t = C')` \\ 227 `(e = \t. C')` by PROVE_TAC [] >> art [CONTEXT2]) 228 >> PROVE_TAC [CCS_distinct], 229 (* goal 3 (of 3) *) 230 METIS_TAC [] ] 231QED 232 233Theorem CONTEXT7_backward : 234 !e rf. CONTEXT (\t. relab (e t) rf) ==> CONTEXT e 235Proof 236 rpt STRIP_TAC 237 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [CONTEXT_cases])) 238 >> fs [FUN_EQ_THM] (* 3 subgoals left *) 239 >| [ (* goal 1 (of 3) *) 240 POP_ASSUM (MP_TAC o (Q.SPEC `nil`)) \\ 241 SIMP_TAC std_ss [CCS_distinct], 242 (* goal 2 (of 3) *) 243 Cases_on `p` (* 8 sub-goals here *) 244 >- PROVE_TAC [CCS_distinct] 245 >- PROVE_TAC [CCS_distinct] 246 >- PROVE_TAC [CCS_distinct] 247 >- PROVE_TAC [CCS_distinct] 248 >- PROVE_TAC [CCS_distinct] 249 >- PROVE_TAC [CCS_distinct] 250 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 251 rename1 `!t. (e t = C') /\ (rf = R)` \\ 252 `(e = \t. C')` by PROVE_TAC [] >> art [CONTEXT2]) 253 >> PROVE_TAC [CCS_distinct], 254 (* goal 3 (of 3) *) 255 METIS_TAC [] ] 256QED 257 258Theorem CONTEXT8_backward : 259 !e X. CONTEXT (\t. rec X (e t)) ==> CONTEXT e 260Proof 261 rpt STRIP_TAC 262 >> MATCH_MP_TAC CONTEXT_CONST 263 >> MATCH_MP_TAC CONTEXT8_IMP_CONST 264 >> Q.EXISTS_TAC `X` >> art [] 265QED 266 267val CONTEXT_combin = store_thm ( 268 "CONTEXT_combin", ``!c1 c2. CONTEXT c1 /\ CONTEXT c2 ==> CONTEXT (c1 o c2)``, 269 REPEAT STRIP_TAC 270 >> NTAC 2 (POP_ASSUM MP_TAC) 271 >> Q.SPEC_TAC (`c1`, `c`) 272 >> HO_MATCH_MP_TAC CONTEXT_ind 273 >> REWRITE_TAC [o_DEF] 274 >> BETA_TAC 275 >> REWRITE_TAC [ETA_AX] 276 >> REPEAT STRIP_TAC (* 6 sub-goals here *) 277 >| [ REWRITE_TAC [CONTEXT2], 278 FULL_SIMP_TAC std_ss [CONTEXT3], 279 FULL_SIMP_TAC std_ss [CONTEXT4], 280 FULL_SIMP_TAC std_ss [CONTEXT5], 281 FULL_SIMP_TAC std_ss [CONTEXT6], 282 FULL_SIMP_TAC std_ss [CONTEXT7] ]); 283 284(* One-hole contexts are also multi-hole contexts *) 285val OH_CONTEXT_IMP_CONTEXT = store_thm ( 286 "OH_CONTEXT_IMP_CONTEXT", ``!c. OH_CONTEXT c ==> CONTEXT c``, 287 Induct_on `OH_CONTEXT` 288 >> rpt STRIP_TAC (* 8 sub-goals here *) 289 >| [ (* goal 1 (of 8) *) 290 REWRITE_TAC [CONTEXT1], 291 (* goal 2 (of 8) *) 292 MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [], 293 (* goal 3 (of 8) *) 294 `CONTEXT (\y. x)` by REWRITE_TAC [CONTEXT2] \\ 295 Know `CONTEXT (\t. c t + (\y. x) t)` 296 >- ( MATCH_MP_TAC CONTEXT4 >> ASM_REWRITE_TAC [] ) \\ 297 BETA_TAC >> REWRITE_TAC [], 298 (* goal 4 (of 8) *) 299 `CONTEXT (\y. x)` by REWRITE_TAC [CONTEXT2] \\ 300 Know `CONTEXT (\t. (\y. x) t + c t)` 301 >- ( MATCH_MP_TAC CONTEXT4 >> ASM_REWRITE_TAC [] ) \\ 302 BETA_TAC >> REWRITE_TAC [], 303 (* goal 5 (of 8) *) 304 `CONTEXT (\y. x)` by REWRITE_TAC [CONTEXT2] \\ 305 Know `CONTEXT (\t. par (c t) ((\y. x) t))` 306 >- ( MATCH_MP_TAC CONTEXT5 >> ASM_REWRITE_TAC [] ) \\ 307 BETA_TAC >> REWRITE_TAC [], 308 (* goal 6 (of 8) *) 309 `CONTEXT (\y. x)` by REWRITE_TAC [CONTEXT2] \\ 310 Know `CONTEXT (\t. par ((\y. x) t) (c t))` 311 >- ( MATCH_MP_TAC CONTEXT5 >> ASM_REWRITE_TAC [] ) \\ 312 BETA_TAC >> REWRITE_TAC [], 313 (* goal 7 (of 8) *) 314 MATCH_MP_TAC CONTEXT6 >> ASM_REWRITE_TAC [], 315 (* goal 8 (of 8) *) 316 MATCH_MP_TAC CONTEXT7 >> ASM_REWRITE_TAC [] ]); 317 318val STRONG_EQUIV_SUBST_CONTEXT = store_thm ( 319 "STRONG_EQUIV_SUBST_CONTEXT", 320 ``!P Q. STRONG_EQUIV P Q ==> !E. CONTEXT E ==> STRONG_EQUIV (E P) (E Q)``, 321 rpt GEN_TAC >> DISCH_TAC 322 >> Induct_on `CONTEXT` >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 323 >- ASM_REWRITE_TAC [] 324 >- REWRITE_TAC [STRONG_EQUIV_REFL] 325 >| [ (* goal 1 (of 5) *) 326 MATCH_MP_TAC STRONG_EQUIV_SUBST_PREFIX >> ASM_REWRITE_TAC [], 327 (* goal 2 (of 5) *) 328 IMP_RES_TAC STRONG_EQUIV_PRESD_BY_SUM, 329 (* goal 3 (of 5) *) 330 IMP_RES_TAC STRONG_EQUIV_PRESD_BY_PAR, 331 (* goal 4 (of 5) *) 332 MATCH_MP_TAC STRONG_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [], 333 (* goal 5 (of 5) *) 334 MATCH_MP_TAC STRONG_EQUIV_SUBST_RELAB >> ASM_REWRITE_TAC [] ]); 335 336val OBS_CONGR_SUBST_CONTEXT = store_thm ( 337 "OBS_CONGR_SUBST_CONTEXT", 338 ``!P Q. OBS_CONGR P Q ==> !E. CONTEXT E ==> OBS_CONGR (E P) (E Q)``, 339 rpt GEN_TAC >> DISCH_TAC 340 >> Induct_on `CONTEXT` >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 341 >- ASM_REWRITE_TAC [] 342 >- REWRITE_TAC [OBS_CONGR_REFL] 343 >| [ (* goal 1 (of 5) *) 344 MATCH_MP_TAC OBS_CONGR_SUBST_PREFIX >> ASM_REWRITE_TAC [], 345 (* goal 2 (of 5) *) 346 IMP_RES_TAC OBS_CONGR_PRESD_BY_SUM, 347 (* goal 3 (of 5) *) 348 IMP_RES_TAC OBS_CONGR_PRESD_BY_PAR, 349 (* goal 4 (of 5) *) 350 MATCH_MP_TAC OBS_CONGR_SUBST_RESTR >> ASM_REWRITE_TAC [], 351 (* goal 5 (of 5) *) 352 MATCH_MP_TAC OBS_CONGR_SUBST_RELAB >> ASM_REWRITE_TAC [] ]); 353 354(******************************************************************************) 355(* *) 356(* Multi-hole context with guarded sums (GCONTEXT) *) 357(* *) 358(******************************************************************************) 359 360Inductive GCONTEXT : 361 ( GCONTEXT (\t. t)) /\ (* GCONTEXT1 *) 362 (!p. GCONTEXT (\t. p)) /\ (* GCONTEXT2 *) 363 (!a e. GCONTEXT e ==> GCONTEXT (\t. prefix a (e t))) /\ (* GCONTEXT3 *) 364 (!a1 a2 e1 e2. 365 GCONTEXT e1 /\ GCONTEXT e2 366 ==> GCONTEXT (\t. sum (prefix a1 (e1 t)) (* GCONTEXT4 *) 367 (prefix a2 (e2 t)))) /\ 368 (!e1 e2. GCONTEXT e1 /\ GCONTEXT e2 369 ==> GCONTEXT (\t. par (e1 t) (e2 t))) /\ (* GCONTEXT5 *) 370 (!L e. GCONTEXT e ==> GCONTEXT (\t. restr L (e t))) /\ (* GCONTEXT6 *) 371 (!rf e. GCONTEXT e ==> GCONTEXT (\t. relab (e t) rf)) (* GCONTEXT7 *) 372End 373 374val [GCONTEXT1, GCONTEXT2, GCONTEXT3, GCONTEXT4, GCONTEXT5, 375 GCONTEXT6, GCONTEXT7] = 376 map save_thm 377 (combine (["GCONTEXT1", "GCONTEXT2", "GCONTEXT3", "GCONTEXT4", 378 "GCONTEXT5", "GCONTEXT6", "GCONTEXT7"], 379 CONJUNCTS GCONTEXT_rules)); 380 381val GCONTEXT3a = store_thm ( 382 "GCONTEXT3a", 383 ``!a :'b Action. GCONTEXT (\t. prefix a t)``, 384 ASSUME_TAC GCONTEXT1 385 >> IMP_RES_TAC GCONTEXT3 386 >> POP_ASSUM MP_TAC 387 >> BETA_TAC >> REWRITE_TAC []); 388 389val GCONTEXT_combin = store_thm ( 390 "GCONTEXT_combin", ``!c1 c2. GCONTEXT c1 /\ GCONTEXT c2 ==> GCONTEXT (c1 o c2)``, 391 REPEAT STRIP_TAC 392 >> NTAC 2 (POP_ASSUM MP_TAC) 393 >> Q.SPEC_TAC (`c1`, `c`) 394 >> HO_MATCH_MP_TAC GCONTEXT_ind 395 >> REWRITE_TAC [o_DEF] 396 >> BETA_TAC 397 >> REWRITE_TAC [ETA_AX] 398 >> rpt STRIP_TAC (* 6 sub-goals here *) 399 >| [ REWRITE_TAC [GCONTEXT2], 400 FULL_SIMP_TAC std_ss [GCONTEXT3], 401 FULL_SIMP_TAC std_ss [GCONTEXT4], 402 FULL_SIMP_TAC std_ss [GCONTEXT5], 403 FULL_SIMP_TAC std_ss [GCONTEXT6], 404 FULL_SIMP_TAC std_ss [GCONTEXT7] ]); 405 406val GCONTEXT_IMP_CONTEXT = store_thm ( 407 "GCONTEXT_IMP_CONTEXT", ``!c. GCONTEXT c ==> CONTEXT c``, 408 Induct_on `GCONTEXT` 409 >> rpt STRIP_TAC (* 7 sub-goals here *) 410 >| [ (* goal 1 (of 7) *) 411 REWRITE_TAC [CONTEXT1], 412 (* goal 2 (of 7) *) 413 REWRITE_TAC [CONTEXT2], 414 (* goal 3 (of 7) *) 415 MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [], 416 (* goal 4 (of 7) *) 417 Know `CONTEXT (\t. (prefix a1 (e1 t)))` 418 >- ( MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [] ) \\ 419 Know `CONTEXT (\t. (prefix a2 (e2 t)))` 420 >- ( MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [] ) \\ 421 KILL_TAC \\ 422 NTAC 2 DISCH_TAC \\ 423 Know `CONTEXT (\t. (\t. (prefix a1 (e1 t))) t + (\t. (prefix a2 (e2 t))) t)` 424 >- ( MATCH_MP_TAC CONTEXT4 >> ASM_REWRITE_TAC [] ) \\ 425 BETA_TAC >> REWRITE_TAC [], 426 (* goal 5 (of 7) *) 427 MATCH_MP_TAC CONTEXT5 >> ASM_REWRITE_TAC [], 428 (* goal 6 (of 7) *) 429 MATCH_MP_TAC CONTEXT6 >> ASM_REWRITE_TAC [], 430 (* goal 7 (of 7) *) 431 MATCH_MP_TAC CONTEXT7 >> ASM_REWRITE_TAC [] ]); 432 433val WEAK_EQUIV_SUBST_GCONTEXT = store_thm ( 434 "WEAK_EQUIV_SUBST_GCONTEXT", 435 ``!P Q. WEAK_EQUIV P Q ==> !E. GCONTEXT E ==> WEAK_EQUIV (E P) (E Q)``, 436 rpt GEN_TAC >> DISCH_TAC 437 >> Induct_on `GCONTEXT` 438 >> BETA_TAC >> rpt STRIP_TAC (* 7 sub-goals here *) 439 >- ASM_REWRITE_TAC [] 440 >- REWRITE_TAC [WEAK_EQUIV_REFL] 441 >| [ (* goal 1 (of 5) *) 442 MATCH_MP_TAC WEAK_EQUIV_SUBST_PREFIX >> ASM_REWRITE_TAC [], 443 (* goal 2 (of 5) *) 444 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_GUARDED_SUM \\ 445 ASM_REWRITE_TAC [], 446 (* goal 3 (of 5) *) 447 IMP_RES_TAC WEAK_EQUIV_PRESD_BY_PAR, 448 (* goal 4 (of 5) *) 449 MATCH_MP_TAC WEAK_EQUIV_SUBST_RESTR >> ASM_REWRITE_TAC [], 450 (* goal 5 (of 5) *) 451 MATCH_MP_TAC WEAK_EQUIV_SUBST_RELAB >> ASM_REWRITE_TAC [] ]); 452 453(******************************************************************************) 454(* *) 455(* congruence and precongruence *) 456(* *) 457(******************************************************************************) 458 459Definition precongruence : 460 precongruence R = PreOrder R /\ 461 !x y ctx. CONTEXT ctx ==> R x y ==> R (ctx x) (ctx y) 462End 463 464(* a special version of precongruence with only guarded sums *) 465Definition precongruence' : 466 precongruence' R = PreOrder R /\ 467 !x y ctx. GCONTEXT ctx ==> R x y ==> R (ctx x) (ctx y) 468End 469 470(* The definition of congruence for CCS, TODO: use precongruence *) 471Definition congruence : 472 congruence R = equivalence R /\ 473 !x y ctx. CONTEXT ctx ==> R x y ==> R (ctx x) (ctx y) 474End 475 476(* a special version of congruence with only guarded sums *) 477Definition congruence' : 478 congruence' R = equivalence R /\ 479 !x y ctx. GCONTEXT ctx ==> R x y ==> R (ctx x) (ctx y) 480End 481 482val STRONG_EQUIV_congruence = store_thm ( 483 "STRONG_EQUIV_congruence", ``congruence STRONG_EQUIV``, 484 REWRITE_TAC [congruence, STRONG_EQUIV_equivalence] 485 >> PROVE_TAC [STRONG_EQUIV_SUBST_CONTEXT]); 486 487val WEAK_EQUIV_congruence = store_thm ( 488 "WEAK_EQUIV_congruence", ``congruence' WEAK_EQUIV``, 489 REWRITE_TAC [congruence', WEAK_EQUIV_equivalence] 490 >> PROVE_TAC [WEAK_EQUIV_SUBST_GCONTEXT]); 491 492val OBS_CONGR_congruence = store_thm ( 493 "OBS_CONGR_congruence", ``congruence OBS_CONGR``, 494 REWRITE_TAC [congruence, OBS_CONGR_equivalence] 495 >> PROVE_TAC [OBS_CONGR_SUBST_CONTEXT]); 496 497(* Building (pre)congruence closure from any relation on CCS *) 498val CC_def = Define ` 499 CC R = (\g h. !c. CONTEXT c ==> R (c g) (c h))`; 500 501val GCC_def = Define ` 502 GCC R = (\g h. !c. GCONTEXT c ==> R (c g) (c h))`; 503 504val CC_precongruence = store_thm ( 505 "CC_precongruence", ``!R. PreOrder R ==> precongruence (CC R)``, 506 REWRITE_TAC [precongruence, CC_def] 507 >> RW_TAC std_ss [] 508 >| [ (* goal 1 (of 2) *) 509 REWRITE_TAC [PreOrder] \\ 510 rpt STRIP_TAC >| (* 2 sub-goals here *) 511 [ (* goal 1.1 (of 2) *) 512 REWRITE_TAC [reflexive_def] >> BETA_TAC \\ 513 rpt STRIP_TAC \\ 514 PROVE_TAC [PreOrder, reflexive_def], 515 (* goal 1.2 (of 2) *) 516 REWRITE_TAC [transitive_def] >> BETA_TAC \\ 517 rpt STRIP_TAC >> RES_TAC \\ 518 PROVE_TAC [PreOrder, transitive_def] ], 519 (* goal 2 (of 2) *) 520 `CONTEXT (c o ctx)` by PROVE_TAC [CONTEXT_combin] \\ 521 RES_TAC >> FULL_SIMP_TAC std_ss [o_THM] ]); 522 523(* The built relation is indeed congruence *) 524val CC_congruence = store_thm ( 525 "CC_congruence", ``!R. equivalence R ==> congruence (CC R)``, 526 REWRITE_TAC [congruence, CC_def] 527 >> RW_TAC std_ss [] (* 2 sub-goals here *) 528 >| [ (* goal 1 (of 2) *) 529 REWRITE_TAC [equivalence_def] \\ 530 rpt STRIP_TAC >| (* 3 sub-goals here *) 531 [ (* goal 1.1 (of 3) *) 532 REWRITE_TAC [reflexive_def] >> BETA_TAC \\ 533 rpt STRIP_TAC \\ 534 PROVE_TAC [equivalence_def, reflexive_def], 535 (* goal 1.2 (of 3) *) 536 REWRITE_TAC [symmetric_def] >> BETA_TAC \\ 537 rpt GEN_TAC >> EQ_TAC >> rpt STRIP_TAC >> RES_TAC \\ (* 2 sub-goals here *) 538 PROVE_TAC [equivalence_def, symmetric_def], 539 (* goal 1.3 (of 3) *) 540 REWRITE_TAC [transitive_def] >> BETA_TAC \\ 541 rpt STRIP_TAC >> RES_TAC \\ 542 PROVE_TAC [equivalence_def, transitive_def] ], 543 (* goal 2 (of 2) *) 544 `CONTEXT (c o ctx)` by PROVE_TAC [CONTEXT_combin] \\ 545 RES_TAC >> FULL_SIMP_TAC std_ss [o_THM] ]); 546 547(* The congruence is finer than original relation *) 548val CC_is_finer = store_thm ( 549 "CC_is_finer", ``!R. (CC R) RSUBSET R``, 550 REWRITE_TAC [RSUBSET] 551 >> REPEAT GEN_TAC 552 >> REWRITE_TAC [CC_def] 553 >> BETA_TAC 554 >> REPEAT STRIP_TAC 555 >> `CONTEXT (\x. x)` by PROVE_TAC [CONTEXT_rules] 556 >> RES_TAC 557 >> POP_ASSUM (ACCEPT_TAC o BETA_RULE)); 558 559(* The congruence built by above method is the coarsest congruence contained in R *) 560val CC_is_coarsest = store_thm ( 561 "CC_is_coarsest", 562 ``!R R'. congruence R' /\ R' RSUBSET R ==> R' RSUBSET (CC R)``, 563 REWRITE_TAC [congruence, RSUBSET, CC_def] 564 >> RW_TAC std_ss []); 565 566Theorem PCC_is_coarsest : 567 !R R'. precongruence R' /\ R' RSUBSET R ==> R' RSUBSET (CC R) 568Proof 569 REWRITE_TAC [precongruence, RSUBSET, CC_def] 570 >> RW_TAC std_ss [] 571QED 572 573(******************************************************************************) 574(* *) 575(* Weakly guarded (WG) expressions *) 576(* *) 577(******************************************************************************) 578 579Inductive WG : 580 (!p. WG (\t. p)) /\ (* WG2 *) 581 (!a e. CONTEXT e ==> WG (\t. prefix a (e t))) /\ (* WG3 *) 582 (!e1 e2. WG e1 /\ WG e2 ==> WG (\t. sum (e1 t) (e2 t))) /\ (* WG4 *) 583 (!e1 e2. WG e1 /\ WG e2 ==> WG (\t. par (e1 t) (e2 t))) /\ (* WG5 *) 584 (!L e. WG e ==> WG (\t. restr L (e t))) /\ (* WG6 *) 585 (!rf e. WG e ==> WG (\t. relab (e t) rf)) (* WG7 *) 586End 587 588val [WG2, WG3, WG4, WG5, WG6, WG7] = 589 map save_thm 590 (combine (["WG2", "WG3", "WG4", "WG5", "WG6", "WG7"], CONJUNCTS WG_rules)); 591 592Theorem WG1 : (* WG1 is derivable from WG3 *) 593 !a :'b Action. WG (\t. prefix a t) 594Proof 595 ASSUME_TAC CONTEXT1 596 >> IMP_RES_TAC WG3 597 >> POP_ASSUM MP_TAC 598 >> BETA_TAC >> art [] 599QED 600 601Theorem NO_WG0 : 602 ~WG (\t. t) 603Proof 604 ONCE_REWRITE_TAC [WG_cases] >> rpt STRIP_TAC (* 6 subgoals *) 605 >- (fs [FUN_EQ_THM] \\ 606 STRIP_ASSUME_TAC (Q.SPEC `p` CCS_distinct_exists) >> METIS_TAC []) 607 >> fs [FUN_EQ_THM] 608 >> Q.PAT_X_ASSUM `!t. t = X` (ASSUME_TAC o (Q.SPEC `nil`)) 609 >> fs [CCS_distinct] 610QED 611 612Theorem WG_CONST : 613 !e. IS_CONST e ==> WG e 614Proof 615 RW_TAC std_ss [IS_CONST_def] 616 >> Know `e = (\t. e nil)` >- fs [FUN_EQ_THM] 617 >> Rewr' >> REWRITE_TAC [WG2] 618QED 619 620Theorem NO_WG8 : 621 !e X. ~IS_CONST e ==> ~WG (\t. rec X (e t)) 622Proof 623 rpt GEN_TAC >> ONCE_REWRITE_TAC [WG_cases] 624 >> fs [FUN_EQ_THM, IS_CONST_def] 625 >> rpt STRIP_TAC 626 >> Cases_on `p` >> fs [FUN_EQ_THM] 627 >> METIS_TAC [] 628QED 629 630Theorem WG8_IMP_CONST : 631 !e X. WG (\t. rec X (e t)) ==> IS_CONST e 632Proof 633 METIS_TAC [NO_WG8] 634QED 635 636Theorem WG3_backward : 637 !e u. WG (\t. prefix u (e t)) ==> CONTEXT e 638Proof 639 rpt GEN_TAC 640 >> ONCE_REWRITE_TAC [WG_cases] 641 >> RW_TAC std_ss [FUN_EQ_THM] (* 2 subgoals left *) 642 >| [ (* goal 1 (of 2) *) 643 Cases_on `p` (* 8 sub-goals here *) 644 >- PROVE_TAC [CCS_distinct] 645 >- PROVE_TAC [CCS_distinct] 646 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 647 rename1 `!t. (u = o') /\ (e t = C')` \\ 648 `(e = \t. C')` by PROVE_TAC [] >> art [CONTEXT2]) 649 >> PROVE_TAC [CCS_distinct], 650 (* goal 2 (of 2) *) 651 METIS_TAC [] ] 652QED 653 654Theorem WG4_backward : 655 !e e'. WG (\t. sum (e t) (e' t)) ==> WG e /\ WG e' 656Proof 657 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 658 ( POP_ASSUM (STRIP_ASSUME_TAC o 659 (ONCE_REWRITE_RULE [WG_cases])) (* 6 sub-goals here *) 660 >| [ (* goal 1 (of 6) *) 661 fs [FUN_EQ_THM] \\ 662 Cases_on `p` (* 8 sub-goals here *) 663 >- PROVE_TAC [CCS_distinct] 664 >- PROVE_TAC [CCS_distinct] 665 >- PROVE_TAC [CCS_distinct] 666 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 667 rename1 `!t. (e t = C') /\ (e' t = C0)` \\ 668 `(e = \t. C') /\ (e' = \t. C0)` by PROVE_TAC [] \\ 669 ASM_REWRITE_TAC [WG2]) 670 >> PROVE_TAC [CCS_distinct], 671 (* goal 2 (of 6) *) 672 fs [FUN_EQ_THM], 673 (* goal 3 (of 6) *) 674 fs [FUN_EQ_THM] >> METIS_TAC [], 675 (* goal 4 (of 6) *) 676 fs [FUN_EQ_THM], 677 (* goal 5 (of 6) *) 678 fs [FUN_EQ_THM], 679 (* goal 6 (of 6) *) 680 fs [FUN_EQ_THM] ] ) 681QED 682 683Theorem WG5_backward : 684 !e e'. WG (\t. par (e t) (e' t)) ==> WG e /\ WG e' 685Proof 686 rpt STRIP_TAC \\ (* 2 subgoals here, same tacticals *) 687 ( POP_ASSUM (STRIP_ASSUME_TAC o 688 (ONCE_REWRITE_RULE [WG_cases])) \\ (* 6 subgoals here *) 689 fs [FUN_EQ_THM] (* 2 subgoals left *) 690 >| [ (* goal 1 (of 2) *) 691 Cases_on `p` (* 8 sub-goals here *) 692 >- PROVE_TAC [CCS_distinct] 693 >- PROVE_TAC [CCS_distinct] 694 >- PROVE_TAC [CCS_distinct] 695 >- PROVE_TAC [CCS_distinct] 696 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 697 rename1 `!t. (e t = C') /\ (e' t = C0)` \\ 698 `(e = \t. C') /\ (e' = \t. C0)` by PROVE_TAC [] \\ 699 ASM_REWRITE_TAC [WG2]) 700 >> PROVE_TAC [CCS_distinct], 701 (* goal 2 (of 2) *) 702 METIS_TAC [] ] ) 703QED 704 705Theorem WG6_backward : 706 !e L. WG (\t. restr L (e t)) ==> WG e 707Proof 708 rpt STRIP_TAC 709 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WG_cases])) 710 >> fs [FUN_EQ_THM] (* 2 subgoals left *) 711 >| [ (* goal 1 (of 2) *) 712 Cases_on `p` (* 8 sub-goals here *) 713 >- PROVE_TAC [CCS_distinct] 714 >- PROVE_TAC [CCS_distinct] 715 >- PROVE_TAC [CCS_distinct] 716 >- PROVE_TAC [CCS_distinct] 717 >- PROVE_TAC [CCS_distinct] 718 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 719 rename1 `!t. (L = f) /\ (e t = C')` \\ 720 `(e = \t. C')` by PROVE_TAC [] >> art [WG2]) 721 >> PROVE_TAC [CCS_distinct], 722 (* goal 2 (of 2) *) 723 METIS_TAC [] ] 724QED 725 726Theorem WG7_backward : 727 !e rf. WG (\t. relab (e t) rf) ==> WG e 728Proof 729 rpt STRIP_TAC 730 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [WG_cases])) 731 >> fs [FUN_EQ_THM] 732 >| [ (* goal 1 (of 2) *) 733 Cases_on `p` (* 8 sub-goals here *) 734 >- PROVE_TAC [CCS_distinct] 735 >- PROVE_TAC [CCS_distinct] 736 >- PROVE_TAC [CCS_distinct] 737 >- PROVE_TAC [CCS_distinct] 738 >- PROVE_TAC [CCS_distinct] 739 >- PROVE_TAC [CCS_distinct] 740 >- (FULL_SIMP_TAC std_ss [CCS_11] \\ 741 rename1 `!t. (e t = C') /\ (rf = R)` \\ 742 `(e = \t. C')` by PROVE_TAC [] >> art [WG2]) 743 >> PROVE_TAC [CCS_distinct], 744 (* goal 2 (of 2) *) 745 METIS_TAC [] ] 746QED 747 748Theorem WG8_backward : 749 !e X. WG (\t. rec X (e t)) ==> WG e 750Proof 751 rpt STRIP_TAC 752 >> MATCH_MP_TAC WG_CONST 753 >> MATCH_MP_TAC WG8_IMP_CONST 754 >> Q.EXISTS_TAC `X` >> art [] 755QED 756 757(* Weakly guarded expressions are also expressions *) 758val WG_IMP_CONTEXT = store_thm ( 759 "WG_IMP_CONTEXT", ``!e. WG e ==> CONTEXT e``, 760 Induct_on `WG` 761 >> rpt STRIP_TAC (* 6 sub-goals here *) 762 >| [ REWRITE_TAC [CONTEXT2], 763 MATCH_MP_TAC CONTEXT3 >> art [], 764 MATCH_MP_TAC CONTEXT4 >> art [], 765 MATCH_MP_TAC CONTEXT5 >> art [], 766 MATCH_MP_TAC CONTEXT6 >> art [], 767 MATCH_MP_TAC CONTEXT7 >> art [] ]); 768 769val CONTEXT_WG_combin = store_thm ( 770 "CONTEXT_WG_combin", ``!c e. CONTEXT c /\ WG e ==> WG (c o e)``, 771 rpt STRIP_TAC 772 >> NTAC 2 (POP_ASSUM MP_TAC) 773 >> Q.SPEC_TAC (`c`, `c`) 774 >> HO_MATCH_MP_TAC CONTEXT_ind 775 >> REWRITE_TAC [o_DEF] 776 >> BETA_TAC 777 >> REWRITE_TAC [ETA_AX] 778 >> rpt STRIP_TAC >> RES_TAC (* 6 sub-goals here *) 779 >| [ (* goal 1 (of 6) *) 780 REWRITE_TAC [WG2], 781 (* goal 2 (of 6) *) 782 IMP_RES_TAC WG_IMP_CONTEXT \\ 783 MP_TAC (Q.SPECL [`a`, `(\x. (c :('a, 'b) context) (e x))`] WG3) \\ 784 BETA_TAC >> RW_TAC std_ss [], 785 (* goal 3 (of 6) *) 786 MP_TAC (Q.SPECL [`(\x. (c :('a, 'b) context) (e x))`, 787 `(\x. (c' :('a, 'b) context) (e x))`] WG4) \\ 788 BETA_TAC >> RW_TAC std_ss [], 789 (* goal 4 (of 6) *) 790 MP_TAC (Q.SPECL [`(\x. (c :('a, 'b) context) (e x))`, 791 `(\x. (c' :('a, 'b) context) (e x))`] WG5) \\ 792 BETA_TAC >> RW_TAC std_ss [], 793 (* goal 5 (of 6) *) 794 MP_TAC (Q.SPECL [`L`, `(\x. (c :('a, 'b) context) (e x))`] WG6) \\ 795 BETA_TAC >> RW_TAC std_ss [], 796 (* goal 6 (of 6) *) 797 MP_TAC (Q.SPECL [`rf`, `(\x. (c :('a, 'b) context) (e x))`] WG7) \\ 798 BETA_TAC >> RW_TAC std_ss [] ]); 799 800(******************************************************************************) 801(* *) 802(* Strongly guarded (SG) expressions *) 803(* *) 804(******************************************************************************) 805 806(* X is guarded in E if each occurrence of X is within some subexpression of E of 807 the form l.F *) 808Inductive SG : 809 (!p. SG (\t. p)) /\ (* SG1 *) 810 (!l e. CONTEXT e ==> SG (\t. prefix (label l) (e t))) /\ (* SG2 *) 811 (!a e. SG e ==> SG (\t. prefix a (e t))) /\ (* SG3 *) 812 (!e1 e2. SG e1 /\ SG e2 ==> SG (\t. sum (e1 t) (e2 t))) /\ (* SG4 *) 813 (!e1 e2. SG e1 /\ SG e2 ==> SG (\t. par (e1 t) (e2 t))) /\ (* SG5 *) 814 (!L e. SG e ==> SG (\t. restr L (e t))) /\ (* SG6 *) 815 (!rf e. SG e ==> SG (\t. relab (e t) rf)) (* SG7 *) 816End 817 818val [SG1, SG2, SG3, SG4, SG5, SG6, SG7] = 819 map save_thm 820 (combine (["SG1", "SG2", "SG3", "SG4", "SG5", "SG6", "SG7"], 821 CONJUNCTS SG_rules)); 822 823(* Strongly guarded expressions are expressions *) 824val SG_IMP_CONTEXT = store_thm ( 825 "SG_IMP_CONTEXT", ``!e. SG e ==> CONTEXT e``, 826 Induct_on `SG` 827 >> rpt STRIP_TAC (* 7 sub-goals here *) 828 >| [ REWRITE_TAC [CONTEXT2], 829 MATCH_MP_TAC CONTEXT3 >> art [], 830 MATCH_MP_TAC CONTEXT3 >> art [], 831 MATCH_MP_TAC CONTEXT4 >> art [], 832 MATCH_MP_TAC CONTEXT5 >> art [], 833 MATCH_MP_TAC CONTEXT6 >> art [], 834 MATCH_MP_TAC CONTEXT7 >> art [] ]); 835 836(* Strong guardness implies weak guardness *) 837val SG_IMP_WG = store_thm ( 838 "SG_IMP_WG", ``!e. SG e ==> WG e``, 839 Induct_on `SG` 840 >> rpt STRIP_TAC (* 7 sub-goals here *) 841 >| [ REWRITE_TAC [WG2], 842 MATCH_MP_TAC WG3 >> art [], 843 MATCH_MP_TAC WG3 >> IMP_RES_TAC SG_IMP_CONTEXT, 844 MATCH_MP_TAC WG4 >> art [], 845 MATCH_MP_TAC WG5 >> art [], 846 MATCH_MP_TAC WG6 >> art [], 847 MATCH_MP_TAC WG7 >> art [] ]); 848 849val lemma = Q.prove (`!p :('a, 'b) CCS. ?q. q <> p`, 850 Cases_on `p` 851 >- ( Q.EXISTS_TAC `nil + nil` >> PROVE_TAC [CCS_distinct'] ) 852 >> ( Q.EXISTS_TAC `nil` >> PROVE_TAC [CCS_distinct'] )); 853 854(* an important backward property of SG *) 855Theorem SG3_backward : 856 !e. SG (\t. prefix tau (e t)) ==> SG e 857Proof 858 rpt STRIP_TAC 859 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 860 >| [ (* goal 1 (of 7) *) 861 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 862 Cases_on `p` (* 8 or 9 sub-goals here *) 863 >- PROVE_TAC [CCS_distinct'] 864 >- PROVE_TAC [CCS_distinct'] 865 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 866 `(e = \t. C') \/ (e = \t. C)` by PROVE_TAC [] \\ (* 2 sub-goals *) 867 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 868 >> PROVE_TAC [CCS_distinct'], 869 (* goal 2 (of 7) *) 870 qpat_x_assum `(\t. prefix tau (e t)) = X` 871 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 872 PROVE_TAC [CCS_11, Action_distinct], 873 (* goal 3 (of 7) *) 874 qpat_x_assum `(\t. prefix tau (e t)) = X` 875 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 876 FULL_SIMP_TAC std_ss [CCS_11] \\ 877 METIS_TAC [], 878 (* goal 4 (of 7) *) 879 qpat_x_assum `(\t. prefix tau (e t)) = X` 880 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 881 PROVE_TAC [CCS_distinct'], 882 (* goal 5 (of 7) *) 883 qpat_x_assum `(\t. prefix tau (e t)) = X` 884 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 885 PROVE_TAC [CCS_distinct'], 886 (* goal 6 (of 7) *) 887 qpat_x_assum `(\t. prefix tau (e t)) = X` 888 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 889 PROVE_TAC [CCS_distinct'], 890 (* goal 7 (of 7) *) 891 qpat_x_assum `(\t. prefix tau (e t)) = X` 892 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 893 PROVE_TAC [CCS_distinct'] ] 894QED 895 896(* another important backward property of SG *) 897Theorem SG4_backward : 898 !e e'. SG (\t. sum (e t) (e' t)) ==> SG e /\ SG e' 899Proof 900 rpt STRIP_TAC \\ (* 2 sub-goals here, same tacticals *) 901 ( POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 902 >| [ (* goal 1 (of 7) *) 903 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 904 Cases_on `p` (* 8 or 9 sub-goals here *) 905 >- PROVE_TAC [CCS_distinct] 906 >- PROVE_TAC [CCS_distinct] 907 >- PROVE_TAC [CCS_distinct] 908 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 909 `((e = \t. C) \/ (e = \t. C')) /\ (e' = \t. C0)` by PROVE_TAC [] \\ 910 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 911 >> PROVE_TAC [CCS_distinct], 912 (* goal 2 (of 7) *) 913 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 914 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 915 PROVE_TAC [CCS_distinct'], 916 (* goal 3 (of 7) *) 917 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 918 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 919 PROVE_TAC [CCS_distinct'], 920 (* goal 4 (of 7) *) 921 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 922 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 923 FULL_SIMP_TAC std_ss [CCS_11] \\ 924 METIS_TAC [], 925 (* goal 5 (of 7) *) 926 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 927 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 928 PROVE_TAC [CCS_distinct'], 929 (* goal 6 (of 7) *) 930 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 931 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 932 PROVE_TAC [CCS_distinct'], 933 (* goal 7 (of 7) *) 934 qpat_x_assum `(\t. sum (e t) (e' t)) = X` 935 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 936 PROVE_TAC [CCS_distinct'] ] ) 937QED 938 939val SG10 = store_thm ("SG10", 940 ``!e e'. SG (\t. sum (prefix tau (e t)) (prefix tau (e' t))) ==> SG e /\ SG e'``, 941 rpt STRIP_TAC 942 >| [ (* goal 1 (of 2) *) 943 POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) >| (* 7 sub-goals here *) 944 [ (* goal 1.1 (of 7) *) 945 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 946 Cases_on `p` (* 8 or 9 sub-goals here *) 947 >- PROVE_TAC [CCS_distinct] 948 >- PROVE_TAC [CCS_distinct] 949 >- PROVE_TAC [CCS_distinct] 950 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 951 (TRY (Cases_on `C'`) >> TRY (Cases_on `C`)) (* 8 or 9 sub-goals here *) 952 >- PROVE_TAC [CCS_distinct] 953 >- PROVE_TAC [CCS_distinct] 954 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 955 `(e = \t. C'') \/ (e = \t. C')` by PROVE_TAC [] \\ 956 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 957 >> PROVE_TAC [CCS_distinct] ) 958 >> PROVE_TAC [CCS_distinct], 959 (* goal 1.2 (of 7) *) 960 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 961 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 962 PROVE_TAC [CCS_distinct'], 963 (* goal 1.3 (of 7) *) 964 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 965 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 966 PROVE_TAC [CCS_distinct'], 967 (* goal 1.4 (of 7) *) 968 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 969 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 970 FULL_SIMP_TAC std_ss [CCS_11] \\ 971 `e1 = \t. prefix tau (e t)` by PROVE_TAC [] \\ 972 FULL_SIMP_TAC std_ss [] \\ 973 IMP_RES_TAC SG3_backward, 974 (* goal 1.5 (of 7) *) 975 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 976 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 977 PROVE_TAC [CCS_distinct'], 978 (* goal 1.6 (of 7) *) 979 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 980 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 981 PROVE_TAC [CCS_distinct'], 982 (* goal 1.7 (of 7) *) 983 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 984 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 985 PROVE_TAC [CCS_distinct'] ], 986 (* goal 2 (of 2) *) 987 POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) >| (* 7 sub-goals here *) 988 [ (* goal 1.1 (of 7) *) 989 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 990 Cases_on `p` (* 8 or 9 sub-goals here *) 991 >- PROVE_TAC [CCS_distinct] 992 >- PROVE_TAC [CCS_distinct] 993 >- PROVE_TAC [CCS_distinct] 994 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 995 Cases_on `C0` (* 8 or 9 sub-goals here *) 996 >- PROVE_TAC [CCS_distinct] 997 >- PROVE_TAC [CCS_distinct] 998 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 999 `(e' = \t. C'') \/ (e' = \t. C')` by PROVE_TAC [] \\ 1000 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 1001 >> PROVE_TAC [CCS_distinct] ) 1002 >> PROVE_TAC [CCS_distinct], 1003 (* goal 1.2 (of 7) *) 1004 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1005 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1006 PROVE_TAC [CCS_distinct'], 1007 (* goal 1.3 (of 7) *) 1008 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1009 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1010 PROVE_TAC [CCS_distinct'], 1011 (* goal 1.4 (of 7) *) 1012 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1013 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1014 FULL_SIMP_TAC std_ss [CCS_11] \\ 1015 `e2 = \t. prefix tau (e' t)` by PROVE_TAC [] \\ 1016 FULL_SIMP_TAC std_ss [] \\ 1017 IMP_RES_TAC SG3_backward, 1018 (* goal 1.5 (of 7) *) 1019 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1020 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1021 PROVE_TAC [CCS_distinct'], 1022 (* goal 1.6 (of 7) *) 1023 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1024 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1025 PROVE_TAC [CCS_distinct'], 1026 (* goal 1.7 (of 7) *) 1027 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix tau (e' t))) = X` 1028 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1029 PROVE_TAC [CCS_distinct'] ]]); 1030 1031val SG11 = store_thm ("SG11", 1032 ``!e e' L. SG (\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) ==> SG e``, 1033 rpt STRIP_TAC 1034 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 1035 >| [ (* goal 1 (of 7) *) 1036 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 1037 Cases_on `p` (* 8 or 9 sub-goals here *) 1038 >- PROVE_TAC [CCS_distinct] 1039 >- PROVE_TAC [CCS_distinct] 1040 >- PROVE_TAC [CCS_distinct] 1041 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 1042 (TRY (Cases_on `C'`) >> TRY (Cases_on `C`)) (* 8 or 9 sub-goals here *) 1043 >- PROVE_TAC [CCS_distinct] 1044 >- PROVE_TAC [CCS_distinct] 1045 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 1046 `(e = \t. C'') \/ (e = \t. C')` by PROVE_TAC [] \\ 1047 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 1048 >> PROVE_TAC [CCS_distinct] ) 1049 >> PROVE_TAC [CCS_distinct], 1050 (* goal 2 (of 7) *) 1051 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1052 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1053 PROVE_TAC [CCS_distinct'], 1054 (* goal 3 (of 7) *) 1055 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1056 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1057 PROVE_TAC [CCS_distinct'], 1058 (* goal 4 (of 7) *) 1059 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1060 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1061 FULL_SIMP_TAC std_ss [CCS_11] \\ 1062 `e1 = \t. prefix tau (e t)` by PROVE_TAC [] \\ 1063 FULL_SIMP_TAC std_ss [] \\ 1064 IMP_RES_TAC SG3_backward, 1065 (* goal 5 (of 7) *) 1066 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1067 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1068 PROVE_TAC [CCS_distinct'], 1069 (* goal 6 (of 7) *) 1070 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1071 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1072 PROVE_TAC [CCS_distinct'], 1073 (* goal 7 (of 7) *) 1074 qpat_x_assum `(\t. sum (prefix tau (e t)) (prefix (label L) (e' t))) = X` 1075 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1076 PROVE_TAC [CCS_distinct'] ]); 1077 1078val SG11' = store_thm ("SG11'", 1079 ``!e e' L. SG (\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) ==> SG e'``, 1080 rpt STRIP_TAC 1081 >> POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 1082 >| [ (* goal 1 (of 7) *) 1083 POP_ASSUM (ASSUME_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 1084 Cases_on `p` (* 8 or 9 sub-goals here *) 1085 >- PROVE_TAC [CCS_distinct] 1086 >- PROVE_TAC [CCS_distinct] 1087 >- PROVE_TAC [CCS_distinct] 1088 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 1089 Cases_on `C0` (* 8 or 9 sub-goals here *) 1090 >- PROVE_TAC [CCS_distinct] 1091 >- PROVE_TAC [CCS_distinct] 1092 >- ( FULL_SIMP_TAC std_ss [CCS_11] \\ 1093 `(e' = \t. C'') \/ (e' = \t. C')` by PROVE_TAC [] \\ 1094 ASM_REWRITE_TAC [] >> REWRITE_TAC [SG1] ) 1095 >> PROVE_TAC [CCS_distinct] ) 1096 >> PROVE_TAC [CCS_distinct], 1097 (* goal 2 (of 7) *) 1098 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1099 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1100 PROVE_TAC [CCS_distinct'], 1101 (* goal 3 (of 7) *) 1102 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1103 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1104 PROVE_TAC [CCS_distinct'], 1105 (* goal 4 (of 7) *) 1106 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1107 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1108 FULL_SIMP_TAC std_ss [CCS_11] \\ 1109 `e2 = \t. prefix tau (e' t)` by PROVE_TAC [] \\ 1110 FULL_SIMP_TAC std_ss [] \\ 1111 IMP_RES_TAC SG3_backward, 1112 (* goal 5 (of 7) *) 1113 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1114 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1115 PROVE_TAC [CCS_distinct'], 1116 (* goal 6 (of 7) *) 1117 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1118 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1119 PROVE_TAC [CCS_distinct'], 1120 (* goal 7 (of 7) *) 1121 qpat_x_assum `(\t. sum (prefix (label L) (e t)) (prefix tau (e' t))) = X` 1122 (ASSUME_TAC o BETA_RULE o (REWRITE_RULE [FUN_EQ_THM])) \\ 1123 PROVE_TAC [CCS_distinct'] ]); 1124 1125(******************************************************************************) 1126(* *) 1127(* Sequential (SEQ) expressions *) 1128(* *) 1129(******************************************************************************) 1130 1131(* X is sequential in E if every subexpression of E which contains X, apart from 1132 X itself, is of the form a.F or Sigma F_i *) 1133Inductive SEQ : 1134 ( SEQ (\t. t)) /\ (* SEQ1 *) 1135 (!p. SEQ (\t. p)) /\ (* SEQ2 *) 1136 (!a e. SEQ e ==> SEQ (\t. prefix a (e t))) /\ (* SEQ3 *) 1137 (!e1 e2. SEQ e1 /\ SEQ e2 ==> SEQ (\t. sum (e1 t) (e2 t))) (* SEQ4 *) 1138End 1139 1140val [SEQ1, SEQ2, SEQ3, SEQ4] = 1141 map save_thm (combine (["SEQ1", "SEQ2", "SEQ3", "SEQ4"], CONJUNCTS SEQ_rules)); 1142 1143val SEQ3a = store_thm ("SEQ3a", 1144 ``!a :'b Action. SEQ (\t. prefix a t)``, 1145 ASSUME_TAC SEQ1 1146 >> IMP_RES_TAC SEQ3 1147 >> POP_ASSUM MP_TAC 1148 >> BETA_TAC >> REWRITE_TAC []); 1149 1150val SEQ_IMP_CONTEXT = store_thm ( 1151 "SEQ_IMP_CONTEXT", ``!e. SEQ e ==> CONTEXT e``, 1152 Induct_on `SEQ` 1153 >> rpt STRIP_TAC (* 4 sub-goals here *) 1154 >| [ REWRITE_TAC [CONTEXT1], 1155 REWRITE_TAC [CONTEXT2], 1156 MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [], 1157 MATCH_MP_TAC CONTEXT4 >> ASM_REWRITE_TAC [] ]); 1158 1159val SEQ_combin = store_thm ( 1160 "SEQ_combin", ``!E. SEQ E ==> !E'. SEQ E' ==> SEQ (E o E')``, 1161 Induct_on `SEQ` 1162 >> REWRITE_TAC [o_DEF] >> BETA_TAC 1163 >> REWRITE_TAC [ETA_THM] 1164 >> rpt STRIP_TAC (* 3 sub-goals here *) 1165 >| [ (* goal 1 (of 3) *) 1166 REWRITE_TAC [SEQ2], 1167 (* goal 2 (of 3) *) 1168 RES_TAC >> IMP_RES_TAC SEQ3 \\ 1169 NTAC 2 (POP_ASSUM K_TAC) \\ 1170 POP_ASSUM (MP_TAC o (Q.SPEC `a`)) \\ 1171 KILL_TAC \\ 1172 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1173 (* goal 3 (of 3) *) 1174 `SEQ (\x. E (E'' x)) /\ SEQ (\x. E' (E'' x))` by METIS_TAC [] \\ 1175 METIS_TAC [SEQ4] ]); 1176 1177val OBS_CONGR_SUBST_SEQ = store_thm ( 1178 "OBS_CONGR_SUBST_SEQ", 1179 ``!P Q. OBS_CONGR P Q ==> !E. SEQ E ==> OBS_CONGR (E P) (E Q)``, 1180 rpt GEN_TAC >> DISCH_TAC 1181 >> Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 1182 >- ASM_REWRITE_TAC [] 1183 >- REWRITE_TAC [OBS_CONGR_REFL] 1184 >| [ (* goal 1 (of 2) *) 1185 MATCH_MP_TAC OBS_CONGR_SUBST_PREFIX \\ 1186 ASM_REWRITE_TAC [], 1187 (* goal 2 (of 2) *) 1188 IMP_RES_TAC OBS_CONGR_PRESD_BY_SUM ]); 1189 1190(* Sequential expression with guarded sums *) 1191Inductive GSEQ : 1192 ( GSEQ (\t. t)) /\ (* GSEQ1 *) 1193 (!p. GSEQ (\t. p)) /\ (* GSEQ2 *) 1194 (!a e. GSEQ e ==> GSEQ (\t. prefix a (e t))) /\ (* GSEQ3 *) 1195 (!a1 a2 e1 e2. 1196 GSEQ e1 /\ GSEQ e2 ==> GSEQ (\t. sum (prefix a1 (e1 t)) (* GSEQ4 *) 1197 (prefix a2 (e2 t)))) 1198End 1199 1200val [GSEQ1, GSEQ2, GSEQ3, GSEQ4] = 1201 map save_thm (combine (["GSEQ1", "GSEQ2", "GSEQ3", "GSEQ4"], 1202 CONJUNCTS GSEQ_rules)); 1203 1204val GSEQ3a = store_thm ("GSEQ3a", 1205 ``!a :'b Action. GSEQ (\t. prefix a t)``, 1206 ASSUME_TAC GSEQ1 1207 >> IMP_RES_TAC GSEQ3 1208 >> POP_ASSUM MP_TAC 1209 >> BETA_TAC >> REWRITE_TAC []); 1210 1211val GSEQ_IMP_CONTEXT = store_thm ( 1212 "GSEQ_IMP_CONTEXT", ``!e. GSEQ e ==> CONTEXT e``, 1213 Induct_on `GSEQ` 1214 >> rpt STRIP_TAC (* 4 sub-goals here *) 1215 >| [ REWRITE_TAC [CONTEXT1], 1216 REWRITE_TAC [CONTEXT2], 1217 MATCH_MP_TAC CONTEXT3 >> ASM_REWRITE_TAC [], 1218 qpat_x_assum `CONTEXT e1` (ASSUME_TAC o (Q.SPEC `a1`) o (MATCH_MP CONTEXT3)) \\ 1219 qpat_x_assum `CONTEXT e2` (ASSUME_TAC o (Q.SPEC `a2`) o (MATCH_MP CONTEXT3)) \\ 1220 MP_TAC (Q.SPECL [`\t. (prefix a1 (e1 t))`, `\t. (prefix a2 (e2 t))`] CONTEXT4) \\ 1221 BETA_TAC >> RW_TAC std_ss [] ]); 1222 1223val GSEQ_combin = store_thm ( 1224 "GSEQ_combin", ``!E. GSEQ E ==> !E'. GSEQ E' ==> GSEQ (E o E')``, 1225 Induct_on `GSEQ` 1226 >> REWRITE_TAC [o_DEF] >> BETA_TAC 1227 >> REWRITE_TAC [ETA_THM] 1228 >> rpt STRIP_TAC (* 3 sub-goals here *) 1229 >| [ (* goal 1 (of 3) *) 1230 REWRITE_TAC [GSEQ2], 1231 (* goal 2 (of 3) *) 1232 RES_TAC >> IMP_RES_TAC GSEQ3 \\ 1233 NTAC 2 (POP_ASSUM K_TAC) \\ 1234 POP_ASSUM (MP_TAC o (Q.SPEC `a`)) \\ 1235 KILL_TAC \\ 1236 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1237 (* goal 3 (of 3) *) 1238 `GSEQ (\x. E (E'' x)) /\ GSEQ (\x. E' (E'' x))` by METIS_TAC [] \\ 1239 METIS_TAC [GSEQ4] ]); 1240 1241val WEAK_EQUIV_SUBST_GSEQ = store_thm ( 1242 "WEAK_EQUIV_SUBST_GSEQ", 1243 ``!P Q. WEAK_EQUIV P Q ==> !E. GSEQ E ==> WEAK_EQUIV (E P) (E Q)``, 1244 rpt GEN_TAC >> DISCH_TAC 1245 >> Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC (* 4 sub-goals here *) 1246 >- ASM_REWRITE_TAC [] 1247 >- REWRITE_TAC [WEAK_EQUIV_REFL] 1248 >| [ (* goal 1 (of 2) *) 1249 MATCH_MP_TAC WEAK_EQUIV_SUBST_PREFIX >> ASM_REWRITE_TAC [], 1250 (* goal 2 (of 2) *) 1251 MATCH_MP_TAC WEAK_EQUIV_PRESD_BY_GUARDED_SUM \\ 1252 ASM_REWRITE_TAC [] ]); 1253 1254(* A combined (strong) induction theorem for SG + SEQ expression, it's easier to prove 1255 this induction theorem than defining another combined inductive relation SG_SEQ and 1256 prove SG /\ SEQ = SQ_SEQ, which is a combinatorial explosion of cases. 1257 *) 1258val SG_SEQ_strong_induction = store_thm ( 1259 "SG_SEQ_strong_induction", 1260 ``!R. (!p. R (\t. p)) /\ 1261 (!(l :'b Label) e. SEQ e ==> R (\t. prefix (label l) (e t))) /\ 1262 (!(a :'b Action) e. SG e /\ SEQ e /\ R e ==> R (\t. prefix a (e t))) /\ 1263 (!e1 e2. SG e1 /\ SEQ e1 /\ R e1 /\ 1264 SG e2 /\ SEQ e2 /\ R e2 ==> R (\t. sum (e1 t) (e2 t))) 1265 ==> (!e. SG e /\ SEQ e ==> R e)``, 1266 rpt STRIP_TAC 1267 >> qpat_x_assum `SG e` MP_TAC 1268 >> POP_ASSUM MP_TAC 1269 >> Q.SPEC_TAC (`e`, `e`) 1270 >> Induct_on `SEQ` 1271 >> rpt STRIP_TAC >> FULL_SIMP_TAC std_ss [] (* 3 sub-goals here *) 1272 >| [ (* goal 1 (of 3) *) 1273 Suff `~SG (\t. t)` >- PROVE_TAC [] \\ 1274 KILL_TAC \\ 1275 CCONTR_TAC >> FULL_SIMP_TAC std_ss [] \\ 1276 POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 1277 >- ( POP_ASSUM (MP_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 1278 STRIP_ASSUME_TAC (Q.SPEC `p` lemma) >> PROVE_TAC [] ) \\ 1279 qpat_x_assum `(\t. t) = X` 1280 (ASSUME_TAC o BETA_RULE o (Q.SPEC `nil`) o (REWRITE_RULE [FUN_EQ_THM])) \\ 1281 PROVE_TAC [CCS_distinct'], 1282 (* goal 2 (of 3) *) 1283 reverse (Cases_on `a`) >| (* 2 sub-goals here *) 1284 [ (* goal 2.1 (of 2) *) 1285 qpat_x_assum `!l e. SEQ e ==> P` MATCH_MP_TAC \\ 1286 ASM_REWRITE_TAC [], 1287 (* goal 2.2 (of 2) *) 1288 Suff `SG e` >- ( DISCH_TAC \\ 1289 qpat_x_assum `!a e. SG e /\ SEQ e /\ R e ==> P` MATCH_MP_TAC \\ 1290 ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1291 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1292 MATCH_MP_TAC SG3_backward >> ASM_REWRITE_TAC [] ], 1293 (* goal 3 (of 3) *) 1294 qpat_x_assum `!e1 e2. X` MATCH_MP_TAC \\ 1295 ASM_REWRITE_TAC [] \\ 1296 Suff `SG e /\ SG e'` >- ( STRIP_TAC >> ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1297 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1298 MATCH_MP_TAC SG4_backward >> ASM_REWRITE_TAC [] ]); 1299 1300val SG_GSEQ_strong_induction = store_thm ( 1301 "SG_GSEQ_strong_induction", 1302 ``!R. (!p. R (\t. p)) /\ 1303 (!(l :'b Label) e. GSEQ e ==> R (\t. prefix (label l) (e t))) /\ 1304 (!(a :'b Action) e. SG e /\ GSEQ e /\ R e ==> R (\t. prefix a (e t))) /\ 1305 (!e1 e2. SG e1 /\ GSEQ e1 /\ R e1 /\ SG e2 /\ GSEQ e2 /\ R e2 1306 ==> R (\t. sum (prefix tau (e1 t)) (prefix tau (e2 t)))) /\ 1307 (!l2 e1 e2. SG e1 /\ GSEQ e1 /\ R e1 /\ GSEQ e2 1308 ==> R (\t. sum (prefix tau (e1 t)) (prefix (label l2) (e2 t)))) /\ 1309 (!l1 e1 e2. GSEQ e1 /\ SG e2 /\ GSEQ e2 /\ R e2 1310 ==> R (\t. sum (prefix (label l1) (e1 t)) (prefix tau (e2 t)))) /\ 1311 (!l1 l2 e1 e2. GSEQ e1 /\ GSEQ e2 1312 ==> R (\t. sum (prefix (label l1) (e1 t)) (prefix (label l2) (e2 t)))) 1313 ==> (!e. SG e /\ GSEQ e ==> R e)``, 1314 rpt STRIP_TAC 1315 >> qpat_x_assum `SG e` MP_TAC 1316 >> POP_ASSUM MP_TAC 1317 >> Q.SPEC_TAC (`e`, `e`) 1318 >> Induct_on `GSEQ` 1319 >> rpt STRIP_TAC >> FULL_SIMP_TAC std_ss [] (* 3 sub-goals here *) 1320 >| [ (* goal 1 (of 3) *) 1321 Suff `~SG (\t. t)` >- PROVE_TAC [] \\ 1322 KILL_TAC \\ 1323 CCONTR_TAC >> FULL_SIMP_TAC std_ss [] \\ 1324 POP_ASSUM (STRIP_ASSUME_TAC o (ONCE_REWRITE_RULE [SG_cases])) (* 7 sub-goals here *) 1325 >- ( POP_ASSUM (MP_TAC o BETA_RULE o (ONCE_REWRITE_RULE [FUN_EQ_THM])) \\ 1326 STRIP_ASSUME_TAC (Q.SPEC `p` lemma) >> PROVE_TAC [] ) \\ 1327 qpat_x_assum `(\t. t) = X` 1328 (ASSUME_TAC o BETA_RULE o (Q.SPEC `nil`) o (REWRITE_RULE [FUN_EQ_THM])) \\ 1329 PROVE_TAC [CCS_distinct'], 1330 (* goal 2 (of 3) *) 1331 reverse (Cases_on `a`) >| (* 2 sub-goals here *) 1332 [ (* goal 2.1 (of 2) *) 1333 qpat_x_assum `!l e. GSEQ e ==> P` MATCH_MP_TAC \\ 1334 ASM_REWRITE_TAC [], 1335 (* goal 2.2 (of 2) *) 1336 Suff `SG e` >- ( DISCH_TAC \\ 1337 qpat_x_assum `!a e. SG e /\ GSEQ e /\ R e ==> P` MATCH_MP_TAC \\ 1338 ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1339 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1340 MATCH_MP_TAC SG3_backward >> ASM_REWRITE_TAC [] ], 1341 (* goal 3 (of 3) *) 1342 Cases_on `a1` >> Cases_on `a2` >| (* 4 sub-goals here *) 1343 [ (* goal 3.1 (of 4) *) 1344 qpat_x_assum `!e1 e2. X ==> R (\t. prefix tau (e1 t) + prefix tau (e2 t))` MATCH_MP_TAC \\ 1345 ASM_REWRITE_TAC [] \\ 1346 Suff `SG e /\ SG e'` >- ( STRIP_TAC >> ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1347 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1348 MATCH_MP_TAC SG10 >> ASM_REWRITE_TAC [], 1349 (* goal 3.2 (of 4) *) 1350 qpat_x_assum `!l2 e1 e2. X ==> R (\t. prefix tau (e1 t) + prefix (label l2) (e2 t))` 1351 MATCH_MP_TAC \\ 1352 ASM_REWRITE_TAC [] \\ 1353 Suff `SG e` >- ( STRIP_TAC >> ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1354 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1355 MATCH_MP_TAC SG11 >> take [`e'`, `x`] >> ASM_REWRITE_TAC [], 1356 (* goal 3.2 (of 4) *) 1357 qpat_x_assum `!l1 e1 e2. X ==> R (\t. prefix (label l1) (e1 t) + prefix tau (e2 t))` 1358 MATCH_MP_TAC \\ 1359 ASM_REWRITE_TAC [] \\ 1360 Suff `SG e'` >- ( STRIP_TAC >> ASM_REWRITE_TAC [] >> METIS_TAC [] ) \\ 1361 POP_ASSUM MP_TAC >> KILL_TAC >> DISCH_TAC \\ 1362 MATCH_MP_TAC SG11' >> take [`e`, `x`] >> ASM_REWRITE_TAC [], 1363 (* goal 3.4 (of 4) *) 1364 qpat_x_assum `!l1 l2 e1 e2. X ==> R (\t. prefix (label l1) (e1 t) + prefix (label l2) (e2 t))` 1365 MATCH_MP_TAC \\ 1366 ASM_REWRITE_TAC [] ] ]); 1367 1368val SG_SEQ_combin = store_thm ( 1369 "SG_SEQ_combin", ``!E. SG E /\ SEQ E ==> !H. SEQ H ==> (SG (H o E) /\ SEQ (H o E))``, 1370 HO_MATCH_MP_TAC SG_SEQ_strong_induction 1371 >> REWRITE_TAC [o_DEF] 1372 >> BETA_TAC >> rpt STRIP_TAC (* 8 sub-goals here *) 1373 >| [ (* goal 1 (of 8) *) 1374 REWRITE_TAC [SG1], 1375 (* goal 2 (of 8) *) 1376 REWRITE_TAC [SEQ2], 1377 (* goal 3 (of 8) *) 1378 POP_ASSUM MP_TAC >> Q.SPEC_TAC (`H`, `H`) \\ 1379 Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1380 [ (* goal 3.1 (of 4) *) 1381 IMP_RES_TAC SEQ_IMP_CONTEXT \\ 1382 MATCH_MP_TAC SG2 >> ASM_REWRITE_TAC [], 1383 (* goal 3.2 (of 4) *) 1384 REWRITE_TAC [SG1], 1385 (* goal 3.3 (of 4) *) 1386 IMP_RES_TAC SG3 \\ 1387 POP_ASSUM MP_TAC >> BETA_TAC \\ 1388 STRIP_TAC >> METIS_TAC [], 1389 (* goal 3.4 (of 4) *) 1390 IMP_RES_TAC (Q.SPECL [`\x. H (prefix (label l) (E x))`, 1391 `\x. H' (prefix (label l) (E x))`] SG4) \\ 1392 POP_ASSUM K_TAC \\ 1393 POP_ASSUM MP_TAC \\ 1394 NTAC 2 (POP_ASSUM K_TAC) \\ 1395 BETA_TAC >> DISCH_TAC >> METIS_TAC [] ], 1396 (* goal 4 (of 8) *) 1397 ASSUME_TAC (Q.SPECL [`label l`, `E`] SEQ3) \\ 1398 RES_TAC \\ 1399 ASSUME_TAC (Q.SPEC `H` SEQ_combin) \\ 1400 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1401 POP_ASSUM MP_TAC >> KILL_TAC \\ 1402 REWRITE_TAC [o_DEF] >> BETA_TAC \\ 1403 REWRITE_TAC [], 1404 (* goal 5 (of 8) *) 1405 POP_ASSUM MP_TAC \\ 1406 Q.SPEC_TAC (`H`, `H`) \\ 1407 Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1408 [ (* goal 5.1 (of 4) *) 1409 MATCH_MP_TAC SG3 >> ASM_REWRITE_TAC [], 1410 (* goal 5.2 (of 4) *) 1411 REWRITE_TAC [SG1], 1412 (* goal 5.3 (of 4) *) 1413 ASSUME_TAC (Q.SPECL [`a' :'b Action`, 1414 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (prefix a (E x))`] SG3) \\ 1415 POP_ASSUM MP_TAC \\ 1416 BETA_TAC >> rpt STRIP_TAC >> RES_TAC, 1417 (* goal 5.4 (of 4) *) 1418 IMP_RES_TAC (Q.SPECL [`\x. H (prefix a (E x))`, `\x. H' (prefix a (E x))`] SG4) \\ 1419 POP_ASSUM K_TAC \\ 1420 POP_ASSUM MP_TAC \\ 1421 NTAC 2 (POP_ASSUM K_TAC) \\ 1422 BETA_TAC >> DISCH_TAC \\ 1423 METIS_TAC [] ], 1424 (* goal 6 (of 8) *) 1425 ASSUME_TAC (Q.SPECL [`a :'b Action`, `E`] SEQ3) \\ 1426 RES_TAC >> NTAC 4 (POP_ASSUM K_TAC) \\ 1427 ASSUME_TAC (Q.SPEC `H` SEQ_combin) \\ 1428 POP_ASSUM (ASSUME_TAC o (fn th => MP th (ASSUME ``SEQ H``))) \\ 1429 POP_ASSUM (ASSUME_TAC o (Q.SPEC `\t. prefix a (E t)`)) \\ 1430 POP_ASSUM MP_TAC \\ 1431 REWRITE_TAC [o_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1432 PROVE_TAC [], 1433 (* goal 7 (of 8) *) 1434 POP_ASSUM MP_TAC \\ 1435 Q.SPEC_TAC (`H`, `H`) \\ 1436 Induct_on `SEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1437 [ (* goal 7.1 (of 4) *) 1438 MATCH_MP_TAC SG4 >> ASM_REWRITE_TAC [], 1439 (* goal 7.2 (of 4) *) 1440 REWRITE_TAC [SG1], 1441 (* goal 7.3 (of 4) *) 1442 ASSUME_TAC (Q.SPECL [`a :'b Action`, 1443 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (E x + E' x)`] SG3) \\ 1444 POP_ASSUM MP_TAC >> BETA_TAC >> rpt STRIP_TAC \\ 1445 PROVE_TAC [], 1446 (* goal 7.4 (of 4) *) 1447 IMP_RES_TAC (Q.SPECL [`\x. H (E x + E' x)`, 1448 `\x. H' (E x + E' x)`] SG4) \\ 1449 POP_ASSUM K_TAC \\ 1450 POP_ASSUM MP_TAC \\ 1451 NTAC 2 (POP_ASSUM K_TAC) \\ 1452 BETA_TAC >> DISCH_TAC \\ 1453 METIS_TAC [] ], 1454 (* goal 8 (of 8) *) 1455 ASSUME_TAC (Q.SPECL [`E`, `E'`] SEQ4) \\ 1456 NTAC 2 (qpat_x_assum `!H. X` K_TAC) >> RES_TAC \\ 1457 ASSUME_TAC (Q.SPEC `H` SEQ_combin) \\ 1458 RES_TAC >> NTAC 3 (POP_ASSUM K_TAC) \\ 1459 POP_ASSUM MP_TAC >> REWRITE_TAC [o_DEF] >> BETA_TAC >> REWRITE_TAC [] ]); 1460 1461val SG_GSEQ_combin = store_thm ( 1462 "SG_GSEQ_combin", ``!E. SG E /\ GSEQ E ==> !H. GSEQ H ==> (SG (H o E) /\ GSEQ (H o E))``, 1463 HO_MATCH_MP_TAC SG_GSEQ_strong_induction 1464 >> REWRITE_TAC [o_DEF] 1465 >> BETA_TAC >> rpt STRIP_TAC (* 14 sub-goals here *) 1466 >| [ (* goal 1 (of 14) *) 1467 REWRITE_TAC [SG1], 1468 (* goal 2 (of 14) *) 1469 REWRITE_TAC [GSEQ2], 1470 (* goal 3 (of 14) *) 1471 POP_ASSUM MP_TAC >> Q.SPEC_TAC (`H`, `H`) \\ 1472 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1473 [ (* goal 3.1 (of 4) *) 1474 IMP_RES_TAC GSEQ_IMP_CONTEXT \\ 1475 MATCH_MP_TAC SG2 >> ASM_REWRITE_TAC [], 1476 (* goal 3.2 (of 4) *) 1477 REWRITE_TAC [SG1], 1478 (* goal 3.3 (of 4) *) 1479 IMP_RES_TAC SG3 \\ 1480 POP_ASSUM MP_TAC >> BETA_TAC \\ 1481 STRIP_TAC >> METIS_TAC [], 1482 (* goal 3.4 (of 4) *) 1483 IMP_RES_TAC SG3 \\ 1484 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1485 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1486 BETA_TAC >> rpt DISCH_TAC \\ 1487 IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix (label l) (E t))))`, 1488 `\t. (prefix a2 (H' (prefix (label l) (E t))))`] SG4) \\ 1489 NTAC 2 (POP_ASSUM K_TAC) \\ 1490 POP_ASSUM MP_TAC \\ 1491 POP_ASSUM K_TAC \\ 1492 BETA_TAC >> DISCH_TAC >> METIS_TAC [] ], 1493 (* goal 4 (of 14) *) 1494 ASSUME_TAC (Q.SPECL [`label l`, `E`] GSEQ3) \\ 1495 RES_TAC \\ 1496 ASSUME_TAC (Q.SPEC `H` GSEQ_combin) \\ 1497 RES_TAC >> NTAC 2 (POP_ASSUM K_TAC) \\ 1498 POP_ASSUM MP_TAC >> KILL_TAC \\ 1499 REWRITE_TAC [o_DEF] >> BETA_TAC \\ 1500 REWRITE_TAC [], 1501 (* goal 5 (of 14) *) 1502 POP_ASSUM MP_TAC \\ 1503 Q.SPEC_TAC (`H`, `H`) \\ 1504 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1505 [ (* goal 5.1 (of 4) *) 1506 MATCH_MP_TAC SG3 >> ASM_REWRITE_TAC [], 1507 (* goal 5.2 (of 4) *) 1508 REWRITE_TAC [SG1], 1509 (* goal 5.3 (of 4) *) 1510 ASSUME_TAC (Q.SPECL [`a' :'b Action`, 1511 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (prefix a (E x))`] SG3) \\ 1512 POP_ASSUM MP_TAC \\ 1513 BETA_TAC >> rpt STRIP_TAC >> RES_TAC, 1514 (* goal 5.4 (of 4) *) 1515 IMP_RES_TAC SG3 >> POP_ASSUM K_TAC \\ 1516 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1517 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1518 BETA_TAC >> rpt DISCH_TAC \\ 1519 IMP_RES_TAC (Q.SPECL [`\t. (prefix a1 (H (prefix a (E t))))`, 1520 `\t. (prefix a2 (H' (prefix a (E t))))`] SG4) \\ 1521 NTAC 2 (POP_ASSUM K_TAC) \\ 1522 POP_ASSUM MP_TAC \\ 1523 POP_ASSUM K_TAC \\ 1524 BETA_TAC >> DISCH_TAC >> METIS_TAC [] ], 1525 (* goal 6 (of 14) *) 1526 ASSUME_TAC (Q.SPECL [`a :'b Action`, `E`] GSEQ3) \\ 1527 RES_TAC >> NTAC 4 (POP_ASSUM K_TAC) \\ 1528 ASSUME_TAC (Q.SPEC `H` GSEQ_combin) \\ 1529 POP_ASSUM (ASSUME_TAC o (fn th => MP th (ASSUME ``GSEQ H``))) \\ 1530 POP_ASSUM (ASSUME_TAC o (Q.SPEC `\t. prefix a (E t)`)) \\ 1531 POP_ASSUM MP_TAC \\ 1532 REWRITE_TAC [o_DEF] >> BETA_TAC >> rpt STRIP_TAC \\ 1533 PROVE_TAC [], 1534 (* goal 7 (of 14) *) 1535 POP_ASSUM MP_TAC \\ 1536 Q.SPEC_TAC (`H`, `H`) \\ 1537 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1538 [ (* goal 7.1 (of 4) *) 1539 IMP_RES_TAC SG3 \\ 1540 NTAC 2 (POP_ASSUM (MP_TAC o (Q.SPEC `tau`))) >> rpt DISCH_TAC \\ 1541 IMP_RES_TAC (Q.SPECL [`\t. (prefix tau (E t))`, `\t. (prefix tau (E' t))`] SG4) \\ 1542 NTAC 2 (POP_ASSUM K_TAC) \\ 1543 POP_ASSUM MP_TAC \\ 1544 POP_ASSUM K_TAC \\ 1545 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1546 (* goal 7.2 (of 4) *) 1547 REWRITE_TAC [SG1], 1548 (* goal 7.3 (of 4) *) 1549 ASSUME_TAC 1550 (Q.SPECL [`a :'b Action`, 1551 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (tau..(E x) + tau..(E' x))`] SG3) \\ 1552 POP_ASSUM MP_TAC >> BETA_TAC >> rpt STRIP_TAC \\ 1553 PROVE_TAC [], 1554 (* goal 7.4 (of 4) *) 1555 IMP_RES_TAC SG3 >> NTAC 2 (POP_ASSUM K_TAC) \\ 1556 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1557 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1558 BETA_TAC >> rpt DISCH_TAC \\ 1559 IMP_RES_TAC (Q.SPECL [`\t. a1..(H (tau..(E t) + tau..(E' t)))`, 1560 `\t. a2..(H' (tau..(E t) + tau..(E' t)))`] SG4) \\ 1561 NTAC 2 (POP_ASSUM K_TAC) \\ 1562 POP_ASSUM MP_TAC \\ 1563 POP_ASSUM K_TAC \\ 1564 BETA_TAC >> DISCH_TAC \\ 1565 METIS_TAC [] ], 1566 (* goal 8 (of 14) *) 1567 ASSUME_TAC (Q.SPECL [`tau`, `tau`, `E`, `E'`] GSEQ4) \\ 1568 NTAC 2 (qpat_x_assum `!H. X` K_TAC) >> RES_TAC \\ 1569 ASSUME_TAC (Q.SPEC `H` GSEQ_combin) \\ 1570 RES_TAC >> NTAC 3 (POP_ASSUM K_TAC) \\ 1571 POP_ASSUM MP_TAC >> REWRITE_TAC [o_DEF] >> BETA_TAC >> REWRITE_TAC [], 1572 (* goal 9 (of 14) *) 1573 POP_ASSUM MP_TAC \\ 1574 Q.SPEC_TAC (`H`, `H`) \\ 1575 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1576 [ (* goal 9.1 (of 4) *) 1577 IMP_RES_TAC SG3 \\ 1578 POP_ASSUM (ASSUME_TAC o (Q.SPEC `tau`)) \\ 1579 IMP_RES_TAC GSEQ_IMP_CONTEXT \\ 1580 POP_ASSUM K_TAC \\ 1581 IMP_RES_TAC SG2 \\ 1582 POP_ASSUM (ASSUME_TAC o (Q.SPEC `l2`)) \\ 1583 IMP_RES_TAC (Q.SPECL [`\t. (prefix tau (E t))`, `\t. (prefix (label l2) (e2 t))`] SG4) \\ 1584 POP_ASSUM MP_TAC \\ 1585 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1586 (* goal 9.2 (of 4) *) 1587 REWRITE_TAC [SG1], 1588 (* goal 9.3 (of 4) *) 1589 ASSUME_TAC 1590 (Q.SPECL [`a :'b Action`, 1591 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) (tau..(E x) + (label l2)..(e2 x))`] SG3) \\ 1592 POP_ASSUM MP_TAC >> BETA_TAC >> rpt STRIP_TAC \\ 1593 PROVE_TAC [], 1594 (* goal 9.4 (of 4) *) 1595 IMP_RES_TAC SG3 >> POP_ASSUM K_TAC \\ 1596 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1597 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1598 BETA_TAC >> rpt DISCH_TAC \\ 1599 IMP_RES_TAC (Q.SPECL [`\t. a1..(H (tau..(E t) + (label l2)..(e2 t)))`, 1600 `\t. a2..(H' (tau..(E t) + (label l2)..(e2 t)))`] SG4) \\ 1601 NTAC 2 (POP_ASSUM K_TAC) \\ 1602 POP_ASSUM MP_TAC \\ 1603 POP_ASSUM K_TAC \\ 1604 BETA_TAC >> DISCH_TAC \\ 1605 METIS_TAC [] ], 1606 (* goal 10 (of 14) *) 1607 ASSUME_TAC (Q.SPECL [`tau`, `label l2`, `E`, `e2`] GSEQ4) \\ 1608 qpat_x_assum `!H. X` K_TAC >> RES_TAC \\ 1609 ASSUME_TAC (Q.SPEC `H` GSEQ_combin) \\ 1610 RES_TAC >> NTAC 3 (POP_ASSUM K_TAC) \\ 1611 POP_ASSUM MP_TAC >> REWRITE_TAC [o_DEF] >> BETA_TAC >> REWRITE_TAC [], 1612 (* goal 11 (of 14) *) 1613 POP_ASSUM MP_TAC \\ 1614 Q.SPEC_TAC (`H`, `H`) \\ 1615 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1616 [ (* goal 11.1 (of 4) *) 1617 IMP_RES_TAC SG3 \\ 1618 POP_ASSUM (ASSUME_TAC o (Q.SPEC `tau`)) \\ 1619 IMP_RES_TAC GSEQ_IMP_CONTEXT \\ 1620 qpat_x_assum `CONTEXT E` K_TAC \\ 1621 IMP_RES_TAC SG2 \\ 1622 POP_ASSUM (ASSUME_TAC o (Q.SPEC `l1`)) \\ 1623 IMP_RES_TAC (Q.SPECL [`\t. (prefix (label l1) (e1 t))`, 1624 `\t. (prefix tau (E t))`] SG4) \\ 1625 POP_ASSUM MP_TAC \\ 1626 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1627 (* goal 11.2 (of 4) *) 1628 REWRITE_TAC [SG1], 1629 (* goal 11.3 (of 4) *) 1630 ASSUME_TAC 1631 (Q.SPECL [`a :'b Action`, 1632 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) 1633 ((label l1)..(e1 x) + tau..(E x))`] SG3) \\ 1634 POP_ASSUM MP_TAC >> BETA_TAC >> rpt STRIP_TAC \\ 1635 PROVE_TAC [], 1636 (* goal 11.4 (of 4) *) 1637 IMP_RES_TAC SG3 >> POP_ASSUM K_TAC \\ 1638 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1639 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1640 BETA_TAC >> rpt DISCH_TAC \\ 1641 IMP_RES_TAC (Q.SPECL [`\t. a1..(H ((label l2)..(e2 t) + tau..(E t)))`, 1642 `\t. a2..(H' ((label l2)..(e2 t) + tau..(E t)))`] SG4) \\ 1643 NTAC 2 (POP_ASSUM K_TAC) \\ 1644 POP_ASSUM MP_TAC \\ 1645 POP_ASSUM K_TAC \\ 1646 BETA_TAC >> DISCH_TAC \\ 1647 METIS_TAC [] ], 1648 (* goal 12 (of 14) *) 1649 ASSUME_TAC (Q.SPECL [`label l1`, `tau`, `e1`, `E`] GSEQ4) \\ 1650 qpat_x_assum `!H. X` K_TAC >> RES_TAC \\ 1651 ASSUME_TAC (Q.SPEC `H` GSEQ_combin) \\ 1652 RES_TAC >> NTAC 3 (POP_ASSUM K_TAC) \\ 1653 POP_ASSUM MP_TAC >> REWRITE_TAC [o_DEF] >> BETA_TAC >> REWRITE_TAC [], 1654 (* goal 13 (of 14) *) 1655 POP_ASSUM MP_TAC \\ 1656 Q.SPEC_TAC (`H`, `H`) \\ 1657 Induct_on `GSEQ` >> BETA_TAC >> rpt STRIP_TAC >| (* 4 sub-goals here *) 1658 [ (* goal 13.1 (of 4) *) 1659 IMP_RES_TAC GSEQ_IMP_CONTEXT \\ 1660 IMP_RES_TAC SG2 \\ 1661 POP_ASSUM (MP_TAC o (Q.SPEC `l2`)) \\ 1662 POP_ASSUM (MP_TAC o (Q.SPEC `l1`)) \\ 1663 rpt DISCH_TAC \\ 1664 IMP_RES_TAC (Q.SPECL [`\t. (prefix (label l1) (e1 t))`, 1665 `\t. (prefix (label l2) (e2 t))`] SG4) \\ 1666 POP_ASSUM K_TAC \\ 1667 POP_ASSUM MP_TAC >> KILL_TAC \\ 1668 BETA_TAC >> DISCH_TAC >> METIS_TAC [], 1669 (* goal 13.2 (of 4) *) 1670 REWRITE_TAC [SG1], 1671 (* goal 13.3 (of 4) *) 1672 ASSUME_TAC 1673 (Q.SPECL [`a :'b Action`, 1674 `\x. (H :('a, 'b) CCS -> ('a, 'b) CCS) 1675 ((label l1)..(e1 x) + (label l2)..(e2 x))`] SG3) \\ 1676 POP_ASSUM MP_TAC >> BETA_TAC >> rpt STRIP_TAC >> PROVE_TAC [], 1677 (* goal 13.4 (of 4) *) 1678 IMP_RES_TAC SG3 \\ 1679 POP_ASSUM (MP_TAC o (Q.SPEC `a1`)) \\ 1680 POP_ASSUM (MP_TAC o (Q.SPEC `a2`)) \\ 1681 BETA_TAC >> rpt DISCH_TAC \\ 1682 IMP_RES_TAC (Q.SPECL [`\t. a1..(H ((label l1)..(e1 t) + (label l2)..(e2 t)))`, 1683 `\t. a2..(H' ((label l1)..(e1 t) + (label l2)..(e2 t)))`] SG4) \\ 1684 NTAC 2 (POP_ASSUM K_TAC) \\ 1685 POP_ASSUM MP_TAC >> KILL_TAC \\ 1686 BETA_TAC >> DISCH_TAC >> METIS_TAC [] ], 1687 (* goal 14 (of 14) *) 1688 MP_TAC (Q.SPECL [`label l1`, `label l2`, `e1`, `e2`] GSEQ4) \\ 1689 MP_TAC (Q.SPEC `H` GSEQ_combin) \\ 1690 RW_TAC std_ss [] \\ 1691 qpat_x_assum `!E'. GSEQ E' ==> X` 1692 (MP_TAC o (Q.SPEC `\t. (label l1)..(e1 t) + (label l2)..(e2 t)`)) \\ 1693 REWRITE_TAC [o_DEF] >> BETA_TAC >> METIS_TAC [] ]); 1694 1695(******************************************************************************) 1696(* *) 1697(* Weakly guarded expressions with guarded sums *) 1698(* *) 1699(******************************************************************************) 1700 1701(* The only difference from WG is at WGS4, in which the sum has prefixed args, 1702 and the underlying e1 & e2 can be simply GCONTEXT. *) 1703val (WGS_rules, WGS_ind, WGS_cases) = Hol_reln ` 1704 (!p. WGS (\t. p)) /\ (* WGS2 *) 1705 (!a e. GCONTEXT e ==> WGS (\t. prefix a (e t))) /\ (* WGS3 *) 1706 (!a1 a2 e1 e2. 1707 GCONTEXT e1 /\ GCONTEXT e2 1708 ==> WGS (\t. sum (prefix a1 (e1 t)) (* WGS4 *) 1709 (prefix a2 (e2 t)))) /\ 1710 (!e1 e2. WGS e1 /\ WGS e2 ==> WGS (\t. par (e1 t) (e2 t))) /\ (* WGS5 *) 1711 (!L e. WGS e ==> WGS (\t. restr L (e t))) /\ (* WGS6 *) 1712 (!rf e. WGS e ==> WGS (\t. relab (e t) rf)) `; (* WGS7 *) 1713 1714val WGS_strongind = DB.fetch "-" "WGS_strongind"; 1715 1716val [WGS2, WGS3, WGS4, WGS5, WGS6, WGS7] = 1717 map save_thm 1718 (combine (["WGS2", "WGS3", "WGS4", "WGS5", "WGS6", "WGS7"], 1719 CONJUNCTS WGS_rules)); 1720 1721(** WGS1 is derivable from WGS3 *) 1722val WGS1 = store_thm ("WGS1", 1723 ``!a :'b Action. WGS (\t. prefix a t)``, 1724 ASSUME_TAC GCONTEXT1 1725 >> IMP_RES_TAC WGS3 1726 >> POP_ASSUM MP_TAC 1727 >> BETA_TAC 1728 >> REWRITE_TAC []); 1729 1730val WGS_IMP_GCONTEXT = store_thm ( 1731 "WGS_IMP_GCONTEXT", ``!e. WGS e ==> GCONTEXT e``, 1732 Induct_on `WGS` 1733 >> rpt STRIP_TAC (* 6 sub-goals here *) 1734 >| [ REWRITE_TAC [GCONTEXT2], 1735 MATCH_MP_TAC GCONTEXT3 >> ASM_REWRITE_TAC [], 1736 MATCH_MP_TAC GCONTEXT4 >> ASM_REWRITE_TAC [], 1737 MATCH_MP_TAC GCONTEXT5 >> ASM_REWRITE_TAC [], 1738 MATCH_MP_TAC GCONTEXT6 >> ASM_REWRITE_TAC [], 1739 MATCH_MP_TAC GCONTEXT7 >> ASM_REWRITE_TAC [] ]); 1740 1741val WGS_IMP_CONTEXT = store_thm ( 1742 "WGS_IMP_CONTEXT", ``!e. WGS e ==> CONTEXT e``, 1743 rpt STRIP_TAC 1744 >> MATCH_MP_TAC GCONTEXT_IMP_CONTEXT 1745 >> IMP_RES_TAC WGS_IMP_GCONTEXT); 1746 1747val GCONTEXT_WGS_combin = store_thm ( 1748 "GCONTEXT_WGS_combin", ``!c e. GCONTEXT c /\ WGS e ==> WGS (c o e)``, 1749 rpt STRIP_TAC 1750 >> NTAC 2 (POP_ASSUM MP_TAC) 1751 >> Q.SPEC_TAC (`c`, `c`) 1752 >> HO_MATCH_MP_TAC GCONTEXT_ind 1753 >> REWRITE_TAC [o_DEF] 1754 >> BETA_TAC 1755 >> REWRITE_TAC [ETA_AX] 1756 >> rpt STRIP_TAC >> RES_TAC (* 6 sub-goals here *) 1757 >| [ (* goal 1 (of 6) *) 1758 REWRITE_TAC [WGS2], 1759 (* goal 2 (of 6) *) 1760 IMP_RES_TAC WGS_IMP_GCONTEXT \\ 1761 MP_TAC (Q.SPECL [`a`, `(\x. (c :('a, 'b) context) (e x))`] WGS3) \\ 1762 BETA_TAC >> RW_TAC std_ss [], 1763 (* goal 3 (of 6) *) 1764 MP_TAC (Q.SPECL [`a1`, `a2`, `(\x. (c :('a, 'b) context) (e x))`, 1765 `(\x. (c' :('a, 'b) context) (e x))`] WGS4) \\ 1766 BETA_TAC \\ 1767 IMP_RES_TAC WGS_IMP_GCONTEXT >> RW_TAC std_ss [], 1768 (* goal 4 (of 6) *) 1769 MP_TAC (Q.SPECL [`(\x. (c :('a, 'b) context) (e x))`, 1770 `(\x. (c' :('a, 'b) context) (e x))`] WGS5) \\ 1771 BETA_TAC >> RW_TAC std_ss [], 1772 (* goal 5 (of 6) *) 1773 MP_TAC (Q.SPECL [`L`, `(\x. (c :('a, 'b) context) (e x))`] WGS6) \\ 1774 BETA_TAC >> RW_TAC std_ss [], 1775 (* goal 6 (of 6) *) 1776 MP_TAC (Q.SPECL [`rf`, `(\x. (c :('a, 'b) context) (e x))`] WGS7) \\ 1777 BETA_TAC >> RW_TAC std_ss [] ]); 1778 1779val _ = export_theory (); 1780val _ = html_theory "Congruence"; 1781 1782(* last updated: Oct 12, 2017 *) 1783