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