ordinalNotationScript.sml
1Theory ordinalNotation
2Ancestors
3 num prim_rec arithmetic
4Libs
5 IndDefLib
6
7val _ = numLib.temp_prefer_num();
8
9(*---------------------------------------------------------------------------*)
10(* Functionality discussed with Matt Kaufmann *)
11(*---------------------------------------------------------------------------*)
12
13fun DISPOSE_TAC q = Q.PAT_X_ASSUM q (K ALL_TAC);
14
15fun DROP_ASSUMS_TAC [] (asl,c) = REPEAT (WEAKEN_TAC (K true)) (asl,c)
16 | DROP_ASSUMS_TAC nlist (asl,c) =
17 let val tmlist = map (fn n => el (n+1) (rev asl)) nlist
18 in MAP_EVERY (fn tm => UNDISCH_THEN tm (K ALL_TAC)) tmlist
19 end (asl,c);
20
21fun DROP_ASSUM n = DROP_ASSUMS_TAC [n];
22
23val meter = Count.mk_meter();
24
25(*---------------------------------------------------------------------------*)
26(* Start the theory *)
27(*---------------------------------------------------------------------------*)
28
29(*---------------------------------------------------------------------------*)
30(* Raw syntax of ordinals *)
31(*---------------------------------------------------------------------------*)
32
33val _ = set_fixity "=" (Infix(NONASSOC, 100))
34Datatype:
35 osyntax = End num | Plus osyntax num osyntax
36End
37
38val osyntax_11 = TypeBase.one_one_of ``:osyntax``;
39val osyntax_distinct = TypeBase.distinct_of ``:osyntax``;
40
41(*---------------------------------------------------------------------------*)
42(* And operations over osyntax. *)
43(*---------------------------------------------------------------------------*)
44
45Definition expt_def:
46 (expt (End _) = End 0) /\
47 (expt (Plus e k t) = e)
48End
49
50Definition coeff_def:
51 (coeff (End x) = x) /\
52 (coeff (Plus e k t) = k)
53End
54
55Definition finp_def:
56 (finp (End _) = T) /\
57 (finp (Plus _ _ _) = F)
58End
59
60Definition tail_def:
61 tail (Plus e k t) = t
62End
63
64Definition rank_def:
65 (rank (End _) = 0) /\
66 (rank (Plus e k t) = 1 + rank e)
67End
68
69val ord_ss = arith_ss ++ rewrites
70 [expt_def, coeff_def, finp_def, tail_def, rank_def, GSYM IMP_DISJ_THM];
71
72(*---------------------------------------------------------------------------*)
73(* Definition of less-than on osyntax *)
74(*---------------------------------------------------------------------------*)
75
76val (oless_rules, oless_ind, oless_cases) =
77 Hol_reln
78 `(!k1 k2. k1 < k2 ==> oless (End k1) (End k2)) /\
79 (!k1 e2 k2 t2. oless (End k1) (Plus e2 k2 t2)) /\
80 (!e1 k1 t1 e2 k2 t2. oless e1 e2 ==> oless (Plus e1 k1 t1) (Plus e2 k2 t2)) /\
81 (!e1 k1 t1 e2 k2 t2. (e1=e2) /\ k1<k2
82 ==> oless (Plus e1 k1 t1) (Plus e2 k2 t2)) /\
83 (!e1 k1 t1 e2 k2 t2. (e1=e2) /\ (k1=k2) /\ oless t1 t2
84 ==> oless (Plus e1 k1 t1) (Plus e2 k2 t2))`;
85
86Theorem oless_strong_ind = theorem "oless_strongind";
87
88Theorem oless_End_End:
89 !k1 k2. oless (End k1) (End k2) ==> k1 < k2
90Proof
91 RW_TAC ord_ss [Once oless_cases]
92QED
93
94(*---------------------------------------------------------------------------*)
95(* Version of oless suitable for ML execution. *)
96(*---------------------------------------------------------------------------*)
97
98Theorem oless_equations:
99 (oless (End m) (End n) <=> m < n) /\
100 (oless (End m) (Plus e k t) <=> T) /\
101 (oless (Plus e k t) (End m) <=> F) /\
102 (oless (Plus e1 k1 t1) (Plus e2 k2 t2) <=>
103 if oless e1 e2 then T else
104 if (e1 = e2) /\ k1 < k2 then T else
105 if (e1 = e2) /\ (k1 = k2) /\ oless t1 t2 then T
106 else F)
107Proof
108 SIMP_TAC arith_ss [EQ_IMP_THM] THEN REPEAT CONJ_TAC THENL
109 [RW_TAC arith_ss [Once oless_cases],
110 METIS_TAC [oless_rules],
111 METIS_TAC [oless_rules],
112 RW_TAC arith_ss [Once oless_cases] THEN METIS_TAC[],
113 RW_TAC arith_ss [Once oless_cases] THEN METIS_TAC[],
114 METIS_TAC [oless_rules]]
115QED
116
117(*---------------------------------------------------------------------------*)
118(* Subset of osyntax things that are ordinals in Cantor Normal Form *)
119(*---------------------------------------------------------------------------*)
120
121val (is_ord_rules, is_ord_ind, is_ord_cases) =
122 Hol_reln
123 `(!k. is_ord (End k)) /\
124 (!e k t. is_ord e /\ ~(e = End 0) /\ 0 < k /\ is_ord t /\ oless (expt t) e
125 ==> is_ord (Plus e k t))`;
126
127Theorem is_ord_strong_ind = theorem "is_ord_strongind"
128
129Theorem decompose_plus:
130 !e k t. is_ord (Plus e k t) ==>
131 is_ord e /\ ~(e = End 0) /\ 0 < k /\ is_ord t /\ oless (expt t) e
132Proof
133 METIS_TAC [is_ord_cases,osyntax_distinct,osyntax_11]
134QED
135
136(*---------------------------------------------------------------------------*)
137(* Functional version of is_ord *)
138(*---------------------------------------------------------------------------*)
139
140Theorem is_ord_equations:
141 (is_ord (End k) <=> T) /\
142 (is_ord (Plus e k t) <=>
143 is_ord e /\ ~(e = End 0) /\ 0 < k /\ is_ord t /\ oless (expt t) e)
144Proof
145 METIS_TAC [is_ord_rules,decompose_plus]
146QED
147
148val is_ord_End = CONJUNCT1 is_ord_rules;
149
150val ord_ss = ord_ss ++ rewrites [is_ord_End];
151
152(*---------------------------------------------------------------------------*)
153(* Closure properties of ordinal operations. *)
154(*---------------------------------------------------------------------------*)
155
156Theorem is_ord_expt_closed:
157 !x. is_ord x ==> is_ord (expt x)
158Proof
159 Induct THEN RW_TAC ord_ss [] THEN METIS_TAC [decompose_plus]
160QED
161
162Theorem is_ord_tail_closed:
163 !x. ~finp x /\ is_ord x ==> is_ord (tail x)
164Proof
165Induct THEN RW_TAC ord_ss [] THEN METIS_TAC [decompose_plus]
166QED
167
168Theorem is_ord_downclosed:
169 is_ord (Plus w k t) ==> is_ord w /\ is_ord t
170Proof
171 METIS_TAC [is_ord_cases,osyntax_11,osyntax_distinct]
172QED
173
174Theorem is_ord_coeff_pos:
175 !x. ~finp(x) /\ is_ord x ==> 0 < coeff x
176Proof
177Induct THEN RW_TAC ord_ss [] THEN METIS_TAC [decompose_plus]
178QED
179
180Theorem rank_expt:
181 !x n. is_ord(x) /\ (rank x = SUC n) ==> (rank (expt x) = n)
182Proof
183 Cases THEN RW_TAC ord_ss []
184QED
185
186(*---------------------------------------------------------------------------*)
187(* oless is antireflexive *)
188(*---------------------------------------------------------------------------*)
189
190Theorem oless_antirefl_lem[local]:
191 !x y. oless x y ==> (x=y) /\ is_ord x ==> F
192Proof
193 HO_MATCH_MP_TAC oless_ind
194 THEN RW_TAC ord_ss [] THEN METIS_TAC[decompose_plus]
195QED
196
197Theorem oless_antirefl:
198 !x. is_ord x ==> ~oless x x
199Proof
200 METIS_TAC[oless_antirefl_lem]
201QED
202
203(*---------------------------------------------------------------------------*)
204(* oless is antisymmetric *)
205(*---------------------------------------------------------------------------*)
206
207Theorem oless_antisym_lem[local]:
208 !x y. oless x y ==> is_ord x /\ is_ord y ==> ~oless y x
209Proof
210 HO_MATCH_MP_TAC oless_strong_ind THEN RW_TAC std_ss []
211 THEN ONCE_REWRITE_TAC [oless_cases]
212 THEN RW_TAC ord_ss []
213 THEN METIS_TAC [oless_antirefl,decompose_plus]
214QED
215
216Theorem oless_antisym:
217 !x y. is_ord x /\ is_ord y /\ oless x y ==> ~oless y x
218Proof
219 METIS_TAC [oless_antisym_lem]
220QED
221
222(*---------------------------------------------------------------------------*)
223(* trichotomy and transitivity of oless ... not proved *)
224(*---------------------------------------------------------------------------*)
225(*
226val oless_trichotomy =
227 ``!x y. is_ord x /\ is_ord y ==> oless x y \/ (x=y) \/ oless y x``;
228
229val oless_transitivity =
230 ``!x y. is_ord x /\ is_ord y /\ is_ord x /\ oless x y /\ oless y z ==> oless x z``
231*)
232
233(*---------------------------------------------------------------------------*)
234(* rank less implies oless *)
235(*---------------------------------------------------------------------------*)
236
237Theorem rank_less_imp_oless:
238 !x y. is_ord x /\ is_ord y /\ rank x < rank y ==> oless x y
239Proof
240 measureInduct_on `rank x`
241 THEN Cases_on `x` THEN Cases_on `y`
242 THEN FULL_SIMP_TAC ord_ss [] THENL
243 [METIS_TAC [oless_rules],
244 RW_TAC ord_ss [] THEN
245 METIS_TAC [DECIDE``x < x + 1n``,decompose_plus,oless_rules]]
246QED
247
248(*---------------------------------------------------------------------------*)
249(* oless implies rank leq. *)
250(*---------------------------------------------------------------------------*)
251
252Theorem oless_imp_rank_leq:
253 !x y. is_ord x /\ is_ord y /\ oless x y ==> rank x <= rank y
254Proof
255 RW_TAC ord_ss [] THEN SPOSE_NOT_THEN ASSUME_TAC THEN
256 `rank y < rank x` by DECIDE_TAC THEN
257 METIS_TAC [rank_less_imp_oless,oless_antisym]
258QED
259
260(*---------------------------------------------------------------------------*)
261(* Ordinals of rank 0 are essentially natural numbers *)
262(*---------------------------------------------------------------------------*)
263
264Theorem rank_0_End:
265 !x. (rank x = 0) = ?n. x = End n
266Proof
267 Cases THEN RW_TAC ord_ss [rank_def]
268QED
269
270Theorem rank_finp:
271 !x. (rank x = 0) = finp x
272Proof
273 Cases THEN RW_TAC ord_ss [rank_def,finp_def]
274QED
275
276Theorem rank_positive_exists:
277 !x. 0 < rank x <=> ?e c t. x = Plus e c t
278Proof
279 Cases THEN RW_TAC ord_ss [rank_def]
280QED
281
282Theorem rank_positive:
283 !x. 0 < rank x <=> (x = Plus (expt x) (coeff x) (tail x))
284Proof
285 Cases THEN RW_TAC ord_ss [rank_def,expt_def, coeff_def, tail_def]
286QED
287
288Theorem rank_positive_expt:
289 !x n. (rank x = SUC n) ==> (rank(expt x) = n)
290Proof
291 Cases THEN RW_TAC ord_ss [rank_def,expt_def]
292QED
293
294(*---------------------------------------------------------------------------*)
295(* Proper subterms of an ordinal are oless than the ordinal *)
296(*---------------------------------------------------------------------------*)
297
298Theorem oless_expt:
299 !e k t. is_ord (Plus e k t) ==> oless e (Plus e k t)
300Proof
301 REPEAT STRIP_TAC THEN
302 MATCH_MP_TAC rank_less_imp_oless THEN
303 RW_TAC ord_ss [] THEN
304 METIS_TAC [is_ord_downclosed]
305QED
306
307Theorem oless_tail_lem[local]:
308 !x. is_ord x ==> ~finp x ==> oless (tail x) x
309Proof
310 HO_MATCH_MP_TAC is_ord_ind THEN
311 RW_TAC ord_ss [tail_def,finp_def] THEN
312 Cases_on `x'` THEN FULL_SIMP_TAC ord_ss [finp_def,tail_def,expt_def] THEN
313 METIS_TAC [oless_rules]
314QED
315
316Theorem oless_tail:
317 !x. is_ord x /\ ~finp x ==> oless (tail x) x
318Proof
319 METIS_TAC [oless_tail_lem]
320QED
321
322
323(*---------------------------------------------------------------------------*)
324(* A non-empty set of ordinals of rank at most SUC n has either got at least *)
325(* one element of rank <= n or all are of rank = n+1. *)
326(*---------------------------------------------------------------------------*)
327
328Theorem split_lem[local]:
329 !P n. (?x. P x) /\ (!x. P x ==> rank x <= SUC n) ==>
330 (?x. P x /\ rank x <= n) \/ (!x. P x ==> (rank x = SUC n))
331Proof
332 RW_TAC ord_ss [] THEN SPOSE_NOT_THEN ASSUME_TAC THEN RW_TAC arith_ss [] THEN
333 STRIP_ASSUME_TAC
334 (Q.SPECL [`rank x'`, `n`]
335 (DECIDE ``!x y. x <= y \/ (x = SUC y) \/ (x > SUC y)``)) THENL
336 [METIS_TAC [], RES_TAC THEN DECIDE_TAC]
337QED
338
339(*---------------------------------------------------------------------------*)
340(* Every n.e. set of ordinals of rank <= n has an oless-minimal element *)
341(* imples every n.e. set having at least one ordinal of rank <= n has an *)
342(* oless-minimal element. *)
343(*---------------------------------------------------------------------------*)
344
345Theorem stronger[local]:
346 (!n. !P:osyntax->bool. !x.
347 P x /\ (!x. P x ==> is_ord(x) /\ rank(x) <= n) ==>
348 ?m. is_ord m /\ P m /\ rank m <= n /\
349 !y. is_ord y /\ rank y <= n /\ oless y m ==> ~P y)
350 ==>
351 (!n. !P:osyntax->bool.
352 (?x. is_ord x /\ P x /\ rank x <= n) ==>
353 ?m. is_ord m /\ P m /\ rank m <= n /\
354 !y. is_ord y /\ rank y <= n /\ oless y m ==> ~P y)
355Proof
356 RW_TAC std_ss [] THEN
357 Q.PAT_X_ASSUM `$!M`
358 (MP_TAC o Q.SPEC `\a. P a /\ is_ord a /\ rank a <= n` o Q.ID_SPEC) THEN
359 DISCH_THEN (MP_TAC o Q.ID_SPEC) THEN RW_TAC std_ss [] THEN METIS_TAC []
360QED
361
362
363(*---------------------------------------------------------------------------*)
364(* Main lemma: every non-empty set having at least one ordinal of rank <= n *)
365(* has an oless-minimal element. The proof is by induction on n. *)
366(*---------------------------------------------------------------------------*)
367
368val _ = Parse.hide "S"; (* used as a variable in the following proof *)
369
370Theorem lemma:
371 !n. !P:osyntax->bool.
372 (?x. is_ord x /\ P x /\ rank x <= n) ==>
373 ?m. is_ord m /\ P m /\ rank m <= n /\
374 !y. is_ord y /\ rank y <= n /\ oless y m ==> ~P y
375Proof
376
377 MATCH_MP_TAC stronger THEN Induct THENL
378
379(*---------------------------------------------------------------------------*)
380(* Base case .... everything in P has rank 0, so are natural numbers. *)
381(*---------------------------------------------------------------------------*)
382
383[
384RW_TAC ord_ss [] THEN
385`?n. is_ord (End n) /\ P (End n) /\ (rank (End n) = 0) /\
386 !m. m<n ==> ~(is_ord (End m) /\ P (End m) /\ (rank (End m) = 0))`
387 by let val End_pred = ``\x. is_ord (End x) /\ P (End x) /\ (rank (End x) = 0)``
388 val End_WOP = BETA_RULE (ISPEC End_pred WOP)
389 in METIS_TAC [End_WOP,rank_0_End]
390 end THEN METIS_TAC[oless_End_End,rank_0_End],
391ALL_TAC
392]
393
394THEN
395
396(*---------------------------------------------------------------------------*)
397(* Step case: everything in P has rank <= n+1, so some b has rank <= n or *)
398(* all els of P have rank = n+1. Hence case split. *)
399(*---------------------------------------------------------------------------*)
400
401RW_TAC ord_ss [] THEN
402`(?b. P b /\ rank b <= n) \/ !b. P b ==> (rank b = SUC n)`
403 by METIS_TAC [split_lem]
404
405THENL
406
407(*---------------------------------------------------------------------------*)
408(* Some b has rank <= n. Use IH on b. *)
409(*---------------------------------------------------------------------------*)
410[
411FIRST_ASSUM (MP_TAC o SPEC ``\x. is_ord(x) /\ P x /\ rank(x) <= n``)
412THEN RW_TAC std_ss []
413THEN `?m. is_ord m /\ P m /\ rank m <= n /\
414 !y. is_ord y /\ rank y <= n /\ oless y m ==> ~P y` by METIS_TAC[]
415THEN Q.EXISTS_TAC `m` THEN RW_TAC ord_ss []
416THEN `rank y <= rank m` by METIS_TAC [oless_imp_rank_leq]
417THEN METIS_TAC [LESS_EQ_TRANS,DECIDE ``x <= SUC x``],
418ALL_TAC
419]
420
421THEN
422
423(*---------------------------------------------------------------------------*)
424(* Adjust goal to take account of fact that everything in P has rank n+1. *)
425(*---------------------------------------------------------------------------*)
426
427`!x. P x ==> is_ord x /\ (rank x = SUC n)` by METIS_TAC [] THEN
428 DROP_ASSUMS_TAC [2,3] THEN
429`(?m. is_ord m /\ P m /\ (rank m = SUC n) /\
430 !y. is_ord y /\ (rank y = SUC n) /\ oless y m ==> ~P y)
431 ==>
432 ?m.
433 is_ord m /\ P m /\ rank m <= SUC n /\
434 !y. is_ord y /\ rank y <= SUC n /\ oless y m ==> ~P y`
435 by (RW_TAC ord_ss [] THEN Q.EXISTS_TAC `m` THEN RW_TAC ord_ss []
436 THEN METIS_TAC[])
437 THEN POP_ASSUM MATCH_MP_TAC
438
439THEN
440
441(*---------------------------------------------------------------------------*)
442(* Start proof by contradiction. Thus we assume that every element a in P *)
443(* has a b also in P such that oless b a. *)
444(*---------------------------------------------------------------------------*)
445
446 SPOSE_NOT_THEN
447 (ASSUME_TAC o SIMP_RULE ord_ss [DECIDE ``A \/ B <=> ~A ==> B``,
448 DECIDE ``a ==> b ==> c <=> a /\ b ==> c``])
449THEN
450
451(*---------------------------------------------------------------------------*)
452(* So there is a set S of such sets *)
453(*---------------------------------------------------------------------------*)
454
455`?S. (?si. S(si)) /\
456 (!si. S si <=> (?x. si x) /\
457 (!x. si(x) ==> is_ord(x) /\ (rank x = SUC n) /\ ?y. si y /\ oless y x))`
458 by (Q.EXISTS_TAC `\si.
459 (?a. si a) /\
460 (!b. si b ==> is_ord b /\ (rank b = SUC n) /\ ?d. si d /\ oless d b)`
461 THEN METIS_TAC []) THEN
462 DROP_ASSUMS_TAC [1,2,3] (* used to show existence of S; can now toss *)
463
464THEN
465
466(*---------------------------------------------------------------------------*)
467(* The set of all first exponents of ordinals anywhere in S is n.e. and *)
468(* everything in it has rank at most n. *)
469(*---------------------------------------------------------------------------*)
470
471`?E. (?e. E e) /\ (!e. E e = ?si x. S si /\ si x /\ (e = expt x))`
472 by (Q.EXISTS_TAC `\x. ?si y. S si /\ si y /\ (x = expt y)`
473 THEN METIS_TAC[]) THEN
474`!e. E e ==> is_ord(e) /\ rank e <= n` by
475 (RW_TAC ord_ss [] THEN METIS_TAC [is_ord_expt_closed,rank_expt,LESS_OR_EQ])
476
477THEN
478
479(*---------------------------------------------------------------------------*)
480(* So has a minimal element (alpha_1) by the IH *)
481(*---------------------------------------------------------------------------*)
482
483`?alpha_1. is_ord(alpha_1) /\ E alpha_1 /\ rank alpha_1 <= n /\
484 !y. is_ord(y) /\ rank y <= n /\ oless y alpha_1 ==> ~E y`
485 by (RES_TAC THEN METIS_TAC [])
486
487THEN
488
489(*---------------------------------------------------------------------------*)
490(* Now we are going to work inside a particular set of ordinals that has an *)
491(* element that alpha_1 is the first exponent of. There may be more than one *)
492(* such set, of course, but we already have a witness from showing the *)
493(* existence of alpha_1. *)
494(*---------------------------------------------------------------------------*)
495
496`?sj x. S sj /\ sj x /\ (alpha_1 = expt x)` by METIS_TAC[]
497
498THEN
499
500(*---------------------------------------------------------------------------*)
501(* Now consider the subset of sj where all the ordinals have first exponent *)
502(* equal to alpha_1. Call it s_alpha_1. *)
503(*---------------------------------------------------------------------------*)
504
505`?s_alpha_1.
506 (?a. s_alpha_1 a) /\
507 (!b. s_alpha_1(b) <=> sj(b) /\ (expt b = alpha_1))`
508 by (Q.EXISTS_TAC `\x. sj(x) /\ (expt x = alpha_1)` THEN METIS_TAC [])
509
510THEN
511
512(*---------------------------------------------------------------------------*)
513(* Now we want to consider the set of all first coeff. for any ordinal in *)
514(* s_alpha_1. This is a set of nums, so has a minimum element, k_1. *)
515(*---------------------------------------------------------------------------*)
516
517let val wop_thm =
518REWRITE_RULE []
519 (Q.SPEC `a`
520 (Q.SPEC `coeff a`
521 (Ho_Rewrite.REWRITE_RULE
522 [GSYM LEFT_FORALL_IMP_THM,
523 GSYM LEFT_EXISTS_AND_THM,
524 GSYM RIGHT_EXISTS_AND_THM]
525 (BETA_RULE (SPEC ``\n. ?x. s_alpha_1(x) /\ (n = coeff x)`` WOP)))))
526in
527`?k_1 x1. (s_alpha_1 x1 /\ (k_1 = coeff x1)) /\
528 !m. m < k_1 ==> ~?b. s_alpha_1 b /\ (m = coeff b)`
529 by (MATCH_MP_TAC wop_thm THEN FIRST_ASSUM ACCEPT_TAC)
530end
531
532THEN
533
534(*---------------------------------------------------------------------------*)
535(* Consider the subset of ordinals in s_alpha_1 that have k_1 as first expt. *)
536(* This is n.e. *)
537(*---------------------------------------------------------------------------*)
538
539`?s_alpha_1_k_1.
540 (?a1. s_alpha_1_k_1(a1)) /\
541 (!b. s_alpha_1_k_1(b) <=> s_alpha_1 b /\ (coeff(b) = k_1))`
542 by (Q.EXISTS_TAC `\x. s_alpha_1(x) /\ (coeff(x) = k_1)` THEN METIS_TAC [])
543
544THEN
545
546(*---------------------------------------------------------------------------*)
547(* Consider the set of all tails of elements of s_alpha_1_k_1. This is n.e. *)
548(*---------------------------------------------------------------------------*)
549
550`?Tails. (?b. Tails b) /\
551 (!c. Tails(c) <=> ?b. s_alpha_1_k_1(b) /\ (c = tail b))`
552 by (Q.EXISTS_TAC `\x. ?b. s_alpha_1_k_1(b) /\ (x = tail b)`
553 THEN METIS_TAC [])
554
555THEN
556
557`!q. Tails q ==> is_ord q` by
558 (RW_TAC std_ss [] THEN
559 METIS_TAC [rank_finp,NOT_SUC,is_ord_tail_closed])
560
561THEN
562
563(*---------------------------------------------------------------------------*)
564(* Consider whether there is some x in Tails with rank <= n. If so, use IH; *)
565(* otherwise, all x in Tails have rank n+1 and we recap. *)
566(*---------------------------------------------------------------------------*)
567
568Cases_on `?d. Tails(d) /\ rank d <= n`
569
570THENL
571
572(*---------------------------------------------------------------------------*)
573(* Start first case. There is a "d" in Tails with rank <=n. *)
574(* Use IH to get min.el. t *)
575(*---------------------------------------------------------------------------*)
576
577[`?t. Tails t /\ rank t <= n /\
578 !y. is_ord y /\ rank y <= n /\ oless y t ==> ~Tails y`
579 by (POP_ASSUM STRIP_ASSUME_TAC THEN
580 Q.ABBREV_TAC `Q = \x. Tails x /\ rank(x) <= n` THEN
581 `?x. Q x /\ !x. Q x ==> is_ord(x) /\ rank(x) <= n` by METIS_TAC[] THEN
582 Q.PAT_X_ASSUM `!P:osyntax->bool. !x. A P x ==> B P x`
583 (MP_TAC o BETA_RULE o Q.SPECL [`Q`, `x'`]) THEN
584 Q.UNABBREV_TAC `Q` THEN ASM_REWRITE_TAC [] THEN BETA_TAC THEN
585 REPEAT (POP_ASSUM (K ALL_TAC)) THEN METIS_TAC[])
586
587 THEN
588
589(*---------------------------------------------------------------------------*)
590(* Then w^alpha_1 \cdot k_1 + t is in sj. *)
591(*---------------------------------------------------------------------------*)
592
593`sj (Plus alpha_1 k_1 t)` by
594 (`?v. s_alpha_1_k_1 v /\ (t = tail v)` by METIS_TAC[] THEN
595 `s_alpha_1 v /\ (coeff v = coeff x1)` by METIS_TAC [] THEN
596 `sj(v) /\ (expt v = expt x)` by METIS_TAC [] THEN
597 `v = Plus (expt v) (coeff v) (tail v)`
598 by METIS_TAC [rank_positive,LESS_0] THEN
599 METIS_TAC [])
600
601THEN
602
603(*---------------------------------------------------------------------------*)
604(* The ordinal (Plus alpha_1 k_1 t) is minimal in sj, so contradiction *)
605(*---------------------------------------------------------------------------*)
606
607`?y. sj y /\ oless y (Plus alpha_1 k_1 t)` by METIS_TAC [] THEN
608`is_ord y /\ (y = Plus (expt y) (coeff y) (tail y))`
609 by METIS_TAC [rank_positive,LESS_0] THEN POP_ASSUM SUBST_ALL_TAC THEN
610 Q.PAT_X_ASSUM `oless _ _` MP_TAC THEN
611 RW_TAC ord_ss [Once oless_cases] THENL
612 [METIS_TAC [expt_def],
613 METIS_TAC [expt_def,coeff_def],
614 `Tails (tail y)` by METIS_TAC [tail_def, expt_def,coeff_def] THEN
615 `is_ord (tail y)` by METIS_TAC [is_ord_tail_closed,finp_def] THEN STRIP_TAC THEN
616 `rank (tail y) <= rank t` by METIS_TAC [oless_imp_rank_leq] THEN
617 METIS_TAC[LESS_EQ_TRANS]],
618 ALL_TAC
619]
620
621(*---------------------------------------------------------------------------*)
622(* End first case. *)
623(*---------------------------------------------------------------------------*)
624
625THEN
626
627(*---------------------------------------------------------------------------*)
628(* Other side of case: Everything in Tails has rank = n+1 *)
629(*---------------------------------------------------------------------------*)
630
631`!d. Tails(d) ==> n < rank (d)` by METIS_TAC[DECIDE``~(x<=y) <=> y<x``] THEN
632`!d. Tails(d) ==> rank d <= SUC n`
633 by (RW_TAC ord_ss [] THEN `SUC n = rank b'` by METIS_TAC []
634 THEN POP_ASSUM SUBST1_TAC
635 THEN METIS_TAC [oless_imp_rank_leq,rank_finp, SUC_NOT,
636 is_ord_tail_closed,oless_tail]) THEN
637`!d. Tails d ==> (rank d = SUC n)`
638 by METIS_TAC [DECIDE ``x < y /\ y <= SUC x ==> (y=SUC x)``] THEN
639 POP_ASSUM (fn th => NTAC 3 (POP_ASSUM (K ALL_TAC)) THEN ASSUME_TAC th)
640
641THEN
642
643(*---------------------------------------------------------------------------*)
644(* Now split on if Tails has a minimal element *)
645(*---------------------------------------------------------------------------*)
646
647Cases_on `!c. Tails(c) ==> ?d. Tails d /\ oless d c`
648
649THENL
650[
651(*---------------------------------------------------------------------------*)
652(* First case: No min.el., so contradiction because Tails \in S, but can't *)
653(* be, because of what S is. *)
654(*---------------------------------------------------------------------------*)
655
656`S Tails` by (RW_TAC ord_ss [] THEN METIS_TAC[]) THEN
657`!d. Tails d ==> oless (expt d) (expt x)`
658 by METIS_TAC [decompose_plus,rank_positive,LESS_0] THEN
659`!d. Tails d ==> oless (expt x) (expt d)`
660 by METIS_TAC [decompose_plus, rank_positive_expt,DECIDE``(m=n)==>m<=n``]
661THEN METIS_TAC [oless_antisym],
662ALL_TAC
663]
664
665THEN
666
667(*---------------------------------------------------------------------------*)
668(* Otherwise, Tails has an oless min.el., so build min.el of sj, in a *)
669(* similar way to how it was already done above. *)
670(*---------------------------------------------------------------------------*)
671
672`?t. Tails t /\ !u. is_ord u /\ oless u t ==> ~Tails u` by METIS_TAC [] THEN
673`sj (Plus alpha_1 k_1 t)` by
674 (`?v. s_alpha_1_k_1 v /\ (t = tail v)` by METIS_TAC[] THEN
675 `s_alpha_1 v /\ (coeff v = coeff x1)` by METIS_TAC [] THEN
676 `sj(v) /\ (expt v = expt x)` by METIS_TAC [] THEN
677 `v = Plus (expt v) (coeff v) (tail v)` by METIS_TAC [rank_positive,LESS_0]
678 THEN METIS_TAC [])
679
680THEN
681
682(*---------------------------------------------------------------------------*)
683(* But S implies there is an element of sj less than w^alpha_1 * k1 + t. And *)
684(* we again get a contradiction. *)
685(*---------------------------------------------------------------------------*)
686
687`?y. sj y /\ oless y (Plus alpha_1 k_1 t)` by METIS_TAC [] THEN
688 POP_ASSUM MP_TAC THEN RW_TAC ord_ss [Once oless_cases] THENL
689 [METIS_TAC [rank_def,SUC_NOT],
690 METIS_TAC [is_ord_downclosed,rank_positive_expt,expt_def,DECIDE``(m=n) ==> m<=n``],
691 METIS_TAC [coeff_def,expt_def],
692 METIS_TAC [expt_def,coeff_def,tail_def]]
693
694(*---------------------------------------------------------------------------*)
695(* Done. *)
696(*---------------------------------------------------------------------------*)
697
698QED
699
700
701(*---------------------------------------------------------------------------*)
702(* Now to use the lemma. First instantiate it to rank(x). *)
703(*---------------------------------------------------------------------------*)
704
705val lemma' =
706 SIMP_RULE std_ss [LESS_EQ_REFL]
707 (Q.SPEC `x`
708 (SIMP_RULE std_ss [GSYM LEFT_FORALL_IMP_THM]
709 (SPEC_ALL (Q.SPEC `rank x` lemma))));
710
711(*---------------------------------------------------------------------------*)
712(* So can rephrase lemma by getting rid of the rank restriction. *)
713(*---------------------------------------------------------------------------*)
714
715Theorem main_lemma:
716 !P. (?x. P x /\ is_ord x) ==>
717 ?x. P x /\ is_ord x /\ !y. is_ord y /\ oless y x ==> ~P y
718Proof
719 REPEAT STRIP_TAC THEN
720 `?m. is_ord m /\ P m /\ rank m <= rank x /\
721 !y. is_ord y /\ rank y <= rank x /\ oless y m ==> ~P y` by METIS_TAC [lemma']
722 THEN METIS_TAC [oless_imp_rank_leq,LESS_EQ_TRANS]
723QED
724
725(*---------------------------------------------------------------------------*)
726(* less-than on ordinals. *)
727(*---------------------------------------------------------------------------*)
728
729Definition ord_less_def:
730 ord_less x y <=> is_ord x /\ is_ord y /\ oless x y
731End
732
733
734(*---------------------------------------------------------------------------*)
735(* ord_less is well-founded. *)
736(*---------------------------------------------------------------------------*)
737
738Theorem WF_ord_less:
739 WF ord_less
740Proof
741 RW_TAC ord_ss [relationTheory.WF_DEF,ord_less_def] THEN
742 METIS_TAC [main_lemma,ord_less_def]
743QED
744
745(*---------------------------------------------------------------------------*)
746(* Hence induction and recursion on the ordinals up to e_0, ala ACL2. *)
747(*---------------------------------------------------------------------------*)
748
749val WF_ord_measure =
750 SPEC_ALL (MATCH_MP relationTheory.WF_inv_image WF_ord_less);
751
752Theorem e0_INDUCTION =
753 GEN ``P:'a->bool``
754 (GEN ``f:'a->osyntax``
755 (SPEC_ALL
756 (SIMP_RULE std_ss [relationTheory.inv_image_def]
757 (MATCH_MP relationTheory.WF_INDUCTION_THM WF_ord_measure))));
758
759Theorem e0_RECURSION:
760 !f. ?!g. !x. g x = M (RESTRICT g (\x y. ord_less (f x) (f y)) x) x
761Proof
762 MATCH_ACCEPT_TAC
763 (SIMP_RULE std_ss [relationTheory.inv_image_def]
764 (MATCH_MP relationTheory.WF_RECURSION_THM WF_ord_measure))
765QED
766
767(*---------------------------------------------------------------------------*)
768(* Ordinal addition, subtraction, multiplication and exponentiation. Taken *)
769(* from Manolios and Vroon, JAR. *)
770(*---------------------------------------------------------------------------*)
771
772Definition ord_add_def:
773 (ord_add (End m) (End n) = End (m+n)) /\
774 (ord_add (End m) (Plus p k t) = Plus p k t) /\
775 (ord_add (Plus e k t) (End m) = Plus e k (ord_add t (End m))) /\
776 (ord_add (Plus e1 k1 t1) (Plus e2 k2 t2) =
777 if oless e1 e2 then Plus e2 k2 t2 else
778 if e1 = e2 then Plus e2 (k1+k2) t2 else
779 Plus e1 k1 (ord_add t1 (Plus e2 k2 t2)))
780End
781
782Definition ord_sub_def:
783 (ord_sub (End m) (End n) = End (m-n)) /\
784 (ord_sub (End m) (Plus p k t) = End 0) /\
785 (ord_sub (Plus e k t) (End m) = Plus e k t) /\
786 (ord_sub (Plus e1 k1 t1) (Plus e2 k2 t2) =
787 if oless e1 e2 then End 0 else
788 if e1 = e2
789 then (if k1<k2 then End 0 else
790 if k1>k2 then Plus e1 (k1-k2) t1
791 else ord_sub t1 t2)
792 else Plus e1 k1 t1)
793End
794
795(*---------------------------------------------------------------------------*)
796(* Weird renaming in last two clauses by Define. *)
797(*---------------------------------------------------------------------------*)
798
799Definition ord_mult_def:
800 ord_mult x y =
801 if (x = End 0) \/ (y = End 0) then End 0 else
802 case (x,y)
803 of (End m, End n) => End (m * n)
804 | (End m, Plus e k t) => Plus (ord_add (End 0) e) k (ord_mult (End m) t)
805 | (Plus e k t, End n) => Plus e (k*n) t
806 | (Plus e1 k1 t1, Plus e2 k2 t2) => Plus (ord_add e1 e2) k2
807 (ord_mult (Plus e1 k1 t1) t2)
808End
809
810val _ = Count.report (Count.read meter);
811
812(* ----------------------------------------------------------------------
813 More efficient multiplication (again from Manolios & Vroon)
814 ---------------------------------------------------------------------- *)
815
816Definition restn_def:
817 (restn a 0 = a) /\
818 (restn a (SUC n) = restn (tail a) n)
819End
820
821Definition cf1_def[simp]:
822 (cf1 (End _) b = 0) /\
823 (cf1 (Plus e1 c1 k1) b = if ord_less (expt b) e1 then 1 + cf1 k1 b
824 else 0)
825End
826
827Definition cf2_def: cf2 a b n = n + cf1 (restn a n) b
828End
829
830Definition padd_def:
831 (padd a b 0 = ord_add a b) /\
832 (padd a b (SUC n) = Plus (expt a) (coeff a) (padd (tail a) b n))
833End
834
835val pmult_def = tDefine "pmult" `
836 pmult a b n =
837 if (a = End 0) \/ (b = End 0) then End 0
838 else
839 case (a,b) of
840 (End i, End j) => End (i * j)
841 | (Plus e1 c1 k1, End j) => Plus e1 (c1 * j) k1
842 | (_, Plus e2 c2 k2) =>
843 let m = cf2 (expt a) e2 n
844 in
845 Plus (padd (expt a) e2 m) c2 (pmult a k2 m)
846` (WF_REL_TAC `measure (osyntax_size o FST o SND)`)