1open HolKernel boolLib Parse BasicProvers simpLib numLib metisLib markerLib; 2open pred_setTheory pairTheory arithmeticTheory open optionTheory relationTheory; 3 4val Define = TotalDefn.Define; 5val Hol_reln = IndDefLib.Hol_reln; 6 7val _ = new_theory "set_relation"; 8 9local open OpenTheoryMap 10 val ns = ["Relation"] 11in 12 fun ot0 x y = OpenTheory_const_name{const={Thy="set_relation",Name=x},name=(ns,y)} 13 fun ot x = ot0 x x 14end 15 16(* ------------------------------------------------------------------------ *) 17(* Basic concepts *) 18(* ------------------------------------------------------------------------ *) 19 20val _ = type_abbrev ("reln", ``:'a # 'a -> bool``); 21 22val rextension = Q.store_thm ("rextension", 23`!s t. (s = t) = !x y. (x,y) IN s = (x,y) IN t`, 24SRW_TAC [] [] THEN 25EQ_TAC THEN 26SRW_TAC [] [EXTENSION] THEN 27Cases_on `x` THEN 28SRW_TAC [] []); 29 30val domain_def = Define ` 31 domain r = {x | ?y. (x, y) IN r}`; 32val _ = ot "domain" 33 34val range_def = Define ` 35 range r = {y | ?x. (x, y) IN r}`; 36val _ = ot "range" 37 38val in_domain = Q.store_thm ("in_domain", 39`!x r. x IN domain r = ?y. (x,y) IN r`, 40SRW_TAC [] [domain_def]); 41 42val in_range = Q.store_thm ("in_range", 43`!y r. y IN range r = ?x. (x,y) IN r`, 44SRW_TAC [] [range_def]); 45 46val in_dom_rg = Q.store_thm ("in_dom_rg", 47 `(x, y) IN r ==> x IN domain r /\ y IN range r`, 48 REWRITE_TAC [in_domain, in_range] THEN PROVE_TAC []) ; 49 50val domain_mono = Q.store_thm ("domain_mono", 51 `r SUBSET r' ==> domain r SUBSET domain r'`, 52 REWRITE_TAC [in_domain, SUBSET_DEF] THEN 53 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `y` THEN RES_TAC) ; 54 55val range_mono = Q.store_thm ("range_mono", 56 `r SUBSET r' ==> range r SUBSET range r'`, 57 REWRITE_TAC [in_range, SUBSET_DEF] THEN 58 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `x'` THEN RES_TAC) ; 59 60val rrestrict_def = Define ` 61 rrestrict r s = {(x, y) | (x, y) IN r /\ x IN s /\ y IN s}`; 62val _ = ot0 "rrestrict" "restrict" 63 64val in_rrestrict = Q.store_thm ("in_rrestrict", 65`!x y r s. (x, y) IN rrestrict r s = (x, y) IN r /\ x IN s /\ y IN s`, 66SRW_TAC [] [rrestrict_def]); 67 68val in_rrestrict_alt = Q.store_thm ("in_rrestrict_alt", 69 `x IN rrestrict r s <=> x IN r /\ FST x IN s /\ SND x IN s`, 70 Cases_on `x` THEN REWRITE_TAC [in_rrestrict, FST, SND]) ; 71 72val rrestrict_SUBSET = Q.store_thm ("rrestrict_SUBSET", 73 `rrestrict r s SUBSET r`, 74 REWRITE_TAC [in_rrestrict_alt, SUBSET_DEF] THEN REPEAT STRIP_TAC) ; 75 76val rrestrict_union = Q.store_thm ("rrestrict_union", 77`!r1 r2 s. rrestrict (r1 UNION r2) s = (rrestrict r1 s) UNION (rrestrict r2 s)`, 78SRW_TAC [] [rrestrict_def, EXTENSION] THEN 79METIS_TAC []); 80 81val rrestrict_rrestrict = Q.store_thm ("rrestrict_rrestrict", 82`!r x y. rrestrict (rrestrict r x) y = rrestrict r (x INTER y)`, 83SRW_TAC [] [rrestrict_def, EXTENSION] THEN 84EQ_TAC THEN 85SRW_TAC [] []); 86 87val domain_rrestrict_SUBSET = Q.store_thm ("domain_rrestrict_SUBSET", 88 `domain (rrestrict r s) SUBSET s`, 89 REWRITE_TAC [in_domain, SUBSET_DEF, in_rrestrict] THEN REPEAT STRIP_TAC) ; 90 91val range_rrestrict_SUBSET = Q.store_thm ("range_rrestrict_SUBSET", 92 `range (rrestrict r s) SUBSET s`, 93 REWRITE_TAC [in_range, SUBSET_DEF, in_rrestrict] THEN REPEAT STRIP_TAC) ; 94 95val rcomp_def = Define ` 96 rcomp r1 r2 = { (x, y) | ?z. (x, z) IN r1 /\ (z, y) IN r2}`; 97 98val _ = overload_on ("OO", ``rcomp``); 99val _ = set_fixity "OO" (Infixr 800); 100 101val strict_def = Define ` 102 strict r = {(x, y) | (x, y) IN r /\ x <> y}`; 103 104val strict_rrestrict = Q.store_thm ("strict_rrestrict", 105`!r s. strict (rrestrict r s) = rrestrict (strict r) s`, 106SRW_TAC [] [strict_def, rrestrict_def, EXTENSION] THEN 107METIS_TAC []); 108 109val univ_reln_def = Define ` 110 univ_reln xs = {(x1, x2) | x1 IN xs /\ x2 IN xs}`; 111 112val finite_prefixes_def = Define ` 113 finite_prefixes r s = !e. e IN s ==> FINITE {e' | (e', e) IN r}`; 114val _ = ot0 "finite_prefixes" "finitePrefixes" 115 116val finite_prefixes_subset_s = Q.store_thm ("finite_prefixes_subset_s", 117`!r s s'. finite_prefixes r s /\ s' SUBSET s ==> finite_prefixes r s'`, 118SRW_TAC [] [finite_prefixes_def, SUBSET_DEF]); 119 120val finite_prefixes_subset_r = Q.store_thm ("finite_prefixes_subset_r", 121`!r r' s. finite_prefixes r s /\ r' SUBSET r ==> finite_prefixes r' s`, 122 SRW_TAC [] [finite_prefixes_def, SUBSET_DEF] THEN 123 RES_TAC THEN IMP_RES_THEN MATCH_MP_TAC SUBSET_FINITE THEN 124 SRW_TAC [] [SUBSET_DEF]); 125 126val finite_prefixes_subset_rs = Q.store_thm ("finite_prefixes_subset_rs", 127`!r s r' s'. finite_prefixes r s ==> r' SUBSET r ==> s' SUBSET s ==> 128 finite_prefixes r' s'`, 129 REPEAT STRIP_TAC THEN IMP_RES_TAC finite_prefixes_subset_r THEN 130 IMP_RES_TAC finite_prefixes_subset_s) ; 131 132val finite_prefixes_subset = Q.store_thm ("finite_prefixes_subset", 133`!r s s'. 134 finite_prefixes r s /\ s' SUBSET s 135 ==> 136 finite_prefixes r s' /\ finite_prefixes (rrestrict r s') s'`, 137SRW_TAC [] [finite_prefixes_def, SUBSET_DEF, rrestrict_def, GSPEC_AND] THEN 138METIS_TAC [INTER_FINITE, INTER_COMM]); 139 140val finite_prefixes_union = Q.store_thm ("finite_prefixes_union", 141`!r1 r2 s1 s2. 142 finite_prefixes r1 s1 /\ finite_prefixes r2 s2 143 ==> 144 finite_prefixes (r1 UNION r2) (s1 INTER s2)`, 145SRW_TAC [] [finite_prefixes_def, GSPEC_OR]); 146 147val finite_prefixes_comp = Q.store_thm ("finite_prefixes_comp", 148`!r1 r2 s1 s2. 149 finite_prefixes r1 s1 /\ finite_prefixes r2 s2 /\ 150 { x | ?y. y IN s2 /\ (x, y) IN r2 } SUBSET s1 151 ==> 152 finite_prefixes (rcomp r1 r2) s2`, 153SRW_TAC [] [finite_prefixes_def, SUBSET_DEF, rcomp_def] THEN 154`{ e' | ?z. (e', z) IN r1 /\ (z, e) IN r2 } = 155 BIGUNION (IMAGE (\z. { e' | (e', z) IN r1}) { z | (z, e) IN r2 })` 156 by (SRW_TAC [] [EXTENSION] THEN 157 EQ_TAC THEN 158 SRW_TAC [] [] THENL 159 [Q.EXISTS_TAC `{ x | (x, z) IN r1 }` THEN 160 SRW_TAC [] [] THEN 161 METIS_TAC [], 162 METIS_TAC []]) THEN 163SRW_TAC [] [] THEN 164METIS_TAC []); 165 166val finite_prefixes_inj_image = Q.store_thm ("finite_prefixes_inj_image", 167`!f r s. 168 (!x y. (f x = f y) ==> (x = y)) /\ 169 finite_prefixes r s 170 ==> 171 finite_prefixes { (f x, f y) | (x, y) IN r } (IMAGE f s)`, 172SRW_TAC [] [finite_prefixes_def] THEN 173`{e' | ?x' y. ((e' = f x') /\ (f x = f y)) /\ (x',y) IN r} 174 SUBSET 175 IMAGE f { e' | (e', x) IN r }` 176 by (SRW_TAC [] [SUBSET_DEF] THEN 177 METIS_TAC []) THEN 178METIS_TAC [SUBSET_FINITE, IMAGE_FINITE]); 179 180val finite_prefixes_range = Q.store_thm ("finite_prefixes_range", 181`!r s t. finite_prefixes r s /\ DISJOINT t (range r) ==> 182 finite_prefixes r (s UNION t)`, 183SRW_TAC [] [finite_prefixes_def, DISJOINT_DEF, range_def, INTER_DEF, EXTENSION] THEN1 184METIS_TAC [] THEN 185`{e' | (e', e) IN r} = {}` 186 by (SRW_TAC [] [EXTENSION] THEN 187 METIS_TAC []) THEN 188METIS_TAC [FINITE_EMPTY]); 189 190(* ------------------------------------------------------------------------ *) 191(* Transitive closure *) 192(* ------------------------------------------------------------------------ *) 193 194val (tc_rules, tc_ind, tc_cases) = Hol_reln ` 195(!x y. r (x, y) ==> tc r (x, y)) /\ 196(!x y. (?z. tc r (x, z) /\ tc r (z, y)) ==> tc r (x, y))`; 197 198val tc_rules = Q.store_thm ("tc_rules", 199`!r. 200 (!x y. (x,y) IN r ==> (x, y) IN tc r) /\ 201 (!x y. (?z. (x, z) IN tc r /\ (z, y) IN tc r) ==> (x, y) IN tc r)`, 202SRW_TAC [] [SPECIFICATION, tc_rules]); 203 204val tc_cases = Q.store_thm ("tc_cases", 205`!r x y. 206 (x, y) IN tc r = 207 ((x, y) IN r) \/ 208 (?z. (x, z) IN tc r /\ (z, y) IN tc r)`, 209SRW_TAC [] [SPECIFICATION] THEN 210SRW_TAC [] [Once (Q.SPECL [`r`, `(x, y)`] tc_cases)]); 211 212val tc_ind = Q.store_thm ("tc_ind", 213`!r tc'. 214 (!x y. (x, y) IN r ==> tc' x y) /\ 215 (!x y. (?z. tc' x z /\ tc' z y) ==> tc' x y) ==> 216 !x y. (x, y) IN tc r ==> tc' x y`, 217SRW_TAC [] [SPECIFICATION] THEN 218IMP_RES_TAC (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM] 219 (Q.SPECL [`r`, `\(x, y). tc' x y`] tc_ind))); 220 221val [tc_rule1', tc_rule2] = CONJUNCTS (SPEC_ALL tc_rules) ; 222val tc_rule1 = Ho_Rewrite.REWRITE_RULE [GSYM FORALL_PROD] tc_rule1' ; 223 224(** closure rules for tc **) 225 226val tc_closure = Q.store_thm ("tc_closure", 227 `r SUBSET tc s ==> tc r SUBSET tc s`, 228 Ho_Rewrite.REWRITE_TAC [SUBSET_DEF, FORALL_PROD] THEN DISCH_TAC THEN 229 HO_MATCH_MP_TAC tc_ind THEN CONJ_TAC 230 THENL [ POP_ASSUM ACCEPT_TAC, MATCH_ACCEPT_TAC tc_rule2]) ; 231 232val subset_tc = Q.store_thm ("subset_tc", 233 `r SUBSET tc r`, 234 Ho_Rewrite.REWRITE_TAC [SUBSET_DEF, FORALL_PROD] THEN 235 MATCH_ACCEPT_TAC tc_rule1) ; 236 237val tc_idemp = Q.store_thm ("tc_idemp", 238 `tc (tc r) = tc r`, 239 REWRITE_TAC [SET_EQ_SUBSET] THEN CONJ_TAC 240 THENL [irule tc_closure THEN irule SUBSET_REFL, irule subset_tc]) ; 241 242val tc_mono = Q.store_thm ("tc_mono", 243 `r SUBSET s ==> tc r SUBSET tc s`, 244 DISCH_TAC THEN irule tc_closure THEN 245 irule SUBSET_TRANS THEN Q.EXISTS_TAC `s` THEN 246 ASM_REWRITE_TAC [subset_tc]) ; 247 248val tc_strongind = Q.store_thm ("tc_strongind", 249`!r tc'. 250 (!x y. (x, y) IN r ==> tc' x y) /\ 251 (!x y. (?z. (x,z) IN tc r /\ tc' x z /\ (z,y) IN tc r /\ tc' z y) ==> tc' x y) ==> 252 !x y. (x, y) IN tc r ==> tc' x y`, 253SRW_TAC [] [SPECIFICATION] THEN 254IMP_RES_TAC (SIMP_RULE (srw_ss()) [LAMBDA_PROD, GSYM PFORALL_THM] 255 (Q.SPECL [`r`, `\(x, y). tc' x y`] (fetch "-" "tc_strongind")))); 256 257val tc_cases_lem = Q.prove ( 258`!x y. 259 (x, y) IN tc r 260 ==> 261 (x, y) IN r \/ 262 ((?z. (x, z) IN tc r /\ (z, y) IN r) /\ 263 (?z. (x, z) IN r /\ (z, y) IN tc r))`, 264HO_MATCH_MP_TAC tc_ind THEN 265SRW_TAC [] [] THEN 266METIS_TAC [tc_rules]); 267 268val tc_cases_right = Q.store_thm ("tc_cases_right", 269`!r x y. 270 (x, y) IN tc r = 271 ((x, y) IN r) \/ 272 (?z. (x, z) IN tc r /\ (z, y) IN r)`, 273METIS_TAC [tc_cases_lem, tc_rules]); 274 275val tc_cases_left = Q.store_thm ("tc_cases_left", 276`!r x y. 277 (x, y) IN tc r = 278 ((x, y) IN r) \/ 279 (?z. (x, z) IN r /\ (z, y) IN tc r)`, 280METIS_TAC [tc_cases_lem, tc_rules]); 281 282val tc_ind_left_lem = Q.prove ( 283`!r P. 284 (!x y. (x, y) IN r ==> P x y) /\ 285 (!x y. (?z. (x, z) IN r /\ P z y) ==> P x y) 286 ==> 287 (!x y. (x, y) IN tc r ==> (!z. P x y /\ P y z ==> P x z) /\ P x y)`, 288NTAC 3 STRIP_TAC THEN 289HO_MATCH_MP_TAC tc_ind THEN 290SRW_TAC [] [] THEN 291METIS_TAC []); 292 293val tc_ind_left = Q.store_thm ("tc_ind_left", 294`!r tc'. 295 (!x y. (x, y) IN r ==> tc' x y) /\ 296 (!x y. (?z. (x, z) IN r /\ tc' z y) ==> tc' x y) 297 ==> 298 (!x y. (x, y) IN tc r ==> tc' x y)`, 299METIS_TAC [tc_ind_left_lem]); 300 301val tc_strongind_left_lem = Q.prove ( 302`!r P. 303 (!x y. (x, y) IN r ==> P x y) /\ 304 (!x y. (?z. (x, z) IN r /\ (z,y) IN tc r /\ P z y) ==> P x y) 305 ==> 306 (!x y. (x, y) IN tc r ==> 307 (!z. P x y /\ P y z /\ (y,z) IN tc r ==> P x z) /\ P x y)`, 308NTAC 3 STRIP_TAC THEN 309HO_MATCH_MP_TAC tc_strongind THEN 310SRW_TAC [] [] THEN 311METIS_TAC [tc_rules]); 312 313val tc_strongind_left = Q.store_thm ("tc_strongind_left", 314`!r tc'. 315 (!x y. (x, y) IN r ==> tc' x y) /\ 316 (!x y. (?z. (x, z) IN r /\ (z,y) IN tc r /\ tc' z y) ==> tc' x y) 317 ==> 318 (!x y. (x, y) IN tc r ==> tc' x y)`, 319METIS_TAC [tc_strongind_left_lem]); 320 321val tc_ind_right_lem = Q.prove ( 322`!r P. 323 (!x y. (x, y) IN r ==> P x y) /\ 324 (!x y. (?z. P x z /\ (z, y) IN r) ==> P x y) 325 ==> 326 (!x y. (x, y) IN tc r ==> (!z. P z x /\ P x y ==> P z y) /\ P x y)`, 327NTAC 3 STRIP_TAC THEN 328HO_MATCH_MP_TAC tc_ind THEN 329SRW_TAC [] [] THEN 330METIS_TAC []); 331 332val tc_ind_right = Q.store_thm ("tc_ind_right", 333`!r tc'. 334 (!x y. (x, y) IN r ==> tc' x y) /\ 335 (!x y. (?z. tc' x z /\ (z, y) IN r) ==> tc' x y) 336 ==> 337 (!x y. (x, y) IN tc r ==> tc' x y)`, 338METIS_TAC [tc_ind_right_lem]); 339 340val rtc_ind_right = Q.store_thm ("rtc_ind_right", 341`!r tc'. 342 (!x. x IN domain r \/ x IN range r ==> tc' x x) /\ 343 (!x y. (?z. tc' x z /\ (z,y) IN r) ==> tc' x y) 344 ==> 345 (!x y. (x,y) IN tc r ==> tc' x y)`, 346NTAC 3 STRIP_TAC THEN 347HO_MATCH_MP_TAC tc_ind_right THEN 348SRW_TAC [] [] THEN 349FULL_SIMP_TAC (srw_ss()) [domain_def, range_def] THEN 350METIS_TAC []); 351 352val tc_strongind_right_lem = Q.prove ( 353`!r P. 354 (!x y. (x, y) IN r ==> P x y) /\ 355 (!x y. (?z. (x,z) IN tc r /\ P x z /\ (z, y) IN r) ==> P x y) 356 ==> 357 (!x y. (x, y) IN tc r ==> 358 (!z. (z,x) IN tc r /\ P z x /\ P x y ==> P z y) /\ P x y)`, 359NTAC 3 STRIP_TAC THEN 360HO_MATCH_MP_TAC tc_strongind THEN 361SRW_TAC [] [] THEN 362METIS_TAC [tc_rules]); 363 364val tc_strongind_right = Q.store_thm ("tc_strongind_right", 365`!r tc'. 366 (!x y. (x, y) IN r ==> tc' x y) /\ 367 (!x y. (?z. (x,z) IN tc r /\ tc' x z /\ (z, y) IN r) ==> tc' x y) 368 ==> 369 (!x y. (x, y) IN tc r ==> tc' x y)`, 370METIS_TAC [tc_strongind_right_lem]); 371 372val tc_union = Q.store_thm ("tc_union", 373`!x y. (x, y) IN tc r1 ==> !r2. (x, y) IN tc (r1 UNION r2)`, 374HO_MATCH_MP_TAC tc_ind THEN 375SRW_TAC [] [] THENL 376[SRW_TAC [] [Once tc_cases], 377 METIS_TAC [tc_rules]]); 378 379val tc_implication_lem = Q.prove ( 380`!x y. (x, y) IN tc r1 ==> 381 !r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==> (x, y) IN tc r2`, 382HO_MATCH_MP_TAC tc_ind THEN 383SRW_TAC [] [] THEN 384METIS_TAC [tc_rules]); 385 386val tc_implication = Q.store_thm ("tc_implication", 387`!r1 r2. (!x y. (x, y) IN r1 ==> (x, y) IN r2) ==> 388 (!x y. (x, y) IN tc r1 ==> (x, y) IN tc r2)`, 389METIS_TAC [tc_implication_lem]); 390 391val tc_empty = Q.prove ( 392`!x y. (x, y) IN tc {} ==> F`, 393HO_MATCH_MP_TAC tc_ind THEN 394SRW_TAC [] []); 395 396val _ = save_thm ("tc_empty", SIMP_RULE (srw_ss()) [] tc_empty); 397 398val tc_empty_eqn = Q.store_thm( 399 "tc_empty_eqn[simp]", 400 `tc {} = {}`, 401 asm_simp_tac(srw_ss())[EXTENSION, pairTheory.FORALL_PROD, tc_empty]) 402 403val tc_domain_range = Q.store_thm ("tc_domain_range", 404`!x y. (x, y) IN tc r ==> x IN domain r /\ y IN range r`, 405HO_MATCH_MP_TAC tc_ind THEN 406SRW_TAC [] [domain_def, range_def] THEN 407METIS_TAC []); 408 409val rrestrict_tc = Q.store_thm ("rrestrict_tc", 410`!e e'. (e, e') IN tc (rrestrict r x) ==> (e, e') IN tc r`, 411HO_MATCH_MP_TAC tc_ind THEN 412SRW_TAC [] [rrestrict_def] THEN 413METIS_TAC [tc_rules]); 414 415val pair_in_IMAGE_SWAP = Q.prove ( 416 `((a, b) IN IMAGE SWAP r) = ((b, a) IN r)`, 417 Ho_Rewrite.REWRITE_TAC [IN_IMAGE, EXISTS_PROD, SWAP_def, 418 FST, SND, PAIR_EQ] THEN 419 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN PROVE_TAC []) ; 420 421val tc_ind' = Ho_Rewrite.REWRITE_RULE [PULL_FORALL] tc_ind ; 422 423val tc_SWAP = Q.store_thm ("tc_SWAP", 424 `tc (IMAGE SWAP r) = IMAGE SWAP (tc r)`, 425 Ho_Rewrite.REWRITE_TAC [SET_EQ_SUBSET, SUBSET_DEF, 426 FORALL_PROD, pair_in_IMAGE_SWAP] THEN CONJ_TAC 427 THENL [ 428 HO_MATCH_MP_TAC tc_ind THEN 429 REWRITE_TAC [pair_in_IMAGE_SWAP] THEN REPEAT STRIP_TAC 430 THENL [IMP_RES_TAC tc_rule1, IMP_RES_TAC tc_rule2], 431 REPEAT GEN_TAC THEN HO_MATCH_MP_TAC tc_ind' THEN REPEAT STRIP_TAC 432 THENL [irule tc_rule1 THEN ASM_REWRITE_TAC [pair_in_IMAGE_SWAP], 433 IMP_RES_TAC tc_rule2]]) ; 434 435(* ------------------------------------------------------------------------ *) 436(* Acyclic relations *) 437(* ------------------------------------------------------------------------ *) 438 439val acyclic_def = Define ` 440 acyclic r = !x. (x, x) NOTIN tc r`; 441 442val acyclic_subset = Q.store_thm ("acyclic_subset", 443`!r1 r2. acyclic r1 /\ r2 SUBSET r1 ==> acyclic r2`, 444SRW_TAC [] [acyclic_def, SUBSET_DEF] THEN 445METIS_TAC [tc_implication_lem]); 446 447val acyclic_union = Q.store_thm ("acyclic_union", 448`!r1 r2. acyclic (r1 UNION r2) ==> acyclic r1 /\ acyclic r2`, 449SRW_TAC [] [acyclic_def] THEN 450METIS_TAC [tc_union, UNION_COMM]); 451 452val acyclic_rrestrict = Q.store_thm ("acyclic_rrestrict", 453`!r s. acyclic r ==> acyclic (rrestrict r s)`, 454SRW_TAC [] [rrestrict_def] THEN 455`r = {(x,y) | (x,y) IN r /\ x IN s /\ y IN s} UNION r` 456 by SRW_TAC [] [UNION_DEF, rextension, EQ_IMP_THM] THEN 457METIS_TAC [acyclic_union]); 458 459val acyclic_irreflexive = Q.store_thm ("acyclic_irreflexive", 460`!r x. acyclic r ==> (x, x) NOTIN r`, 461SRW_TAC [] [acyclic_def] THEN 462METIS_TAC [tc_cases]); 463 464val acyclic_SWAP = Q.store_thm ("acyclic_SWAP", 465 `acyclic (IMAGE SWAP r) = acyclic r`, 466 REWRITE_TAC [acyclic_def, tc_SWAP, pair_in_IMAGE_SWAP]) ; 467 468val tc_BIGUNION_lem = Q.prove ( 469`!x y. (x, y) IN tc (BIGUNION rs) ==> 470(!r r'. 471 r IN rs /\ r' IN rs /\ r <> r' 472 ==> 473 DISJOINT (domain r UNION range r) (domain r' UNION range r')) ==> 474?r. r IN rs /\ (x, y) IN tc r`, 475HO_MATCH_MP_TAC tc_ind THEN 476SRW_TAC [] [] THEN1 477METIS_TAC [tc_rules] THEN 478RES_TAC THEN 479IMP_RES_TAC tc_domain_range THEN 480FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN 481`r = r'` 482 by (SRW_TAC [] [EXTENSION] THEN 483 METIS_TAC []) THEN 484METIS_TAC [tc_rules]); 485 486val acyclic_bigunion = Q.store_thm ("acyclic_bigunion", 487`!rs. 488 (!r r'. 489 r IN rs /\ r' IN rs /\ r <> r' 490 ==> 491 DISJOINT (domain r UNION range r) (domain r' UNION range r')) /\ 492 (!r. r IN rs ==> acyclic r) 493 ==> 494 acyclic (BIGUNION rs)`, 495SRW_TAC [] [acyclic_def] THEN 496CCONTR_TAC THEN 497FULL_SIMP_TAC (srw_ss()) [] THEN 498IMP_RES_TAC tc_BIGUNION_lem THEN 499FULL_SIMP_TAC (srw_ss()) [] THEN 500METIS_TAC []); 501 502val acyclic_union = Q.store_thm ("acyclic_union", 503`!r r'. 504 DISJOINT (domain r UNION range r) (domain r' UNION range r') /\ 505 acyclic r /\ 506 acyclic r' 507 ==> 508 acyclic (r UNION r')`, 509SRW_TAC [] [] THEN 510MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.SPEC `{r; r'}` acyclic_bigunion)) THEN 511SRW_TAC [] [] THEN 512METIS_TAC [DISJOINT_SYM]); 513 514(* ------------------------------------------------------------------------ *) 515(* Orders *) 516(* ------------------------------------------------------------------------ *) 517 518val reflexive_def = Define ` 519 reflexive r s = !x. x IN s ==> (x, x) IN r`; 520 521val irreflexive_def = Define ` 522 irreflexive r s = !x. x IN s ==> (x, x) NOTIN r`; 523 524val transitive_def = Define ` 525 transitive r = 526 !x y z. (x, y) IN r /\ (y, z) IN r ==> (x, z) IN r`; 527val _ = ot "transitive" 528 529val transitive_tc_lem = Q.prove ( 530`!x y. (x, y) IN tc r ==> transitive r ==> (x, y) IN r`, 531HO_MATCH_MP_TAC tc_ind THEN 532SRW_TAC [] [] THEN 533RES_TAC THEN 534FULL_SIMP_TAC (srw_ss()) [transitive_def] THEN 535METIS_TAC []); 536 537val transitive_tc = Q.store_thm ("transitive_tc", 538`!r. transitive r ==> (tc r = r)`, 539SRW_TAC [] [EXTENSION] THEN 540EQ_TAC THEN 541SRW_TAC [] [] THEN 542Cases_on `x` THEN1 543METIS_TAC [transitive_tc_lem] THEN 544FULL_SIMP_TAC (srw_ss()) [transitive_def] THEN 545METIS_TAC [tc_rules]); 546 547val tc_transitive = Q.store_thm ("tc_transitive", 548`!r. transitive (tc r)`, 549SRW_TAC [] [transitive_def] THEN 550METIS_TAC [tc_rules]); 551 552val antisym_def = Define ` 553 antisym r = !x y. (x, y) IN r /\ (y, x) IN r ==> (x = y)`; 554val _ = ot0 "antisym" "antisymmetric" 555 556val partial_order_def = Define ` 557 partial_order r s = 558 domain r SUBSET s /\ range r SUBSET s /\ 559 transitive r /\ reflexive r s /\ antisym r`; 560 561val antisym_subset = Q.store_thm ("antisym_subset", 562 `antisym t ==> s SUBSET t ==> antisym s`, 563 REWRITE_TAC [antisym_def, SUBSET_DEF] THEN 564 REPEAT STRIP_TAC THEN RES_TAC THEN 565 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC []) ; 566 567val partial_order_dom_rng = Q.store_thm ("partial_order_dom_rng", 568`!r s x y. (x, y) IN r /\ partial_order r s ==> x IN s /\ y IN s`, 569SRW_TAC [] [partial_order_def, domain_def, range_def, SUBSET_DEF] THEN 570METIS_TAC []); 571 572val partial_order_subset = Q.store_thm ("partial_order_subset", 573`!r s s'. 574 partial_order r s /\ s' SUBSET s ==> partial_order (rrestrict r s') s'`, 575SRW_TAC [] [partial_order_def, SUBSET_DEF, reflexive_def, transitive_def, 576 antisym_def, domain_def, range_def, rrestrict_def] THEN 577METIS_TAC []); 578 579val strict_partial_order = Q.store_thm ("strict_partial_order", 580`!r s. 581 partial_order r s 582 ==> 583 domain (strict r) SUBSET s /\ range (strict r) SUBSET s /\ 584 transitive (strict r) /\ antisym (strict r)`, 585SRW_TAC [] [domain_def, SUBSET_DEF, range_def, partial_order_def, strict_def] 586THENL 587[METIS_TAC [], 588 METIS_TAC [], 589 FULL_SIMP_TAC (srw_ss()) [transitive_def, strict_def, antisym_def] THEN 590 METIS_TAC [], 591 FULL_SIMP_TAC (srw_ss()) [antisym_def] THEN 592 METIS_TAC []]); 593 594val strict_partial_order_acyclic = Q.store_thm ("strict_partial_order_acyclic", 595`!r s. partial_order r s ==> acyclic (strict r)`, 596SRW_TAC [] [acyclic_def] THEN 597IMP_RES_TAC strict_partial_order THEN 598SRW_TAC [] [transitive_tc, strict_def]); 599 600val linear_order_def = Define ` 601 linear_order r s = 602 domain r SUBSET s /\ range r SUBSET s /\ 603 transitive r /\ antisym r /\ 604 (!x y. x IN s /\ y IN s ==> (x, y) IN r \/ (y, x) IN r)`; 605val _ = ot0 "linear_order" "linearOrder" 606 607val linear_order_subset = Q.store_thm ("linear_order_subset", 608`!r s s'. 609 linear_order r s /\ s' SUBSET s ==> linear_order (rrestrict r s') s'`, 610SRW_TAC [] [linear_order_def, SUBSET_DEF, transitive_def, 611 antisym_def, domain_def, range_def, rrestrict_def] THEN 612METIS_TAC []); 613 614val partial_order_linear_order = Q.store_thm ("partial_order_linear_order", 615`!r s. linear_order r s ==> partial_order r s`, 616SRW_TAC [] [linear_order_def, partial_order_def, reflexive_def] THEN 617METIS_TAC []); 618 619val strict_linear_order_def = Define ` 620 strict_linear_order r s = 621 domain r SUBSET s /\ range r SUBSET s /\ 622 transitive r /\ 623 (!x. (x, x) NOTIN r) /\ 624 (!x y. x IN s /\ y IN s /\ x <> y ==> (x, y) IN r \/ (y, x) IN r)`; 625 626val strict_linear_order_dom_rng = Q.store_thm ("strict_linear_order_dom_rng", 627`!r s x y. (x, y) IN r /\ strict_linear_order r s ==> x IN s /\ y IN s`, 628SRW_TAC [] [strict_linear_order_def, domain_def, range_def, SUBSET_DEF] THEN 629METIS_TAC []); 630 631val linear_order_dom_rng = Q.store_thm ("linear_order_dom_rng", 632`!r s x y. (x, y) IN r /\ linear_order r s ==> x IN s /\ y IN s`, 633SRW_TAC [] [linear_order_def, domain_def, range_def, SUBSET_DEF] THEN 634METIS_TAC []); 635 636(* ------------------------------------------------------------------------ *) 637(* Link to relation theory *) 638(* ------------------------------------------------------------------------ *) 639val reln_to_rel_def = Define `reln_to_rel r = (\x y. (x,y) IN r)` 640val rel_to_reln_def = Define `rel_to_reln R = {(x, y) | x, y | R x y}` 641val RRUNIV_def = Define `RRUNIV s = (\x y. x IN s /\ y IN s)` 642val RREFL_EXP_def = Define `RREFL_EXP R s = (R RUNION (\x y. (x = y) /\ ~(x IN s) ))` 643 644val RREFL_EXP_RSUBSET = Q.store_thm ("RREFL_EXP_RSUBSET", 645`R RSUBSET (RREFL_EXP R s)`, 646SRW_TAC [] [RSUBSET, RREFL_EXP_def, RUNION]); 647 648val RREFL_EXP_UNIV = Q.store_thm ("RREFL_EXP_UNIV", 649`RREFL_EXP R UNIV = R`, 650SRW_TAC [] [FUN_EQ_THM, RREFL_EXP_def, RUNION]); 651 652val REL_RESTRICT_UNIV = Q.store_thm ("REL_RESTRICT_UNIV", 653`REL_RESTRICT R UNIV = R`, 654SRW_TAC [] [FUN_EQ_THM, REL_RESTRICT_DEF, RINTER, RRUNIV_def]); 655 656val in_rel_to_reln = Q.store_thm ("in_rel_to_reln", 657`xy IN (rel_to_reln R) = R (FST xy) (SND xy)`, 658Cases_on `xy` THEN SRW_TAC [] [rel_to_reln_def]) 659 660val reln_to_rel_app = Q.store_thm ("reln_to_rel_app", 661`(reln_to_rel r) x y = (x, y) IN r`, 662SRW_TAC [] [reln_to_rel_def]) 663 664val rel_to_reln_IS_UNCURRY = Q.store_thm ("rel_to_reln_IS_UNCURRY", 665 `rel_to_reln = UNCURRY`, 666 REWRITE_TAC [FUN_EQ_THM, 667 REWRITE_RULE [IN_APP] in_rel_to_reln, UNCURRY_VAR]) ; 668 669val reln_to_rel_IS_CURRY = Q.store_thm ("reln_to_rel_IS_CURRY", 670 `reln_to_rel = CURRY`, 671 REWRITE_TAC [FUN_EQ_THM, CURRY_DEF, reln_to_rel_app, IN_APP]) ; 672 673val rel_to_reln_inv = Q.store_thm ("rel_to_reln_inv", 674`reln_to_rel (rel_to_reln R) = R`, 675SRW_TAC [] [reln_to_rel_def, rel_to_reln_def, FUN_EQ_THM]) 676 677val reln_to_rel_inv = Q.store_thm ("reln_to_rel_inv", 678`rel_to_reln (reln_to_rel r) = r`, 679SRW_TAC [] [reln_to_rel_app, EXTENSION, in_rel_to_reln]); 680 681val reln_to_rel_11 = Q.store_thm ("reln_to_rel_11", 682`(reln_to_rel r1 = reln_to_rel r2) <=> (r1 = r2)`, 683SRW_TAC [] [reln_to_rel_app, FUN_EQ_THM, FORALL_PROD, IN_DEF]) 684 685val rel_to_reln_11 = Q.store_thm ("rel_to_reln_11", 686`(rel_to_reln R1 = rel_to_reln R2) <=> (R1 = R2)`, 687SRW_TAC [] [in_rel_to_reln, EXTENSION, FORALL_PROD] THEN 688SRW_TAC [] [FUN_EQ_THM]); 689 690val reln_rel_conv_props = 691LIST_CONJ [in_rel_to_reln, reln_to_rel_app, rel_to_reln_inv, reln_to_rel_inv, 692reln_to_rel_11, rel_to_reln_11] 693 694val rel_to_reln_swap = Q.store_thm("rel_to_reln_swap", 695`(r = rel_to_reln R) <=> (reln_to_rel r = R)`, 696METIS_TAC [rel_to_reln_inv, reln_to_rel_inv]); 697 698val domain_to_rel_conv = Q.store_thm ("domain_to_rel_conv", 699 `domain r = RDOM (reln_to_rel r)`, 700SRW_TAC [] [domain_def, EXTENSION, IN_RDOM, reln_rel_conv_props]) 701 702val range_to_rel_conv = Q.store_thm ("range_to_rel_conv", 703 `range r = RRANGE (reln_to_rel r)`, 704SRW_TAC [] [range_def, EXTENSION, IN_RRANGE, reln_rel_conv_props]) 705 706val strict_to_rel_conv = Q.store_thm ("strict_to_rel_conv", 707 `strict r = rel_to_reln (STRORD (reln_to_rel r))`, 708SRW_TAC [] [strict_def, rextension, reln_rel_conv_props, STRORD]); 709 710val rrestrict_to_rel_conv = Q.store_thm ("rrestrict_to_rel_conv", 711 `rrestrict r s = rel_to_reln (REL_RESTRICT (reln_to_rel r) s)`, 712SRW_TAC [boolSimps.EQUIV_EXTRACT_ss] [rrestrict_def, rextension, reln_rel_conv_props, REL_RESTRICT_DEF, RINTER, RRUNIV_def]) 713 714val rcomp_to_rel_conv = Q.store_thm ("rcomp_to_rel_conv", 715 `r1 OO r2 = rel_to_reln ((reln_to_rel r2) O (reln_to_rel r1))`, 716SRW_TAC [] [rcomp_def, rextension, reln_rel_conv_props, relationTheory.O_DEF]) 717 718val univ_reln_to_rel_conv = Q.store_thm ("univ_reln_to_rel_conv", 719 `univ_reln s = rel_to_reln (RRUNIV s)`, 720SRW_TAC [] [univ_reln_def, rextension, reln_rel_conv_props, RRUNIV_def]) 721 722val tc_to_rel_conv = Q.store_thm ("tc_to_rel_conv", 723`tc r = rel_to_reln ((reln_to_rel r)^+)`, 724SRW_TAC [] [rextension, reln_rel_conv_props] THEN 725EQ_TAC THENL [ 726 MATCH_MP_TAC tc_ind THEN 727 METIS_TAC [TC_RULES, reln_to_rel_app], 728 729 Q.SPEC_TAC (`y`, `y`) THEN 730 Q.SPEC_TAC (`x`, `x`) THEN 731 HO_MATCH_MP_TAC TC_INDUCT THEN 732 METIS_TAC [tc_rules, reln_to_rel_app] 733]) 734 735val acyclic_reln_to_rel_conv = Q.store_thm ("acyclic_reln_to_rel_conv", 736`acyclic r = irreflexive ((reln_to_rel r)^+)`, 737SRW_TAC [] [acyclic_def, tc_to_rel_conv, reln_rel_conv_props] THEN 738SRW_TAC [] [FUN_EQ_THM, relationTheory.irreflexive_def]) 739 740val irreflexive_reln_to_rel_conv = Q.store_thm ("irreflexive_reln_to_rel_conv", 741`(set_relation$irreflexive) r s = (relation$irreflexive) (REL_RESTRICT (reln_to_rel r) s)`, 742SRW_TAC [] [irreflexive_def, relationTheory.irreflexive_def, REL_RESTRICT_DEF, RINTER, RRUNIV_def, reln_rel_conv_props] THEN 743PROVE_TAC[]) 744 745val irreflexive_reln_to_rel_conv_UNIV = Q.store_thm ("irreflexive_reln_to_rel_conv_UNIV", 746`(set_relation$irreflexive) r UNIV = (relation$irreflexive) (reln_to_rel r)`, 747SIMP_TAC std_ss [irreflexive_reln_to_rel_conv, REL_RESTRICT_UNIV]) 748 749val reflexive_reln_to_rel_conv = Q.store_thm ("reflexive_reln_to_rel_conv", 750`(set_relation$reflexive) r s = (relation$reflexive) (RREFL_EXP (reln_to_rel r) s)`, 751SRW_TAC [] [reflexive_def, relationTheory.reflexive_def, reln_rel_conv_props, RREFL_EXP_def, RUNION, RRUNIV_def] THEN 752PROVE_TAC[]) 753 754val reflexive_reln_to_rel_conv_UNIV = Q.store_thm ("reflexive_reln_to_rel_conv_UNIV", 755`(set_relation$reflexive) r UNIV = (relation$reflexive) (reln_to_rel r)`, 756REWRITE_TAC[reflexive_reln_to_rel_conv, RREFL_EXP_UNIV]) 757 758val transitive_reln_to_rel_conv = Q.store_thm ("reflexive_reln_to_rel_conv", 759`(set_relation$transitive) r = (relation$transitive) (reln_to_rel r)`, 760SRW_TAC [] [transitive_def, relationTheory.transitive_def, reln_rel_conv_props]) 761 762val antisym_reln_to_rel_conv = Q.store_thm ("antisym_reln_to_rel_conv", 763`(set_relation$antisym) r = (relation$antisymmetric) (reln_to_rel r)`, 764SRW_TAC [] [antisym_def, relationTheory.antisymmetric_def, reln_rel_conv_props]) 765 766local 767 768val aux1 = prove(``((reln_to_rel r) RSUBSET RRUNIV s) = 769 (domain r SUBSET s /\ range r SUBSET s)``, 770SRW_TAC [] [RSUBSET, RRUNIV_def, domain_def, range_def, reln_to_rel_app, SUBSET_DEF] THEN 771PROVE_TAC[]) 772 773val aux2 = prove(``(domain r SUBSET s /\ range r SUBSET s) ==> 774 (transitive (RREFL_EXP (reln_to_rel r) s) = 775 transitive (reln_to_rel r))``, 776SRW_TAC [] [relationTheory.transitive_def, RREFL_EXP_def, RUNION, reln_to_rel_app, SUBSET_DEF, in_range, in_domain, 777 GSYM LEFT_FORALL_IMP_THM] THEN 778PROVE_TAC[]) 779 780val aux3 = prove(``(domain r SUBSET s /\ range r SUBSET s) ==> 781 (antisymmetric (RREFL_EXP (reln_to_rel r) s) = 782 antisymmetric (reln_to_rel r))``, 783SRW_TAC [] [relationTheory.antisymmetric_def, RREFL_EXP_def, RUNION, reln_to_rel_app, SUBSET_DEF, in_range, in_domain, 784 GSYM LEFT_FORALL_IMP_THM] THEN 785PROVE_TAC[]) 786 787in 788 789val partial_order_reln_to_rel_conv = Q.store_thm ("partial_order_reln_to_rel_conv", 790`partial_order r s = ((reln_to_rel r) RSUBSET RRUNIV s) /\ 791 WeakOrder (RREFL_EXP (reln_to_rel r) s)`, 792SRW_TAC [boolSimps.EQUIV_EXTRACT_ss] [partial_order_def, WeakOrder, reflexive_reln_to_rel_conv, 793 transitive_reln_to_rel_conv, antisym_reln_to_rel_conv, 794 aux1, aux2, aux3]); 795 796val partial_order_reln_to_rel_conv_UNIV = Q.store_thm ("partial_order_reln_to_rel_conv_UNIV", 797`partial_order r UNIV = WeakOrder (reln_to_rel r)`, 798SRW_TAC [] [partial_order_reln_to_rel_conv, RREFL_EXP_UNIV, RSUBSET, RRUNIV_def]); 799 800end 801 802val linear_order_reln_to_rel_conv_UNIV = Q.store_thm ("linear_order_reln_to_rel_conv_UNIV", 803`linear_order r UNIV = WeakLinearOrder (reln_to_rel r)`, 804SRW_TAC [] [linear_order_def, WeakLinearOrder_dichotomy, reflexive_reln_to_rel_conv_UNIV, 805 transitive_reln_to_rel_conv, antisym_reln_to_rel_conv, WeakOrder, 806 relationTheory.reflexive_def, reln_to_rel_app] THEN 807PROVE_TAC[]); 808 809val strict_linear_order_reln_to_rel_conv_UNIV = Q.store_thm ("strict_linear_order_reln_to_rel_conv_UNIV", 810`strict_linear_order r UNIV = StrongLinearOrder (reln_to_rel r)`, 811SRW_TAC [] [strict_linear_order_def, StrongLinearOrder, reflexive_reln_to_rel_conv_UNIV, 812 transitive_reln_to_rel_conv, antisym_reln_to_rel_conv, StrongOrder, 813 relationTheory.irreflexive_def, reln_to_rel_app, trichotomous] THEN 814PROVE_TAC[]); 815 816val reln_rel_conv_thms = save_thm ("reln_rel_conv_thms", LIST_CONJ [ 817 reln_rel_conv_props, 818 RREFL_EXP_UNIV, 819 REL_RESTRICT_UNIV, 820 domain_to_rel_conv, 821 range_to_rel_conv, 822 strict_to_rel_conv, 823 rrestrict_to_rel_conv, 824 rcomp_to_rel_conv, 825 univ_reln_to_rel_conv, 826 tc_to_rel_conv, 827 acyclic_reln_to_rel_conv, 828 irreflexive_reln_to_rel_conv, 829 reflexive_reln_to_rel_conv, 830 transitive_reln_to_rel_conv, 831 antisym_reln_to_rel_conv, 832 partial_order_reln_to_rel_conv_UNIV, 833 linear_order_reln_to_rel_conv_UNIV, 834 strict_linear_order_reln_to_rel_conv_UNIV]) 835 836 837val acyclic_WF = Q.store_thm ("acyclic_WF", 838`FINITE s /\ acyclic r /\ domain r SUBSET s /\ range r SUBSET s ==> 839 WF (reln_to_rel r)`, 840REPEAT STRIP_TAC THEN 841`(REL_RESTRICT (reln_to_rel r) s) = (reln_to_rel r)` by ( 842 FULL_SIMP_TAC std_ss [SUBSET_DEF, in_domain, in_range, 843 GSYM LEFT_FORALL_IMP_THM, FUN_EQ_THM, 844 REL_RESTRICT_DEF, reln_to_rel_app] THEN 845 PROVE_TAC[] 846) THEN 847FULL_SIMP_TAC std_ss [acyclic_reln_to_rel_conv] THEN 848PROVE_TAC[FINITE_WF_noloops]); 849 850(* ------------------------------------------------------------------------ *) 851(* Minimal and maximal elements *) 852(* ------------------------------------------------------------------------ *) 853 854val maximal_elements_def = Define ` 855 maximal_elements xs r = 856 {x | x IN xs /\ !x'. x' IN xs /\ (x, x') IN r ==> (x = x')}`; 857 858val minimal_elements_def = Define ` 859 minimal_elements xs r = 860 {x | x IN xs /\ !x'. x' IN xs /\ (x', x) IN r ==> (x = x')}`; 861val _ = ot0 "minimal_elements" "minimalElements" 862 863val minimal_elements_subset = Q.store_thm ("minimal_elements_subset", 864 `minimal_elements s lo SUBSET s`, 865 SRW_TAC [] [SUBSET_DEF, minimal_elements_def]) ; 866 867val minimal_elements_SWAP = Q.store_thm ("minimal_elements_SWAP", 868 `minimal_elements xs (IMAGE SWAP r) = maximal_elements xs r`, 869 REWRITE_TAC [minimal_elements_def, maximal_elements_def, 870 EXTENSION, pair_in_IMAGE_SWAP]) ; 871 872val maximal_union = Q.store_thm ("maximal_union", 873`!e s r1 r2. 874 e IN maximal_elements s (r1 UNION r2) 875 ==> 876 e IN maximal_elements s r1 /\ 877 e IN maximal_elements s r2`, 878SRW_TAC [] [maximal_elements_def]); 879 880val minimal_union = Q.store_thm ("minimal_union", 881`!e s r1 r2. 882 e IN minimal_elements s (r1 UNION r2) 883 ==> 884 e IN minimal_elements s r1 /\ 885 e IN minimal_elements s r2`, 886SRW_TAC [] [minimal_elements_def]); 887 888val minimal_elements_mono = Q.store_thm ("minimal_elements_mono", 889 `r SUBSET r' ==> minimal_elements xs r' SUBSET minimal_elements xs r`, 890 Ho_Rewrite.REWRITE_TAC [minimal_elements_def, SUBSET_DEF, IN_GSPEC_IFF] THEN 891 REPEAT STRIP_TAC THENL [FIRST_ASSUM ACCEPT_TAC, REPEAT RES_TAC]) ; 892 893val minimal_elements_rrestrict = Q.store_thm ("minimal_elements_rrestrict", 894 `minimal_elements xs (rrestrict r xs) = minimal_elements xs r`, 895 Ho_Rewrite.REWRITE_TAC [minimal_elements_def, 896 in_rrestrict, EXTENSION, IN_GSPEC_IFF] THEN 897 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 898 (FIRST_ASSUM ACCEPT_TAC ORELSE RES_TAC)) ; 899 900val WF_has_minimal_path = Q.store_thm ("WF_has_minimal_path", 901 `WF (reln_to_rel r) ==> x IN s ==> 902 ?y. y IN minimal_elements s r /\ ((y,x) IN tc r \/ (y = x))`, 903 Ho_Rewrite.REWRITE_TAC 904 [WF_DEF, reln_to_rel_app, minimal_elements_def, IN_GSPEC_IFF] THEN 905 REPEAT STRIP_TAC THEN 906 VALIDATE (FIRST_X_ASSUM (ASSUME_TAC o UNDISCH o 907 Q.SPEC `\z. z IN s /\ ((z, x) IN tc r \/ (z = x))`)) 908 THENL [ 909 Q.EXISTS_TAC `x` THEN BETA_TAC THEN 910 ASM_REWRITE_TAC [], 911 POP_ASSUM CHOOSE_TAC THEN 912 Q.EXISTS_TAC `min` THEN 913 RULE_L_ASSUM_TAC (CONJUNCTS o BETA_RULE) THEN 914 ASM_REWRITE_TAC [] THEN 915 REPEAT STRIP_TAC THEN RES_TAC THEN 916 IMP_RES_TAC tc_rule1 THEN 917 FIRST_ASSUM DISJ_CASES_TAC 918 THENL [ 919 IMP_RES_TAC tc_rule2, 920 BasicProvers.VAR_EQ_TAC] THEN 921 RES_TAC]) ; 922 923val tc_path_max_lem = Q.prove ( 924`!s. FINITE s ==> 925 s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s (tc r)`, 926HO_MATCH_MP_TAC FINITE_INDUCT THEN 927SRW_TAC [] [] THEN 928Cases_on `s={}` THEN1 929SRW_TAC [] [maximal_elements_def] THEN 930RES_TAC THEN 931Cases_on `(x, e) IN (tc r)` THENL 932[Q.EXISTS_TAC `e` THEN 933 SRW_TAC [] [maximal_elements_def] THEN 934 `(x, x'') IN (tc r)` by METIS_TAC [tc_rules] THEN 935 FULL_SIMP_TAC (srw_ss()) [acyclic_def, maximal_elements_def] THEN 936 METIS_TAC [], 937 FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN 938 METIS_TAC []]); 939 940val tc_path_min_lem = Q.prove ( 941`!s. FINITE s ==> 942 s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s (tc r)`, 943HO_MATCH_MP_TAC FINITE_INDUCT THEN 944SRW_TAC [] [] THEN 945Cases_on `s={}` THEN1 946SRW_TAC [] [minimal_elements_def] THEN 947RES_TAC THEN 948Cases_on `(e, x) IN (tc r)` THENL 949[Q.EXISTS_TAC `e` THEN 950 SRW_TAC [] [minimal_elements_def] THEN 951 `(x'', x) IN (tc r)` by METIS_TAC [tc_rules] THEN 952 FULL_SIMP_TAC (srw_ss()) [acyclic_def, minimal_elements_def] THEN 953 METIS_TAC [], 954 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 955 METIS_TAC []]); 956 957val finite_acyclic_has_maximal = Q.store_thm ("finite_acyclic_has_maximal", 958`!s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN maximal_elements s r`, 959SRW_TAC [] [] THEN 960IMP_RES_TAC tc_path_max_lem THEN 961FULL_SIMP_TAC (srw_ss()) [maximal_elements_def] THEN 962METIS_TAC [tc_rules]); 963 964val finite_acyclic_has_minimal = Q.store_thm ("finite_acyclic_has_minimal", 965`!s. FINITE s ==> s <> {} ==> !r. acyclic r ==> ?x. x IN minimal_elements s r`, 966SRW_TAC [] [] THEN 967IMP_RES_TAC tc_path_min_lem THEN 968FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 969METIS_TAC [tc_rules]); 970 971local 972 973val lemma1 = Q.prove ( 974`!x y. (x, y) IN tc r ==> ?z. (x, z) IN r /\ (x <> y ==> x <> z)`, 975HO_MATCH_MP_TAC tc_ind THEN 976SRW_TAC [] [] THEN 977METIS_TAC []); 978 979in 980 981val maximal_tc = Q.store_thm ("maximal_TC", 982`!s r. 983 domain r SUBSET s /\ range r SUBSET s 984 ==> 985 (maximal_elements s (tc r) = maximal_elements s r)`, 986SRW_TAC [] [EXTENSION, maximal_elements_def, domain_def, range_def, 987 SUBSET_DEF] THEN 988EQ_TAC THEN 989SRW_TAC [] [] THEN 990METIS_TAC [lemma1, tc_rules]); 991 992end; 993 994local 995 996val lemma1 = Q.prove ( 997`!y x. (y, x) IN tc r ==> ?z. (z, x) IN r /\ (x <> y ==> x <> z)`, 998HO_MATCH_MP_TAC tc_ind THEN 999SRW_TAC [] [] THEN 1000METIS_TAC []); 1001 1002in 1003 1004val minimal_tc = Q.store_thm ("minimal_TC", 1005`!s r. 1006 domain r SUBSET s /\ range r SUBSET s 1007 ==> 1008 (minimal_elements s (tc r) = minimal_elements s r)`, 1009SRW_TAC [] [EXTENSION, minimal_elements_def, domain_def, range_def, 1010 SUBSET_DEF] THEN 1011EQ_TAC THEN 1012SRW_TAC [] [] THEN 1013METIS_TAC [lemma1, tc_rules]); 1014 1015end; 1016 1017val rr_acyclic_WF = Q.INST [`r` |-> `rrestrict r s`] acyclic_WF ; 1018val rme = MATCH_MP WF_has_minimal_path (UNDISCH_ALL rr_acyclic_WF) ; 1019val irme = Q.INST [`s'` |-> `s`] rme ; 1020val urme = REWRITE_RULE [domain_rrestrict_SUBSET, range_rrestrict_SUBSET, 1021 minimal_elements_rrestrict] (DISCH_ALL irme) ; 1022 1023val tcrr = REWRITE_RULE [SUBSET_DEF] (MATCH_MP tc_mono rrestrict_SUBSET) ; 1024 1025val finite_acyclic_has_minimal_path = Q.store_thm 1026("finite_acyclic_has_minimal_path", 1027`!s r x. 1028 FINITE s /\ 1029 acyclic r /\ 1030 x IN s /\ 1031 x NOTIN minimal_elements s r 1032 ==> 1033 ?y. y IN minimal_elements s r /\ (y, x) IN tc r`, 1034 REPEAT STRIP_TAC THEN 1035 IMP_RES_THEN (ASSUME_TAC o Q.SPEC `s`) acyclic_rrestrict THEN 1036 IMP_RES_TAC urme THEN 1037 TRY (BasicProvers.VAR_EQ_TAC THEN RES_TAC) THEN 1038 Q.EXISTS_TAC `y'` THEN 1039 ASM_REWRITE_TAC [] THEN 1040 IMP_RES_TAC tcrr) ; 1041 1042val tc_SWAP' = REWRITE_RULE [rextension, pair_in_IMAGE_SWAP] tc_SWAP ; 1043 1044val finite_acyclic_has_maximal_path = Q.store_thm 1045("finite_acyclic_has_maximal_path", 1046`!s r x. 1047 FINITE s /\ 1048 acyclic r /\ 1049 x IN s /\ 1050 x NOTIN maximal_elements s r 1051 ==> 1052 ?y. y IN maximal_elements s r /\ (x, y) IN tc r`, 1053 ONCE_REWRITE_TAC [GSYM tc_SWAP', GSYM minimal_elements_SWAP, 1054 GSYM acyclic_SWAP] THEN REPEAT STRIP_TAC THEN 1055 irule finite_acyclic_has_minimal_path THEN rpt conj_tac THEN 1056 FIRST_ASSUM ACCEPT_TAC) ; 1057 1058val finite_prefix_po_has_minimal_path = Q.store_thm 1059("finite_prefix_po_has_minimal_path", 1060`!r s x s'. 1061 partial_order r s /\ 1062 finite_prefixes r s /\ 1063 x NOTIN minimal_elements s' r /\ 1064 x IN s' /\ 1065 s' SUBSET s 1066 ==> 1067 ?x'. x' IN minimal_elements s' r /\ (x', x) IN r`, 1068SRW_TAC [] [finite_prefixes_def] THEN 1069IMP_RES_TAC strict_partial_order_acyclic THEN 1070`?x'. x' IN minimal_elements (s' INTER {x' | (x', x) IN r}) 1071 (strict r) /\ 1072 (x', x) IN tc (strict r)` 1073 by (MATCH_MP_TAC finite_acyclic_has_minimal_path THEN 1074 SRW_TAC [] [] THEN 1075 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, strict_def, 1076 SUBSET_DEF, partial_order_def, 1077 reflexive_def] THEN 1078 METIS_TAC [INTER_FINITE, INTER_COMM]) THEN 1079Q.EXISTS_TAC `x'` THEN 1080SRW_TAC [] [] THEN 1081FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 1082SRW_TAC [] [] THEN 1083FULL_SIMP_TAC (srw_ss()) [partial_order_def, domain_def, SUBSET_DEF, 1084 transitive_def, strict_def] THEN 1085METIS_TAC []); 1086 1087val empty_strict_linear_order = Q.store_thm ("empty_strict_linear_order", 1088`!r. strict_linear_order r {} = (r = {})`, 1089SRW_TAC [] [strict_linear_order_def, RES_FORALL_THM, domain_def, range_def, 1090 transitive_def, EXTENSION] THEN 1091EQ_TAC THEN 1092SRW_TAC [] [] THEN 1093Cases_on `x` THEN 1094SRW_TAC [] []); 1095 1096val empty_linear_order = Q.store_thm ("empty_linear_order", 1097`!r. linear_order r {} = (r = {})`, 1098SRW_TAC [] [linear_order_def, RES_FORALL_THM, domain_def, range_def, 1099 transitive_def, antisym_def, EXTENSION] THEN 1100EQ_TAC THEN 1101SRW_TAC [] [] THEN 1102Cases_on `x` THEN 1103SRW_TAC [] []); 1104 1105val linear_order_restrict = Q.store_thm ("linear_order_restrict", 1106`!s r s'. linear_order r s ==> linear_order (rrestrict r s') (s INTER s')`, 1107 Ho_Rewrite.REWRITE_TAC 1108 [linear_order_def, rrestrict_def, domain_def, range_def, 1109 SUBSET_DEF, transitive_def, antisym_def, 1110 IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF, IN_INTER] THEN 1111 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN_LT 1112 LASTGOAL (FIRST_X_ASSUM irule THEN rpt conj_tac >> FIRST_ASSUM ACCEPT_TAC) >> 1113 RES_TAC) ; 1114 1115val strict_linear_order_restrict = Q.store_thm ("strict_linear_order_restrict", 1116`!s r s'. 1117 strict_linear_order r s 1118 ==> 1119 strict_linear_order (rrestrict r s') (s INTER s')`, 1120 Ho_Rewrite.REWRITE_TAC 1121 [strict_linear_order_def, rrestrict_def, domain_def, range_def, 1122 SUBSET_DEF, transitive_def, antisym_def, 1123 IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF, IN_INTER] THEN 1124 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN_LT 1125 LASTGOAL (FIRST_X_ASSUM irule >> rpt conj_tac >> FIRST_ASSUM ACCEPT_TAC) THEN 1126 RES_TAC) ; 1127 1128val linear_order_dom_rg = Q.store_thm ("linear_order_dom_rg", 1129 `linear_order lo X ==> (domain lo UNION range lo = X)`, 1130 REWRITE_TAC [linear_order_def] THEN STRIP_TAC THEN 1131 ASM_REWRITE_TAC [SET_EQ_SUBSET, UNION_SUBSET] THEN 1132 REWRITE_TAC [SUBSET_DEF, IN_UNION, in_domain] THEN 1133 REPEAT STRIP_TAC THEN RES_TAC THEN DISJ1_TAC THEN 1134 Q.EXISTS_TAC `x` THEN POP_ASSUM ACCEPT_TAC ) ; 1135 1136val linear_order_refl = Q.store_thm ("linear_order_refl", 1137 `linear_order lo X ==> x IN X ==> (x, x) IN lo`, 1138 REWRITE_TAC [linear_order_def] THEN REPEAT STRIP_TAC THEN RES_TAC) ; 1139 1140val linear_order_in_set = Q.store_thm ("linear_order_in_set", 1141 `linear_order lo X ==> (x, y) IN lo ==> x IN X /\ y IN X`, 1142 REPEAT DISCH_TAC THEN IMP_RES_TAC linear_order_dom_rg THEN 1143 VAR_EQ_TAC THEN 1144 IMP_RES_TAC in_dom_rg THEN ASM_REWRITE_TAC [IN_UNION]) ; 1145 1146val IN_MIN_LO = Q.store_thm ("IN_MIN_LO", 1147 `x IN X ==> linear_order lo X ==> y IN minimal_elements X lo ==> 1148 (y, x) IN lo`, 1149 Ho_Rewrite.REWRITE_TAC [minimal_elements_def, linear_order_def, 1150 EXTENSION, IN_GSPEC_IFF] THEN 1151 REPEAT STRIP_TAC THEN 1152 FIRST_X_ASSUM (ASSUME_TAC o Q.SPECL [`x`, `y`]) THEN 1153 FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC `x`) THEN 1154 RES_TAC THEN RES_TAC THEN FULL_SIMP_TAC std_ss []) ; 1155 1156val extend_linear_order = Q.store_thm ("extend_linear_order", 1157`!r s x. 1158 x NOTIN s /\ 1159 linear_order r s 1160 ==> 1161 linear_order (r UNION {(y, x) | y | y IN (s UNION {x})}) (s UNION {x})`, 1162 Ho_Rewrite.REWRITE_TAC [linear_order_def, domain_def, range_def, 1163 transitive_def, antisym_def, SUBSET_DEF, 1164 IN_UNION, IN_SING, PAIR_IN_GSPEC_1, PAIR_IN_GSPEC_2, IN_GSPEC_IFF] THEN 1165 REPEAT STRIP_TAC THEN 1166 ASM_REWRITE_TAC [] THEN METIS_TAC []) ; 1167 1168val strict_linear_order_acyclic = Q.store_thm ("strict_linear_order_acyclic", 1169`!r s. strict_linear_order r s ==> acyclic r`, 1170SRW_TAC [] [acyclic_def, strict_linear_order_def] THEN 1171IMP_RES_TAC transitive_tc THEN 1172FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, transitive_def]); 1173 1174val acyclic_union = Q.prove ( 1175 `acyclic (r1 UNION r2) ==> (q, r) IN r2 ==> (r, q) NOTIN r1`, 1176 REWRITE_TAC [acyclic_def] THEN 1177 REPEAT STRIP_TAC THEN 1178 VALIDATE (FIRST_ASSUM (CONTR_TAC o UNDISCH o 1179 MATCH_MP F_IMP o Q.SPEC `q`)) THEN 1180 irule tc_rule2 THEN Q.EXISTS_TAC `r` THEN 1181 CONJ_TAC THEN irule tc_rule1 THEN ASM_REWRITE_TAC [IN_UNION]) ; 1182 1183val strict_linear_order_union_acyclic = Q.store_thm 1184("strict_linear_order_union_acyclic", 1185`!r1 r2 s. 1186 strict_linear_order r1 s /\ 1187 ((domain r2) UNION (range r2)) SUBSET s 1188 ==> 1189 (acyclic (r1 UNION r2) = r2 SUBSET r1)`, 1190SRW_TAC [] [] THEN 1191EQ_TAC THEN 1192SRW_TAC [] [] THENL 1193[ FULL_SIMP_TAC (srw_ss()) [strict_linear_order_def, domain_def, 1194 transitive_def, range_def, SUBSET_DEF] THEN 1195 REPEAT STRIP_TAC THEN 1196 Cases_on `x` THEN 1197 RES_TAC THEN RES_TAC THEN 1198 IMP_RES_TAC acyclic_union THEN 1199 IMP_RES_TAC acyclic_irreflexive THEN 1200 CCONTR_TAC THEN FULL_SIMP_TAC std_ss [IN_UNION], 1201 `r1 UNION r2 = r1` 1202 by (FULL_SIMP_TAC (srw_ss()) [domain_def, range_def, SUBSET_DEF, 1203 EXTENSION] THEN 1204 METIS_TAC []) THEN 1205 SRW_TAC [] [] THEN 1206 METIS_TAC [strict_linear_order_acyclic]]); 1207 1208val strict_linear_order = Q.store_thm ("strict_linear_order", 1209`!r s. linear_order r s ==> strict_linear_order (strict r) s`, 1210 Ho_Rewrite.REWRITE_TAC [linear_order_def, strict_linear_order_def, 1211 strict_def, domain_def, range_def, SUBSET_DEF, transitive_def, 1212 antisym_def, IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF] THEN 1213 REPEAT STRIP_TAC THEN 1214 REPEAT BasicProvers.VAR_EQ_TAC THEN 1215 ASM_REWRITE_TAC [] THEN METIS_TAC []) ; 1216 1217val linear_order = Q.store_thm ("linear_order", 1218`!r s. strict_linear_order r s ==> linear_order (r UNION {(x, x) | x IN s}) s`, 1219 Ho_Rewrite.REWRITE_TAC [linear_order_def, strict_linear_order_def, 1220 domain_def, range_def, SUBSET_DEF, transitive_def, antisym_def, 1221 IN_UNION, IN_GSPEC_IFF, PAIR_IN_GSPEC_IFF, PAIR_IN_GSPEC_same] THEN 1222 REPEAT STRIP_TAC THEN 1223 REPEAT BasicProvers.VAR_EQ_TAC THEN 1224 ASM_REWRITE_TAC [] THEN METIS_TAC []) ; 1225 1226val finite_strict_linear_order_has_maximal = Q.store_thm 1227("finite_strict_linear_order_has_maximal", 1228`!s r. 1229 FINITE s /\ strict_linear_order r s /\ s <> {} 1230 ==> 1231 ?x. x IN maximal_elements s r`, 1232METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_maximal]); 1233 1234val finite_strict_linear_order_has_minimal = Q.store_thm 1235("finite_strict_linear_order_has_minimal", 1236`!s r. 1237 FINITE s /\ strict_linear_order r s /\ s <> {} 1238 ==> 1239 ?x. x IN minimal_elements s r`, 1240METIS_TAC [strict_linear_order_acyclic, finite_acyclic_has_minimal]); 1241 1242val finite_linear_order_has_maximal = Q.store_thm 1243("finite_linear_order_has_maximal", 1244`!s r. 1245 FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN maximal_elements s r`, 1246SRW_TAC [] [] THEN 1247IMP_RES_TAC strict_linear_order THEN 1248IMP_RES_TAC finite_strict_linear_order_has_maximal THEN 1249Q.EXISTS_TAC `x` THEN 1250FULL_SIMP_TAC (srw_ss()) [maximal_elements_def, strict_def] THEN 1251METIS_TAC []); 1252 1253val finite_linear_order_has_minimal = Q.store_thm 1254("finite_linear_order_has_minimal", 1255`!s r. 1256 FINITE s /\ linear_order r s /\ s <> {} ==> ?x. x IN minimal_elements s r`, 1257SRW_TAC [] [] THEN 1258IMP_RES_TAC strict_linear_order THEN 1259IMP_RES_TAC finite_strict_linear_order_has_minimal THEN 1260Q.EXISTS_TAC `x` THEN 1261FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, strict_def] THEN 1262METIS_TAC []); 1263 1264val maximal_linear_order = Q.store_thm ("maximal_linear_order", 1265`!s r x y. 1266 y IN s /\ linear_order r s /\ x IN maximal_elements s r ==> (y, x) IN r`, 1267SRW_TAC [] [linear_order_def, maximal_elements_def] THEN 1268METIS_TAC []); 1269 1270val minimal_linear_order = Q.store_thm ("minimal_linear_order", 1271`!s r x y. 1272 y IN s /\ linear_order r s /\ x IN minimal_elements s r ==> (x, y) IN r`, 1273SRW_TAC [] [linear_order_def, minimal_elements_def] THEN 1274METIS_TAC []); 1275 1276val minimal_linear_order_unique = Q.store_thm ("minimal_linear_order_unique", 1277`!r s s' x y. 1278 linear_order r s /\ 1279 x IN minimal_elements s' r /\ 1280 y IN minimal_elements s' r /\ 1281 s' SUBSET s 1282 ==> 1283 (x = y)`, 1284SRW_TAC [] [minimal_elements_def, linear_order_def, antisym_def, 1285 SUBSET_DEF] THEN 1286METIS_TAC []); 1287 1288val finite_prefix_linear_order_has_unique_minimal = Q.store_thm 1289("finite_prefix_linear_order_has_unique_minimal", 1290`!r s s'. 1291 linear_order r s /\ 1292 finite_prefixes r s /\ 1293 x IN s' /\ 1294 s' SUBSET s 1295 ==> 1296 SING (minimal_elements s' r)`, 1297SRW_TAC [] [SING_DEF] THEN 1298Cases_on `?y. y IN minimal_elements s' r` THEN1 1299METIS_TAC [UNIQUE_MEMBER_SING, minimal_linear_order_unique] THEN 1300METIS_TAC [partial_order_linear_order, finite_prefix_po_has_minimal_path]); 1301 1302val nat_order_iso_thm = Q.store_thm ("nat_order_iso_thm", 1303`!(f: num -> 'a option) (s : 'a set). 1304 (!n m. (f m = f n) /\ f m <> NONE ==> (m = n)) /\ 1305 (!x. x IN s ==> ?m. (f m = SOME x)) /\ 1306 (!m x. (f m = SOME x) ==> x IN s) 1307 ==> 1308 linear_order {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\ 1309 finite_prefixes {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s`, 1310SRW_TAC [] [linear_order_def, domain_def, range_def, SUBSET_DEF, 1311 transitive_def, antisym_def, finite_prefixes_def] THENL 1312[METIS_TAC [], 1313 METIS_TAC [], 1314 METIS_TAC [LESS_EQ_TRANS, SOME_11, NOT_SOME_NONE], 1315 METIS_TAC [LESS_EQUAL_ANTISYM, SOME_11, NOT_SOME_NONE], 1316 METIS_TAC [NOT_LESS_EQUAL, LESS_IMP_LESS_OR_EQ], 1317 `?n. SOME e = f n` by METIS_TAC [] THEN 1318 SRW_TAC [] [] THEN 1319 `{SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} SUBSET 1320 IMAGE f (count (SUC n))` 1321 by (SRW_TAC [] [SUBSET_DEF, count_def, 1322 DECIDE ``!x:num y. x < SUC y = x <= y``] THEN 1323 METIS_TAC [NOT_SOME_NONE]) THEN 1324 `{x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)} = 1325 IMAGE THE {SOME x | ?m n'. m <= n' /\ (f m = SOME x) /\ (f n' = f n)}` 1326 by (SRW_TAC [] [EXTENSION] THEN 1327 METIS_TAC [THE_DEF]) THEN 1328 METIS_TAC [IMAGE_FINITE, SUBSET_FINITE, FINITE_COUNT]]); 1329 1330val chain_def = Define ` 1331 chain s r = 1332 !x y. x IN s /\ y IN s ==> (x,y) IN r \/ (y,x) IN r`; 1333 1334val upper_bounds_def = Define ` 1335 upper_bounds s r = {x | x IN range r /\ !y. y IN s ==> (y,x) IN r}`; 1336 1337val upper_bounds_lem = Q.store_thm ("upper_bounds_lem", 1338`!r s x1 x2. 1339 transitive r /\ x1 IN upper_bounds s r /\ (x1,x2) IN r 1340 ==> 1341 x2 IN upper_bounds s r`, 1342SRW_TAC [] [transitive_def, upper_bounds_def, range_def] THEN 1343METIS_TAC []); 1344 1345(* ----------------- Zorn's lemma ---------------- *) 1346(* Following "A short proof of Zorn's Lemma" by J.D. Weston, Archiv der 1347* Mathematik, 1957 *) 1348 1349(* Chains that are built by transfinite repetition of adding an arbitrary 1350* minimal upper bound *) 1351val fchains_def = Define ` 1352 fchains r = 1353 { k | chain k r /\ k <> {} /\ 1354 !C. chain C r /\ C SUBSET k /\ 1355 (upper_bounds C r DIFF C) INTER k <> {} ==> 1356 (CHOICE (upper_bounds C r DIFF C) IN 1357 minimal_elements ((upper_bounds C r DIFF C) INTER k) r) }`; 1358 1359local 1360 1361val lemma1 = Q.prove ( 1362`!x s r. chain s r /\ x IN s ==> x IN domain r /\ x IN range r`, 1363SRW_TAC [] [chain_def, in_domain, in_range] THEN 1364METIS_TAC []); 1365 1366val lemma2 = Q.prove ( 1367`!r k1 k2 x x'. 1368 transitive r /\ 1369 k1 IN fchains r /\ 1370 k2 IN fchains r /\ 1371 x IN k1 /\ 1372 x' IN k2 /\ 1373 x' NOTIN k1 1374 ==> 1375 (x,x') IN r`, 1376SRW_TAC [] [] THEN 1377`x IN range r /\ x' IN range r` 1378 by (FULL_SIMP_TAC (srw_ss()) [fchains_def] THEN 1379 METIS_TAC [lemma1]) THEN 1380Q.ABBREV_TAC `C = {x | x IN k1 /\ x IN k2 /\ (x,x') IN r}` THEN 1381`x' IN upper_bounds C r DIFF C` 1382 by (Q.UNABBREV_TAC `C` THEN 1383 FULL_SIMP_TAC (srw_ss()) [upper_bounds_def]) THEN 1384`chain C r /\ C SUBSET k2 /\ C SUBSET k1` 1385 by (Q.UNABBREV_TAC `C` THEN 1386 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF, chain_def, fchains_def]) THEN 1387`CHOICE (upper_bounds C r DIFF C) IN 1388 minimal_elements ((upper_bounds C r DIFF C) INTER k2) r` 1389 by (FULL_SIMP_TAC (srw_ss()) [fchains_def] THEN 1390 METIS_TAC [NOT_IN_EMPTY, IN_DIFF, IN_INTER]) THEN 1391`CHOICE (upper_bounds C r DIFF C) IN k2 /\ 1392 (CHOICE (upper_bounds C r DIFF C), x') IN r` 1393 by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, chain_def, 1394 fchains_def] THEN 1395 METIS_TAC []) THEN 1396`(upper_bounds C r DIFF C) INTER k1 = {}` 1397 by (SRW_TAC [] [EXTENSION] THEN 1398 CCONTR_TAC THEN 1399 FULL_SIMP_TAC (srw_ss()) [] THEN 1400 `CHOICE (upper_bounds C r DIFF C) IN k1` 1401 by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, 1402 chain_def, fchains_def] THEN 1403 METIS_TAC [NOT_IN_EMPTY, IN_DIFF, IN_INTER]) THEN 1404 `CHOICE (upper_bounds C r DIFF C) IN C` 1405 by (Q.UNABBREV_TAC `C` THEN 1406 FULL_SIMP_TAC (srw_ss()) []) THEN 1407 METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY, IN_DIFF]) THEN 1408`?x''. x'' IN C /\ (x,x'') IN r` 1409 by (FULL_SIMP_TAC (srw_ss()) [EXTENSION, upper_bounds_def, fchains_def, 1410 SUBSET_DEF, chain_def] THEN 1411 METIS_TAC []) THEN 1412`(x'',x') IN r` 1413 by (Q.UNABBREV_TAC `C` THEN 1414 FULL_SIMP_TAC (srw_ss()) []) THEN 1415METIS_TAC [transitive_def]); 1416 1417val lemma3 = Q.prove ( 1418`!r k1 k2. 1419 transitive r /\ antisym r /\ k1 IN fchains r /\ k2 IN fchains r 1420 ==> 1421 k1 SUBSET k2 \/ k2 SUBSET k1`, 1422SRW_TAC [] [antisym_def, SUBSET_DEF] THEN 1423CCONTR_TAC THEN 1424FULL_SIMP_TAC (srw_ss()) [] THEN 1425`(x,x') IN r` by METIS_TAC [lemma2] THEN 1426METIS_TAC [lemma2]); 1427 1428val lemma4 = Q.prove ( 1429`!r. antisym r /\ transitive r ==> 1430 chain (BIGUNION (fchains r)) r /\ 1431 (!x x' k. 1432 (x',x) IN r /\ 1433 x' IN BIGUNION (fchains r) /\ 1434 x IN BIGUNION (fchains r) /\ 1435 k IN fchains r /\ 1436 x IN k 1437 ==> 1438 x' IN k)`, 1439SRW_TAC [] [chain_def] THENL 1440[Cases_on `y IN s` THENL 1441 [FULL_SIMP_TAC (srw_ss()) [fchains_def, chain_def] THEN 1442 METIS_TAC [], 1443 METIS_TAC [lemma2]], 1444 METIS_TAC [lemma2, antisym_def]]); 1445 1446val lemma5 = Q.prove ( 1447`!r s. range r SUBSET s /\ (range r <> {}) /\ reflexive r s ==> 1448 { CHOICE (range r) } IN fchains r`, 1449SRW_TAC [] [fchains_def] THENL 1450[FULL_SIMP_TAC (srw_ss()) [chain_def, reflexive_def, SUBSET_DEF] THEN 1451 METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY], 1452 FULL_SIMP_TAC (srw_ss()) [GSYM DISJOINT_DEF, IN_DISJOINT] THEN 1453 SRW_TAC [] [minimal_elements_def, upper_bounds_def] THEN 1454 METIS_TAC [CHOICE_DEF, MEMBER_NOT_EMPTY]]); 1455 1456val lemma6 = Q.prove ( 1457`!r k x C. 1458 transitive r /\ 1459 antisym r /\ 1460 k IN fchains r /\ 1461 x IN k /\ 1462 chain C r /\ 1463 x IN upper_bounds C r DIFF C /\ 1464 C SUBSET BIGUNION (fchains r) 1465 ==> 1466 CHOICE (upper_bounds C r DIFF C) IN k /\ (CHOICE (upper_bounds C r DIFF C),x) IN r`, 1467SRW_TAC [] [] THEN 1468`!x'. x' IN C ==> (x',x) IN r /\ (x' <> x)` 1469 by FULL_SIMP_TAC (srw_ss()) [upper_bounds_def] THEN 1470`C SUBSET k` 1471 by (FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 1472 SRW_TAC [] [] THEN 1473 RES_TAC THEN 1474 IMP_RES_TAC lemma4 THEN 1475 METIS_TAC [IN_BIGUNION]) THEN 1476FULL_SIMP_TAC (srw_ss()) [fchains_def, minimal_elements_def, chain_def] THEN 1477`(upper_bounds C r DIFF C) INTER k <> {}` 1478 by (FULL_SIMP_TAC (srw_ss()) [GSYM DISJOINT_DEF, IN_DISJOINT, 1479 IN_DIFF] THEN 1480 METIS_TAC []) THEN 1481METIS_TAC []); 1482 1483val lemma7 = Q.prove ( 1484`!r s. 1485 range r SUBSET s /\ (range r <> {}) /\ antisym r /\ reflexive r s /\ 1486 transitive r 1487 ==> 1488 BIGUNION (fchains r) IN fchains r`, 1489SRW_TAC [] [fchains_def] THEN 1490FULL_SIMP_TAC (srw_ss()) [GSYM fchains_def] THEN1 1491METIS_TAC [lemma4] THEN1 1492METIS_TAC [lemma5, NOT_IN_EMPTY] THENL 1493[`{ CHOICE (range r) } IN fchains r` by METIS_TAC [lemma5] THEN 1494 CCONTR_TAC THEN 1495 FULL_SIMP_TAC (srw_ss()) [], 1496 `?x k. x IN (upper_bounds C r DIFF C) /\ x IN k /\ k IN fchains r` 1497 by METIS_TAC [GSYM DISJOINT_DEF, IN_DISJOINT, IN_BIGUNION] THEN 1498 `CHOICE (upper_bounds C r DIFF C) IN k /\ 1499 (CHOICE (upper_bounds C r DIFF C),x) IN r` 1500 by METIS_TAC [lemma6] THEN 1501 SRW_TAC [] [minimal_elements_def] THEN 1502 FULL_SIMP_TAC (srw_ss()) [] THEN1 1503 METIS_TAC [CHOICE_DEF, IN_DIFF] THEN1 1504 METIS_TAC [CHOICE_DEF, IN_DIFF] THEN1 1505 METIS_TAC [] THEN 1506 `(CHOICE (upper_bounds C r DIFF C),x'') IN r` 1507 by METIS_TAC [lemma6, IN_DIFF] THEN 1508 METIS_TAC [antisym_def]]); 1509 1510val lemma8 = Q.prove ( 1511`!r s k. 1512 range r SUBSET s /\ 1513 (range r <> {}) /\ 1514 reflexive r s /\ antisym r /\ transitive r /\ 1515 k IN fchains r /\ 1516 (upper_bounds k r DIFF k <> {}) 1517 ==> 1518 (CHOICE (upper_bounds k r DIFF k) INSERT k IN fchains r)`, 1519SRW_TAC [] [fchains_def] THEN 1520`CHOICE (upper_bounds k r DIFF k) IN upper_bounds k r DIFF k` 1521 by METIS_TAC [IN_DIFF, IN_DISJOINT, DISJOINT_DEF, CHOICE_DEF] THENL 1522[FULL_SIMP_TAC (srw_ss()) [chain_def, upper_bounds_def] THEN 1523 SRW_TAC [] [] THEN 1524 FULL_SIMP_TAC (srw_ss()) [reflexive_def, SUBSET_DEF], 1525 `CHOICE (upper_bounds C r DIFF C) IN upper_bounds C r DIFF C` 1526 by METIS_TAC [IN_DIFF, IN_DISJOINT, DISJOINT_DEF, CHOICE_DEF] THEN 1527 `C SUBSET k` 1528 by (FULL_SIMP_TAC (srw_ss()) [IN_DISJOINT, GSYM DISJOINT_DEF, 1529 SUBSET_DEF, upper_bounds_def] THEN 1530 SRW_TAC [] [] THEN 1531 METIS_TAC [antisym_def]) THEN 1532 Cases_on `(upper_bounds C r DIFF C) INTER k <> {}` THENL 1533 [SRW_TAC [] [minimal_elements_def] THEN1 1534 METIS_TAC [IN_DIFF] THEN1 1535 METIS_TAC [IN_DIFF] THEN 1536 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 1537 FULL_SIMP_TAC (srw_ss()) [IN_DISJOINT, GSYM DISJOINT_DEF, SUBSET_DEF, 1538 upper_bounds_def] THEN 1539 SRW_TAC [] [] THEN 1540 METIS_TAC [antisym_def], 1541 Q_TAC SUFF_TAC `(upper_bounds C r DIFF C = upper_bounds k r DIFF k)` THENL 1542 [FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, 1543 upper_bounds_def] THEN 1544 SRW_TAC [] [] THEN1 1545 METIS_TAC [] THEN1 1546 METIS_TAC [] THEN 1547 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN 1548 METIS_TAC [], 1549 SRW_TAC [] [EXTENSION] THEN 1550 EQ_TAC THEN 1551 SRW_TAC [] [] THEN 1552 FULL_SIMP_TAC (srw_ss()) [transitive_def, reflexive_def, 1553 chain_def, SUBSET_DEF, 1554 upper_bounds_def, range_def] THEN 1555 METIS_TAC []]]]); 1556 1557val lemma9 = Q.prove ( 1558`!r s. 1559 range r SUBSET s /\ 1560 (range r <> {}) /\ 1561 antisym r /\ reflexive r s /\ transitive r 1562 ==> 1563 upper_bounds (BIGUNION (fchains r)) r SUBSET maximal_elements s r`, 1564SRW_TAC [] [] THEN 1565`BIGUNION (fchains r) IN fchains r` by METIS_TAC [lemma7] THEN 1566Cases_on `upper_bounds (BIGUNION (fchains r)) r DIFF (BIGUNION (fchains r)) <> 1567 {}` 1568THENL [ 1569 `(CHOICE (upper_bounds (BIGUNION (fchains r)) r DIFF 1570 (BIGUNION (fchains r))) INSERT (BIGUNION (fchains r)) 1571 IN fchains r)` 1572 by METIS_TAC [lemma8] THEN 1573 METIS_TAC [MEMBER_NOT_EMPTY, CHOICE_DEF, IN_BIGUNION, IN_DIFF, IN_INSERT], 1574 SIMP_TAC (srw_ss()) [SUBSET_DEF, maximal_elements_def] THEN 1575 Q.X_GEN_TAC `u` THEN STRIP_TAC THEN CONJ_TAC THENL [ 1576 ALL_TAC, 1577 Q.X_GEN_TAC `e` THEN STRIP_TAC 1578 ] THEN 1579 `?k. k IN fchains r /\ u IN k` 1580 by METIS_TAC [IN_DIFF, MEMBER_NOT_EMPTY, IN_BIGUNION] 1581 THENL [ 1582 FULL_SIMP_TAC (srw_ss()) [fchains_def, chain_def, range_def, SUBSET_DEF] THEN 1583 METIS_TAC [], 1584 `e IN upper_bounds (BIGUNION (fchains r)) r` by METIS_TAC [upper_bounds_lem] THEN 1585 `u IN (BIGUNION (fchains r)) /\ e IN (BIGUNION (fchains r))` 1586 by METIS_TAC [IN_BIGUNION, IN_DIFF, MEMBER_NOT_EMPTY] THEN 1587 FULL_SIMP_TAC (srw_ss()) [upper_bounds_def, antisym_def] THEN 1588 METIS_TAC [] 1589 ] 1590]); 1591 1592in 1593 1594val zorns_lemma = Q.store_thm ("zorns_lemma", 1595`!r s. (s <> {}) /\ partial_order r s /\ 1596 (!t. chain t r ==> upper_bounds t r <> {}) 1597 ==> 1598 (?x. x IN maximal_elements s r)`, 1599SRW_TAC [] [partial_order_def] THEN 1600Q.EXISTS_TAC `CHOICE (upper_bounds (BIGUNION (fchains r)) r)` THEN 1601SRW_TAC [] [] THEN 1602`range r <> {}` 1603 by (FULL_SIMP_TAC (srw_ss()) [range_def, reflexive_def, 1604 GSYM MEMBER_NOT_EMPTY] THEN 1605 METIS_TAC []) THEN 1606METIS_TAC [SUBSET_DEF, lemma9, MEMBER_NOT_EMPTY, CHOICE_DEF, lemma4]); 1607 1608end 1609 1610(* ------------------------------------------------------------------------ *) 1611(* Equivalences *) 1612(* ------------------------------------------------------------------------ *) 1613 1614val per_def = Define ` 1615 per xs xss = 1616 (BIGUNION xss) SUBSET xs /\ {} NOTIN xss /\ 1617 !xs1 xs2. xs1 IN xss /\ xs2 IN xss /\ xs1 <> xs2 ==> DISJOINT xs1 xs2`; 1618 1619val per_restrict_def = Define ` 1620 per_restrict xss xs = {xs' INTER xs | xs' IN xss} DELETE {}`; 1621 1622val per_delete = Q.store_thm ("per_delete", 1623`!xs xss e. per xs xss ==> 1624 per (xs DELETE e) 1625 {es | es IN (IMAGE (\es. es DELETE e) xss) /\ es <> {}}`, 1626SRW_TAC [] [per_def, SUBSET_DEF, RES_FORALL_THM] THENL 1627[FULL_SIMP_TAC (srw_ss()) [IN_DELETE] THEN 1628 METIS_TAC [], 1629 FULL_SIMP_TAC (srw_ss()) [IN_DELETE] THEN 1630 METIS_TAC [], 1631 FULL_SIMP_TAC (srw_ss()) [EXTENSION, DISJOINT_DEF] THEN 1632 METIS_TAC []]); 1633 1634val per_restrict_per = Q.store_thm ("per_restrict_per", 1635`!r s s'. per s r ==> per s' (per_restrict r s')`, 1636SRW_TAC [] [per_def, per_restrict_def, RES_FORALL_THM, SUBSET_DEF, 1637 DISJOINT_DEF] THENL 1638[FULL_SIMP_TAC (srw_ss()) [], 1639 FULL_SIMP_TAC (srw_ss()) [EXTENSION, SPECIFICATION] THEN 1640 METIS_TAC []]); 1641 1642val countable_per = Q.store_thm ("countable_per", 1643`!xs xss. countable xs /\ per xs xss ==> countable xss`, 1644SRW_TAC [] [per_def, SUBSET_DEF, DISJOINT_DEF, EXTENSION] THEN 1645MATCH_MP_TAC (METIS_PROVE [inj_countable] 1646 ``countable xs /\ INJ CHOICE xss xs ==> countable xss``) THEN 1647SRW_TAC [] [INJ_DEF, EXTENSION] THEN 1648METIS_TAC [CHOICE_DEF]); 1649 1650 1651 1652(* ------------------------------------------------------------------------ *) 1653(* Misc *) 1654(* ------------------------------------------------------------------------ *) 1655 1656val all_choices_def = Define ` 1657 all_choices xss = 1658 {IMAGE choice xss | choice | !xs. xs IN xss ==> choice xs IN xs}`; 1659 1660val all_choices_thm = Q.store_thm ("all_choices_thm", 1661`!x s y. x IN all_choices s /\ y IN x ==> ?z. z IN s /\ y IN z`, 1662SRW_TAC [] [all_choices_def] THEN 1663FULL_SIMP_TAC (srw_ss()) [] THEN 1664METIS_TAC [SPECIFICATION]); 1665 1666 1667val num_order_def = Define ` 1668 num_order (f:'a -> num) s = {(x, y) | x IN s /\ y IN s /\ f x <= f y}`; 1669 1670val linear_order_num_order = Q.store_thm ("linear_order_num_order", 1671`!f s t. INJ f s t ==> linear_order (num_order f s) s`, 1672SRW_TAC [] [linear_order_def, transitive_def, antisym_def, num_order_def, 1673 domain_def, range_def, SUBSET_DEF, INJ_DEF] THEN1 1674DECIDE_TAC THEN1 1675METIS_TAC [EQ_LESS_EQ] THEN1 1676DECIDE_TAC); 1677 1678val num_order_finite_prefix = Q.store_thm ("num_order_finite_prefix", 1679`!f s t. INJ f s t ==> finite_prefixes (num_order f s) s`, 1680SRW_TAC [] [finite_prefixes_def, num_order_def] THEN 1681`INJ f {e' | e' IN s /\ f e' <= f e} (count (SUC (f e)))` 1682 by (FULL_SIMP_TAC (srw_ss()) [count_def, INJ_DEF] THEN 1683 SRW_TAC [] [] THEN 1684 DECIDE_TAC) THEN 1685METIS_TAC [FINITE_INJ, FINITE_COUNT]); 1686 1687(* ------------------------------------------------------------------------ *) 1688(* A big theorem that a partial order with finite prefixes over a countable*) 1689(* set can be extended to a linear order with finite prefixes. *) 1690(* ------------------------------------------------------------------------ *) 1691 1692val po2lolem1= Q.prove ( 1693`!(f: num -> 'a option) (s : 'a set). 1694 (!n m. (f m = f n) /\ ~(f m = NONE) ==> (m = n)) /\ 1695 (!x. x IN s ==> ?m. (f m = SOME x)) /\ 1696 (!m x. (f m = SOME x) ==> x IN s) 1697 ==> 1698 linear_order {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s /\ 1699 finite_prefixes {(x, y) | ?m n. m <= n /\ (f m = SOME x) /\ (f n = SOME y)} s`, 1700SRW_TAC [] [] THEN 1701IMP_RES_TAC nat_order_iso_thm THEN 1702SRW_TAC [] [finite_prefixes_def]); 1703 1704val get_min_def = Define ` 1705 get_min r' (s, r) = 1706 let mins = minimal_elements (minimal_elements s r) r' in 1707 if SING mins then 1708 SOME (CHOICE mins) 1709 else 1710 NONE`; 1711 1712val nth_min_def = Define ` 1713 (nth_min r' (s, r) 0 = get_min r' (s, r)) /\ 1714 (nth_min r' (s, r) (SUC n) = 1715 let min = get_min r' (s, r) in 1716 if min = NONE then 1717 NONE 1718 else 1719 nth_min r' (s DELETE (THE min), r) n)`; 1720 1721val nth_min_surj_lem1 = Q.prove ( 1722`!r' s' x s r. 1723 linear_order r' s /\ 1724 finite_prefixes r' s /\ 1725 partial_order r s /\ 1726 x IN minimal_elements s' r /\ 1727 s' SUBSET s 1728 ==> 1729 ?m. nth_min r' (s', r) m = SOME x`, 1730NTAC 5 STRIP_TAC THEN 1731Induct_on `CARD {x' | x' IN s' /\ (x', x) IN r'}` THEN 1732SRW_TAC [] [] THEN 1733`FINITE {x' | x' IN s' /\ (x', x) IN r'}` 1734 by (FULL_SIMP_TAC (srw_ss()) [finite_prefixes_def, minimal_elements_def, 1735 SUBSET_DEF, GSPEC_AND] THEN 1736 METIS_TAC [INTER_COMM, INTER_FINITE]) THENL 1737[Q.EXISTS_TAC `0` THEN 1738 SRW_TAC [] [nth_min_def, get_min_def] THEN 1739 `{x' | x' IN s' /\ (x', x) IN r'} = {}` by METIS_TAC [CARD_EQ_0] THEN 1740 FULL_SIMP_TAC (srw_ss()) [] THEN 1741 `mins = {x}` suffices_by SRW_TAC [] [] THEN 1742 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 1743 Q.UNABBREV_TAC `mins` THEN 1744 FULL_SIMP_TAC (srw_ss()) [EXTENSION, linear_order_def, SUBSET_DEF] THEN 1745 METIS_TAC [], 1746 Q.PAT_ASSUM `!s' x r'. P s' x r'` 1747 (STRIP_ASSUME_TAC o 1748 Q.SPECL [`s' DELETE THE (get_min r' (s', r))`, `x`, `r'`]) THEN 1749 `SING (minimal_elements (minimal_elements s' r) r')` 1750 by (MATCH_MP_TAC finite_prefix_linear_order_has_unique_minimal THEN 1751 Q.EXISTS_TAC `s` THEN 1752 SRW_TAC [] [SUBSET_DEF, minimal_elements_def] THEN 1753 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]) THEN 1754 FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM] THEN 1755 FULL_SIMP_TAC (srw_ss()) [SING_DEF] THEN 1756 FULL_SIMP_TAC (srw_ss()) [] THEN 1757 Cases_on `x = x'` THENL 1758 [Q.EXISTS_TAC `0` THEN 1759 SRW_TAC [] [nth_min_def, get_min_def] THEN 1760 UNABBREV_ALL_TAC THEN 1761 SRW_TAC [] [], 1762 `x IN s' /\ x' IN s'` 1763 by (FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, 1764 EXTENSION] THEN 1765 METIS_TAC []) THEN 1766 `v = CARD ({x' | x' IN s' /\ (x',x) IN r'} DELETE x')` 1767 by (SRW_TAC [] [] THEN1 1768 DECIDE_TAC THEN 1769 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, EXTENSION, 1770 linear_order_def, 1771 SUBSET_DEF] THEN 1772 METIS_TAC []) THEN 1773 `{x' | x' IN s' /\ (x',x) IN r'} DELETE x' = 1774 {x'' | (x'' IN s' /\ x'' <> x') /\ (x'',x) IN r'}` 1775 by (FULL_SIMP_TAC (srw_ss()) [EXTENSION, linear_order_def, 1776 domain_def, SUBSET_DEF] THEN 1777 METIS_TAC []) THEN 1778 FULL_SIMP_TAC (srw_ss()) [] THEN 1779 `?m. nth_min r' (s' DELETE x', r) m = SOME x` 1780 by (Q.PAT_ASSUM `P ==> ?m. Q m` MATCH_MP_TAC THEN 1781 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, 1782 rrestrict_def, 1783 SUBSET_DEF]) THEN 1784 Q.EXISTS_TAC `SUC m` THEN 1785 SRW_TAC [] [nth_min_def] THEN 1786 Q.UNABBREV_TAC `min` THEN 1787 SRW_TAC [] [] THEN 1788 Cases_on `get_min r' (s', r)` THEN 1789 FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM, SING_DEF] THEN 1790 METIS_TAC [NOT_SOME_NONE, CHOICE_SING, SOME_11]]]); 1791 1792val nth_min_surj_lem2 = Q.prove ( 1793`!r' s r m m' x x'. 1794 (nth_min r' (s, r) m = SOME x) /\ 1795 (nth_min r' (s DIFF {x | ?n. n <= m /\ (nth_min r' (s,r) n = SOME x)}, r) m' 1796 = 1797 SOME x') 1798 ==> 1799 (nth_min r' (s, r) (SUC (m + m')) = SOME x')`, 1800Induct_on `m` THEN 1801SRW_TAC [] [nth_min_def] THEN 1802UNABBREV_ALL_TAC THEN 1803SRW_TAC [] [DELETE_DEF] THEN 1804FULL_SIMP_TAC (srw_ss()) [LET_THM] THEN 1805Cases_on `get_min r' (s, r)` THEN 1806FULL_SIMP_TAC (srw_ss()) [DELETE_DEF] THEN 1807SRW_TAC [] [arithmeticTheory.ADD] THEN 1808Q.PAT_ASSUM `!r' s r m' x x'. P r' s r m' x x'` MATCH_MP_TAC THEN 1809SRW_TAC [] [] THEN 1810`s DIFF {x''} DIFF 1811 {x | ?n. n <= m /\ (nth_min r' (s DIFF {x''}, r) n = SOME x)} = 1812 s DIFF {x | ?n. n <= SUC m /\ (nth_min r' (s,r) n = SOME x)}` 1813 by (SRW_TAC [] [EXTENSION] THEN 1814 EQ_TAC THEN 1815 SRW_TAC [] [] THENL 1816 [Cases_on `n` THEN 1817 SRW_TAC [] [nth_min_def] THEN 1818 UNABBREV_ALL_TAC THEN 1819 SRW_TAC [] [DELETE_DEF] THEN 1820 POP_ASSUM (MP_TAC o Q.SPEC `n'`) THEN 1821 SRW_TAC [] [] THENL 1822 [DISJ1_TAC THEN 1823 DECIDE_TAC, 1824 METIS_TAC []], 1825 CCONTR_TAC THEN 1826 SRW_TAC [] [] THEN 1827 POP_ASSUM (MP_TAC o Q.SPEC `0`) THEN 1828 SRW_TAC [] [nth_min_def], 1829 POP_ASSUM (MP_TAC o Q.SPEC `SUC n`) THEN 1830 SRW_TAC [] [] THENL 1831 [DISJ1_TAC THEN 1832 DECIDE_TAC, 1833 FULL_SIMP_TAC (srw_ss()) [nth_min_def, LET_THM] THEN 1834 POP_ASSUM MP_TAC THEN 1835 SRW_TAC [] [DELETE_DEF]]]) THEN 1836SRW_TAC [] []); 1837 1838 1839val nth_min_surj_lem3 = Q.prove ( 1840`!r' s r s' x. 1841 linear_order r' s /\ 1842 finite_prefixes r' s /\ 1843 partial_order r s /\ 1844 finite_prefixes r s /\ 1845 s' SUBSET s /\ 1846 x IN s' 1847 ==> 1848 ?m. nth_min r' (s', r) m = SOME x`, 1849NTAC 5 STRIP_TAC THEN 1850completeInduct_on `CARD {x' | x' IN s' /\ (x', x) IN r}` THEN 1851SRW_TAC [] [] THEN 1852Cases_on `x IN minimal_elements s' r` THEN1 1853METIS_TAC [nth_min_surj_lem1] THEN 1854`?x'. x' IN minimal_elements s' r /\ (x', x) IN r` 1855 by METIS_TAC [finite_prefix_po_has_minimal_path] THEN 1856`?m. nth_min r' (s', r) m = SOME x'` by METIS_TAC [nth_min_surj_lem1] THEN 1857Q.ABBREV_TAC `s'' = {x | ?n. n <= m /\ (nth_min r' (s', r) n = SOME x)}` THEN 1858`{x''' | (x''' IN s' /\ x''' NOTIN s'') /\ (x''',x) IN r} PSUBSET 1859 {x' | x' IN s' /\ (x',x) IN r}` 1860 by (SRW_TAC [] [PSUBSET_DEF, SUBSET_DEF, EXTENSION] THEN 1861 Q.EXISTS_TAC `x'` THEN 1862 SRW_TAC [] [] THEN 1863 Q.UNABBREV_TAC `s''` THEN 1864 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def] THEN 1865 METIS_TAC [LESS_EQ_REFL]) THEN 1866`FINITE {x' | x' IN s' /\ (x',x) IN r}` 1867 by (FULL_SIMP_TAC (srw_ss()) [finite_prefixes_def, SUBSET_DEF, 1868 minimal_elements_def, GSPEC_AND] THEN 1869 METIS_TAC [INTER_FINITE, INTER_COMM]) THEN 1870Cases_on `x IN s' DIFF s''` THENL 1871[FULL_SIMP_TAC (srw_ss()) [AND_IMP_INTRO, GSYM RIGHT_FORALL_IMP_THM] THEN 1872 `?m. nth_min r' (s' DIFF s'', r) m = SOME x` 1873 by (Q.PAT_ASSUM `!s''' x'' r''. P s''' x'' r''` MATCH_MP_TAC THEN 1874 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 1875 METIS_TAC [CARD_PSUBSET]) THEN 1876 Q.EXISTS_TAC `SUC (m + m')` THEN 1877 METIS_TAC [nth_min_surj_lem2], 1878 FULL_SIMP_TAC (srw_ss()) [] THEN1 1879 METIS_TAC [] THEN 1880 Q.UNABBREV_TAC `s''` THEN 1881 FULL_SIMP_TAC (srw_ss()) [] THEN 1882 METIS_TAC []]); 1883 1884val get_min_lem1 = Q.prove ( 1885`!r' s r x. (get_min r' (s, r) = SOME x) ==> x IN s`, 1886SRW_TAC [] [get_min_def, LET_THM, SING_DEF] THEN 1887FULL_SIMP_TAC (srw_ss()) [] THEN 1888FULL_SIMP_TAC (srw_ss()) [EXTENSION, minimal_elements_def] THEN 1889METIS_TAC []); 1890 1891val nth_min_lem1 = Q.prove ( 1892`!r' s r m x. (nth_min r' (s, r) m = SOME x) ==> x IN s`, 1893Induct_on `m` THEN 1894SRW_TAC [] [nth_min_def, LET_DEF] THEN1 1895METIS_TAC [get_min_lem1] THEN 1896RES_TAC THEN 1897FULL_SIMP_TAC (srw_ss()) []); 1898 1899val nth_min_lem2 = Q.prove ( 1900`!r' s r n m. 1901 nth_min r' (s, r) m <> NONE 1902 ==> 1903 nth_min r' (s, r) m <> nth_min r' (s, r) (SUC (m + n))`, 1904Induct_on `m` THEN 1905SRW_TAC [] [nth_min_def, LET_THM] THEN 1906Cases_on `get_min r' (s, r)` THEN 1907FULL_SIMP_TAC (srw_ss()) [] THENL 1908[CCONTR_TAC THEN 1909 FULL_SIMP_TAC (srw_ss()) [] THEN 1910 `x IN s DELETE x` by METIS_TAC [nth_min_lem1] THEN 1911 FULL_SIMP_TAC (srw_ss()) [], 1912 `SUC m + n = SUC (m + n)` by DECIDE_TAC THEN 1913 METIS_TAC [NOT_IS_SOME_EQ_NONE]]); 1914 1915val nth_min_inj_lem = Q.prove ( 1916`!r' s r. 1917 (nth_min r' (s, r) m = nth_min r' (s, r) n) /\ nth_min r' (s, r) m <> NONE 1918 ==> 1919 (m = n)`, 1920STRIP_ASSUME_TAC (DECIDE ``m:num < n \/ n < m \/ (m = n)``) THEN 1921SRW_TAC [] [] THENL 1922[`SUC (m + (n - m - 1)) = n` by DECIDE_TAC THEN 1923 METIS_TAC [nth_min_lem2], 1924 Cases_on `nth_min r' (s, r) n = NONE` THEN 1925 FULL_SIMP_TAC (srw_ss()) [] THEN 1926 `SUC (n + (m - n - 1)) = m` by DECIDE_TAC THEN 1927 METIS_TAC [nth_min_lem2]]); 1928 1929val nth_min_subset_lem1 = Q.prove ( 1930`!m n x y s r r'. 1931 m < n /\ x <> y /\ 1932 (nth_min r' (s, r) n = SOME x) /\ (nth_min r' (s, r) m = SOME y) 1933 ==> 1934 (x, y) NOTIN r`, 1935Induct THEN 1936SRW_TAC [] [nth_min_def] THENL 1937[IMP_RES_TAC get_min_lem1 THEN 1938 IMP_RES_TAC nth_min_lem1 THEN 1939 FULL_SIMP_TAC (srw_ss()) [get_min_def, LET_THM] THEN 1940 Cases_on `SING (minimal_elements (minimal_elements s r) r')` THEN 1941 FULL_SIMP_TAC (srw_ss()) [SING_DEF] THEN 1942 FULL_SIMP_TAC (srw_ss()) [] THEN 1943 SRW_TAC [] [] THEN 1944 FULL_SIMP_TAC (srw_ss()) [minimal_elements_def, EXTENSION] THEN 1945 METIS_TAC [], 1946 FULL_SIMP_TAC (srw_ss()) [LET_THM] THEN 1947 Cases_on `get_min r' (s, r)` THEN 1948 FULL_SIMP_TAC (srw_ss()) [] THEN 1949 Cases_on `n` THEN 1950 FULL_SIMP_TAC (srw_ss()) [nth_min_def, LET_THM] THEN 1951 RES_TAC THEN 1952 FULL_SIMP_TAC (srw_ss()) [] THEN 1953 FULL_SIMP_TAC (srw_ss()) [Q.prove (`(x, y) IN {(x, y) | P x y} = P x y`, 1954 SRW_TAC [] [])] THEN 1955 IMP_RES_TAC nth_min_lem1 THEN 1956 FULL_SIMP_TAC (srw_ss()) []]); 1957 1958val nth_min_subset_lem2 = Q.prove ( 1959`!r' r s. 1960 linear_order {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\ 1961 (nth_min r' (s, r) n = SOME y)} s /\ 1962 domain r SUBSET s /\ 1963 range r SUBSET s 1964 ==> 1965 r SUBSET {(x, y) | ?m n. m <= n /\ (nth_min r' (s, r) m = SOME x) /\ 1966 (nth_min r' (s, r) n = SOME y)}`, 1967SRW_TAC [] [SUBSET_DEF] THEN 1968Cases_on `x` THEN 1969SRW_TAC [] [] THEN 1970`?m n. m <= n /\ (((nth_min r' (s, r) m = SOME q) /\ 1971 (nth_min r' (s, r) n = SOME r'')) \/ 1972 ((nth_min r' (s, r) n = SOME q) /\ 1973 (nth_min r' (s, r) m = SOME r'')))` 1974 by (FULL_SIMP_TAC (srw_ss()) [linear_order_def, domain_def, 1975 range_def] THEN 1976 METIS_TAC []) THEN1 1977METIS_TAC [] THEN 1978Cases_on `m = n` THEN1 1979METIS_TAC [] THEN 1980`m < n` by DECIDE_TAC THEN 1981`~(q = r'')` 1982 by (CCONTR_TAC THEN 1983 FULL_SIMP_TAC (srw_ss()) [] THEN 1984 METIS_TAC [nth_min_inj_lem, NOT_SOME_NONE]) THEN 1985METIS_TAC [nth_min_subset_lem1]); 1986 1987val linear_order_of_countable_po = Q.store_thm ("linear_order_of_countable_po", 1988`!r s. 1989 countable s /\ partial_order r s /\ finite_prefixes r s 1990 ==> 1991 ?r'. linear_order r' s /\ finite_prefixes r' s /\ r SUBSET r'`, 1992SRW_TAC [] [countable_def] THEN 1993Q.ABBREV_TAC `f' = nth_min (num_order f s) (s, r)` THEN 1994`!n m. (f' m = f' n) /\ f' m <> NONE ==> (m = n)` 1995 by METIS_TAC [nth_min_inj_lem] THEN 1996`!x. x IN s ==> ?m. f' m = SOME x` 1997 by METIS_TAC [nth_min_surj_lem3, linear_order_num_order, SUBSET_REFL, 1998 num_order_finite_prefix] THEN 1999`!m x. (f' m = SOME x) ==> x IN s` by METIS_TAC [nth_min_lem1] THEN 2000Q.EXISTS_TAC `{(x,y) | ?m n. m <= n /\ (f' m = SOME x) /\ (f' n = SOME y)}` THEN 2001IMP_RES_TAC po2lolem1 THEN 2002SRW_TAC [] [] THEN 2003METIS_TAC [partial_order_def, nth_min_subset_lem2]); 2004 2005val _ = export_theory (); 2006