1(*---------------------------------------------------------------------------* 2 * A theory about relations, taken as functions of type 'a->'a->bool. * 3 * We treat various kinds of closure (reflexive, transitive, r&t) * 4 * and wellfoundedness to start. A few other notions, like inverse image, * 5 * are also defined. * 6 *---------------------------------------------------------------------------*) 7 8open HolKernel Parse boolLib QLib tautLib mesonLib metisLib 9 simpLib boolSimps BasicProvers; 10 11(* mention satTheory to work around dependency-analysis flaw in Holmake; 12 satTheory is a dependency of BasicProvers, but without explicit mention 13 here, Holmake will not rebuild relationTheory when satTheory changes. *) 14local open combinTheory satTheory in end; 15 16val _ = new_theory "relation"; 17 18(*---------------------------------------------------------------------------*) 19(* Basic properties of relations. *) 20(*---------------------------------------------------------------------------*) 21 22val transitive_def = 23Q.new_definition 24("transitive_def", 25 `transitive (R:'a->'a->bool) = !x y z. R x y /\ R y z ==> R x z`); 26val _ = OpenTheoryMap.OpenTheory_const_name 27 {const={Thy="relation",Name="transitive"}, 28 name=(["Relation"],"transitive")} 29 30val reflexive_def = new_definition( 31 "reflexive_def", 32 ``reflexive (R:'a->'a->bool) = !x. R x x``); 33val _ = OpenTheoryMap.OpenTheory_const_name 34 {const={Thy="relation",Name="reflexive"}, 35 name=(["Relation"],"reflexive")} 36 37val irreflexive_def = new_definition( 38 "irreflexive_def", 39 ``irreflexive (R:'a->'a->bool) = !x. ~R x x``); 40val _ = OpenTheoryMap.OpenTheory_const_name 41 {const={Thy="relation",Name="irreflexive"}, 42 name=(["Relation"],"irreflexive")} 43 44val symmetric_def = new_definition( 45 "symmetric_def", 46 ``symmetric (R:'a->'a->bool) = !x y. R x y = R y x``); 47 48val antisymmetric_def = new_definition( 49 "antisymmetric_def", 50 ``antisymmetric (R:'a->'a->bool) = !x y. R x y /\ R y x ==> (x = y)``); 51 52val equivalence_def = new_definition( 53 "equivalence_def", 54 ���equivalence (R:'a->'a->bool) <=> reflexive R /\ symmetric R /\ transitive R��� 55); 56 57val total_def = new_definition( 58 "total_def", 59 ``total (R:'a->'a->bool) = !x y. R x y \/ R y x``); 60 61val trichotomous = new_definition( 62 "trichotomous", 63 ``trichotomous (R:'a->'a->bool) = !a b. R a b \/ R b a \/ (a = b)``); 64 65(*---------------------------------------------------------------------------*) 66(* Closures *) 67(*---------------------------------------------------------------------------*) 68 69(* The TC and RTC suffixes are tighter than function application. This 70 means that 71 inv R^+ 72 is the inverse of the transitive closure, and you need parentheses to 73 write the transitive closure of the inverse: 74 (inv R)^+ 75*) 76val TC_DEF = Q.new_definition 77 ("TC_DEF", 78 `TC (R:'a->'a->bool) a b = 79 !P.(!x y. R x y ==> P x y) /\ 80 (!x y z. P x y /\ P y z ==> P x z) ==> P a b`); 81val _ = add_rule { fixity = Suffix 2100, 82 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)), 83 paren_style = OnlyIfNecessary, 84 pp_elements = [TOK "^+"], 85 term_name = "TC" } 86val _ = Unicode.unicode_version {u = Unicode.UChar.sup_plus, tmnm = "TC"} 87val _ = TeX_notation {hol = Unicode.UChar.sup_plus, 88 TeX = ("\\HOLTokenSupPlus{}", 1)} 89val _ = TeX_notation {hol = "^+", TeX = ("\\HOLTokenSupPlus{}", 1)} 90val _ = OpenTheoryMap.OpenTheory_const_name 91 {const={Thy="relation",Name="TC"}, 92 name=(["Relation"],"transitiveClosure")} 93 94 95Inductive RTC: 96 (!x. RTC R x x) 97 /\ 98 (!x y z. R x y /\ RTC R y z ==> RTC R x z) 99End 100val _ = add_rule { fixity = Suffix 2100, 101 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)), 102 paren_style = OnlyIfNecessary, 103 pp_elements = [TOK "^*"], 104 term_name = "RTC" } 105val _ = Unicode.unicode_version {u = UTF8.chr 0xA673, tmnm = "RTC"} 106val _ = TeX_notation {hol = UTF8.chr 0xA673, TeX = ("\\HOLTokenSupStar{}", 1)} 107val _ = TeX_notation {hol = "^*", TeX = ("\\HOLTokenSupStar{}", 1)} 108 109val RC_DEF = new_definition( 110 "RC_DEF", 111 ``RC (R:'a->'a->bool) x y <=> (x = y) \/ R x y``); 112 113val SC_DEF = new_definition( 114 "SC_DEF", 115 ``SC (R:'a->'a->bool) x y <=> R x y \/ R y x``); 116 117val EQC_DEF = new_definition( 118 "EQC_DEF", 119 ``EQC (R:'a->'a->bool) = RC (TC (SC R))``); 120val _ = add_rule { fixity = Suffix 2100, 121 block_style = (AroundEachPhrase, (Portable.CONSISTENT,0)), 122 paren_style = OnlyIfNecessary, 123 pp_elements = [TOK "^="], 124 term_name = "EQC" } 125 126 127val SC_SYMMETRIC = store_thm( 128 "SC_SYMMETRIC", 129 ``!R. symmetric (SC R)``, 130 REWRITE_TAC [symmetric_def, SC_DEF] THEN MESON_TAC []); 131 132Theorem TC_TRANSITIVE[simp]: 133 !R:'a->'a->bool. transitive(TC R) 134Proof 135 REWRITE_TAC[transitive_def,TC_DEF] 136 THEN REPEAT STRIP_TAC 137 THEN RES_TAC THEN ASM_MESON_TAC[] 138QED 139 140Theorem RTC_INDUCT: 141 !R P. (!x. P x x) /\ (!x y z. R x y /\ P y z ==> P x z) ==> 142 (!x (y:'a). RTC R x y ==> P x y) 143Proof 144 MESON_TAC [RTC_ind] (* differs only in choice of induction variable "P" *) 145QED 146 147val TC_RULES = store_thm( 148 "TC_RULES", 149 ``!R. (!x (y:'a). R x y ==> TC R x y) /\ 150 (!x y z. TC R x y /\ TC R y z ==> TC R x z)``, 151 REWRITE_TAC [TC_DEF] THEN REPEAT STRIP_TAC THENL [ 152 ASM_MESON_TAC [], 153 FIRST_ASSUM MATCH_MP_TAC THEN RES_TAC THEN ASM_MESON_TAC [] 154 ]); 155 156Theorem RTC_RULES = RTC_rules; 157Theorem RTC_REFL[simp]: 158 RTC R x x 159Proof REWRITE_TAC [RTC_RULES] 160QED 161 162Theorem RTC_SINGLE[simp]: 163 !R x y. R x y ==> RTC R x y 164Proof 165 PROVE_TAC [RTC_RULES] 166QED 167 168Theorem RTC_STRONG_INDUCT[rule_induction]: 169 !R P. (!x. P x x) /\ (!x y z. R x y /\ RTC R y z /\ P y z ==> P x z) ==> 170 (!x (y:'a). RTC R x y ==> P x y) 171Proof 172 ASM_MESON_TAC [RTC_strongind] 173QED 174 175val RTC_RTC = store_thm( 176 "RTC_RTC", 177 ``!R (x:'a) y. RTC R x y ==> !z. RTC R y z ==> RTC R x z``, 178 GEN_TAC THEN HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN MESON_TAC [RTC_RULES]); 179 180val RTC_TRANSITIVE = store_thm( 181 "RTC_TRANSITIVE[simp]", 182 ``!R:'a->'a->bool. transitive (RTC R)``, 183 REWRITE_TAC [transitive_def] THEN MESON_TAC [RTC_RTC]); 184val transitive_RTC = save_thm("transitive_RTC", RTC_TRANSITIVE); 185 186val RTC_REFLEXIVE = store_thm( 187 "RTC_REFLEXIVE", 188 ``!R:'a->'a->bool. reflexive (RTC R)``, 189 MESON_TAC [reflexive_def, RTC_RULES]); 190val reflexive_RTC = save_thm("reflexive_RTC", RTC_REFLEXIVE); 191val _ = export_rewrites ["reflexive_RTC"] 192 193val RC_REFLEXIVE = store_thm( 194 "RC_REFLEXIVE", 195 ``!R:'a->'a->bool. reflexive (RC R)``, 196 MESON_TAC [reflexive_def, RC_DEF]); 197val reflexive_RC = save_thm("reflexive_RC", RC_REFLEXIVE); 198val _ = export_rewrites ["reflexive_RC"] 199 200val RC_lifts_monotonicities = store_thm( 201 "RC_lifts_monotonicities", 202 ``(!x y. R x y ==> R (f x) (f y)) ==> !x y. RC R x y ==> RC R (f x) (f y)``, 203 METIS_TAC [RC_DEF]); 204 205val RC_MONOTONE = store_thm( 206 "RC_MONOTONE[mono]", 207 ``(!x y. R x y ==> Q x y) ==> RC R x y ==> RC Q x y``, 208 STRIP_TAC THEN REWRITE_TAC [RC_DEF] THEN STRIP_TAC THEN 209 ASM_REWRITE_TAC [] THEN RES_TAC THEN ASM_REWRITE_TAC []) 210 211val RC_lifts_invariants = store_thm( 212 "RC_lifts_invariants", 213 ``(!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ RC R x y ==> P y)``, 214 METIS_TAC [RC_DEF]); 215 216val RC_lifts_equalities = store_thm( 217 "RC_lifts_equalities", 218 ``(!x y. R x y ==> (f x = f y)) ==> (!x y. RC R x y ==> (f x = f y))``, 219 METIS_TAC [RC_DEF]); 220 221val SC_lifts_monotonicities = store_thm( 222 "SC_lifts_monotonicities", 223 ``(!x y. R x y ==> R (f x) (f y)) ==> !x y. SC R x y ==> SC R (f x) (f y)``, 224 METIS_TAC [SC_DEF]); 225 226val SC_lifts_equalities = store_thm( 227 "SC_lifts_equalities", 228 ``(!x y. R x y ==> (f x = f y)) ==> !x y. SC R x y ==> (f x = f y)``, 229 METIS_TAC [SC_DEF]); 230 231val SC_MONOTONE = store_thm( 232 "SC_MONOTONE[mono]", 233 ``(!x:'a y. R x y ==> Q x y) ==> SC R x y ==> SC Q x y``, 234 STRIP_TAC THEN REWRITE_TAC [SC_DEF] THEN STRIP_TAC THEN RES_TAC THEN 235 ASM_REWRITE_TAC []) 236 237val symmetric_RC = store_thm( 238 "symmetric_RC", 239 ``!R. symmetric (RC R) = symmetric R``, 240 REWRITE_TAC [symmetric_def, RC_DEF] THEN 241 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN ASM_MESON_TAC []); 242val _ = export_rewrites ["symmetric_RC"] 243 244val antisymmetric_RC = store_thm( 245 "antisymmetric_RC", 246 ``!R. antisymmetric (RC R) = antisymmetric R``, 247 SRW_TAC [][antisymmetric_def, RC_DEF] THEN PROVE_TAC []); 248val _ = export_rewrites ["antisymmetric_RC"] 249 250val transitive_RC = store_thm( 251 "transitive_RC", 252 ``!R. transitive R ==> transitive (RC R)``, 253 SRW_TAC [][transitive_def, RC_DEF] THEN PROVE_TAC []); 254 255val TC_SUBSET = Q.store_thm("TC_SUBSET", 256`!R x (y:'a). R x y ==> TC R x y`, 257REWRITE_TAC[TC_DEF] THEN MESON_TAC[]); 258 259val RTC_SUBSET = store_thm( 260 "RTC_SUBSET", 261 ``!R (x:'a) y. R x y ==> RTC R x y``, 262 MESON_TAC [RTC_RULES]); 263 264val RC_SUBSET = store_thm( 265 "RC_SUBSET", 266 ``!R (x:'a) y. R x y ==> RC R x y``, 267 MESON_TAC [RC_DEF]); 268 269val RC_RTC = store_thm( 270 "RC_RTC", 271 ``!R (x:'a) y. RC R x y ==> RTC R x y``, 272 MESON_TAC [RC_DEF, RTC_RULES]); 273 274val tc = ``tc : ('a -> 'a -> bool) -> ('a -> 'a -> bool)`` 275val tc_left_asm = 276 ``tc = \R a b. !P. (!x y. R x y ==> P x y) /\ 277 (!x y z. R x y /\ P y z ==> P x z) ==> 278 P a b``; 279val tc_right_asm = 280 ``tc = \R a b. !P. (!x y. R x y ==> P x y) /\ 281 (!x y z. P x y /\ R y z ==> P x z) ==> 282 P a b``; 283 284val tc_left_rules0 = prove( 285 ``^tc_left_asm ==> (!x y. R x y ==> tc R x y) /\ 286 (!x y z. R x y /\ tc R y z ==> tc R x z)``, 287 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []); 288val tc_left_rules = UNDISCH tc_left_rules0 289 290val tc_right_rules = UNDISCH (prove( 291 ``^tc_right_asm ==> (!x y. R x y ==> tc R x y) /\ 292 (!x y z. tc R x y /\ R y z ==> tc R x z)``, 293 STRIP_TAC THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC [])); 294 295val tc_left_ind = TAC_PROOF( 296 ([tc_left_asm], 297 ``!R P. (!x y. R x y ==> P x y) /\ 298 (!x y z. R x y /\ P y z ==> P x z) ==> 299 (!x y. tc R x y ==> P x y)``), 300 ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []); 301 302val tc_right_ind = TAC_PROOF( 303 ([tc_right_asm], 304 ``!R P. (!x y. R x y ==> P x y) /\ 305 (!x y z. P x y /\ R y z ==> P x z) ==> 306 (!x y. tc R x y ==> P x y)``), 307 ASM_REWRITE_TAC [] THEN BETA_TAC THEN MESON_TAC []); 308 309val tc_left_twice = TAC_PROOF( 310 ([tc_left_asm], 311 ``!R x y. ^tc R x y ==> !z. tc R y z ==> tc R x z``), 312 GEN_TAC THEN 313 HO_MATCH_MP_TAC tc_left_ind THEN MESON_TAC [tc_left_rules]); 314val tc_right_twice = TAC_PROOF( 315 ([tc_right_asm], 316 ``!R x y. ^tc R x y ==> !z. tc R z x ==> tc R z y``), 317 GEN_TAC THEN HO_MATCH_MP_TAC tc_right_ind THEN MESON_TAC [tc_right_rules]); 318 319 320val TC_INDUCT = Q.store_thm("TC_INDUCT", 321`!(R:'a->'a->bool) P. 322 (!x y. R x y ==> P x y) /\ 323 (!x y z. P x y /\ P y z ==> P x z) 324 ==> !u v. (TC R) u v ==> P u v`, 325REWRITE_TAC[TC_DEF] THEN MESON_TAC[]); 326 327val tc_left_TC = TAC_PROOF( 328 ([tc_left_asm], 329 ``!R x y. tc R x y = TC R x y``), 330 GEN_TAC THEN 331 SIMP_TAC bool_ss [FORALL_AND_THM, EQ_IMP_THM] THEN CONJ_TAC THENL [ 332 HO_MATCH_MP_TAC tc_left_ind THEN MESON_TAC [TC_RULES], 333 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [tc_left_twice, tc_left_rules] 334 ]); 335val tc_right_TC = TAC_PROOF( 336 ([tc_right_asm], 337 ``!R x y. tc R x y = TC R x y``), 338 GEN_TAC THEN 339 SIMP_TAC bool_ss [FORALL_AND_THM, EQ_IMP_THM] THEN CONJ_TAC THENL [ 340 HO_MATCH_MP_TAC tc_right_ind THEN MESON_TAC [TC_RULES], 341 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [tc_right_twice, tc_right_rules] 342 ]); 343 344val tc_left_exists = SIMP_PROVE bool_ss [] ``?tc. ^tc_left_asm``; 345val tc_right_exists = SIMP_PROVE bool_ss [] ``?tc. ^tc_right_asm``; 346 347val TC_INDUCT_LEFT1 = save_thm( 348 "TC_INDUCT_LEFT1", 349 CHOOSE(tc, tc_left_exists) (REWRITE_RULE [tc_left_TC] tc_left_ind)); 350val TC_INDUCT_RIGHT1 = save_thm( 351 "TC_INDUCT_RIGHT1", 352 CHOOSE(tc, tc_right_exists) (REWRITE_RULE [tc_right_TC] tc_right_ind)); 353 354val TC_INDUCT_TAC = 355 let val tc_thm = TC_INDUCT 356 fun tac (asl,w) = 357 let val (u,Body) = dest_forall w 358 val (v,Body) = dest_forall Body 359 val (ant,conseq) = dest_imp Body 360 val (TC, R, u', v') = case strip_comb ant of 361 (TC, [R, u', v']) => (TC, R, u', v') 362 | _ => raise Match 363 val _ = assert (equal "TC") (fst (dest_const TC)) 364 val _ = assert (aconv u) u' 365 val _ = assert (aconv v) v' 366 val P = list_mk_abs([u,v], conseq) 367 val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) 368 in MATCH_MP_TAC tc_thm' (asl,w) 369 end 370 handle _ => raise mk_HOL_ERR "<top-level>" "TC_INDUCT_TAC" 371 "Unanticipated term structure" 372 in tac 373 end; 374 375val TC_STRONG_INDUCT0 = prove( 376 ``!R P. (!x y. R x y ==> P x y) /\ 377 (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==> 378 (!u v. TC R u v ==> P u v /\ TC R u v)``, 379 REPEAT GEN_TAC THEN STRIP_TAC THEN TC_INDUCT_TAC THEN 380 ASM_MESON_TAC [TC_RULES]); 381 382Theorem TC_STRONG_INDUCT[rule_induction]: 383 !R P. (!x y. R x y ==> P x y) /\ 384 (!x y z. P x y /\ P y z /\ TC R x y /\ TC R y z ==> P x z) ==> 385 (!u v. TC R u v ==> P u v) 386Proof REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT0 387QED 388 389val TC_STRONG_INDUCT_LEFT1_0 = prove( 390 ``!R P. (!x y. R x y ==> P x y) /\ 391 (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==> 392 (!u v. TC R u v ==> P u v /\ TC R u v)``, 393 REPEAT GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN 394 ASM_MESON_TAC [TC_RULES]); 395 396val TC_STRONG_INDUCT_RIGHT1_0 = prove( 397 ``!R P. (!x y. R x y ==> P x y) /\ 398 (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==> 399 (!u v. TC R u v ==> P u v /\ TC R u v)``, 400 REPEAT GEN_TAC THEN STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN 401 ASM_MESON_TAC [TC_RULES]); 402 403val TC_STRONG_INDUCT_LEFT1 = store_thm( 404 "TC_STRONG_INDUCT_LEFT1", 405 ``!R P. (!x y. R x y ==> P x y) /\ 406 (!x y z. R x y /\ P y z /\ TC R y z ==> P x z) ==> 407 (!u v. TC R u v ==> P u v)``, 408 REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT_LEFT1_0); 409val TC_STRONG_INDUCT_RIGHT1 = store_thm( 410 "TC_STRONG_INDUCT_RIGHT1", 411 ``!R P. (!x y. R x y ==> P x y) /\ 412 (!x y z. P x y /\ TC R x y /\ R y z ==> P x z) ==> 413 (!u v. TC R u v ==> P u v)``, 414 REPEAT STRIP_TAC THEN IMP_RES_TAC TC_STRONG_INDUCT_RIGHT1_0); 415 416(* can get inductive principles for properties which do not hold generally 417 but only for particular cases of x or y in TC R x y *) 418 419fun tc_ind_alt_tacs tc_ind_thm tq = 420 REPEAT STRIP_TAC THEN 421 POP_ASSUM (ASSUME_TAC o Ho_Rewrite.REWRITE_RULE [BETA_THM] 422 o Q.SPEC tq o GEN_ALL o MATCH_MP (REORDER_ANTS rev tc_ind_thm)) THEN 423 VALIDATE (POP_ASSUM (ACCEPT_TAC o UNDISCH)) THEN 424 POP_ASSUM (K ALL_TAC) THEN REPEAT STRIP_TAC THEN 425 TRY COND_CASES_TAC THEN 426 FULL_SIMP_TAC bool_ss [TC_SUBSET] THEN 427 RES_TAC THEN IMP_RES_TAC TC_RULES ; 428 429val TC_INDUCT_ALT_LEFT = Q.store_thm ("TC_INDUCT_ALT_LEFT", 430 `!R Q. (!x. R x b ==> Q x) /\ (!x y. R x y /\ Q y ==> Q x) ==> 431 !a. TC R a b ==> Q a`, 432 tc_ind_alt_tacs TC_INDUCT_LEFT1 `\x y. if y = b then Q x else TC R x y`) ; 433 434val TC_INDUCT_ALT_RIGHT = Q.store_thm ("TC_INDUCT_ALT_RIGHT", 435 `!R Q. (!y. R a y ==> Q y) /\ (!x y. Q x /\ R x y ==> Q y) ==> 436 !b. TC R a b ==> Q b`, 437 tc_ind_alt_tacs TC_INDUCT_RIGHT1 `\x y. if x = a then Q y else TC R x y`) ; 438 439val TC_lifts_monotonicities = store_thm( 440 "TC_lifts_monotonicities", 441 ``(!x y. R x y ==> R (f x) (f y)) ==> 442 !x y. TC R x y ==> TC R (f x) (f y)``, 443 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN 444 METIS_TAC [TC_RULES]); 445 446val TC_lifts_invariants = store_thm( 447 "TC_lifts_invariants", 448 ``(!x y. P x /\ R x y ==> P y) ==> (!x y. P x /\ TC R x y ==> P y)``, 449 STRIP_TAC THEN 450 Q_TAC SUFF_TAC `!x y. TC R x y ==> P x ==> P y` THEN1 METIS_TAC [] THEN 451 HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC []); 452 453val TC_lifts_equalities = store_thm( 454 "TC_lifts_equalities", 455 ``(!x y. R x y ==> (f x = f y)) ==> (!x y. TC R x y ==> (f x = f y))``, 456 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC []); 457 458(* generalisation of above results *) 459val TC_lifts_transitive_relations = store_thm( 460 "TC_lifts_transitive_relations", 461 ``(!x y. R x y ==> Q (f x) (f y)) /\ transitive Q ==> 462 (!x y. TC R x y ==> Q (f x) (f y))``, 463 STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN METIS_TAC [transitive_def]); 464 465val TC_implies_one_step = Q.store_thm( 466"TC_implies_one_step", 467`!x y . R^+ x y /\ x <> y ==> ?z. R x z /\ x <> z`, 468REWRITE_TAC [GSYM AND_IMP_INTRO] THEN 469HO_MATCH_MP_TAC TC_INDUCT THEN 470SRW_TAC [SatisfySimps.SATISFY_ss][] THEN 471PROVE_TAC []); 472 473val TC_RTC = store_thm( 474 "TC_RTC", 475 ``!R (x:'a) y. TC R x y ==> RTC R x y``, 476 GEN_TAC THEN TC_INDUCT_TAC THEN MESON_TAC [RTC_RULES, RTC_RTC]); 477 478val RTC_TC_RC = store_thm( 479 "RTC_TC_RC", 480 ``!R (x:'a) y. RTC R x y ==> RC R x y \/ TC R x y``, 481 GEN_TAC THEN HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN 482 REPEAT STRIP_TAC THENL [ 483 REWRITE_TAC [RC_DEF], 484 FULL_SIMP_TAC bool_ss [RC_DEF] THEN ASM_MESON_TAC [TC_RULES], 485 ASM_MESON_TAC [TC_RULES] 486 ]); 487 488val TC_RC_EQNS = store_thm( 489 "TC_RC_EQNS", 490 ``!R:'a->'a->bool. (RC (TC R) = RTC R) /\ (TC (RC R) = RTC R)``, 491 REPEAT STRIP_TAC THEN 492 CONV_TAC (Q.X_FUN_EQ_CONV `u`) THEN GEN_TAC THEN 493 CONV_TAC (Q.X_FUN_EQ_CONV `v`) THEN GEN_TAC THEN 494 EQ_TAC THENL [ 495 REWRITE_TAC [RC_DEF] THEN MESON_TAC [TC_RTC, RTC_RULES], 496 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN 497 HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN 498 SIMP_TAC bool_ss [RC_DEF] THEN MESON_TAC [TC_RULES], 499 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN 500 HO_MATCH_MP_TAC TC_INDUCT THEN MESON_TAC [RC_RTC, RTC_RTC], 501 Q.ID_SPEC_TAC `v` THEN Q.ID_SPEC_TAC `u` THEN 502 HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [TC_RULES, RC_DEF] 503 ]); 504 505(* can get inductive principles for properties which do not hold generally 506 but only for particular cases of x or y in RTC R x y *) 507 508Theorem RTC_ALT_DEF: 509 !R a b. RTC R a b <=> !Q. Q b /\ (!x y. R x y /\ Q y ==> Q x) ==> Q a 510Proof 511 REWRITE_TAC [EQ_IMP_THM] THEN CONV_TAC (REDEPTH_CONV FORALL_AND_CONV) THEN 512 CONJ_TAC THEN1 (GEN_TAC THEN Induct_on `RTC` THEN METIS_TAC[]) THEN 513 REPEAT GEN_TAC THEN 514 DISCH_THEN (Q.SPEC_THEN `\z. RTC R z b` (MATCH_MP_TAC o BETA_RULE)) THEN 515 METIS_TAC[RTC_RULES] 516QED 517 518val RTC_ALT_INDUCT = Q.store_thm ("RTC_ALT_INDUCT", 519 `!R Q b. Q b /\ (!x y. R x y /\ Q y ==> Q x) ==> !x. RTC R x b ==> Q x`, 520 REWRITE_TAC [RTC_ALT_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC) ; 521 522val RTC_ALT_RIGHT_DEF = Q.store_thm ("RTC_ALT_RIGHT_DEF", 523 `!R a b. RTC R a b = !Q. Q a /\ (!y z. Q y /\ R y z ==> Q z) ==> Q b`, 524 REWRITE_TAC [RTC_ALT_DEF] THEN REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 525 FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `$~ o Q`) THEN 526 REV_FULL_SIMP_TAC bool_ss [combinTheory.o_THM] THEN RES_TAC) ; 527 528val RTC_ALT_RIGHT_INDUCT = Q.store_thm ("RTC_ALT_RIGHT_INDUCT", 529 `!R Q a. Q a /\ (!y z. Q y /\ R y z ==> Q z) ==> !z. RTC R a z ==> Q z`, 530 REWRITE_TAC [RTC_ALT_RIGHT_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC) ; 531 532val RTC_INDUCT_RIGHT1 = store_thm( 533 "RTC_INDUCT_RIGHT1", 534 ``!R P. (!x. P x x) /\ 535 (!x y z. P x y /\ R y z ==> P x z) ==> 536 (!x y. RTC R x y ==> P x y)``, 537 REPEAT STRIP_TAC THEN 538 FIRST_X_ASSUM (irule o MATCH_MP (REORDER_ANTS rev RTC_ALT_RIGHT_INDUCT)) THEN 539 ASM_REWRITE_TAC []) ; 540 541val RTC_RULES_RIGHT1 = store_thm( 542 "RTC_RULES_RIGHT1", 543 ``!R. (!x. RTC R x x) /\ (!x y z. RTC R x y /\ R y z ==> RTC R x z)``, 544 REWRITE_TAC [RTC_ALT_RIGHT_DEF] THEN 545 REPEAT STRIP_TAC THEN RES_TAC THEN RES_TAC) ; 546 547val RTC_STRONG_INDUCT_RIGHT1 = store_thm( 548 "RTC_STRONG_INDUCT_RIGHT1", 549 ``!R P. (!x. P x x) /\ 550 (!x y z. P x y /\ RTC R x y /\ R y z ==> P x z) ==> 551 (!x y. RTC R x y ==> P x y)``, 552 REPEAT STRIP_TAC THEN 553 Q_TAC SUFF_TAC `P x y /\ RTC R x y` THEN1 MESON_TAC [] THEN 554 Q.UNDISCH_THEN `RTC R x y` MP_TAC THEN 555 MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN 556 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN 557 ASM_MESON_TAC [RTC_RULES_RIGHT1]); 558 559 560val EXTEND_RTC_TC = store_thm( 561 "EXTEND_RTC_TC", 562 ``!R x y z. R x y /\ RTC R y z ==> TC R x z``, 563 GEN_TAC THEN 564 Q_TAC SUFF_TAC `!y z. RTC R y z ==> !x. R x y ==> TC R x z` THEN1 565 MESON_TAC [] THEN 566 HO_MATCH_MP_TAC RTC_INDUCT THEN 567 MESON_TAC [TC_RULES]); 568 569 570val EXTEND_RTC_TC_EQN = store_thm( 571 "EXTEND_RTC_TC_EQN", 572 ``!R x z. TC R x z = ?y. (R x y /\ RTC R y z)``, 573 GEN_TAC THEN 574 Q_TAC SUFF_TAC `!x z. TC R x z ==> ?y. R x y /\ RTC R y z` THEN1 575 MESON_TAC [EXTEND_RTC_TC] THEN 576 HO_MATCH_MP_TAC TC_INDUCT THEN 577 PROVE_TAC[RTC_RULES, RTC_TRANSITIVE, transitive_def, 578 RTC_RULES_RIGHT1]); 579 580Theorem EXTEND_RTC_TC_RIGHT1: 581 !R x y z. RTC R x y /\ R y z ==> TC R x z 582Proof 583 GEN_TAC THEN 584 Q_TAC SUFF_TAC `!x y. RTC R x y ==> !z. R y z ==> TC R x z` THEN1 585 MESON_TAC [] THEN 586 HO_MATCH_MP_TAC RTC_INDUCT_RIGHT1 THEN 587 MESON_TAC [TC_RULES] 588QED 589 590Theorem EXTEND_RTC_TC_RIGHT1_EQN: 591 !R x z. TC R x z = ?y. (RTC R x y /\ R y z) 592Proof 593 GEN_TAC THEN 594 Q_TAC SUFF_TAC `!x z. TC R x z ==> ?y. RTC R x y /\ R y z` THEN1 595 MESON_TAC [EXTEND_RTC_TC_RIGHT1] THEN 596 HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN 597 PROVE_TAC[RTC_RULES, RTC_TRANSITIVE, transitive_def, 598 RTC_RULES_RIGHT1] 599QED 600 601val reflexive_RC_identity = store_thm( 602 "reflexive_RC_identity", 603 ``!R. reflexive R ==> (RC R = R)``, 604 SIMP_TAC bool_ss [reflexive_def, RC_DEF, FUN_EQ_THM] THEN MESON_TAC []); 605 606val symmetric_SC_identity = store_thm( 607 "symmetric_SC_identity", 608 ``!R. symmetric R ==> (SC R = R)``, 609 SIMP_TAC bool_ss [symmetric_def, SC_DEF, FUN_EQ_THM]); 610 611val transitive_TC_identity = store_thm( 612 "transitive_TC_identity", 613 ``!R. transitive R ==> (TC R = R)``, 614 SIMP_TAC bool_ss [transitive_def, FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM, 615 TC_RULES] THEN GEN_TAC THEN STRIP_TAC THEN 616 HO_MATCH_MP_TAC TC_INDUCT THEN ASM_MESON_TAC []); 617 618val RC_IDEM = store_thm( 619 "RC_IDEM", 620 ``!R:'a->'a->bool. RC (RC R) = RC R``, 621 SIMP_TAC bool_ss [RC_REFLEXIVE, reflexive_RC_identity]); 622val _ = export_rewrites ["RC_IDEM"] 623 624val SC_IDEM = store_thm( 625 "SC_IDEM", 626 ``!R:'a->'a->bool. SC (SC R) = SC R``, 627 SIMP_TAC bool_ss [SC_SYMMETRIC, symmetric_SC_identity]); 628val _ = export_rewrites ["SC_IDEM"] 629 630val TC_IDEM = store_thm( 631 "TC_IDEM", 632 ``!R:'a->'a->bool. TC (TC R) = TC R``, 633 SIMP_TAC bool_ss [TC_TRANSITIVE, transitive_TC_identity]); 634val _ = export_rewrites ["TC_IDEM"] 635 636val RC_MOVES_OUT = store_thm( 637 "RC_MOVES_OUT", 638 ``!R. (SC (RC R) = RC (SC R)) /\ (RC (RC R) = RC R) /\ 639 (TC (RC R) = RC (TC R))``, 640 REWRITE_TAC [TC_RC_EQNS, RC_IDEM] THEN 641 SIMP_TAC bool_ss [SC_DEF, RC_DEF, FUN_EQ_THM] THEN MESON_TAC []); 642 643val symmetric_TC = store_thm( 644 "symmetric_TC", 645 ``!R. symmetric R ==> symmetric (TC R)``, 646 REWRITE_TAC [symmetric_def] THEN GEN_TAC THEN STRIP_TAC THEN 647 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 648 HO_MATCH_MP_TAC TC_INDUCT, 649 CONV_TAC SWAP_VARS_CONV THEN HO_MATCH_MP_TAC TC_INDUCT 650 ] THEN ASM_MESON_TAC [TC_RULES]); 651 652val reflexive_TC = store_thm( 653 "reflexive_TC", 654 ``!R. reflexive R ==> reflexive (TC R)``, 655 PROVE_TAC [reflexive_def,TC_SUBSET]); 656 657val EQC_EQUIVALENCE = store_thm( 658 "EQC_EQUIVALENCE", 659 ``!R. equivalence (EQC R)``, 660 REWRITE_TAC [equivalence_def, EQC_DEF, RC_REFLEXIVE, symmetric_RC] THEN 661 MESON_TAC [symmetric_TC, TC_RC_EQNS, TC_TRANSITIVE, SC_SYMMETRIC]); 662val _ = export_rewrites ["EQC_EQUIVALENCE"] 663 664val EQC_IDEM = store_thm( 665 "EQC_IDEM", 666 ``!R:'a->'a->bool. EQC(EQC R) = EQC R``, 667 SIMP_TAC bool_ss [EQC_DEF, RC_MOVES_OUT, symmetric_SC_identity, 668 symmetric_TC, SC_SYMMETRIC, TC_IDEM]); 669val _ = export_rewrites ["EQC_IDEM"] 670 671 672val RTC_IDEM = store_thm( 673 "RTC_IDEM", 674 ``!R:'a->'a->bool. RTC (RTC R) = RTC R``, 675 SIMP_TAC bool_ss [GSYM TC_RC_EQNS, RC_MOVES_OUT, TC_IDEM]); 676val _ = export_rewrites ["RTC_IDEM"] 677 678val RTC_CASES1 = store_thm( 679 "RTC_CASES1", 680 ``!R (x:'a) y. RTC R x y <=> (x = y) \/ ?u. R x u /\ RTC R u y``, 681 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 682 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES], 683 MESON_TAC [RTC_RULES] 684 ]); 685 686val RTC_CASES_TC = store_thm( 687 "RTC_CASES_TC", 688 ``!R x y. R^* x y <=> (x = y) \/ R^+ x y``, 689 METIS_TAC [EXTEND_RTC_TC_EQN, RTC_CASES1]); 690 691val RTC_CASES2 = store_thm( 692 "RTC_CASES2", 693 ``!R (x:'a) y. RTC R x y <=> (x = y) \/ ?u. RTC R x u /\ R u y``, 694 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 695 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES], 696 MESON_TAC [RTC_RULES, RTC_SUBSET, RTC_RTC] 697 ]); 698 699val RTC_CASES_RTC_TWICE = store_thm( 700 "RTC_CASES_RTC_TWICE", 701 ``!R (x:'a) y. RTC R x y <=> ?u. RTC R x u /\ RTC R u y``, 702 SIMP_TAC bool_ss [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 703 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN MESON_TAC [RTC_RULES], 704 MESON_TAC [RTC_RULES, RTC_SUBSET, RTC_RTC] 705 ]); 706 707val TC_CASES1_E = 708Q.store_thm 709("TC_CASES1_E", 710 `!R x z. TC R x z ==> R x z \/ ?y:'a. R x y /\ TC R y z`, 711GEN_TAC 712 THEN TC_INDUCT_TAC 713 THEN MESON_TAC [REWRITE_RULE[transitive_def] TC_TRANSITIVE, TC_SUBSET]); 714 715val TC_CASES1 = store_thm( 716 "TC_CASES1", 717 ``TC R x z <=> R x z \/ ?y:'a. R x y /\ TC R y z``, 718 MESON_TAC[TC_RULES, TC_CASES1_E]) 719 720val TC_CASES2_E = 721Q.store_thm 722("TC_CASES2_E", 723 `!R x z. TC R x z ==> R x z \/ ?y:'a. TC R x y /\ R y z`, 724GEN_TAC 725 THEN TC_INDUCT_TAC 726 THEN MESON_TAC [REWRITE_RULE[transitive_def] TC_TRANSITIVE, TC_SUBSET]); 727 728val TC_CASES2 = store_thm( 729 "TC_CASES2", 730 ``TC R x z <=> R x z \/ ?y:'a. TC R x y /\ R y z``, 731 MESON_TAC [TC_RULES, TC_CASES2_E]); 732 733val TC_MONOTONE = store_thm( 734 "TC_MONOTONE[mono]", 735 ``(!x y. R x y ==> Q x y) ==> TC R x y ==> TC Q x y``, 736 REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN 737 TC_INDUCT_TAC THEN ASM_MESON_TAC [TC_RULES]); 738 739val RTC_MONOTONE = store_thm( 740 "RTC_MONOTONE[mono]", 741 ``(!x y. R x y ==> Q x y) ==> RTC R x y ==> RTC Q x y``, 742 REPEAT GEN_TAC THEN STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN 743 HO_MATCH_MP_TAC RTC_INDUCT THEN ASM_MESON_TAC [RTC_RULES]); 744 745val EQC_INDUCTION = store_thm( 746 "EQC_INDUCTION", 747 ``!R P. (!x y. R x y ==> P x y) /\ 748 (!x. P x x) /\ 749 (!x y. P x y ==> P y x) /\ 750 (!x y z. P x y /\ P y z ==> P x z) ==> 751 (!x y. EQC R x y ==> P x y)``, 752 REWRITE_TAC [EQC_DEF] THEN REPEAT STRIP_TAC THEN 753 FULL_SIMP_TAC bool_ss [RC_DEF] THEN 754 Q.PAT_X_ASSUM `TC _ x y` MP_TAC THEN 755 MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN 756 HO_MATCH_MP_TAC TC_INDUCT THEN REWRITE_TAC [SC_DEF] THEN 757 ASM_MESON_TAC []); 758 759val EQC_REFL = store_thm( 760 "EQC_REFL", 761 ``!R x. EQC R x x``, 762 SRW_TAC [][EQC_DEF, RC_DEF]); 763val _ = export_rewrites ["EQC_REFL"] 764 765val EQC_R = store_thm( 766 "EQC_R", 767 ``!R x y. R x y ==> EQC R x y``, 768 SRW_TAC [][EQC_DEF, RC_DEF] THEN 769 DISJ2_TAC THEN MATCH_MP_TAC TC_SUBSET THEN 770 SRW_TAC [][SC_DEF]); 771 772val EQC_SYM = store_thm( 773 "EQC_SYM", 774 ``!R x y. EQC R x y ==> EQC R y x``, 775 SRW_TAC [][EQC_DEF, RC_DEF] THEN 776 Q.SUBGOAL_THEN `symmetric (TC (SC R))` ASSUME_TAC THEN1 777 SRW_TAC [][SC_SYMMETRIC, symmetric_TC] THEN 778 PROVE_TAC [symmetric_def]); 779 780val EQC_TRANS = store_thm( 781 "EQC_TRANS", 782 ``!R x y z. EQC R x y /\ EQC R y z ==> EQC R x z``, 783 REPEAT GEN_TAC THEN 784 Q_TAC SUFF_TAC `transitive (EQC R)` THEN1 PROVE_TAC [transitive_def] THEN 785 SRW_TAC [][EQC_DEF, transitive_RC, TC_TRANSITIVE]) 786 787val transitive_EQC = Q.store_thm( 788"transitive_EQC", 789`transitive (EQC R)`, 790PROVE_TAC [transitive_def,EQC_TRANS]); 791 792val symmetric_EQC = Q.store_thm( 793"symmetric_EQC", 794`symmetric (EQC R)`, 795PROVE_TAC [symmetric_def,EQC_SYM]); 796 797val reflexive_EQC = Q.store_thm( 798"reflexive_EQC", 799`reflexive (EQC R)`, 800PROVE_TAC [reflexive_def,EQC_REFL]); 801 802Theorem EQC_MOVES_IN[simp]: 803 !R. (EQC (RC R) = EQC R) /\ (EQC (SC R) = EQC R) /\ (EQC (TC R) = EQC R) 804Proof 805 SRW_TAC [][EQC_DEF,RC_MOVES_OUT,SC_IDEM] THEN 806 AP_TERM_TAC THEN 807 SRW_TAC [][FUN_EQ_THM] THEN 808 REVERSE EQ_TAC THEN 809 MAP_EVERY Q.ID_SPEC_TAC [`x'`,`x`] THEN 810 HO_MATCH_MP_TAC TC_INDUCT THEN1 (SRW_TAC [][SC_DEF] THEN 811 PROVE_TAC [TC_RULES,SC_DEF]) THEN 812 REVERSE (SRW_TAC [][SC_DEF]) THEN1 813 PROVE_TAC [TC_RULES,SC_DEF] THEN 814 Q.MATCH_ASSUM_RENAME_TAC `R^+ a b` THEN 815 POP_ASSUM MP_TAC THEN 816 MAP_EVERY Q.ID_SPEC_TAC [`b`,`a`] THEN 817 HO_MATCH_MP_TAC TC_INDUCT THEN 818 SRW_TAC [][SC_DEF] THEN 819 PROVE_TAC [TC_RULES,SC_DEF] 820QED 821 822Theorem STRONG_EQC_INDUCTION[rule_induction]: 823 !R P. (!x y. R x y ==> P x y) /\ 824 (!x. P x x) /\ 825 (!x y. EQC R x y /\ P x y ==> P y x) /\ 826 (!x y z. P x y /\ P y z /\ EQC R x y /\ EQC R y z ==> P x z) 827 ==> 828 !x y. EQC R x y ==> P x y 829Proof 830 REPEAT GEN_TAC THEN STRIP_TAC THEN 831 Q_TAC SUFF_TAC `!x y. EQC R x y ==> EQC R x y /\ P x y` 832 THEN1 PROVE_TAC [] THEN 833 HO_MATCH_MP_TAC EQC_INDUCTION THEN 834 PROVE_TAC [EQC_R, EQC_REFL, EQC_SYM, EQC_TRANS] 835QED 836 837val ALT_equivalence = store_thm( 838 "ALT_equivalence", 839 ``!R. equivalence R = !x y. R x y = (R x = R y)``, 840 REWRITE_TAC [equivalence_def, reflexive_def, symmetric_def, 841 transitive_def, FUN_EQ_THM, EQ_IMP_THM] THEN 842 MESON_TAC []); 843 844val EQC_MONOTONE = store_thm( 845 "EQC_MONOTONE[mono]", 846 ``(!x y. R x y ==> R' x y) ==> EQC R x y ==> EQC R' x y``, 847 STRIP_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`y`, `x`] THEN 848 HO_MATCH_MP_TAC STRONG_EQC_INDUCTION THEN 849 METIS_TAC [EQC_R, EQC_TRANS, EQC_SYM, EQC_REFL]); 850 851val RTC_EQC = store_thm( 852 "RTC_EQC", 853 ``!x y. RTC R x y ==> EQC R x y``, 854 HO_MATCH_MP_TAC RTC_INDUCT THEN METIS_TAC [EQC_R, EQC_REFL, EQC_TRANS]); 855 856val RTC_lifts_monotonicities = store_thm( 857 "RTC_lifts_monotonicities", 858 ``(!x y. R x y ==> R (f x) (f y)) ==> 859 !x y. R^* x y ==> R^* (f x) (f y)``, 860 STRIP_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN 861 METIS_TAC [RTC_RULES]); 862 863val RTC_lifts_reflexive_transitive_relations = Q.store_thm( 864 "RTC_lifts_reflexive_transitive_relations", 865 `(!x y. R x y ==> Q (f x) (f y)) /\ reflexive Q /\ transitive Q ==> 866 !x y. R^* x y ==> Q (f x) (f y)`, 867 STRIP_TAC THEN 868 HO_MATCH_MP_TAC RTC_INDUCT THEN 869 FULL_SIMP_TAC bool_ss [reflexive_def,transitive_def] THEN 870 METIS_TAC []); 871 872val RTC_lifts_equalities = Q.store_thm( 873 "RTC_lifts_equalities", 874 `(!x y. R x y ==> (f x = f y)) ==> !x y. R^* x y ==> (f x = f y)`, 875 STRIP_TAC THEN 876 HO_MATCH_MP_TAC RTC_lifts_reflexive_transitive_relations THEN 877 ASM_SIMP_TAC bool_ss [reflexive_def,transitive_def]); 878 879val RTC_lifts_invariants = Q.store_thm( 880 "RTC_lifts_invariants", 881 `(!x y. P x /\ R x y ==> P y) ==> !x y. P x /\ R^* x y ==> P y`, 882 STRIP_TAC THEN 883 REWRITE_TAC [Once CONJ_COMM] THEN 884 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN 885 HO_MATCH_MP_TAC RTC_INDUCT THEN 886 METIS_TAC []); 887 888(*---------------------------------------------------------------------------* 889 * Wellfounded relations. Wellfoundedness: Every non-empty set has an * 890 * R-minimal element. Applications of wellfoundedness to specific types * 891 * (numbers, lists, etc.) can be found in the respective theories. * 892 *---------------------------------------------------------------------------*) 893 894val WF_DEF = 895Q.new_definition 896 ("WF_DEF", `WF R = !B. (?w:'a. B w) ==> ?min. B min /\ !b. R b min ==> ~B b`); 897val _ = OpenTheoryMap.OpenTheory_const_name 898 {const={Thy="relation",Name="WF"},name=(["Relation"],"wellFounded")} 899 900(*---------------------------------------------------------------------------*) 901(* Misc. proof tools, from pre-automation days. *) 902(*---------------------------------------------------------------------------*) 903 904val USE_TAC = IMP_RES_THEN(fn th => ONCE_REWRITE_TAC[th]); 905 906val NNF_CONV = 907 let val DE_MORGAN = REWRITE_CONV 908 [TAUT `~(x==>y) = (x /\ ~y)`, 909 TAUT `~x \/ y <=> (x ==> y)`,DE_MORGAN_THM] 910 val QUANT_CONV = NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV 911 in REDEPTH_CONV (QUANT_CONV ORELSEC CHANGED_CONV DE_MORGAN) 912 end; 913 914val NNF_TAC = CONV_TAC NNF_CONV; 915 916 917(*---------------------------------------------------------------------------* 918 * * 919 * WELL FOUNDED INDUCTION * 920 * * 921 * Proof: For RAA, assume there's a z s.t. ~P z. By wellfoundedness, * 922 * there's a minimal object w s.t. ~P w. (P holds of all objects "less" * 923 * than w.) By the other assumption, i.e., * 924 * * 925 * !x. (!y. R y x ==> P y) ==> P x, * 926 * * 927 * P w holds, QEA. * 928 * * 929 *---------------------------------------------------------------------------*) 930 931val WF_INDUCTION_THM = 932Q.store_thm("WF_INDUCTION_THM", 933`!(R:'a->'a->bool). 934 WF R ==> !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x`, 935GEN_TAC THEN REWRITE_TAC[WF_DEF] 936 THEN DISCH_THEN (fn th => GEN_TAC THEN (MP_TAC (Q.SPEC `\x:'a. ~P x` th))) 937 THEN BETA_TAC THEN REWRITE_TAC[] THEN STRIP_TAC THEN CONV_TAC CONTRAPOS_CONV 938 THEN NNF_TAC THEN STRIP_TAC THEN RES_TAC 939 THEN Q.EXISTS_TAC`min` THEN ASM_REWRITE_TAC[]); 940 941 942val INDUCTION_WF_THM = Q.store_thm("INDUCTION_WF_THM", 943`!R:'a->'a->bool. 944 (!P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x) ==> WF R`, 945GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[WF_DEF] THEN GEN_TAC THEN 946 CONV_TAC CONTRAPOS_CONV THEN NNF_TAC THEN 947 DISCH_THEN (fn th => POP_ASSUM (MATCH_MP_TAC o BETA_RULE o Q.SPEC`\w. ~B w`) 948 THEN ASSUME_TAC th) THEN GEN_TAC THEN 949 CONV_TAC CONTRAPOS_CONV THEN NNF_TAC 950 THEN POP_ASSUM MATCH_ACCEPT_TAC); 951 952val WF_EQ_INDUCTION_THM = Q.store_thm("WF_EQ_INDUCTION_THM", 953 `!R:'a->'a->bool. 954 WF R = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. P x`, 955GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL 956 [IMP_RES_TAC WF_INDUCTION_THM, IMP_RES_TAC INDUCTION_WF_THM]); 957 958 959(*--------------------------------------------------------------------------- 960 * A tactic for doing wellfounded induction. Lifted and adapted from 961 * John Harrison's definition of WO_INDUCT_TAC in the wellordering library. 962 *---------------------------------------------------------------------------*) 963 964val _ = Parse.hide "C"; 965 966val WF_INDUCT_TAC = 967 let val wf_thm0 = CONV_RULE (ONCE_DEPTH_CONV ETA_CONV) 968 (REWRITE_RULE [TAUT`A==>B==>C <=> A/\B==>C`] 969 (CONV_RULE (ONCE_DEPTH_CONV RIGHT_IMP_FORALL_CONV) 970 WF_INDUCTION_THM)) 971 val [R,P] = fst(strip_forall(concl wf_thm0)) 972 val wf_thm1 = GENL [P,R](SPEC_ALL wf_thm0) 973 fun tac (asl,w) = 974 let val (Rator,Rand) = dest_comb w 975 val _ = assert (equal "!") (fst (dest_const Rator)) 976 val thi = ISPEC Rand wf_thm1 977 fun eqRand t = Term.compare(Rand,t) = EQUAL 978 val thf = CONV_RULE(ONCE_DEPTH_CONV 979 (BETA_CONV o assert (eqRand o rator))) thi 980 in MATCH_MP_TAC thf (asl,w) 981 end 982 handle _ => raise mk_HOL_ERR "" "WF_INDUCT_TAC" 983 "Unanticipated term structure" 984 in tac 985 end; 986 987 988val ex_lem = Q.prove(`!x. (?y. y = x) /\ ?y. x=y`, 989GEN_TAC THEN CONJ_TAC THEN Q.EXISTS_TAC`x` THEN REFL_TAC); 990 991val WF_NOT_REFL = Q.store_thm("WF_NOT_REFL", 992`!R x y. WF R ==> R x y ==> ~(x=y)`, 993REWRITE_TAC[WF_DEF] 994 THEN REPEAT GEN_TAC 995 THEN DISCH_THEN (MP_TAC o Q.SPEC`\x. x=y`) 996 THEN BETA_TAC THEN REWRITE_TAC[ex_lem] 997 THEN STRIP_TAC 998 THEN Q.UNDISCH_THEN `min=y` SUBST_ALL_TAC 999 THEN DISCH_TAC THEN RES_TAC); 1000 1001(* delete this or the previous if we abbreviate irreflexive *) 1002val WF_irreflexive = store_thm( 1003 "WF_irreflexive", 1004 ``WF R ==> irreflexive R``, 1005 METIS_TAC [WF_NOT_REFL, irreflexive_def]); 1006 1007(*--------------------------------------------------------------------------- 1008 * Some combinators for wellfounded relations. 1009 *---------------------------------------------------------------------------*) 1010 1011(*--------------------------------------------------------------------------- 1012 * The empty relation is wellfounded. 1013 *---------------------------------------------------------------------------*) 1014 1015val EMPTY_REL_DEF = 1016Q.new_definition 1017 ("EMPTY_REL_DEF", `EMPTY_REL (x:'a) (y:'a) = F`); 1018val _ = export_rewrites ["EMPTY_REL_DEF"] 1019Overload REMPTY = ``EMPTY_REL`` 1020val _ = Unicode.unicode_version {u = UnicodeChars.emptyset ^ UnicodeChars.sub_r, 1021 tmnm = "EMPTY_REL"} 1022 1023 1024val WF_EMPTY_REL = 1025Q.store_thm 1026 ("WF_EMPTY_REL", 1027 `WF (EMPTY_REL:'a->'a->bool)`, 1028REWRITE_TAC[EMPTY_REL_DEF,WF_DEF]); 1029 1030 1031(*--------------------------------------------------------------------------- 1032 * Subset: if R is a WF relation and P is a subrelation of R, then 1033 * P is a wellfounded relation. 1034 *---------------------------------------------------------------------------*) 1035 1036val WF_SUBSET = Q.store_thm("WF_SUBSET", 1037`!(R:'a->'a->bool) P. 1038 WF R /\ (!x y. P x y ==> R x y) ==> WF P`, 1039REWRITE_TAC[WF_DEF] 1040 THEN REPEAT STRIP_TAC 1041 THEN RES_TAC 1042 THEN Q.EXISTS_TAC`min` 1043 THEN ASM_REWRITE_TAC[] 1044 THEN GEN_TAC 1045 THEN DISCH_TAC 1046 THEN REPEAT RES_TAC); 1047 1048 1049(*--------------------------------------------------------------------------- 1050 * The transitive closure of a wellfounded relation is wellfounded. 1051 * I got the clue about the witness from Peter Johnstone's book: 1052 * "Notes on Logic and Set Theory". An alternative proof that Bernhard 1053 * Schaetz showed me uses well-founded induction then case analysis. In that 1054 * approach, the IH must be quantified over all sets, so that we can 1055 * specialize it later to an extension of B. 1056 *---------------------------------------------------------------------------*) 1057 1058val WF_TC = Q.store_thm("WF_TC", 1059`!R:'a->'a->bool. WF R ==> WF(TC R)`, 1060GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[WF_DEF] 1061 THEN NNF_TAC THEN DISCH_THEN (Q.X_CHOOSE_THEN `B` MP_TAC) 1062 THEN DISCH_THEN (fn th => 1063 Q.EXISTS_TAC`\m:'a. ?a z. B a /\ TC R a m /\ TC R m z /\ B z` 1064 THEN BETA_TAC THEN CONJ_TAC THEN STRIP_ASSUME_TAC th) 1065 THENL 1066 [RES_TAC THEN RES_TAC THEN MAP_EVERY Q.EXISTS_TAC[`b`, `b'`, `w`] 1067 THEN ASM_REWRITE_TAC[], 1068 Q.X_GEN_TAC`m` THEN STRIP_TAC THEN Q.UNDISCH_TAC`TC R (a:'a) m` 1069 THEN DISCH_THEN(fn th => STRIP_ASSUME_TAC 1070 (CONJ th (MATCH_MP TC_CASES2_E th))) 1071 THENL 1072 [ Q.EXISTS_TAC`a` THEN ASM_REWRITE_TAC[] THEN RES_TAC 1073 THEN MAP_EVERY Q.EXISTS_TAC [`b'`, `z`] THEN ASM_REWRITE_TAC[], 1074 Q.EXISTS_TAC`y` THEN ASM_REWRITE_TAC[] 1075 THEN MAP_EVERY Q.EXISTS_TAC[`a`,`z`] THEN ASM_REWRITE_TAC[] 1076 THEN IMP_RES_TAC TC_SUBSET] 1077 THEN 1078 IMP_RES_TAC(REWRITE_RULE[transitive_def] TC_TRANSITIVE)]); 1079 1080val WF_TC_EQN = store_thm( 1081 "WF_TC_EQN", 1082 ``WF (R^+) <=> WF R``, 1083 METIS_TAC [WF_TC, TC_SUBSET, WF_SUBSET]); 1084 1085val WF_noloops = store_thm( 1086 "WF_noloops", 1087 ``WF R ==> TC R x y ==> x <> y``, 1088 METIS_TAC [WF_NOT_REFL, WF_TC_EQN]); 1089 1090val WF_antisymmetric = store_thm( 1091 "WF_antisymmetric", 1092 ``WF R ==> antisymmetric R``, 1093 REWRITE_TAC [antisymmetric_def] THEN STRIP_TAC THEN 1094 MAP_EVERY Q.X_GEN_TAC [`a`, `b`] THEN 1095 STRIP_TAC THEN Q_TAC SUFF_TAC `TC R a a` THEN1 METIS_TAC [WF_noloops] THEN 1096 METIS_TAC [TC_RULES]); 1097 1098(*--------------------------------------------------------------------------- 1099 * Inverse image theorem: mapping into a wellfounded relation gives a 1100 * derived well founded relation. A "size" mapping, like "length" for 1101 * lists is such a relation. 1102 * 1103 * Proof. 1104 * f is total and maps from one n.e. set (Alpha) into another (Beta which is 1105 * "\y. ?x:'a. Alpha x /\ (f x = y)"). Since the latter is n.e. 1106 * and has a wellfounded relation R on it, it has an R-minimal element 1107 * (call it "min"). There exists an x:'a s.t. f x = min. Such an x is an 1108 * R1-minimal element of Alpha (R1 is our derived ordering.) Why is x 1109 * R1-minimal in Alpha? Well, if there was a y:'a s.t. R1 y x, then f y 1110 * would not be in Beta (being less than f x, i.e., min). If f y wasn't in 1111 * Beta, then y couldn't be in Alpha. 1112 *---------------------------------------------------------------------------*) 1113 1114val inv_image_def = 1115Q.new_definition 1116("inv_image_def", 1117 `inv_image R (f:'a->'b) = \x y. R (f x) (f y):bool`); 1118 1119val inv_image_thm = save_thm( 1120 "inv_image_thm", 1121 SIMP_RULE bool_ss [FUN_EQ_THM] inv_image_def) 1122val _ = export_rewrites ["inv_image_thm"] 1123 1124val WF_inv_image = Q.store_thm("WF_inv_image", 1125`!R (f:'a->'b). WF R ==> WF (inv_image R f)`, 1126REPEAT GEN_TAC 1127 THEN REWRITE_TAC[inv_image_def,WF_DEF] THEN BETA_TAC 1128 THEN DISCH_THEN (fn th => Q.X_GEN_TAC`Alpha` THEN STRIP_TAC THEN MP_TAC th) 1129 THEN Q.SUBGOAL_THEN`?w:'b. (\y. ?x:'a. Alpha x /\ (f x = y)) w` MP_TAC 1130 THENL 1131 [ BETA_TAC 1132 THEN MAP_EVERY Q.EXISTS_TAC[`f(w:'a)`,`w`] 1133 THEN ASM_REWRITE_TAC[], 1134 DISCH_THEN (fn th => DISCH_THEN (MP_TAC o C MATCH_MP th)) THEN BETA_TAC 1135 THEN NNF_TAC 1136 THEN REPEAT STRIP_TAC 1137 THEN Q.EXISTS_TAC`x` 1138 THEN ASM_REWRITE_TAC[] 1139 THEN GEN_TAC 1140 THEN DISCH_THEN (ANTE_RES_THEN (MP_TAC o Q.SPEC`b`)) 1141 THEN REWRITE_TAC[]]); 1142 1143val total_inv_image = store_thm( 1144 "total_inv_image", 1145 ``!R f. total R ==> total (inv_image R f)``, 1146 SRW_TAC[][total_def, inv_image_def]); 1147val _ = export_rewrites ["total_inv_image"] 1148 1149val reflexive_inv_image = store_thm( 1150 "reflexive_inv_image", 1151 ``!R f. reflexive R ==> reflexive (inv_image R f)``, 1152 SRW_TAC[][reflexive_def, inv_image_def]); 1153val _ = export_rewrites ["reflexive_inv_image"] 1154 1155val symmetric_inv_image = store_thm( 1156 "symmetric_inv_image", 1157 ``!R f. symmetric R ==> symmetric (inv_image R f)``, 1158 SRW_TAC[][symmetric_def, inv_image_def]); 1159val _ = export_rewrites ["symmetric_inv_image"] 1160 1161val transitive_inv_image = store_thm( 1162 "transitive_inv_image", 1163 ``!R f. transitive R ==> transitive (inv_image R f)``, 1164 SRW_TAC[][transitive_def, inv_image_def] THEN METIS_TAC[]); 1165val _ = export_rewrites ["transitive_inv_image"] 1166 1167(*--------------------------------------------------------------------------- 1168 * Now the WF recursion theorem. Based on Tobias Nipkow's Isabelle development 1169 * of wellfounded recursion, which itself is a generalization of Mike 1170 * Gordon's HOL development of the primitive recursion theorem. 1171 *---------------------------------------------------------------------------*) 1172 1173val RESTRICT_DEF = 1174Q.new_definition 1175("RESTRICT_DEF", 1176 `RESTRICT (f:'a->'b) R (x:'a) = \y:'a. if R y x then f y else ARB`); 1177 1178 1179(*--------------------------------------------------------------------------- 1180 * Obvious, but crucially useful. Unary case. Handling the n-ary case might 1181 * be messy! 1182 *---------------------------------------------------------------------------*) 1183 1184val RESTRICT_LEMMA = Q.store_thm("RESTRICT_LEMMA", 1185`!(f:'a->'b) R (y:'a) (z:'a). 1186 R y z ==> (RESTRICT f R z y = f y)`, 1187REWRITE_TAC [RESTRICT_DEF] THEN BETA_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC 1188THEN ASM_REWRITE_TAC[]); 1189 1190 1191(*--------------------------------------------------------------------------- 1192 * Two restricted functions are equal just when they are equal on each 1193 * element of their domain. 1194 *---------------------------------------------------------------------------*) 1195 1196val CUTS_EQ = Q.prove( 1197`!R f g (x:'a). 1198 (RESTRICT f R x = RESTRICT g R x) 1199 = !y:'a. R y x ==> (f y:'b = g y)`, 1200REPEAT GEN_TAC THEN REWRITE_TAC[RESTRICT_DEF] 1201 THEN CONV_TAC (DEPTH_CONV FUN_EQ_CONV) THEN BETA_TAC THEN EQ_TAC 1202 THENL 1203 [ CONV_TAC RIGHT_IMP_FORALL_CONV THEN GEN_TAC 1204 THEN DISCH_THEN (MP_TAC o Q.SPEC`y`) THEN COND_CASES_TAC THEN REWRITE_TAC[], 1205 DISCH_TAC THEN GEN_TAC THEN COND_CASES_TAC THEN RES_TAC 1206 THEN ASM_REWRITE_TAC[]]); 1207 1208 1209val EXPOSE_CUTS_TAC = 1210 BETA_TAC THEN AP_THM_TAC THEN AP_TERM_TAC 1211 THEN REWRITE_TAC[CUTS_EQ] 1212 THEN REPEAT STRIP_TAC; 1213 1214 1215(*--------------------------------------------------------------------------- 1216 * The set of approximations to the function being defined, restricted to 1217 * being R-parents of x. This has the consequence (approx_ext): 1218 * 1219 * approx R M x f = !w. f w = ((R w x) => (M (RESTRICT f R w w) | (@v. T)) 1220 * 1221 *---------------------------------------------------------------------------*) 1222 1223val approx_def = 1224Q.new_definition 1225 ("approx_def", 1226 `approx R M x (f:'a->'b) = (f = RESTRICT (\y. M (RESTRICT f R y) y) R x)`); 1227 1228(* This could, in fact, be the definition. *) 1229val approx_ext = 1230BETA_RULE(ONCE_REWRITE_RULE[RESTRICT_DEF] 1231 (CONV_RULE (ONCE_DEPTH_CONV (Q.X_FUN_EQ_CONV`w`)) approx_def)); 1232 1233val approx_SELECT0 = 1234 Q.GEN`g` (Q.SPEC`g` 1235 (BETA_RULE(Q.ISPEC `\f:'a->'b. approx R M x f` boolTheory.SELECT_AX))); 1236 1237val approx_SELECT1 = CONV_RULE FORALL_IMP_CONV approx_SELECT0; 1238 1239 1240(*--------------------------------------------------------------------------- 1241 * Choose an approximation for R and M at x. Thus it is a 1242 * kind of "lookup" function, associating partial functions with arguments. 1243 * One can easily prove 1244 * (?g. approx R M x g) ==> 1245 * (!w. the_fun R M x w = ((R w x) => (M (RESTRICT (the_fun R M x) R w) w) 1246 * | (@v. T))) 1247 *---------------------------------------------------------------------------*) 1248 1249val the_fun_def = 1250Q.new_definition 1251("the_fun_def", 1252 `the_fun R M x = @f:'a->'b. approx R M x f`); 1253 1254val approx_the_fun0 = ONCE_REWRITE_RULE [GSYM the_fun_def] approx_SELECT0; 1255val approx_the_fun1 = ONCE_REWRITE_RULE [GSYM the_fun_def] approx_SELECT1; 1256val approx_the_fun2 = SUBS [Q.SPECL[`R`,`M`,`x`,`the_fun R M x`] approx_ext] 1257 approx_the_fun1; 1258 1259Triviality the_fun_rw1: 1260 (?g:'a->'b. approx R M x g) 1261 ==> 1262 !w. R w x 1263 ==> 1264 (the_fun R M x w = M (RESTRICT (the_fun R M x) R w) w) 1265Proof 1266 DISCH_THEN (MP_TAC o MP approx_the_fun2) THEN 1267 DISCH_THEN (fn th => GEN_TAC THEN MP_TAC (SPEC_ALL th)) 1268 THEN COND_CASES_TAC 1269 THEN ASM_REWRITE_TAC[] 1270QED 1271 1272Triviality the_fun_rw2: 1273 (?g:'a->'b. approx R M x g) ==> !w. ~R w x ==> (the_fun R M x w = ARB) 1274Proof 1275 DISCH_THEN (MP_TAC o MP approx_the_fun2) THEN 1276 DISCH_THEN (fn th => GEN_TAC THEN MP_TAC (SPEC_ALL th)) 1277 THEN COND_CASES_TAC 1278 THEN ASM_REWRITE_TAC[] 1279QED 1280 1281(*--------------------------------------------------------------------------- 1282 * Define a recursion operator for wellfounded relations. This takes the 1283 * (canonical) function obeying the recursion for all R-ancestors of x: 1284 * 1285 * \p. R p x => the_fun (TC R) (\f v. M (f%R,v) v) x p | Arb 1286 * 1287 * as the function made available for M to use, along with x. Notice that the 1288 * function unrolls properly for each R-ancestor, but only gets applied 1289 * "parentwise", i.e., you can't apply it to any old ancestor, just to a 1290 * parent. This holds recursively, which is what the theorem we eventually 1291 * prove is all about. 1292 *---------------------------------------------------------------------------*) 1293 1294val WFREC_DEF = 1295Q.new_definition 1296("WFREC_DEF", 1297 `WFREC R (M:('a->'b) -> ('a->'b)) = 1298 \x. M (RESTRICT (the_fun (TC R) (\f v. M (RESTRICT f R v) v) x) R x) x`); 1299 1300 1301(*--------------------------------------------------------------------------- 1302 * Two approximations agree on their common domain. 1303 *---------------------------------------------------------------------------*) 1304 1305val APPROX_EQUAL_BELOW = Q.prove( 1306`!R M f g u v. 1307 WF R /\ transitive R /\ 1308 approx R M u f /\ approx R M v g 1309 ==> !x:'a. R x u ==> R x v 1310 ==> (f x:'b = g x)`, 1311REWRITE_TAC[approx_ext] THEN REPEAT GEN_TAC THEN STRIP_TAC 1312 THEN WF_INDUCT_TAC THEN Q.EXISTS_TAC`R` 1313 THEN ASM_REWRITE_TAC[] THEN REPEAT STRIP_TAC 1314 THEN REPEAT COND_CASES_TAC THEN RES_TAC 1315 THEN EXPOSE_CUTS_TAC 1316 THEN ASM_REWRITE_TAC[] 1317 THEN RULE_ASSUM_TAC (REWRITE_RULE[TAUT`A==>B==>C==>D <=> A/\B/\C==>D`, 1318 transitive_def]) 1319 THEN FIRST_ASSUM MATCH_MP_TAC 1320 THEN RES_TAC THEN ASM_REWRITE_TAC[]); 1321 1322Triviality AGREE_BELOW = 1323 REWRITE_RULE[TAUT`A==>B==>C==>D <=> B/\C/\A==>D`] 1324 (CONV_RULE (DEPTH_CONV RIGHT_IMP_FORALL_CONV) APPROX_EQUAL_BELOW); 1325 1326 1327(*--------------------------------------------------------------------------- 1328 * A specialization of AGREE_BELOW 1329 *---------------------------------------------------------------------------*) 1330 1331val RESTRICT_FUN_EQ = Q.prove( 1332`!R M f (g:'a->'b) u v. 1333 WF R /\ 1334 transitive R /\ 1335 approx R M u f /\ 1336 approx R M v g /\ 1337 R v u 1338 ==> (RESTRICT f R v = g)`, 1339REWRITE_TAC[RESTRICT_DEF,transitive_def] THEN REPEAT STRIP_TAC 1340 THEN CONV_TAC (Q.X_FUN_EQ_CONV`w`) THEN BETA_TAC THEN GEN_TAC 1341 THEN COND_CASES_TAC (* on R w v *) 1342 THENL [ MATCH_MP_TAC AGREE_BELOW THEN REPEAT ID_EX_TAC 1343 THEN RES_TAC THEN ASM_REWRITE_TAC[transitive_def], 1344 Q.UNDISCH_TAC`approx R M v (g:'a->'b)` 1345 THEN DISCH_THEN(fn th => 1346 ASM_REWRITE_TAC[REWRITE_RULE[approx_ext]th])]); 1347 1348 1349(*--------------------------------------------------------------------------- 1350 * Every x has an approximation. This is the crucial theorem. 1351 *---------------------------------------------------------------------------*) 1352 1353Theorem EXISTS_LEMMA[local]: 1354 !R M. WF R /\ transitive R ==> !x. ?f:'a->'b. approx R M x f 1355Proof 1356REPEAT GEN_TAC >> STRIP_TAC 1357 >> WF_INDUCT_TAC 1358 >> Q.EXISTS_TAC`R` >> ASM_REWRITE_TAC[] >> GEN_TAC 1359 >> DISCH_THEN (* Adjust IH by applying Choice *) 1360 (ASSUME_TAC o Q.GEN`y` o Q.DISCH`R (y:'a) (x:'a)` 1361 o (fn th => REWRITE_RULE[GSYM the_fun_def] th) 1362 o SELECT_RULE o UNDISCH o Q.ID_SPEC) 1363 >> Q.EXISTS_TAC`\p. if R p x then M (the_fun R M p) p else ARB` (* witness *) 1364 >> REWRITE_TAC[approx_ext] >> BETA_TAC >> GEN_TAC 1365 >> COND_CASES_TAC 1366 >> ASM_REWRITE_TAC[] 1367 >> EXPOSE_CUTS_TAC 1368 >> RES_THEN (SUBST1_TAC o REWRITE_RULE[approx_def]) (* use IH *) 1369 >> REWRITE_TAC[CUTS_EQ] 1370 >> Q.X_GEN_TAC`v` >> BETA_TAC >> DISCH_TAC 1371 >> RULE_ASSUM_TAC(REWRITE_RULE[transitive_def]) >> RES_TAC 1372 >> ASM_REWRITE_TAC[] 1373 >> EXPOSE_CUTS_TAC 1374 >> MATCH_MP_TAC RESTRICT_FUN_EQ 1375 >> MAP_EVERY Q.EXISTS_TAC[`M`,`w`] 1376 >> ASM_REWRITE_TAC[transitive_def] 1377 >> RES_TAC 1378QED 1379 1380 1381val the_fun_unroll = Q.prove( 1382 `!R M x (w:'a). 1383 WF R /\ transitive R 1384 ==> R w x 1385 ==> (the_fun R M x w:'b = M (RESTRICT (the_fun R M x) R w) w)`, 1386REPEAT GEN_TAC THEN DISCH_TAC 1387 THEN Q.ID_SPEC_TAC`w` 1388 THEN MATCH_MP_TAC the_fun_rw1 1389 THEN MATCH_MP_TAC EXISTS_LEMMA 1390 THEN POP_ASSUM ACCEPT_TAC); 1391 1392(*--------------------------------------------------------------------------- 1393 * Unrolling works for any R M and x, hence it works for "TC R" and 1394 * "\f v. M (f % R,v) v". 1395 *---------------------------------------------------------------------------*) 1396 1397val the_fun_TC0 = 1398 BETA_RULE 1399 (REWRITE_RULE[MATCH_MP WF_TC (Q.ASSUME`WF (R:'a->'a->bool)`), 1400 TC_TRANSITIVE] 1401 (Q.SPECL[`TC R`,`\f v. M (RESTRICT f R v) v`,`x`] the_fun_unroll)); 1402 1403 1404(*--------------------------------------------------------------------------- 1405 * There's a rewrite rule that simplifies this mess. 1406 *---------------------------------------------------------------------------*) 1407val TC_RESTRICT_LEMMA = Q.prove( 1408 `!(f:'a->'b) R w. RESTRICT (RESTRICT f (TC R) w) R w = RESTRICT f R w`, 1409REPEAT GEN_TAC 1410 THEN REWRITE_TAC[RESTRICT_DEF] 1411 THEN CONV_TAC (Q.X_FUN_EQ_CONV`p`) 1412 THEN BETA_TAC THEN GEN_TAC 1413 THEN COND_CASES_TAC 1414 THENL [IMP_RES_TAC TC_SUBSET, ALL_TAC] 1415 THEN ASM_REWRITE_TAC[]); 1416 1417val the_fun_TC = REWRITE_RULE[TC_RESTRICT_LEMMA] the_fun_TC0; 1418 1419 1420(*--------------------------------------------------------------------------- 1421 * WFREC R M behaves as a fixpoint operator should. 1422 *---------------------------------------------------------------------------*) 1423 1424val WFREC_THM = Q.store_thm 1425("WFREC_THM", 1426 `!R. !M:('a -> 'b) -> ('a -> 'b). 1427 WF R ==> !x. WFREC R M x = M (RESTRICT (WFREC R M) R x) x`, 1428REPEAT STRIP_TAC THEN REWRITE_TAC[WFREC_DEF] 1429 THEN EXPOSE_CUTS_TAC THEN BETA_TAC 1430 THEN IMP_RES_TAC TC_SUBSET 1431 THEN USE_TAC the_fun_TC 1432 THEN EXPOSE_CUTS_TAC 1433 THEN MATCH_MP_TAC AGREE_BELOW 1434 THEN MAP_EVERY Q.EXISTS_TAC [`TC R`, `\f v. M (RESTRICT f R v) v`, `x`, `y`] 1435 THEN IMP_RES_TAC WF_TC 1436 THEN ASSUME_TAC(SPEC_ALL TC_TRANSITIVE) 1437 THEN IMP_RES_TAC TC_SUBSET THEN POP_ASSUM (K ALL_TAC) 1438 THEN ASM_REWRITE_TAC[] 1439 THEN REPEAT CONJ_TAC 1440 THENL [ RULE_ASSUM_TAC(REWRITE_RULE[transitive_def]) THEN RES_TAC, 1441 ALL_TAC,ALL_TAC] 1442 THEN MATCH_MP_TAC approx_the_fun1 1443 THEN MATCH_MP_TAC EXISTS_LEMMA 1444 THEN ASM_REWRITE_TAC[]); 1445 1446 1447(*---------------------------------------------------------------------------* 1448 * This is what is used by TFL. * 1449 *---------------------------------------------------------------------------*) 1450 1451val WFREC_COROLLARY = 1452 Q.store_thm("WFREC_COROLLARY", 1453 `!M R (f:'a->'b). 1454 (f = WFREC R M) ==> WF R ==> !x. f x = M (RESTRICT f R x) x`, 1455REPEAT GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[WFREC_THM]); 1456 1457 1458(*---------------------------------------------------------------------------* 1459 * The usual phrasing of the wellfounded recursion theorem. * 1460 *---------------------------------------------------------------------------*) 1461 1462val WF_RECURSION_THM = Q.store_thm("WF_RECURSION_THM", 1463`!R. WF R ==> !M. ?!f:'a->'b. !x. f x = M (RESTRICT f R x) x`, 1464GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN CONV_TAC EXISTS_UNIQUE_CONV 1465THEN CONJ_TAC THENL 1466[Q.EXISTS_TAC`WFREC R M` THEN MATCH_MP_TAC WFREC_THM THEN POP_ASSUM ACCEPT_TAC, 1467 REPEAT STRIP_TAC THEN CONV_TAC (Q.X_FUN_EQ_CONV`w`) THEN WF_INDUCT_TAC 1468 THEN Q.EXISTS_TAC`R` THEN CONJ_TAC THENL 1469 [ FIRST_ASSUM ACCEPT_TAC, 1470 GEN_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN AP_THM_TAC THEN 1471 AP_TERM_TAC THEN REWRITE_TAC[CUTS_EQ] THEN GEN_TAC THEN 1472 FIRST_ASSUM MATCH_ACCEPT_TAC]]); 1473 1474 1475(*---------------------------------------------------------------------------*) 1476(* The wellfounded part of a relation. Defined inductively. *) 1477(*---------------------------------------------------------------------------*) 1478 1479val WFP_DEF = Q.new_definition 1480 ("WFP_DEF", 1481 `WFP R a = !P. (!x. (!y. R y x ==> P y) ==> P x) ==> P a`); 1482 1483val WFP_RULES = Q.store_thm 1484 ("WFP_RULES", 1485 `!R x. (!y. R y x ==> WFP R y) ==> WFP R x`, 1486 REWRITE_TAC [WFP_DEF] THEN MESON_TAC []); 1487 1488val WFP_INDUCT = Q.store_thm 1489 ("WFP_INDUCT", 1490 `!R P. (!x. (!y. R y x ==> P y) ==> P x) ==> !x. WFP R x ==> P x`, 1491 REWRITE_TAC [WFP_DEF] THEN MESON_TAC []); 1492 1493val WFP_CASES = Q.store_thm 1494 ("WFP_CASES", 1495 `!R x. WFP R x = !y. R y x ==> WFP R y`, 1496 REPEAT STRIP_TAC THEN EQ_TAC 1497 THENL [Q.ID_SPEC_TAC `x` THEN HO_MATCH_MP_TAC WFP_INDUCT, ALL_TAC] 1498 THEN MESON_TAC [WFP_RULES]); 1499 1500(* ------------------------------------------------------------------------- *) 1501(* Wellfounded part induction, strong version. *) 1502(* ------------------------------------------------------------------------- *) 1503 1504val WFP_STRONG_INDUCT = Q.store_thm 1505 ("WFP_STRONG_INDUCT", 1506 `!R. (!x. WFP R x /\ (!y. R y x ==> P y) ==> P x) 1507 ==> 1508 !x. WFP R x ==> P x`, 1509 REPEAT GEN_TAC THEN STRIP_TAC 1510 THEN ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a /\ b`] 1511 THEN HO_MATCH_MP_TAC WFP_INDUCT THEN ASM_MESON_TAC[WFP_RULES]); 1512 1513 1514(* ------------------------------------------------------------------------- *) 1515(* A relation is wellfounded iff WFP is the whole universe. *) 1516(* ------------------------------------------------------------------------- *) 1517 1518val WF_EQ_WFP = Q.store_thm 1519("WF_EQ_WFP", 1520 `!R. WF R = !x. WFP R x`, 1521 GEN_TAC THEN EQ_TAC THENL 1522 [REWRITE_TAC [WF_EQ_INDUCTION_THM] THEN MESON_TAC [WFP_RULES], 1523 DISCH_TAC THEN MATCH_MP_TAC (SPEC_ALL INDUCTION_WF_THM) 1524 THEN GEN_TAC THEN MP_TAC (SPEC_ALL WFP_STRONG_INDUCT) 1525 THEN ASM_REWRITE_TAC []]); 1526 1527(*---------------------------------------------------------------------------*) 1528(* A formalization of some of the results in *) 1529(* *) 1530(* "Inductive Invariants for Nested Recursion", *) 1531(* Sava Krsti\'{c} and John Matthews, *) 1532(* TPHOLs 2003, LNCS vol. 2758, pp. 253-269. *) 1533(* *) 1534(*---------------------------------------------------------------------------*) 1535 1536 1537(*---------------------------------------------------------------------------*) 1538(* Definition. P is an "inductive invariant" of the functional M with *) 1539(* respect to the wellfounded relation R. *) 1540(*---------------------------------------------------------------------------*) 1541 1542val INDUCTIVE_INVARIANT_DEF = 1543 Q.new_definition 1544 ("INDUCTIVE_INVARIANT_DEF", 1545 `INDUCTIVE_INVARIANT R P M = 1546 !f x. (!y. R y x ==> P y (f y)) ==> P x (M f x)`); 1547 1548(*---------------------------------------------------------------------------*) 1549(* Definition. P is an inductive invariant of the functional M on set D with *) 1550(* respect to the wellfounded relation R. *) 1551(*---------------------------------------------------------------------------*) 1552 1553val INDUCTIVE_INVARIANT_ON_DEF = 1554 Q.new_definition 1555 ("INDUCTIVE_INVARIANT_ON_DEF", 1556 `INDUCTIVE_INVARIANT_ON R D P M = 1557 !f x. D x /\ (!y. D y ==> R y x ==> P y (f y)) ==> P x (M f x)`); 1558 1559(*---------------------------------------------------------------------------*) 1560(* The key theorem, corresponding to theorem 1 of the paper. *) 1561(*---------------------------------------------------------------------------*) 1562 1563val INDUCTIVE_INVARIANT_WFREC = Q.store_thm 1564("INDUCTIVE_INVARIANT_WFREC", 1565 `!R P M. WF R /\ INDUCTIVE_INVARIANT R P M ==> !x. P x (WFREC R M x)`, 1566 REPEAT GEN_TAC THEN STRIP_TAC 1567 THEN IMP_RES_THEN HO_MATCH_MP_TAC WF_INDUCTION_THM 1568 THEN FULL_SIMP_TAC bool_ss [INDUCTIVE_INVARIANT_DEF] 1569 THEN METIS_TAC [WFREC_THM,RESTRICT_DEF]); 1570 1571Theorem TFL_INDUCTIVE_INVARIANT_WFREC: 1572 !f R P M x. (f = WFREC R M) /\ WF R /\ INDUCTIVE_INVARIANT R P M ==> P x (f x) 1573Proof PROVE_TAC [INDUCTIVE_INVARIANT_WFREC] 1574QED 1575 1576val lem = 1577 INDUCTIVE_INVARIANT_WFREC |> Q.SPEC ���R��� |> Q.SPEC ���\x y. D x ==> P x y��� 1578 |> REWRITE_RULE[INDUCTIVE_INVARIANT_DEF] 1579 |> BETA_RULE 1580 1581Theorem INDUCTIVE_INVARIANT_ON_WFREC: 1582 !R P M D x. WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==> 1583 P x (WFREC R M x) 1584Proof 1585 SIMP_TAC bool_ss [INDUCTIVE_INVARIANT_ON_DEF] THEN PROVE_TAC [lem] 1586QED 1587 1588 1589Theorem TFL_INDUCTIVE_INVARIANT_ON_WFREC: 1590 !f R D P M x. 1591 f = WFREC R M /\ WF R /\ INDUCTIVE_INVARIANT_ON R D P M /\ D x ==> 1592 P x (f x) 1593Proof PROVE_TAC [INDUCTIVE_INVARIANT_ON_WFREC] 1594QED 1595 1596local val lem = 1597 GEN_ALL 1598 (REWRITE_RULE [] 1599 (BETA_RULE 1600 (Q.INST [`P` |-> `\a b. (M (WFREC R M) a = b) /\ 1601 (WFREC R M a = b) /\ P a b`] 1602 (SPEC_ALL INDUCTIVE_INVARIANT_ON_WFREC)))) 1603in 1604val IND_FIXPOINT_ON_LEMMA = Q.prove 1605(`!R D M P x. 1606 WF R /\ D x /\ 1607 (!f x. D x /\ (!y. D y /\ R y x ==> P y (WFREC R M y) /\ (f y = WFREC R M y)) 1608 ==> P x (WFREC R M x) /\ (M f x = WFREC R M x)) 1609 ==> 1610 (M (WFREC R M) x = WFREC R M x) /\ P x (WFREC R M x)`, 1611 REPEAT GEN_TAC THEN STRIP_TAC 1612 THEN MATCH_MP_TAC lem 1613 THEN ID_EX_TAC 1614 THEN ASM_REWRITE_TAC [INDUCTIVE_INVARIANT_ON_DEF] 1615 THEN METIS_TAC []) 1616end; 1617 1618(*---------------------------------------------------------------------------*) 1619(* End of Krstic/Matthews results *) 1620(*---------------------------------------------------------------------------*) 1621 1622 1623(* ---------------------------------------------------------------------- 1624 inverting a relation 1625 ---------------------------------------------------------------------- *) 1626 1627val inv_DEF = new_definition( 1628 "inv_DEF", 1629 ``inv (R:'a->'b->bool) x y = R y x``); 1630val _ = export_rewrites ["inv_DEF"] 1631(* superscript suffix T, for "transpose" *) 1632val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 1633 fixity = Suffix 2100, 1634 paren_style = OnlyIfNecessary, 1635 pp_elements = [TOK (UTF8.chr 0x1D40)], 1636 term_name = "relinv"} 1637Overload relinv = ``inv`` 1638val _ = TeX_notation { hol = (UTF8.chr 0x1D40), 1639 TeX = ("\\HOLTokenRInverse{}", 1) } 1640 1641Theorem inv_inv[simp]: 1642 !R. inv (inv R) = R 1643Proof SIMP_TAC bool_ss [FUN_EQ_THM, inv_DEF] 1644QED 1645 1646val inv_RC = store_thm( 1647 "inv_RC", 1648 ``!R. inv (RC R) = RC (inv R)``, 1649 SIMP_TAC bool_ss [RC_DEF, inv_DEF, FUN_EQ_THM] THEN MESON_TAC []); 1650 1651Theorem inv_SC[simp]: 1652 !R. (inv (SC R) = SC R) /\ (SC (inv R) = SC R) 1653Proof 1654 SIMP_TAC bool_ss [inv_DEF, SC_DEF, FUN_EQ_THM] THEN MESON_TAC [] 1655QED 1656 1657val inv_TC = store_thm( 1658 "inv_TC", 1659 ``!R. inv (TC R) = TC (inv R)``, 1660 GEN_TAC THEN SIMP_TAC bool_ss [FUN_EQ_THM, inv_DEF, EQ_IMP_THM, 1661 FORALL_AND_THM] THEN 1662 CONJ_TAC THENL [ 1663 CONV_TAC SWAP_VARS_CONV, 1664 ALL_TAC 1665 ] THEN HO_MATCH_MP_TAC TC_INDUCT THEN 1666 MESON_TAC [inv_DEF, TC_RULES]); 1667 1668Theorem inv_EQC[simp]: 1669 !R. (inv (EQC R) = EQC R) /\ (EQC (inv R) = EQC R) 1670Proof 1671 SIMP_TAC bool_ss [EQC_DEF, inv_TC, inv_SC, inv_RC] 1672QED 1673 1674val inv_MOVES_OUT = store_thm( 1675 "inv_MOVES_OUT", 1676 ``!R. (inv (inv R) = R) /\ (SC (inv R) = SC R) /\ 1677 (RC (inv R) = inv (RC R)) /\ (TC (inv R) = inv (TC R)) /\ 1678 (RTC (inv R) = inv (RTC R)) /\ (EQC (inv R) = EQC R)``, 1679 SIMP_TAC bool_ss [GSYM TC_RC_EQNS, EQC_DEF, inv_TC, inv_SC, inv_inv, inv_RC]) 1680 1681Theorem reflexive_inv[simp]: 1682 !R. reflexive (inv R) = reflexive R 1683Proof SIMP_TAC bool_ss [inv_DEF, reflexive_def] 1684QED 1685 1686Theorem irreflexive_inv[simp]: 1687 !R. irreflexive (inv R) = irreflexive R 1688Proof 1689 SRW_TAC [][irreflexive_def, inv_DEF] 1690QED 1691 1692Theorem symmetric_inv[simp]: 1693 !R. symmetric (inv R) = symmetric R 1694Proof 1695 SIMP_TAC bool_ss [inv_DEF, symmetric_def] THEN MESON_TAC [] 1696QED 1697 1698Theorem antisymmetric_inv[simp]: 1699 !R. antisymmetric (inv R) = antisymmetric R 1700Proof 1701 SRW_TAC [][antisymmetric_def, inv_DEF] THEN PROVE_TAC [] 1702QED 1703 1704Theorem transitive_inv[simp]: 1705 !R. transitive (inv R) = transitive R 1706Proof 1707 SIMP_TAC bool_ss [inv_DEF, transitive_def] THEN MESON_TAC [] 1708QED 1709 1710val symmetric_inv_identity = store_thm( 1711 "symmetric_inv_identity", 1712 ``!R. symmetric R ==> (inv R = R)``, 1713 SIMP_TAC bool_ss [inv_DEF, symmetric_def, FUN_EQ_THM]); 1714 1715val equivalence_inv_identity = store_thm( 1716 "equivalence_inv_identity", 1717 ``!R. equivalence R ==> (inv R = R)``, 1718 SIMP_TAC bool_ss [equivalence_def, symmetric_inv_identity]); 1719 1720(* ---------------------------------------------------------------------- 1721 properties of relations, and set-like operations on relations from 1722 Lockwood Morris 1723 ---------------------------------------------------------------------- *) 1724 1725(* ---------------------------------------------------------------------- 1726 Involutions (functions whose square is the identity) 1727 ---------------------------------------------------------------------- *) 1728 1729 1730val INVOL_DEF = new_definition( 1731 "INVOL_DEF", 1732 ``INVOL (f:'z->'z) = (f o f = I)``); 1733 1734val INVOL = store_thm( 1735 "INVOL", 1736 ``!f:'z->'z. INVOL f = (!x. f (f x) = x)``, 1737 SRW_TAC [] [FUN_EQ_THM, INVOL_DEF]); 1738 1739val INVOL_ONE_ONE = store_thm ( 1740 "INVOL_ONE_ONE", 1741 ``!f:'z->'z. INVOL f ==> (!a b. (f a = f b) = (a = b))``, 1742 PROVE_TAC [INVOL]); 1743 1744val INVOL_ONE_ENO = store_thm ( 1745 "INVOL_ONE_ENO", 1746 ``!f:'z->'z. INVOL f ==> (!a b. (f a = b) = (a = f b))``, 1747 PROVE_TAC [INVOL]); 1748 1749(* logical negation is an involution. *) 1750val NOT_INVOL = store_thm ( 1751 "NOT_INVOL", 1752 ``INVOL (~)``, 1753 REWRITE_TAC [INVOL, NOT_CLAUSES]); 1754 1755(* ---------------------------------------------------------------------- 1756 Idempotent functions are those where f o f = f 1757 ---------------------------------------------------------------------- *) 1758 1759val IDEM_DEF = new_definition( 1760 "IDEM_DEF", 1761 ``IDEM (f:'z->'z) = (f o f = f)``); 1762 1763val IDEM = store_thm ( 1764 "IDEM", 1765 ``!f:'z->'z. IDEM f = (!x. f (f x) = f x)``, 1766 SRW_TAC [][IDEM_DEF, FUN_EQ_THM]); 1767 1768(* set up Id as a synonym for equality... *) 1769Overload Id = ���(=)��� 1770 1771(* but prefer = as the printing form when with two arguments *) 1772Overload "=" = ���(=)��� 1773 1774(* code below even sets things up so that Id is preferred printing form when 1775 an equality term does not have two arguments. It causes grief in 1776 parsing though - another project for the future maybe. 1777val _ = remove_termtok {term_name = "=", tok = "="} 1778val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 2)), 1779 fixity = Infix(NONASSOC, 100), 1780 paren_style = OnlyIfNecessary, 1781 pp_elements = [HardSpace 1, TOK "=", BreakSpace(1,0)], 1782 term_name = "Id"} 1783*) 1784 1785(* inv is an involution, which we know from theorem inv_inv above *) 1786val inv_INVOL = store_thm( 1787 "inv_INVOL", 1788 ``INVOL inv``, 1789 REWRITE_TAC [INVOL, inv_inv]); 1790 1791(* ---------------------------------------------------------------------- 1792 composition of two relations, written O (Isabelle/HOL notation) 1793 ---------------------------------------------------------------------- *) 1794 1795(* This way 'round by analogy with function composition, where the 1796 second argument to composition acts on the "input" first. This is also 1797 consistent with the way this constant is defined in Isabelle/HOL. *) 1798val O_DEF = new_definition( 1799 "O_DEF", 1800 ``(O) R1 R2 (x:'g) (z:'k) = ?y:'h. R2 x y /\ R1 y z``); 1801val _ = set_fixity "O" (Infixr 800) 1802val _ = Unicode.unicode_version {u = UTF8.chr 0x2218 ^ UnicodeChars.sub_r, 1803 tmnm = "O"} 1804val _ = TeX_notation { hol = UTF8.chr 0x2218 ^ UnicodeChars.sub_r, 1805 TeX = ("\\HOLTokenRCompose{}", 1) } 1806 1807val inv_O = store_thm( 1808 "inv_O", 1809 ``!R R'. inv (R O R') = inv R' O inv R``, 1810 SRW_TAC [][FUN_EQ_THM, O_DEF, inv_DEF] THEN PROVE_TAC []); 1811 1812(* ---------------------------------------------------------------------- 1813 relational inclusion, analog of SUBSET 1814 ---------------------------------------------------------------------- *) 1815 1816val RSUBSET = new_definition( 1817 "RSUBSET", 1818 ``(RSUBSET) R1 R2 = !x y. R1 x y ==> R2 x y``); 1819val _ = set_fixity "RSUBSET" (Infix(NONASSOC, 450)); 1820val _ = OpenTheoryMap.OpenTheory_const_name 1821 {const={Thy="relation",Name="RSUBSET"}, 1822 name=(["Relation"],"subrelation")} 1823val _ = Unicode.unicode_version {u = UnicodeChars.subset ^ UnicodeChars.sub_r, 1824 tmnm = "RSUBSET"} 1825val _ = TeX_notation { hol = UnicodeChars.subset ^ UnicodeChars.sub_r, 1826 TeX = ("\\HOLTokenRSubset{}", 1) } 1827 1828val irreflexive_RSUBSET = store_thm( 1829 "irreflexive_RSUBSET", 1830 ``!R1 R2. irreflexive R2 /\ R1 RSUBSET R2 ==> irreflexive R1``, 1831 SRW_TAC [][irreflexive_def, RSUBSET] THEN PROVE_TAC []); 1832 1833(* ---------------------------------------------------------------------- 1834 relational union 1835 ---------------------------------------------------------------------- *) 1836 1837val RUNION = new_definition( 1838 "RUNION", 1839 ``(RUNION) R1 R2 x y <=> R1 x y \/ R2 x y``); 1840val _ = set_fixity "RUNION" (Infixl 500) 1841val _ = OpenTheoryMap.OpenTheory_const_name 1842 {const={Thy="relation",Name="RUNION"},name=(["Relation"],"union")} 1843 1844val RUNION_COMM = store_thm( 1845 "RUNION_COMM", 1846 ``R1 RUNION R2 = R2 RUNION R1``, 1847 SRW_TAC [][RUNION, FUN_EQ_THM] THEN PROVE_TAC []); 1848 1849val RUNION_ASSOC = store_thm( 1850 "RUNION_ASSOC", 1851 ``R1 RUNION (R2 RUNION R3) = (R1 RUNION R2) RUNION R3``, 1852 SRW_TAC [][RUNION, FUN_EQ_THM] THEN PROVE_TAC []); 1853 1854val _ = Unicode.unicode_version {u = UnicodeChars.union ^ UnicodeChars.sub_r, 1855 tmnm = "RUNION"} 1856val _ = TeX_notation { hol = UnicodeChars.union ^ UnicodeChars.sub_r, 1857 TeX = ("\\HOLTokenRUnion{}", 1) } 1858 1859(* ---------------------------------------------------------------------- 1860 relational intersection 1861 ---------------------------------------------------------------------- *) 1862 1863val RINTER = new_definition( 1864 "RINTER", 1865 ``(RINTER) R1 R2 x y <=> R1 x y /\ R2 x y``); 1866val _ = set_fixity "RINTER" (Infixl 600) 1867val _ = OpenTheoryMap.OpenTheory_const_name 1868 {const={Thy="relation",Name="RINTER"},name=(["Relation"],"intersect")} 1869val _ = Unicode.unicode_version {u = UnicodeChars.inter ^ UnicodeChars.sub_r, 1870 tmnm = "RINTER"} 1871val _ = TeX_notation { hol = UnicodeChars.inter ^ UnicodeChars.sub_r, 1872 TeX = ("\\HOLTokenRInter{}", 1) } 1873 1874val RINTER_COMM = store_thm( 1875 "RINTER_COMM", 1876 ``R1 RINTER R2 = R2 RINTER R1``, 1877 SRW_TAC [][RINTER, FUN_EQ_THM] THEN PROVE_TAC []); 1878 1879val RINTER_ASSOC = store_thm( 1880 "RINTER_ASSOC", 1881 ``R1 RINTER (R2 RINTER R3) = (R1 RINTER R2) RINTER R3``, 1882 SRW_TAC [][RINTER, FUN_EQ_THM] THEN PROVE_TAC []); 1883 1884val antisymmetric_RINTER = Q.store_thm( 1885 "antisymmetric_RINTER", 1886 `(antisymmetric R1 ==> antisymmetric (R1 RINTER R2)) /\ 1887 (antisymmetric R2 ==> antisymmetric (R1 RINTER R2))`, 1888 SRW_TAC [][antisymmetric_def,RINTER]); 1889val _ = export_rewrites ["antisymmetric_RINTER"] 1890 1891val transitive_RINTER = Q.store_thm( 1892 "transitive_RINTER", 1893 `transitive R1 /\ transitive R2 ==> transitive (R1 RINTER R2)`, 1894 SRW_TAC [SatisfySimps.SATISFY_ss][transitive_def,RINTER]); 1895val _ = export_rewrites ["transitive_RINTER"] 1896 1897Theorem RTC_RINTER: 1898 !R1 R2 x y. RTC (R1 RINTER R2) x y ==> ((RTC R1) RINTER (RTC R2)) x y 1899Proof 1900 ntac 2 gen_tac >> 1901 match_mp_tac RTC_INDUCT >> 1902 asm_simp_tac(srw_ss())[RINTER] >> 1903 METIS_TAC[RTC_CASES1] 1904QED 1905 1906(* ---------------------------------------------------------------------- 1907 relational complement 1908 ---------------------------------------------------------------------- *) 1909 1910val RCOMPL = new_definition( 1911 "RCOMPL", 1912 ``RCOMPL R x y = ~R x y``); 1913 1914(* ---------------------------------------------------------------------- 1915 theorems about reflexive, symmetric and transitive predicates in 1916 terms of particular relational-subsets 1917 ---------------------------------------------------------------------- *) 1918 1919val reflexive_Id_RSUBSET = store_thm( 1920 "reflexive_Id_RSUBSET", 1921 ``!R. reflexive R = (Id RSUBSET R)``, 1922 SRW_TAC [][RSUBSET, reflexive_def]); 1923 1924val symmetric_inv_RSUBSET = store_thm( 1925 "symmetric_inv_RSUBSET", 1926 ``symmetric R = (inv R RSUBSET R)``, 1927 SRW_TAC [][symmetric_def, inv_DEF, RSUBSET] THEN PROVE_TAC []); 1928 1929val transitive_O_RSUBSET = store_thm( 1930 "transitive_O_RSUBSET", 1931 ``transitive R = (R O R RSUBSET R)``, 1932 SRW_TAC [][transitive_def, O_DEF, RSUBSET] THEN PROVE_TAC []); 1933 1934(* ---------------------------------------------------------------------- 1935 various sorts of orders 1936 ---------------------------------------------------------------------- *) 1937 1938val PreOrder = new_definition( 1939 "PreOrder", 1940 ``PreOrder R <=> reflexive R /\ transitive R``); 1941 1942(* The following definition follows Rob Arthan's idea of staying mum, 1943 for the most general notion of (partial) order, about whether the 1944 relation is to be reflexive, irreflexive, or something in 1945 between. *) 1946 1947val Order = new_definition( 1948 "Order", 1949 ``Order (Z:'g->'g->bool) <=> antisymmetric Z /\ transitive Z``); 1950 1951val WeakOrder = new_definition( 1952 "WeakOrder", 1953 ``WeakOrder (Z:'g->'g->bool) <=> 1954 reflexive Z /\ antisymmetric Z /\ transitive Z``); 1955 1956val StrongOrder = new_definition( 1957 "StrongOrder", 1958 ``StrongOrder (Z:'g->'g->bool) <=> irreflexive Z /\ transitive Z``); 1959 1960val irrefl_trans_implies_antisym = store_thm( 1961 "irrefl_trans_implies_antisym", 1962 ``!R. irreflexive R /\ transitive R ==> antisymmetric R``, 1963 SRW_TAC [][antisymmetric_def, transitive_def, irreflexive_def] THEN 1964 METIS_TAC []); 1965 1966val StrongOrd_Ord = store_thm( 1967 "StrongOrd_Ord", 1968 ``!R. StrongOrder R ==> Order R``, 1969 SRW_TAC [][StrongOrder, Order, irrefl_trans_implies_antisym]); 1970 1971val WeakOrd_Ord = store_thm( 1972 "WeakOrd_Ord", 1973 ``!R. WeakOrder R ==> Order R``, 1974 SRW_TAC [][WeakOrder, Order]); 1975 1976val WeakOrder_EQ = store_thm( 1977 "WeakOrder_EQ", 1978 ``!R. WeakOrder R ==> !y z. (y = z) <=> R y z /\ R z y``, 1979 SRW_TAC [][WeakOrder, reflexive_def, antisymmetric_def] THEN PROVE_TAC []); 1980 1981val RSUBSET_ANTISYM = store_thm( 1982 "RSUBSET_ANTISYM", 1983 ``!R1 R2. R1 RSUBSET R2 /\ R2 RSUBSET R1 ==> (R1 = R2)``, 1984 SRW_TAC [][RSUBSET, FUN_EQ_THM] THEN PROVE_TAC []); 1985 1986val RSUBSET_antisymmetric = store_thm( 1987 "RSUBSET_antisymmetric", 1988 ``antisymmetric (RSUBSET)``, 1989 REWRITE_TAC [antisymmetric_def, RSUBSET_ANTISYM]); 1990 1991val RSUBSET_WeakOrder = store_thm( 1992 "RSUBSET_WeakOrder", 1993 ``WeakOrder (RSUBSET)``, 1994 SRW_TAC [][WeakOrder, reflexive_def, antisymmetric_def, transitive_def, 1995 RSUBSET, FUN_EQ_THM] THEN 1996 PROVE_TAC []); 1997 1998val EqIsBothRSUBSET = save_thm( 1999 "EqIsBothRSUBSET", 2000 MATCH_MP WeakOrder_EQ RSUBSET_WeakOrder) 2001(* |- !y z. (y = z) = y RSUBSET z /\ z RSUBSET y *) 2002 2003(* ---------------------------------------------------------------------- 2004 STRORD makes an order strict (or "strong") 2005 ---------------------------------------------------------------------- *) 2006 2007val STRORD = new_definition( 2008 "STRORD", 2009 ``STRORD R a b <=> R a b /\ ~(a = b)``); 2010 2011val STRORD_AND_NOT_Id = store_thm( 2012 "STRORD_AND_NOT_Id", 2013 ``STRORD R = R RINTER (RCOMPL Id)``, 2014 SRW_TAC [][STRORD, RINTER, RCOMPL, FUN_EQ_THM]); 2015 2016(* the corresponding "UNSTRORD", which makes an order weak is just RC *) 2017 2018val RC_OR_Id = store_thm( 2019 "RC_OR_Id", 2020 ``RC R = R RUNION Id``, 2021 SRW_TAC [][RC_DEF, RUNION, FUN_EQ_THM] THEN PROVE_TAC []); 2022 2023val RC_Weak = store_thm( 2024 "RC_Weak", 2025 ``Order R = WeakOrder (RC R)``, 2026 SRW_TAC [][Order, WeakOrder, EQ_IMP_THM, transitive_RC] THEN 2027 FULL_SIMP_TAC (srw_ss()) [transitive_def, RC_DEF, antisymmetric_def] THEN 2028 PROVE_TAC []); 2029 2030val STRORD_Strong = store_thm( 2031 "STRORD_Strong", 2032 ``!R. Order R = StrongOrder (STRORD R)``, 2033 SRW_TAC [][Order, StrongOrder, STRORD, antisymmetric_def, transitive_def, 2034 irreflexive_def] THEN PROVE_TAC []); 2035 2036val STRORD_RC = store_thm( 2037 "STRORD_RC", 2038 ``!R. StrongOrder R ==> (STRORD (RC R) = R)``, 2039 SRW_TAC [][StrongOrder, STRORD, RC_DEF, irreflexive_def, antisymmetric_def, 2040 transitive_def, FUN_EQ_THM] THEN PROVE_TAC []); 2041 2042val RC_STRORD = store_thm( 2043 "RC_STRORD", 2044 ``!R. WeakOrder R ==> (RC (STRORD R) = R)``, 2045 SRW_TAC [][WeakOrder, STRORD, RC_DEF, reflexive_def, antisymmetric_def, 2046 transitive_def, FUN_EQ_THM] THEN PROVE_TAC []); 2047 2048val IDEM_STRORD = store_thm( 2049 "IDEM_STRORD", 2050 ``IDEM STRORD``, 2051 SRW_TAC [][STRORD, IDEM, FUN_EQ_THM] THEN PROVE_TAC []); 2052 2053val IDEM_RC = store_thm( 2054 "IDEM_RC", 2055 ``IDEM RC``, 2056 SRW_TAC [][IDEM, RC_IDEM]); 2057 2058val IDEM_SC = store_thm( 2059 "IDEM_SC", 2060 ``IDEM SC``, 2061 SRW_TAC [][IDEM, SC_IDEM]); 2062 2063val IDEM_TC = store_thm( 2064 "IDEM_TC", 2065 ``IDEM TC``, 2066 SRW_TAC [][IDEM, TC_IDEM]); 2067 2068val IDEM_RTC = store_thm( 2069 "IDEM_RTC", 2070 ``IDEM RTC``, 2071 SRW_TAC [][IDEM, RTC_IDEM]); 2072 2073val trichotomous_STRORD = store_thm( 2074 "trichotomous_STRORD", 2075 ``trichotomous (STRORD R) <=> trichotomous R``, 2076 SRW_TAC [][STRORD, trichotomous] THEN METIS_TAC[]); 2077val _ = export_rewrites ["trichotomous_STRORD"] 2078 2079val trichotomous_RC = store_thm( 2080 "trichotomous_RC", 2081 ``trichotomous (RC R) <=> trichotomous R``, 2082 SRW_TAC [][RC_DEF, trichotomous] THEN METIS_TAC[]); 2083val _ = export_rewrites ["trichotomous_RC"] 2084 2085(* ---------------------------------------------------------------------- 2086 We may define notions of linear (i.e., total) order, but in the 2087 absence of numbers I don't see much to prove about them. 2088 ---------------------------------------------------------------------- *) 2089 2090val LinearOrder = new_definition( 2091 "LinearOrder", 2092 ``LinearOrder (R:'a->'a->bool) <=> Order R /\ trichotomous R``); 2093 2094val StrongLinearOrder = new_definition( 2095 "StrongLinearOrder", 2096 ``StrongLinearOrder (R:'a->'a->bool) <=> StrongOrder R /\ trichotomous R``); 2097 2098val WeakLinearOrder = new_definition( 2099 "WeakLinearOrder", 2100 ``WeakLinearOrder (R:'a->'a->bool) <=> WeakOrder R /\ trichotomous R``); 2101 2102val WeakLinearOrder_dichotomy = store_thm( 2103 "WeakLinearOrder_dichotomy", 2104 ``!R:'a->'a->bool. WeakLinearOrder R <=> 2105 WeakOrder R /\ (!a b. R a b \/ R b a)``, 2106 SRW_TAC [][WeakLinearOrder, trichotomous] THEN 2107 PROVE_TAC [WeakOrder_EQ]); 2108 2109(* ---------------------------------------------------------------------- 2110 other stuff (inspired by Isabelle's Relation theory) 2111 ---------------------------------------------------------------------- *) 2112 2113val diag_def = new_definition( 2114 "diag_def", 2115 ``diag A x y <=> (x = y) /\ x IN A``); 2116 2117(* properties of O *) 2118 2119val O_ASSOC = store_thm( 2120 "O_ASSOC", 2121 ``R1 O (R2 O R3) = (R1 O R2) O R3``, 2122 SRW_TAC [][O_DEF, FUN_EQ_THM] THEN PROVE_TAC []); 2123 2124val Id_O = store_thm( 2125 "Id_O", 2126 ``Id O R = R``, 2127 SRW_TAC [][O_DEF, FUN_EQ_THM]) 2128val _ = export_rewrites ["Id_O"] 2129 2130val O_Id = store_thm( 2131 "O_Id", 2132 ``R O Id = R``, 2133 SRW_TAC [][O_DEF, FUN_EQ_THM]); 2134val _ = export_rewrites ["O_Id"] 2135 2136val O_MONO = store_thm( 2137 "O_MONO", 2138 ``R1 RSUBSET R2 /\ S1 RSUBSET S2 ==> (R1 O S1) RSUBSET (R2 O S2)``, 2139 SRW_TAC [][RSUBSET, O_DEF] THEN PROVE_TAC []); 2140 2141val inv_Id = store_thm( 2142 "inv_Id", 2143 ``inv Id = Id``, 2144 SRW_TAC [][FUN_EQ_THM, inv_DEF, EQ_SYM_EQ]); 2145 2146val inv_diag = store_thm( 2147 "inv_diag", 2148 ``inv (diag A) = diag A``, 2149 SRW_TAC [][FUN_EQ_THM, inv_DEF, diag_def] THEN PROVE_TAC []); 2150 2151(* domain of a relation *) 2152(* if I just had UNIONs and the like around, I could prove great things like 2153 RDOM (R RUNION R') = RDOM R UNION RDOM R' 2154 I can still prove x IN RDOM (R1 RUNION R2) = x IN RDOM R1 \/ x IN RDOM R2 2155 though. 2156*) 2157val RDOM_DEF = new_definition( 2158 "RDOM_DEF", 2159 ``RDOM R x = ?y. R x y``); 2160 2161val IN_RDOM = store_thm( 2162 "IN_RDOM", 2163 ``x IN RDOM R <=> ?y. R x y``, 2164 SRW_TAC [][RDOM_DEF, IN_DEF]); 2165 2166(* range of a relation *) 2167val RRANGE_DEF = new_definition( 2168 "RRANGE", 2169 ``RRANGE R y = ?x. R x y``); 2170 2171val IN_RRANGE = store_thm( 2172 "IN_RRANGE", 2173 ``y IN RRANGE R <=> ?x. R x y``, 2174 SRW_TAC [][RRANGE_DEF, IN_DEF]); 2175 2176val IN_RDOM_RUNION = store_thm( 2177 "IN_RDOM_RUNION", 2178 ``x IN RDOM (R1 RUNION R2) <=> x IN RDOM R1 \/ x IN RDOM R2``, 2179 SIMP_TAC (srw_ss()) [RDOM_DEF, RUNION, boolTheory.IN_DEF, EXISTS_OR_THM]); 2180 2181(* top and bottom elements of RSUBSET lattice *) 2182val RUNIV = new_definition( 2183 "RUNIV", 2184 ``RUNIV x y = T``); 2185val _ = export_rewrites ["RUNIV"] 2186val _ = OpenTheoryMap.OpenTheory_const_name 2187 {const={Thy="relation",Name="RUNIV"},name=(["Relation"],"universe")} 2188val _ = Unicode.unicode_version { 2189 u = UnicodeChars.universal_set ^ UnicodeChars.sub_r, 2190 tmnm = "RUNIV"} 2191 2192 2193val RUNIV_SUBSET = store_thm( 2194 "RUNIV_SUBSET", 2195 ``(RUNIV RSUBSET R <=> (R = RUNIV)) /\ 2196 (R RSUBSET RUNIV)``, 2197 SRW_TAC [][RSUBSET, FUN_EQ_THM]); 2198val _ = export_rewrites ["RUNIV_SUBSET"] 2199 2200val REMPTY_SUBSET = store_thm( 2201 "REMPTY_SUBSET", 2202 ``REMPTY RSUBSET R /\ 2203 (R RSUBSET REMPTY <=> (R = REMPTY))``, 2204 SRW_TAC [][RSUBSET, FUN_EQ_THM]); 2205val _ = export_rewrites ["REMPTY_SUBSET"] 2206 2207(* ---------------------------------------------------------------------- 2208 Restrictions on relations 2209 2210 In theory there are 3 flavours of restriction, each taking a relation 2211 and a set. 2212 2213 1. restricting the domain of a relation (perhaps the most natural, 2214 gets to be RRESTRICT below) 2215 2. restricting the range of a relation 2216 3. restricting both, forcing the relation to be 'a -> 'a -> bool 2217 2218 In addition, it might be nice to have notation for removal of just 2219 one element in each flavour, which can be expressed as restriction 2220 to the complement of the singleton set containing that element. 2221 2222 ---------------------------------------------------------------------- *) 2223 2224val RRESTRICT_DEF = new_definition( 2225 "RRESTRICT_DEF", 2226 ``RRESTRICT R s (x:'a) (y:'b) <=> R x y /\ x IN s``); 2227val _ = export_rewrites ["RRESTRICT_DEF"] 2228 2229val IN_RDOM_RRESTRICT = store_thm( 2230 "IN_RDOM_RRESTRICT", 2231 ``x IN RDOM (RRESTRICT (R:'a -> 'b -> bool) s) <=> x IN RDOM R /\ x IN s``, 2232 SIMP_TAC bool_ss [boolTheory.IN_DEF, RDOM_DEF, RRESTRICT_DEF] THEN 2233 METIS_TAC[]) 2234val _ = export_rewrites ["IN_RDOM_RRESTRICT"] 2235 2236val RDOM_DELETE_DEF = new_definition( 2237 "RDOM_DELETE_DEF", 2238 ``RDOM_DELETE R x u v <=> R u v /\ u <> x``); 2239val _ = export_rewrites ["RDOM_DELETE_DEF"] 2240 2241(* this syntax is compatible (easily confused) with that for finite maps *) 2242val _ = set_fixity "\\\\" (Infixl 600) 2243Overload "\\\\" = ���RDOM_DELETE��� 2244 2245val IN_RDOM_DELETE = store_thm( 2246 "IN_RDOM_DELETE", 2247 ``x IN RDOM (R \\ k) <=> x IN RDOM R /\ x <> k``, 2248 SIMP_TAC bool_ss [boolTheory.IN_DEF, RDOM_DEF, RDOM_DELETE_DEF] THEN 2249 METIS_TAC[]); 2250val _ = export_rewrites ["IN_RDOM_DELETE"] 2251 2252 2253 2254 2255(*===========================================================================*) 2256(* Some notions from Term Rewriting Systems, leading to simple results about *) 2257(* things like confluence and normalisation *) 2258(*===========================================================================*) 2259 2260val diamond_def = new_definition( 2261 "diamond_def", 2262 ``diamond (R:'a->'a->bool) = !x y z. R x y /\ R x z ==> ?u. R y u /\ R z u``) 2263 2264val rcdiamond_def = new_definition( (* reflexive closure half diamond *) 2265 "rcdiamond_def", 2266 ``rcdiamond (R:'a->'a->bool) = 2267 !x y z. R x y /\ R x z ==> ?u. RC R y u /\ RC R z u``); 2268 2269val CR_def = new_definition( (* Church-Rosser *) 2270 "CR_def", 2271 ``CR R = diamond (RTC R)``); 2272 2273val WCR_def = new_definition( (* weakly Church-Rosser *) 2274 "WCR_def", 2275 ``WCR R = !x y z. R x y /\ R x z ==> ?u. RTC R y u /\ RTC R z u``); 2276 2277val SN_def = new_definition( (* strongly normalising *) 2278 "SN_def", 2279 ``SN R = WF (inv R)``); 2280 2281val nf_def = new_definition( (* normal-form *) 2282 "nf_def", 2283 ``nf R x = !y. ~R x y``) 2284 2285(* results *) 2286 2287(* that proving rcdiamond R is equivalent to establishing diamond (RC R) *) 2288val rcdiamond_diamond = store_thm( 2289 "rcdiamond_diamond", 2290 ``!R. rcdiamond R = diamond (RC R)``, 2291 SRW_TAC [][rcdiamond_def, diamond_def, RC_DEF] THEN 2292 METIS_TAC []); (* PROVE_TAC can't cope with this *) 2293 2294val diamond_RC_diamond = store_thm( 2295 "diamond_RC_diamond", 2296 ``!R. diamond R ==> diamond (RC R)``, 2297 SRW_TAC [][diamond_def, RC_DEF] THEN METIS_TAC []); 2298 2299val diamond_TC_diamond = store_thm( 2300 "diamond_TC_diamond", 2301 ``!R. diamond R ==> diamond (TC R)``, 2302 REWRITE_TAC [diamond_def] THEN GEN_TAC THEN STRIP_TAC THEN 2303 Q_TAC SUFF_TAC 2304 `!x y. TC R x y ==> !z. TC R x z ==> ?u. TC R y u /\ TC R z u` THEN1 2305 METIS_TAC [] THEN 2306 HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN 2307 Q.SUBGOAL_THEN 2308 `!x y. TC R x y ==> !z. R x z ==> ?u. TC R y u /\ TC R z u` 2309 ASSUME_TAC 2310 THENL [ 2311 HO_MATCH_MP_TAC TC_INDUCT_LEFT1 THEN PROVE_TAC [TC_RULES], 2312 ALL_TAC (* METIS_TAC very slow in comparison on line above *) 2313 ] THEN PROVE_TAC [TC_RULES]); 2314 2315val RTC_eq_TCRC = prove( 2316 ``RTC R = TC (RC R)``, 2317 REWRITE_TAC [TC_RC_EQNS]); 2318 2319val establish_CR = store_thm( 2320 "establish_CR", 2321 ``!R. (rcdiamond R ==> CR R) /\ (diamond R ==> CR R)``, 2322 REWRITE_TAC [CR_def, RTC_eq_TCRC] THEN 2323 PROVE_TAC [diamond_RC_diamond, rcdiamond_diamond, diamond_TC_diamond]); 2324 2325fun (g by tac) = 2326 Q.SUBGOAL_THEN g STRIP_ASSUME_TAC THEN1 tac 2327 2328val Newmans_lemma = store_thm( 2329 "Newmans_lemma", 2330 ``!R. WCR R /\ SN R ==> CR R``, 2331 REPEAT STRIP_TAC THEN 2332 `WF (TC (inv R))` by PROVE_TAC [WF_TC, SN_def] THEN 2333 REWRITE_TAC [CR_def, diamond_def] THEN 2334 POP_ASSUM (HO_MATCH_MP_TAC o MATCH_MP WF_INDUCTION_THM) THEN 2335 SRW_TAC [][inv_MOVES_OUT, inv_DEF] THEN 2336 `(x = y) \/ ?y1. R x y1 /\ RTC R y1 y` by PROVE_TAC [RTC_CASES1] THENL [ 2337 SRW_TAC [][] THEN PROVE_TAC [RTC_RULES], 2338 ALL_TAC 2339 ] THEN 2340 `(x = z) \/ ?z1. R x z1 /\ RTC R z1 z` by PROVE_TAC [RTC_CASES1] THENL [ 2341 SRW_TAC [][] THEN PROVE_TAC [RTC_RULES], 2342 ALL_TAC 2343 ] THEN 2344 `?x0. RTC R y1 x0 /\ RTC R z1 x0` by PROVE_TAC [WCR_def] THEN 2345 `TC R x y1 /\ TC R x z1` by PROVE_TAC [TC_RULES] THEN 2346 `?y2. RTC R y y2 /\ RTC R x0 y2` by PROVE_TAC [] THEN 2347 `?z2. RTC R z z2 /\ RTC R x0 z2` by PROVE_TAC [] THEN 2348 `TC R x x0` by PROVE_TAC [EXTEND_RTC_TC] THEN 2349 PROVE_TAC [RTC_RTC]); 2350 2351val _ = export_theory(); 2352