ordNotationSemanticsScript.sml
1Theory ordNotationSemantics
2Ancestors
3 ordinalBasic ordinal cardinal ordinalNotation
4
5val _ = export_rewrites ["ordinalNotation.finp_def", "ordinalNotation.tail_def",
6 "ordinalNotation.is_ord_equations",
7 "ordinalNotation.osyntax_size_def",
8 "ordinalNotation.oless_equations",
9 "ordinalNotation.expt_def"]
10
11Definition ordModel_def[simp]:
12 (ordModel (End n) = &n) /\
13 (ordModel (Plus e c t) = omega ** ordModel e * &c + ordModel t)
14End
15
16val _ = add_rule {fixity = Closefix, term_name = "ordModel",
17 block_style = (AroundEachPhrase, (PP.CONSISTENT,2)),
18 paren_style = OnlyIfNecessary,
19 pp_elements = [TOK "<[", TM, TOK "]>"]}
20val _ = add_rule {fixity = Closefix, term_name = "ordModel",
21 block_style = (AroundEachPhrase, (PP.CONSISTENT,2)),
22 paren_style = OnlyIfNecessary,
23 pp_elements = [TOK "⟦", TM, TOK "⟧"]}
24
25Theorem osyntax_EQ_0:
26 !a. is_ord a ==> ((<[a]> = 0) <=> (a = End 0))
27Proof
28 Induct_on `is_ord` THEN SRW_TAC [][ordModel_def] THEN
29 `k <> 0` by DECIDE_TAC THEN SRW_TAC [][ordEXP_EQ_0]
30QED
31
32Theorem oless_0[simp]:
33 !n. oless n (End 0) = F
34Proof
35 Cases_on `n` >> simp[]
36QED
37
38Theorem oless_0a[simp]:
39 oless (End 0) n <=> n <> End 0
40Proof
41 Cases_on `n` >> simp[]
42QED
43
44Theorem oless_x_End:
45 oless x (End n) <=> ?m. (x = End m) /\ m < n
46Proof
47 Cases_on `x` >> simp[]
48QED
49
50Theorem is_ord_expt:
51 is_ord e ==> is_ord (expt e)
52Proof
53 Cases_on `e` >> simp[]
54QED
55
56Theorem ordModel_lt_epsilon0:
57 !a. <[a]> < epsilon0
58Proof
59 Induct_on `a` THEN
60 SRW_TAC [][ordMUL_under_epsilon0, ordEXP_under_epsilon0,
61 ordADD_under_epsilon0, ordModel_def]
62QED
63
64val asimp = asm_simp_tac (srw_ss() ++ ARITH_ss)
65val bsimp = asm_simp_tac bool_ss
66val csimp = asm_simp_tac (srw_ss() ++ boolSimps.CONJ_ss)
67val dsimp = asm_simp_tac (srw_ss() ++ boolSimps.DNF_ss)
68
69Theorem ord_less_models_ordlt:
70 !x. is_ord x ==>
71 (!y. oless x y /\ is_ord y ==> <[x]> :'a ordinal < <[y]>) /\
72 (~finp x ==> <[tail x]> < omega ** <[expt x]> :'a ordinal)
73Proof
74 completeInduct_on `osyntax_size x` THEN
75 RULE_ASSUM_TAC
76 (SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [AND_IMP_INTRO]) >> fs[] >>
77 gen_tac >>
78 `(?m. x = End m) \/ (?e c t. x = Plus e c t)` by (Cases_on `x` >> simp[])
79 >- (simp[] >> strip_tac >> qx_gen_tac `y` >>
80 `(?n. y = End n) \/ (?e c t. y = Plus e c t)` by (Cases_on `y` >> simp[])>>
81 simp[] >> strip_tac >>
82 match_mp_tac ordlte_TRANS >> qexists_tac `omega` >> rw[] >>
83 match_mp_tac ordle_TRANS >> qexists_tac `omega ** <[e]> * &c` >> rw[] >>
84 match_mp_tac ordle_TRANS >> qexists_tac `omega ** <[e]>` >>
85 asm_simp_tac (srw_ss() ++ ARITH_ss) [] >>
86 SIMP_TAC bool_ss [Once (GSYM ordEXP_1R), SimpR ``ordlt``] THEN
87 MATCH_MP_TAC ordEXP_le_MONO_R THEN simp[] >>
88 metis_tac [IFF_ZERO_lt, osyntax_EQ_0]) >>
89 simp[] >> disch_then SUBST_ALL_TAC >> strip_tac >>
90 REVERSE conj_tac
91 >- (`omega ** <[e]> = <[Plus e 1 (End 0)]>` by simp[] >> pop_assum SUBST1_TAC >>
92 first_assum match_mp_tac >> simp[] >> Cases_on `t` >> fs[]) >>
93 qx_gen_tac `y` >>
94 `(?n. y = End n) \/ (?e2 c2 t2. y = Plus e2 c2 t2)`
95 by (Cases_on `y` >> simp[]) >> simp[] >> strip_tac
96 >- (`<[t]> < <[Plus e 1 (End 0)]>`
97 by (first_assum match_mp_tac >> asimp[] >> Cases_on `t` >> fs[]) >>
98 pop_assum mp_tac >> simp[] >> strip_tac >>
99 match_mp_tac ordlt_TRANS >> qexists_tac `omega ** <[e]> * &(SUC c)` >>
100 conj_tac
101 >- (match_mp_tac ordlte_TRANS >>
102 qexists_tac `omega ** <[e]> * &c + omega ** <[e]>` >> simp[]) >>
103 match_mp_tac ordlte_TRANS >> qexists_tac `omega ** <[e2]>` >> REVERSE conj_tac
104 >- (match_mp_tac ordle_TRANS >> qexists_tac `omega ** <[e2]> * &c2` >>
105 simp[]) >>
106 `omega ** <[e]> * &(SUC c) = eval_poly omega [(&SUC c, <[e]>)]` by simp[] >>
107 pop_assum SUBST1_TAC >>
108 match_mp_tac (GEN_ALL is_polyform_head_dominates_tail) >>
109 simp[is_polyform_def] >> qexists_tac `1` >> simp[])
110 >- (simp[] >>
111 `<[t]> < <[Plus e 1 (End 0)]>`
112 by (first_assum match_mp_tac >> asimp[] >> Cases_on `t` >> fs[]) >>
113 pop_assum mp_tac >> simp[] >> strip_tac >>
114 match_mp_tac ordlte_TRANS >> qexists_tac `omega ** <[e2]> * &(SUC c)` >>
115 conj_tac >- simp[] >>
116 match_mp_tac ordle_TRANS >> qexists_tac `omega ** <[e2]> * &c2` >> simp[]) >>
117 simp[]
118QED
119
120Theorem oless_total:
121 !m n. oless m n \/ oless n m \/ (m = n)
122Proof
123 Induct
124 >- (map_every qx_gen_tac [`i`, `n`] >>
125 `(?j. n = End j) \/ (?e2 c2 t2. n = Plus e2 c2 t2)`
126 by (Cases_on `n` >> simp[]) >> simp[]) >>
127 map_every qx_gen_tac [`i`, `n`] >>
128 qmatch_rename_tac `oless (Plus e1 i t1) n \/ _` >>
129 `(?j. n = End j) \/ (?e2 j t2. n = Plus e2 j t2)`
130 by (Cases_on `n` >> simp[]) >> simp[] >>
131 `oless e1 e2 \/ oless e2 e1 \/ (e2 = e1)` by metis_tac[] >> rw[] >>
132 `oless t1 t2 \/ oless t2 t1 \/ (t2 = t1)` by metis_tac[] >> rw[] >>
133 metis_tac [DECIDE ``x:num < y \/ y < x \/ (x = y)``]
134QED
135
136Theorem ord_less_modelled:
137 ord_less x y <=> is_ord x /\ is_ord y /\ <[x]> < <[y]>
138Proof
139 metis_tac [ord_less_def, ord_less_models_ordlt, ordlt_REFL, ordlt_TRANS,
140 oless_total]
141QED
142
143Theorem oless_modelled:
144 is_ord x /\ is_ord y ==> (oless x y <=> <[x]> < <[y]>)
145Proof
146 metis_tac [ord_less_def, ord_less_modelled]
147QED
148
149Theorem WF_ord_less:
150 WF ord_less
151Proof
152 match_mp_tac relationTheory.WF_SUBSET >>
153 qexists_tac `inv_image ordlt ordModel` >>
154 simp[relationTheory.WF_inv_image, ordlt_WF] >>
155 simp[ord_less_modelled, relationTheory.inv_image_def]
156QED
157
158(* |- <[expt t]> < <[e]> /\ is_ord e /\ is_ord t ==> <[t]> < omega ** <[e]> *)
159Theorem neqend0_lemma[local]:
160 x < <[e]> ==> e <> End 0
161Proof
162 rpt strip_tac >> fs[]
163QED
164
165Theorem tail_dominated =
166 ord_less_models_ordlt
167 |> Q.SPEC `Plus e 1 t`
168 |> SIMP_RULE (srw_ss() ++ boolSimps.CONJ_ss)
169 [oless_modelled, is_ord_expt]
170 |> REWRITE_RULE [neqend0_lemma |> Q.INST [`x` |-> `<[expt t]>`] |> UNDISCH]
171 |> REWRITE_RULE [ASSUME ``<[expt t]> < <[e]> :'a ordinal``]
172 |> DISCH_ALL |> REWRITE_RULE [AND_IMP_INTRO];
173
174Theorem addL_disappears:
175 !e a. a < omega ** e ==> (a + omega ** e = omega ** e)
176Proof
177 ho_match_mp_tac simple_ord_induction >> simp[] >> rpt conj_tac
178 >- (qx_gen_tac `a` >> strip_tac >> `a = 0` by metis_tac [IFF_ZERO_lt] >>
179 simp[])
180 >- (simp[omega_islimit] >> qx_gen_tac `e` >> strip_tac >> qx_gen_tac `a` >>
181 dsimp[sup_thm, IMAGE_cardleq_rwt, preds_inj_univ] >> qx_gen_tac `c` >>
182 strip_tac >>
183 `IMAGE ($* (omega ** e)) (preds omega) <> {}`
184 by simp[pred_setTheory.EXTENSION] >>
185 simp[ordADD_continuous, IMAGE_cardleq_rwt, preds_inj_univ] >>
186 simp[GSYM pred_setTheory.IMAGE_COMPOSE, combinTheory.o_ABS_R] >>
187 match_mp_tac sup_eq_sup >> dsimp[IMAGE_cardleq_rwt, preds_inj_univ] >>
188 conj_tac
189 >- (qx_gen_tac `d` >>
190 disch_then (Q.X_CHOOSE_THEN `dn` STRIP_ASSUME_TAC o
191 SIMP_RULE (srw_ss()) [lt_omega]) >>
192 `(dn = 0) \/ ?dn0. dn = SUC dn0` by (Cases_on `dn` >> simp[])
193 >- (rw[] >> qexists_tac `c` >> simp[ordle_lteq]) >>
194 `dn = 1 + dn0` by decide_tac >>
195 Q.UNDISCH_THEN `dn = SUC dn0` (K ALL_TAC) >> srw_tac[][] >>
196 SIMP_TAC bool_ss [GSYM ordADD_fromNat, ordMULT_LDISTRIB] >>
197 simp[] >>
198 `0 < c` by (spose_not_then strip_assume_tac >> fs[]) >>
199 `0 < omega ** e` by (spose_not_then strip_assume_tac >> fs[]) >>
200 qspecl_then [`a`, `omega ** e`] mp_tac ordDIVISION >>
201 qabbrev_tac `q = a / omega ** e` >> qabbrev_tac `r = a % omega ** e` >>
202 simp[] >> strip_tac >>
203 `omega ** e * q + r + (omega ** e + omega ** e * &dn0) =
204 omega ** e * q + omega ** e + omega ** e * &dn0`
205 by metis_tac [ordADD_ASSOC] >>
206 simp[] >>
207 `q < c`
208 by (spose_not_then strip_assume_tac >>
209 `omega ** e * c <= omega ** e * q` by simp[] >>
210 `omega ** e * q <= omega ** e * q+ r` by simp[] >>
211 metis_tac [ordlte_TRANS, ordle_TRANS, ordlt_REFL]) >>
212 `q < omega` by metis_tac [ordlt_TRANS] >>
213 qexists_tac `q + 1 + &dn0` >>
214 simp[ordMULT_LDISTRIB] >> fs[lt_omega]) >>
215 qx_gen_tac `d` >> strip_tac >> qexists_tac `d` >> simp[]) >>
216 qx_gen_tac `e` >> strip_tac >>
217 `IMAGE ($** omega) (preds e) <> {}`
218 by (simp[pred_setTheory.EXTENSION] >> strip_tac >> fs[]) >>
219 dsimp[sup_thm, ordADD_continuous, IMAGE_cardleq_rwt, preds_inj_univ,
220 GSYM pred_setTheory.IMAGE_COMPOSE] >>
221 map_every qx_gen_tac [`a`, `x`] >> strip_tac >>
222 match_mp_tac sup_eq_sup >> dsimp[IMAGE_cardleq_rwt, preds_inj_univ] >>
223 conj_tac
224 >- (qx_gen_tac `y` >> strip_tac >>
225 `(x = y) \/ x < y \/ y < x` by metis_tac [ordlt_trichotomy]
226 >- metis_tac[ordlt_REFL]
227 >- (`omega ** x < omega ** y` by simp[] >>
228 `a < omega ** y` by metis_tac [ordlt_TRANS] >>
229 metis_tac [ordlt_REFL]) >>
230 metis_tac [ordlt_CANCEL, ordEXP_lt_IFF, lt_omega, ordle_lteq]) >>
231 qx_gen_tac `y` >> strip_tac >>
232 `(x = y) \/ x < y \/ y < x` by metis_tac [ordlt_trichotomy]
233 >- metis_tac [ordlt_REFL]
234 >- (`omega ** x < omega ** y` by simp[] >>
235 `a < omega ** y` by metis_tac [ordlt_TRANS] >>
236 metis_tac [ordlt_REFL]) >>
237 metis_tac [ordlt_CANCEL, ordEXP_lt_IFF, lt_omega, ordle_lteq]
238QED
239
240Theorem add_nat1_disappears:
241 omega <= a ==> (&n + a = a)
242Proof
243 rpt strip_tac >> fs [ordle_EXISTS_ADD] >>
244 qspecl_then [`1`, `&n`] mp_tac addL_disappears >> simp[ordADD_ASSOC]
245QED
246
247Theorem add_nat1_disappears_kexp:
248 e <> 0 /\ 0 < k ==> (&n + omega ** e * &k = omega ** e * &k)
249Proof
250 strip_tac >> match_mp_tac add_nat1_disappears >> match_mp_tac ordle_TRANS >>
251 qexists_tac `omega ** e` >> simp[] >>
252 match_mp_tac ordle_TRANS >> qexists_tac `omega ** 1` >> simp[] >>
253 metis_tac [IFF_ZERO_lt]
254QED
255
256Theorem add_disappears_kexp:
257 e <> 0 /\ 0 < k /\ a < omega ** e ==> (a + omega ** e * &k = omega ** e * &k)
258Proof
259 strip_tac >>
260 `(k = 0) \/ ?k0. k = SUC k0` by (Cases_on `k` >> simp[]) >- fs[] >>
261 `k = 1 + k0` by decide_tac >> pop_assum SUBST1_TAC >>
262 bsimp[GSYM ordADD_fromNat, ordMULT_LDISTRIB] >>
263 simp[ordADD_ASSOC, addL_disappears]
264QED
265
266(* |- e1 < e2 ==> &k * omega ** e1 < omega ** e2 *)
267Theorem kexp_lt = (let
268 val zero_ltk_or_eqzero = DECIDE ``0n < k \/ (k = 0)``
269 val zero_ltk =
270 is_polyform_head_dominates_tail
271 |> Q.INST [`a` |-> `omega`, `t` |-> `[(&k,e1)]`, `c` |-> `1`, `e` |-> `e2`]
272 |> SIMP_RULE (srw_ss()) [is_polyform_def, ASSUME ``e1:'a ordinal < e2``]
273 |> UNDISCH_ALL
274 val eqzero = TAC_PROOF(([``k = 0n``], ``omega ** e1 * &k < omega ** e2``),
275 simp[ASSUME ``k = 0n``] >> spose_not_then assume_tac >>
276 fs[ordEXP_EQ_0])
277in
278 DISJ_CASES zero_ltk_or_eqzero zero_ltk eqzero |> DISCH_ALL
279end)
280
281Theorem ord_add_correct:
282 !x y. is_ord x /\ is_ord y ==> (<[ord_add x y]> = <[x]> + <[y]>)
283Proof
284 ho_match_mp_tac ord_add_ind >>
285 simp_tac (srw_ss() ++ boolSimps.CONJ_ss)
286 [ord_add_def, oless_modelled, AND_IMP_INTRO, is_ord_expt, ordADD_ASSOC] >>
287 rw[add_nat1_disappears_kexp, osyntax_EQ_0]
288 >- (AP_THM_TAC >> AP_TERM_TAC >> simp[Once EQ_SYM_EQ] >>
289 match_mp_tac (add_disappears_kexp |> GEN_ALL) >>
290 simp[osyntax_EQ_0] >> match_mp_tac ordlt_TRANS >>
291 qexists_tac `omega ** <[e1]> * &(SUC k1)` >> simp[kexp_lt, tail_dominated])
292 >- (AP_THM_TAC >> AP_TERM_TAC >> simp[GSYM ordADD_ASSOC] >>
293 simp[add_disappears_kexp, tail_dominated, osyntax_EQ_0] >>
294 bsimp[GSYM ordADD_fromNat, ordMULT_LDISTRIB]) >>
295 simp[ordADD_ASSOC]
296QED
297
298Theorem notation_exists:
299 !a. a < epsilon0 ==> ?n. is_ord n /\ (<[n]> = a) /\
300 (0 < a ==> (<[expt n]> = SND (HD (CNF a))))
301Proof
302 ho_match_mp_tac ord_induction >> rpt strip_tac >>
303 `(CNF a = []) \/ ?c e t. (CNF a = (c,e)::t)`
304 by metis_tac [listTheory.list_CASES, pairTheory.pair_CASES]
305 >- (fs[polyform_EQ_NIL] >> qexists_tac `End 0` >> simp[]) >>
306 `(eval_poly omega ((c,e)::t) = a) /\ is_polyform omega ((c,e)::t)`
307 by metis_tac [polyform_def, fromNat_lt_omega] >>
308 `c < omega /\ 0 < c /\ is_polyform omega t`
309 by (imp_res_tac is_polyform_CONS_E >> simp[]) >>
310 `eval_poly omega t < a`
311 by (rw[] >> match_mp_tac ordlte_TRANS >>
312 qexists_tac `omega ** e` >> conj_tac
313 >- (match_mp_tac (GEN_ALL is_polyform_head_dominates_tail) >>
314 metis_tac[fromNat_lt_omega]) >>
315 match_mp_tac ordle_TRANS >> qexists_tac `omega ** e * c` >> simp[] >>
316 qsuff_tac `c <> 0` >- simp[] >> strip_tac >> fs[]) >>
317 `?tn. is_ord tn /\ (<[tn]> = eval_poly omega t) /\
318 (0 < eval_poly omega t ==> (<[expt tn]> = SND (HD (CNF (eval_poly omega t)))))`
319 by (first_x_assum (qspec_then `eval_poly omega t` mp_tac) >> simp[] >>
320 disch_then match_mp_tac >> metis_tac [ordlt_TRANS]) >>
321 `CNF (eval_poly omega t) = t` by simp[polyform_eval_poly] >> fs[] >>
322 `?cn. c = &cn` by metis_tac[lt_omega] >>
323 `e < a`
324 by (spose_not_then strip_assume_tac >>
325 `omega ** e * c <= a` by rw[] >>
326 `omega ** e <= omega ** e * c` by (simp[] >> qsuff_tac `cn <> 0` >- simp[] >>
327 strip_tac >> fs[]) >>
328 `omega ** e <= e` by metis_tac [ordle_TRANS] >>
329 `epsilon0 <= e` by metis_tac [epsilon0_least_fixpoint] >>
330 `a < e` by metis_tac [ordlte_TRANS] >>
331 `e <= omega ** e` by simp[x_le_ordEXP_x] >>
332 metis_tac [ordlt_REFL, ordlte_TRANS, ordle_TRANS]) >>
333 Cases_on `e = 0`
334 >- (qexists_tac `End cn` >> simp[] >> fs[] >>
335 `&cn = a`
336 by (qsuff_tac `t = []` >- (strip_tac >> fs[]) >>
337 spose_not_then strip_assume_tac >>
338 `?c' e' t'. t = (c',e')::t'`
339 by metis_tac [listTheory.list_CASES, pairTheory.pair_CASES] >>
340 fs[is_polyform_def])) >>
341 `?en. is_ord en /\ (<[en]> = e)` by metis_tac[ordlt_TRANS] >>
342 `en <> End 0` by (strip_tac >> fs[]) >>
343 qexists_tac `Plus en cn tn` >> simp[] >> rw[] >- fs[] >>
344 simp[oless_modelled, is_ord_expt] >>
345 `(t = []) \/ ?c2 e2 t2. t = (c2,e2)::t2`
346 by metis_tac [listTheory.list_CASES, pairTheory.pair_CASES]
347 >- (fs[] >> Q.UNDISCH_THEN `<[tn]> = 0` mp_tac >> simp[osyntax_EQ_0] >>
348 strip_tac >> spose_not_then assume_tac >> fs[]) >>
349 `0 < eval_poly omega t` by (spose_not_then assume_tac >> fs[polyform_0]) >>
350 pop_assum (fn th => RULE_ASSUM_TAC (REWRITE_RULE [th])) >> rw[] >>
351 fs[is_polyform_def]
352QED
353
354Theorem ordModel_11:
355 is_ord n1 /\ is_ord n2 ==> ((<[n1]> = <[n2]>) <=> (n1 = n2))
356Proof
357 simp[EQ_IMP_THM] >> rpt strip_tac >>
358 `(n1 = n2) \/ oless n1 n2 \/ oless n2 n1` by metis_tac [oless_total] >>
359 pop_assum mp_tac >> simp[oless_modelled]
360QED
361
362Theorem ordModel_BIJ:
363 BIJ ordModel { n | is_ord n } { a | a < epsilon0 }
364Proof
365 simp[pred_setTheory.BIJ_DEF, pred_setTheory.INJ_DEF, pred_setTheory.SURJ_DEF,
366 ordModel_lt_epsilon0, ordModel_11] >> metis_tac [notation_exists]
367QED
368
369Theorem nat_times_omega:
370 !e m. 0 < m /\ 0 < e ==> (&m * omega ** e = omega ** e)
371Proof
372 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
373 >- (qx_gen_tac `e` >> strip_tac >>
374 Cases_on `0 < e` >- simp[ordMULT_ASSOC] >> fs[] >>
375 simp[omega_islimit] >> simp[omega_def, SimpRHS] >> rpt strip_tac >>
376 match_mp_tac sup_eq_sup >> simp[IMAGE_cardleq_rwt, preds_inj_univ] >>
377 dsimp[] >> rpt conj_tac
378 >- (qsuff_tac `{&i | T}:'a ordinal set =~ univ(:num)`
379 >- metis_tac [cardinalTheory.CARDEQ_CARDLEQ,
380 cardinalTheory.cardeq_REFL,
381 Unum_cle_Uinf] >>
382 simp[Once cardinalTheory.cardeq_SYM] >>
383 simp[cardinalTheory.cardeq_def] >> qexists_tac `fromNat` >>
384 simp[pred_setTheory.SURJ_DEF, pred_setTheory.BIJ_DEF,
385 pred_setTheory.INJ_DEF] >> dsimp[])
386 >- (dsimp[lt_omega] >> metis_tac [DECIDE ``~(x:num < x)``]) >>
387 qx_gen_tac `i` >> qexists_tac `&i` >> simp[]) >>
388 qx_gen_tac `e` >> strip_tac >>
389 `IMAGE ($** omega) (preds e) <> {}`
390 by (simp[pred_setTheory.EXTENSION] >> strip_tac >> fs[]) >>
391 simp[ordMULT_continuous, IMAGE_cardleq_rwt, preds_inj_univ,
392 GSYM pred_setTheory.IMAGE_COMPOSE, combinTheory.o_DEF] >>
393 rpt strip_tac >> match_mp_tac sup_eq_sup >>
394 dsimp[IMAGE_cardleq_rwt, preds_inj_univ] >> conj_tac
395 >- (qx_gen_tac `a` >> strip_tac >> Cases_on `0 < a`
396 >- (csimp[] >> qexists_tac `a` >> simp[]) >> fs[] >>
397 qexists_tac `1` >> simp[ordle_lteq] >>
398 metis_tac [ORD_ONE, islimit_SUC_lt]) >>
399 qx_gen_tac `a` >> strip_tac >> qexists_tac `a` >> simp[] >>
400 bsimp [Once (GSYM ordMULT_1L), SimpR ``ordlt``] >>
401 match_mp_tac ordMULT_le_MONO_L >> simp[]
402QED
403
404Theorem kexp_sum_times_nat:
405 !c2 c t e. 0 < c2 /\ 0 < c /\ t < omega ** e ==>
406 ((omega ** e * &c + t) * &c2 = omega ** e * &(c * c2) + t)
407Proof
408 Induct >> simp[] >> map_every qx_gen_tac [`c`, `t`, `e`] >> simp[] >>
409 REVERSE (Cases_on `0 < e`)
410 >- (fs[] >> strip_tac >> `t = 0` by metis_tac [IFF_ZERO_lt] >>
411 simp[arithmeticTheory.MULT_CLAUSES]) >>
412 `(c2 = 0) \/ ?c20. c2 = SUC c20` by (Cases_on `c2` >> simp[]) >- simp[] >>
413 strip_tac >>
414 Q.UNDISCH_THEN `c2 = SUC c20`
415 (fn th => RULE_ASSUM_TAC
416 (REWRITE_RULE [
417 MATCH_MP (DECIDE ``!x y. (x = SUC y) ==> 0 < x``)
418 th])) >>
419 simp[] >> simp[ordADD_ASSOC] >> AP_THM_TAC >> AP_TERM_TAC >>
420 bsimp[GSYM ordMULT_fromNat, fromNat_SUC, ordMULT_ASSOC] >>
421 simp[ordMULT_def] >>
422 simp[GSYM ordADD_ASSOC] >> match_mp_tac (GEN_ALL add_disappears_kexp) >>
423 simp[] >> strip_tac >> fs[]
424QED
425
426Theorem kexp_mult:
427 !e2 e1 c t.
428 0 < e2 /\ t < omega ** e1 /\ 0 < c ==>
429 ((omega ** e1 * &c + t) * omega ** e2 = omega ** (e1 + e2))
430Proof
431 ho_match_mp_tac simple_ord_induction >> simp[] >> conj_tac
432 >- (qx_gen_tac `e2` >> strip_tac >> map_every qx_gen_tac [`e1`, `c`, `t`] >>
433 strip_tac >>
434 Cases_on `0 < e2` >- simp[ordMULT_ASSOC] >>
435 fs[] >> simp[omega_islimit] >> match_mp_tac sup_eq_sup >>
436 dsimp[IMAGE_cardleq_rwt, preds_inj_univ] >> conj_tac
437 >- (qx_gen_tac `a` >> strip_tac >> `?an. a = &an` by fs[lt_omega] >>
438 REVERSE (Cases_on `0 < an`)
439 >- (`an = 0` by decide_tac >> simp[] >> qexists_tac `0` >> simp[]) >>
440 simp[kexp_sum_times_nat] >>
441 qexists_tac `ordSUC (&(an * c))` >> simp[] >>
442 bsimp[GSYM fromNat_SUC, fromNat_lt_omega, ordle_lteq]) >>
443 qx_gen_tac `x` >> strip_tac >> qexists_tac `x` >>
444 `?m. x = &m` by fs[lt_omega] >> REVERSE (Cases_on `0 < m`)
445 >- (`m = 0` by decide_tac >> simp[]) >>
446 simp[kexp_sum_times_nat] >> match_mp_tac ordle_TRANS >>
447 qexists_tac `omega ** e1 * &(c * m)` >> simp[]) >>
448 qx_gen_tac `e2` >> strip_tac >> map_every qx_gen_tac [`e1`, `c`, `t`] >>
449 strip_tac >>
450 `IMAGE ($+ e1) (preds e2) <> {}`
451 by (simp[pred_setTheory.EXTENSION] >> strip_tac >> fs[]) >>
452 simp[ordEXP_continuous, ordMULT_continuous, IMAGE_cardleq_rwt,
453 preds_inj_univ, GSYM pred_setTheory.IMAGE_COMPOSE, combinTheory.o_DEF] >>
454 match_mp_tac sup_eq_sup >> dsimp[IMAGE_cardleq_rwt, preds_inj_univ] >>
455 conj_tac
456 >- (qx_gen_tac `a` >> strip_tac >>
457 Cases_on `0 < a` >- metis_tac[ordlt_REFL] >>
458 fs[] >> qexists_tac `1` >> conj_tac
459 >- metis_tac[ORD_ONE, islimit_SUC_lt] >>
460 match_mp_tac ordle_TRANS >> qexists_tac `omega ** e1 * (ordSUC &c)` >>
461 conj_tac >- simp[ordle_lteq] >>
462 bsimp[ordle_lteq] >> disj1_tac >>
463 bsimp[GSYM fromNat_SUC] >> match_mp_tac (GEN_ALL kexp_lt) >> simp[]) >>
464 qx_gen_tac `a` >> strip_tac >>
465 Cases_on `0 < a`
466 >- (qexists_tac `a` >> simp[]) >>
467 qexists_tac `1` >> `1 < e2` by metis_tac [ORD_ONE, islimit_SUC_lt] >>
468 simp[] >> fs[]
469QED
470
471Theorem ord_mult_correct:
472 !x y. is_ord x /\ is_ord y ==> (<[ord_mult x y]> = <[x]> * <[y]>)
473Proof
474 ho_match_mp_tac ord_mult_ind >> csimp[] >> map_every qx_gen_tac [`x`, `y`] >>
475 rpt strip_tac >>
476 `(?m. x = End m) \/ ?e1 c1 t1. x = Plus e1 c1 t1` by (Cases_on `x` >> simp[])
477 >- (`(?n. y = End n) \/ ?e2 c2 t2. y = Plus e2 c2 t2`
478 by (Cases_on `y` >> simp[])
479 >- (simp[Once ord_mult_def] >> Cases_on `(m = 0) \/ (n = 0)` >> simp[]) >>
480 rw[] >> Cases_on `m = 0` >> simp[Once ord_mult_def] >>
481 fs[ord_add_correct] >> simp[ordMULT_LDISTRIB] >> AP_THM_TAC >>
482 AP_TERM_TAC >>
483 `0 < <[e2]>`
484 by (spose_not_then assume_tac >> fs[] >> metis_tac [osyntax_EQ_0]) >>
485 `0 < m` by decide_tac >> metis_tac[nat_times_omega, ordMULT_ASSOC]) >>
486 `(?n. y = End n) \/ ?e2 c2 t2. y = Plus e2 c2 t2` by (Cases_on `y` >> simp[])
487 >- (simp[Once ord_mult_def] >> rw[ordMULT_LDISTRIB] >> fs[] >>
488 Induct_on `n` >> simp[] >>
489 `(n = 0) \/ ?m. n = SUC m` by (Cases_on `n` >> simp[]) >- simp[] >>
490 fs[] >> pop_assum (fn nSm => pop_assum (SUBST_ALL_TAC o SYM) >>
491 REWRITE_TAC [SYM nSm]) >>
492 bsimp[GSYM ordMULT_fromNat, ordMULT_ASSOC, fromNat_SUC] >>
493 simp[ordMULT_def, GSYM ordADD_ASSOC] >> simp[ordADD_ASSOC] >>
494 AP_THM_TAC >> AP_TERM_TAC >> simp[Once EQ_SYM_EQ] >>
495 match_mp_tac (GEN_ALL add_disappears_kexp) >> simp[] >> conj_tac
496 >- metis_tac [osyntax_EQ_0] >>
497 qpat_x_assum `oless MM NN` mp_tac >> simp[oless_modelled, is_ord_expt] >>
498 simp[tail_dominated]) >>
499 fs[] >> simp[Once ord_mult_def, ord_add_correct, ordMULT_LDISTRIB] >>
500 AP_THM_TAC >> AP_TERM_TAC >> simp[ordMULT_ASSOC] >>
501 AP_THM_TAC >> AP_TERM_TAC >> simp[ordMULT_ASSOC] >>
502 simp[Once EQ_SYM_EQ] >> match_mp_tac kexp_mult >> simp[] >>
503 conj_tac >- (spose_not_then assume_tac >> fs[] >> metis_tac [osyntax_EQ_0]) >>
504 Q.UNDISCH_THEN `oless (expt t1) e1` mp_tac >>
505 simp[oless_modelled, is_ord_expt, tail_dominated]
506QED
507
508(* also showing the more efficient version of multiplication correct *)
509val model_expt0 =
510 notation_exists
511 |> Q.SPEC `<[a]>`
512 |> SIMP_RULE (srw_ss() ++ boolSimps.CONJ_ss)
513 [ordModel_lt_epsilon0, ASSUME ``is_ord a /\ 0 < <[a]>``,
514 ordModel_11]
515 |> DISCH_ALL
516
517Theorem model_expt:
518 is_ord a ==> (<[expt a]> = if a = End 0 then 0 else olog <[a]>)
519Proof
520 rw[] >>
521 `0 < <[a]>` by(spose_not_then assume_tac >> fs[] >> metis_tac [osyntax_EQ_0]) >>
522 simp[model_expt0]
523QED
524
525Theorem ord_less_expt_monotone:
526 ord_less x y ==> (expt x = expt y) \/ ord_less (expt x) (expt y)
527Proof
528 rw[ord_less_modelled, is_ord_expt, model_expt] >>
529 bsimp[GSYM ordModel_11, is_ord_rules, is_ord_expt, model_expt, ordModel_def]
530 >- metis_tac [ordle_lteq, ordlt_ZERO] >>
531 qsuff_tac `olog <[x]> <= olog <[y]>` >- metis_tac [ordle_lteq] >> strip_tac >>
532 `0 < <[x]> :'a ordinal /\ 0 < <[y]> : 'a ordinal`
533 by (strip_tac >> spose_not_then strip_assume_tac >> fs[] >>
534 metis_tac [osyntax_EQ_0]) >>
535 `<[y]> :'a ordinal < omega ** olog <[x]> /\
536 omega ** olog <[x]> <= <[x]> : 'a ordinal` by metis_tac [olog_correct] >>
537 metis_tac [ordlet_TRANS, ordlt_TRANS, ordlt_REFL]
538QED
539
540Theorem mvjar_lemma3:
541 ord_less d b ==> cf1 a b <= cf1 a d
542Proof
543 Induct_on `cf1 a b` >- metis_tac[DECIDE ``0n <= n``] >>
544 rpt strip_tac >>
545 `?n. (a = End n) \/ (?e1 c1 k1. a = Plus e1 c1 k1)`
546 by (Cases_on `a` >> simp[]) >- fs[cf1_def] >>
547 pop_assum SUBST_ALL_TAC >>
548 RULE_ASSUM_TAC (SIMP_RULE (srw_ss()) [cf1_def]) >>
549 `ord_less (expt b) e1` by (spose_not_then assume_tac >> fs[]) >>
550 full_simp_tac (srw_ss() ++ ARITH_ss) [arithmeticTheory.ADD1] >>
551 first_x_assum (qspecl_then [`k1`, `b`] mp_tac) >> simp[] >>
552 qsuff_tac `ord_less (expt d) e1` >- simp[] >>
553 `(expt d = expt b) \/ ord_less (expt d) (expt b)`
554 by metis_tac [ord_less_expt_monotone]
555 >- simp[] >> metis_tac [ord_less_modelled, ordlt_TRANS]
556QED
557
558val _ = export_rewrites ["ordinalNotation.restn_def",
559 "ordinalNotation.coeff_def"]
560
561Theorem mvjar_lemma4:
562 !a n b. n <= cf1 a b ==> (cf1 a b = cf2 a b n)
563Proof
564 simp[cf2_def] >> Induct_on `a` >> simp[] >>
565 map_every qx_gen_tac [`n`, `m`, `b`] >>
566 Cases_on `ord_less (expt b) a` >> simp[] >> strip_tac >>
567 `(m = 0) \/ (?k. m = SUC k)` by (Cases_on `m` >> simp[]) >> simp[] >>
568 asm_simp_tac (srw_ss() ++ numSimps.ARITH_NORM_ss) [arithmeticTheory.ADD1] >>
569 asimp[]
570QED
571
572Theorem mvjar_lemma5:
573 (padd a b (cf1 a b) = ord_add a b)
574Proof
575 Induct_on `cf1 a b` >> simp[] >- metis_tac [padd_def] >>
576 map_every qx_gen_tac [`a`, `b`] >>
577 `?n. (a = End n) \/ (?e1 c1 k1. a = Plus e1 c1 k1)`
578 by (Cases_on `a` >> simp[]) >> simp[cf1_def] >>
579 Cases_on `ord_less (expt b) e1` >> asimp[arithmeticTheory.ADD1] >> rw[] >>
580 first_x_assum (qspecl_then [`k1`, `b`] mp_tac) >> simp[] >>
581 `cf1 k1 b + 1 = SUC (cf1 k1 b)` by decide_tac >> simp[padd_def] >>
582 strip_tac >> Cases_on `b` >> simp[ord_add_def] >> fs[ord_less_def] >>
583 qpat_x_assum `oless XX YY` mp_tac >>
584 simp[oless_modelled] >> rw[] >> metis_tac [ordlt_TRANS, ordlt_REFL]
585QED
586
587Theorem better_pmult_def:
588 (pmult a (Plus be bc bt) n =
589 if a = End 0 then End 0
590 else
591 let m = cf2 (expt a) be n
592 in
593 Plus (padd (expt a) be m) bc (pmult a bt m))
594Proof
595 Cases_on `a` >> simp[SimpLHS, Once pmult_def] >> simp[]
596QED
597
598Theorem better_ord_mult_def:
599 ord_mult a (Plus be bc bt) =
600 if a = End 0 then End 0
601 else Plus (ord_add (expt a) be) bc (ord_mult a bt)
602Proof
603 Cases_on `a` >> simp[SimpLHS, Once ord_mult_def] >> simp[]
604QED
605
606Theorem mvjar_theorem10:
607 !n a b. is_ord a /\ is_ord b /\ n <= cf1 (expt a) (expt b) ==>
608 (<[pmult a b n]> = <[a]> * <[b]>)
609Proof
610 Induct_on `b`
611 >- (Cases_on `a` >> simp[pmult_def] >> rw[] >>
612 qmatch_abbrev_tac
613 `omega ** <[e1]> * &(i * j) + <[t]> =
614 (omega ** <[e1]> * &i + <[t]>) * &j` >>
615 markerLib.RM_ALL_ABBREVS_TAC >>
616 `0 < i /\ 0 < j` by decide_tac >>
617 qsuff_tac `<[t]> < omega ** <[e1]>` >- simp[kexp_sum_times_nat] >>
618 match_mp_tac (GEN_ALL tail_dominated) >>
619 metis_tac [oless_modelled, is_ord_expt]) >>
620 rpt strip_tac >>
621 qmatch_abbrev_tac
622 `<[pmult a (Plus be bc bt) nn]> = <[a]> * <[Plus be bc bt]>` >>
623 markerLib.RM_ALL_ABBREVS_TAC >>
624 qabbrev_tac `m = cf2 (expt a) be nn` >>
625 `m = cf1 (expt a) be` by metis_tac [mvjar_lemma4, expt_def] >>
626 RULE_ASSUM_TAC (SIMP_RULE (srw_ss()) []) >>
627 `m <= cf1 (expt a) (expt bt)`
628 by metis_tac [mvjar_lemma3, ord_less_def, is_ord_expt] >>
629 simp[Once better_pmult_def] >> Cases_on `a = End 0` >>
630 simp[mvjar_lemma5, ord_add_correct, is_ord_expt] >>
631 qmatch_abbrev_tac `LHS = RHS` >>
632 qsuff_tac `LHS = <[ord_mult a (Plus be bc bt)]>`
633 >- simp[Abbr`RHS`, ord_mult_correct] >>
634 simp[Abbr`LHS`, Once better_ord_mult_def, ord_add_correct] >>
635 simp[ord_mult_correct, ord_add_correct, is_ord_expt]
636QED