1(* file wotScript.sml; author F.L.Morris; created as Script file. 2/24/10 *) 2(* Proves the well-ordering theorem for an arbitrary HOL type, beginning 3 with the existence of a total order, stealing ideas from the proof of 4 Zorn's Lemma in Halmos's Naive Set Theory, and trying to streamline by 5 using the whole (arbitrary) type 'x in place of an explicit set X. *) 6 7(* ******************************************************************* *) 8(* Revised Oct. 2013 to export just one theorem StrongWellOrderExists: *) 9(* *) 10(* |- ?R:'a reln. StrongLinearOrder R /\ WF R *) 11(* *) 12(* expressed with constants from relationTheory. *) 13(* ******************************************************************* *) 14 15open HolKernel boolLib Parse bossLib; 16val _ = set_trace "Unicode" 0; 17open pred_setLib pred_setTheory relationTheory; 18 19val _ = new_theory "wot"; 20val _ = ParseExtras.temp_loose_equality() 21 22val AR = ASM_REWRITE_TAC []; 23fun ulist x = [x]; 24 25val _ = type_abbrev ("reln", ``:'a->'a->bool``); 26 27(* Generalities that I don't find in pred_setTheory *) 28 29val leibniz_law = prove (``!a b:'a. (a = b) <=> !P. P a <=> P b``, 30REPEAT GEN_TAC THEN EQ_TAC THENL 31[STRIP_TAC THEN AR 32,CONV_TAC LEFT_IMP_FORALL_CONV THEN 33 EXISTS_TAC ``\c:'a. a = c`` THEN CONV_TAC (ONCE_DEPTH_CONV BETA_CONV) THEN 34 REWRITE_TAC []]); 35 36val set_leibniz = prove (``!a b:'a. (a = b) = !Q. a IN Q = b IN Q``, 37REWRITE_TAC [SPECIFICATION] THEN ACCEPT_TAC leibniz_law); 38 39val PSUBSET_EXISTS = prove ( 40``!X Y:'a set. X PSUBSET Y ==> ?a. a IN Y /\ a NOTIN X``, 41REWRITE_TAC [PSUBSET_DEF, EXTENSION, SUBSET_DEF, EQ_EXPAND] THEN 42CONV_TAC (DEPTH_CONV NOT_FORALL_CONV) THEN 43REWRITE_TAC [DE_MORGAN_THM] THEN REPEAT STRIP_TAC THEN 44EXISTS_TAC ``x:'a`` THEN AR THEN RES_TAC); 45 46(* A general set lemma, dual-ish to BIGUNION_SUBSET but only an ==> : *) 47 48val SUBSET_BIGUNION = prove ( 49``!X:'a set P. (?Y. Y IN P /\ X SUBSET Y) ==> X SUBSET BIGUNION P``, 50REPEAT GEN_TAC THEN REWRITE_TAC [SUBSET_DEF, BIGUNION] THEN 51CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 52REPEAT STRIP_TAC THEN EXISTS_TAC ``Y:'a set`` THEN RES_TAC THEN AR); 53 54(* Make relation symbols to be defined here into infixes: *) 55 56val _ = set_fixity "cpl" (Infixr 850); 57val _ = set_fixity "mex_less_eq" (Infix (NONASSOC, 450)); 58val _ = set_fixity "mex_less" (Infix (NONASSOC, 450)); 59 60(* set comparability and inclusion chains: *) 61 62val cpl_def = Define`A:'x set cpl B = A SUBSET B \/ B SUBSET A`; 63 64val cpl_lem = prove ( 65``!A B:'x set. B cpl A ==> A SUBSET B \/ B PSUBSET A``, 66REPEAT STRIP_TAC THEN IMP_RES_TAC cpl_def THEN AR THEN 67Cases_on `B:'x set = A` THEN ASM_REWRITE_TAC [SUBSET_REFL, PSUBSET_DEF]); 68 69val chain_def = Define 70 `chain (C:'x set set) = !a b. a IN C /\ b IN C ==> a cpl b`; 71 72(* define a "successor" on (all) subsets of 'x. *) 73 74val mex_def = Define`mex (s:'x set) = CHOICE (COMPL s)`; 75 76val setsuc_def = Define`setsuc (s:'x set) = mex s INSERT s`; 77 78val setsuc_incr = prove (``!s:'x set. s SUBSET setsuc s``, 79REWRITE_TAC [SUBSET_DEF, setsuc_def, IN_INSERT] THEN 80REPEAT STRIP_TAC THEN AR); 81 82(* define closure under "successor". *) 83 84val succl_def = Define`succl (c:'x set set) = !s. s IN c ==> setsuc s IN c`; 85 86(* and closure under unions of chains *) 87 88val uncl_def = Define 89`uncl (c:'x set set) = !w. w SUBSET c /\ chain w ==> BIGUNION w IN c`; 90 91(* and the combination (uncl entails containing the empty set): *) 92 93val tower_def = Define`tower (A:'x set set) = succl A /\ uncl A`; 94 95(* We prefer to treat tower as a predicate: *) 96 97val IN_tower = prove (``!r:'x set set. r IN tower <=> tower r``, 98REWRITE_TAC [SPECIFICATION]); 99 100(* Now the big move that also starts Zorn's lemma proof in Halmos: *) 101 102val t0_def = zDefine`t0:'x set set = BIGINTER tower`; 103 104(* We will prove, in imitation of Halmos/Zermelo/Zorn, chain (t0) . *) 105 106(* No need here for general orders: SUBSET is it. *) 107 108val tower_t0 = prove (``tower (t0:'x set set)``, 109REWRITE_TAC [tower_def, t0_def, succl_def, uncl_def, IN_BIGINTER] THEN 110REWRITE_TAC [IN_tower] THEN CONJ_TAC THENL 111[REPEAT STRIP_TAC THEN IMP_RES_TAC tower_def THEN 112 RES_TAC THEN IMP_RES_TAC succl_def 113,REWRITE_TAC [BIGINTER, uncl_def, SUBSET_DEF] THEN 114 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 115 REWRITE_TAC [IN_tower, tower_def] THEN REPEAT STRIP_TAC THEN 116 MATCH_MP_TAC (REWRITE_RULE [uncl_def] (ASSUME ``uncl (P:'x set set)``)) THEN 117 ASM_REWRITE_TAC [SUBSET_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC]); 118 119val least_t0 = prove ( 120``!t:'x set set. tower t ==> t0 SUBSET t``, 121REPEAT STRIP_TAC THEN 122REWRITE_TAC [t0_def, BIGINTER, SUBSET_DEF, IN_tower] THEN 123GEN_TAC THEN CONV_TAC (LAND_CONV SET_SPEC_CONV) THEN 124REPEAT STRIP_TAC THEN RES_TAC); 125 126val [t0_succl, t0_uncl] = CONJ_LIST 2 (REWRITE_RULE [tower_def] tower_t0); 127 128(* t0_succl = |- succl t0 t0_uncl = |- uncl t0 *) 129 130(* We set out to prove that t0 is a chain. *) 131 132(* Try Halmos's "comparable" as a predicate, and not nec. only on t0. *) 133 134val comparable_def = zDefine`comparable (p:'x set) = !q. q IN t0 ==> p cpl q`; 135 136val psub_lem = prove (``!A B:'x set. A PSUBSET B ==> ~(B PSUBSET setsuc A)``, 137REPEAT GEN_TAC THEN 138REWRITE_TAC [setsuc_def, PSUBSET_DEF, SUBSET_DEF, IN_INSERT, EXTENSION] THEN 139CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV NOT_FORALL_CONV) THENC 140 RAND_CONV (ONCE_DEPTH_CONV (REWR_CONV EQ_IMP_THM))) THEN 141REWRITE_TAC [EQ_EXPAND, DE_MORGAN_THM] THEN STRIP_TAC THEN 142REWRITE_TAC [GSYM IMP_DISJ_THM] THEN STRIP_TAC THEN GEN_TAC THEN AR THENL 143[RES_TAC THEN UNDISCH_THEN ``x:'x = mex A`` (SUBST1_TAC o SYM) THEN 144 STRIP_TAC THEN AR THEN RES_TAC 145,RES_TAC]); 146 147val gAC_lem = prove (``!C:'x set. comparable C ==> 148 !A. A IN t0 /\ A PSUBSET C ==> setsuc A SUBSET C``, 149REPEAT STRIP_TAC THEN 150IMP_RES_TAC (REWRITE_RULE [succl_def] t0_succl) THEN 151IMP_RES_TAC psub_lem THEN IMP_RES_TAC comparable_def THEN 152IMP_RES_TAC cpl_lem); 153 154(* Above, and all about U to follow now, straight steals from Halmos *) 155 156val U_def = zDefine`U (C:'x set) = { A | A IN t0 /\ 157 (A SUBSET C \/ setsuc C SUBSET A)}`; 158 159val IN_U = prove (``!C:'x set A. A IN U C <=> 160 A IN t0 /\ (A SUBSET C \/ setsuc C SUBSET A)``, 161REPEAT GEN_TAC THEN REWRITE_TAC [U_def] THEN 162CONV_TAC (LAND_CONV SET_SPEC_CONV) THEN REFL_TAC); 163 164val U_lem = prove (``!C A:'x set. A IN U C ==> A cpl setsuc C``, 165REPEAT GEN_TAC THEN REWRITE_TAC [cpl_def, IN_U] THEN STRIP_TAC THEN 166AR THEN DISJ1_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN 167EXISTS_TAC ``C:'x set`` THEN ASM_REWRITE_TAC [setsuc_incr]); 168 169val tower_U = prove ( 170``!C:'x set. C IN t0 /\ comparable C ==> tower (U C)``, 171RW_TAC bool_ss [tower_def] THENL 172[REWRITE_TAC [succl_def, IN_U] THEN 173 GEN_TAC THEN STRIP_TAC THEN (CONJ_TAC THENL 174 [IMP_RES_TAC (REWRITE_RULE [succl_def] t0_succl), ALL_TAC]) THENL 175 [Cases_on `s:'x set PSUBSET C` THENL 176 [DISJ1_TAC THEN IMP_RES_TAC gAC_lem 177 ,DISJ2_TAC THEN 178 IMP_RES_THEN (ASSUME_TAC o 179 CONV_RULE (CONTRAPOS_CONV THENC REWRITE_CONV [NOT_CLAUSES])) 180 PSUBSET_DEF THEN 181 RES_TAC THEN ASM_REWRITE_TAC [SUBSET_REFL] 182 ] 183 ,DISJ2_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC ``s:'x set`` THEN 184 ASM_REWRITE_TAC [setsuc_incr] 185 ] 186,REWRITE_TAC [uncl_def, U_def] THEN 187 GEN_TAC THEN CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV SUBSET_DEF)) THENC 188 ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 189 REPEAT STRIP_TAC THENL 190 [MATCH_MP_TAC (REWRITE_RULE [uncl_def] t0_uncl) THEN AR THEN 191 REWRITE_TAC [SUBSET_DEF] THEN REPEAT STRIP_TAC THEN RES_TAC 192 ,Cases_on `!A:'x set. A IN w ==> A SUBSET C` THENL 193 [DISJ1_TAC THEN REWRITE_TAC [BIGUNION_SUBSET] THEN AR 194 ,DISJ2_TAC THEN MATCH_MP_TAC SUBSET_BIGUNION THEN 195 UNDISCH_TAC ``~!A:'x set. A IN w ==> A SUBSET C`` THEN 196 CONV_TAC (LAND_CONV NOT_FORALL_CONV) THEN REWRITE_TAC [NOT_IMP] THEN 197 STRIP_TAC THEN EXISTS_TAC ``A:'x set`` THEN AR THEN RES_TAC 198]]]); 199 200val U_conclusion = prove ( 201 ``!C:'x set. C IN t0 /\ comparable C ==> (U C = t0)``, 202REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL 203[REWRITE_TAC [IN_U, SUBSET_DEF] THEN REPEAT STRIP_TAC THEN AR 204,IMP_RES_TAC tower_U THEN IMP_RES_TAC least_t0]); 205 206(* Prepare to show (comparable INTER t0) is a tower. *) 207 208val comp_setsuc_comp = prove ( 209 ``!C:'x set. C IN t0 /\ comparable C ==> comparable (setsuc C)``, 210REPEAT STRIP_TAC THEN REWRITE_TAC [comparable_def] THEN GEN_TAC THEN 211IMP_RES_TAC (GSYM U_conclusion) THEN AR THEN 212REWRITE_TAC [U_def] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 213REWRITE_TAC [cpl_def] THEN STRIP_TAC THEN AR THEN 214DISJ2_TAC THEN MATCH_MP_TAC SUBSET_TRANS THEN EXISTS_TAC ``C:'x set`` THEN 215ASM_REWRITE_TAC [setsuc_incr]); 216 217(* "Since the union of a chain of comparable sets is comparable... ." *) 218 219val uchain_comp = prove (``uncl (comparable:'x set set)``, 220REWRITE_TAC [uncl_def, chain_def, SUBSET_DEF] THEN GEN_TAC THEN 221REWRITE_TAC [ISPEC ``comparable:'x set set`` SPECIFICATION] THEN 222REWRITE_TAC [comparable_def, cpl_def] THEN 223REPEAT STRIP_TAC THEN 224Cases_on `!x:'x set. x IN w ==> x SUBSET q` THENL 225[DISJ1_TAC THEN ASM_REWRITE_TAC [BIGUNION_SUBSET] 226,DISJ2_TAC THEN UNDISCH_TAC ``~!x:'x set. x IN w ==> x SUBSET q`` THEN 227 CONV_TAC (LAND_CONV NOT_FORALL_CONV) THEN REWRITE_TAC [NOT_IMP] THEN 228 STRIP_TAC THEN MATCH_MP_TAC SUBSET_BIGUNION THEN 229 EXISTS_TAC ``x:'x set`` THEN AR THEN RES_TAC 230]); 231 232val tower_comp = prove ( 233``tower (t0:'x set set INTER comparable)``, 234REWRITE_TAC [tower_def, IN_INTER, succl_def, uncl_def] THEN 235REWRITE_TAC [ISPEC ``comparable:'x set set`` SPECIFICATION] THEN 236REWRITE_TAC [SUBSET_INTER] THEN REPEAT STRIP_TAC THENL 237[IMP_RES_TAC (REWRITE_RULE [succl_def] t0_succl) 238,IMP_RES_TAC comp_setsuc_comp 239,IMP_RES_TAC (REWRITE_RULE [uncl_def] t0_uncl) 240,IMP_RES_TAC (REWRITE_RULE [uncl_def, SPECIFICATION] uchain_comp)]); 241 242val chain_t0 = prove (``chain (t0:'x set set)``, 243SUBGOAL_THEN ``t0:'x set set SUBSET t0 INTER comparable`` 244 (MP_TAC o REWRITE_RULE [SUBSET_INTER, SUBSET_REFL]) THENL 245[MATCH_MP_TAC least_t0 THEN ACCEPT_TAC tower_comp 246,REWRITE_TAC [SUBSET_DEF, ISPEC ``comparable:'x set set`` SPECIFICATION] THEN 247 REWRITE_TAC [chain_def, comparable_def] THEN 248 REPEAT STRIP_TAC THEN RES_TAC]); 249 250(* Existence of a maximal set in t0 is "UNIV IN t0", but not needed here. *) 251 252(* Now we diverge from Zorn's lemma proof: prove SUBSET wellorders t0. *) 253 254(* Imitation of gAC_lem for t0, now known to be a chain: *) 255 256val psub_setsuc = prove (``!s t:'x set. 257 s IN t0 /\ t IN t0 ==> s PSUBSET t ==> setsuc s SUBSET t``, 258REPEAT STRIP_TAC THEN 259IMP_RES_TAC (REWRITE_RULE [succl_def] t0_succl) THEN 260IMP_RES_TAC psub_lem THEN 261ASSUME_TAC (MATCH_MP (REWRITE_RULE [chain_def] chain_t0) 262 (CONJ (ASSUME ``t:'x set IN t0``) 263 (ASSUME ``setsuc (s:'x set) IN t0``))) THEN 264IMP_RES_TAC cpl_lem); 265 266(* just a lemma: *) 267 268val dilemlem = prove (``!B:'x set set. (?a. !y. y IN B ==> a NOTIN y) ==> 269 setsuc (BIGUNION B) NOTIN B``, 270GEN_TAC THEN STRIP_TAC THEN REWRITE_TAC [setsuc_def, mex_def] THEN 271SUBGOAL_THEN ``CHOICE (COMPL (BIGUNION (B:'x set set))) IN 272 COMPL (BIGUNION (B))`` MP_TAC THENL 273[MATCH_MP_TAC CHOICE_DEF THEN 274 REWRITE_TAC [GSYM MEMBER_NOT_EMPTY, COMPL_DEF] THEN 275 EXISTS_TAC ``a:'x`` THEN REWRITE_TAC [IN_DIFF, IN_UNIV, BIGUNION] THEN 276 CONV_TAC (RAND_CONV SET_SPEC_CONV THENC NOT_EXISTS_CONV) THEN GEN_TAC THEN 277 REWRITE_TAC [DE_MORGAN_THM, GSYM IMP_DISJ_THM] THEN STRIP_TAC THEN RES_TAC 278,REWRITE_TAC [IN_COMPL, IN_BIGUNION] THEN 279 CONV_TAC (LAND_CONV NOT_EXISTS_CONV) THEN 280 REWRITE_TAC [DE_MORGAN_THM, GSYM IMP_DISJ_THM] THEN DISCH_TAC THEN 281 SUBGOAL_THEN ``CHOICE (COMPL (BIGUNION (B:'x set set))) IN 282 CHOICE (COMPL (BIGUNION (B))) INSERT BIGUNION B`` 283 (fn th => ASSUME_TAC th THEN RES_TAC) THEN 284 REWRITE_TAC [IN_INSERT] 285]); 286 287(* Now show that t0 is well-ordered by SUBSET (not a case of WeakWellOrder 288because it does not extend over all of 'x set); there look to be two 289cases: If the union of the subsets of everybody in B is itself in B, 290then it is the minimum of B; but if it is a limit set, it may not be in B, 291in which case its successor is the minimum. "lub_sub" is that union. *) 292 293val lub_sub_def = zDefine`lub_sub (B:'x set set) = 294 BIGUNION {y | y IN t0 /\ !x. x IN B ==> y SUBSET x}`; 295 296val lub_sub_in_t0 = prove ( 297``!B:'x set set. B SUBSET t0 ==> lub_sub B IN t0``, 298REWRITE_TAC [SUBSET_DEF] THEN REPEAT STRIP_TAC THEN 299REWRITE_TAC [lub_sub_def] THEN 300MATCH_MP_TAC (REWRITE_RULE [uncl_def] t0_uncl) THEN 301CONV_TAC (LAND_CONV (REWR_CONV SUBSET_DEF)) THEN 302REWRITE_TAC [chain_def] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 303ASSUME_TAC (REWRITE_RULE [chain_def] chain_t0) THEN 304REPEAT STRIP_TAC THEN AR THEN RES_TAC); 305 306val setsuc_sub = prove ( 307``!B:'x set set. B SUBSET t0 /\ lub_sub B NOTIN B ==> 308 !x. x IN B ==> lub_sub B PSUBSET x /\ setsuc (lub_sub B) SUBSET x``, 309GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN DISCH_TAC THEN 310SUBGOAL_THEN ``lub_sub B PSUBSET (x:'x set)`` ASSUME_TAC THENL 311[REWRITE_TAC [PSUBSET_DEF] THEN CONJ_TAC THENL 312 [REWRITE_TAC [lub_sub_def, SUBSET_DEF, IN_BIGUNION] THEN 313 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 314 REPEAT STRIP_TAC THEN RES_TAC 315 ,ONCE_REWRITE_TAC [set_leibniz] (* loops if not "ONCE_" *) THEN 316 CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC ``B:'x set set`` THEN AR 317 ] 318,AR THEN 319 IMP_RES_TAC (REWRITE_RULE [SUBSET_DEF] (ASSUME ``B:'x set set SUBSET t0``)) 320 THEN IMP_RES_TAC lub_sub_in_t0 THEN 321 MATCH_MP_TAC (MATCH_MP psub_setsuc 322 (CONJ (ASSUME ``lub_sub (B:'x set set) IN t0``) 323 (ASSUME ``x:'x set IN t0``))) THEN AR 324]); 325 326(* The big fish, proof in two cases as advertised above: *) 327 328val wellord_t0 = prove (``!B. B SUBSET t0 /\ B <> {} ==> 329 ?m:'x set. m IN B /\ !b. b IN B ==> m SUBSET b``, 330REWRITE_TAC [GSYM MEMBER_NOT_EMPTY] THEN REPEAT STRIP_TAC THEN 331EXISTS_TAC ``BIGINTER (B:'x set set)`` THEN 332SUBGOAL_THEN ``BIGINTER (B:'x set set) IN B`` 333(fn BIN => REWRITE_TAC [BIN] THEN 334 REWRITE_TAC [BIGINTER, SUBSET_DEF] THEN 335 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN REPEAT STRIP_TAC THEN RES_TAC) THEN 336Cases_on `lub_sub (B:'x set set) IN B` THENL 337[SUBGOAL_THEN ``BIGINTER (B:'x set set) = lub_sub B`` 338 (ASM_REWRITE_TAC o ulist) THEN 339 MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL 340 [REWRITE_TAC [BIGINTER, SUBSET_DEF] THEN 341 GEN_TAC THEN 342 CONV_TAC (LAND_CONV SET_SPEC_CONV THENC LEFT_IMP_FORALL_CONV) THEN 343 EXISTS_TAC ``lub_sub (B:'x set set)`` THEN AR 344 ,REWRITE_TAC [lub_sub_def, BIGINTER, SUBSET_DEF, IN_BIGUNION] THEN 345 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 346 REPEAT STRIP_TAC THEN RES_TAC 347 ] 348,IMP_RES_TAC setsuc_sub THEN 349 SUBGOAL_THEN ``setsuc (lub_sub (B:'x set set)) IN B`` ASSUME_TAC THENL 350 [SUBGOAL_THEN ``setsuc (lub_sub (B:'x set set)) NOTIN B ==> 351 setsuc (lub_sub B) IN {y | y IN t0 /\ !x. x IN B ==> y SUBSET x}`` 352 MP_TAC THENL 353 [CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 354 REPEAT STRIP_TAC THENL 355 [MATCH_MP_TAC (REWRITE_RULE [succl_def] t0_succl) THEN 356 IMP_RES_TAC lub_sub_in_t0 357 ,IMP_RES_TAC setsuc_sub 358 ] 359 ,CONV_TAC CONTRAPOS_CONV THEN 360 DISCH_TAC THEN AR THEN 361 REWRITE_TAC [lub_sub_def] THEN MATCH_MP_TAC dilemlem THEN 362 IMP_RES_TAC PSUBSET_EXISTS THEN EXISTS_TAC ``a:'x`` THEN 363 MP_TAC (ASSUME ``a:'x NOTIN lub_sub B``) THEN 364 REWRITE_TAC [lub_sub_def, IN_BIGUNION] THEN 365 CONV_TAC (LAND_CONV NOT_EXISTS_CONV THENC ONCE_DEPTH_CONV SET_SPEC_CONV) 366 THEN REPEAT STRIP_TAC THEN RES_TAC 367 ] 368 ,SUBGOAL_THEN ``BIGINTER (B:'x set set) = setsuc (lub_sub B)`` 369 (ASM_REWRITE_TAC o ulist) THEN 370 MATCH_MP_TAC SUBSET_ANTISYM THEN CONJ_TAC THENL 371 [REWRITE_TAC [BIGINTER, SUBSET_DEF] THEN 372 GEN_TAC THEN 373 CONV_TAC (LAND_CONV SET_SPEC_CONV THENC LEFT_IMP_FORALL_CONV) THEN 374 EXISTS_TAC ``setsuc (lub_sub (B:'x set set))`` THEN AR 375 ,REWRITE_TAC [SUBSET_BIGINTER] THEN GEN_TAC THEN 376 DISCH_TAC THEN IMP_RES_TAC lub_sub_in_t0 THEN 377 IMP_RES_TAC (REWRITE_RULE [SUBSET_DEF] (ASSUME ``B:'x set set SUBSET t0``)) 378 THEN MATCH_MP_TAC (MATCH_MP psub_setsuc (CONJ 379 (ASSUME ``(lub_sub B):'x set IN t0``) 380 (ASSUME ``Y:'x set IN t0``))) THEN 381 IMP_RES_TAC setsuc_sub 382]]]); 383 384(* ***************************************************************** *) 385 386(* Now to prove that the type 'x itself can be well-ordered: 387 To each a in 'x we make correspond that set in t0 into which setsuc 388 puts a, definable as the union of the a-less sets in t0. *) 389 390val preds_def = zDefine 391 `preds (a:'x) = BIGUNION {s:'x set | s IN t0 /\ a NOTIN s}`; 392 393val preds_in_t0 = prove (``!a:'x. preds a IN t0``, 394GEN_TAC THEN REWRITE_TAC [preds_def] THEN 395MATCH_MP_TAC (REWRITE_RULE [uncl_def] t0_uncl) THEN CONJ_TAC THENL 396 [REWRITE_TAC [SUBSET_DEF] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 397 REPEAT STRIP_TAC 398 ,REWRITE_TAC [chain_def] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 399 REPEAT STRIP_TAC THEN IMP_RES_TAC (REWRITE_RULE [chain_def] chain_t0) 400 ]); 401 402val a_in_suc_preds = prove (``!a:'x. a IN setsuc (preds a)``, 403GEN_TAC THEN 404PURE_ONCE_REWRITE_TAC [GSYM (CONJUNCT1 NOT_CLAUSES)] THEN DISCH_TAC THEN 405SUBGOAL_THEN ``setsuc (preds (a:'x)) SUBSET preds a`` MP_TAC THENL 406[CONV_TAC (RAND_CONV (REWR_CONV preds_def)) THEN 407 MATCH_MP_TAC SUBSET_BIGUNION THEN EXISTS_TAC ``setsuc (preds (a:'x))`` THEN 408 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 409 ASM_REWRITE_TAC [SUBSET_REFL] THEN 410 MATCH_MP_TAC (REWRITE_RULE [succl_def] t0_succl) THEN 411 MATCH_ACCEPT_TAC preds_in_t0 412,REWRITE_TAC [SUBSET_DEF, setsuc_def, IN_INSERT] THEN 413 CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC ``mex (preds (a:'x))`` THEN 414 REWRITE_TAC [mex_def, GSYM IN_COMPL] THEN 415 MATCH_MP_TAC CHOICE_DEF THEN 416 REWRITE_TAC [GSYM MEMBER_NOT_EMPTY, IN_COMPL] THEN EXISTS_TAC ``a:'x`` THEN 417 UNDISCH_TAC ``a:'x NOTIN setsuc (preds a)`` THEN 418 REWRITE_TAC [setsuc_def, IN_INSERT, DE_MORGAN_THM] THEN STRIP_TAC]); 419 420val mex_preds = prove (``!a:'x. mex (preds a) = a``, 421GEN_TAC THEN CONV_TAC (REWR_CONV EQ_SYM_EQ) THEN 422MP_TAC (SPEC_ALL a_in_suc_preds) THEN 423REWRITE_TAC [setsuc_def, IN_INSERT] THEN 424SUBGOAL_THEN ``a:'x NOTIN preds a`` (REWRITE_TAC o ulist) THEN 425REWRITE_TAC [preds_def, IN_BIGUNION] THEN 426CONV_TAC (NOT_EXISTS_CONV THENC ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 427REPEAT STRIP_TAC); 428 429(* Now define what will be the (weak) order on 'x *) 430 431val mex_less_eq_def = Define`a:'x mex_less_eq b = preds a SUBSET preds b`; 432 433val preds_one_one = prove ( 434``!x y:'x. (preds x = preds y) <=> (x = y)``, 435REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL 436[CONV_TAC (BINOP_CONV (REWR_CONV (GSYM mex_preds))) THEN AR, AR]); 437 438(* The following is an easy consequence of chain_t0 *) 439 440val TotOrdTheorem = prove (``WeakLinearOrder ($mex_less_eq:'x reln)``, 441REWRITE_TAC [WeakLinearOrder, trichotomous, WeakOrder, 442 reflexive_def, antisymmetric_def, transitive_def, mex_less_eq_def] THEN 443REWRITE_TAC [SUBSET_TRANS, SUBSET_REFL] THEN CONJ_TAC THENL 444[REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [GSYM preds_one_one] THEN 445 MATCH_ACCEPT_TAC SUBSET_ANTISYM 446,REPEAT GEN_TAC THEN REWRITE_TAC [DISJ_ASSOC] THEN DISJ1_TAC 447 THEN MATCH_MP_TAC (REWRITE_RULE [cpl_def, chain_def] chain_t0) THEN 448 REWRITE_TAC [preds_in_t0] 449]); 450 451(* Likewise for the corresponding strong order on 'x *) 452 453val mex_less_def = Define`$mex_less:'x reln = STRORD $mex_less_eq`; 454 455val TotOrdTheorem_ALT = prove (``StrongLinearOrder ($mex_less:'x reln)``, 456REWRITE_TAC [mex_less_def, StrongLinearOrder, GSYM STRORD_Strong, 457 trichotomous_STRORD] THEN 458CONJ_TAC THENL [MATCH_MP_TAC WeakOrd_Ord, ALL_TAC] THEN 459REWRITE_TAC [REWRITE_RULE [WeakLinearOrder] TotOrdTheorem]); 460 461val WeakWellOrder = xDefine "WeakWellOrder" 462 `WeakWellOrder (R:'a reln) = WeakOrder R /\ !B. B <> {} ==> 463 ?m. m IN B /\ !b. b IN B ==> R m b`; 464 465val weakwell_weaklinear = prove ( 466``!R:'a reln. WeakWellOrder R ==> WeakLinearOrder R``, 467GEN_TAC THEN REWRITE_TAC [WeakWellOrder, WeakLinearOrder_dichotomy] THEN 468CONV_TAC ANTE_CONJ_CONV THEN DISCH_TAC THEN AR THEN 469REWRITE_TAC [trichotomous] THEN 470DISCH_THEN (fn fa => REPEAT GEN_TAC THEN MP_TAC fa) THEN 471CONV_TAC LEFT_IMP_FORALL_CONV THEN EXISTS_TAC ``{a:'a; b}`` THEN 472REWRITE_TAC [NOT_INSERT_EMPTY, IN_INSERT, NOT_IN_EMPTY] THEN 473CONV_TAC (ONCE_DEPTH_CONV (REWR_CONV EQ_SYM_EQ)) THEN 474STRIP_TAC THEN AR THENL [DISJ1_TAC, DISJ2_TAC] THEN 475UNDISCH_THEN ``!b':'a. (a = b') \/ (b = b') ==> R (m:'a) b'`` 476 MATCH_MP_TAC THEN REWRITE_TAC []); 477 478(* The next definition is used only in the annoyingly long proof of the main 479 result, which is really an immediate consequence of wellord_t0: *) 480 481val preds_image_def = Define`preds_image (X:'x set) = {preds x | x IN X}`; 482 483val WellOrd_mex_less_eq = prove (``WeakWellOrder ($mex_less_eq:'x reln)``, 484REWRITE_TAC [WeakWellOrder, GSYM MEMBER_NOT_EMPTY] THEN 485REPEAT STRIP_TAC THENL 486[REWRITE_TAC [REWRITE_RULE [WeakLinearOrder] TotOrdTheorem] 487,SUBGOAL_THEN 488 ``?M. M IN preds_image (B:'x set) /\ !N. N IN preds_image B ==> M SUBSET N`` 489 STRIP_ASSUME_TAC THENL 490 [MATCH_MP_TAC wellord_t0 THEN CONJ_TAC THENL 491 [REWRITE_TAC [preds_image_def, SUBSET_DEF] THEN 492 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 493 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [preds_in_t0] 494 ,REWRITE_TAC [GSYM MEMBER_NOT_EMPTY] THEN EXISTS_TAC ``preds (x:'x)`` THEN 495 REWRITE_TAC [preds_image_def] THEN CONV_TAC SET_SPEC_CONV THEN 496 EXISTS_TAC ``x:'x`` THEN AR 497 ] 498 ,EXISTS_TAC ``mex (M:'x set)`` THEN 499 SUBGOAL_THEN ``?m:'x. (M = preds m) /\ m IN B`` STRIP_ASSUME_TAC THENL 500 [UNDISCH_TAC ``M:'x set IN preds_image B`` THEN 501 REWRITE_TAC [preds_image_def] THEN CONV_TAC (LAND_CONV SET_SPEC_CONV) THEN 502 REWRITE_TAC [] 503 ,ASM_REWRITE_TAC [mex_preds] THEN 504 SUBGOAL_THEN ``!m:'x. m IN B ==> preds m IN preds_image B`` 505 ASSUME_TAC THENL 506 [REPEAT STRIP_TAC THEN REWRITE_TAC [preds_image_def] THEN 507 CONV_TAC SET_SPEC_CONV THEN EXISTS_TAC ``m':'x`` THEN AR 508 ,REPEAT STRIP_TAC THEN REWRITE_TAC [mex_less_eq_def] THEN 509 UNDISCH_THEN ``M:'x set = preds m`` (SUBST1_TAC o SYM) THEN 510 UNDISCH_THEN ``!N:'x set. N IN preds_image B ==> M SUBSET N`` 511 MATCH_MP_TAC THEN RES_TAC 512]]]]); 513 514(* Now the same for the strong order. WF is from relationTheory. *) 515 516val StrongWellOrder = xDefine "StrongWellOrder" 517 `StrongWellOrder (R:'a reln) = StrongLinearOrder R /\ WF R`; 518 519val weakwell_strongwell = prove ( 520``!R:'a reln. WeakWellOrder R ==> StrongWellOrder (STRORD R)``, 521REPEAT STRIP_TAC THEN 522IMP_RES_TAC (REWRITE_RULE [SPECIFICATION, GSYM MEMBER_NOT_EMPTY] 523 WeakWellOrder) THEN 524IMP_RES_TAC weakwell_weaklinear THEN IMP_RES_TAC WeakLinearOrder THEN 525IMP_RES_TAC WeakOrd_Ord THEN IMP_RES_TAC Order THEN 526REWRITE_TAC [StrongWellOrder, StrongLinearOrder] THEN 527ASM_REWRITE_TAC [trichotomous_STRORD, GSYM STRORD_Strong, WF_DEF] THEN 528REPEAT STRIP_TAC THEN RES_TAC THEN 529EXISTS_TAC ``m:'a`` THEN ASM_REWRITE_TAC [STRORD] THEN 530GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC [] THEN 531DISCH_THEN (ANTE_RES_THEN STRIP_ASSUME_TAC) THEN 532STRIP_TAC THEN IMP_RES_TAC antisymmetric_def); 533 534val WellOrd_mex_less = prove (``StrongWellOrder ($mex_less:'x reln)``, 535REWRITE_TAC [mex_less_def] THEN MATCH_MP_TAC weakwell_strongwell THEN 536ACCEPT_TAC WellOrd_mex_less_eq); 537 538val StrongWellOrderExists = store_thm ("StrongWellOrderExists", 539``?R:'a reln. StrongLinearOrder R /\ WF R``, 540Q.EXISTS_TAC `$mex_less` THEN 541REWRITE_TAC [WellOrd_mex_less, GSYM StrongWellOrder]); 542 543val _ = delete_const"t0"; 544 545val _ = export_theory (); 546