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