ordinalScript.sml
1Theory ordinal
2Ancestors
3 option set_relation pred_set wellorder cardinal topology ordinalBasic
4 sum pair
5Libs
6 boolSimps
7
8(* The ordinals' notation is exported here rather than by ordinalBasic,
9 which the datatype package's construction ancestors and everything
10 that declares a datatype therefore loads: `+`, `<` and `TC` would
11 otherwise mean what they mean here everywhere, and a numeral whose
12 type is not pinned would be an ordinal. *)
13Overload "<" = “ordlt”
14Overload "<=" = “\a b. ~ordlt b a”
15Overload TC = “ordSUC”
16Overload islimit = “\a:'a ordinal. omax (preds a) = NONE”
17Overload "+" = “ordADD”
18Overload "ω" = “omega”
19val _ = add_numeral_form (#"o", SOME "fromNat")
20
21Theorem ordlt_preds_mono:
22 a < b ==> preds a <<= preds b
23Proof
24 strip_tac >> irule CARD_LE_SUBSET >> simp[SUBSET_DEF] >>
25 metis_tac[ordlt_TRANS]
26QED
27
28Type cord = ``:unit ordinal``
29
30Theorem unitinf_univnum:
31 univ(:unit inf) =~ univ(:num)
32Proof
33 simp[cardeq_def] >>
34 qexists_tac `\s. case s of INL n => n + 1 | INR () => 0` >>
35 simp[BIJ_DEF, INJ_DEF, SURJ_DEF, EXISTS_SUM, FORALL_SUM] >>
36 Cases >> simp[arithmeticTheory.ADD1] >>
37 qexists_tac `()` >> simp[]
38QED
39
40Theorem cord_countable_preds:
41 countable (preds (ord:cord))
42Proof
43 simp[countable_thm] >>
44 qsuff_tac `preds ord <<= univ(:unit inf)`
45 >- metis_tac [unitinf_univnum, CARDEQ_CARDLEQ, cardeq_REFL] >>
46 simp[preds_inj_univ]
47QED
48
49Theorem univ_cord_uncountable:
50 ~countable (univ(:cord))
51Proof
52 simp[countable_thm] >> strip_tac >>
53 `univ(:cord) <<= univ(:unit inf)`
54 by metis_tac [CARDEQ_CARDLEQ, cardeq_REFL, unitinf_univnum] >>
55 fs[univ_ord_greater_cardinal]
56QED
57
58
59
60
61
62Theorem sup_eq_sup:
63 (s1:'a ordinal set) <<= univ(:'a inf) /\
64 (s2:'a ordinal set) <<= univ(:'a inf) /\
65 (!a. a IN s1 ==> ?b. b IN s2 /\ a <= b) /\
66 (!b. b IN s2 ==> ?a. a IN s1 /\ b <= a) ==> (sup s1 = sup s2)
67Proof
68 strip_tac >> match_mp_tac ordle_ANTISYM >> simp[sup_thm] >>
69 metis_tac [suple_thm, ordle_TRANS]
70QED
71
72val impI = DECIDE ``~p \/ q <=> (p ==> q)``
73
74Theorem predimage_suplt_ELIM =
75 predimage_sup_thm |> SPEC_ALL |> Q.AP_TERM `$~`
76 |> CONV_RULE (RAND_CONV (SIMP_CONV bool_ss [impI]))
77 |> EQ_IMP_RULE |> #1
78 |> SIMP_RULE bool_ss [SimpL ``$==>``, ordle_lteq]
79 |> SIMP_RULE bool_ss [DISJ_IMP_THM]
80 |> CONJUNCT1
81Theorem suppred_suplt_ELIM =
82 predimage_suplt_ELIM |> Q.INST [`f` |-> `\x.x`]
83 |> SIMP_RULE (srw_ss()) [];
84
85Overload countableOrd = ``\a. countable(preds a)``
86
87Theorem countableOrds_dclosed:
88 a < b /\ countableOrd b ==> countableOrd a
89Proof
90 strip_tac >>
91 `preds a SUBSET preds b` by metis_tac [preds_lt_PSUBSET, PSUBSET_DEF] >>
92 metis_tac[subset_countable]
93QED
94
95
96Theorem omax_sup:
97 (omax s = SOME a) ==> (sup s = a)
98Proof
99 simp[omax_SOME, sup_def] >> strip_tac >>
100 DEEP_INTRO_TAC oleast_intro >> simp[] >> conj_tac
101 >- (qsuff_tac `?b. !c. b IN preds c ==> c NOTIN s` >- metis_tac[] >>
102 simp[] >> metis_tac[]) >>
103 dsimp [] >> qx_gen_tac `b` >> strip_tac >>
104 `!c. b IN preds c ==> c NOTIN s` by metis_tac[] >>
105 fs [] >> qsuff_tac `a <= b /\ b <= a` >- metis_tac [ordlt_trichotomy] >>
106 metis_tac[]
107QED
108
109
110
111
112
113Theorem ordle_CANCEL_ADDR[simp]:
114 x <= x + a
115Proof
116 simp[ordle_lteq] >> metis_tac[ordlt_trichotomy, ordlt_ZERO]
117QED
118
119Theorem countableOrds_uncountable:
120 ~countable { a:'a ordinal | countableOrd a }
121Proof
122 strip_tac >> qabbrev_tac `CO = { a | countableOrd a }` >>
123 `CO <<= univ(:'a inf)`
124 by metis_tac[countable_thm, cardleq_TRANS, Unum_cle_Uinf] >>
125 `!b. b < sup CO <=> ?d. d IN CO /\ b < d` by metis_tac [sup_thm] >>
126 `countableOrd (sup CO)`
127 by (`preds (sup CO) = dclose CO` by simp[preds_sup] >>
128 simp[countable_thm, dclose_BIGUNION] >>
129 match_mp_tac CARD_BIGUNION >>
130 asm_simp_tac (srw_ss() ++ DNF_ss) [] >> conj_tac
131 >- (match_mp_tac IMAGE_cardleq_rwt >> fs[countable_thm]) >>
132 simp[Abbr`CO`, countable_thm]) >>
133 `countable (preds (sup CO)^+)` by simp[preds_ordSUC] >>
134 `(sup CO)^+ IN CO` by simp[Abbr`CO`] >>
135 `sup CO < (sup CO)^+` by simp[] >>
136 metis_tac [ordlt_REFL]
137QED
138
139Theorem dclose_cardleq_univinf:
140 (s:'a ordinal set) <<= univ(:'a inf) ==> dclose s <<= univ(:'a inf)
141Proof
142 strip_tac >> simp[dclose_BIGUNION] >>
143 match_mp_tac CARD_BIGUNION >>
144 dsimp[preds_inj_univ] >> metis_tac [cardleq_TRANS, IMAGE_cardleq]
145QED
146
147fun mklesup th =
148 th |> UNDISCH_ALL |> Q.SPEC `sup s`
149 |> SIMP_RULE (srw_ss()) [] |> REWRITE_RULE [impI] |> DISCH_ALL
150
151Theorem sup_lt_implies:
152 (s:'a ordinal set) <<= univ(:'a inf) /\ sup s < a /\ b IN s ==> b < a
153Proof
154 strip_tac >>
155 `sup s <= a` by simp[ordle_lteq] >>
156 pop_assum mp_tac >> simp[sup_thm, impI] >> strip_tac >>
157 `b <= a` by simp[] >> fs[ordle_lteq] >> fs[] >>
158 `a <= sup s` by metis_tac [mklesup sup_thm]
159QED
160
161Theorem sup_eq_SUC:
162 s:'a ordinal set <<= univ(:'a inf) /\ sup s = a^+ ==> a^+ IN s
163Proof
164 rpt strip_tac >> `a < sup s` by simp[] >>
165 pop_assum mp_tac >> pop_assum (mp_tac o SYM) >> simp[sup_thm] >> strip_tac >>
166 disch_then (Q.X_CHOOSE_THEN `b` strip_assume_tac) >>
167 qsuff_tac `b = a^+` >- metis_tac[] >>
168 match_mp_tac ordle_ANTISYM >> conj_tac
169 >- metis_tac [sup_lt_implies, ordlt_REFL] >>
170 simp[ordlt_SUC_DISCRETE] >> metis_tac[ordle_lteq, ordlt_REFL]
171QED
172
173
174Theorem generic_continuity:
175 (!a. 0 < a /\ islimit a ==> f a :'a ordinal = sup (IMAGE f (preds a))) /\
176 (!x y. x <= y ==> f x <= f y) ==>
177 !s:'a ordinal set.
178 s <<= univ(:'a inf) /\ s <> {} ==> f (sup s) = sup (IMAGE f s)
179Proof
180 rpt strip_tac >>
181 `islimit (sup s) \/ ?a. omax (preds (sup s)) = SOME a`
182 by metis_tac [option_CASES]
183 >| [
184 Cases_on `sup s = 0` >> simp[]
185 >- (pop_assum (mp_tac o Q.AP_TERM `preds`) >>
186 asm_simp_tac bool_ss [preds_sup] >> simp[dclose_def, EXTENSION] >>
187 fs[omax_NONE] >>
188 disch_then (qspec_then `0` mp_tac) >>
189 disch_then (assume_tac o SIMP_RULE (srw_ss()) []) >>
190 `s = {0}` by (fs[EXTENSION] >> metis_tac[]) >> simp[]) >>
191 match_mp_tac ordle_ANTISYM >> Tactical.REVERSE conj_tac
192 >- (dsimp[sup_thm, IMAGE_cardleq_rwt, impI, dclose_cardleq_univinf] >>
193 ntac 2 strip_tac >> first_x_assum match_mp_tac >>
194 simp[mklesup sup_thm]) >>
195 `0 < sup s` by metis_tac [ordlt_trichotomy, ordlt_ZERO] >>
196 simp[preds_sup] >>
197 qpat_x_assum `islimit (sup s)` mp_tac >> simp[preds_sup] >> strip_tac >>
198 dsimp[sup_thm, IMAGE_cardleq_rwt, impI, dclose_cardleq_univinf,
199 dclose_def] >>
200 ntac 4 strip_tac >>
201 match_mp_tac ordle_TRANS >> qexists_tac `f y` >> conj_tac
202 >- metis_tac [ordle_lteq] >>
203 match_mp_tac
204 (SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] (mklesup sup_thm)) >>
205 simp[IMAGE_cardleq_rwt] >> metis_tac[],
206
207 `sup (preds (sup s)) = a` by metis_tac[omax_sup] >>
208 fs[preds_omax_SOME_SUC] >>
209 `a^+ IN s` by metis_tac [sup_eq_SUC] >>
210 ONCE_REWRITE_TAC [EQ_SYM_EQ] >>
211 match_mp_tac sup_eq_max >> dsimp[] >>
212 ntac 2 strip_tac >> first_x_assum match_mp_tac >>
213 metis_tac [mklesup sup_thm]
214 ]
215QED
216
217
218Theorem islimit_0: islimit 0
219Proof simp[]
220QED
221
222(* An intermediate value theorem of sorts.
223
224 Thanks to Martin Ward for the theorem and some related discussion.
225 For the moment, we don't have a proof without the weakly increasing
226 side condition, which is annoying.
227*)
228
229Theorem ordinal_IVT:
230 (!a:'a ordinal.
231 0 < a /\ islimit a ==> f a : 'a ordinal = sup (IMAGE f (preds a))) /\
232 (!x y. x <= y ==> f x <= f y) /\ a1 < a2 /\ f a1 <= c /\ c < f a2 ==>
233 ?b. a1 <= b /\ b < a2 /\ f b <= c /\ c < f b^+
234Proof
235 strip_tac >>
236 qabbrev_tac `mu = oleast a. c < f a /\ a1 < a` >>
237 `c < f mu /\ a1 < mu /\ (!a. a < mu ==> f a <= c \/ a <= a1)`
238 by (simp[Abbr`mu`] >> DEEP_INTRO_TAC oleast_intro >> conj_tac
239 >- (qexists_tac `a2` >> simp[ordle_lteq]) >> simp[]) >>
240 markerLib.RM_ALL_ABBREVS_TAC >>
241 `~islimit mu`
242 by (strip_tac >> `sup (preds mu)= mu` by fs[sup_preds_omax_NONE] >>
243 `0 < mu` by (spose_not_then assume_tac >> fs[]) >>
244 `f mu = sup (IMAGE f (preds mu))` by metis_tac[] >>
245 `?d. d < mu /\ c < f d` by metis_tac[predimage_sup_thm] >>
246 `d <= a1` by metis_tac[] >>
247 `f d <= f a1` by metis_tac[] >>
248 metis_tac [ordlte_TRANS, ordle_TRANS]) >>
249 `?d. mu = d^+` by metis_tac[ord_CASES, islimit_0] >>
250 `d < mu` by simp[] >>
251 qexists_tac `d` >>
252 `a1 <= d` by metis_tac[ordlt_SUC_DISCRETE, ordle_lteq] >>
253 `f d <= c` by metis_tac[ordle_ANTISYM] >>
254 `d < a2` suffices_by metis_tac[] >>
255 metis_tac[ordle_TRANS, ordle_TRANS]
256QED
257
258Theorem ordADD_continuous =
259 generic_continuity |> Q.INST [`f` |-> `$+ a`] |> SIMP_RULE (srw_ss()) []
260
261Theorem ordADD_ASSOC:
262 !a b c:'a ordinal. a + (b + c) = (a + b) + c
263Proof
264 qsuff_tac `!c a b:'a ordinal. a + (b + c) = (a + b) + c` >- simp[] >>
265 ho_match_mp_tac simple_ord_induction >> simp[predimage_sup_thm] >>
266 qx_gen_tac `c` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >>
267 `IMAGE ($+ (a + b)) (preds c) = IMAGE ($+ a) (IMAGE ($+ b) (preds c))`
268 by (dsimp[EXTENSION] >> asm_simp_tac (srw_ss() ++ CONJ_ss) []) >>
269 simp[] >>
270 match_mp_tac ordADD_continuous >>
271 simp[IMAGE_cardleq_rwt, preds_inj_univ] >>
272 metis_tac [preds_0, preds_11, ordlt_REFL]
273QED
274
275Theorem exists_C[local]:
276 (?h:'a -> 'a -> 'a. P h) <=> (?h. P (combin$C h))
277Proof
278 eq_tac >> strip_tac
279 >- (qexists_tac `combin$C h` >>
280 qsuff_tac `combin$C (combin$C h) = h` >- simp[] >>
281 simp[FUN_EQ_THM]) >> metis_tac[]
282QED
283
284Theorem ADD1R:
285 a + 1 = a^+
286Proof
287 REWRITE_TAC [GSYM ORD_ONE] >> simp[]
288QED
289
290Theorem ordADD_weak_MONO:
291 !c a b:'a ordinal. a < b ==> a + c <= b + c
292Proof
293 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
294 >- simp[ordle_lteq] >>
295 qx_gen_tac `c` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >>
296 strip_tac >> simp[predimage_sup_thm, impI] >> qx_gen_tac `d` >> strip_tac >>
297 strip_tac >>
298 `a + d <= b + d` by metis_tac[] >>
299 `b + d IN IMAGE ($+ b) (preds c)` by simp[] >>
300 metis_tac[sup_lt_implies, IMAGE_cardleq_rwt, preds_inj_univ]
301QED
302
303(* Multiplication *)
304
305val ordMULT_def = new_specification(
306 "ordMULT_def", ["ordMULT"],
307 ord_RECURSION |> INST_TYPE [beta |-> ``:'a ordinal``]
308 |> Q.SPEC `0`
309 |> Q.SPEC `\ap r. r + b`
310 |> Q.SPEC `\a preds. sup preds`
311 |> Q.GEN `b`
312 |> CONV_RULE SKOLEM_CONV
313 |> BETA_RULE)
314val _ = export_rewrites ["ordMULT_def"]
315Overload "*" = ``ordMULT``
316
317Theorem ordMULT_0L[simp]:
318 !a:'a ordinal. 0 * a = 0
319Proof
320 ho_match_mp_tac simple_ord_induction >> simp[] >> qx_gen_tac `a` >>
321 strip_tac >> qsuff_tac `IMAGE ($* 0) (preds a) = {0}` >> simp[] >>
322 simp[EXTENSION] >> metis_tac[]
323QED
324
325Theorem ordMULT_0R: !a:'a ordinal. a * 0 = 0
326Proof simp[]
327QED
328
329Theorem ordMULT_1L[simp]:
330 !a. 1 * (a:'a ordinal) = a
331Proof
332 ho_match_mp_tac simple_ord_induction >> simp[ADD1R] >> qx_gen_tac `a` >>
333 strip_tac >> qsuff_tac `IMAGE ($* 1) (preds a) = preds a`
334 >- fs [sup_preds_omax_NONE] >>
335 dsimp[EXTENSION] >> asm_simp_tac (srw_ss() ++ CONJ_ss) []
336QED
337
338Theorem ordMULT_1R[simp]:
339 !a:'a ordinal. a * 1 = a
340Proof
341 simp_tac bool_ss [GSYM ORD_ONE, ordMULT_def, ordADD_0L]
342QED
343
344Theorem ordMULT_2R:
345 (a:'a ordinal) * 2 = a + a
346Proof
347 `2 = 1^+` by simp[] >> pop_assum SUBST1_TAC >> simp[]
348QED
349
350Theorem ordMULT_lt_MONO_R:
351 !a b c:'a ordinal. a < b /\ 0 < c ==> c * a < c * b
352Proof
353 qsuff_tac `!b a c:'a ordinal. a < b /\ 0 < c ==> c * a < c * b` >- metis_tac[]>>
354 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
355 >- (simp[ordlt_SUC_DISCRETE] >> qx_gen_tac `b` >> strip_tac >>
356 map_every qx_gen_tac [`a`, `c`] >>
357 Cases_on `a = b` >> simp[] >> strip_tac >>
358 `c * a < c * b` by metis_tac[] >>
359 `c * b < c * b + c` by simp[] >> metis_tac [ordlt_TRANS]) >>
360 qx_gen_tac `b` >> strip_tac >> map_every qx_gen_tac [`a`, `c`] >>
361 strip_tac >> simp[predimage_sup_thm] >>
362 `?d. a < d /\ d < b`
363 by metis_tac[sup_preds_omax_NONE, IN_preds, preds_inj_univ, sup_thm] >>
364 metis_tac[]
365QED
366
367Theorem ordMULT_le_MONO_R:
368 !a b c:'a ordinal. a <= b ==> c * a <= c * b
369Proof
370 simp[ordle_lteq] >> rpt strip_tac >> simp[] >>
371 Cases_on `c = 0` >> simp[] >>
372 `0 < c` by metis_tac [ordlt_ZERO, ordlt_trichotomy] >>
373 metis_tac [ordMULT_lt_MONO_R]
374QED
375
376Theorem ordMULT_lt_MONO_R_EQN[simp]:
377 c * a < c * b <=> a < b /\ 0 < c
378Proof
379 simp[EQ_IMP_THM, ordMULT_lt_MONO_R] >>
380 Cases_on `0 < c` >- metis_tac [ordMULT_le_MONO_R] >> fs[]
381QED
382
383Theorem ordADD_le_MONO_L:
384 x <= y ==> x + z <= y + z
385Proof
386 simp[ordle_lteq, SimpL ``$==>``] >> simp[DISJ_IMP_THM, ordADD_weak_MONO]
387QED
388
389Theorem ordMULT_le_MONO_L:
390 !a b c:'a ordinal. a <= b ==> a * c <= b * c
391Proof
392 qsuff_tac `!c a b:'a ordinal. a <= b ==> a * c <= b * c` >- metis_tac[] >>
393 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
394 >- (qx_gen_tac `c` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >>
395 strip_tac >>
396 `a * c + a <= a * c + b` by simp[] >>
397 match_mp_tac ordle_TRANS >> qexists_tac `a * c + b` >> simp[] >>
398 simp[ordADD_le_MONO_L]) >>
399 qx_gen_tac `c` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >> strip_tac>>
400 simp[predimage_sup_thm, impI] >> qx_gen_tac `d` >> strip_tac >>
401 match_mp_tac ordle_TRANS >> qexists_tac `b * d` >> simp[] >>
402 qsuff_tac `b * d IN IMAGE ($* b) (preds c)`
403 >- metis_tac [mklesup sup_thm, IMAGE_cardleq_rwt, preds_inj_univ] >>
404 simp[] >> metis_tac[]
405QED
406
407Theorem ordMULT_CANCEL_R[simp]:
408 (z * x = z * y:'a ordinal) <=> (z = 0) \/ (x = y)
409Proof
410 simp[EQ_IMP_THM, DISJ_IMP_THM] >> strip_tac >>
411 Tactical.REVERSE (Cases_on `0 < z`) >- fs[] >>
412 `x < y \/ (x = y) \/ y < x` by metis_tac [ordlt_trichotomy] >>
413 metis_tac [ordMULT_lt_MONO_R_EQN, ordlt_REFL]
414QED
415
416val ordMULT_continuous0 =
417 generic_continuity |> Q.INST [`f` |-> `$* a`]
418 |> SIMP_RULE (srw_ss()) []
419
420Theorem ordMULT_continuous:
421 !s:'a ordinal set. s <<= univ(:'a inf) ==> a * sup s = sup (IMAGE ($* a) s)
422Proof
423 rpt strip_tac >> Cases_on `s = {}` >> simp[ordMULT_continuous0]
424QED
425
426Theorem ordMULT_fromNat[simp]:
427 (&n : 'a ordinal) * &m = &(n * m)
428Proof
429 Induct_on `m` >> simp[arithmeticTheory.MULT_CLAUSES]
430QED
431
432Theorem omega_MUL_fromNat:
433 0 < n ==> &n * omega = omega
434Proof
435 simp[omax_preds_omega] >> strip_tac >>
436 match_mp_tac ordle_ANTISYM >> dsimp[predimage_sup_thm, lt_omega, impI] >>
437 conj_tac >- simp[ordle_lteq] >>
438 qx_gen_tac `m` >>
439 qsuff_tac `&m < sup (IMAGE ($* &n) (preds omega))` >- metis_tac[ordlt_REFL]>>
440 dsimp[predimage_sup_thm, lt_omega] >>
441 qexists_tac `m + 1` >> simp[arithmeticTheory.LEFT_ADD_DISTRIB] >>
442 qsuff_tac `m <= m * n /\ m * n < n + m * n` >- DECIDE_TAC >>
443 simp[]
444QED
445
446Theorem ordMULT_LDISTRIB:
447 !a b c:'a ordinal. c * (a + b) = c * a + c * b
448Proof
449 qsuff_tac `!b a c. c * (a + b) = c * a + c * b` >- simp[] >>
450 ho_match_mp_tac simple_ord_induction >> simp[ordADD_ASSOC] >>
451 qx_gen_tac `b` >> strip_tac >>
452 `preds b <> {}` by (strip_tac >> fs[]) >>
453 simp[ordADD_continuous, ordMULT_continuous, IMAGE_cardleq_rwt,
454 preds_inj_univ] >>
455 rpt strip_tac >> AP_TERM_TAC >> dsimp[EXTENSION] >>
456 asm_simp_tac (srw_ss() ++ CONJ_ss) []
457QED
458
459Theorem ordMULT_ASSOC:
460 !a b c:'a ordinal. a * (b * c) = (a * b) * c
461Proof
462 qsuff_tac `!c a b:'a ordinal. a * (b * c) = (a * b) * c` >- simp[] >>
463 ho_match_mp_tac simple_ord_induction >> simp[ordMULT_LDISTRIB] >>
464 simp[ordMULT_continuous, IMAGE_cardleq_rwt, preds_inj_univ] >>
465 rpt strip_tac >> AP_TERM_TAC >> dsimp[EXTENSION] >>
466 asm_simp_tac (srw_ss() ++ CONJ_ss) []
467QED
468
469Theorem ordDIVISION0[local]:
470 !a b:'a ordinal. 0 < b ==> ?q r. a = b * q + r /\ r < b
471Proof
472 rpt strip_tac >>
473 qabbrev_tac `d = sup { c | b * c <= a }` >>
474 `!c. b * c <= a ==> c <= a`
475 by (ntac 2 strip_tac >> match_mp_tac ordle_TRANS >>
476 qexists_tac `b * c` >> simp[] >>
477 match_mp_tac ordle_TRANS >> qexists_tac `1 * c` >> conj_tac >- simp[]>>
478 match_mp_tac ordMULT_le_MONO_L >>
479 simp_tac bool_ss [GSYM ORD_ONE, ordlt_SUC_DISCRETE] >>
480 simp[] >> strip_tac >> fs[]) >>
481 `!aa. aa IN { c | b * c <= a } ==> aa < a^+`
482 by (simp[ordlt_SUC_DISCRETE] >> metis_tac [ordle_lteq]) >>
483 `!aa. aa < d <=> ?c. b * c <= a /\ aa < c`
484 by (simp[Abbr`d`] >> pop_assum (assume_tac o MATCH_MP ubsup_thm) >>
485 simp[]) >>
486 `b * d <= a`
487 by (simp[Abbr`d`] >>
488 `{ c | b * c <= a } <<= univ(:'a inf)`
489 by (`{ c | b * c <= a } <<= preds a^+`
490 by simp[SUBSET_DEF, SUBSET_CARDLEQ] >>
491 `preds a^+ <<= univ(:'a inf)` by simp[preds_inj_univ] >>
492 metis_tac [cardleq_TRANS]) >>
493 dsimp[ordMULT_continuous, sup_thm, IMAGE_cardleq_rwt, impI]) >>
494 `?r. b * d + r = a` by metis_tac [ordle_EXISTS_ADD] >>
495 qsuff_tac `r < b` >- metis_tac[] >>
496 spose_not_then strip_assume_tac >>
497 `?bb. b + bb = r` by metis_tac [ordle_EXISTS_ADD] >>
498 `b * d^+ + bb = a` by simp[GSYM ordADD_ASSOC] >>
499 `!c. b * c <= a ==> c <= d` by metis_tac [ordlt_REFL] >>
500 metis_tac [ordlt_SUC, ordle_EXISTS_ADD]
501QED
502
503(* old definition:
504val ordDIVISION = new_specification(
505 "ordDIVISION", ["ordDIV", "ordMOD"],
506 SIMP_RULE (srw_ss()) [SKOLEM_THM, GSYM RIGHT_EXISTS_IMP_THM] ordDIVISION0)
507 *)
508
509(* new definition (by Chun Tian as OpenTheory workarounds) *)
510Theorem ordDIVISION1[local] :
511 !a b:'a ordinal. 0 < b ==> ?c. a = b * FST c + SND c /\ SND c < b
512Proof
513 rpt STRIP_TAC
514 >> STRIP_ASSUME_TAC
515 (SIMP_RULE (srw_ss()) [SKOLEM_THM, GSYM RIGHT_EXISTS_IMP_THM] ordDIVISION0)
516 >> POP_ASSUM (MP_TAC o (Q.SPECL [‘a’, ‘b’]))
517 >> RW_TAC std_ss []
518 >> rename1 ‘g a b < b’
519 >> Q.EXISTS_TAC ‘(f a b,g a b)’ >> rw []
520QED
521
522(* The next 3 theorems are skipped in ordinal.otd *)
523val ordDIVMOD = new_specification(
524 "ordDIVMOD", ["ordDIVMOD"],
525 SIMP_RULE (srw_ss()) [SKOLEM_THM, GSYM RIGHT_EXISTS_IMP_THM] ordDIVISION1);
526
527Definition ordDIV :
528 ordDIV a b = FST (ordDIVMOD a b)
529End
530
531Definition ordMOD :
532 ordMOD a b = SND (ordDIVMOD a b)
533End
534
535(* |- !a b. 0 < b ==> a = b * ordDIV a b + ordMOD a b /\ ordMOD a b < b *)
536Theorem ordDIVISION =
537 REWRITE_RULE [GSYM ordDIV, GSYM ordMOD] ordDIVMOD
538
539(* end of new definition of ordDIV and ordMOD *)
540
541val _ = set_fixity "/" (Infixl 600)
542Overload "/" = ``ordDIV``
543
544val _ = set_fixity "%" (Infixl 650)
545Overload "%" = ``ordMOD``
546
547Theorem ordDIV_UNIQUE:
548 !a b q r. 0 < (b:'a ordinal) /\ a = b*q + r /\ r < b ==> a / b = q
549Proof
550 rpt strip_tac >>
551 `a = b * (a / b) + a % b /\ a % b < b` by metis_tac [ordDIVISION] >>
552 `a / b < q \/ a / b = q \/ q < a / b` by metis_tac [ordlt_trichotomy] >| [
553 `?bb. (q = a/b + bb) /\ 0 < bb`
554 by metis_tac [ordlt_EXISTS_ADD, ordlt_trichotomy, ordlt_ZERO] >>
555 `a = b * (a/b + bb) + r` by metis_tac[] >>
556 `_ = b * (a/b) + b * bb + r` by metis_tac[ordMULT_LDISTRIB] >>
557 `a % b = b * bb + r` by metis_tac [ordADD_ASSOC, ordADD_RIGHT_CANCEL] >>
558 `b * bb + r < b` by metis_tac[] >>
559 `b <= b * bb`
560 by (simp_tac bool_ss [Once (GSYM ordMULT_1R), SimpR ``ordlt``] >>
561 match_mp_tac ordMULT_le_MONO_R >>
562 simp_tac bool_ss [GSYM ORD_ONE, ordlt_SUC_DISCRETE] >>
563 simp[] >> strip_tac >> fs[]) >>
564 `b <= b * bb + r` by metis_tac [ordle_CANCEL_ADDR, ordADD_le_MONO_L,
565 ordle_TRANS],
566
567 `?bb. q + bb = a/b /\ 0 < bb`
568 by metis_tac [ordlt_EXISTS_ADD, ordlt_trichotomy, ordlt_ZERO] >>
569 `a = b * (q + bb) + a % b` by metis_tac[] >>
570 `_ = b * q + b * bb + a % b` by simp[ordMULT_LDISTRIB] >>
571 `r = b * bb + a % b` by metis_tac [ordADD_ASSOC, ordADD_RIGHT_CANCEL] >>
572 `b * bb + a % b < b` by metis_tac[] >>
573 `b <= b * bb`
574 by (simp_tac bool_ss [Once (GSYM ordMULT_1R), SimpR ``ordlt``] >>
575 match_mp_tac ordMULT_le_MONO_R >>
576 simp_tac bool_ss [GSYM ORD_ONE, ordlt_SUC_DISCRETE] >>
577 simp[] >> strip_tac >> fs[]) >>
578 `b <= b * bb + a % b`
579 by metis_tac [ordle_CANCEL_ADDR, ordADD_le_MONO_L, ordle_TRANS]
580 ]
581QED
582
583Theorem ordMOD_UNIQUE:
584 !a b q r. 0 < b /\ a = b * q + r /\ r < b ==> a % b = r
585Proof
586 rpt strip_tac >>
587 `(a = b * (a / b) + a % b) /\ a % b < b` by metis_tac [ordDIVISION] >>
588 `a / b = q` by metis_tac [ordDIV_UNIQUE] >> pop_assum SUBST_ALL_TAC >>
589 qabbrev_tac `r' = a % b` >> fs[]
590QED
591
592(* Exponentiation *)
593val ordEXP_def = new_specification(
594 "ordEXP_def", ["ordEXP"],
595 ord_RECURSION |> INST_TYPE [beta |-> ``:'a ordinal``]
596 |> Q.SPEC `1`
597 |> Q.SPEC `\ap r. r * a`
598 |> Q.SPEC `\a preds. sup preds`
599 |> Q.GEN `a`
600 |> CONV_RULE SKOLEM_CONV
601 |> BETA_RULE
602 |> SIMP_RULE (srw_ss()) [FORALL_AND_THM])
603val _ = export_rewrites ["ordEXP_def"]
604Overload "**" = ``ordEXP``
605
606Theorem ordEXP_1R[simp]:
607 (a:'a ordinal) ** 1 = a
608Proof
609 simp_tac bool_ss [GSYM ORD_ONE, ordEXP_def] >> simp[]
610QED
611
612Theorem ordEXP_1L[simp]:
613 !a:'a ordinal. 1 ** a = 1
614Proof
615 ho_match_mp_tac simple_ord_induction >> simp[] >> qx_gen_tac `a` >>
616 strip_tac >> qsuff_tac `IMAGE ($** 1) (preds a) = {1}` >> simp[] >>
617 simp[EXTENSION] >> asm_simp_tac (srw_ss() ++ CONJ_ss) [] >> metis_tac[]
618QED
619
620Theorem ordEXP_2R:
621 (a:'a ordinal) ** 2 = a * a
622Proof
623 `2 = 1^+` by simp[] >> pop_assum SUBST1_TAC >> simp[]
624QED
625
626Theorem ordEXP_fromNat[simp]:
627 (&x:'a ordinal) ** &n = &(x ** n)
628Proof
629 Induct_on `n` >> simp[arithmeticTheory.EXP]
630QED
631
632Theorem ordEXP_le_MONO_L:
633 !x a b. a <= b ==> a ** x <= b ** x
634Proof
635 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
636 >- (qx_gen_tac `x` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >>
637 strip_tac >> match_mp_tac ordle_TRANS >>
638 qexists_tac `a ** x * b` >> simp[ordMULT_le_MONO_L, ordMULT_le_MONO_R]) >>
639 qx_gen_tac `x` >> strip_tac >> map_every qx_gen_tac [`a`, `b`] >>
640 strip_tac >> simp[predimage_sup_thm, impI] >>
641 qx_gen_tac `d` >> strip_tac >>
642 `a ** d <= b ** d` by simp[] >>
643 `b ** d IN IMAGE ($** b) (preds x)` by (simp[] >> metis_tac[]) >>
644 metis_tac [mklesup sup_thm, ordle_TRANS, IMAGE_cardleq_rwt, preds_inj_univ]
645QED
646
647Theorem ordEXP_ZERO_limit:
648 !x. islimit x ==> 0 ** x = 1
649Proof
650 ho_match_mp_tac simple_ord_induction >> simp[] >>
651 qx_gen_tac `x` >> strip_tac >>
652 qsuff_tac `IMAGE ($** 0) (preds x) = {0; 1}`
653 >- (simp[] >> dsimp[sup_def, impI] >> strip_tac >>
654 DEEP_INTRO_TAC oleast_intro >> simp[] >>
655 conj_tac >- metis_tac [ordlt_REFL] >>
656 qx_gen_tac `a` >> strip_tac >>
657 qsuff_tac `a <= 1` >- metis_tac[ordle_ANTISYM] >>
658 metis_tac[ordlt_REFL]) >>
659 simp[EXTENSION] >> qx_gen_tac `y` >> dsimp[EQ_IMP_THM] >>
660 Tactical.REVERSE (rpt conj_tac)
661 >- (strip_tac >> qexists_tac `0` >> simp[])
662 >- (strip_tac >> qexists_tac `0^+` >> simp[] >>
663 spose_not_then strip_assume_tac >> fs[ordle_lteq]
664 >- metis_tac [ordlt_DISCRETE1, ORD_ONE] >>
665 fs[]) >>
666 qx_gen_tac `z` >> strip_tac >> Cases_on `islimit z` >- metis_tac[] >>
667 `?z0. z = z0^+`
668 by metis_tac [preds_omax_SOME_SUC, option_CASES] >>
669 simp[]
670QED
671
672Theorem ordEXP_ZERO_nonlimit:
673 ~islimit x ==> 0 ** x = 0
674Proof
675 metis_tac [preds_omax_SOME_SUC, option_CASES, ordEXP_def,
676 ordMULT_0R]
677QED
678
679Theorem ordADD_EQ_0[simp]:
680 !y x. (x:'a ordinal) + y = 0 <=> x = 0 /\ y = 0
681Proof
682 ho_match_mp_tac simple_ord_induction >> simp[] >>
683 simp[sup_EQ_0, IMAGE_cardleq_rwt, preds_inj_univ] >>
684 qx_gen_tac `y` >> strip_tac >> qx_gen_tac `x` >>
685 `preds y <> {}` by (strip_tac >> fs[]) >>
686 simp[EXTENSION] >>
687 `y <> 0` by metis_tac [ordlt_REFL] >> simp[] >>
688 qexists_tac `x^+` >> simp[] >> qexists_tac `1` >>
689 metis_tac [ADD1R, islimit_SUC_lt, ORD_ONE]
690QED
691
692Theorem IMAGE_EQ_SING:
693 IMAGE f s = {x} <=> (?y. y IN s) /\ !y. y IN s ==> f y = x
694Proof
695 simp[EXTENSION] >> metis_tac []
696QED
697
698Theorem ordMULT_EQ_0[simp]:
699 !x y. x * y = 0 <=> x = 0 \/ y = 0
700Proof
701 CONV_TAC SWAP_FORALL_CONV >>
702 ho_match_mp_tac simple_ord_induction >> simp[] >>
703 simp_tac (srw_ss() ++ CONJ_ss) [] >> qx_gen_tac `x` >> strip_tac >>
704 simp[sup_EQ_0, IMAGE_cardleq_rwt, preds_inj_univ] >>
705 `preds x <> {} /\ x <> 0` by (rpt strip_tac >> fs[]) >>
706 qx_gen_tac `y` >> eq_tac
707 >- (simp[IMAGE_EQ_SING] >> strip_tac >>
708 pop_assum (qspec_then `1` mp_tac) >> simp[] >>
709 disch_then match_mp_tac >> metis_tac [islimit_SUC_lt, ORD_ONE]) >>
710 simp[IMAGE_EQ_SING] >> metis_tac[]
711QED
712
713Theorem ordEXP_EQ_0:
714 !y x. x ** y = 0 <=> x = 0 /\ ~islimit y
715Proof
716 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
717 >- metis_tac[] >>
718 qx_gen_tac `y` >> strip_tac >>
719 simp[sup_EQ_0, IMAGE_cardleq_rwt, preds_inj_univ] >>
720 simp[IFF_ZERO_lt] >>
721 `preds y <> {}` by (strip_tac >> fs[]) >> simp[] >>
722 simp[IMAGE_EQ_SING] >> qx_gen_tac `x` >> DISJ2_TAC >>
723 qexists_tac `0` >> simp[]
724QED
725
726Theorem ZERO_lt_ordEXP_I:
727 !a x:'a ordinal. 0 < a ==> 0 < a ** x
728Proof
729 metis_tac [IFF_ZERO_lt, ordEXP_EQ_0]
730QED
731
732Theorem ZERO_lt_ordEXP:
733 0 < a ** x <=> 0 < a \/ islimit x
734Proof
735 metis_tac [ordEXP_EQ_0, IFF_ZERO_lt]
736QED
737
738Theorem ordEXP_lt_MONO_R:
739 !y x a:'a ordinal. 1 < a /\ x < y ==> a ** x < a ** y
740Proof
741 ho_match_mp_tac simple_ord_induction >> simp[] >> rpt conj_tac >>
742 qx_gen_tac `y` >> strip_tac >> map_every qx_gen_tac [`x`, `a`]
743 >- (simp[ordlt_SUC_DISCRETE] >> rw[] >| [
744 match_mp_tac ordlt_TRANS >> qexists_tac `a ** y` >> simp[],
745 ALL_TAC
746 ] >> simp_tac bool_ss [SimpL ``ordlt``, Once (GSYM ordMULT_1R)] >>
747 simp[ZERO_lt_ordEXP] >> DISJ1_TAC >>
748 match_mp_tac ordlt_TRANS >> qexists_tac `1` >> simp[]) >>
749 simp[predimage_sup_thm] >> fs[omax_NONE] >>
750 metis_tac[]
751QED
752
753Theorem ordEXP_lt_IFF[simp]:
754 !x y a:'a ordinal. 1 < a ==> (a ** x < a ** y <=> x < y)
755Proof
756 simp[EQ_IMP_THM, ordEXP_lt_MONO_R] >> rpt strip_tac >>
757 spose_not_then strip_assume_tac >> fs[ordle_lteq]
758 >- metis_tac[ordlt_TRANS, ordlt_REFL, ordEXP_lt_MONO_R] >> fs[]
759QED
760
761Theorem ordEXP_le_MONO_R:
762 !x y a. 0 < a /\ x <= y ==> a ** x <= a ** y
763Proof
764 rpt gen_tac >> simp[ordle_lteq] >> rw[] >> Cases_on `a = 1` >- simp[] >>
765 qsuff_tac `1 < a` >- metis_tac [ordEXP_lt_MONO_R] >>
766 spose_not_then strip_assume_tac >> fs[ordle_lteq] >> fs[] >>
767 metis_tac [ORD_ONE, ordlt_DISCRETE1]
768QED
769
770Theorem ordEXP_continuous:
771 !a s:'a ordinal set.
772 0 < a /\ s <<= univ(:'a inf) /\ s <> {} ==>
773 a ** sup s = sup (IMAGE ($** a) s)
774Proof
775 simp[generic_continuity, ordEXP_le_MONO_R]
776QED
777
778Theorem ordEXP_ADD:
779 0 < x ==> x ** (y + z) = x ** y * x ** z
780Proof
781 map_every qid_spec_tac [`x`,`y`,`z`] >>
782 ho_match_mp_tac simple_ord_induction >> simp[ordMULT_ASSOC] >>
783 qx_gen_tac `z` >> strip_tac >> map_every qx_gen_tac [`y`, `x`] >>
784 `preds z <> {}` by (strip_tac >> fs[]) >>
785 simp[ordEXP_continuous, IMAGE_cardleq_rwt, preds_inj_univ,
786 ordMULT_continuous, GSYM IMAGE_COMPOSE] >>
787 simp[combinTheory.o_DEF] >> strip_tac >> AP_TERM_TAC >>
788 simp[EXTENSION] >> metis_tac[]
789QED
790
791Theorem ordEXP_MUL:
792 0 < x ==> x ** (y * z) = (x ** y) ** z
793Proof
794 strip_tac >> map_every qid_spec_tac [`y`, `z`] >>
795 ho_match_mp_tac simple_ord_induction >> simp[ordEXP_ADD] >>
796 qx_gen_tac `z` >> strip_tac >> qx_gen_tac `y` >>
797 `preds z <> {}` by (strip_tac >> fs[]) >>
798 simp[ordEXP_continuous, IMAGE_cardleq_rwt, preds_inj_univ,
799 GSYM IMAGE_COMPOSE] >>
800 simp[combinTheory.o_DEF] >> AP_TERM_TAC >>
801 simp[EXTENSION] >> metis_tac []
802QED
803
804Theorem fixpoints_exist:
805 (!s:'a ordinal set. s <> {} /\ s <<= univ(:'a inf) ==>
806 f (sup s) = sup (IMAGE f s)) /\
807 (!x. x <= f x) ==>
808 !a. ?b. a <= b /\ f b = b
809Proof
810 rpt strip_tac >> qexists_tac `sup { FUNPOW f n a | n | T }` >>
811 `{FUNPOW f n a | n | T} <<= univ(:'a inf)`
812 by (simp[cardleq_def] >>
813 qsuff_tac `?g. SURJ g univ(:'a inf) {FUNPOW f n a | n | T}`
814 >- metis_tac[SURJ_INJ_INV] >>
815 qexists_tac `\x. case x of INL n => FUNPOW f n a
816 | INR n => a` >>
817 dsimp[SURJ_DEF] >> conj_tac
818 >- (simp[sumTheory.FORALL_SUM] >>
819 metis_tac [arithmeticTheory.FUNPOW]) >>
820 qx_gen_tac `n` >> qexists_tac `INL n` >> simp[]) >>
821 conj_tac
822 >- (match_mp_tac suple_thm >> simp[] >> qexists_tac `0` >> simp[]) >>
823 `{ FUNPOW f n a | n | T } <> {}` by simp[EXTENSION] >>
824 simp[] >> match_mp_tac sup_eq_sup >>
825 dsimp[IMAGE_cardleq_rwt] >>
826 `!n. ?m. f (FUNPOW f n a) <= FUNPOW f m a`
827 by (strip_tac >> qexists_tac `SUC n` >>
828 simp[arithmeticTheory.FUNPOW_SUC]) >>
829 `!n. ?m. FUNPOW f n a <= f (FUNPOW f m a)`
830 by (strip_tac >> qexists_tac `n` >> simp[]) >> simp[]
831QED
832
833Theorem x_le_ordEXP_x:
834 !a x. 1 < a ==> x <= a ** x
835Proof
836 gen_tac >> Cases_on `1 < a` >> simp[] >>
837 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac >>
838 qx_gen_tac `x` >> strip_tac
839 >- (qsuff_tac `x < a ** x * a`
840 >- (simp[ordlt_SUC_DISCRETE] >> simp[ordle_lteq] >>
841 metis_tac[ordlt_REFL]) >>
842 qsuff_tac `a ** x < a ** x * a`
843 >- metis_tac[ordle_lteq, ordlt_TRANS] >>
844 SIMP_TAC bool_ss [SimpL ``ordlt``, Once (GSYM ordMULT_1R)] >>
845 simp[ZERO_lt_ordEXP] >> DISJ1_TAC >> match_mp_tac ordlt_TRANS >>
846 qexists_tac `1` >> simp[]) >>
847 `!b. b < x ==> b^+ < x` by metis_tac [islimit_SUC_lt] >>
848 fs[omax_NONE] >> strip_tac >>
849 `?b. b < x /\ sup (IMAGE ($** a) (preds x)) < b` by metis_tac[] >>
850 `!d. d < x ==> a ** d <= b` by metis_tac[predimage_suplt_ELIM] >>
851 `a ** b < a ** b^+` by simp[] >>
852 `a ** b^+ <= b` by metis_tac[] >>
853 `b <= a ** b` by metis_tac[] >>
854 metis_tac[ordlt_TRANS, ordle_lteq, ordlt_REFL]
855QED
856
857Definition epsilon0_def:
858 epsilon0 = oleast x. omega ** x = x
859End
860
861Overload "ε₀" = ``epsilon0``
862
863Theorem epsilon0_fixpoint:
864 omega ** epsilon0 = epsilon0
865Proof
866 simp[epsilon0_def] >> DEEP_INTRO_TAC oleast_intro >> simp[] >>
867 metis_tac [fromNat_lt_omega, ordEXP_continuous, x_le_ordEXP_x,
868 fixpoints_exist]
869QED
870
871Theorem epsilon0_least_fixpoint:
872 !a. a < epsilon0 ==> a < omega ** a /\ omega ** a < epsilon0
873Proof
874 gen_tac >> simp[epsilon0_def] >> DEEP_INTRO_TAC oleast_intro >>
875 metis_tac [epsilon0_fixpoint, x_le_ordEXP_x, ordle_lteq, ordEXP_lt_MONO_R,
876 fromNat_lt_omega]
877QED
878
879val zero_lt_epsilon0 =
880 epsilon0_fixpoint |> SIMP_RULE (srw_ss()) [ASSUME ``epsilon0 = 0``]
881 |> DISCH_ALL
882 |> SIMP_RULE (srw_ss()) [IFF_ZERO_lt]
883
884val one_lt_epsilon0 =
885 MATCH_MP epsilon0_least_fixpoint zero_lt_epsilon0
886 |> SIMP_RULE (srw_ss()) []
887
888(* |- omega < epsilon0 *)
889Theorem omega_lt_epsilon0[simp] =
890 MATCH_MP epsilon0_least_fixpoint one_lt_epsilon0
891 |> SIMP_RULE (srw_ss()) []
892
893Theorem fromNat_lt_epsilon0[simp]:
894 &n < epsilon0
895Proof
896 metis_tac [ordlt_TRANS, fromNat_lt_omega, omega_lt_epsilon0]
897QED
898
899Theorem add_nat_islimit[simp]:
900 0 < n ==> islimit (a + &n) = F
901Proof
902 Induct_on `n` >> simp[]
903QED
904
905Theorem strict_continuity_preserves_islimit:
906 (!s. s <<= univ(:'a inf) /\ s <> {} ==>
907 f (sup s) = sup (IMAGE f s) : 'a ordinal) /\
908 (!x y. x < y ==> f x < f y) /\
909 islimit (a:'a ordinal) /\ a <> 0 ==> islimit (f a)
910Proof
911 strip_tac >> fs[sup_preds_omax_NONE] >>
912 first_assum (fn th => simp_tac (srw_ss()) [SimpRHS, Once (SYM th)]) >>
913 `preds a <> {}`
914 by (strip_tac >> `0 < a` by fs[IFF_ZERO_lt] >> rw[] >> fs[]) >>
915 simp[preds_inj_univ] >>
916 match_mp_tac ordle_ANTISYM >>
917 simp[sup_thm, IMAGE_cardleq_rwt, preds_inj_univ, impI] >> conj_tac
918 >- (qx_gen_tac `b` >> strip_tac >> match_mp_tac ordle_TRANS >>
919 qexists_tac `f a` >> conj_tac >- simp[ordle_lteq] >>
920 Q.UNDISCH_THEN `sup (preds a) = a`
921 (fn th => simp_tac (srw_ss()) [SimpR ``ordlt``, Once (SYM th)]) >>
922 simp[preds_inj_univ]) >>
923 asm_simp_tac (srw_ss() ++ DNF_ss) [] >> qx_gen_tac `x` >> strip_tac >>
924 match_mp_tac suple_thm >> simp[preds_inj_univ]
925QED
926
927Theorem add_omega_islimit[simp]:
928 islimit (a + omega)
929Proof
930 ho_match_mp_tac strict_continuity_preserves_islimit >>
931 simp[omax_preds_omega, ordADD_continuous]
932QED
933
934Theorem islimit_mul_R:
935 !a. islimit a ==> islimit (b * a)
936Proof
937 Cases_on `b = 0` >- simp[] >> fs[IFF_ZERO_lt] >> gen_tac >>
938 Cases_on `a = 0` >- simp[] >> fs[IFF_ZERO_lt] >> strip_tac >>
939 qspec_then `$* b` mp_tac
940 (Q.GEN `f` strict_continuity_preserves_islimit) >> simp[] >>
941 simp[ordMULT_continuous, IFF_ZERO_lt]
942QED
943
944Theorem mul_omega_islimit:
945 islimit (omega * a)
946Proof
947 qspec_then `a` strip_assume_tac ord_CASES >> simp[islimit_mul_R]
948QED
949
950Theorem omega_exp_islimit:
951 0 < a ==> islimit (omega ** a)
952Proof
953 qspec_then `a` strip_assume_tac ord_CASES
954 >- simp[]
955 >- (simp[] >> simp[islimit_mul_R, omax_preds_omega]) >>
956 strip_tac >> ho_match_mp_tac strict_continuity_preserves_islimit >>
957 simp[IFF_ZERO_lt, ordEXP_continuous]
958QED
959
960Theorem expbound_add:
961 !a x y. x < omega ** a /\ y < omega ** a ==> x + y < omega ** a
962Proof
963 ho_match_mp_tac simple_ord_induction >> simp[] >> rpt conj_tac
964 >- metis_tac [IFF_ZERO_lt, ordADD_def]
965 >- (qx_gen_tac `a` >> strip_tac >>
966 simp_tac bool_ss [ordMULT_def,omega_islimit,fromNat_lt_omega] >>
967 simp[predimage_sup_thm] >>
968 map_every qx_gen_tac [`x`, `y`] >>
969 CONV_TAC (LAND_CONV (BINOP_CONV
970 (SIMP_CONV(srw_ss() ++ DNF_ss)[lt_omega]))) >>
971 disch_then (CONJUNCTS_THEN2
972 (Q.X_CHOOSE_THEN `b` strip_assume_tac)
973 (Q.X_CHOOSE_THEN `c` strip_assume_tac)) >>
974 `x + y < omega ** a * &(b + c)`
975 by (simp_tac bool_ss [ordMULT_LDISTRIB, GSYM ordADD_fromNat] >>
976 match_mp_tac ordlte_TRANS >>
977 qexists_tac `x + omega ** a * &c` >> simp[] >>
978 simp[ordADD_weak_MONO]) >>
979 asm_simp_tac(srw_ss() ++ DNF_ss)[] >> qexists_tac `&(b + c)` >>
980 simp[]) >>
981 qx_gen_tac `a` >> strip_tac >>
982 map_every qx_gen_tac [`x`, `y`] >>
983 simp[predimage_sup_thm] >>
984 disch_then (CONJUNCTS_THEN2
985 (Q.X_CHOOSE_THEN `b` strip_assume_tac)
986 (Q.X_CHOOSE_THEN `c` strip_assume_tac)) >>
987 Cases_on `b < c`
988 >- (`omega ** b < omega ** c` by simp[] >>
989 `x < omega ** c` by metis_tac [ordlt_TRANS] >>
990 metis_tac[]) >>
991 `omega ** c <= omega ** b` by simp[] >>
992 `y < omega ** b` by metis_tac [ordlte_TRANS] >>
993 metis_tac[]
994QED
995
996Theorem downduct[local]:
997 (!n. n <= m /\ P (SUC n) ==> P n) /\ P m ==>
998 (!n. n <= m ==> P n)
999Proof
1000 strip_tac >> fs[arithmeticTheory.LESS_EQ_EXISTS, PULL_EXISTS] >>
1001 CONV_TAC SWAP_FORALL_CONV >>
1002 Induct >> rw[] >> simp[] >>
1003 gvs[DECIDE “n + SUC d = d + m <=> m = SUC n”] >>
1004 metis_tac[arithmeticTheory.ADD_COMM]
1005QED
1006
1007Theorem addL_fixpoint_iff:
1008 a + b = b <=> a * omega <= b
1009Proof
1010 eq_tac
1011 >- (simp[omega_islimit, ordMULT_def, EQ_IMP_THM, sup_thm, IMAGE_cardleq_rwt,
1012 preds_inj_univ, lt_omega] >> strip_tac >>
1013 qx_gen_tac `c` >> Cases_on `b < c` >> simp[] >>
1014 qx_gen_tac `d` >> Cases_on `c = a * d` >> simp[] >> qx_gen_tac `m` >>
1015 strip_tac >> rw[] >>
1016 `!n. n <= m ==> b < a * &n` suffices_by
1017 (disch_then (qspec_then `0` mp_tac) >> simp[]) >>
1018 ho_match_mp_tac downduct >> simp[] >>
1019 qx_gen_tac `n`>>
1020 `a * &n + a = a + a * &n` suffices_by metis_tac[ordlt_CANCEL] >>
1021 Induct_on `n` >> simp[] >> metis_tac[ordADD_ASSOC])
1022 >- (simp[ordle_EXISTS_ADD] >>
1023 disch_then (qx_choose_then `c` SUBST_ALL_TAC) >>
1024 simp[ordADD_ASSOC] >>
1025 `a + a * omega = a * (1 + omega)` by simp[ordMULT_LDISTRIB] >>
1026 simp[ordADD_fromNat_omega, omega_islimit])
1027QED
1028
1029(* And so, arithmetic (addition, multiplication and exponentiation) is
1030 closed under epsilon0 *)
1031Theorem ordADD_under_epsilon0:
1032 x < epsilon0 /\ y < epsilon0 ==> x + y < epsilon0
1033Proof
1034 ONCE_REWRITE_TAC [GSYM epsilon0_fixpoint] >>
1035 simp[expbound_add]
1036QED
1037
1038Theorem ordMUL_under_epsilon0:
1039 x < epsilon0 /\ y < epsilon0 ==> x * y < epsilon0
1040Proof
1041 strip_tac >> imp_res_tac epsilon0_least_fixpoint >>
1042 `x * y < omega ** x * omega ** y`
1043 by (match_mp_tac ordlet_TRANS >>
1044 qexists_tac `omega ** x * y` >> simp[ZERO_lt_ordEXP] >>
1045 match_mp_tac ordMULT_le_MONO_L >> simp[ordle_lteq]) >>
1046 `omega ** x * omega ** y = omega ** (x + y)` by simp[ordEXP_ADD] >>
1047 pop_assum SUBST_ALL_TAC >>
1048 qsuff_tac `omega ** (x + y) < epsilon0` >- metis_tac[ordlt_TRANS] >>
1049 metis_tac [epsilon0_fixpoint, ordADD_under_epsilon0, fromNat_lt_omega,
1050 ordEXP_lt_IFF]
1051QED
1052
1053Theorem ordEXP_under_epsilon0:
1054 a < epsilon0 /\ b < epsilon0 ==> a ** b < epsilon0
1055Proof
1056 strip_tac >>
1057 `a < omega ** a` by imp_res_tac epsilon0_least_fixpoint >>
1058 `a ** b <= (omega ** a) ** b` by metis_tac [ordEXP_le_MONO_L, ordle_lteq] >>
1059 `(omega ** a) ** b = omega ** (a * b)` by simp [GSYM ordEXP_MUL] >>
1060 pop_assum SUBST_ALL_TAC >>
1061 `omega ** (a * b) < epsilon0`
1062 by simp[ordEXP_lt_IFF, ordMUL_under_epsilon0,
1063 Once (GSYM epsilon0_fixpoint)] >>
1064 metis_tac [ordlet_TRANS]
1065QED
1066
1067Definition eval_poly_def[simp]:
1068 eval_poly (a:'a ordinal) [] = 0 /\
1069 eval_poly a ((c,e)::t) = a ** e * c + eval_poly a t
1070End
1071
1072Definition is_polyform_def:
1073 (is_polyform (a:'a ordinal) [] <=> T) /\
1074 (is_polyform a [(c,e)] <=> 0 < c /\ c < a) /\
1075 (is_polyform a ((c1,e1) :: (c2,e2) :: t) <=>
1076 0 < c1 /\ c1 < a /\ e2 < e1 /\ is_polyform a ((c2,e2) :: t))
1077End
1078
1079Theorem is_polyform_ELthm:
1080 is_polyform a ces <=>
1081 (!i j. i < j /\ j < LENGTH ces ==> SND (EL j ces) < SND (EL i ces)) /\
1082 (!c e. MEM (c,e) ces ==> 0 < c /\ c < a)
1083Proof
1084 map_every qid_spec_tac [`ces`, `a`] >>
1085 ho_match_mp_tac (theorem "is_polyform_ind") >> simp[is_polyform_def] >>
1086 simp[DISJ_IMP_THM, FORALL_AND_THM] >> rpt strip_tac >>
1087 eq_tac >> simp[] >| [
1088 strip_tac >> ASM_REWRITE_TAC [] >>
1089 map_every qx_gen_tac [`i`, `j`] >>
1090 `i = 0 \/ ?i0. i = SUC i0` by (Cases_on `i` >> simp[])
1091 >- (simp[] >> strip_tac >>
1092 `?j0. j = SUC j0` by (Cases_on `j` >> fs[]) >>
1093 fs[] >>
1094 `j0 = 0 \/ ?j00. j0 = SUC j00` by (Cases_on `j0` >> simp[]) >> simp[] >>
1095 first_x_assum (qspecl_then [`0`, `j0`] mp_tac) >> simp[] >>
1096 metis_tac [ordlt_TRANS]) >>
1097 strip_tac >>
1098 `?j0. j = SUC j0` by (Cases_on `j` >> fs[]) >> fs[] >>
1099 asm_simp_tac (srw_ss() ++ ARITH_ss) [],
1100 rpt strip_tac
1101 >- (first_x_assum (qspecl_then [`0`, `SUC 0`] mp_tac) >> simp[])
1102 >- (first_x_assum (qspecl_then [`SUC i`, `SUC j`] mp_tac) >> simp[])
1103 >- res_tac >> res_tac
1104 ]
1105QED
1106
1107Theorem polyform_exists:
1108 !a:'a ordinal b.
1109 1 < a ==> ?ces. is_polyform a ces /\ b = eval_poly a ces
1110Proof
1111 gen_tac >> Cases_on `1 < a` >> simp[is_polyform_ELthm] >>
1112 `0 < a` by (match_mp_tac ordlt_TRANS >> qexists_tac `1` >> simp[]) >>
1113 ho_match_mp_tac ord_induction >>
1114 qx_gen_tac `b` >> strip_tac >> Cases_on `b = 0`
1115 >- (qexists_tac `[]` >> simp[]) >>
1116 `0 < b /\ 1 <= b` by fs[IFF_ZERO_lt] >>
1117 qabbrev_tac `s = { e | a ** e <= b }` >>
1118 `!e. e IN s <=> a ** e <= b` by simp[Abbr`s`] >>
1119 `s <> {}` by (simp[EXTENSION] >> qexists_tac `0` >> simp[]) >>
1120 `!c. c IN s ==> c < b^+`
1121 by (simp[ordlt_SUC_DISCRETE, GSYM ordle_lteq] >>
1122 metis_tac [x_le_ordEXP_x, ordle_TRANS]) >>
1123 `s <<= univ(:'a inf)`
1124 by (`s <<= preds b^+` by simp[SUBSET_CARDLEQ, SUBSET_DEF] >>
1125 metis_tac [cardleq_TRANS, preds_inj_univ]) >>
1126 qabbrev_tac `E = sup s` >>
1127 `!g. g < E <=> ?d. d IN s /\ g < d` by simp[sup_thm, Abbr`E`] >>
1128 `a ** E <= b`
1129 by dsimp[Abbr`E`, ordEXP_continuous, sup_thm, IMAGE_cardleq_rwt, impI] >>
1130 `b < a ** E^+`
1131 by (spose_not_then strip_assume_tac >>
1132 `E^+ IN s` by simp[] >> `E^+ <= E` by metis_tac [suple_thm] >>
1133 fs[]) >>
1134 qabbrev_tac `c1 = b / a ** E` >>
1135 qabbrev_tac `r = b % a ** E` >>
1136 `0 < a ** E` by simp[ZERO_lt_ordEXP] >>
1137 `b = a ** E * c1 + r /\ r < a ** E` by metis_tac [ordDIVISION] >>
1138 `r < b` by metis_tac [ordlt_TRANS, ordle_lteq] >>
1139 `0 < c1` by (spose_not_then strip_assume_tac >> fs[]) >>
1140 `c1 < a`
1141 by (spose_not_then strip_assume_tac >>
1142 `a ** E * a <= a ** E * c1` by simp[] >>
1143 `a ** E * a + r <= b` by simp[ordADD_le_MONO_L] >>
1144 metis_tac [ordEXP_def, ordle_CANCEL_ADDR, ordle_TRANS]) >>
1145 `?ces. (!i j. i < j /\ j < LENGTH ces ==> SND (EL j ces) < SND (EL i ces)) /\
1146 (!c e. MEM (c,e) ces ==> 0 < c /\ c < a) /\
1147 r = eval_poly a ces` by metis_tac[] >>
1148 qexists_tac `(c1,E) :: ces` >> dsimp[] >> Tactical.REVERSE (rpt conj_tac)
1149 >- metis_tac[] >- metis_tac[] >>
1150 gen_tac >>
1151 `(?i0. i = SUC i0) \/ i = 0` by (Cases_on `i` >> simp[])
1152 >- (gen_tac >> Cases_on `j` >> simp[]) >>
1153 qpat_x_assum `!g. g < E <=> P` (K ALL_TAC) >> simp[] >>
1154 qsuff_tac `0 < LENGTH ces ==> SND (EL 0 ces) < E`
1155 >- (strip_tac >> qx_gen_tac `j` >> strip_tac >>
1156 `j = 0 \/ ?j0. j = SUC j0` by (Cases_on `j` >> simp[]) >> simp[] >>
1157 `j0 < LENGTH ces` by fs[] >>
1158 `0 < LENGTH ces` by decide_tac >>
1159 Cases_on `j0 = 0` >- asm_simp_tac bool_ss [] >>
1160 `0 < j0` by decide_tac >>
1161 metis_tac [ordlt_TRANS]) >>
1162 `ces = [] \/ ?c0 e0 t. ces = (c0,e0)::t`
1163 by metis_tac [pairTheory.pair_CASES, listTheory.list_CASES] >- simp[] >>
1164 simp[] >> (* rts: e0 < E *) spose_not_then strip_assume_tac >>
1165 `r = a ** e0 * c0 + eval_poly a t` by simp[] >>
1166 `a ** E <= a ** e0` by simp[ordEXP_le_MONO_R] >>
1167 `a ** e0 <= a ** e0 * c0`
1168 by (simp_tac bool_ss [SimpR ``ordlt``, Once (GSYM ordMULT_1R)] >>
1169 match_mp_tac ordMULT_le_MONO_R >> simp[IFF_ZERO_lt] >> fs[]) >>
1170 `a ** e0 * c0 <= a ** e0 * c0 + eval_poly a t` by simp[] >>
1171 metis_tac [ordle_TRANS, ordle_lteq, ordlt_REFL, ordlt_TRANS]
1172QED
1173
1174val polyform_def = new_specification(
1175 "polyform_def",
1176 ["polyform"],
1177 SIMP_RULE (srw_ss()) [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM]
1178 polyform_exists);
1179
1180(* Cantor Normal Form - polynomials where the base is omega *)
1181Overload CNF = ``polyform omega``
1182
1183Theorem CNF_thm =
1184 polyform_def |> SPEC ``omega`` |> SIMP_RULE (srw_ss()) []
1185
1186Theorem polyform_0:
1187 1 < a ==> polyform a 0 = []
1188Proof
1189 strip_tac >>
1190 qspecl_then [`a`, `0`] mp_tac polyform_def >> simp[] >>
1191 `polyform a 0 = [] \/ ?c e t. polyform a 0 = (c,e)::t`
1192 by metis_tac[pairTheory.pair_CASES, listTheory.list_CASES]
1193 >- simp[] >>
1194 simp[SimpL ``$==>``] >> strip_tac >> fs[]
1195 >- fs[ordEXP_EQ_0] >>
1196 `0 < c` by metis_tac[is_polyform_ELthm,listTheory.MEM] >>
1197 metis_tac[IFF_ZERO_lt]
1198QED
1199
1200Theorem polyform_EQ_NIL:
1201 1 < a ==> (polyform a x = [] <=> x = 0)
1202Proof
1203 simp[EQ_IMP_THM, polyform_0] >>
1204 rpt strip_tac >>
1205 qspecl_then [`a`, `x`] mp_tac polyform_def >> simp[]
1206QED
1207
1208Theorem is_polyform_CONS_E:
1209 is_polyform a ((c,e)::t) ==> 0 < c /\ c < a /\ is_polyform a t
1210Proof
1211 Cases_on `t` >> simp[is_polyform_def] >> Cases_on `h` >>
1212 simp[is_polyform_def]
1213QED
1214
1215Theorem expbounds[local]:
1216 1 < (a:'a ordinal) /\ y < a ** e /\ c < a /\ e < e' ==>
1217 a ** e * c + y < a ** e'
1218Proof
1219 strip_tac >>
1220 `a ** e * c + y < a ** e * c + a ** e` by simp[] >>
1221 `a ** e * c + a ** e = a ** e * ordSUC c` by simp[] >>
1222 pop_assum SUBST_ALL_TAC >>
1223 `c^+ <= a` by metis_tac [ordlt_DISCRETE1] >>
1224 `a ** e * c^+ <= a ** e * a` by simp[ordMULT_le_MONO_R] >>
1225 `a ** e * a = a ** e^+` by simp[] >> pop_assum SUBST_ALL_TAC >>
1226 `a ** e^+ <= a ** e'`
1227 by (match_mp_tac ordEXP_le_MONO_R >> conj_tac
1228 >- (spose_not_then strip_assume_tac >> fs[]) >>
1229 metis_tac [ordlt_DISCRETE1]) >>
1230 metis_tac [ordlte_TRANS, ordle_TRANS]
1231QED
1232
1233Theorem is_polyform_head_dominates_tail:
1234 1 < a /\ is_polyform a ((c,e)::t) ==> eval_poly a t < a ** e
1235Proof
1236 qsuff_tac
1237 `!a ces. 1 < a /\ is_polyform a ces /\ ces <> [] ==>
1238 eval_poly a (TL ces) < a ** SND (HD ces)`
1239 >- (disch_then (qspecl_then [`a`, `(c,e)::t`] strip_assume_tac) >>
1240 strip_tac >> fs[]) >>
1241 ho_match_mp_tac (theorem "is_polyform_ind") >> simp[is_polyform_def] >>
1242 rpt strip_tac
1243 >- (spose_not_then strip_assume_tac >> fs[] >> fs[ordEXP_EQ_0]) >>
1244 fs[] >> metis_tac[is_polyform_CONS_E, expbounds]
1245QED
1246
1247Theorem cx_lt_x[simp]:
1248 x * c < (x:'a ordinal) <=> 0 < x /\ c = 0
1249Proof
1250 simp_tac bool_ss [SimpLHS, SimpR ``ordlt``, Once (GSYM ordMULT_1R)] >>
1251 simp[] >> metis_tac [IFF_ZERO_lt]
1252QED
1253
1254Theorem explemma[local]:
1255 1 < a /\ a ** e1 * c1 + eval_poly a t1 = a ** e2 * c2 + eval_poly a t2 /\
1256 is_polyform a ((c1,e1)::t1) /\ is_polyform a ((c2,e2)::t2) ==>
1257 e1 <= e2
1258Proof
1259 rpt strip_tac (* e2 < e1 *) >>
1260 `eval_poly a t2 < a ** e2` by metis_tac [is_polyform_head_dominates_tail] >>
1261 imp_res_tac is_polyform_CONS_E >>
1262 `a ** e2 * c2 + eval_poly a t2 < a ** e1` by simp[expbounds] >>
1263 `a ** e1 <= a ** e1 * c1` by (simp[IFF_ZERO_lt] >> rw[] >> fs[]) >>
1264 `a ** e1 * c1 <= a ** e1 * c1 + eval_poly a t1` by simp[] >>
1265 metis_tac[ordlte_TRANS, ordle_TRANS, ordlt_REFL]
1266QED
1267
1268Theorem coefflemma[local]:
1269 1 < a /\ a ** e * c1 + eval_poly a t1 = a ** e * c2 + eval_poly a t2 /\
1270 is_polyform a ((c1,e)::t1) /\ is_polyform a ((c2,e)::t2) ==>
1271 c1 <= c2
1272Proof
1273 rpt strip_tac (* c2 < c1 *) >>
1274 `eval_poly a t2 < a ** e` by metis_tac [is_polyform_head_dominates_tail] >>
1275 imp_res_tac is_polyform_CONS_E >>
1276 `a ** e * c2 + eval_poly a t2 < a ** e * c2 + a ** e` by simp[] >>
1277 `a ** e * c2 + a ** e = a ** e * c2^+` by simp[] >> pop_assum SUBST_ALL_TAC >>
1278 `a ** e * c2^+ <= a ** e * c1` by (simp[] >> metis_tac [ordlt_DISCRETE1]) >>
1279 `a ** e * c1 <= a ** e * c1 + eval_poly a t1` by simp[] >>
1280 metis_tac [ordlte_TRANS, ordle_TRANS, ordlt_REFL]
1281QED
1282
1283Theorem polyform_UNIQUE:
1284 !a b ces.
1285 1 < a /\ is_polyform a ces /\ b = eval_poly a ces ==>
1286 polyform a b = ces
1287Proof
1288 gen_tac >> ho_match_mp_tac ord_induction >> qx_gen_tac `b` >>
1289 strip_tac >> qx_gen_tac `ces1` >> strip_tac >>
1290 `0 < a` by (`0 < 1o` by simp[] >> metis_tac [ordlt_TRANS]) >>
1291 qspecl_then [`a`, `b`] mp_tac polyform_def >>
1292 disch_then (strip_assume_tac o REWRITE_RULE [ASSUME``1<a:'a ordinal``]) >>
1293 `ces1 = [] \/ ?c e t. ces1 = (c,e)::t`
1294 by metis_tac[pairTheory.pair_CASES, listTheory.list_CASES]
1295 >- (pop_assum SUBST_ALL_TAC >> `b = 0` by fs[] >> simp[polyform_0]) >>
1296 pop_assum SUBST_ALL_TAC >>
1297 `0 < c /\ c < a` by metis_tac[listTheory.MEM, is_polyform_ELthm] >>
1298 `b = a ** e * c + eval_poly a t` by fs[] >>
1299 `polyform a b <> []` by simp[polyform_EQ_NIL, IFF_ZERO_lt, ZERO_lt_ordEXP] >>
1300 `?c' e' t'. polyform a b = (c',e')::t'`
1301 by metis_tac [listTheory.list_CASES, pairTheory.pair_CASES] >>
1302 `0 < c' /\ c' < a` by metis_tac [is_polyform_CONS_E] >>
1303 `b = a ** e' * c' + eval_poly a t'` by fs[] >>
1304 `e' = e` by metis_tac [explemma, ordle_ANTISYM] >> pop_assum SUBST_ALL_TAC >>
1305 `c' = c` by metis_tac [coefflemma, ordle_ANTISYM] >> pop_assum SUBST_ALL_TAC>>
1306 `eval_poly a t = eval_poly a t'` by metis_tac [ordADD_RIGHT_CANCEL] >>
1307 qsuff_tac `t = t'` >- simp[] >>
1308 `eval_poly a t < b`
1309 by (`eval_poly a t < a ** e`
1310 by metis_tac [is_polyform_head_dominates_tail] >>
1311 `a ** e <= a ** e * c` by simp[IFF_ZERO_lt, Excl "lift_disj_eq"] >>
1312 `a ** e * c <= a ** e * c + eval_poly a t` by simp[] >>
1313 metis_tac [ordlte_TRANS, ordle_TRANS]) >>
1314 metis_tac [is_polyform_CONS_E]
1315QED
1316
1317Theorem polyform_eval_poly:
1318 1 < a /\ is_polyform a b ==> (polyform a (eval_poly a b) = b)
1319Proof
1320 strip_tac >> match_mp_tac polyform_UNIQUE >> simp[]
1321QED
1322
1323Theorem CNF_nat:
1324 CNF &n = if n = 0 then [] else [(&n,0)]
1325Proof
1326 rw[] >> match_mp_tac polyform_UNIQUE >> rw[is_polyform_def] >> decide_tac
1327QED
1328
1329Overload ordLOG = ``\b x. SND (HD (polyform b x))``
1330Overload olog = ``\x. ordLOG omega x``
1331Theorem ordLOG_correct:
1332 1 < b /\ 0 < x ==> ordEXP b (ordLOG b x) <= x /\
1333 !a. ordLOG b x < a ==> x < ordEXP b a
1334Proof
1335 strip_tac >>
1336 `(polyform b x = []) \/ ?c e t. polyform b x = (c,e) :: t`
1337 by metis_tac [pairTheory.pair_CASES, listTheory.list_CASES]
1338 >- (pop_assum mp_tac >> fs[polyform_EQ_NIL] >> strip_tac >> fs[]) >>
1339 simp[] >>
1340 `is_polyform b (polyform b x) /\ (x = eval_poly b (polyform b x))`
1341 by metis_tac [polyform_def] >>
1342 first_assum SUBST1_TAC >> simp[] >>
1343 `0 < c /\ c < b /\ is_polyform b t` by metis_tac[is_polyform_CONS_E] >>
1344 `c <> 0` by (strip_tac >> fs[]) >>
1345 conj_tac
1346 >- (match_mp_tac ordle_TRANS >> qexists_tac `b ** e * c` >> simp[]) >>
1347 rpt strip_tac >>
1348 (is_polyform_head_dominates_tail
1349 |> Q.INST [`a` |-> `b`, `c` |-> `1`, `e` |-> `a`, `t` |-> `polyform b x`]
1350 |> MP_TAC) >> simp[] >> disch_then match_mp_tac >>
1351 simp[is_polyform_def] >> metis_tac[]
1352QED
1353
1354(* |- 0 < x ==> omega ** olog x <= x /\ !a. olog x < a ==> x < omega ** a *)
1355Theorem olog_correct =
1356 ordLOG_correct |> Q.INST [`b` |-> `omega`] |> SIMP_RULE (srw_ss()) [];
1357
1358
1359
1360Theorem CARD_FINITE_preds:
1361 CARD (preds (&n : 'a ordinal)) = CARD (preds (&n : unit ordinal))
1362Proof
1363 simp[preds_nat, CARD_INJ_IMAGE]
1364QED
1365
1366Theorem csuc_nat:
1367 csuc (fromNat n) = ordSUC (fromNat n)
1368Proof
1369 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
1370 rpt strip_tac >- metis_tac[cardinality_bump_exists] >>
1371 gs[] >> irule ordle_ANTISYM >> rpt strip_tac
1372 >- (gs[preds_lt_PSUBSET] >> qpat_x_assum ‘preds _ <</= preds _’ mp_tac >>
1373 simp[] >>
1374 drule_at (Pos last) CARD_PSUBSET >>
1375 simp[FINITE_preds, GSYM fromNat_SUC, Excl "fromNat_SUC"] >>
1376 simp[] >>
1377 ‘FINITE (preds a)’
1378 by metis_tac[SUBSET_FINITE, FINITE_preds, fromNat_SUC, PSUBSET_DEF] >>
1379 simp[CARD_LE_CARD, FINITE_preds, preds_ordSUC, CARD_FINITE_preds]) >>
1380 first_x_assum drule >>
1381 simp[preds_nat, preds_ordSUC, CARD_LT_CARD, CARD_INJ_IMAGE]
1382QED
1383
1384
1385(* uncountable ordinals *)
1386Type ucinf = “:('a + num -> bool) inf”
1387Type ucord = “:('a + num -> bool) ordinal”
1388
1389
1390Theorem ucinf_uncountable: ~countable univ(:'a ucinf)
1391Proof
1392 simp[SUM_UNIV, UNIV_FUN_TO_BOOL, infinite_pow_uncountable]
1393QED
1394
1395Theorem Unum_cardlt_ucinf: univ(:num) <</= univ(:'a ucinf)
1396Proof
1397 simp[cardlt_lenoteq] >> conj_tac
1398 >- (simp[cardleq_def] >> qexists_tac `INL` >> simp[INJ_INL]) >>
1399 strip_tac >> drule countable_cardeq >>
1400 simp[ucinf_uncountable, num_countable] >> strip_tac >>
1401 resolve_then Any drule UNIV_fun_exp (iffLR countable_cardeq) >>
1402 simp[countable_setexp, SUM_UNIV]
1403QED
1404
1405Theorem Unum_cardle_ucinf: univ(:num) <<= univ(:'a ucinf)
1406Proof
1407 simp[cardleq_lteq, Unum_cardlt_ucinf]
1408QED
1409
1410Theorem ucord_sup_exists_lemma:
1411 { a:'a ucord | countableOrd a } <<= univ(:'a ucinf)
1412Proof
1413 spose_not_then assume_tac >> fs[cardlt_lenoteq] >>
1414 `?f. INJ f univ(:'a ucinf) {a:'a ucord | countableOrd a}`
1415 by metis_tac[cardleq_def] >>
1416 `(!u. countableOrd (f u)) /\ (!u v. f u = f v <=> u = v)`
1417 by fs[INJ_IFF] >>
1418 qabbrev_tac `fU = IMAGE f univ(:'a ucinf)` >>
1419 `fU <<= univ(:'a ucinf)` by simp[Abbr`fU`, IMAGE_cardleq] >>
1420 drule_then assume_tac sup_thm >>
1421 Cases_on `countableOrd (sup fU)`
1422 >- (`!u. f u <= sup fU`
1423 by (gen_tac >> match_mp_tac suple_thm >> simp[Abbr`fU`]) >>
1424 qsuff_tac `univ(:'a ucinf) <<= preds (sup fU)`
1425 >- (strip_tac >>
1426 `preds (sup fU) <<= univ(:num)` by fs[countable_thm] >>
1427 drule_all cardleq_TRANS >>
1428 REWRITE_TAC [GSYM countable_thm, ucinf_uncountable]) >>
1429 Cases_on `?u. f u = sup fU`
1430 >- (pop_assum strip_assume_tac >>
1431 `!v. v <> u ==> f v < sup fU` by metis_tac[ordle_lteq] >>
1432 qabbrev_tac `U0 = univ(:'a ucinf) DELETE u` >>
1433 `univ(:'a ucinf) = u INSERT U0`
1434 by metis_tac[INSERT_DELETE, IN_UNIV] >>
1435 `U0 =~ univ(:'a ucinf)`
1436 by metis_tac[finite_countable, FINITE_DELETE, ucinf_uncountable,
1437 cardeq_SYM, CARDEQ_INSERT_RWT] >>
1438 qsuff_tac `U0 <<= preds (sup fU)`
1439 >- metis_tac[CARDEQ_CARDLEQ, cardeq_REFL] >>
1440 simp[cardleq_def] >> qexists_tac `f` >>
1441 simp[INJ_DEF, Abbr`U0`]) >>
1442 pop_assum (fn th => `!u. f u < sup fU` by metis_tac[ordle_lteq, th]) >>
1443 simp[cardleq_def] >> qexists_tac `f` >> simp[INJ_DEF]) >>
1444 `{ a:'a ucord | countableOrd a } <<= preds (sup fU)`
1445 by (match_mp_tac SUBSET_CARDLEQ >> simp[SUBSET_DEF] >>
1446 qx_gen_tac `c` >> strip_tac >>
1447 spose_not_then assume_tac >>
1448 `sup fU <= c` by metis_tac[] >>
1449 `preds (sup fU) SUBSET preds c`
1450 by (simp[SUBSET_DEF] >> metis_tac [ordlte_TRANS]) >>
1451 metis_tac [subset_countable]) >>
1452 qsuff_tac `preds (sup fU) <<= univ(:'a ucinf)`
1453 >- metis_tac [cardleq_ANTISYM, cardleq_TRANS] >>
1454 simp[preds_sup, dclose_BIGUNION] >>
1455 match_mp_tac CARD_BIGUNION >>
1456 dsimp[IMAGE_cardleq_rwt] >>
1457 dsimp[Abbr`fU`] >>
1458 metis_tac[countable_thm, cardleq_TRANS, Unum_cardle_ucinf]
1459QED
1460
1461Definition omega1_def:
1462 omega1 : 'a ucord = sup { a | countableOrd a }
1463End
1464Overload "ω₁" = “omega1”
1465
1466Theorem x_lt_omega1_countable: x < omega1 <=> countableOrd x
1467Proof
1468 simp[omega1_def, sup_thm, ucord_sup_exists_lemma, EQ_IMP_THM] >>
1469 rpt strip_tac >- metis_tac[countableOrds_dclosed] >>
1470 qexists_tac `x^+` >> simp[preds_ordSUC]
1471QED
1472
1473(* |- ~countableOrd omega1 *)
1474Theorem omega1_not_countable =
1475 x_lt_omega1_countable |> Q.INST[`x` |-> `omega1`] |> SIMP_RULE (srw_ss()) []
1476
1477Theorem preds_omega_UNIV:
1478 preds omega =~ univ(:num)
1479Proof
1480 simp[cardeq_def] >>
1481 ONCE_REWRITE_TAC [BIJ_SYM] >>
1482 simp[BIJ_DEF, INJ_IFF, SURJ_DEF, lt_omega, PULL_EXISTS] >>
1483 qexists_tac ‘fromNat’ >> simp[]
1484QED
1485
1486Theorem preds_omega_lt_preds_omega1:
1487 preds omega <</= preds (omega1 : ('a + num -> bool) ordinal)
1488Proof
1489 assume_tac omega1_not_countable >>
1490 gs[countable_thm] >>
1491 resolve_then (Pos hd) (resolve_then (Pos hd) irule cardeq_REFL)
1492 preds_omega_UNIV (iffRL CARD_LT_CONG) >> simp[]
1493QED
1494
1495Theorem csuc_omega:
1496 csuc omega = omega1
1497Proof
1498 simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >> conj_tac
1499 >- irule_at Any preds_omega_lt_preds_omega1 >>
1500 rpt strip_tac >> irule ordle_ANTISYM >> CCONTR_TAC >> gs[]
1501 >- (rename [‘a < omega1’, ‘preds omega <</= preds a’] >>
1502 gs[x_lt_omega1_countable, countable_thm] >>
1503 metis_tac[CARD_LE_CONG, cardeq_REFL, preds_omega_UNIV]) >>
1504 first_x_assum drule >> simp[preds_omega_lt_preds_omega1]
1505QED
1506
1507(* ----------------------------------------------------------------------
1508 Connection to topological notions
1509 ---------------------------------------------------------------------- *)
1510
1511Definition ival_def:
1512 ival (a:'a ordinal) b = { e | a < e /\ e < b }
1513End
1514
1515(* including rays (2nd disj'n) lets the space cover all ordinals (incl. 0). *)
1516Theorem order_topology_exists:
1517 istopology { s | !e. e IN s ==>
1518 (?a:'a ordinal b. e IN ival a b /\ ival a b SUBSET s) \/
1519 ?b. e < b /\ !d. d < b ==> d IN s }
1520Proof
1521 simp[istopology, PULL_EXISTS, DISJ_IMP_THM, FORALL_AND_THM] >> rw[]
1522 >- (rpt $ first_x_assum dxrule >> rpt strip_tac >~
1523 [‘ival _ _ SUBSET s /\ ival _ _ SUBSET t’, ‘ival a b SUBSET s’,
1524 ‘ival x y SUBSET t’]
1525 >- (disj1_tac >>
1526 wlog_tac ‘a <= x’ [‘a’, ‘b’, ‘x’, ‘y’, ‘s’, ‘t’]
1527 >- (gvs[] >> metis_tac[ordle_lteq]) >>
1528 qexistsl_tac [‘x’, ‘if y <= b then y else b’] >>
1529 rw[] >> gvs[ival_def, SUBSET_DEF] >>
1530 metis_tac[ordlet_TRANS, ordlte_TRANS, ordlt_TRANS]) >~
1531 [‘ival _ _ SUBSET A /\ ival _ _ SUBSET B’, ‘_ < a ==> _ IN A’,
1532 ‘_ < b ==> _ IN B’]
1533 >- (disj2_tac >> qexists_tac ‘if a < b then a else b’ >> rw[] >>
1534 metis_tac[ordlt_TRANS, ordlte_TRANS]) >>
1535 rename [‘ival a b SUBSET A’, ‘e < c’] >>
1536 disj1_tac >> qexistsl_tac [‘a’, ‘if b < c then b else c’] >> rw[] >>
1537 gvs[ival_def, SUBSET_DEF] >> metis_tac[ordlte_TRANS, ordlt_TRANS]) >>
1538 qpat_x_assum ‘_ SUBSET _’ mp_tac >>
1539 simp[SUBSET_DEF, SimpL “$==>”] >> disch_then drule >> simp[] >>
1540 disch_then drule >> strip_tac >> metis_tac[SUBSET_BIGUNION_SUBSET_I]
1541QED
1542
1543Definition ordlt_top_def:
1544 ordlt_top =
1545 topology { s | !e. e IN s ==>
1546 (?a:'a ordinal b. e IN ival a b /\ ival a b SUBSET s) \/
1547 ?b. e < b /\ !d. d < b ==> d IN s }
1548End
1549
1550Theorem open_in_ordlt:
1551 open_in ordlt_top s <=>
1552 !e. e IN s ==> (?a:'a ordinal b. e IN ival a b /\ ival a b SUBSET s) \/
1553 ?b. e < b /\ !d. d < b ==> d IN s
1554Proof
1555 simp[topology_tybij |> cj 2 |> iffLR, order_topology_exists, ordlt_top_def]
1556QED
1557
1558Theorem topspace_ordlt_top[simp]:
1559 topspace ordlt_top = UNIV
1560Proof
1561 simp[topspace, EXTENSION, open_in_ordlt] >> qx_gen_tac ‘a’ >>
1562 qexists_tac ‘{ e | e < ordSUC a }’ >> simp[] >> metis_tac[]
1563QED
1564
1565Theorem limpt_islimit:
1566 limpt ordlt_top a (preds a) <=> islimit a /\ a <> 0
1567Proof
1568 simp[limpt_thm, EQ_IMP_THM] >> rpt strip_tac >> gvs[]
1569 >- (Cases_on ‘a’ using ord_CASES >> simp[] >>
1570 rename [‘ordSUC a IN _’] >>
1571 pop_assum $ qspec_then ‘ival a (ordSUC (ordSUC a))’ mp_tac >> simp[] >>
1572 rpt strip_tac >~
1573 [‘open_in’]
1574 >- (simp[open_in_ordlt] >> metis_tac[SUBSET_REFL]) >>
1575 simp[ival_def] >>
1576 rename [‘b = ordSUC a’] >> Cases_on ‘b = ordSUC a’ >> simp[] >>
1577 ‘b < ordSUC a \/ ordSUC a < b’ by metis_tac[ordlt_trichotomy] >>
1578 simp[] >> gs[ordlt_SUC_DISCRETE, ordle_lteq])
1579 >- (pop_assum mp_tac >> simp[] >> qexists_tac ‘{ a | a < 1 }’ >>
1580 simp[open_in_ordlt] >> metis_tac[]) >>
1581 gs[open_in_ordlt] >> first_x_assum $ drule_then strip_assume_tac >~
1582 [‘a IN ival x y’, ‘ival x y SUBSET A’]
1583 >- (gs[SUBSET_DEF, ival_def] >>
1584 ‘ordSUC x < a’ by metis_tac[islimit_SUC_lt] >>
1585 ‘ordSUC x IN A’ by metis_tac[ordlt_SUC, ordlt_TRANS] >>
1586 metis_tac[ordlt_REFL]) >>
1587 qexists_tac ‘0’ >> simp[] >>
1588 metis_tac[ordleq0, ordlt_TRANS]
1589QED
1590
1591Theorem open_sing_nonlimit:
1592 open_in ordlt_top {x} <=> ~islimit x \/ x = 0
1593Proof
1594 qspec_then ‘x’ strip_assume_tac ord_CASES >> simp[] >~
1595 [‘open_in _ {0}’]
1596 >- (simp[open_in_ordlt] >> disj2_tac >> qexists_tac ‘1’ >>
1597 simp[ordlt_fromNat, PULL_EXISTS]) >~
1598 [‘open_in _ {ordSUC a}’]
1599 >- (simp[open_in_ordlt] >> disj1_tac >>
1600 qexistsl_tac [‘a’, ‘ordSUC (ordSUC a)’] >>
1601 simp[ival_def, SUBSET_DEF] >>
1602 qx_gen_tac ‘b’ >> Cases_on ‘b = ordSUC a’ >> simp[] >>
1603 ‘b < ordSUC a \/ ordSUC a < b’ by metis_tac[ordlt_trichotomy] >>
1604 simp[] >> CCONTR_TAC >> gs[ordlt_SUC_DISCRETE, ordle_lteq] >>
1605 metis_tac[ordlt_TRANS, ordlt_REFL]) >>
1606 ‘x <> 0’ by (strip_tac >> gvs[]) >> simp[open_in_ordlt] >>
1607 rw[] >> simp[ival_def, SUBSET_DEF] >~
1608 [‘x <= a’, ‘b <= x’]
1609 >- (Cases_on ‘x <= a’ >> gs[] >>
1610 Cases_on ‘b <= x’ >> gs[] >>
1611 ‘ordSUC a < x’ by simp[islimit_SUC_lt] >> qexists_tac ‘ordSUC a’ >>
1612 simp[] >> metis_tac[ordlt_TRANS, ordlt_REFL]) >>
1613 rename [‘a <= x’, ‘_ <> x’] >>
1614 Cases_on ‘x < a’ >> simp[] >> qexists_tac ‘0’ >>
1615 metis_tac[ordleq0, ordlt_TRANS]
1616QED
1617
1618Theorem rays_open:
1619 open_in ordlt_top { x | x < a } /\
1620 open_in ordlt_top { x | a < x }
1621Proof
1622 conj_tac >- (simp[open_in_ordlt] >> metis_tac[]) >>
1623 qabbrev_tac ‘k = { ival a b | b | T}’ >>
1624 ‘!s. s IN k ==> open_in ordlt_top s’
1625 by (simp[Abbr‘k’, open_in_ordlt, PULL_EXISTS] >>
1626 metis_tac[SUBSET_REFL]) >>
1627 ‘{ x | a < x } = BIGUNION k’ suffices_by metis_tac[OPEN_IN_BIGUNION] >>
1628 simp[Once EXTENSION, Abbr‘k’, PULL_EXISTS, ival_def] >>
1629 metis_tac[ordlt_SUC]
1630QED
1631
1632
1633Theorem closed_sing:
1634 closed_in ordlt_top {x}
1635Proof
1636 simp[closed_in] >>
1637 ‘UNIV DIFF {x} = {y | y < x} UNION {y | x < y}’
1638 by (simp[EXTENSION] >> metis_tac[ordlt_trichotomy, ordlt_REFL]) >>
1639 simp[OPEN_IN_UNION, rays_open]
1640QED
1641
1642