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