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