1 (* Title: ZF/OrderType.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory |
|
7 |
|
8 Ordinal arithmetic is traditionally defined in terms of order types, as here. |
|
9 But a definition by transfinite recursion would be much simpler! |
|
10 *) |
|
11 |
|
12 |
|
13 (*??for Ordinal.ML*) |
|
14 (*suitable for rewriting PROVIDED i has been fixed*) |
|
15 Goal "[| j:i; Ord(i) |] ==> Ord(j)"; |
|
16 by (blast_tac (claset() addIs [Ord_in_Ord]) 1); |
|
17 qed "Ord_in_Ord'"; |
|
18 |
|
19 |
|
20 (**** Proofs needing the combination of Ordinal.thy and Order.thy ****) |
|
21 |
|
22 val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))"; |
|
23 by (rtac well_ordI 1); |
|
24 by (rtac (wf_Memrel RS wf_imp_wf_on) 1); |
|
25 by (resolve_tac [prem RS ltE] 1); |
|
26 by (asm_simp_tac (simpset() addsimps [linear_def, |
|
27 [ltI, prem] MRS lt_trans2 RS ltD]) 1); |
|
28 by (REPEAT (resolve_tac [ballI, Ord_linear] 1)); |
|
29 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1)); |
|
30 qed "le_well_ord_Memrel"; |
|
31 |
|
32 (*"Ord(i) ==> well_ord(i, Memrel(i))"*) |
|
33 bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel); |
|
34 |
|
35 (*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord |
|
36 The smaller ordinal is an initial segment of the larger *) |
|
37 Goalw [pred_def, lt_def] |
|
38 "j<i ==> pred(i, j, Memrel(i)) = j"; |
|
39 by (Asm_simp_tac 1); |
|
40 by (blast_tac (claset() addIs [Ord_trans]) 1); |
|
41 qed "lt_pred_Memrel"; |
|
42 |
|
43 Goalw [pred_def,Memrel_def] |
|
44 "x:A ==> pred(A, x, Memrel(A)) = A Int x"; |
|
45 by (Blast_tac 1); |
|
46 qed "pred_Memrel"; |
|
47 |
|
48 Goal "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"; |
|
49 by (ftac lt_pred_Memrel 1); |
|
50 by (etac ltE 1); |
|
51 by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN |
|
52 assume_tac 3 THEN assume_tac 1); |
|
53 by (rewtac ord_iso_def); |
|
54 (*Combining the two simplifications causes looping*) |
|
55 by (Asm_simp_tac 1); |
|
56 by (blast_tac (claset() addIs [bij_is_fun RS apply_type, Ord_trans]) 1); |
|
57 qed "Ord_iso_implies_eq_lemma"; |
|
58 |
|
59 (*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*) |
|
60 Goal "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |] \ |
|
61 \ ==> i=j"; |
|
62 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1); |
|
63 by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1)); |
|
64 qed "Ord_iso_implies_eq"; |
|
65 |
|
66 |
|
67 (**** Ordermap and ordertype ****) |
|
68 |
|
69 Goalw [ordermap_def,ordertype_def] |
|
70 "ordermap(A,r) : A -> ordertype(A,r)"; |
|
71 by (rtac lam_type 1); |
|
72 by (rtac (lamI RS imageI) 1); |
|
73 by (REPEAT (assume_tac 1)); |
|
74 qed "ordermap_type"; |
|
75 |
|
76 (*** Unfolding of ordermap ***) |
|
77 |
|
78 (*Useful for cardinality reasoning; see CardinalArith.ML*) |
|
79 Goalw [ordermap_def, pred_def] |
|
80 "[| wf[A](r); x:A |] ==> \ |
|
81 \ ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"; |
|
82 by (Asm_simp_tac 1); |
|
83 by (etac (wfrec_on RS trans) 1); |
|
84 by (assume_tac 1); |
|
85 by (asm_simp_tac (simpset() addsimps [subset_iff, image_lam, |
|
86 vimage_singleton_iff]) 1); |
|
87 qed "ordermap_eq_image"; |
|
88 |
|
89 (*Useful for rewriting PROVIDED pred is not unfolded until later!*) |
|
90 Goal "[| wf[A](r); x:A |] ==> \ |
|
91 \ ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"; |
|
92 by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset, |
|
93 ordermap_type RS image_fun]) 1); |
|
94 qed "ordermap_pred_unfold"; |
|
95 |
|
96 (*pred-unfolded version. NOT suitable for rewriting -- loops!*) |
|
97 bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold); |
|
98 |
|
99 (*The theorem above is |
|
100 |
|
101 [| wf[A](r); x : A |] |
|
102 ==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}} |
|
103 |
|
104 NOTE: the definition of ordermap used here delivers ordinals only if r is |
|
105 transitive. If r is the predecessor relation on the naturals then |
|
106 ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition, |
|
107 like |
|
108 |
|
109 ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}}, |
|
110 |
|
111 might eliminate the need for r to be transitive. |
|
112 *) |
|
113 |
|
114 |
|
115 (*** Showing that ordermap, ordertype yield ordinals ***) |
|
116 |
|
117 fun ordermap_elim_tac i = |
|
118 EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i, |
|
119 assume_tac (i+1), |
|
120 assume_tac i]; |
|
121 |
|
122 Goalw [well_ord_def, tot_ord_def, part_ord_def] |
|
123 "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"; |
|
124 by Safe_tac; |
|
125 by (wf_on_ind_tac "x" [] 1); |
|
126 by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1); |
|
127 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
|
128 by (rewrite_goals_tac [pred_def,Transset_def]); |
|
129 by (Blast_tac 2); |
|
130 by Safe_tac; |
|
131 by (ordermap_elim_tac 1); |
|
132 by (fast_tac (claset() addSEs [trans_onD]) 1); |
|
133 qed "Ord_ordermap"; |
|
134 |
|
135 Goalw [ordertype_def] |
|
136 "well_ord(A,r) ==> Ord(ordertype(A,r))"; |
|
137 by (stac ([ordermap_type, subset_refl] MRS image_fun) 1); |
|
138 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1); |
|
139 by (blast_tac (claset() addIs [Ord_ordermap]) 2); |
|
140 by (rewrite_goals_tac [Transset_def,well_ord_def]); |
|
141 by Safe_tac; |
|
142 by (ordermap_elim_tac 1); |
|
143 by (Blast_tac 1); |
|
144 qed "Ord_ordertype"; |
|
145 |
|
146 (*** ordermap preserves the orderings in both directions ***) |
|
147 |
|
148 Goal "[| <w,x>: r; wf[A](r); w: A; x: A |] ==> \ |
|
149 \ ordermap(A,r)`w : ordermap(A,r)`x"; |
|
150 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1); |
|
151 by (assume_tac 1); |
|
152 by (Blast_tac 1); |
|
153 qed "ordermap_mono"; |
|
154 |
|
155 (*linearity of r is crucial here*) |
|
156 Goalw [well_ord_def, tot_ord_def] |
|
157 "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); \ |
|
158 \ w: A; x: A |] ==> <w,x>: r"; |
|
159 by Safe_tac; |
|
160 by (linear_case_tac 1); |
|
161 by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1); |
|
162 by (dtac ordermap_mono 1); |
|
163 by (REPEAT_SOME assume_tac); |
|
164 by (etac mem_asym 1); |
|
165 by (assume_tac 1); |
|
166 qed "converse_ordermap_mono"; |
|
167 |
|
168 bind_thm ("ordermap_surj", |
|
169 rewrite_rule [symmetric ordertype_def] |
|
170 (ordermap_type RS surj_image)); |
|
171 |
|
172 Goalw [well_ord_def, tot_ord_def, bij_def, inj_def] |
|
173 "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"; |
|
174 by (force_tac (claset() addSIs [ordermap_type, ordermap_surj] |
|
175 addEs [linearE] |
|
176 addDs [ordermap_mono], |
|
177 simpset() addsimps [mem_not_refl]) 1); |
|
178 qed "ordermap_bij"; |
|
179 |
|
180 (*** Isomorphisms involving ordertype ***) |
|
181 |
|
182 Goalw [ord_iso_def] |
|
183 "well_ord(A,r) ==> \ |
|
184 \ ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"; |
|
185 by (safe_tac (claset() addSEs [well_ord_is_wf] |
|
186 addSIs [ordermap_type RS apply_type, |
|
187 ordermap_mono, ordermap_bij])); |
|
188 by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1); |
|
189 qed "ordertype_ord_iso"; |
|
190 |
|
191 Goal "[| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ |
|
192 \ ordertype(A,r) = ordertype(B,s)"; |
|
193 by (ftac well_ord_ord_iso 1 THEN assume_tac 1); |
|
194 by (rtac Ord_iso_implies_eq 1 |
|
195 THEN REPEAT (etac Ord_ordertype 1)); |
|
196 by (deepen_tac (claset() addIs [ord_iso_trans, ord_iso_sym] |
|
197 addSEs [ordertype_ord_iso]) 0 1); |
|
198 qed "ordertype_eq"; |
|
199 |
|
200 Goal "[| ordertype(A,r) = ordertype(B,s); \ |
|
201 \ well_ord(A,r); well_ord(B,s) \ |
|
202 \ |] ==> EX f. f: ord_iso(A,r,B,s)"; |
|
203 by (rtac exI 1); |
|
204 by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1); |
|
205 by (assume_tac 1); |
|
206 by (etac ssubst 1); |
|
207 by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); |
|
208 qed "ordertype_eq_imp_ord_iso"; |
|
209 |
|
210 (*** Basic equalities for ordertype ***) |
|
211 |
|
212 (*Ordertype of Memrel*) |
|
213 Goal "j le i ==> ordertype(j,Memrel(i)) = j"; |
|
214 by (resolve_tac [Ord_iso_implies_eq RS sym] 1); |
|
215 by (etac ltE 1); |
|
216 by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1)); |
|
217 by (rtac ord_iso_trans 1); |
|
218 by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2); |
|
219 by (resolve_tac [id_bij RS ord_isoI] 1); |
|
220 by (Asm_simp_tac 1); |
|
221 by (fast_tac (claset() addEs [ltE, Ord_in_Ord, Ord_trans]) 1); |
|
222 qed "le_ordertype_Memrel"; |
|
223 |
|
224 (*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*) |
|
225 bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel); |
|
226 |
|
227 Goal "ordertype(0,r) = 0"; |
|
228 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1); |
|
229 by (etac emptyE 1); |
|
230 by (rtac well_ord_0 1); |
|
231 by (resolve_tac [Ord_0 RS ordertype_Memrel] 1); |
|
232 qed "ordertype_0"; |
|
233 |
|
234 Addsimps [ordertype_0]; |
|
235 |
|
236 (*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==> |
|
237 ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *) |
|
238 bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq); |
|
239 |
|
240 (*** A fundamental unfolding law for ordertype. ***) |
|
241 |
|
242 (*Ordermap returns the same result if applied to an initial segment*) |
|
243 Goal "[| well_ord(A,r); y:A; z: pred(A,y,r) |] ==> \ |
|
244 \ ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"; |
|
245 by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1); |
|
246 by (wf_on_ind_tac "z" [] 1); |
|
247 by (safe_tac (claset() addSEs [predE])); |
|
248 by (asm_simp_tac |
|
249 (simpset() addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1); |
|
250 (*combining these two simplifications LOOPS! *) |
|
251 by (asm_simp_tac (simpset() addsimps [pred_pred_eq]) 1); |
|
252 by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1); |
|
253 by (rtac (refl RSN (2,RepFun_cong)) 1); |
|
254 by (dtac well_ord_is_trans_on 1); |
|
255 by (fast_tac (claset() addSEs [trans_onD]) 1); |
|
256 qed "ordermap_pred_eq_ordermap"; |
|
257 |
|
258 Goalw [ordertype_def] |
|
259 "ordertype(A,r) = {ordermap(A,r)`y . y : A}"; |
|
260 by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1); |
|
261 qed "ordertype_unfold"; |
|
262 |
|
263 (** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **) |
|
264 |
|
265 Goal "[| well_ord(A,r); x:A |] ==> \ |
|
266 \ ordertype(pred(A,x,r),r) <= ordertype(A,r)"; |
|
267 by (asm_simp_tac (simpset() addsimps [ordertype_unfold, |
|
268 pred_subset RSN (2, well_ord_subset)]) 1); |
|
269 by (fast_tac (claset() addIs [ordermap_pred_eq_ordermap] |
|
270 addEs [predE]) 1); |
|
271 qed "ordertype_pred_subset"; |
|
272 |
|
273 Goal "[| well_ord(A,r); x:A |] ==> \ |
|
274 \ ordertype(pred(A,x,r),r) < ordertype(A,r)"; |
|
275 by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1); |
|
276 by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1)); |
|
277 by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1); |
|
278 by (etac well_ord_iso_predE 3); |
|
279 by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1)); |
|
280 qed "ordertype_pred_lt"; |
|
281 |
|
282 (*May rewrite with this -- provided no rules are supplied for proving that |
|
283 well_ord(pred(A,x,r), r) *) |
|
284 Goal "well_ord(A,r) ==> \ |
|
285 \ ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"; |
|
286 by (rtac equalityI 1); |
|
287 by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD])); |
|
288 by (auto_tac (claset(), |
|
289 simpset() addsimps [ordertype_def, |
|
290 well_ord_is_wf RS ordermap_eq_image, |
|
291 ordermap_type RS image_fun, |
|
292 ordermap_pred_eq_ordermap, |
|
293 pred_subset])); |
|
294 qed "ordertype_pred_unfold"; |
|
295 |
|
296 |
|
297 (**** Alternative definition of ordinal ****) |
|
298 |
|
299 (*proof by Krzysztof Grabczewski*) |
|
300 Goalw [Ord_alt_def] "Ord(i) ==> Ord_alt(i)"; |
|
301 by (rtac conjI 1); |
|
302 by (etac well_ord_Memrel 1); |
|
303 by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]); |
|
304 by (Blast.depth_tac (claset()) 8 1); |
|
305 qed "Ord_is_Ord_alt"; |
|
306 |
|
307 (*proof by lcp*) |
|
308 Goalw [Ord_alt_def, Ord_def, Transset_def, well_ord_def, |
|
309 tot_ord_def, part_ord_def, trans_on_def] |
|
310 "Ord_alt(i) ==> Ord(i)"; |
|
311 by (asm_full_simp_tac (simpset() addsimps [pred_Memrel]) 1); |
|
312 by (blast_tac (claset() addSEs [equalityE]) 1); |
|
313 qed "Ord_alt_is_Ord"; |
|
314 |
|
315 |
|
316 (**** Ordinal Addition ****) |
|
317 |
|
318 (*** Order Type calculations for radd ***) |
|
319 |
|
320 (** Addition with 0 **) |
|
321 |
|
322 Goal "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"; |
|
323 by (res_inst_tac [("d", "Inl")] lam_bijective 1); |
|
324 by Safe_tac; |
|
325 by (ALLGOALS Asm_simp_tac); |
|
326 qed "bij_sum_0"; |
|
327 |
|
328 Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"; |
|
329 by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1); |
|
330 by (assume_tac 2); |
|
331 by (Force_tac 1); |
|
332 qed "ordertype_sum_0_eq"; |
|
333 |
|
334 Goal "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"; |
|
335 by (res_inst_tac [("d", "Inr")] lam_bijective 1); |
|
336 by Safe_tac; |
|
337 by (ALLGOALS Asm_simp_tac); |
|
338 qed "bij_0_sum"; |
|
339 |
|
340 Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"; |
|
341 by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1); |
|
342 by (assume_tac 2); |
|
343 by (Force_tac 1); |
|
344 qed "ordertype_0_sum_eq"; |
|
345 |
|
346 (** Initial segments of radd. Statements by Grabczewski **) |
|
347 |
|
348 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *) |
|
349 Goalw [pred_def] |
|
350 "a:A ==> \ |
|
351 \ (lam x:pred(A,a,r). Inl(x)) \ |
|
352 \ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"; |
|
353 by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1); |
|
354 by Auto_tac; |
|
355 qed "pred_Inl_bij"; |
|
356 |
|
357 Goal "[| a:A; well_ord(A,r) |] ==> \ |
|
358 \ ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \ |
|
359 \ ordertype(pred(A,a,r), r)"; |
|
360 by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
361 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset])); |
|
362 by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1); |
|
363 qed "ordertype_pred_Inl_eq"; |
|
364 |
|
365 Goalw [pred_def, id_def] |
|
366 "b:B ==> \ |
|
367 \ id(A+pred(B,b,s)) \ |
|
368 \ : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"; |
|
369 by (res_inst_tac [("d", "%z. z")] lam_bijective 1); |
|
370 by Safe_tac; |
|
371 by (ALLGOALS (Asm_full_simp_tac)); |
|
372 qed "pred_Inr_bij"; |
|
373 |
|
374 Goal "[| b:B; well_ord(A,r); well_ord(B,s) |] ==> \ |
|
375 \ ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \ |
|
376 \ ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"; |
|
377 by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
378 by (force_tac (claset(), simpset() addsimps [pred_def, id_def]) 2); |
|
379 by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset])); |
|
380 qed "ordertype_pred_Inr_eq"; |
|
381 |
|
382 |
|
383 (*** ordify: trivial coercion to an ordinal ***) |
|
384 |
|
385 Goal "Ord(ordify(x))"; |
|
386 by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1); |
|
387 qed "Ord_ordify"; |
|
388 AddIffs [Ord_ordify]; |
|
389 AddTCs [Ord_ordify]; |
|
390 |
|
391 (*Collapsing*) |
|
392 Goal "ordify(ordify(x)) = ordify(x)"; |
|
393 by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1); |
|
394 qed "ordify_idem"; |
|
395 Addsimps [ordify_idem]; |
|
396 |
|
397 |
|
398 (*** Basic laws for ordinal addition ***) |
|
399 |
|
400 Goal "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"; |
|
401 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Ord_ordertype, well_ord_radd, well_ord_Memrel]) 1); |
|
402 qed "Ord_raw_oadd"; |
|
403 |
|
404 Goal "Ord(i++j)"; |
|
405 by (asm_full_simp_tac (simpset() addsimps [oadd_def, Ord_raw_oadd]) 1); |
|
406 qed "Ord_oadd"; |
|
407 AddIffs [Ord_oadd]; AddTCs [Ord_oadd]; |
|
408 |
|
409 |
|
410 (** Ordinal addition with zero **) |
|
411 |
|
412 Goal "Ord(i) ==> raw_oadd(i,0) = i"; |
|
413 by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_sum_0_eq, |
|
414 ordertype_Memrel, well_ord_Memrel]) 1); |
|
415 qed "raw_oadd_0"; |
|
416 |
|
417 Goal "Ord(i) ==> i++0 = i"; |
|
418 by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0, ordify_def]) 1); |
|
419 qed "oadd_0"; |
|
420 Addsimps [oadd_0]; |
|
421 |
|
422 Goal "Ord(i) ==> raw_oadd(0,i) = i"; |
|
423 by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_0_sum_eq, |
|
424 ordertype_Memrel, well_ord_Memrel]) 1); |
|
425 qed "raw_oadd_0_left"; |
|
426 |
|
427 Goal "Ord(i) ==> 0++i = i"; |
|
428 by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0_left, ordify_def]) 1); |
|
429 qed "oadd_0_left"; |
|
430 Addsimps [oadd_0_left]; |
|
431 |
|
432 |
|
433 Goal "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i) \ |
|
434 \ else (if Ord(j) then j else 0))"; |
|
435 by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, raw_oadd_0]) 1); |
|
436 qed "oadd_eq_if_raw_oadd"; |
|
437 |
|
438 |
|
439 Goal "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"; |
|
440 by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def]) 1); |
|
441 qed "raw_oadd_eq_oadd"; |
|
442 |
|
443 (*** Further properties of ordinal addition. Statements by Grabczewski, |
|
444 proofs by lcp. ***) |
|
445 |
|
446 (*Surely also provable by transfinite induction on j?*) |
|
447 Goal "k<i ==> k < i++j"; |
|
448 by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord2, raw_oadd_0]) 1); |
|
449 by (Clarify_tac 1); |
|
450 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); |
|
451 by (rtac ltE 1 THEN assume_tac 1); |
|
452 by (rtac ltI 1); |
|
453 by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2)); |
|
454 by (force_tac |
|
455 (claset(), |
|
456 simpset() addsimps [ordertype_pred_unfold, |
|
457 well_ord_radd, well_ord_Memrel, |
|
458 ordertype_pred_Inl_eq, |
|
459 lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1); |
|
460 qed "lt_oadd1"; |
|
461 |
|
462 (*Thus also we obtain the rule i++j = k ==> i le k *) |
|
463 Goal "Ord(i) ==> i le i++j"; |
|
464 by (rtac all_lt_imp_le 1); |
|
465 by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1)); |
|
466 qed "oadd_le_self"; |
|
467 |
|
468 (** A couple of strange but necessary results! **) |
|
469 |
|
470 Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"; |
|
471 by (resolve_tac [id_bij RS ord_isoI] 1); |
|
472 by (Asm_simp_tac 1); |
|
473 by (Blast_tac 1); |
|
474 qed "id_ord_iso_Memrel"; |
|
475 |
|
476 Goal "[| well_ord(A,r); k<j |] ==> \ |
|
477 \ ordertype(A+k, radd(A, r, k, Memrel(j))) = \ |
|
478 \ ordertype(A+k, radd(A, r, k, Memrel(k)))"; |
|
479 by (etac ltE 1); |
|
480 by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1); |
|
481 by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1); |
|
482 by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel])); |
|
483 qed "ordertype_sum_Memrel"; |
|
484 |
|
485 Goal "k<j ==> i++k < i++j"; |
|
486 by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, lt_Ord, lt_Ord2]) 1); |
|
487 by (Clarify_tac 1); |
|
488 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); |
|
489 by (rtac ltE 1 THEN assume_tac 1); |
|
490 by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1); |
|
491 by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel])); |
|
492 by (rtac RepFun_eqI 1); |
|
493 by (etac InrI 2); |
|
494 by (asm_simp_tac |
|
495 (simpset() addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, |
|
496 lt_pred_Memrel, leI RS le_ordertype_Memrel, |
|
497 ordertype_sum_Memrel]) 1); |
|
498 qed "oadd_lt_mono2"; |
|
499 |
|
500 Goal "[| i++j < i++k; Ord(j) |] ==> j<k"; |
|
501 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); |
|
502 by (forw_inst_tac [("i","i"),("j","j")] oadd_le_self 2); |
|
503 by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord, not_lt_iff_le RS iff_sym]) 2); |
|
504 by (rtac Ord_linear_lt 1); |
|
505 by (REPEAT_SOME assume_tac); |
|
506 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]))); |
|
507 by (ALLGOALS |
|
508 (blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym]))); |
|
509 qed "oadd_lt_cancel2"; |
|
510 |
|
511 Goal "Ord(j) ==> i++j < i++k <-> j<k"; |
|
512 by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1); |
|
513 qed "oadd_lt_iff2"; |
|
514 |
|
515 Goal "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"; |
|
516 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); |
|
517 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); |
|
518 by (rtac Ord_linear_lt 1); |
|
519 by (REPEAT_SOME assume_tac); |
|
520 by (ALLGOALS |
|
521 (force_tac (claset() addDs [inst "i" "i" oadd_lt_mono2], |
|
522 simpset() addsimps [lt_not_refl]))); |
|
523 qed "oadd_inject"; |
|
524 |
|
525 Goal "k < i++j ==> k<i | (EX l:j. k = i++l )"; |
|
526 by (asm_full_simp_tac (simpset() addsimps [inst "i" "j" Ord_in_Ord', oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); |
|
527 by (asm_full_simp_tac |
|
528 (simpset() addsimps [inst "i" "j" Ord_in_Ord', lt_def]) 2); |
|
529 by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, well_ord_radd, |
|
530 well_ord_Memrel, raw_oadd_def]) 1); |
|
531 by (eresolve_tac [ltD RS RepFunE] 1); |
|
532 by (force_tac (claset(), |
|
533 simpset() addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, |
|
534 ltI, lt_pred_Memrel, le_ordertype_Memrel, leI, |
|
535 ordertype_pred_Inr_eq, |
|
536 ordertype_sum_Memrel]) 1); |
|
537 qed "lt_oadd_disj"; |
|
538 |
|
539 |
|
540 (*** Ordinal addition with successor -- via associativity! ***) |
|
541 |
|
542 Goal "(i++j)++k = i++(j++k)"; |
|
543 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd, Ord_raw_oadd, raw_oadd_0, raw_oadd_0_left]) 1); |
|
544 by (Clarify_tac 1); |
|
545 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); |
|
546 by (resolve_tac [ordertype_eq RS trans] 1); |
|
547 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS |
|
548 sum_ord_iso_cong) 1); |
|
549 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); |
|
550 by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1); |
|
551 by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS |
|
552 ordertype_eq) 2); |
|
553 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1)); |
|
554 qed "oadd_assoc"; |
|
555 |
|
556 Goal "[| Ord(i); Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"; |
|
557 by (rtac (subsetI RS equalityI) 1); |
|
558 by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1); |
|
559 by (REPEAT (ares_tac [Ord_oadd] 1)); |
|
560 by (force_tac (claset() addIs [lt_oadd1, oadd_lt_mono2], |
|
561 simpset() addsimps [Ord_mem_iff_lt]) 3); |
|
562 by (Blast_tac 2); |
|
563 by (blast_tac (claset() addSEs [ltE]) 1); |
|
564 qed "oadd_unfold"; |
|
565 |
|
566 Goal "Ord(i) ==> i++1 = succ(i)"; |
|
567 by (asm_simp_tac (simpset() addsimps [oadd_unfold, Ord_1, oadd_0]) 1); |
|
568 by (Blast_tac 1); |
|
569 qed "oadd_1"; |
|
570 |
|
571 Goal "Ord(j) ==> i++succ(j) = succ(i++j)"; |
|
572 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); |
|
573 by (Clarify_tac 1); |
|
574 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); |
|
575 by (asm_simp_tac (simpset() |
|
576 addsimps [inst "i" "j" oadd_1 RS sym, inst "i" "i++j" oadd_1 RS sym, oadd_assoc]) 1); |
|
577 qed "oadd_succ"; |
|
578 Addsimps [oadd_succ]; |
|
579 |
|
580 |
|
581 (** Ordinal addition with limit ordinals **) |
|
582 |
|
583 val prems = |
|
584 Goal "[| !!x. x:A ==> Ord(j(x)); a:A |] ==> \ |
|
585 \ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; |
|
586 by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, |
|
587 lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD] |
|
588 addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1); |
|
589 qed "oadd_UN"; |
|
590 |
|
591 Goal "Limit(j) ==> i++j = (UN k:j. i++k)"; |
|
592 by (forward_tac [Limit_has_0 RS ltD] 1); |
|
593 by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, |
|
594 oadd_UN RS sym, Union_eq_UN RS sym, |
|
595 Limit_Union_eq]) 1); |
|
596 qed "oadd_Limit"; |
|
597 |
|
598 (** Order/monotonicity properties of ordinal addition **) |
|
599 |
|
600 Goal "Ord(i) ==> i le j++i"; |
|
601 by (eres_inst_tac [("i","i")] trans_induct3 1); |
|
602 by (asm_simp_tac (simpset() addsimps [Ord_0_le]) 1); |
|
603 by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_leI]) 1); |
|
604 by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1); |
|
605 by (rtac le_trans 1); |
|
606 by (rtac le_implies_UN_le_UN 2); |
|
607 by (etac bspec 2); |
|
608 by (assume_tac 2); |
|
609 by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, |
|
610 le_refl, Limit_is_Ord]) 1); |
|
611 qed "oadd_le_self2"; |
|
612 |
|
613 Goal "k le j ==> k++i le j++i"; |
|
614 by (ftac lt_Ord 1); |
|
615 by (ftac le_Ord2 1); |
|
616 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); |
|
617 by (Clarify_tac 1); |
|
618 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); |
|
619 by (eres_inst_tac [("i","i")] trans_induct3 1); |
|
620 by (Asm_simp_tac 1); |
|
621 by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1); |
|
622 by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1); |
|
623 by (rtac le_implies_UN_le_UN 1); |
|
624 by (Blast_tac 1); |
|
625 qed "oadd_le_mono1"; |
|
626 |
|
627 Goal "[| i' le i; j'<j |] ==> i'++j' < i++j"; |
|
628 by (rtac lt_trans1 1); |
|
629 by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE, |
|
630 Ord_succD] 1)); |
|
631 qed "oadd_lt_mono"; |
|
632 |
|
633 Goal "[| i' le i; j' le j |] ==> i'++j' le i++j"; |
|
634 by (asm_simp_tac (simpset() delsimps [oadd_succ] |
|
635 addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1); |
|
636 qed "oadd_le_mono"; |
|
637 |
|
638 Goal "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"; |
|
639 by (asm_simp_tac (simpset() delsimps [oadd_succ] |
|
640 addsimps [oadd_lt_iff2, oadd_succ RS sym, Ord_succ]) 1); |
|
641 qed "oadd_le_iff2"; |
|
642 |
|
643 |
|
644 (** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). |
|
645 Probably simpler to define the difference recursively! |
|
646 **) |
|
647 |
|
648 Goal "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"; |
|
649 by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1); |
|
650 by (blast_tac (claset() addSIs [if_type]) 1); |
|
651 by (fast_tac (claset() addSIs [case_type]) 1); |
|
652 by (etac sumE 2); |
|
653 by (ALLGOALS Asm_simp_tac); |
|
654 qed "bij_sum_Diff"; |
|
655 |
|
656 Goal "i le j ==> \ |
|
657 \ ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) = \ |
|
658 \ ordertype(j, Memrel(j))"; |
|
659 by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); |
|
660 by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1); |
|
661 by (etac well_ord_Memrel 3); |
|
662 by (assume_tac 1); |
|
663 by (Asm_simp_tac 1); |
|
664 by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1); |
|
665 by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1); |
|
666 by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1); |
|
667 by (blast_tac (claset() addIs [lt_trans2, lt_trans]) 1); |
|
668 qed "ordertype_sum_Diff"; |
|
669 |
|
670 Goalw [odiff_def] |
|
671 "[| Ord(i); Ord(j) |] ==> Ord(i--j)"; |
|
672 by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, |
|
673 Diff_subset] 1)); |
|
674 qed "Ord_odiff"; |
|
675 Addsimps [Ord_odiff]; AddTCs [Ord_odiff]; |
|
676 |
|
677 |
|
678 Goal |
|
679 "i le j \ |
|
680 \ ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"; |
|
681 by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, odiff_def]) 1); |
|
682 by (safe_tac (claset() addSDs [le_subset_iff RS iffD1])); |
|
683 by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1); |
|
684 by (etac id_ord_iso_Memrel 1); |
|
685 by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1); |
|
686 by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset, |
|
687 Diff_subset] 1)); |
|
688 qed "raw_oadd_ordertype_Diff"; |
|
689 |
|
690 Goal "i le j ==> i ++ (j--i) = j"; |
|
691 by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2, oadd_def, ordify_def, raw_oadd_ordertype_Diff, ordertype_sum_Diff, |
|
692 ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1); |
|
693 qed "oadd_odiff_inverse"; |
|
694 |
|
695 (*By oadd_inject, the difference between i and j is unique. Note that we get |
|
696 i++j = k ==> j = k--i. *) |
|
697 Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"; |
|
698 by (rtac oadd_inject 1); |
|
699 by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2)); |
|
700 by (blast_tac (claset() addIs [oadd_odiff_inverse, oadd_le_self]) 1); |
|
701 qed "odiff_oadd_inverse"; |
|
702 |
|
703 Goal "[| i<j; k le i |] ==> i--k < j--k"; |
|
704 by (res_inst_tac [("i","k")] oadd_lt_cancel2 1); |
|
705 by (asm_full_simp_tac (simpset() addsimps [oadd_odiff_inverse]) 1); |
|
706 by (stac oadd_odiff_inverse 1); |
|
707 by (blast_tac (claset() addIs [le_trans, leI]) 1); |
|
708 by (assume_tac 1); |
|
709 by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2]) 1); |
|
710 qed "odiff_lt_mono2"; |
|
711 |
|
712 |
|
713 (**** Ordinal Multiplication ****) |
|
714 |
|
715 Goalw [omult_def] |
|
716 "[| Ord(i); Ord(j) |] ==> Ord(i**j)"; |
|
717 by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1)); |
|
718 qed "Ord_omult"; |
|
719 Addsimps [Ord_omult]; AddTCs [Ord_omult]; |
|
720 |
|
721 (*** A useful unfolding law ***) |
|
722 |
|
723 Goalw [pred_def] |
|
724 "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) = \ |
|
725 \ pred(A,a,r)*B Un ({a} * pred(B,b,s))"; |
|
726 by (Blast_tac 1); |
|
727 qed "pred_Pair_eq"; |
|
728 |
|
729 Goal "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \ |
|
730 \ ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \ |
|
731 \ ordertype(pred(A,a,r)*B + pred(B,b,s), \ |
|
732 \ radd(A*B, rmult(A,r,B,s), B, s))"; |
|
733 by (asm_simp_tac (simpset() addsimps [pred_Pair_eq]) 1); |
|
734 by (resolve_tac [ordertype_eq RS sym] 1); |
|
735 by (rtac prod_sum_singleton_ord_iso 1); |
|
736 by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset])); |
|
737 by (blast_tac (claset() addSEs [predE]) 1); |
|
738 qed "ordertype_pred_Pair_eq"; |
|
739 |
|
740 Goalw [raw_oadd_def, omult_def] |
|
741 "[| i'<i; j'<j |] ==> \ |
|
742 \ ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \ |
|
743 \ rmult(i,Memrel(i),j,Memrel(j))) = \ |
|
744 \ raw_oadd (j**i', j')"; |
|
745 by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, |
|
746 ltD, lt_Ord2, well_ord_Memrel]) 1); |
|
747 by (rtac trans 1); |
|
748 by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2); |
|
749 by (rtac ord_iso_refl 3); |
|
750 by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1); |
|
751 by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst])); |
|
752 by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
|
753 Ord_ordertype])); |
|
754 by (ALLGOALS Asm_simp_tac); |
|
755 by Safe_tac; |
|
756 by (ALLGOALS (blast_tac (claset() addIs [Ord_trans]))); |
|
757 qed "ordertype_pred_Pair_lemma"; |
|
758 |
|
759 Goalw [omult_def] |
|
760 "[| Ord(i); Ord(j); k<j**i |] ==> \ |
|
761 \ EX j' i'. k = j**i' ++ j' & j'<j & i'<i"; |
|
762 by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, |
|
763 well_ord_rmult, well_ord_Memrel]) 1); |
|
764 by (safe_tac (claset() addSEs [ltE])); |
|
765 by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI, |
|
766 symmetric omult_def, |
|
767 inst "i" "i" Ord_in_Ord', inst "i" "j" Ord_in_Ord', raw_oadd_eq_oadd]) 1); |
|
768 by (blast_tac (claset() addIs [ltI]) 1); |
|
769 qed "lt_omult"; |
|
770 |
|
771 Goalw [omult_def] |
|
772 "[| j'<j; i'<i |] ==> j**i' ++ j' < j**i"; |
|
773 by (rtac ltI 1); |
|
774 by (asm_simp_tac |
|
775 (simpset() addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, |
|
776 lt_Ord2]) 2); |
|
777 by (asm_simp_tac |
|
778 (simpset() addsimps [ordertype_pred_unfold, |
|
779 well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1); |
|
780 by (rtac bexI 1); |
|
781 by (blast_tac (claset() addSEs [ltE]) 2); |
|
782 by (asm_simp_tac |
|
783 (simpset() addsimps [ordertype_pred_Pair_lemma, ltI, |
|
784 symmetric omult_def]) 1); |
|
785 by (asm_simp_tac (simpset() addsimps [ |
|
786 lt_Ord, lt_Ord2, raw_oadd_eq_oadd]) 1); |
|
787 qed "omult_oadd_lt"; |
|
788 |
|
789 Goal "[| Ord(i); Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"; |
|
790 by (rtac (subsetI RS equalityI) 1); |
|
791 by (resolve_tac [lt_omult RS exE] 1); |
|
792 by (etac ltI 3); |
|
793 by (REPEAT (ares_tac [Ord_omult] 1)); |
|
794 by (blast_tac (claset() addSEs [ltE]) 1); |
|
795 by (blast_tac (claset() addIs [omult_oadd_lt RS ltD, ltI]) 1); |
|
796 qed "omult_unfold"; |
|
797 |
|
798 (*** Basic laws for ordinal multiplication ***) |
|
799 |
|
800 (** Ordinal multiplication by zero **) |
|
801 |
|
802 Goalw [omult_def] "i**0 = 0"; |
|
803 by (Asm_simp_tac 1); |
|
804 qed "omult_0"; |
|
805 |
|
806 Goalw [omult_def] "0**i = 0"; |
|
807 by (Asm_simp_tac 1); |
|
808 qed "omult_0_left"; |
|
809 |
|
810 Addsimps [omult_0, omult_0_left]; |
|
811 |
|
812 (** Ordinal multiplication by 1 **) |
|
813 |
|
814 Goalw [omult_def] "Ord(i) ==> i**1 = i"; |
|
815 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); |
|
816 by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1); |
|
817 by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, |
|
818 well_ord_Memrel, ordertype_Memrel])); |
|
819 by (ALLGOALS Asm_simp_tac); |
|
820 qed "omult_1"; |
|
821 |
|
822 Goalw [omult_def] "Ord(i) ==> 1**i = i"; |
|
823 by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1); |
|
824 by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1); |
|
825 by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, |
|
826 well_ord_Memrel, ordertype_Memrel])); |
|
827 by (ALLGOALS Asm_simp_tac); |
|
828 qed "omult_1_left"; |
|
829 |
|
830 Addsimps [omult_1, omult_1_left]; |
|
831 |
|
832 (** Distributive law for ordinal multiplication and addition **) |
|
833 |
|
834 Goal "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"; |
|
835 by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); |
|
836 by (asm_full_simp_tac (simpset() addsimps [omult_def, raw_oadd_def]) 1); |
|
837 by (resolve_tac [ordertype_eq RS trans] 1); |
|
838 by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS |
|
839 prod_ord_iso_cong) 1); |
|
840 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
|
841 Ord_ordertype] 1)); |
|
842 by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1); |
|
843 by (rtac ordertype_eq 2); |
|
844 by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2); |
|
845 by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, |
|
846 Ord_ordertype] 1)); |
|
847 qed "oadd_omult_distrib"; |
|
848 |
|
849 Goal "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"; |
|
850 by (asm_simp_tac (simpset() |
|
851 delsimps [oadd_succ] |
|
852 addsimps [inst "i" "j" oadd_1 RS sym, oadd_omult_distrib]) 1); |
|
853 qed "omult_succ"; |
|
854 |
|
855 (** Associative law **) |
|
856 |
|
857 Goalw [omult_def] |
|
858 "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"; |
|
859 by (resolve_tac [ordertype_eq RS trans] 1); |
|
860 by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS |
|
861 prod_ord_iso_cong) 1); |
|
862 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1)); |
|
863 by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS |
|
864 ordertype_eq RS trans] 1); |
|
865 by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS |
|
866 ordertype_eq) 2); |
|
867 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1)); |
|
868 qed "omult_assoc"; |
|
869 |
|
870 |
|
871 (** Ordinal multiplication with limit ordinals **) |
|
872 |
|
873 val prems = |
|
874 Goal "[| Ord(i); !!x. x:A ==> Ord(j(x)) |] ==> \ |
|
875 \ i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"; |
|
876 by (asm_simp_tac (simpset() addsimps prems @ [Ord_UN, omult_unfold]) 1); |
|
877 by (Blast_tac 1); |
|
878 qed "omult_UN"; |
|
879 |
|
880 Goal "[| Ord(i); Limit(j) |] ==> i**j = (UN k:j. i**k)"; |
|
881 by (asm_simp_tac |
|
882 (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, |
|
883 Union_eq_UN RS sym, Limit_Union_eq]) 1); |
|
884 qed "omult_Limit"; |
|
885 |
|
886 |
|
887 (*** Ordering/monotonicity properties of ordinal multiplication ***) |
|
888 |
|
889 (*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *) |
|
890 Goal "[| k<i; 0<j |] ==> k < i**j"; |
|
891 by (safe_tac (claset() addSEs [ltE] addSIs [ltI, Ord_omult])); |
|
892 by (asm_simp_tac (simpset() addsimps [omult_unfold]) 1); |
|
893 by (REPEAT_FIRST (ares_tac [bexI])); |
|
894 by (Asm_simp_tac 1); |
|
895 qed "lt_omult1"; |
|
896 |
|
897 Goal "[| Ord(i); 0<j |] ==> i le i**j"; |
|
898 by (rtac all_lt_imp_le 1); |
|
899 by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1)); |
|
900 qed "omult_le_self"; |
|
901 |
|
902 Goal "[| k le j; Ord(i) |] ==> k**i le j**i"; |
|
903 by (ftac lt_Ord 1); |
|
904 by (ftac le_Ord2 1); |
|
905 by (etac trans_induct3 1); |
|
906 by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1); |
|
907 by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1); |
|
908 by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1); |
|
909 by (rtac le_implies_UN_le_UN 1); |
|
910 by (Blast_tac 1); |
|
911 qed "omult_le_mono1"; |
|
912 |
|
913 Goal "[| k<j; 0<i |] ==> i**k < i**j"; |
|
914 by (rtac ltI 1); |
|
915 by (asm_simp_tac (simpset() addsimps [omult_unfold, lt_Ord2]) 1); |
|
916 by (safe_tac (claset() addSEs [ltE] addSIs [Ord_omult])); |
|
917 by (REPEAT_FIRST (ares_tac [bexI])); |
|
918 by (asm_simp_tac (simpset() addsimps [Ord_omult]) 1); |
|
919 qed "omult_lt_mono2"; |
|
920 |
|
921 Goal "[| k le j; Ord(i) |] ==> i**k le i**j"; |
|
922 by (rtac subset_imp_le 1); |
|
923 by (safe_tac (claset() addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult])); |
|
924 by (asm_full_simp_tac (simpset() addsimps [omult_unfold]) 1); |
|
925 by (deepen_tac (claset() addEs [Ord_trans]) 0 1); |
|
926 qed "omult_le_mono2"; |
|
927 |
|
928 Goal "[| i' le i; j' le j |] ==> i'**j' le i**j"; |
|
929 by (rtac le_trans 1); |
|
930 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE, |
|
931 Ord_succD] 1)); |
|
932 qed "omult_le_mono"; |
|
933 |
|
934 Goal "[| i' le i; j'<j; 0<i |] ==> i'**j' < i**j"; |
|
935 by (rtac lt_trans1 1); |
|
936 by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE, |
|
937 Ord_succD] 1)); |
|
938 qed "omult_lt_mono"; |
|
939 |
|
940 Goal "[| Ord(i); 0<j |] ==> i le j**i"; |
|
941 by (ftac lt_Ord2 1); |
|
942 by (eres_inst_tac [("i","i")] trans_induct3 1); |
|
943 by (Asm_simp_tac 1); |
|
944 by (asm_simp_tac (simpset() addsimps [omult_succ]) 1); |
|
945 by (etac lt_trans1 1); |
|
946 by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN |
|
947 rtac oadd_lt_mono2 2); |
|
948 by (REPEAT (ares_tac [Ord_omult] 1)); |
|
949 by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1); |
|
950 by (rtac le_trans 1); |
|
951 by (rtac le_implies_UN_le_UN 2); |
|
952 by (Blast_tac 2); |
|
953 by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, |
|
954 Limit_is_Ord]) 1); |
|
955 qed "omult_le_self2"; |
|
956 |
|
957 |
|
958 (** Further properties of ordinal multiplication **) |
|
959 |
|
960 Goal "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"; |
|
961 by (rtac Ord_linear_lt 1); |
|
962 by (REPEAT_SOME assume_tac); |
|
963 by (ALLGOALS |
|
964 (force_tac (claset() addDs [omult_lt_mono2], |
|
965 simpset() addsimps [lt_not_refl]))); |
|
966 qed "omult_inject"; |
|
967 |
|