Library/wo.ml

   1 (* ========================================================================= *)
   2 (* Proof of some useful AC equivalents like wellordering and Zorn's Lemma.   *)
   3 (*                                                                           *)
   4 (* This is a straight port of the old HOL88 wellorder library. I started to  *)
   5 (* clean up the proofs to exploit first order automation, but didn't have    *)
   6 (* the patience to persist till the end. Anyway, the proofs work!            *)
   7 (* ========================================================================= *)
   8
   9 let PBETA_TAC = CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV);;
  10
  11 let EXPAND_TAC s = FIRST_ASSUM(SUBST1_TAC o SYM o
  12   check((=) s o fst o dest_var o rhs o concl)) THEN BETA_TAC;;
  13
  14 let SUBSET_PRED = prove
  15  (`!P Q. P SUBSET Q <=> !x. P x ==> Q x`,
  16   REWRITE_TAC[SUBSET; IN]);;
  17
  18 let UNIONS_PRED = prove
  19  (`UNIONS P = \x. ?p. P p /\ p x`,
  20   REWRITE_TAC[UNIONS; FUN_EQ_THM; IN_ELIM_THM; IN]);;
  21
  22 (* ======================================================================== *)
  23 (* (1) Definitions and general lemmas.                                      *)
  24 (* ======================================================================== *)
  25
  26 (* ------------------------------------------------------------------------ *)
  27 (* Irreflexive version of an ordering.                                      *)
  28 (* ------------------------------------------------------------------------ *)
  29
  30 let less = new_definition
  31   `(less l)(x,y) <=> (l:A#A->bool)(x,y) /\ ~(x = y)`;;
  32
  33 (* ------------------------------------------------------------------------ *)
  34 (* Field of an uncurried binary relation                                    *)
  35 (* ------------------------------------------------------------------------ *)
  36
  37 let fl = new_definition
  38   `fl(l:A#A->bool) x <=> ?y:A. l(x,y) \/ l(y,x)`;;
  39
  40 (* ------------------------------------------------------------------------ *)
  41 (* Partial order (we infer the domain from the field of the relation)       *)
  42 (* ------------------------------------------------------------------------ *)
  43
  44 let poset = new_definition
  45   `poset (l:A#A->bool) <=>
  46        (!x. fl(l) x ==> l(x,x)) /\
  47        (!x y z. l(x,y) /\ l(y,z) ==> l(x,z)) /\
  48        (!x y. l(x,y) /\ l(y,x) ==> (x = y))`;;
  49
  50 (* ------------------------------------------------------------------------ *)
  51 (* Chain in a poset (Defined as a subset of the field, not the ordering)    *)
  52 (* ------------------------------------------------------------------------ *)
  53
  54 let chain = new_definition
  55   `chain(l:A#A->bool) P <=> (!x y. P x /\ P y ==> l(x,y) \/ l(y,x))`;;
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* Total order.                                                              *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61 let toset = new_definition
  62  `toset (l:A#A->bool) <=>
  63         poset l /\ !x y. x IN fl(l) /\ y IN fl(l) ==> l(x,y) \/ l(y,x)`;;
  64
  65 (* ------------------------------------------------------------------------ *)
  66 (* Wellorder                                                                *)
  67 (* ------------------------------------------------------------------------ *)
  68
  69 let woset = new_definition
  70  `woset (l:A#A->bool) <=>
  71        (!x. fl(l) x ==> l(x,x)) /\
  72        (!x y z. l(x,y) /\ l(y,z) ==> l(x,z)) /\
  73        (!x y. l(x,y) /\ l(y,x) ==> (x = y)) /\
  74        (!x y. fl(l) x /\ fl(l) y ==> l(x,y) \/ l(y,x)) /\
  75        (!P. (!x. P x ==> fl(l) x) /\ (?x. P x) ==>
  76             (?y. P y /\ (!z. P z ==> l(y,z))))`;;
  77
  78 (* ------------------------------------------------------------------------ *)
  79 (* General (reflexive) notion of initial segment.                           *)
  80 (* ------------------------------------------------------------------------ *)
  81
  82 parse_as_infix("inseg",(12,"right"));;
  83
  84 let inseg = new_definition
  85   `(l:A#A->bool) inseg m <=> !x y. l(x,y) <=> m(x,y) /\ fl(l) y`;;
  86
  87 (* ------------------------------------------------------------------------ *)
  88 (* Specific form of initial segment: `all elements in fl(l) less than a`.   *)
  89 (* ------------------------------------------------------------------------ *)
  90
  91 let linseg = new_definition
  92   `linseg (l:A#A->bool) a = \(x,y). l(x,y) /\ (less l)(y,a)`;;
  93
  94 (* ------------------------------------------------------------------------ *)
  95 (* `Ordinals`, i.e. canonical wosets using choice operator.                 *)
  96 (* ------------------------------------------------------------------------ *)
  97
  98 let ordinal = new_definition
  99   `ordinal(l:A#A->bool) <=>
 100     woset(l) /\ (!x. fl(l) x ==> (x = (@) (\y. ~(less l)(y,x))))`;;
 101
 102 (* ------------------------------------------------------------------------ *)
 103 (* Now useful things about the orderings                                    *)
 104 (* ------------------------------------------------------------------------ *)
 105
 106 let [POSET_REFL; POSET_TRANS; POSET_ANTISYM] =
 107   map (GEN `l:A#A->bool` o DISCH_ALL)
 108   (CONJUNCTS(PURE_ONCE_REWRITE_RULE[poset] (ASSUME `poset (l:A#A->bool)`)));;
 109
 110 let POSET_FLEQ = prove
 111  (`!l:A#A->bool. poset l ==> (!x. fl(l) x <=> l(x,x))`,
 112   MESON_TAC[POSET_REFL; fl]);;
 113
 114 let CHAIN_SUBSET = prove
 115  (`!(l:A#A->bool) P Q. chain(l) P /\ Q SUBSET P ==> chain(l) Q`,
 116   REWRITE_TAC[chain; SUBSET_PRED] THEN MESON_TAC[]);;
 117
 118 let [WOSET_REFL; WOSET_TRANS; WOSET_ANTISYM; WOSET_TOTAL; WOSET_WELL] =
 119   map (GEN `l:A#A->bool` o DISCH_ALL)
 120     (CONJUNCTS(PURE_ONCE_REWRITE_RULE[woset] (ASSUME `woset (l:A#A->bool)`)));;
 121
 122 let WOSET_POSET = prove
 123  (`!l:A#A->bool. woset l ==> poset l`,
 124   GEN_TAC THEN REWRITE_TAC[woset; poset] THEN DISCH_TAC THEN
 125   ASM_REWRITE_TAC[]);;
 126
 127 let WOSET_FLEQ = prove
 128  (`!l:A#A->bool. woset l ==> (!x. fl(l) x <=> l(x,x))`,
 129   MESON_TAC[WOSET_POSET; POSET_FLEQ]);;
 130
 131 let WOSET_TRANS_LESS = prove
 132  (`!l:A#A->bool. woset l ==>
 133        !x y z. (less l)(x,y) /\ l(y,z) ==> (less l)(x,z)`,
 134   REWRITE_TAC[woset; less] THEN MESON_TAC[]);;
 135
 136 (* ------------------------------------------------------------------------ *)
 137 (* Antisymmetry and wellfoundedness are sufficient for a wellorder          *)
 138 (* ------------------------------------------------------------------------ *)
 139
 140 let WOSET = prove
 141  (`!l:A#A->bool. woset l <=>
 142         (!x y. l(x,y) /\ l(y,x) ==> (x = y)) /\
 143         (!P. (!x. P x ==> fl(l) x) /\ (?x. P x) ==>
 144              (?y. P y /\ (!z. P z ==> l(y,z))))`,
 145   GEN_TAC THEN REWRITE_TAC[woset] THEN EQ_TAC THEN
 146   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 147   SUBGOAL_THEN `(!x y z. l(x,y) /\ l(y,z) ==> l(x,z)) /\
 148                 (!x:A y. fl(l) x /\ fl(l) y ==> l(x,y) \/ l(y,x))`
 149   MP_TAC THENL [ALL_TAC; MESON_TAC[]] THEN REPEAT STRIP_TAC THENL
 150    [FIRST_ASSUM(MP_TAC o SPEC `\w:A. (w = x) \/ (w = y) \/ (w = z)`) THEN
 151     REWRITE_TAC[fl];
 152     FIRST_ASSUM(MP_TAC o SPEC `\w:A. (w = x) \/ (w = y)`)] THEN
 153   ASM_MESON_TAC[]);;
 154
 155 (* ------------------------------------------------------------------------ *)
 156 (* Misc lemmas.                                                             *)
 157 (* ------------------------------------------------------------------------ *)
 158
 159 let PAIRED_EXT = prove
 160  (`!(l:A#B->C) m. (!x y. l(x,y) = m(x,y)) <=> (l = m)`,
 161   REPEAT GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
 162   REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `p:A#B` THEN
 163   SUBST1_TAC(SYM(SPEC `p:A#B` PAIR)) THEN POP_ASSUM MATCH_ACCEPT_TAC);;
 164
 165 let WOSET_TRANS_LE = prove
 166  (`!l:A#A->bool. woset l ==>
 167        !x y z. l(x,y) /\ (less l)(y,z) ==> (less l)(x,z)`,
 168   REWRITE_TAC[less] THEN MESON_TAC[WOSET_TRANS; WOSET_ANTISYM]);;
 169
 170 let WOSET_WELL_CONTRAPOS = prove
 171  (`!l:A#A->bool. woset l ==>
 172                 (!P. (!x. P x ==> fl(l) x) /\ (?x. P x) ==>
 173                      (?y. P y /\ (!z. (less l)(z,y) ==> ~P z)))`,
 174   GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN
 175   FIRST_ASSUM(MP_TAC o SPEC `P:A->bool` o MATCH_MP WOSET_WELL) THEN
 176   ASM_MESON_TAC[WOSET_TRANS_LE; less]);;
 177
 178 let WOSET_TOTAL_LE = prove
 179  (`!l:A#A->bool. woset l
 180                  ==> !x y. fl(l) x /\ fl(l) y ==> l(x,y) \/ (less l)(y,x)`,
 181   REWRITE_TAC[less] THEN MESON_TAC[WOSET_REFL; WOSET_TOTAL]);;
 182
 183 let WOSET_TOTAL_LT = prove
 184  (`!l:A#A->bool. woset l ==>
 185      !x y. fl(l) x /\ fl(l) y ==> (x = y) \/ (less l)(x,y) \/ (less l)(y,x)`,
 186   REWRITE_TAC[less] THEN MESON_TAC[WOSET_TOTAL]);;
 187
 188 (* ======================================================================== *)
 189 (* (2) AXIOM OF CHOICE ==> CANTOR-ZERMELO WELLORDERING THEOREM              *)
 190 (* ======================================================================== *)
 191
 192 (* ------------------------------------------------------------------------ *)
 193 (* UNIONS of initial segments is an initial segment.                        *)
 194 (* ------------------------------------------------------------------------ *)
 195
 196 let UNION_FL = prove
 197  (`!P (l:A#A->bool). fl(UNIONS P) x <=> ?l. P l /\ fl(l) x`,
 198   REPEAT GEN_TAC THEN REWRITE_TAC[UNIONS_PRED; fl] THEN MESON_TAC[]);;
 199
 200 let UNION_INSEG = prove
 201  (`!P (l:A#A->bool). (!m. P m ==> m inseg l) ==> (UNIONS P) inseg l`,
 202   REWRITE_TAC[inseg; UNION_FL; UNIONS_PRED] THEN ASM_MESON_TAC[]);;
 203
 204 (* ------------------------------------------------------------------------ *)
 205 (* Initial segment of a woset is a woset.                                   *)
 206 (* ------------------------------------------------------------------------ *)
 207
 208 let INSEG_SUBSET = prove
 209  (`!(l:A#A->bool) m. m inseg l ==> !x y. m(x,y) ==> l(x,y)`,
 210   REPEAT GEN_TAC THEN REWRITE_TAC[inseg] THEN MESON_TAC[]);;
 211
 212 let INSEG_SUBSET_FL = prove
 213  (`!(l:A#A->bool) m. m inseg l ==> !x. fl(m) x ==> fl(l) x`,
 214   REWRITE_TAC[fl] THEN MESON_TAC[INSEG_SUBSET]);;
 215
 216 let INSEG_WOSET = prove
 217  (`!(l:A#A->bool) m. m inseg l /\ woset l ==> woset m`,
 218   REWRITE_TAC[inseg] THEN REPEAT STRIP_TAC THEN
 219   REWRITE_TAC[WOSET] THEN CONJ_TAC THENL
 220    [ASM_MESON_TAC[WOSET_ANTISYM];
 221     GEN_TAC THEN FIRST_ASSUM(MP_TAC o SPEC_ALL o MATCH_MP WOSET_WELL) THEN
 222     ASM_MESON_TAC[fl]]);;
 223
 224 (* ------------------------------------------------------------------------ *)
 225 (* Properties of segments of the `linseg` form.                             *)
 226 (* ------------------------------------------------------------------------ *)
 227
 228 let LINSEG_INSEG = prove
 229  (`!(l:A#A->bool) a. woset l ==> (linseg l a) inseg l`,
 230   REPEAT STRIP_TAC THEN REWRITE_TAC[inseg; linseg; fl] THEN PBETA_TAC THEN
 231   ASM_MESON_TAC[WOSET_TRANS_LE]);;
 232
 233 let LINSEG_WOSET = prove
 234  (`!(l:A#A->bool) a. woset l ==> woset(linseg l a)`,
 235   MESON_TAC[INSEG_WOSET; LINSEG_INSEG]);;
 236
 237 let LINSEG_FL = prove
 238  (`!(l:A#A->bool) a x. woset l ==> (fl (linseg l a) x <=> (less l)(x,a))`,
 239   REWRITE_TAC[fl; linseg; less] THEN PBETA_TAC THEN
 240   MESON_TAC[WOSET_REFL; WOSET_TRANS; WOSET_ANTISYM; fl]);;
 241
 242 (* ------------------------------------------------------------------------ *)
 243 (* Key fact: a proper initial segment is of the special form.               *)
 244 (* ------------------------------------------------------------------------ *)
 245
 246 let INSEG_PROPER_SUBSET = prove
 247  (`!(l:A#A->bool) m. m inseg l /\ ~(l = m) ==>
 248                    ?x y. l(x,y) /\ ~m(x,y)`,
 249   REWRITE_TAC[GSYM PAIRED_EXT] THEN MESON_TAC[INSEG_SUBSET]);;
 250
 251 let INSEG_PROPER_SUBSET_FL = prove
 252  (`!(l:A#A->bool) m. m inseg l /\ ~(l = m) ==>
 253                    ?a. fl(l) a /\ ~fl(m) a`,
 254   MESON_TAC[INSEG_PROPER_SUBSET; fl; inseg]);;
 255
 256 let INSEG_LINSEG = prove
 257  (`!(l:A#A->bool) m. woset l ==>
 258       (m inseg l <=> (m = l) \/ (?a. fl(l) a /\ (m = linseg l a)))`,
 259   REPEAT STRIP_TAC THEN ASM_CASES_TAC `m:A#A->bool = l` THEN
 260   ASM_REWRITE_TAC[] THENL
 261    [REWRITE_TAC[inseg; fl] THEN MESON_TAC[]; ALL_TAC] THEN
 262   EQ_TAC THEN STRIP_TAC THENL [ALL_TAC; ASM_MESON_TAC[LINSEG_INSEG]] THEN
 263   FIRST_ASSUM(MP_TAC o MATCH_MP WOSET_WELL_CONTRAPOS) THEN
 264   DISCH_THEN(MP_TAC o SPEC `\x:A. fl(l) x /\ ~fl(m) x`) THEN REWRITE_TAC[] THEN
 265   REWRITE_TAC[linseg; GSYM PAIRED_EXT] THEN PBETA_TAC THEN
 266   W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
 267    [ASM_MESON_TAC[INSEG_PROPER_SUBSET_FL]; ALL_TAC] THEN
 268   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN
 269   EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[] THEN
 270   ASM_MESON_TAC[INSEG_SUBSET; INSEG_SUBSET_FL; fl;
 271     WOSET_TOTAL_LE; less; inseg]);;
 272
 273 (* ------------------------------------------------------------------------ *)
 274 (* A proper initial segment can be extended by its bounding element.        *)
 275 (* ------------------------------------------------------------------------ *)
 276
 277 let EXTEND_FL = prove
 278  (`!(l:A#A->bool) x. woset l ==> (fl (\(x,y). l(x,y) /\ l(y,a)) x <=> l(x,a))`,
 279   REPEAT STRIP_TAC THEN REWRITE_TAC[fl] THEN PBETA_TAC THEN
 280   ASM_MESON_TAC[WOSET_TRANS; WOSET_REFL; fl]);;
 281
 282 let EXTEND_INSEG = prove
 283  (`!(l:A#A->bool) a. woset l /\ fl(l) a ==> (\(x,y). l(x,y) /\ l(y,a)) inseg l`,
 284   REPEAT STRIP_TAC THEN REWRITE_TAC[inseg] THEN PBETA_TAC THEN
 285   REPEAT GEN_TAC THEN IMP_RES_THEN (fun t ->REWRITE_TAC[t]) EXTEND_FL);;
 286
 287 let EXTEND_LINSEG = prove
 288  (`!(l:A#A->bool) a. woset l /\ fl(l) a ==>
 289        (\(x,y). linseg l a (x,y) \/ (y = a) /\ (fl(linseg l a) x \/ (x = a)))
 290                 inseg l`,
 291   REPEAT GEN_TAC THEN DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN
 292     MP_TAC (MATCH_MP EXTEND_INSEG th)) THEN
 293   MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
 294   AP_TERM_TAC THEN ONCE_REWRITE_TAC[GSYM PAIRED_EXT] THEN PBETA_TAC THEN
 295   REPEAT GEN_TAC THEN IMP_RES_THEN (fun th -> REWRITE_TAC[th]) LINSEG_FL THEN
 296   REWRITE_TAC[linseg; less] THEN PBETA_TAC THEN ASM_MESON_TAC[WOSET_REFL]);;
 297
 298 (* ------------------------------------------------------------------------ *)
 299 (* Key canonicality property of ordinals.                                   *)
 300 (* ------------------------------------------------------------------------ *)
 301
 302 let ORDINAL_CHAINED_LEMMA = prove
 303  (`!(k:A#A->bool) l m. ordinal(l) /\ ordinal(m)
 304                        ==> k inseg l /\ k inseg m
 305                            ==> (k = l) \/ (k = m) \/ ?a. fl(l) a /\ fl(m) a /\
 306                                                          (k = linseg l a) /\
 307                                                          (k = linseg m a)`,
 308   REPEAT GEN_TAC THEN REWRITE_TAC[ordinal] THEN STRIP_TAC THEN
 309   EVERY_ASSUM(fun th -> TRY
 310     (fun g -> REWRITE_TAC[MATCH_MP INSEG_LINSEG th] g)) THEN
 311   ASM_CASES_TAC `k:A#A->bool = l` THEN ASM_REWRITE_TAC[] THEN
 312   ASM_CASES_TAC `k:A#A->bool = m` THEN ASM_REWRITE_TAC[] THEN
 313   DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC)
 314                              (X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC)) THEN
 315   EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[] THEN
 316   SUBGOAL_THEN `a:A = b` (fun th -> ASM_MESON_TAC[th]) THEN
 317   FIRST_ASSUM(fun th -> SUBST1_TAC(MATCH_MP th (ASSUME `fl(l) (a:A)`))) THEN
 318   FIRST_ASSUM(fun th -> SUBST1_TAC(MATCH_MP th (ASSUME `fl(m) (b:A)`))) THEN
 319   AP_TERM_TAC THEN ABS_TAC THEN AP_TERM_TAC THEN
 320   UNDISCH_TAC `k = linseg m (b:A)` THEN ASM_REWRITE_TAC[] THEN
 321   REWRITE_TAC[linseg; GSYM PAIRED_EXT] THEN PBETA_TAC THEN
 322   ASM_MESON_TAC[WOSET_REFL; less; fl]);;
 323
 324 let ORDINAL_CHAINED = prove
 325  (`!(l:A#A->bool) m. ordinal(l) /\ ordinal(m) ==> m inseg l \/ l inseg m`,
 326   REPEAT GEN_TAC THEN
 327   DISCH_THEN(fun th -> STRIP_ASSUME_TAC(REWRITE_RULE[ordinal] th) THEN
 328                        ASSUME_TAC (MATCH_MP ORDINAL_CHAINED_LEMMA th)) THEN
 329   MP_TAC(SPEC `\k:A#A->bool. k inseg l /\ k inseg m` UNION_INSEG) THEN
 330   DISCH_THEN(fun th ->
 331     MP_TAC(CONJ (SPEC `l:A#A->bool` th) (SPEC `m:A#A->bool` th))) THEN
 332   REWRITE_TAC[TAUT `(a /\ b ==> a) /\ (a /\ b ==> b)`] THEN
 333   DISCH_THEN(fun th -> STRIP_ASSUME_TAC th THEN
 334                        FIRST_ASSUM(REPEAT_TCL DISJ_CASES_THEN MP_TAC o
 335                        C MATCH_MP th)) THENL
 336    [ASM_MESON_TAC[]; ASM_MESON_TAC[]; ALL_TAC] THEN
 337   DISCH_THEN(X_CHOOSE_THEN `a:A` STRIP_ASSUME_TAC) THEN
 338   MP_TAC(ASSUME `UNIONS (\k. k inseg l /\ k inseg m) = linseg l (a:A)`) THEN
 339   CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
 340   REWRITE_TAC[FUN_EQ_THM] THEN DISCH_THEN(MP_TAC o SPEC `(a:A,a)`) THEN
 341   REWRITE_TAC[linseg] THEN PBETA_TAC THEN REWRITE_TAC[less] THEN
 342   REWRITE_TAC[UNIONS_PRED] THEN EXISTS_TAC
 343   `\(x,y). linseg l a (x,y) \/ (y = a) /\ (fl(linseg l a) x \/ (x = a:A))` THEN
 344   PBETA_TAC THEN REWRITE_TAC[] THEN CONJ_TAC THENL
 345    [ALL_TAC;
 346     UNDISCH_TAC `UNIONS (\k. k inseg l /\ k inseg m) = linseg l (a:A)` THEN
 347     DISCH_THEN(SUBST1_TAC o SYM) THEN ASM_REWRITE_TAC[]] THEN
 348   MATCH_MP_TAC EXTEND_LINSEG THEN ASM_REWRITE_TAC[]);;
 349
 350 (* ------------------------------------------------------------------------ *)
 351 (* Proof that any none-universe ordinal can be extended to its "successor". *)
 352 (* ------------------------------------------------------------------------ *)
 353
 354 let FL_SUC = prove
 355  (`!(l:A#A->bool) a.
 356      fl(\(x,y). l(x,y) \/ (y = a) /\ (fl(l) x \/ (x = a))) x <=>
 357      fl(l) x \/ (x = a)`,
 358   REPEAT GEN_TAC THEN REWRITE_TAC[fl] THEN PBETA_TAC THEN EQ_TAC THEN
 359   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN TRY DISJ1_TAC THEN
 360   ASM_MESON_TAC[]);;
 361
 362 let ORDINAL_SUC = prove
 363  (`!l:A#A->bool. ordinal(l) /\ (?x. ~(fl(l) x)) ==>
 364                  ordinal(\(x,y). l(x,y) \/ (y = @y. ~fl(l) y) /\
 365                                            (fl(l) x \/ (x = @y. ~fl(l) y)))`,
 366   REPEAT GEN_TAC THEN REWRITE_TAC[ordinal] THEN
 367   DISCH_THEN(REPEAT_TCL CONJUNCTS_THEN ASSUME_TAC) THEN
 368   ABBREV_TAC `a:A = @y. ~fl(l) y` THEN
 369   SUBGOAL_THEN `~fl(l:A#A->bool) a` ASSUME_TAC THENL
 370    [EXPAND_TAC "a" THEN CONV_TAC SELECT_CONV THEN
 371     ASM_REWRITE_TAC[]; ALL_TAC] THEN
 372   PBETA_TAC THEN CONJ_TAC THENL
 373    [REWRITE_TAC[WOSET] THEN PBETA_TAC THEN CONJ_TAC THENL
 374      [REPEAT GEN_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 375        [ASM_MESON_TAC[WOSET_ANTISYM]; ALL_TAC; ALL_TAC] THEN
 376       UNDISCH_TAC `~fl(l:A#A->bool) a` THEN CONV_TAC CONTRAPOS_CONV THEN
 377       DISCH_TAC THEN FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
 378       DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[fl] THENL
 379        [EXISTS_TAC `y:A`; EXISTS_TAC `x:A`] THEN
 380       ASM_REWRITE_TAC[];
 381       X_GEN_TAC `P:A->bool` THEN REWRITE_TAC[FL_SUC] THEN
 382       DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `w:A`)) THEN
 383       IMP_RES_THEN (MP_TAC o SPEC `\x:A. P x /\ fl(l) x`) WOSET_WELL THEN
 384       BETA_TAC THEN REWRITE_TAC[TAUT `a /\ b ==> b`] THEN
 385       ASM_CASES_TAC `?x:A. P x /\ fl(l) x` THEN ASM_REWRITE_TAC[] THENL
 386        [ASM_MESON_TAC[];
 387         FIRST_ASSUM(MP_TAC o SPEC `w:A` o
 388           GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
 389         ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 390         ASM_MESON_TAC[]]];
 391     X_GEN_TAC `z:A` THEN REWRITE_TAC[FL_SUC; less] THEN
 392     PBETA_TAC THEN DISCH_THEN DISJ_CASES_TAC THENL
 393      [UNDISCH_TAC `!x:A. fl l x ==> (x = (@y. ~less l (y,x)))` THEN
 394       DISCH_THEN(IMP_RES_THEN MP_TAC) THEN
 395       DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN
 396       AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 397       X_GEN_TAC `y:A` THEN
 398       BETA_TAC THEN REWRITE_TAC[less] THEN AP_TERM_TAC THEN
 399       ASM_CASES_TAC `y:A = z` THEN ASM_REWRITE_TAC[] THEN
 400       EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 401       UNDISCH_TAC `fl(l:A#A->bool) z` THEN ASM_REWRITE_TAC[];
 402       UNDISCH_TAC `z:A = a` THEN DISCH_THEN SUBST_ALL_TAC THEN
 403       GEN_REWRITE_TAC LAND_CONV [SYM(ASSUME `(@y:A. ~fl(l) y) = a`)] THEN
 404       AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 405       X_GEN_TAC `y:A` THEN
 406       BETA_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[] THEN
 407       ASM_CASES_TAC `y:A = a` THEN ASM_REWRITE_TAC[] THEN
 408       EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 409       REWRITE_TAC[fl] THEN EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]]]);;
 410
 411 (* ------------------------------------------------------------------------ *)
 412 (* The union of a set of ordinals is an ordinal.                            *)
 413 (* ------------------------------------------------------------------------ *)
 414
 415 let ORDINAL_UNION = prove
 416  (`!P. (!l:A#A->bool. P l ==> ordinal(l)) ==> ordinal(UNIONS P)`,
 417   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ordinal; WOSET] THEN
 418   REPEAT CONJ_TAC THENL
 419    [MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN REWRITE_TAC[UNIONS_PRED] THEN
 420     BETA_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
 421      (X_CHOOSE_THEN `l:A#A->bool` (CONJUNCTS_THEN2 (ANTE_RES_THEN ASSUME_TAC)
 422         ASSUME_TAC))
 423      (X_CHOOSE_THEN `m:A#A->bool` (CONJUNCTS_THEN2 (ANTE_RES_THEN ASSUME_TAC)
 424         ASSUME_TAC))) THEN
 425     MP_TAC(SPECL [`l:A#A->bool`; `m:A#A->bool`] ORDINAL_CHAINED) THEN
 426     ASM_REWRITE_TAC[] THEN DISCH_THEN DISJ_CASES_TAC THENL
 427      [MP_TAC(SPEC `l:A#A->bool` WOSET_ANTISYM);
 428       MP_TAC(SPEC `m:A#A->bool` WOSET_ANTISYM)] THEN
 429     RULE_ASSUM_TAC(REWRITE_RULE[ordinal]) THEN
 430     ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
 431     ASM_REWRITE_TAC[] THEN IMP_RES_THEN MATCH_MP_TAC INSEG_SUBSET THEN
 432     ASM_REWRITE_TAC[];
 433     X_GEN_TAC `Q:A->bool` THEN REWRITE_TAC[UNION_FL] THEN
 434     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC `a:A`)) THEN
 435     MP_TAC(ASSUME `!x:A. Q x ==> (?l. P l /\ fl l x)`) THEN
 436     DISCH_THEN(IMP_RES_THEN
 437       (X_CHOOSE_THEN `l:A#A->bool` STRIP_ASSUME_TAC)) THEN
 438     IMP_RES_THEN ASSUME_TAC (ASSUME `!l:A#A->bool. P l ==> ordinal l`) THEN
 439     ASSUME_TAC(CONJUNCT1
 440       (REWRITE_RULE[ordinal] (ASSUME `ordinal(l:A#A->bool)`))) THEN
 441     IMP_RES_THEN(MP_TAC o SPEC `\x:A. fl(l) x /\ Q x`) WOSET_WELL THEN
 442     BETA_TAC THEN REWRITE_TAC[TAUT `a /\ b ==> a`] THEN
 443     SUBGOAL_THEN `?x:A. fl(l) x /\ Q x` (fun th -> REWRITE_TAC[th]) THENL
 444      [EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 445     DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC) THEN
 446     EXISTS_TAC `b:A` THEN ASM_REWRITE_TAC[] THEN
 447     X_GEN_TAC `x:A` THEN DISCH_TAC THEN
 448     ANTE_RES_THEN MP_TAC (ASSUME `(Q:A->bool) x`) THEN
 449     DISCH_THEN(X_CHOOSE_THEN `m:A#A->bool` STRIP_ASSUME_TAC) THEN
 450     ANTE_RES_THEN ASSUME_TAC (ASSUME `(P:(A#A->bool)->bool) m`) THEN
 451     MP_TAC(SPECL [`l:A#A->bool`; `m:A#A->bool`] ORDINAL_CHAINED) THEN
 452     ASM_REWRITE_TAC[UNIONS_PRED] THEN BETA_TAC THEN
 453     DISCH_THEN DISJ_CASES_TAC THENL
 454      [EXISTS_TAC `l:A#A->bool` THEN ASM_REWRITE_TAC[] THEN
 455       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 456       IMP_RES_THEN MATCH_MP_TAC INSEG_SUBSET_FL THEN ASM_REWRITE_TAC[];
 457       EXISTS_TAC `m:A#A->bool` THEN ASM_REWRITE_TAC[] THEN
 458       FIRST_ASSUM(MP_TAC o SPECL [`x:A`; `b:A`] o REWRITE_RULE[inseg]) THEN
 459       ASM_REWRITE_TAC[] THEN DISCH_THEN(ASSUME_TAC o SYM) THEN
 460       IMP_RES_THEN (MP_TAC o SPEC `b:A`) INSEG_SUBSET_FL THEN
 461       ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 462       MP_TAC(CONJUNCT1(REWRITE_RULE[ordinal]
 463         (ASSUME `ordinal(m:A#A->bool)`))) THEN
 464       DISCH_THEN(MP_TAC o SPECL [`b:A`; `x:A`] o MATCH_MP WOSET_TOTAL) THEN
 465       ASM_REWRITE_TAC[] THEN DISCH_THEN (DISJ_CASES_THEN MP_TAC) THEN
 466       ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 467       IMP_RES_THEN MATCH_MP_TAC INSEG_SUBSET THEN
 468       FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[fl] THEN
 469       EXISTS_TAC `b:A` THEN ASM_REWRITE_TAC[]];
 470     X_GEN_TAC `x:A` THEN REWRITE_TAC[UNION_FL] THEN
 471     DISCH_THEN(X_CHOOSE_THEN `l:A#A->bool` STRIP_ASSUME_TAC) THEN
 472     MP_TAC(ASSUME `!l:A#A->bool. P l ==> ordinal l`) THEN
 473     DISCH_THEN(IMP_RES_THEN MP_TAC) THEN REWRITE_TAC[ordinal] THEN
 474     DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (MP_TAC o SPEC `x:A`)) THEN
 475     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN
 476     REPEAT AP_TERM_TAC THEN GEN_REWRITE_TAC I [FUN_EQ_THM] THEN
 477     X_GEN_TAC `y:A` THEN BETA_TAC THEN AP_TERM_TAC THEN
 478     ASM_CASES_TAC `y:A = x` THEN ASM_REWRITE_TAC[less; UNIONS_PRED] THEN
 479     BETA_TAC THEN EQ_TAC THEN DISCH_TAC THENL
 480      [EXISTS_TAC `l:A#A->bool` THEN ASM_REWRITE_TAC[];
 481       FIRST_ASSUM(X_CHOOSE_THEN `m:A#A->bool` STRIP_ASSUME_TAC) THEN
 482       SUBGOAL_THEN `ordinal(l:A#A->bool) /\ ordinal(m:A#A->bool)` MP_TAC THENL
 483        [CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 484         DISCH_THEN(DISJ_CASES_TAC o MATCH_MP ORDINAL_CHAINED)] THENL
 485        [IMP_RES_THEN MATCH_MP_TAC INSEG_SUBSET THEN ASM_REWRITE_TAC[];
 486         RULE_ASSUM_TAC(REWRITE_RULE[inseg]) THEN ASM_REWRITE_TAC[]]]]);;
 487
 488 (* ------------------------------------------------------------------------ *)
 489 (* Consequently, every type can be wellordered (and by an ordinal).         *)
 490 (* ------------------------------------------------------------------------ *)
 491
 492 let ORDINAL_UNION_LEMMA = prove
 493  (`!(l:A#A->bool) x. ordinal l ==> fl(l) x ==> fl(UNIONS(ordinal)) x`,
 494   REPEAT STRIP_TAC THEN REWRITE_TAC[UNION_FL] THEN
 495   EXISTS_TAC `l:A#A->bool` THEN ASM_REWRITE_TAC[]);;
 496
 497 let ORDINAL_UP = prove
 498  (`!l:A#A->bool. ordinal(l) ==> (!x. fl(l) x) \/
 499                           (?m x. ordinal(m) /\ fl(m) x /\ ~fl(l) x)`,
 500   GEN_TAC THEN DISCH_TAC THEN
 501   REWRITE_TAC[TAUT `a \/ b <=> ~a ==> b`] THEN
 502   GEN_REWRITE_TAC LAND_CONV [NOT_FORALL_THM] THEN DISCH_TAC THEN
 503   MP_TAC(SPEC `l:A#A->bool` ORDINAL_SUC) THEN ASM_REWRITE_TAC[] THEN
 504   DISCH_TAC THEN MAP_EVERY EXISTS_TAC
 505    [`\(x,y). l(x,y) \/ (y = @y:A. ~fl l y) /\ (fl(l) x \/ (x = @y. ~fl l y))`;
 506     `@y. ~fl(l:A#A->bool) y`] THEN
 507   ASM_REWRITE_TAC[FL_SUC] THEN
 508   CONV_TAC SELECT_CONV THEN ASM_REWRITE_TAC[]);;
 509
 510 let LEMMA = prove
 511  (`?l:A#A->bool. ordinal(l) /\ !x. fl(l) x`,
 512   EXISTS_TAC `UNIONS (ordinal:(A#A->bool)->bool)` THEN
 513   MATCH_MP_TAC(TAUT `a /\ (a ==> b) ==> a /\ b`) THEN CONJ_TAC THENL
 514    [MATCH_MP_TAC ORDINAL_UNION THEN REWRITE_TAC[];
 515     DISCH_THEN(DISJ_CASES_TAC o MATCH_MP ORDINAL_UP) THEN
 516     ASM_REWRITE_TAC[] THEN POP_ASSUM(X_CHOOSE_THEN `m:A#A->bool`
 517      (X_CHOOSE_THEN `x:A` STRIP_ASSUME_TAC)) THEN
 518     IMP_RES_THEN (IMP_RES_THEN MP_TAC) ORDINAL_UNION_LEMMA THEN
 519     ASM_REWRITE_TAC[]]);;
 520
 521 (* ------------------------------------------------------------------------ *)
 522 (* At least -- every set can be wellordered.                                *)
 523 (* ------------------------------------------------------------------------ *)
 524
 525 let FL_RESTRICT = prove
 526  (`!l. woset l ==>
 527        !P. fl(\(x:A,y). P x /\ P y /\ l(x,y)) x <=> P x /\ fl(l) x`,
 528   REPEAT STRIP_TAC THEN REWRITE_TAC[fl] THEN PBETA_TAC THEN EQ_TAC THEN
 529   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 530   TRY(EXISTS_TAC `y:A` THEN ASM_REWRITE_TAC[] THEN NO_TAC) THEN
 531   EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC[] THEN
 532   IMP_RES_THEN MATCH_MP_TAC WOSET_REFL THEN
 533   REWRITE_TAC[fl] THEN EXISTS_TAC `y:A` THEN ASM_REWRITE_TAC[]);;
 534
 535 let WO = prove
 536  (`!P. ?l:A#A->bool. woset l /\ (fl(l) = P)`,
 537   GEN_TAC THEN X_CHOOSE_THEN `l:A#A->bool` STRIP_ASSUME_TAC
 538    (REWRITE_RULE[ordinal] LEMMA) THEN
 539   EXISTS_TAC `\(x:A,y). P x /\ P y /\ l(x,y)` THEN REWRITE_TAC[WOSET] THEN
 540   PBETA_TAC THEN
 541   GEN_REWRITE_TAC RAND_CONV [FUN_EQ_THM] THEN
 542   FIRST_ASSUM(fun th -> REWRITE_TAC[MATCH_MP FL_RESTRICT th]) THEN
 543   PBETA_TAC THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
 544    [REPEAT GEN_TAC THEN DISCH_TAC THEN
 545     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP WOSET_ANTISYM) THEN
 546     ASM_REWRITE_TAC[];
 547     X_GEN_TAC `Q:A->bool` THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
 548     FIRST_ASSUM(MP_TAC o MATCH_MP WOSET_WELL) THEN
 549     DISCH_THEN(MP_TAC o SPEC `Q:A->bool`) THEN ASM_REWRITE_TAC[] THEN
 550     DISCH_THEN(X_CHOOSE_THEN `y:A` STRIP_ASSUME_TAC) THEN
 551     EXISTS_TAC `y:A` THEN ASM_REWRITE_TAC[] THEN GEN_TAC THEN DISCH_TAC THEN
 552     REPEAT CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
 553     FIRST_ASSUM ACCEPT_TAC]);;
 554
 555 (* ======================================================================== *)
 556 (* (3) CANTOR-ZERMELO WELL-ORDERING THEOREM ==> HAUSDORFF MAXIMAL PRINCIPLE *)
 557 (* ======================================================================== *)
 558
 559 let HP = prove
 560  (`!l:A#A->bool. poset l ==>
 561         ?P. chain(l) P /\ !Q. chain(l) Q  /\ P SUBSET Q ==> (Q = P)`,
 562   GEN_TAC THEN DISCH_TAC THEN
 563   X_CHOOSE_THEN `w:A#A->bool` MP_TAC (SPEC `\x:A. T` WO) THEN
 564   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 565   GEN_REWRITE_TAC LAND_CONV [FUN_EQ_THM] THEN BETA_TAC THEN
 566   REWRITE_TAC[] THEN DISCH_TAC THEN
 567   IMP_RES_THEN (MP_TAC o SPEC `\x:A. fl(l) x`) WOSET_WELL THEN
 568   BETA_TAC THEN ASM_REWRITE_TAC[] THEN
 569   ASM_CASES_TAC `?x:A. fl(l) x` THEN ASM_REWRITE_TAC[] THENL
 570    [DISCH_THEN(X_CHOOSE_THEN `b:A` STRIP_ASSUME_TAC);
 571     FIRST_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
 572     EXISTS_TAC `\x:A. F` THEN REWRITE_TAC[chain; SUBSET_PRED] THEN
 573     GEN_TAC THEN GEN_REWRITE_TAC RAND_CONV [FUN_EQ_THM] THEN
 574     CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN
 575     DISCH_THEN(X_CHOOSE_THEN `u:A` MP_TAC o
 576       GEN_REWRITE_RULE I [NOT_FORALL_THM]) THEN
 577     REWRITE_TAC[] THEN DISCH_TAC THEN
 578     DISCH_THEN(MP_TAC o SPECL [`u:A`; `u:A`]) THEN
 579     IMP_RES_THEN(ASSUME_TAC o GSYM) POSET_FLEQ THEN ASM_REWRITE_TAC[]] THEN
 580   SUBGOAL_THEN `?f. !x. f x = if fl(l) x /\
 581                                  (!y. less w (y,x) ==> l (x,f y) \/ l (f y,x))
 582                               then (x:A) else b`
 583   (CHOOSE_TAC o GSYM) THENL
 584    [SUBGOAL_THEN `WF(\x:A y. (less w)(x,y))` MP_TAC THENL
 585      [REWRITE_TAC[WF] THEN GEN_TAC THEN
 586       FIRST_ASSUM(MP_TAC o SPEC_ALL o MATCH_MP WOSET_WELL) THEN
 587       ASM_REWRITE_TAC[less] THEN ASM_MESON_TAC[WOSET_ANTISYM];
 588       DISCH_THEN(MATCH_MP_TAC o MATCH_MP WF_REC) THEN
 589       REWRITE_TAC[] THEN REPEAT GEN_TAC THEN
 590       REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 591       ASM_MESON_TAC[]]; ALL_TAC] THEN
 592   IMP_RES_THEN(IMP_RES_THEN ASSUME_TAC) POSET_REFL THEN
 593   SUBGOAL_THEN `(f:A->A) b = b` ASSUME_TAC THENL
 594    [FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `b:A`) THEN
 595     REWRITE_TAC[COND_ID] THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 596   SUBGOAL_THEN `!x:A. fl(l:A#A->bool) (f x)` ASSUME_TAC THENL
 597    [GEN_TAC THEN FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `x:A`) THEN
 598     COND_CASES_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
 599   FIRST_ASSUM(ANTE_RES_THEN (ASSUME_TAC o GEN_ALL) o SPEC_ALL) THEN
 600   SUBGOAL_THEN `!x:A. (l:A#A->bool)(b,f x) \/ l(f x,b)` ASSUME_TAC THENL
 601    [GEN_TAC THEN MP_TAC(SPEC `x:A` (ASSUME `!x:A. (w:A#A->bool)(b,f x)`)) THEN
 602     FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `x:A`) THEN
 603     COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 604     ASM_CASES_TAC `x:A = b` THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 605     SUBGOAL_THEN `(less w)(b:A,x)` MP_TAC THENL
 606      [ASM_REWRITE_TAC[less] THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
 607       FIRST_ASSUM ACCEPT_TAC; ALL_TAC] THEN
 608     DISCH_THEN(fun th -> FIRST_ASSUM(MP_TAC o C MATCH_MP th o CONJUNCT2)) THEN
 609     ASM_REWRITE_TAC[] THEN DISCH_THEN DISJ_CASES_TAC THEN
 610     ASM_REWRITE_TAC[]; ALL_TAC] THEN
 611   SUBGOAL_THEN `!x y. l((f:A->A) x,f y) \/ l(f y,f x)` ASSUME_TAC THENL
 612    [REPEAT GEN_TAC THEN
 613     IMP_RES_THEN(MP_TAC o SPECL [`x:A`; `y:A`]) WOSET_TOTAL_LT THEN
 614     ASM_REWRITE_TAC[] THEN
 615     DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THENL
 616      [ASM_REWRITE_TAC[] THEN IMP_RES_THEN MATCH_MP_TAC POSET_REFL;
 617       ONCE_REWRITE_TAC[DISJ_SYM] THEN
 618       FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `y:A`);
 619       FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `x:A`)] THEN
 620     TRY COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 621     FIRST_ASSUM(IMP_RES_THEN ACCEPT_TAC o CONJUNCT2); ALL_TAC] THEN
 622   EXISTS_TAC `\y:A. ?x:A. y = f(x)` THEN
 623   SUBGOAL_THEN `chain(l:A#A->bool)(\y. ?x:A. y = f x)` ASSUME_TAC THENL
 624    [REWRITE_TAC[chain] THEN BETA_TAC THEN REPEAT GEN_TAC THEN
 625     DISCH_THEN(CONJUNCTS_THEN(CHOOSE_THEN SUBST1_TAC)); ALL_TAC] THEN
 626   ASM_REWRITE_TAC[] THEN X_GEN_TAC `Q:A->bool` THEN STRIP_TAC THEN
 627   GEN_REWRITE_TAC I [FUN_EQ_THM] THEN X_GEN_TAC `z:A` THEN EQ_TAC THENL
 628    [DISCH_TAC THEN BETA_TAC THEN EXISTS_TAC `z:A` THEN
 629     FIRST_ASSUM(SUBST1_TAC o SYM o SPEC `z:A`) THEN
 630     SUBGOAL_THEN `fl(l:A#A->bool) z /\
 631                   !y. (less w)(y,z) ==> l(z,f y) \/ l(f y,z)`
 632     (fun th -> REWRITE_TAC[th]) THEN CONJ_TAC THENL
 633      [UNDISCH_TAC `chain(l:A#A->bool) Q` THEN REWRITE_TAC[chain] THEN
 634       DISCH_THEN(MP_TAC o SPECL [`z:A`; `z:A`]) THEN ASM_REWRITE_TAC[fl] THEN
 635       DISCH_TAC THEN EXISTS_TAC `z:A` THEN ASM_REWRITE_TAC[];
 636       X_GEN_TAC `y:A` THEN DISCH_TAC THEN
 637       UNDISCH_TAC `chain(l:A#A->bool) Q` THEN REWRITE_TAC[chain] THEN
 638       DISCH_THEN(MP_TAC o SPECL [`z:A`; `(f:A->A) y`]) THEN
 639       DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
 640       FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET_PRED]) THEN
 641       BETA_TAC THEN EXISTS_TAC `y:A` THEN REFL_TAC];
 642     SPEC_TAC(`z:A`,`z:A`) THEN ASM_REWRITE_TAC[GSYM SUBSET_PRED]]);;
 643
 644 (* ======================================================================== *)
 645 (* (4) HAUSDORFF MAXIMAL PRINCIPLE ==> ZORN'S LEMMA                         *)
 646 (* ======================================================================== *)
 647
 648 let ZL = prove
 649  (`!l:A#A->bool. poset l /\
 650            (!P. chain(l) P ==> (?y. fl(l) y /\ !x. P x ==> l(x,y))) ==>
 651         ?y. fl(l) y /\ !x. l(y,x) ==> (y = x)`,
 652   GEN_TAC THEN STRIP_TAC THEN
 653   FIRST_ASSUM(X_CHOOSE_THEN `M:A->bool` STRIP_ASSUME_TAC o MATCH_MP HP) THEN
 654   UNDISCH_TAC `!P. chain(l:A#A->bool) P
 655                    ==> (?y. fl(l) y /\ !x. P x ==> l(x,y))` THEN
 656   DISCH_THEN(MP_TAC o SPEC `M:A->bool`) THEN ASM_REWRITE_TAC[] THEN
 657   DISCH_THEN(X_CHOOSE_THEN `m:A` STRIP_ASSUME_TAC) THEN
 658   EXISTS_TAC `m:A` THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `z:A` THEN
 659   DISCH_TAC THEN GEN_REWRITE_TAC I [TAUT `a <=> ~ ~a`] THEN DISCH_TAC THEN
 660   SUBGOAL_THEN `chain(l) (\x:A. M x \/ (x = z))` MP_TAC THENL
 661    [REWRITE_TAC[chain] THEN BETA_TAC THEN REPEAT GEN_TAC THEN
 662     DISCH_THEN(CONJUNCTS_THEN DISJ_CASES_TAC) THEN
 663     ASM_REWRITE_TAC[] THENL
 664      [UNDISCH_TAC `chain(l:A#A->bool) M` THEN REWRITE_TAC[chain] THEN
 665       DISCH_THEN MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
 666       DISJ1_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP POSET_TRANS) THEN
 667       EXISTS_TAC `m:A` THEN ASM_REWRITE_TAC[] THEN
 668       FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC;
 669       DISJ2_TAC THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP POSET_TRANS) THEN
 670       EXISTS_TAC `m:A` THEN ASM_REWRITE_TAC[] THEN
 671       FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC;
 672       FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP POSET_REFL) THEN
 673       REWRITE_TAC[fl] THEN EXISTS_TAC `m:A` THEN ASM_REWRITE_TAC[]];
 674     ALL_TAC] THEN
 675   SUBGOAL_THEN `M SUBSET (\x:A. M x \/ (x = z))` MP_TAC THENL
 676    [REWRITE_TAC[SUBSET_PRED] THEN GEN_TAC THEN BETA_TAC THEN
 677     DISCH_THEN(fun th -> REWRITE_TAC[th]); ALL_TAC] THEN
 678   GEN_REWRITE_TAC I [TAUT `(a ==> b ==> c) <=> (b /\ a ==> c)`] THEN
 679   DISCH_THEN(fun th -> FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
 680   REWRITE_TAC[] THEN GEN_REWRITE_TAC RAND_CONV [FUN_EQ_THM] THEN
 681   DISCH_THEN(MP_TAC o SPEC `z:A`) THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN
 682   DISCH_THEN(fun th -> FIRST_ASSUM(ASSUME_TAC o C MATCH_MP th)) THEN
 683   FIRST_ASSUM(MP_TAC o SPECL [`m:A`; `z:A`] o MATCH_MP POSET_ANTISYM) THEN
 684   ASM_REWRITE_TAC[]);;
 685
 686 (* ======================================================================== *)
 687 (* (5) ZORN'S LEMMA ==> KURATOWSKI'S LEMMA                                  *)
 688 (* ======================================================================== *)
 689
 690 let KL_POSET_LEMMA = prove
 691  (`poset (\(c1,c2). C SUBSET c1 /\ c1 SUBSET c2 /\ chain(l:A#A->bool) c2)`,
 692   REWRITE_TAC[poset] THEN PBETA_TAC THEN REPEAT CONJ_TAC THENL
 693    [X_GEN_TAC `P:A->bool` THEN REWRITE_TAC[fl] THEN PBETA_TAC THEN
 694     DISCH_THEN(X_CHOOSE_THEN `Q:A->bool` STRIP_ASSUME_TAC) THEN
 695     ASM_REWRITE_TAC[SUBSET_REFL] THENL
 696      [MATCH_MP_TAC CHAIN_SUBSET; MATCH_MP_TAC SUBSET_TRANS];
 697     GEN_TAC THEN X_GEN_TAC `Q:A->bool` THEN GEN_TAC THEN STRIP_TAC THEN
 698     ASM_REWRITE_TAC[] THEN MATCH_MP_TAC SUBSET_TRANS;
 699     REPEAT STRIP_TAC THEN MATCH_MP_TAC SUBSET_ANTISYM] THEN
 700   TRY(EXISTS_TAC `Q:A->bool`) THEN ASM_REWRITE_TAC[]);;
 701
 702 let KL = prove
 703  (`!l:A#A->bool. poset l ==>
 704         !C. chain(l) C ==>
 705             ?P. (chain(l) P /\ C SUBSET P) /\
 706                 (!R. chain(l) R /\ P SUBSET R ==> (R = P))`,
 707   REPEAT STRIP_TAC THEN
 708   MP_TAC(ISPEC `\(c1,c2). C SUBSET c1 /\ c1 SUBSET c2 /\
 709                           chain(l:A#A->bool) c2` ZL) THEN PBETA_TAC THEN
 710   REWRITE_TAC[KL_POSET_LEMMA; MATCH_MP POSET_FLEQ KL_POSET_LEMMA] THEN
 711   PBETA_TAC THEN
 712   W(C SUBGOAL_THEN (fun t ->REWRITE_TAC[t]) o
 713   funpow 2 (fst o dest_imp) o snd) THENL
 714    [X_GEN_TAC `P:(A->bool)->bool` THEN GEN_REWRITE_TAC LAND_CONV [chain] THEN
 715     PBETA_TAC THEN DISCH_TAC THEN ASM_CASES_TAC `?D:A->bool. P D` THENL
 716      [EXISTS_TAC `UNIONS(P) :A->bool` THEN REWRITE_TAC[SUBSET_REFL] THEN
 717       FIRST_ASSUM(X_CHOOSE_TAC `D:A->bool`) THEN
 718       FIRST_ASSUM(MP_TAC o SPECL [`D:A->bool`; `D:A->bool`]) THEN
 719       REWRITE_TAC[ASSUME `(P:(A->bool)->bool) D`; SUBSET_REFL] THEN
 720       STRIP_TAC THEN
 721       MATCH_MP_TAC(TAUT `a /\ b /\ (a /\ b ==> c) ==> (a /\ b) /\ c`) THEN
 722       REPEAT CONJ_TAC THENL
 723        [REWRITE_TAC[UNIONS_PRED; SUBSET_PRED] THEN REPEAT STRIP_TAC THEN
 724         BETA_TAC THEN EXISTS_TAC `D:A->bool` THEN ASM_REWRITE_TAC[] THEN
 725         FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET_PRED]) THEN
 726         ASM_REWRITE_TAC[];
 727         REWRITE_TAC[chain; UNIONS_PRED] THEN
 728         MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN
 729         BETA_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
 730          (X_CHOOSE_TAC `A:A->bool`) (X_CHOOSE_TAC `B:A->bool`)) THEN
 731         FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
 732         DISCH_THEN(MP_TAC o SPECL [`A:A->bool`; `B:A->bool`]) THEN
 733         ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
 734          [UNDISCH_TAC `chain(l:A#A->bool) B`;
 735           UNDISCH_TAC `chain(l:A#A->bool) A`] THEN
 736         REWRITE_TAC[chain] THEN DISCH_THEN MATCH_MP_TAC THEN
 737         ASM_REWRITE_TAC[] THEN
 738         FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[SUBSET_PRED]) THEN
 739         ASM_REWRITE_TAC[];
 740         STRIP_TAC THEN X_GEN_TAC `X:A->bool` THEN DISCH_TAC THEN
 741         FIRST_ASSUM(MP_TAC o SPECL [`X:A->bool`; `X:A->bool`]) THEN
 742         REWRITE_TAC[] THEN DISCH_THEN(IMP_RES_THEN STRIP_ASSUME_TAC) THEN
 743         ASM_REWRITE_TAC[] THEN REWRITE_TAC[UNIONS_PRED; SUBSET_PRED] THEN
 744         REPEAT STRIP_TAC THEN BETA_TAC THEN EXISTS_TAC `X:A->bool` THEN
 745         ASM_REWRITE_TAC[]];
 746       EXISTS_TAC `C:A->bool` THEN
 747       FIRST_ASSUM(ASSUME_TAC o GEN_REWRITE_RULE I [NOT_EXISTS_THM]) THEN
 748       ASM_REWRITE_TAC[SUBSET_REFL]];
 749     DISCH_THEN(X_CHOOSE_THEN `D:A->bool` STRIP_ASSUME_TAC) THEN
 750     EXISTS_TAC `D:A->bool` THEN ASM_REWRITE_TAC[] THEN
 751     REPEAT STRIP_TAC THEN CONV_TAC SYM_CONV THEN
 752     FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
 753
 754 (* ------------------------------------------------------------------------- *)
 755 (* Also the order extension theorem, using Abian's proof.                    *)
 756 (* ------------------------------------------------------------------------- *)
 757
 758 let OEP = prove
 759  (`!p:A#A->bool. poset p ==> ?t. toset t /\ fl(t) = fl(p) /\ p SUBSET t`,
 760   REPEAT STRIP_TAC THEN
 761   MP_TAC(ISPEC `fl(p:A#A->bool)` WO) THEN ASM_REWRITE_TAC[] THEN
 762   DISCH_THEN(X_CHOOSE_THEN `w:A#A->bool` STRIP_ASSUME_TAC) THEN
 763   ABBREV_TAC
 764    `t = \(x:A,y:A). fl p x /\ fl p y /\
 765                     (x = y \/
 766                      ?i. fl p i /\
 767                          (!j. w(j,i) /\ ~(j = i) ==> (p(j,x) <=> p(j,y))) /\
 768                          ~p(i,x) /\ p(i,y))` THEN
 769   EXISTS_TAC `t:A#A->bool` THEN
 770   SUBGOAL_THEN
 771    `!x:A y:A. fl p x /\ fl p y /\ ~(x = y)
 772               ==> ?i. fl p i /\
 773                       (!j:A. w(j,i) /\ ~(j = i) ==> (p(j,x) <=> p(j,y))) /\
 774                       ~(p(i,x) <=> p(i,y))`
 775   (LABEL_TAC "*") THENL
 776    [REPEAT STRIP_TAC THEN
 777     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [woset]) THEN ASM_SIMP_TAC[] THEN
 778     REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 779     DISCH_THEN(MP_TAC o SPEC `\i:A. fl p i /\ ~(p(i,x) <=> p(i,y))`) THEN
 780     ASM_REWRITE_TAC[] THEN ANTS_TAC THENL
 781      [FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [poset]) THEN ASM_MESON_TAC[];
 782       MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `i:A` THEN
 783        ASM_MESON_TAC[fl]];
 784     ALL_TAC] THEN
 785   SUBGOAL_THEN `!x:A y:A. p(x,y) ==> t(x,y)` ASSUME_TAC THENL
 786    [EXPAND_TAC "t" THEN REWRITE_TAC[] THEN
 787     REPEAT GEN_TAC THEN STRIP_TAC THEN
 788     REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[fl]; ALL_TAC]) THEN
 789     ASM_CASES_TAC `x:A = y` THENL [ASM_MESON_TAC[fl]; ALL_TAC] THEN
 790     REMOVE_THEN "*" (MP_TAC o SPECL [`x:A`; `y:A`]) THEN ASM_SIMP_TAC[] THEN
 791     ANTS_TAC THENL [ASM_MESON_TAC[fl]; MATCH_MP_TAC MONO_EXISTS] THEN
 792     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [poset]) THEN ASM_MESON_TAC[];
 793     ALL_TAC] THEN
 794   ASM_REWRITE_TAC[SUBSET; FORALL_PAIR_THM; IN] THEN
 795   MATCH_MP_TAC(TAUT `q /\ (q ==> p) ==> p /\ q`) THEN CONJ_TAC THENL
 796    [MATCH_MP_TAC SUBSET_ANTISYM THEN
 797     ASM_REWRITE_TAC[SUBSET; FORALL_PAIR_THM; IN] THEN
 798     EXPAND_TAC "t" THEN REWRITE_TAC[fl] THEN ASM_MESON_TAC[];
 799     DISCH_TAC THEN ASM_REWRITE_TAC[toset; poset]] THEN
 800   EXPAND_TAC "t" THEN REWRITE_TAC[] THEN
 801   FIRST_X_ASSUM(STRIP_ASSUME_TAC o GEN_REWRITE_RULE I [poset]) THEN
 802   REPEAT CONJ_TAC THENL
 803    [MAP_EVERY X_GEN_TAC [`x:A`; `y:A`; `z:A`] THEN
 804     ASM_CASES_TAC `x:A = z` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[] THEN
 805     ASM_CASES_TAC `y:A = z` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[] THEN
 806     ASM_CASES_TAC `y:A = x` THEN ASM_REWRITE_TAC[] THEN SIMP_TAC[] THEN
 807     ASM_CASES_TAC `fl p (x:A)` THEN ASM_REWRITE_TAC[] THEN
 808     ASM_CASES_TAC `fl p (y:A)` THEN ASM_REWRITE_TAC[] THEN
 809     ASM_CASES_TAC `fl p (z:A)` THEN ASM_REWRITE_TAC[] THEN
 810     DISCH_THEN(CONJUNCTS_THEN2
 811      (X_CHOOSE_THEN `m:A` STRIP_ASSUME_TAC)
 812      (X_CHOOSE_THEN `n:A` STRIP_ASSUME_TAC)) THEN
 813     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [woset]) THEN
 814     REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 815     DISCH_THEN(MP_TAC o SPECL [`m:A`; `n:A`] o CONJUNCT1) THEN
 816     ANTS_TAC THENL [ASM_MESON_TAC[fl]; ALL_TAC] THEN STRIP_TAC THENL
 817      [EXISTS_TAC `m:A`; EXISTS_TAC `n:A`] THEN ASM_MESON_TAC[];
 818     MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN
 819     ASM_CASES_TAC `y:A = x` THEN ASM_REWRITE_TAC[] THEN
 820     ASM_CASES_TAC `fl p (x:A)` THEN ASM_REWRITE_TAC[] THEN
 821     ASM_CASES_TAC `fl p (y:A)` THEN ASM_REWRITE_TAC[] THEN
 822     DISCH_THEN(CONJUNCTS_THEN2
 823      (X_CHOOSE_THEN `m:A` STRIP_ASSUME_TAC)
 824      (X_CHOOSE_THEN `n:A` STRIP_ASSUME_TAC)) THEN
 825     FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [woset]) THEN
 826     REPLICATE_TAC 3 (DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 827     DISCH_THEN(MP_TAC o SPECL [`m:A`; `n:A`] o CONJUNCT1) THEN
 828     ASM_MESON_TAC[];
 829     MAP_EVERY X_GEN_TAC [`x:A`; `y:A`] THEN
 830     ASM_CASES_TAC `y:A = x` THEN ASM_REWRITE_TAC[IN] THEN
 831     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 832     REMOVE_THEN "*" (MP_TAC o SPECL [`x:A`; `y:A`]) THEN
 833     ASM_REWRITE_TAC[OR_EXISTS_THM] THEN MATCH_MP_TAC MONO_EXISTS THEN
 834     MESON_TAC[]]);;