1 (* ========================================================================= *)
2 (* Proof of some useful AC equivalents like wellordering and Zorn's Lemma. *)
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 (* ========================================================================= *)
9 let PBETA_TAC = CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV);;
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;;
14 let SUBSET_PRED = prove
15 (`!P Q. P SUBSET Q <=> !x. P x ==> Q x`,
16 REWRITE_TAC[SUBSET; IN]);;
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]);;
22 (* ======================================================================== *)
23 (* (1) Definitions and general lemmas. *)
24 (* ======================================================================== *)
26 (* ------------------------------------------------------------------------ *)
27 (* Irreflexive version of an ordering. *)
28 (* ------------------------------------------------------------------------ *)
30 let less = new_definition
31 `(less l)(x,y) <=> (l:A#A->bool)(x,y) /\ ~(x = y)`;;
33 (* ------------------------------------------------------------------------ *)
34 (* Field of an uncurried binary relation *)
35 (* ------------------------------------------------------------------------ *)
37 let fl = new_definition
38 `fl(l:A#A->bool) x <=> ?y:A. l(x,y) \/ l(y,x)`;;
40 (* ------------------------------------------------------------------------ *)
41 (* Partial order (we infer the domain from the field of the relation) *)
42 (* ------------------------------------------------------------------------ *)
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))`;;
50 (* ------------------------------------------------------------------------ *)
51 (* Chain in a poset (Defined as a subset of the field, not the ordering) *)
52 (* ------------------------------------------------------------------------ *)
54 let chain = new_definition
55 `chain(l:A#A->bool) P <=> (!x y. P x /\ P y ==> l(x,y) \/ l(y,x))`;;
57 (* ------------------------------------------------------------------------- *)
59 (* ------------------------------------------------------------------------- *)
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)`;;
65 (* ------------------------------------------------------------------------ *)
67 (* ------------------------------------------------------------------------ *)
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))))`;;
78 (* ------------------------------------------------------------------------ *)
79 (* General (reflexive) notion of initial segment. *)
80 (* ------------------------------------------------------------------------ *)
82 parse_as_infix("inseg",(12,"right"));;
84 let inseg = new_definition
85 `(l:A#A->bool) inseg m <=> !x y. l(x,y) <=> m(x,y) /\ fl(l) y`;;
87 (* ------------------------------------------------------------------------ *)
88 (* Specific form of initial segment: `all elements in fl(l) less than a`. *)
89 (* ------------------------------------------------------------------------ *)
91 let linseg = new_definition
92 `linseg (l:A#A->bool) a = \(x,y). l(x,y) /\ (less l)(y,a)`;;
94 (* ------------------------------------------------------------------------ *)
95 (* `Ordinals`, i.e. canonical wosets using choice operator. *)
96 (* ------------------------------------------------------------------------ *)
98 let ordinal = new_definition
99 `ordinal(l:A#A->bool) <=>
100 woset(l) /\ (!x. fl(l) x ==> (x = (@) (\y. ~(less l)(y,x))))`;;
102 (* ------------------------------------------------------------------------ *)
103 (* Now useful things about the orderings *)
104 (* ------------------------------------------------------------------------ *)
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)`)));;
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]);;
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[]);;
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)`)));;
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
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]);;
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[]);;
136 (* ------------------------------------------------------------------------ *)
137 (* Antisymmetry and wellfoundedness are sufficient for a wellorder *)
138 (* ------------------------------------------------------------------------ *)
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
152 FIRST_ASSUM(MP_TAC o SPEC `\w:A. (w = x) \/ (w = y)`)] THEN
155 (* ------------------------------------------------------------------------ *)
157 (* ------------------------------------------------------------------------ *)
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);;
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]);;
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]);;
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]);;
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]);;
188 (* ======================================================================== *)
189 (* (2) AXIOM OF CHOICE ==> CANTOR-ZERMELO WELLORDERING THEOREM *)
190 (* ======================================================================== *)
192 (* ------------------------------------------------------------------------ *)
193 (* UNIONS of initial segments is an initial segment. *)
194 (* ------------------------------------------------------------------------ *)
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[]);;
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[]);;
204 (* ------------------------------------------------------------------------ *)
205 (* Initial segment of a woset is a woset. *)
206 (* ------------------------------------------------------------------------ *)
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[]);;
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]);;
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]]);;
224 (* ------------------------------------------------------------------------ *)
225 (* Properties of segments of the `linseg` form. *)
226 (* ------------------------------------------------------------------------ *)
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]);;
233 let LINSEG_WOSET = prove
234 (`!(l:A#A->bool) a. woset l ==> woset(linseg l a)`,
235 MESON_TAC[INSEG_WOSET; LINSEG_INSEG]);;
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]);;
242 (* ------------------------------------------------------------------------ *)
243 (* Key fact: a proper initial segment is of the special form. *)
244 (* ------------------------------------------------------------------------ *)
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]);;
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]);;
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]);;
273 (* ------------------------------------------------------------------------ *)
274 (* A proper initial segment can be extended by its bounding element. *)
275 (* ------------------------------------------------------------------------ *)
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]);;
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);;
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)))
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]);;
298 (* ------------------------------------------------------------------------ *)
299 (* Key canonicality property of ordinals. *)
300 (* ------------------------------------------------------------------------ *)
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 /\
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]);;
324 let ORDINAL_CHAINED = prove
325 (`!(l:A#A->bool) m. ordinal(l) /\ ordinal(m) ==> m inseg l \/ l inseg m`,
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
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
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[]);;
350 (* ------------------------------------------------------------------------ *)
351 (* Proof that any none-universe ordinal can be extended to its "successor". *)
352 (* ------------------------------------------------------------------------ *)
356 fl(\(x,y). l(x,y) \/ (y = a) /\ (fl(l) x \/ (x = a))) x <=>
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
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
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
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
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
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
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[]]]);;
411 (* ------------------------------------------------------------------------ *)
412 (* The union of a set of ordinals is an ordinal. *)
413 (* ------------------------------------------------------------------------ *)
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)
423 (X_CHOOSE_THEN `m:A#A->bool` (CONJUNCTS_THEN2 (ANTE_RES_THEN ASSUME_TAC)
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
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
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[]]]]);;
488 (* ------------------------------------------------------------------------ *)
489 (* Consequently, every type can be wellordered (and by an ordinal). *)
490 (* ------------------------------------------------------------------------ *)
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[]);;
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[]);;
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[]]);;
521 (* ------------------------------------------------------------------------ *)
522 (* At least -- every set can be wellordered. *)
523 (* ------------------------------------------------------------------------ *)
525 let FL_RESTRICT = prove
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[]);;
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
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
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]);;
555 (* ======================================================================== *)
556 (* (3) CANTOR-ZERMELO WELL-ORDERING THEOREM ==> HAUSDORFF MAXIMAL PRINCIPLE *)
557 (* ======================================================================== *)
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))
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
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]]);;
644 (* ======================================================================== *)
645 (* (4) HAUSDORFF MAXIMAL PRINCIPLE ==> ZORN'S LEMMA *)
646 (* ======================================================================== *)
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[]];
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
686 (* ======================================================================== *)
687 (* (5) ZORN'S LEMMA ==> KURATOWSKI'S LEMMA *)
688 (* ======================================================================== *)
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[]);;
703 (`!l:A#A->bool. poset l ==>
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
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
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
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
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
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[]]);;
754 (* ------------------------------------------------------------------------- *)
755 (* Also the order extension theorem, using Abian's proof. *)
756 (* ------------------------------------------------------------------------- *)
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
764 `t = \(x:A,y:A). fl p x /\ fl p y /\
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
771 `!x:A y:A. fl p x /\ fl p y /\ ~(x = y)
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
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[];
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
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