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