ordinalBasicScript.sml
1Theory ordinalBasic[bare]
2
3Ancestors
4 wellorder pred_set set_relation pair option cardinalityCore
5Libs
6 HolKernel Parse boolLib boolSimps simpLib BasicProvers QLib metisLib
7 TotalDefn pred_setLib pureSimps TypeBase tautLib[qualified]
8
9(* cardinalityCoreTheory makes no grammar of its own -- it is every
10 theory's ancestor through the datatype package, and the ASCII
11 forms are tokens wherever they reach. What this theory writes
12 it sets up for itself. *)
13Overload "<<="[local] = “cardleq”
14Overload cardlt[local] = “λs1 s2. ¬cardleq s2 s1”
15val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
16val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
17Overload "<</="[local] = “cardlt”
18val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
19val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
20Overload "=~"[local] = “cardeq”
21
22fun bossify stac ths g ctxt =
23 stac (srw_ss_of ctxt ++ numSimps.ARITH_ss) ths g ctxt
24val simp = bossify asm_simp_tac
25fun dsimp ths = simp(SF DNF_ss :: ths)
26val fs = bossify full_simp_tac
27val gvs = bossify (global_simp_tac {droptrues = true, elimvars = true,
28 oldestfirst = true, strip = true})
29val gs = bossify (global_simp_tac {droptrues = true, elimvars = false,
30 oldestfirst = true, strip = true})
31val rw = srw_tac[numSimps.ARITH_ss]
32val metis_tac = METIS_TAC
33
34val impI = tautLib.TAUT_PROVE ``~p \/ q <=> (p ==> q)``
35
36(* perform quotient, creating a type of "ordinals". *)
37fun mk_def(s,t) =
38 {def_name = s ^ "_def", fixity = NONE, fname = s, func = t};
39
40Theorem orderiso_equiv[local]:
41 !s1 s2. orderiso (s1:'a wellorder) (s2:'a wellorder) <=>
42 (orderiso s1 : 'a wellorder set = orderiso s2)
43Proof
44 rw[FUN_EQ_THM, EQ_IMP_THM] >>
45 metis_tac [orderiso_SYM, orderiso_TRANS, orderiso_REFL]
46QED
47
48val alphaise =
49 INST_TYPE [beta |-> ``:'a inf``, delta |-> ``:'a inf``,
50 gamma |-> ``:'a inf``, alpha |-> ``:'a inf``]
51
52val [ordlt_REFL, ordlt_TRANS, ordlt_WF0, ordlt_trichotomy] =
53 quotient.define_quotient_types_full
54 {
55 types = [{name = "ordinal", equiv = alphaise orderiso_equiv}],
56 defs = map mk_def
57 [("ordlt", ``orderlt : 'a inf wellorder -> 'a inf wellorder -> bool``)],
58 tyop_equivs = [],
59 tyop_quotients = [],
60 tyop_simps = [],
61 respects = [alphaise orderlt_orderiso, alphaise finite_iso],
62 poly_preserves = [],
63 poly_respects = [],
64 old_thms = [alphaise orderlt_REFL, alphaise orderlt_TRANS,
65 alphaise (REWRITE_RULE [relationTheory.WF_DEF] orderlt_WF),
66 alphaise orderlt_trichotomy]}
67
68Theorem ordlt_REFL[simp] = ordlt_REFL
69Theorem ordlt_TRANS = ordlt_TRANS
70Theorem ordlt_WF0 = ordlt_WF0
71Theorem ordlt_WF =
72 REWRITE_RULE [GSYM relationTheory.WF_DEF] ordlt_WF0
73
74Overload "<"[local] = ``ordlt``
75Overload "<="[local] = ``\a b. ~(b < a)``
76
77Theorem ordlt_trichotomy = ordlt_trichotomy
78
79Overload mkOrdinal = ``ordinal_ABS``
80
81Definition allOrds_def:
82 allOrds = mkWO { (x,y) | (x = y) \/ ordlt x y }
83End
84
85Theorem wellorder_allOrds:
86 wellorder { (x,y) | x = y \/ ordlt x y }
87Proof
88 simp[wellorder_def, strict_def, wellfounded_WF, relationTheory.WF_DEF] >>
89 rpt conj_tac >| [
90 simp_tac (srw_ss() ++ CONJ_ss)
91 [REWRITE_RULE[SPECIFICATION] GSPECIFICATION, EXISTS_PROD] >>
92 metis_tac[ordlt_REFL, ordlt_WF0],
93 simp[linear_order_def, in_domain, in_range] >> rw[]
94 >- (simp[transitive_def]>> metis_tac [ordlt_TRANS])
95 >- (simp[antisym_def] >> metis_tac [ordlt_TRANS, ordlt_REFL]) >>
96 metis_tac [ordlt_trichotomy],
97 simp[reflexive_def]
98 ]
99QED
100
101Theorem WIN_allOrds:
102 (x,y) WIN allOrds <=> ordlt x y
103Proof
104 simp[allOrds_def, destWO_mkWO, wellorder_allOrds, strict_def] >>
105 metis_tac [ordlt_REFL]
106QED
107
108Theorem elsOf_allOrds:
109 elsOf allOrds = univ(:'a ordinal)
110Proof
111 rw[elsOf_def, EXTENSION, in_domain, in_range, allOrds_def,
112 destWO_mkWO, wellorder_allOrds] >>
113 metis_tac [ordlt_trichotomy]
114QED
115
116val (mkOrdinal_REP, orderiso_mkOrdinal) =
117 theorem "ordinal_QUOTIENT"
118 |> SIMP_RULE (srw_ss()) [quotientTheory.QUOTIENT_def, orderiso_REFL]
119 |> CONJ_PAIR
120Theorem mkOrdinal_REP = mkOrdinal_REP
121Theorem orderiso_mkOrdinal = orderiso_mkOrdinal
122
123Theorem ordlt_mkOrdinal:
124 ordlt o1 o2 <=>
125 !w1 w2. (mkOrdinal w1 = o1) /\ (mkOrdinal w2 = o2) ==> orderlt w1 w2
126Proof
127 rw[definition "ordlt_def"] >> eq_tac >> rpt strip_tac >| [
128 `orderiso w1 (ordinal_REP o1) /\ orderiso w2 (ordinal_REP o2)`
129 by metis_tac [orderiso_mkOrdinal, mkOrdinal_REP] >>
130 metis_tac [orderlt_orderiso],
131 simp[mkOrdinal_REP]
132 ]
133QED
134
135Theorem orderlt_iso_REFL:
136 orderiso w1 w2 ==> ~orderlt w1 w2
137Proof
138 metis_tac [orderlt_orderiso, orderlt_REFL, orderiso_REFL]
139QED
140
141Theorem orderiso_wobound2:
142 orderiso (wobound x w) (wobound y w) ==> ~((x,y) WIN w)
143Proof
144 rpt strip_tac >>
145 qsuff_tac `orderlt (wobound x w) (wobound y w)`
146 >- metis_tac [orderlt_iso_REFL] >>
147 simp[orderlt_def] >> qexists_tac `x` >>
148 simp[elsOf_wobound, wobound2,orderiso_REFL]
149QED
150
151Theorem wellorder_ordinal_isomorphism:
152 !w. orderiso w (wobound (mkOrdinal w) allOrds)
153Proof
154 spose_not_then assume_tac >>
155 pop_assum (strip_assume_tac o REWRITE_RULE [] o
156 HO_MATCH_MP (REWRITE_RULE [relationTheory.WF_DEF] orderlt_WF)) >>
157 `orderlt w (wobound (mkOrdinal w) allOrds) \/
158 orderlt (wobound (mkOrdinal w) allOrds) w`
159 by metis_tac [orderlt_trichotomy]
160 >| [
161 pop_assum mp_tac >> simp[orderlt_def] >> qx_gen_tac `b` >>
162 Cases_on `b IN elsOf (wobound (mkOrdinal w) allOrds)` >> simp[] >>
163 pop_assum mp_tac >> simp[elsOf_wobound, wobound2] >>
164 simp[WIN_allOrds] >> rpt strip_tac >>
165 fs[ordlt_mkOrdinal] >>
166 first_x_assum (qspecl_then [`ordinal_REP b`, `w`] mp_tac) >>
167 simp[mkOrdinal_REP] >> strip_tac >> res_tac >> fs[mkOrdinal_REP] >>
168 metis_tac [orderiso_TRANS, orderiso_SYM, orderlt_iso_REFL],
169 pop_assum mp_tac >> simp[orderlt_def] >> qx_gen_tac `e` >>
170 Cases_on `e IN elsOf w` >> simp[] >> strip_tac >>
171 `orderlt (wobound e w) w`
172 by (simp[orderlt_def] >> metis_tac [orderiso_REFL]) >>
173 qabbrev_tac `E = wobound e w` >>
174 `orderiso E (wobound (mkOrdinal E) allOrds)` by metis_tac[] >>
175 `orderiso (wobound (mkOrdinal w) allOrds) (wobound (mkOrdinal E) allOrds)`
176 by metis_tac [orderiso_TRANS] >>
177 `ordlt (mkOrdinal E) (mkOrdinal w)`
178 by (simp[ordlt_mkOrdinal] >>
179 map_every qx_gen_tac [`w1`, `w2`] >>
180 simp[GSYM orderiso_mkOrdinal] >>
181 metis_tac[orderlt_orderiso, orderiso_SYM]) >>
182 `~((mkOrdinal E, mkOrdinal w) WIN allOrds)`
183 by metis_tac[orderiso_wobound2,orderiso_SYM]>>
184 fs[WIN_allOrds]
185 ]
186QED
187
188Definition preds_def:
189 preds (w : 'a ordinal) = { w0 | ordlt w0 w }
190End
191
192Theorem IN_preds[simp]:
193 x IN preds w <=> ordlt x w
194Proof
195 rw[preds_def]
196QED
197
198Theorem preds_11[simp]:
199 (preds w1 = preds w2) = (w1 = w2)
200Proof
201 rw[EQ_IMP_THM] >>
202 spose_not_then strip_assume_tac >>
203 `ordlt w1 w2 \/ ordlt w2 w1` by metis_tac [ordlt_trichotomy] >>
204 qpat_x_assum `x = y` mp_tac >> rw[EXTENSION, preds_def] >>
205 metis_tac [ordlt_REFL]
206QED
207
208Definition downward_closed_def:
209 downward_closed s <=>
210 !a b. a IN s /\ ordlt b a ==> b IN s
211End
212
213Theorem preds_downward_closed:
214 downward_closed (preds w)
215Proof
216 rw[downward_closed_def, preds_def] >> metis_tac [ordlt_TRANS]
217QED
218
219Theorem preds_bij:
220 BIJ preds UNIV (downward_closed DELETE UNIV)
221Proof
222 rw[BIJ_DEF, INJ_DEF, SURJ_DEF, preds_11] >>
223 fs[SPECIFICATION, preds_downward_closed] >>
224 rw[EXTENSION] >| [
225 metis_tac [IN_preds, ordlt_REFL],
226 metis_tac [IN_preds, ordlt_REFL],
227 qspec_then `\w. w NOTIN x` mp_tac ordlt_WF0 >> simp[] >>
228 qsuff_tac `?w. w NOTIN x`
229 >- metis_tac [downward_closed_def, ordlt_trichotomy] >>
230 fs[EXTENSION] >> metis_tac[]
231 ]
232QED
233
234Theorem preds_lt_PSUBSET:
235 ordlt w1 w2 <=> preds w1 PSUBSET preds w2
236Proof
237 simp[PSUBSET_DEF, SUBSET_DEF, preds_def, EQ_IMP_THM, EXTENSION] >> conj_tac
238 >- metis_tac [ordlt_TRANS, ordlt_REFL] >>
239 simp_tac (srw_ss() ++ CONJ_ss) [] >>
240 metis_tac [ordlt_REFL, ordlt_TRANS, ordlt_trichotomy]
241QED
242
243Theorem preds_wobound:
244 preds ord = elsOf (wobound ord allOrds)
245Proof
246 simp[EXTENSION, elsOf_wobound, preds_def, WIN_allOrds]
247QED
248
249Definition oleast_def:
250 $oleast (P:'a ordinal -> bool) = @x. P x /\ !y. y < x ==> ~P y
251End
252
253val _ = set_fixity "oleast" Binder
254
255Theorem oleast_intro:
256 !Q P. (?a. P a) /\ (!a. (!b. b < a ==> ~ P b) /\ P a ==> Q a) ==>
257 Q ($oleast P)
258Proof
259 rw[oleast_def] >> SELECT_ELIM_TAC >> conj_tac >-
260 (match_mp_tac ordlt_WF0 >> metis_tac[]) >>
261 rw[]
262QED
263
264Definition ordSUC_def:
265 ordSUC a = oleast b. a < b
266End
267Overload TC[local] = ``ordSUC``
268
269Definition fromNat_def:
270 (fromNat 0 = oleast a. T) /\
271 (fromNat (SUC n) = ordSUC (fromNat n))
272End
273Theorem fromNat_SUC[simp] = fromNat_def |> CONJUNCT2
274
275(* The numerals — 0o, 1o, and an unsuffixed numeral wherever the type
276 says ordinal — are available here and exported by ordinalTheory
277 rather than by this theory, as the notation above is. Everything
278 that declares a datatype loads this theory, because the datatype
279 package's construction counts in ordinals, and this theory's notation
280 would otherwise be everybody's: `+` would be ordinal addition, `<`
281 ordinal comparison, `TC` a successor rather than a transitive
282 closure, and a numeral whose type is not pinned an ordinal. *)
283val _ = temp_add_numeral_form (#"o", SOME "fromNat")
284
285(* recursion principles *)
286Theorem restrict_away[local]:
287 IMAGE (RESTRICT f $< (a:'a ordinal)) (preds a) = IMAGE f (preds a)
288Proof
289 rw[EXTENSION, relationTheory.RESTRICT_DEF] >> srw_tac[CONJ_ss][]
290QED
291
292Theorem preds_inj_univ:
293 preds (ord:'a ordinal) <<= univ(:'a inf)
294Proof
295 simp[preds_wobound] >>
296 qspec_then `ordinal_REP ord` mp_tac wellorder_ordinal_isomorphism >>
297 simp[mkOrdinal_REP] >> strip_tac >> imp_res_tac orderiso_SYM >>
298 pop_assum (strip_assume_tac o SIMP_RULE (srw_ss())[orderiso_thm]) >>
299 simp[cardleq_def] >> qexists_tac `f` >>
300 fs[BIJ_DEF, INJ_DEF]
301QED
302
303Theorem univ_ord_greater_cardinal:
304 ~(univ(:'a ordinal) <<= univ(:'a inf))
305Proof
306 strip_tac >>
307 `elsOf allOrds = univ(:'a ordinal)` by simp[elsOf_allOrds] >>
308 `elsOf (allOrds:'a ordinal wellorder) <<= univ(:'a inf)`
309 by simp[] >>
310 `?w:'a inf wellorder. orderiso (allOrds:'a ordinal wellorder) w`
311 by metis_tac [elsOf_cardeq_iso, cardleq_def] >>
312 `orderiso w (wobound (mkOrdinal w) allOrds)`
313 by simp[wellorder_ordinal_isomorphism] >>
314 `mkOrdinal w IN elsOf allOrds` by simp[elsOf_allOrds] >>
315 `orderlt (allOrds:'a ordinal wellorder) (allOrds:'a ordinal wellorder)`
316 by metis_tac [orderlt_def, orderiso_TRANS] >>
317 fs[orderlt_REFL]
318QED
319
320(* prints as 0 <= a *)
321Theorem ordlt_ZERO[simp]:
322 ~(a < 0)
323Proof
324 simp[fromNat_def] >> DEEP_INTRO_TAC oleast_intro >> simp[]
325QED
326
327Theorem preds_surj =
328 preds_bij |> SIMP_RULE (srw_ss()) [BIJ_DEF] |> CONJUNCT2
329 |> SIMP_RULE (srw_ss()) [SURJ_DEF] |> CONJUNCT2
330 |> REWRITE_RULE [SPECIFICATION];
331
332Theorem no_maximal_ordinal:
333 !a. ?b. a < b
334Proof
335 simp[preds_lt_PSUBSET] >> gen_tac >>
336 qabbrev_tac `P = preds a UNION {a}` >>
337 `a NOTIN preds a` by simp[ordlt_REFL] >>
338 `P <> univ(:'a ordinal)`
339 by (strip_tac >>
340 qsuff_tac `P <<= univ(:'a inf)` >-
341 metis_tac [univ_ord_greater_cardinal] >>
342 pop_assum (K ALL_TAC) >>
343 Cases_on `FINITE P` >- simp[FINITE_CLE_INFINITE] >>
344 `P = a INSERT preds a` by metis_tac [INSERT_SING_UNION,UNION_COMM] >>
345 `INFINITE (preds a)` by fs[] >>
346 `P =~ preds a` by metis_tac [cardeq_INSERT] >>
347 metis_tac [CARDEQ_CARDLEQ, cardeq_REFL, preds_inj_univ]) >>
348 `downward_closed P` by (simp[Abbr`P`, downward_closed_def] >>
349 metis_tac [ordlt_TRANS]) >>
350 `?b. preds b = P` by metis_tac [preds_surj] >>
351 qexists_tac `b` >> simp[Abbr`P`] >>
352 simp[PSUBSET_DEF, EXTENSION] >> metis_tac [ordlt_REFL]
353QED
354
355Theorem ordlt_SUC[simp]:
356 a < ordSUC a
357Proof
358 simp[ordSUC_def] >> DEEP_INTRO_TAC oleast_intro >> conj_tac
359 >- metis_tac[no_maximal_ordinal] >> simp[]
360QED
361
362Theorem ordSUC_ZERO[simp]:
363 ordSUC a <> 0
364Proof
365 simp[ordSUC_def] >> DEEP_INTRO_TAC oleast_intro >> conj_tac
366 >- metis_tac [ordlt_SUC] >>
367 rpt strip_tac >> fs[]
368QED
369
370Definition omax_def:
371 omax (s : 'a ordinal set) =
372 some a. maximal_elements s { (x,y) | x <= y } = {a}
373End
374
375Theorem ordle_lteq:
376 (a:'a ordinal) <= b <=> a < b \/ (a = b)
377Proof
378 metis_tac [ordlt_trichotomy, ordlt_REFL, ordlt_TRANS]
379QED
380
381Theorem omax_SOME:
382 (omax s = SOME a) <=> a IN s /\ !b. b IN s ==> b <= a
383Proof
384 simp[omax_def] >> DEEP_INTRO_TAC some_intro >> simp[] >>
385 conj_tac
386 >- (qx_gen_tac `b` >> simp[maximal_elements_def, EXTENSION] >>
387 strip_tac >> eq_tac
388 >- (strip_tac >> simp[] >> conj_tac >- metis_tac[] >>
389 qx_gen_tac `c` >> rpt strip_tac >>
390 metis_tac [ordlt_REFL, ordle_lteq]) >>
391 metis_tac[]) >>
392 simp[EXTENSION, maximal_elements_def] >> strip_tac >> Cases_on `a IN s` >>
393 simp[] >> first_assum (qspec_then `a` mp_tac) >>
394 disch_then (Q.X_CHOOSE_THEN `b` strip_assume_tac) >>
395 Cases_on `b = a`
396 >- (qpat_x_assum `P /\ Q <=/=> R` mp_tac >> simp[] >> metis_tac [ordle_lteq]) >>
397 fs[] >> metis_tac []
398QED
399
400Theorem omax_NONE:
401 (omax s = NONE) <=> !a. a IN s ==> ?b. b IN s /\ a < b
402Proof
403 simp[omax_def] >> DEEP_INTRO_TAC some_intro >>
404 simp[maximal_elements_def, EXTENSION] >>
405 metis_tac [ordle_lteq]
406QED
407
408Theorem omax_EMPTY[simp]:
409 omax {} = NONE
410Proof
411 simp[omax_NONE]
412QED
413
414Theorem ordlt_DISCRETE1:
415 ~(a < b /\ b < ordSUC a)
416Proof
417 simp[ordSUC_def] >> DEEP_INTRO_TAC oleast_intro >> conj_tac >-
418 metis_tac [ordlt_SUC] >> metis_tac [ordle_lteq]
419QED
420
421Theorem ordlt_SUC_DISCRETE:
422 a < ordSUC b <=> a < b \/ (a = b)
423Proof
424 Tactical.REVERSE eq_tac >- metis_tac [ordlt_TRANS, ordlt_SUC] >>
425 metis_tac [ordlt_trichotomy, ordlt_DISCRETE1]
426QED
427
428Theorem preds_omax_SOME_SUC:
429 (omax (preds a) = SOME b) <=> (a = b^+)
430Proof
431 simp[omax_SOME] >> eq_tac >> strip_tac
432 >- (qsuff_tac `a <= b^+ /\ b^+ <= a` >- metis_tac [ordlt_trichotomy] >>
433 rpt strip_tac >- metis_tac [ordlt_SUC] >>
434 metis_tac [ordlt_SUC_DISCRETE, ordlt_TRANS, ordlt_REFL]) >>
435 simp[ordlt_SUC_DISCRETE, ordle_lteq]
436QED
437
438Theorem omax_preds_SUC[simp]: omax (preds a^+) = SOME a
439Proof metis_tac [preds_omax_SOME_SUC]
440QED
441
442Overload islimit[local] = ``\a:'a ordinal. omax (preds a) = NONE``
443
444Theorem ord_RECURSION:
445 !(z:'b) (sf:'a ordinal -> 'b -> 'b) (lf:'a ordinal -> 'b set -> 'b).
446 ?h : 'a ordinal -> 'b.
447 (h 0 = z) /\
448 (!a. h a^+ = sf a (h a)) /\
449 !a. 0 < a /\ islimit a ==>
450 (h a = lf a (IMAGE h (preds a)))
451Proof
452 rpt gen_tac >>
453 qexists_tac `WFREC $< (\g x. if x = 0 then z
454 else
455 case omax (preds x) of
456 NONE => lf x (IMAGE g (preds x))
457 | SOME x0 => sf x0 (g x0)) ` >>
458 rpt conj_tac
459 >- simp[relationTheory.WFREC_THM, ordlt_WF]
460 >- simp[Once relationTheory.WFREC_THM, relationTheory.RESTRICT_DEF, SimpLHS,
461 ordlt_WF] >>
462 simp[relationTheory.WFREC_THM, ordlt_WF, restrict_away] >> qx_gen_tac `a` >>
463 strip_tac >> `a <> 0` by metis_tac [ordlt_REFL] >> simp[]
464QED
465
466Theorem ord_induction =
467 ordlt_WF0 |> Q.SPEC `P` |> CONV_RULE CONTRAPOS_CONV
468 |> CONV_RULE (BINOP_CONV NOT_EXISTS_CONV)
469 |> CONV_RULE (LAND_CONV (REWRITE_CONV [DE_MORGAN_THM] THENC
470 ONCE_REWRITE_CONV [DISJ_SYM] THENC
471 REWRITE_CONV [GSYM IMP_DISJ_THM]))
472 |> Q.INST [`P` |-> `\x. ~ P x`] |> BETA_RULE
473 |> REWRITE_RULE []
474 |> CONV_RULE (RAND_CONV (RENAME_VARS_CONV ["a"]))
475
476Theorem simple_ord_induction:
477 !P. P 0 /\ (!a. P a ==> P a^+) /\
478 (!a. (omax (preds a) = NONE) /\ 0 < a /\ (!b. b < a ==> P b) ==> P a) ==>
479 !a. P a
480Proof
481 gen_tac >> strip_tac >>
482 ho_match_mp_tac ord_induction >> qx_gen_tac `a` >>
483 Cases_on `a = 0` >> simp[] >>
484 `(omax (preds a) = NONE) \/ ?a0. omax (preds a) = SOME a0`
485 by metis_tac [option_CASES]
486 >- (`0 < a` by metis_tac [ordlt_ZERO, ordle_lteq] >> metis_tac[]) >>
487 fs[preds_omax_SOME_SUC]
488QED
489
490Theorem ordSUC_MONO[simp]:
491 a^+ < b^+ <=> a < b
492Proof
493 eq_tac >> spose_not_then strip_assume_tac
494 >- (fs[ordlt_SUC_DISCRETE]
495 >- (`(a = b) \/ b < a` by metis_tac [ordlt_trichotomy] >>
496 metis_tac [ordlt_TRANS, ordlt_REFL, ordlt_SUC]) >>
497 rw[] >> fs[ordlt_SUC]) >>
498 fs[ordlt_SUC_DISCRETE] >>
499 `b < a^+` by metis_tac [ordlt_trichotomy] >>
500 fs[ordlt_SUC_DISCRETE] >> metis_tac [ordlt_TRANS, ordlt_REFL]
501QED
502
503Theorem ordSUC_11[simp]:
504 (a^+ = b^+) <=> (a = b)
505Proof
506 simp[EQ_IMP_THM] >> strip_tac >> spose_not_then assume_tac >>
507 `a < b \/ b < a` by metis_tac [ordlt_trichotomy] >>
508 metis_tac [ordlt_REFL, ordSUC_MONO]
509QED
510
511Definition sup_def:
512 sup ordset = oleast a. a NOTIN BIGUNION (IMAGE preds ordset)
513End
514
515Theorem sup_thm:
516 (s: 'a ordinal set) <<= univ(:'a inf) ==>
517 !a. a < sup s <=> ?b. b IN s /\ a < b
518Proof
519 strip_tac >>
520 qabbrev_tac `apreds = BIGUNION (IMAGE preds s)` >>
521 `apreds <<= univ(:'a inf)`
522 by (qunabbrev_tac `apreds` >> match_mp_tac CARD_BIGUNION >>
523 dsimp[preds_inj_univ] >> metis_tac [cardleq_TRANS, IMAGE_cardleq]) >>
524 `apreds <> univ(:'a ordinal)` by metis_tac [univ_ord_greater_cardinal] >>
525 `downward_closed apreds`
526 by (dsimp[Abbr`apreds`, downward_closed_def] >>
527 metis_tac[ordlt_TRANS]) >>
528 `?a. preds a = apreds`
529 by (mp_tac preds_bij >> simp[BIJ_DEF, SURJ_DEF, SPECIFICATION]) >>
530 `sup s = a`
531 by (asm_simp_tac bool_ss [sup_def] >>
532 DEEP_INTRO_TAC oleast_intro >> conj_tac
533 >- (fs[EXTENSION] >> metis_tac[]) >>
534 Q.RM_ABBREV_TAC ‘apreds’ >>
535 simp[] >> qx_gen_tac `a'` >> strip_tac >>
536 qsuff_tac `a' <= a /\ a <= a'` >- metis_tac [ordlt_trichotomy] >>
537 rpt strip_tac >| [
538 `a IN apreds` by res_tac >> metis_tac [IN_preds, ordlt_REFL],
539 rw[] >> fs[]
540 ]) >>
541 simp[] >>
542 qx_gen_tac `b` >> rpt strip_tac >>
543 `b < a <=> b IN apreds` by metis_tac [IN_preds] >>
544 simp[Abbr`apreds`] >> metis_tac [IN_preds]
545QED
546
547val ordADD_def = new_specification(
548 "ordADD_def", ["ordADD"],
549 ord_RECURSION |> Q.ISPEC `b:'a ordinal` |> Q.SPEC `\(x:'a ordinal) r. r^+`
550 |> Q.SPEC `\x rs. sup rs`
551 |> SIMP_RULE (srw_ss()) []
552 |> Q.GEN `b`
553 |> CONV_RULE SKOLEM_CONV)
554val _ = export_rewrites ["ordADD_def"]
555Overload "+"[local] = ``ordADD``
556
557Theorem sup_preds_omax_NONE:
558 (omax (preds a) = NONE) <=> (sup (preds a) = a)
559Proof
560 simp[omax_NONE, sup_def] >> DEEP_INTRO_TAC oleast_intro >> simp[] >>
561 simp_tac(srw_ss() ++ DNF_ss) [impI] >>
562 qexists_tac `a` >> conj_tac >- simp[ordle_lteq] >>
563 qx_gen_tac `c` >> strip_tac >> Tactical.REVERSE eq_tac
564 >- (rw[] >> metis_tac[]) >>
565 strip_tac >> qsuff_tac `c <= a /\ a <= c` >- metis_tac [ordlt_trichotomy] >>
566 metis_tac [ordlt_TRANS, ordlt_REFL]
567QED
568
569Theorem ordADD_0L[simp]:
570 !a:'a ordinal. 0 + a = a
571Proof
572 ho_match_mp_tac simple_ord_induction >> simp[] >> qx_gen_tac `a` >>
573 strip_tac >>
574 `IMAGE ($+ 0) (preds a) = preds a`
575 by (rpt (asm_simp_tac (srw_ss() ++ CONJ_ss)[EXTENSION])) >>
576 fs[sup_preds_omax_NONE]
577QED
578
579Theorem ordADD_fromNat[simp]:
580 ordADD (&n) (&m) = &(n + m)
581Proof
582 Induct_on `m` >> simp[arithmeticTheory.ADD_CLAUSES]
583QED
584
585Theorem ordleq0[simp]:
586 (x:'a ordinal) <= 0 <=> (x = 0)
587Proof
588 eq_tac >> simp[ordle_lteq]
589QED
590
591Theorem sup_EQ_0:
592 s:'a ordinal set <<= univ(:'a inf) ==> (sup s = 0 <=> s = {} \/ s = {0})
593Proof
594 strip_tac >>
595 qspec_then `0` (mp_tac o Q.AP_TERM `$~`) (sup_thm |> UNDISCH_ALL) >>
596 simp_tac pure_ss [NOT_EXISTS_THM] >> simp[impI] >>
597 disch_then (K ALL_TAC) >> simp[EXTENSION] >> metis_tac[]
598QED
599
600Theorem fromNat_11[simp]:
601 !x y. (&x:'a ordinal = &y) = (x = y)
602Proof
603 Induct >- (Cases >> simp[]) >> Cases >> simp[]
604QED
605
606Theorem ORD_ONE[simp]:
607 0^+ = 1
608Proof
609 simp_tac bool_ss [GSYM fromNat_SUC] >> simp[]
610QED
611
612Theorem ordSUC_NUMERAL[simp]:
613 (&NUMERAL n)^+ = &(NUMERAL n + 1)
614Proof
615 simp[GSYM arithmeticTheory.ADD1]
616QED
617
618Theorem ordZERO_ltSUC[simp]:
619 0 < x^+
620Proof
621 metis_tac [ordSUC_ZERO, ordlt_ZERO, ordlt_trichotomy]
622QED
623
624Theorem IFF_ZERO_lt:
625 (x:'a ordinal <> 0 <=> 0 < x) /\ (1 <= x <=> 0 < x)
626Proof
627 REWRITE_TAC [GSYM ORD_ONE] >> simp[ordlt_SUC_DISCRETE] >>
628 metis_tac [ordlt_trichotomy, ordlt_ZERO]
629QED
630
631Theorem islimit_SUC[simp]:
632 islimit x^+ <=> F
633Proof
634 simp[omax_NONE, impI, ordlt_SUC_DISCRETE] >>
635 metis_tac[ordle_lteq]
636QED
637
638Theorem preds_0[simp]:
639 preds 0 = {}
640Proof
641 simp[preds_def]
642QED
643
644Theorem preds_EQ_EMPTY[simp]:
645 preds x = {} <=> x = 0
646Proof
647 simp[EQ_IMP_THM] >> simp[EXTENSION] >>
648 disch_then (qspec_then `0` mp_tac) >> simp[]
649QED
650
651Theorem islimit_fromNat[simp]:
652 islimit &x <=> x = 0
653Proof
654 Cases_on `x` >> simp[]
655QED
656
657Theorem ordle_ANTISYM:
658 a <= b /\ b <= a ==> (a = b)
659Proof
660 metis_tac [ordlt_trichotomy]
661QED
662
663Theorem ordle_TRANS:
664 !x y z. (x:'a ordinal) <= y /\ y <= z ==> x <= z
665Proof
666 metis_tac [ordlt_TRANS, ordle_lteq]
667QED
668
669Theorem ordlet_TRANS:
670 !x y z. (x:'a ordinal) <= y /\ y < z ==> x < z
671Proof
672 metis_tac [ordle_lteq, ordlt_TRANS]
673QED
674Theorem ordlte_TRANS:
675 !x y z. (x:'a ordinal) < y /\ y <= z ==> x < z
676Proof
677 metis_tac [ordle_lteq, ordlt_TRANS]
678QED
679
680Theorem ubsup_thm:
681 (!a. a IN s ==> a < b) ==> !c. c < sup s <=> ?d. d IN s /\ c < d
682Proof
683 strip_tac >> simp[sup_def] >> gen_tac >> DEEP_INTRO_TAC oleast_intro >>
684 dsimp[impI] >>
685 qexists_tac `b` >> conj_tac >- metis_tac [ordlt_TRANS, ordlt_REFL] >>
686 qx_gen_tac `a` >> strip_tac >> eq_tac >- metis_tac[] >>
687 disch_then (Q.X_CHOOSE_THEN `d` strip_assume_tac) >>
688 `d <= a`by metis_tac[] >> fs[ordle_lteq] >> rw[] >> metis_tac [ordlt_TRANS]
689QED
690
691Theorem sup_eq_max:
692 (!b. b IN s ==> b <= a) /\ a IN s ==> sup s = a
693Proof
694 strip_tac >>
695 `!b. b IN s ==> b < a^+` by fs[ordlt_SUC_DISCRETE, ordle_lteq] >>
696 pop_assum (assume_tac o MATCH_MP ubsup_thm) >>
697 `a <= sup s` by metis_tac [ordlt_REFL] >>
698 `sup s <= a` by simp[impI] >>
699 metis_tac [ordle_ANTISYM]
700QED
701
702Theorem sup_EMPTY[simp]:
703 sup {} = 0
704Proof
705 simp[sup_def] >> DEEP_INTRO_TAC oleast_intro >> simp[] >>
706 qx_gen_tac `a` >> disch_then (qspec_then `0` mp_tac) >>
707 simp[ordle_lteq]
708QED
709
710Theorem sup_SING[simp]:
711 sup {a} = a
712Proof
713 simp[sup_def] >> DEEP_INTRO_TAC oleast_intro >> simp[] >> conj_tac >-
714 (qexists_tac `a` >> simp[]) >>
715 simp[] >> qx_gen_tac `b` >> rw[ordle_lteq] >>
716 metis_tac [ordlt_REFL]
717QED
718
719Theorem sup_preds_SUC:
720 sup (preds a^+) = a
721Proof
722 simp[sup_def] >> DEEP_INTRO_TAC oleast_intro >> simp[] >> conj_tac >-
723 (qsuff_tac `?b. !x. b IN preds x ==> a^+ <= x ` >- metis_tac[] >>
724 simp[] >> qexists_tac `a^+` >> simp[ordle_lteq]) >>
725 qx_gen_tac `b` >> simp_tac (srw_ss() ++ DNF_ss) [] >>
726 strip_tac >>
727 `!d. b < d ==> a^+ <= d` by metis_tac [IN_preds] >>
728 qsuff_tac `b <= a /\ a <= b` >- metis_tac [ordlt_trichotomy] >>
729 rpt strip_tac
730 >- (`?x. a < x /\ x < a^+` by metis_tac [] >>
731 fs[ordlt_SUC_DISCRETE] >> metis_tac [ordlt_REFL, ordlt_TRANS]) >>
732 res_tac >> fs[ordlt_SUC]
733QED
734
735Theorem preds_ordSUC:
736 preds a^+ = a INSERT preds a
737Proof
738 simp[EXTENSION, ordlt_SUC_DISCRETE] >> metis_tac[]
739QED
740
741Theorem preds_nat:
742 preds (&n) = IMAGE fromNat (count n)
743Proof
744 Induct_on ‘n’ >> simp[preds_ordSUC, COUNT_SUC]
745QED
746
747Theorem islimit_SUC_lt:
748 islimit b /\ a < b ==> a^+ < b
749Proof
750 fs[omax_NONE] >> metis_tac [ordlt_SUC_DISCRETE, ordlt_trichotomy, ordle_lteq]
751QED
752
753Theorem predimage_sup_thm:
754 !b:'a ordinal.
755 b < sup (IMAGE f (preds (a:'a ordinal))) <=> ?d. d < a /\ b < f d
756Proof
757 match_mp_tac (sup_thm |> Q.INST [`s` |-> `IMAGE f (preds (a:'b ordinal))`]
758 |> SIMP_RULE (srw_ss() ++ DNF_ss) []) >>
759 metis_tac [cardleq_TRANS, IMAGE_cardleq, preds_inj_univ]
760QED
761
762Theorem lemma[local]:
763 !c a b:'a ordinal. a < b /\ b < a + c ==> ?d. a + d = b
764Proof
765 ho_match_mp_tac simple_ord_induction >> simp[] >> rpt conj_tac
766 >- metis_tac [ordlt_TRANS, ordlt_REFL]
767 >- (simp[ordlt_SUC_DISCRETE] >> metis_tac[]) >>
768 simp[predimage_sup_thm]
769QED
770
771Theorem lt_suppreds =
772 predimage_sup_thm |> Q.INST [`f` |-> `\x. x`] |> SIMP_RULE (srw_ss()) []
773
774Theorem ordlt_CANCEL_ADDR[simp]:
775 !(b:'a ordinal) a. a < a + b <=> 0 < b
776Proof
777 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
778 >- (qx_gen_tac `b` >> strip_tac >> qx_gen_tac `a` >>
779 Cases_on `b = 0` >- simp[] >>
780 match_mp_tac ordlt_TRANS >> qexists_tac `a^+` >> simp[] >>
781 spose_not_then strip_assume_tac >> fs[ordle_lteq]) >>
782 simp_tac (srw_ss() ++ CONJ_ss)[predimage_sup_thm] >> rpt strip_tac >>
783 simp[GSYM lt_suppreds] >> fs[sup_preds_omax_NONE]
784QED
785
786Theorem ordlt_CANCEL_ADDL[simp]:
787 a + b < a <=> F
788Proof
789 simp[ordle_lteq] >> Cases_on `0 < b` >> simp[] >>
790 fs[ordleq0]
791QED
792
793fun mklesup th =
794 th |> UNDISCH_ALL |> Q.SPEC `sup s`
795 |> SIMP_RULE (srw_ss()) [] |> REWRITE_RULE [impI] |> DISCH_ALL
796
797Theorem Unum_cle_Uinf:
798 univ(:num) <<= univ(:'a inf)
799Proof
800 simp[cardleq_def] >> qexists_tac `INL` >> simp[INJ_INL]
801QED
802
803Theorem csup_thm:
804 countable (s : 'a ordinal set) ==> !b. b < sup s <=> ?d. d IN s /\ b < d
805Proof
806 simp[countable_thm] >>
807 metis_tac [sup_thm, cardleq_def, Unum_cle_Uinf, cardleq_TRANS]
808QED
809
810(* |- countable s ==> !d. d IN s ==> d <= sup s *)
811Theorem csup_lesup = mklesup csup_thm
812
813fun mksuple th =
814 th |> UNDISCH_ALL |> Q.SPEC `b` |> AP_TERM ``$~``
815 |> CONV_RULE (RAND_CONV (SIMP_CONV (srw_ss()) []))
816 |> REWRITE_RULE [impI]
817 |> DISCH_ALL
818
819Theorem csup_suple = mksuple csup_thm
820
821
822Theorem ordADD_CANCEL_LEMMA0[local]:
823 a = a + c <=> c = 0
824Proof
825 Cases_on `c = 0` >> simp[] >>
826 qsuff_tac `a < a + c` >- metis_tac[ordlt_REFL] >> simp[] >>
827 spose_not_then strip_assume_tac >> fs[ordle_lteq]
828QED
829Theorem ordADD_CANCEL1[simp] =
830 CONJ (GEN_ALL ordADD_CANCEL_LEMMA0)
831 (ordADD_CANCEL_LEMMA0 |> CONV_RULE (LAND_CONV (REWR_CONV EQ_SYM_EQ))
832 |> GEN_ALL)
833
834Theorem ordADD_MONO:
835 !b:'a ordinal a c. a < b ==> c + a < c + b
836Proof
837 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
838 >- (ntac 2 strip_tac >> simp[ordlt_SUC_DISCRETE] >> rw[] >> rw[]) >>
839 qx_gen_tac `b` >> strip_tac >> simp[predimage_sup_thm] >>
840 map_every qx_gen_tac [`a`, `c`] >> strip_tac >>
841 `?d. d < b /\ a < d`
842 by (simp[GSYM lt_suppreds] >> fs[sup_preds_omax_NONE]) >>
843 metis_tac[]
844QED
845
846Theorem ordlt_CANCEL[simp]:
847 !b a (c:'a ordinal). c + a < c + b <=> a < b
848Proof
849 simp[EQ_IMP_THM, ordADD_MONO] >> rpt strip_tac >>
850 metis_tac[ordlt_trichotomy, ordlt_REFL, ordlt_TRANS, ordADD_MONO]
851QED
852
853Theorem ordADD_RIGHT_CANCEL[simp]:
854 !b a c. ((a:'a ordinal) + b = a + c) <=> (b = c)
855Proof
856 metis_tac[ordlt_trichotomy, ordADD_MONO, ordlt_REFL]
857QED
858
859Theorem leqLEFT_CANCEL[simp]:
860 !x a. x <= a + x
861Proof
862 ho_match_mp_tac simple_ord_induction >> rpt conj_tac >- simp[] >- simp[] >>
863 qx_gen_tac `x` >> strip_tac >>
864 qx_gen_tac `a` >> strip_tac >>
865 `?b. a + x < b /\ b < x` by metis_tac[omax_NONE, IN_preds] >>
866 `b <= a + b` by metis_tac[] >>
867 `a + x < a + b` by metis_tac [ordle_lteq, ordlt_TRANS] >>
868 fs[] >> metis_tac[ordlt_TRANS, ordlt_REFL]
869QED
870
871Theorem ordlt_EXISTS_ADD:
872 !a b:'a ordinal. a < b <=> ?c. c <> 0 /\ b = a + c
873Proof
874 simp_tac (srw_ss() ++ DNF_ss) [EQ_IMP_THM] >> Tactical.REVERSE conj_tac
875 >- metis_tac[ordlt_trichotomy, ordlt_ZERO] >>
876 map_every qx_gen_tac [`a`, `b`] >> strip_tac >>
877 `b <= a + b` by simp[] >> fs[ordle_lteq]
878 >- (`?c. a + c = b` by metis_tac[lemma] >> rw[] >> strip_tac >> fs[]) >>
879 qexists_tac `b` >> simp[] >> strip_tac >> fs[]
880QED
881
882Theorem ordle_EXISTS_ADD:
883 !a b:'a ordinal. a <= b <=> ?c. b = a + c
884Proof
885 simp[ordle_lteq] >> metis_tac [ordlt_EXISTS_ADD, ordADD_def]
886QED
887
888
889(* ----------------------------------------------------------------------
890 Results about cardinalities of ordinal predecessor sets
891 ---------------------------------------------------------------------- *)
892
893Definition omega_def:
894 omega = sup { fromNat i | T }
895End
896Overload "ω"[local] = ``omega``
897
898Definition csuc_def:
899 csuc (a : 'a ordinal) =
900 oleast (b: ('a + num -> bool) ordinal). preds a <</= preds b
901End
902
903Definition cardSUC_def:
904 cardSUC (s : 'a set) = preds $ csuc (oleast a:'a ordinal. preds a =~ s)
905End
906
907Definition dclose_def: dclose s = { x:'a ordinal | ?y. y IN s /\ x < y }
908End
909
910Theorem preds_sup:
911 s <<= univ(:'a inf) ==> (preds (sup s:'a ordinal) = dclose s)
912Proof
913 simp[EXTENSION, sup_thm, dclose_def]
914QED
915
916Theorem bumpUNIV_cardlt:
917 univ(:num + 'a) <</= univ(:num + ('a + num -> bool))
918Proof
919 simp[disjUNION_UNIV] >> Cases_on ‘INFINITE univ(:'a)’
920 >- (‘univ(:num) +_c univ(:'a) =~ univ(:'a)’
921 by (irule cardleq_ANTISYM >>
922 gs[INFINITE_Unum,CARD_ADD_ABSORB_LE, CARD_LE_ADDL]) >>
923 ‘univ(:'a) <</= univ(:num) +_c univ(:'a + num -> bool)’
924 suffices_by metis_tac[CARD_LT_CONG, cardeq_REFL]>>
925 resolve_then (Pos hd) irule
926 CANTOR_THM_UNIV cardlt_leq_trans >>
927 qspec_then ‘univ(:num)’
928 (fn th =>
929 resolve_then (Pos hd) irule th
930 cardleq_TRANS)
931 CARD_LE_ADDL >>
932 irule CARD_LE_ADD >> simp[] >>
933 simp[cardleq_def, INJ_IFF] >>
934 qexists_tac ‘IMAGE INL’ >> simp[IMAGE_11]) >>
935 irule CARD_ADD2_ABSORB_LT >> simp[CARD_ADD_FINITE_EQ] >>
936 conj_tac
937 >- (resolve_then (Pos hd) irule
938 CANTOR_THM_UNIV cardlt_leq_trans >>
939 simp[cardleq_def, INJ_IFF] >>
940 qexists_tac ‘λs. INR (IMAGE INR s)’ >>
941 simp[IMAGE_11]) >>
942 gs[FINITE_CARD_LT] >>
943 pop_assum (C (resolve_then (Pos hd) irule)
944 cardlt_leq_trans) >>
945 simp[CARD_LE_ADDR]
946QED
947
948Theorem cardeq_ordinals_exist:
949 (s:'b set) <<= univ(:num + 'a) ==>
950 ?a:'a ordinal. preds a =~ s
951Proof
952 strip_tac >>
953 qspec_then ‘s’ (qx_choose_then ‘w1’ assume_tac) allsets_wellorderable >>
954 gvs[cardleq_def] >>
955 drule_then (qx_choose_then ‘w2’ assume_tac) elsOf_cardeq_iso>>
956 qspec_then ‘w2’ assume_tac wellorder_ordinal_isomorphism >>
957 qexists_tac ‘mkOrdinal w2’ >>
958 simp[preds_wobound] >> gs[orderiso_thm, cardeq_def] >>
959 metis_tac[BIJ_SYM, BIJ_COMPOSE]
960QED
961
962Theorem suple_thm:
963 !b s:'a ordinal set. s <<= univ(:'a inf) /\ b IN s ==> b <= sup s
964Proof
965 metis_tac [sup_thm, ordlt_REFL]
966QED
967
968Theorem cardinality_bump_exists:
969 !x : 'a ordinal. ?y: ('a + num -> bool) ordinal. cardlt (preds x) (preds y)
970Proof
971 gen_tac >>
972 irule_at (Pos hd)
973 (CARD_LET_TRANS |> Q.ISPEC ‘preds x’
974 |> Q.ISPEC ‘univ(:num + 'a)’) >>
975 simp[preds_inj_univ] >>
976 qexists_tac ‘sup { a | preds a =~ univ(:num + 'a)}’>>
977 qmatch_abbrev_tac ‘UNIV <</= preds (sup ords)’ >>
978 strip_tac >>
979 qabbrev_tac ‘bigU = univ(:num + ('a + num -> bool))’ >>
980 ‘INFINITE bigU /\ !x. x IN bigU’ by simp[Abbr‘bigU’] >>
981 ‘univ(:num + 'a) <</= bigU’ by simp[Abbr‘bigU’, bumpUNIV_cardlt] >>
982 ‘omax ords = NONE’
983 by (simp[omax_NONE] >> CCONTR_TAC >> gs[] >>
984 rename [‘mx IN ords’] >> ‘mx < ordSUC mx’ by simp[] >>
985 ‘ordSUC mx NOTIN ords’ by metis_tac[] >> pop_assum mp_tac >>
986 gs[Abbr‘ords’, preds_ordSUC] >>
987 ‘INFINITE univ(:num+'a)’ by simp[] >>
988 ‘INFINITE (preds mx)’ by metis_tac[CARD_INFINITE_CONG] >>
989 metis_tac[cardeq_INSERT, cardeq_SYM, cardeq_TRANS]) >>
990 ‘ords <<= bigU’ (* can't prove much about sup ords without this *)
991 by (CCONTR_TAC >> gs[cardlt_lenoteq] >>
992 ‘?f. INJ f bigU ords’ by metis_tac[cardleq_def] >>
993 ‘(!u. preds (f u) =~ univ(:num + 'a)) /\
994 (!u v. f u = f v <=> u = v)’
995 by fs[INJ_IFF, Abbr‘ords’] >>
996 qabbrev_tac ‘fU = IMAGE f bigU’ >>
997 ‘fU =~ bigU’
998 by (simp[Abbr‘fU’] >> gs[INJ_DEF, CARD_EQ_IMAGE]) >>
999 ‘fU <<= univ(:num+('a+num->bool))’
1000 by metis_tac[cardleq_REFL, CARD_LE_CONG, cardeq_REFL] >>
1001 drule_then assume_tac sup_thm >>
1002 reverse (Cases_on ‘omax fU’)
1003 >- (gs[omax_SOME] >> rename [‘mx IN fU’] >>
1004 ‘?u. f u = mx’ by gs[Abbr‘fU’] >>
1005 ‘ordSUC mx IN ords’
1006 by (gs[Abbr‘ords’, preds_ordSUC] >>
1007 ‘preds mx =~ univ(:num + 'a)’ by metis_tac[] >>
1008 ‘INFINITE univ(:num + 'a)’ by simp[] >>
1009 ‘INFINITE (preds mx)’ by metis_tac[CARD_INFINITE_CONG] >>
1010 metis_tac[cardeq_INSERT, cardeq_SYM, cardeq_TRANS]) >>
1011 pop_assum mp_tac >> simp[Abbr‘ords’] >> strip_tac >>
1012 ‘fU <<= preds $ ordSUC mx’
1013 by (simp[preds_sup, cardleq_def, INJ_IFF] >>
1014 qexists_tac ‘I’>> simp[] >> rpt strip_tac >>
1015 irule ordlet_TRANS >> qexists_tac ‘mx’ >> simp[]) >>
1016 ‘bigU <<= univ(:num + 'a)’ by metis_tac[CARD_LE_CONG] >>
1017 metis_tac[cardleq_ANTISYM]) >>
1018 Cases_on ‘sup fU IN ords’
1019 >- (‘fU <<= preds (sup fU)’
1020 by (simp[preds_sup,cardleq_def,INJ_IFF] >>
1021 qexists_tac ‘I’ >> simp[dclose_def] >> gs[omax_NONE]) >>
1022 ‘preds (sup fU) =~ univ(:num + 'a)’ by gs[Abbr‘ords’] >>
1023 ‘bigU <<= univ(:num + 'a)’ by metis_tac[CARD_LE_CONG] >>
1024 metis_tac[cardleq_ANTISYM]) >>
1025 ‘!a. a IN ords ==> a < sup fU’
1026 by (simp[] >> CCONTR_TAC >> gs[] >>
1027 ‘sup fU < a’ by metis_tac[sup_thm, ordle_lteq] >>
1028 ‘preds (sup fU) SUBSET preds a’
1029 by metis_tac[PSUBSET_DEF, preds_lt_PSUBSET] >>
1030 ‘fU <<= preds (sup fU)’
1031 by (simp[preds_sup,cardleq_def,INJ_IFF] >>
1032 qexists_tac ‘I’ >> simp[dclose_def] >> gs[omax_NONE])>>
1033 ‘preds a =~ univ(:num + 'a)’ by gs[Abbr‘ords’] >>
1034 ‘fU <<= univ(:num + 'a)’
1035 by metis_tac[cardleq_TRANS, CARD_LE_CONG, cardeq_REFL,
1036 SUBSET_CARDLEQ] >>
1037 ‘bigU <<= univ(:num + 'a)’
1038 by metis_tac[CARD_LE_CONG, cardeq_REFL]>>
1039 metis_tac[cardleq_ANTISYM]) >>
1040 ‘sup fU = sup ords’
1041 by (irule ordle_ANTISYM >> drule_then assume_tac ubsup_thm >>
1042 simp[]>> rw[] >- metis_tac[ordle_lteq] >>
1043 simp[ordle_lteq] >> rename [‘a NOTIN fU \/ _’] >>
1044 Cases_on ‘a IN fU’ >> simp[] >> gs[omax_NONE] >>
1045 ‘a IN ords’ suffices_by metis_tac[] >> gs[INJ_IFF, Abbr‘fU’])>>
1046 ‘fU <<= preds (sup ords)’
1047 by (simp[preds_sup,cardleq_def,INJ_IFF] >>
1048 qexists_tac ‘I’ >> simp[dclose_def] >> gs[omax_NONE])>>
1049 ‘bigU <<= univ(:num + 'a)’
1050 by metis_tac[CARD_LE_CONG, cardeq_REFL, cardleq_TRANS,
1051 cardeq_SYM] >>
1052 metis_tac[cardleq_ANTISYM]) >>
1053 qpat_x_assum ‘preds (sup _) <<= _’ mp_tac >> simp[] >>
1054 ‘sup ords NOTIN ords’
1055 by (gs[omax_NONE] >> strip_tac >> first_x_assum drule >>
1056 metis_tac[suple_thm]) >>
1057 ‘~(univ(:num + 'a) =~ preds (sup ords))’
1058 by (gs[Abbr‘ords’] >> metis_tac[cardeq_SYM]) >>
1059 simp[CARD_LT_LE] >>
1060 ‘?a. a IN ords’ suffices_by
1061 (strip_tac >>
1062 ‘a < sup ords’ by (simp[sup_thm] >> gs[omax_NONE]) >>
1063 ‘preds a SUBSET preds (sup ords)’
1064 by metis_tac[preds_lt_PSUBSET, PSUBSET_DEF] >>
1065 ‘preds a =~ univ(:num + 'a)’ by gs[Abbr‘ords’] >>
1066 metis_tac[CARD_LE_SUBSET, CARD_LE_CONG, cardeq_SYM, cardeq_REFL]) >>
1067 simp[Abbr‘ords’] >> irule cardeq_ordinals_exist >>
1068 simp[cardleq_lteq, Abbr‘bigU’]
1069QED
1070
1071Theorem ZERO_LT_csuc[simp]:
1072 0 < csuc a /\ csuc a <> 0
1073Proof
1074 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
1075 simp[cardinality_bump_exists] >> rpt strip_tac >>
1076 CCONTR_TAC >> gvs[]
1077QED
1078
1079Theorem lt_csuc:
1080 x < csuc y <=> preds x <<= preds y
1081Proof
1082 simp[csuc_def] >>
1083 DEEP_INTRO_TAC oleast_intro >> rpt strip_tac
1084 >- metis_tac[cardinality_bump_exists] >> gs[] >> simp[EQ_IMP_THM] >>
1085 strip_tac >> CCONTR_TAC >> qpat_x_assum ‘a <= x’ mp_tac >>
1086 PURE_REWRITE_TAC[ordle_lteq] >> rpt strip_tac >> gvs[] >>
1087 gs[preds_lt_PSUBSET] >>
1088 ‘preds a <<= preds x’ by metis_tac[CARD_LE_SUBSET, PSUBSET_DEF] >>
1089 metis_tac[cardlt_REFL, CARD_LTE_TRANS, CARD_LE_TRANS]
1090QED
1091
1092Theorem omax_INSERT:
1093 omax (x INSERT y) = if (!e. e IN y ==> e <= x) then SOME x
1094 else omax y
1095Proof
1096 Cases_on‘omax y’ >>
1097 gs[omax_SOME, omax_NONE, AllCaseEqs(), DISJ_IMP_THM, FORALL_AND_THM,
1098 RIGHT_AND_OVER_OR, EXISTS_OR_THM]
1099 >- metis_tac[] >>
1100 rename [‘_ \/ _ /\ a <= b’] >> Cases_on ‘b <= a’
1101 >- metis_tac[ordle_TRANS] >> gs[] >> metis_tac[ordle_lteq]
1102QED
1103
1104Theorem FINITE_omax_IS_SOME:
1105 s <> {} /\ FINITE s ==> ?a. omax s = SOME a
1106Proof
1107 Induct_on ‘FINITE’ >> simp[omax_INSERT, AllCaseEqs(), EXISTS_OR_THM] >>
1108 rw[] >> simp[PULL_EXISTS] >> Cases_on ‘s = {}’ >> simp[] >>
1109 gs[omax_SOME] >>
1110 Cases_on ‘e < a’ >- metis_tac[] >>
1111 metis_tac[ordle_TRANS]
1112QED
1113
1114Theorem FINITE_preds:
1115 FINITE (preds a) <=> ?n. a = &n
1116Proof
1117 simp[EQ_IMP_THM, PULL_EXISTS, preds_nat] >>
1118 qid_spec_tac ‘a’ >> ho_match_mp_tac simple_ord_induction >>
1119 simp[preds_ordSUC] >> rw[] >> gs[]
1120 >- simp[GSYM fromNat_SUC, Excl "fromNat_SUC"] >>
1121 ‘preds a <> {}’ by (strip_tac >> gs[]) >>
1122 drule_all FINITE_omax_IS_SOME >> simp[]
1123QED
1124
1125Theorem ord_CASES:
1126 !a. (a = 0) \/ (?a0. a = a0^+) \/ (0 < a /\ islimit a)
1127Proof
1128 gen_tac >> Cases_on `a = 0` >- simp[] >>
1129 `0 < a` by metis_tac [ordlt_trichotomy, ordlt_ZERO] >>
1130 Cases_on `omax (preds a)` >> simp[] >>
1131 fs[preds_omax_SOME_SUC]
1132QED
1133
1134Theorem ordlt_fromNat:
1135 !n (x:'a ordinal). x < &n <=> ?m. (x = &m) /\ m < n
1136Proof
1137 Induct >>
1138 dsimp [ordlt_SUC_DISCRETE, numLib.DECIDE ``m < SUC n <=> m < n \/ (m = n)``]
1139QED
1140
1141Theorem fromNat_ordlt[simp]:
1142 (&n:'a ordinal < &m) <=> (n < m)
1143Proof
1144 simp[ordlt_fromNat]
1145QED
1146
1147Theorem allNats_dwardclosedetc[local]:
1148 downward_closed { fromNat i : 'a ordinal | T } /\
1149 { fromNat i | T } <> univ(:'a ordinal)
1150Proof
1151 simp[downward_closed_def] >> conj_tac
1152 >- (map_every qx_gen_tac [`a`, `b`] >>
1153 disch_then (CONJUNCTS_THEN2 (Q.X_CHOOSE_THEN `i` assume_tac)
1154 assume_tac) >>
1155 rw[] >> fs[ordlt_fromNat]) >>
1156 qsuff_tac `{&i : 'a ordinal | T} <<= univ(:'a inf)`
1157 >- metis_tac [univ_ord_greater_cardinal] >>
1158 simp[cardleq_def] >> qexists_tac `\a. INL (@n. &n = a)` >>
1159 simp[INJ_DEF] >> rw[] >> fs[]
1160QED
1161
1162Theorem preds_sup_thm:
1163 downward_closed s /\ s <> univ(:'a ordinal) ==>
1164 !b. b < sup s <=> ?d. d IN s /\ b < d
1165Proof
1166 strip_tac >>
1167 qspec_then `s` mp_tac preds_surj >> simp[] >>
1168 disch_then (Q.X_CHOOSE_THEN `a` ASSUME_TAC) >>
1169 `(omax s = NONE) \/ ?b. omax s = SOME b` by (Cases_on `omax s` >> simp[])
1170 >- (`sup s = a`
1171 by (simp[sup_def] >> DEEP_INTRO_TAC oleast_intro >>
1172 dsimp[impI] >> qexists_tac `a` >> conj_tac >- rw[ordle_lteq] >>
1173 qx_gen_tac `b` >> rw[] >>
1174 qsuff_tac `b <= a /\ a <= b` >- metis_tac [ordlt_trichotomy] >>
1175 rpt strip_tac >- metis_tac [ordlt_TRANS, ordlt_REFL] >>
1176 fs[omax_NONE] >> metis_tac[]) >>
1177 pop_assum SUBST1_TAC >> rw[] >> fs[omax_NONE] >>
1178 metis_tac[ordlt_TRANS]) >>
1179 `a = b^+` by (rw[] >> fs[preds_omax_SOME_SUC]) >> qx_gen_tac `d` >> rw[] >>
1180 simp[sup_preds_SUC] >> eq_tac >- (strip_tac >> qexists_tac `b` >> simp[]) >>
1181 simp[ordlt_SUC_DISCRETE] >>
1182 disch_then (Q.X_CHOOSE_THEN `c` strip_assume_tac) >- metis_tac[ordlt_TRANS] >>
1183 rw[]
1184QED
1185
1186Theorem preds_lesup = mklesup preds_sup_thm
1187Theorem preds_suple = mksuple preds_sup_thm
1188
1189val lt_omega0 =
1190 MATCH_MP preds_sup_thm allNats_dwardclosedetc
1191 |> SIMP_RULE (srw_ss() ++ DNF_ss) [SYM omega_def, ordlt_fromNat]
1192
1193Theorem lt_omega:
1194 !a. a < omega <=> ?m. a = &m
1195Proof
1196 simp_tac (srw_ss() ++ DNF_ss) [lt_omega0, EQ_IMP_THM] >> qx_gen_tac `n` >>
1197 qexists_tac `SUC n` >> simp[]
1198QED
1199
1200Theorem fromNat_lt_omega[simp]:
1201 !n. &n < omega
1202Proof
1203 simp[lt_omega]
1204QED
1205
1206Theorem fromNat_eq_omega[simp]:
1207 !n. &n <> omega
1208Proof
1209 metis_tac [ordlt_REFL, fromNat_lt_omega]
1210QED
1211
1212Theorem omax_preds_omega:
1213 omax (preds omega) = NONE
1214Proof
1215 simp_tac (srw_ss() ++ DNF_ss) [omax_NONE, lt_omega] >> qx_gen_tac `m` >>
1216 qexists_tac `SUC m` >> simp[]
1217QED
1218Theorem omega_islimit = omax_preds_omega
1219
1220Theorem ordADD_fromNat_omega:
1221 &n + omega = omega
1222Proof
1223 simp[ordADD_def,omax_preds_omega] >>
1224 `!a. a IN IMAGE ($+ (&n)) (preds omega) ==> a < omega` by dsimp[lt_omega] >>
1225 pop_assum (assume_tac o MATCH_MP ubsup_thm) >>
1226 match_mp_tac ordle_ANTISYM >> simp[] >> conj_tac
1227 >- (qx_gen_tac `d` >> Cases_on `d <= omega` >> simp[] >> fs[] >>
1228 simp[lt_omega] >> qx_gen_tac `x` >>
1229 Cases_on `?m. x = &m` >> fs[] >> strip_tac >>
1230 metis_tac [fromNat_lt_omega, ordlt_TRANS, ordlt_REFL]) >>
1231 simp[lt_omega] >> qx_gen_tac `m` >> strip_tac >>
1232 full_simp_tac (srw_ss() ++ DNF_ss) [lt_omega, impI] >>
1233 first_x_assum (qspec_then `&m` mp_tac) >> simp[] >>
1234 qexists_tac `m+1` >> numLib.DECIDE_TAC
1235QED
1236
1237Theorem csuc_is_nonzero_limit:
1238 omega <= a ==> islimit (csuc a) /\ 0 < csuc a
1239Proof
1240 strip_tac >> simp[] >>
1241 qspec_then ‘a’ (qx_choose_then ‘b’ assume_tac) cardinality_bump_exists >>
1242 CCONTR_TAC >>
1243 ‘csuc a <> 0’ by (strip_tac >> gs[]) >>
1244 ‘?a0. csuc a = ordSUC a0’ by metis_tac[ord_CASES] >>
1245 gs[csuc_def] >> pop_assum mp_tac >>
1246 DEEP_INTRO_TAC oleast_intro >> conj_tac
1247 >- goal_assum drule >>
1248 simp[preds_ordSUC] >>
1249 ‘INFINITE (preds a)’
1250 by (simp[FINITE_preds] >> rpt strip_tac >> gs[]) >>
1251 simp[INFINITE_cardleq_INSERT] >> Cases_on ‘preds a0 <<= preds a’ >>
1252 simp[] >> qexists_tac ‘a0’ >> simp[]
1253QED
1254
1255Theorem dclose_BIGUNION:
1256 dclose s = BIGUNION (IMAGE preds s)
1257Proof
1258 dsimp[Once EXTENSION, dclose_def] >> metis_tac[]
1259QED
1260
1261Theorem cardSUC_EQ0[simp]:
1262 cardSUC A <> {}
1263Proof
1264 simp[cardSUC_def]
1265QED
1266
1267Theorem omega_LEQ_INFINITE_preds:
1268 INFINITE (preds a) ==> omega <= a
1269Proof
1270 CONV_TAC CONTRAPOS_CONV >> simp[FINITE_preds, lt_omega]
1271QED
1272
1273Theorem csuc_EQ_N[simp]:
1274 csuc a = &n <=> ?m. n = SUC m /\ a = &m
1275Proof
1276 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
1277 simp[cardinality_bump_exists] >> qx_gen_tac ‘b’ >> rpt strip_tac >>
1278 simp[EQ_IMP_THM, PULL_EXISTS] >> rw[]
1279 >- (Cases_on ‘n’ >> gvs[] >>
1280 rename [‘a = &m’, ‘preds a <</= preds (ordSUC (&m))’] >>
1281 ‘FINITE (preds (ordSUC (&m) : ('a + num -> bool) ordinal))’
1282 by simp[FINITE_preds, GSYM fromNat_SUC, Excl "fromNat_SUC"] >>
1283 ‘FINITE (preds a)’ by metis_tac[CARD_LE_FINITE, cardleq_lteq] >>
1284 gvs[FINITE_preds, preds_nat,GSYM fromNat_SUC, Excl "fromNat_SUC"] >>
1285 rename [‘cardlt (IMAGE $& (count n)) (IMAGE $& (count (SUC m)))’] >>
1286 gvs[CARD_LE_CARD, CARD_INJ_IMAGE] >> ‘m <= n’ suffices_by simp[] >>
1287 first_x_assum $ qspec_then ‘&m’ mp_tac >>
1288 simp[preds_nat, CARD_LE_CARD, CARD_INJ_IMAGE]) >>
1289 rename [‘preds (&m) <</= preds b’] >>
1290 ‘FINITE (preds b)’
1291 by (CCONTR_TAC >> drule_then assume_tac omega_LEQ_INFINITE_preds >>
1292 ‘&(SUC m) < b’ by (irule ordlte_TRANS >> goal_assum drule >> simp[]) >>
1293 first_x_assum drule >> simp[preds_nat, CARD_LE_CARD, CARD_INJ_IMAGE]) >>
1294 gvs[FINITE_preds] >>
1295 gvs[CARD_LE_CARD, CARD_INJ_IMAGE, preds_nat, GSYM fromNat_SUC,
1296 Excl "fromNat_SUC", arithmeticTheory.NOT_LESS_EQUAL] >>
1297 ‘n - 1 <= m’ suffices_by simp[] >>
1298 first_x_assum $ qspec_then ‘&(n - 1)’ mp_tac >>
1299 simp[preds_nat, CARD_LE_CARD, CARD_INJ_IMAGE]
1300QED
1301
1302Theorem FINITE_cardSUC[simp]:
1303 FINITE (cardSUC A) <=> FINITE A
1304Proof
1305 simp[cardSUC_def, FINITE_preds] >> DEEP_INTRO_TAC oleast_intro >>
1306 rpt strip_tac
1307 >- (irule cardeq_ordinals_exist >>
1308 resolve_then (Pos hd) irule CARD_LE_UNIV cardleq_TRANS >>
1309 simp[disjUNION_UNIV, CARD_LE_ADDL]) >>
1310 eq_tac
1311 >- (strip_tac >> gvs[] >> drule_then irule (iffLR CARDEQ_FINITE) >>
1312 simp[preds_nat]) >>
1313 strip_tac >> drule_then drule (iffRL CARDEQ_FINITE) >>
1314 simp[FINITE_preds]
1315QED
1316
1317Theorem cardlt_preds:
1318 cardlt (preds x) (preds y) ==> x < y
1319Proof
1320 CONV_TAC CONTRAPOS_CONV >> simp[ordle_lteq, DISJ_IMP_THM] >>
1321 metis_tac[PSUBSET_DEF, CARD_LE_SUBSET, preds_lt_PSUBSET]
1322QED
1323
1324Theorem INFINITE_eqpreds:
1325 omega <= (x:'a ordinal) ==> INFINITE { y : 'a ordinal | preds y =~ preds x }
1326Proof
1327 rpt strip_tac >>
1328 ‘{ y : 'a ordinal | preds y =~ preds x} <> {}’
1329 by (simp[EXTENSION] >> metis_tac[cardeq_REFL]) >>
1330 drule_all_then strip_assume_tac FINITE_omax_IS_SOME >>
1331 gs[omax_SOME] >> rename [‘preds a =~ preds x’] >>
1332 ‘INFINITE (preds a)’
1333 by (strip_tac >> gvs[FINITE_preds] >> rename [‘preds (&n) =~ preds x’] >>
1334 ‘x <= &n’ by metis_tac[cardeq_REFL] >>
1335 ‘omega <= &n’ by metis_tac[ordle_TRANS] >> gs[]) >>
1336 ‘preds (ordSUC a) =~ preds x’
1337 by (simp[preds_ordSUC] >> metis_tac[CARDEQ_INSERT_RWT, cardeq_TRANS]) >>
1338 first_x_assum drule >> simp[]
1339QED
1340
1341Theorem cardlt_lepreds:
1342 cardlt (preds (x : 'a ordinal)) { (y : 'a ordinal) | preds y <<= preds x }
1343Proof
1344 rpt strip_tac >>
1345 qabbrev_tac ‘s = { y : 'a ordinal | preds y <<= preds x }’ >>
1346 ‘s <<= univ(:num + 'a)’ by metis_tac[cardleq_TRANS, preds_inj_univ] >>
1347 Cases_on ‘x < omega’
1348 >- (gvs[lt_omega, preds_nat] >>
1349 rev_drule_at (Pos last) CARD_LE_CARD_IMP >> simp[Abbr‘s’] >>
1350 simp[CARD_INJ_IMAGE] >> qmatch_abbrev_tac ‘~(CARD s <= m)’ >>
1351 ‘s = IMAGE $& (count (m + 1))’ suffices_by simp[CARD_INJ_IMAGE] >>
1352 simp[Abbr‘s’, EXTENSION] >> qx_gen_tac ‘n’ >> eq_tac
1353 >- (strip_tac >> drule_at (Pos last) CARD_LE_CARD_IMP >>
1354 simp[CARD_INJ_IMAGE] >>
1355 ‘n < omega’
1356 by (CCONTR_TAC >> qpat_x_assum ‘_ <<= _’ mp_tac >> simp[] >>
1357 irule CARD_LT_FINITE_INFINITE >> simp[FINITE_preds] >>
1358 rpt strip_tac >> gs[]) >> gvs[lt_omega] >>
1359 rename [‘preds (&n)’] >> simp[preds_nat, CARD_INJ_IMAGE]) >>
1360 rw[] >> simp[preds_nat] >> irule CARD_LE_SUBSET >> simp[SUBSET_DEF]) >>
1361 ‘INFINITE s’
1362 by (‘s = { y | preds y =~ preds x} UNION { y | cardlt (preds y) (preds x)}’
1363 by (simp[Abbr‘s’, EXTENSION] >> metis_tac[cardleq_lteq]) >>
1364 simp[INFINITE_eqpreds]) >>
1365 ‘dclose s = s’
1366 by (simp[dclose_def, EXTENSION] >> qx_gen_tac ‘a’ >> eq_tac >>
1367 rpt strip_tac
1368 >- (gs[Abbr‘s’, preds_lt_PSUBSET] >>
1369 metis_tac[cardleq_TRANS, CARD_LE_SUBSET, PSUBSET_DEF]) >>
1370 qexists_tac ‘ordSUC a’ >> simp[] >> gs[Abbr‘s’, preds_ordSUC] >>
1371 irule (iffRL INFINITE_cardleq_INSERT) >> simp[FINITE_preds] >>
1372 rpt strip_tac >> gs[]) >>
1373 ‘preds (sup s) = s’ by simp[preds_sup] >>
1374 Cases_on ‘preds (sup s) =~ preds x’
1375 >- (‘preds (ordSUC (sup s)) =~ preds x’
1376 by (gs[preds_ordSUC] >> metis_tac[cardeq_TRANS, CARDEQ_INSERT_RWT]) >>
1377 ‘!x. x IN s ==> x <= sup s’ by simp[suple_thm] >>
1378 ‘ordSUC (sup s) IN s’ suffices_by (strip_tac >> first_x_assum drule >>
1379 simp[]) >>
1380 qabbrev_tac ‘mx = sup s’ >> simp[Abbr‘s’] >>
1381 metis_tac[cardleq_REFL, CARD_LE_CONG, cardeq_REFL]) >>
1382 Cases_on ‘preds (sup s) <</= preds x’
1383 >- (drule cardlt_preds >> simp[] >> irule suple_thm >> simp[] >>
1384 simp[Abbr‘s’]) >>
1385 ‘preds x <</= preds(sup s)’ by metis_tac[CARD_LT_TOTAL] >> gs[preds_sup]
1386QED
1387
1388Theorem cardle_preds_EQ_cardeq_preds:
1389 omega <= (x:'a ordinal) ==>
1390 { (y:'a ordinal) | preds y <<= preds x } =~
1391 { (y:'a ordinal) | preds y =~ preds x }
1392Proof
1393 strip_tac >> irule cardleq_ANTISYM >> reverse conj_tac
1394 >- (irule CARD_LE_SUBSET >> simp[SUBSET_DEF] >>
1395 metis_tac[CARD_LE_CONG, cardeq_REFL, cardeq_SYM, cardleq_REFL]) >>
1396 ‘{ (y:'a ordinal) | preds y <<= preds x} =
1397 { y | preds y =~ preds x } UNION { y | cardlt (preds y) (preds x) }’
1398 by (simp[EXTENSION, Once cardleq_lteq] >> metis_tac[]) >>
1399 pop_assum SUBST1_TAC >>
1400 resolve_then (Pos hd) irule UNION_LE_ADD_C cardleq_TRANS >>
1401 irule CARD_ADD2_ABSORB_LE >> simp[INFINITE_eqpreds] >>
1402 simp[Once cardleq_def, INJ_IFF, PULL_EXISTS] >>
1403 qexists_tac ‘λy. x + y’ >> simp[] >> qx_gen_tac ‘y’ >>
1404 strip_tac >> drule_then assume_tac cardlt_preds >>
1405 ‘preds (x + y) = preds x UNION IMAGE (λy. x + y) (preds y)’
1406 by (simp[EXTENSION, EQ_IMP_THM] >> rw[] >> simp[]
1407 >- (rename [‘x0 < x + y’] >> Cases_on ‘x0 < x’ >> simp[] >>
1408 gs[ordle_EXISTS_ADD]) >>
1409 irule ordlte_TRANS >> first_assum $ irule_at Any >> simp[]) >>
1410 simp[] >>
1411 ‘preds x INTER IMAGE (λy. x + y) (preds y) = {}’
1412 by (simp[EXTENSION] >> qx_gen_tac ‘a’ >> Cases_on ‘x <= a’ >> simp[] >>
1413 qx_gen_tac ‘b’ >> rpt strip_tac >> gvs[]) >>
1414 dxrule_then assume_tac CARDEQ_DISJOINT_UNION >>
1415 drule_then irule cardeq_TRANS >>
1416 resolve_then (Pos hd) irule CARD_ADD_SYM cardeq_TRANS >>
1417 irule CARD_ADD_ABSORB >> conj_tac
1418 >- (strip_tac >> gvs[FINITE_preds]) >>
1419 irule IMAGE_cardleq_rwt >> metis_tac[cardleq_lteq]
1420QED
1421
1422Theorem cardlt_eqpreds:
1423 omega <= (x:'a ordinal) ==>
1424 cardlt (preds x) { y:'a ordinal | preds y =~ preds x }
1425Proof
1426 strip_tac >>
1427 resolve_then (Pos hd)
1428 (resolve_then Any irule
1429 (ONCE_REWRITE_RULE [cardeq_SYM] cardle_preds_EQ_cardeq_preds))
1430 cardeq_REFL
1431 (iffRL CARD_LT_CONG) >>
1432 simp[cardlt_lepreds]
1433QED
1434
1435Theorem orderiso_cardeq_elsOf:
1436 orderiso w1 w2 ==> elsOf w1 =~ elsOf w2
1437Proof
1438 simp[orderiso_thm, cardeq_def] >> metis_tac[]
1439QED
1440
1441Theorem transfer_ordinals:
1442 !a:'a ordinal.
1443 preds a <<= univ(:num + 'b) ==>
1444 ?b:'b ordinal. orderiso (wobound a allOrds) (wobound b allOrds) /\
1445 preds a =~ preds b
1446Proof
1447 rw[cardleq_def,preds_wobound] >>
1448 drule_then (qx_choose_then ‘w1’ assume_tac) elsOf_cardeq_iso>>
1449 qexists_tac ‘mkOrdinal w1’ >>
1450 qspec_then ‘w1’ assume_tac wellorder_ordinal_isomorphism >>
1451 conj_asm1_tac >- metis_tac[orderiso_TRANS] >>
1452 metis_tac[orderiso_cardeq_elsOf]
1453QED
1454
1455Theorem lt_cardSUC:
1456 A <</= cardSUC A
1457Proof
1458 simp[cardSUC_def] >> qabbrev_tac ‘Aord = oleast a:'a ordinal. preds a =~ A’ >>
1459 ‘preds Aord =~ A’
1460 by (simp[Abbr‘Aord’] >> DEEP_INTRO_TAC oleast_intro >> simp[] >>
1461 irule cardeq_ordinals_exist >>
1462 simp[disjUNION_UNIV] >>
1463 resolve_then (Pos hd) irule CARD_LE_UNIV CARD_LE_TRANS >>
1464 simp[CARD_LE_ADDL]) >>
1465 ‘preds Aord <</= preds (csuc Aord)’
1466 suffices_by metis_tac[CARD_LT_CONG, cardeq_REFL] >>
1467 ‘preds Aord <<= univ(:num + ('a + num -> bool))’
1468 by (resolve_then (Pos hd) irule preds_inj_univ CARD_LE_TRANS >>
1469 simp[Once cardleq_lteq, bumpUNIV_cardlt]) >>
1470 drule_then (qx_choose_then ‘Aord'’ strip_assume_tac) transfer_ordinals >>
1471 ‘Aord' < csuc Aord’
1472 by (simp[lt_csuc] >> metis_tac[CARD_LE_CONG, CARD_LE_REFL, cardeq_REFL]) >>
1473 ‘preds Aord' <</= preds (csuc Aord)’ suffices_by
1474 metis_tac[CARD_LE_CONG, cardeq_REFL, cardeq_SYM] >>
1475 simp[csuc_def] >>
1476 DEEP_INTRO_TAC oleast_intro >> rw[]
1477 >- metis_tac[cardinality_bump_exists] >>
1478 ‘preds a = { y | preds y <<= preds Aord' }’
1479 by (simp[EXTENSION] >> rw[EQ_IMP_THM]
1480 >- metis_tac[CARD_LE_CONG, cardeq_REFL, cardeq_SYM] >>
1481 irule cardlt_preds >>
1482 first_assum $ C (resolve_then (Pos hd) irule) CARD_LET_TRANS >>
1483 metis_tac[CARD_LT_CONG, cardeq_REFL]) >>
1484 simp[cardlt_lepreds]
1485QED
1486
1487Theorem le_cardSUC[simp]:
1488 A <<= cardSUC A
1489Proof
1490 metis_tac[lt_cardSUC, cardleq_lteq]
1491QED
1492
1493Theorem preds_csuc_lemma:
1494 preds a ≼ preds (csuc a)
1495Proof
1496 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
1497 simp[cardinality_bump_exists] >> metis_tac[cardleq_lteq]
1498QED
1499
1500Theorem cardleq_preds_csuc:
1501 preds a <<= preds b ==> preds (csuc a) <<= preds (csuc b)
1502Proof
1503 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
1504 simp[cardinality_bump_exists] >> rw[] >>
1505 DEEP_INTRO_TAC oleast_intro >>
1506 simp[cardinality_bump_exists] >> rw[] >>
1507 rename [‘preds a <<= preds b’, ‘preds b <</= preds c’,
1508 ‘preds a <</= preds d’] >>
1509 CCONTR_TAC >>
1510 ‘?c' : ('a + num -> bool) ordinal.
1511 orderiso (wobound c allOrds) (wobound c' allOrds) /\
1512 preds c =~ preds c'’
1513 by (irule transfer_ordinals >>
1514 resolve_then (Pos last) irule preds_inj_univ cardleq_TRANS >>
1515 metis_tac[cardleq_lteq]) >>
1516 ‘preds c' <</= preds d’ by metis_tac[CARD_LT_CONG, cardeq_REFL] >>
1517 drule_then assume_tac cardlt_preds >> first_x_assum drule >>
1518 metis_tac[CARD_LE_TRANS, CARD_LET_TRANS, CARD_LT_REFL, CARD_LT_CONG,
1519 cardeq_REFL]
1520QED