1 (* Title: ZF/OrderType.thy
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Copyright 1994 University of Cambridge
6 header{*Order Types and Ordinal Arithmetic*}
8 theory OrderType imports OrderArith OrdQuant Nat_ZF begin
10 text{*The order type of a well-ordering is the least ordinal isomorphic to it.
11 Ordinal arithmetic is traditionally defined in terms of order types, as it is
12 here. But a definition by transfinite recursion would be much simpler!*}
15 ordermap :: "[i,i]=>i" where
16 "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
19 ordertype :: "[i,i]=>i" where
20 "ordertype(A,r) == ordermap(A,r)``A"
23 (*alternative definition of ordinal numbers*)
24 Ord_alt :: "i => o" where
25 "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
28 (*coercion to ordinal: if not, just 0*)
29 ordify :: "i=>i" where
30 "ordify(x) == if Ord(x) then x else 0"
33 (*ordinal multiplication*)
34 omult :: "[i,i]=>i" (infixl "**" 70) where
35 "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
39 raw_oadd :: "[i,i]=>i" where
40 "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
43 oadd :: "[i,i]=>i" (infixl "++" 65) where
44 "i ++ j == raw_oadd(ordify(i),ordify(j))"
47 (*ordinal subtraction*)
48 odiff :: "[i,i]=>i" (infixl "--" 65) where
49 "i -- j == ordertype(i-j, Memrel(i))"
53 omult (infixl "\<times>\<times>" 70)
55 notation (HTML output)
56 omult (infixl "\<times>\<times>" 70)
59 subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}
61 lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
62 apply (rule well_ordI)
63 apply (rule wf_Memrel [THEN wf_imp_wf_on])
64 apply (simp add: ltD lt_Ord linear_def
65 ltI [THEN lt_trans2 [of _ j i]])
66 apply (intro ballI Ord_linear)
67 apply (blast intro: Ord_in_Ord lt_Ord)+
70 (*"Ord(i) ==> well_ord(i, Memrel(i))"*)
71 lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel]
73 (*Kunen's Theorem 7.3 (i), page 16; see also Ordinal/Ord_in_Ord
74 The smaller ordinal is an initial segment of the larger *)
76 "j<i ==> pred(i, j, Memrel(i)) = j"
77 apply (unfold pred_def lt_def)
78 apply (simp (no_asm_simp))
79 apply (blast intro: Ord_trans)
83 "x:A ==> pred(A, x, Memrel(A)) = A Int x"
84 by (unfold pred_def Memrel_def, blast)
86 lemma Ord_iso_implies_eq_lemma:
87 "[| j<i; f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
88 apply (frule lt_pred_Memrel)
90 apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)
91 apply (unfold ord_iso_def)
92 (*Combining the two simplifications causes looping*)
93 apply (simp (no_asm_simp))
94 apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
97 (*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
98 lemma Ord_iso_implies_eq:
99 "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |]
101 apply (rule_tac i = i and j = j in Ord_linear_lt)
102 apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
106 subsection{*Ordermap and ordertype*}
109 "ordermap(A,r) : A -> ordertype(A,r)"
110 apply (unfold ordermap_def ordertype_def)
111 apply (rule lam_type)
112 apply (rule lamI [THEN imageI], assumption+)
115 subsubsection{*Unfolding of ordermap *}
117 (*Useful for cardinality reasoning; see CardinalArith.ML*)
118 lemma ordermap_eq_image:
120 ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
121 apply (unfold ordermap_def pred_def)
122 apply (simp (no_asm_simp))
123 apply (erule wfrec_on [THEN trans], assumption)
124 apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
127 (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
128 lemma ordermap_pred_unfold:
130 ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
131 by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
133 (*pred-unfolded version. NOT suitable for rewriting -- loops!*)
134 lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def]
136 (*The theorem above is
138 [| wf[A](r); x : A |]
139 ==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
141 NOTE: the definition of ordermap used here delivers ordinals only if r is
142 transitive. If r is the predecessor relation on the naturals then
143 ordermap(nat,predr) ` n equals {n-1} and not n. A more complicated definition,
146 ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
148 might eliminate the need for r to be transitive.
152 subsubsection{*Showing that ordermap, ordertype yield ordinals *}
155 "[| well_ord(A,r); x:A |] ==> Ord(ordermap(A,r) ` x)"
156 apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
157 apply (rule_tac a=x in wf_on_induct, assumption+)
158 apply (simp (no_asm_simp) add: ordermap_pred_unfold)
159 apply (rule OrdI [OF _ Ord_is_Transset])
160 apply (unfold pred_def Transset_def)
161 apply (blast intro: trans_onD
162 dest!: ordermap_unfold [THEN equalityD1])+
166 "well_ord(A,r) ==> Ord(ordertype(A,r))"
167 apply (unfold ordertype_def)
168 apply (subst image_fun [OF ordermap_type subset_refl])
169 apply (rule OrdI [OF _ Ord_is_Transset])
170 prefer 2 apply (blast intro: Ord_ordermap)
171 apply (unfold Transset_def well_ord_def)
172 apply (blast intro: trans_onD
173 dest!: ordermap_unfold [THEN equalityD1])
177 subsubsection{*ordermap preserves the orderings in both directions *}
180 "[| <w,x>: r; wf[A](r); w: A; x: A |]
181 ==> ordermap(A,r)`w : ordermap(A,r)`x"
182 apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)
185 (*linearity of r is crucial here*)
186 lemma converse_ordermap_mono:
187 "[| ordermap(A,r)`w : ordermap(A,r)`x; well_ord(A,r); w: A; x: A |]
189 apply (unfold well_ord_def tot_ord_def, safe)
190 apply (erule_tac x=w and y=x in linearE, assumption+)
191 apply (blast elim!: mem_not_refl [THEN notE])
192 apply (blast dest: ordermap_mono intro: mem_asym)
195 lemmas ordermap_surj =
196 ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
199 "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
200 apply (unfold well_ord_def tot_ord_def bij_def inj_def)
201 apply (force intro!: ordermap_type ordermap_surj
202 elim: linearE dest: ordermap_mono
203 simp add: mem_not_refl)
206 subsubsection{*Isomorphisms involving ordertype *}
208 lemma ordertype_ord_iso:
210 ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
211 apply (unfold ord_iso_def)
212 apply (safe elim!: well_ord_is_wf
213 intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
214 apply (blast dest!: converse_ordermap_mono)
218 "[| f: ord_iso(A,r,B,s); well_ord(B,s) |]
219 ==> ordertype(A,r) = ordertype(B,s)"
220 apply (frule well_ord_ord_iso, assumption)
221 apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)
222 apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)
225 lemma ordertype_eq_imp_ord_iso:
226 "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r); well_ord(B,s) |]
227 ==> EX f. f: ord_iso(A,r,B,s)"
229 apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
231 apply (erule ordertype_ord_iso [THEN ord_iso_sym])
234 subsubsection{*Basic equalities for ordertype *}
236 (*Ordertype of Memrel*)
237 lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
238 apply (rule Ord_iso_implies_eq [symmetric])
239 apply (erule ltE, assumption)
240 apply (blast intro: le_well_ord_Memrel Ord_ordertype)
241 apply (rule ord_iso_trans)
242 apply (erule_tac [2] le_well_ord_Memrel [THEN ordertype_ord_iso])
243 apply (rule id_bij [THEN ord_isoI])
244 apply (simp (no_asm_simp))
245 apply (fast elim: ltE Ord_in_Ord Ord_trans)
248 (*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
249 lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
251 lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
252 apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])
254 apply (rule well_ord_0)
255 apply (rule Ord_0 [THEN ordertype_Memrel])
258 (*Ordertype of rvimage: [| f: bij(A,B); well_ord(B,s) |] ==>
259 ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
260 lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
262 subsubsection{*A fundamental unfolding law for ordertype. *}
264 (*Ordermap returns the same result if applied to an initial segment*)
265 lemma ordermap_pred_eq_ordermap:
266 "[| well_ord(A,r); y:A; z: pred(A,y,r) |]
267 ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
268 apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])
269 apply (rule_tac a=z in wf_on_induct, assumption+)
270 apply (safe elim!: predE)
271 apply (simp (no_asm_simp) add: ordermap_pred_unfold well_ord_is_wf pred_iff)
272 (*combining these two simplifications LOOPS! *)
273 apply (simp (no_asm_simp) add: pred_pred_eq)
274 apply (simp add: pred_def)
275 apply (rule RepFun_cong [OF _ refl])
276 apply (drule well_ord_is_trans_on)
277 apply (fast elim!: trans_onD)
280 lemma ordertype_unfold:
281 "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
282 apply (unfold ordertype_def)
283 apply (rule image_fun [OF ordermap_type subset_refl])
286 text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
288 lemma ordertype_pred_subset: "[| well_ord(A,r); x:A |] ==>
289 ordertype(pred(A,x,r),r) <= ordertype(A,r)"
290 apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
291 apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
294 lemma ordertype_pred_lt:
295 "[| well_ord(A,r); x:A |]
296 ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"
297 apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])
298 apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])
299 apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])
300 apply (erule_tac [3] well_ord_iso_predE)
301 apply (simp_all add: well_ord_subset [OF _ pred_subset])
304 (*May rewrite with this -- provided no rules are supplied for proving that
305 well_ord(pred(A,x,r), r) *)
306 lemma ordertype_pred_unfold:
308 ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"
309 apply (rule equalityI)
310 apply (safe intro!: ordertype_pred_lt [THEN ltD])
311 apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]
312 ordermap_type [THEN image_fun]
313 ordermap_pred_eq_ordermap pred_subset)
317 subsection{*Alternative definition of ordinal*}
319 (*proof by Krzysztof Grabczewski*)
320 lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
321 apply (unfold Ord_alt_def)
323 apply (erule well_ord_Memrel)
324 apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)
328 lemma Ord_alt_is_Ord:
329 "Ord_alt(i) ==> Ord(i)"
330 apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def
331 tot_ord_def part_ord_def trans_on_def)
332 apply (simp add: pred_Memrel)
333 apply (blast elim!: equalityE)
337 subsection{*Ordinal Addition*}
339 subsubsection{*Order Type calculations for radd *}
341 text{*Addition with 0 *}
343 lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
344 apply (rule_tac d = Inl in lam_bijective, safe)
345 apply (simp_all (no_asm_simp))
348 lemma ordertype_sum_0_eq:
349 "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
350 apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])
351 prefer 2 apply assumption
355 lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
356 apply (rule_tac d = Inr in lam_bijective, safe)
357 apply (simp_all (no_asm_simp))
360 lemma ordertype_0_sum_eq:
361 "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
362 apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])
363 prefer 2 apply assumption
367 text{*Initial segments of radd. Statements by Grabczewski *}
369 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
371 "a:A ==> (lam x:pred(A,a,r). Inl(x))
372 : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
373 apply (unfold pred_def)
374 apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
378 lemma ordertype_pred_Inl_eq:
379 "[| a:A; well_ord(A,r) |]
380 ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =
381 ordertype(pred(A,a,r), r)"
382 apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
383 apply (simp_all add: well_ord_subset [OF _ pred_subset])
384 apply (simp add: pred_def)
390 : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
391 apply (unfold pred_def id_def)
392 apply (rule_tac d = "%z. z" in lam_bijective, auto)
395 lemma ordertype_pred_Inr_eq:
396 "[| b:B; well_ord(A,r); well_ord(B,s) |]
397 ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =
398 ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
399 apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
400 prefer 2 apply (force simp add: pred_def id_def, assumption)
401 apply (blast intro: well_ord_radd well_ord_subset [OF _ pred_subset])
405 subsubsection{*ordify: trivial coercion to an ordinal *}
407 lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
408 by (simp add: ordify_def)
411 lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"
412 by (simp add: ordify_def)
415 subsubsection{*Basic laws for ordinal addition *}
417 lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
418 by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
421 lemma Ord_oadd [iff,TC]: "Ord(i++j)"
422 by (simp add: oadd_def Ord_raw_oadd)
425 text{*Ordinal addition with zero *}
427 lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
428 by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
429 ordertype_Memrel well_ord_Memrel)
431 lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
432 apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
435 lemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"
436 by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel
439 lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
440 by (simp add: oadd_def raw_oadd_0_left ordify_def)
443 lemma oadd_eq_if_raw_oadd:
444 "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)
445 else (if Ord(j) then j else 0))"
446 by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
448 lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
449 by (simp add: oadd_def ordify_def)
451 (*** Further properties of ordinal addition. Statements by Grabczewski,
454 (*Surely also provable by transfinite induction on j?*)
455 lemma lt_oadd1: "k<i ==> k < i++j"
456 apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)
457 apply (simp add: raw_oadd_def)
458 apply (rule ltE, assumption)
460 apply (force simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel
461 ordertype_pred_Inl_eq lt_pred_Memrel leI [THEN le_ordertype_Memrel])
462 apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
465 (*Thus also we obtain the rule i++j = k ==> i le k *)
466 lemma oadd_le_self: "Ord(i) ==> i le i++j"
467 apply (rule all_lt_imp_le)
468 apply (auto simp add: Ord_oadd lt_oadd1)
471 text{*Various other results *}
473 lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
474 apply (rule id_bij [THEN ord_isoI])
475 apply (simp (no_asm_simp))
479 lemma subset_ord_iso_Memrel:
480 "[| f: ord_iso(A,Memrel(B),C,r); A<=B |] ==> f: ord_iso(A,Memrel(A),C,r)"
481 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])
482 apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)
483 apply (simp add: right_comp_id)
486 lemma restrict_ord_iso:
487 "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r); a \<in> A; j < i;
489 ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
491 apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
492 apply (frule ord_iso_restrict_pred, assumption)
493 apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)
494 apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])
497 lemma restrict_ord_iso2:
498 "[| f \<in> ord_iso(Order.pred(A,a,r), r, i, Memrel(i)); a \<in> A;
499 j < i; trans[A](r) |]
500 ==> converse(restrict(converse(f), j))
501 \<in> ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"
502 by (blast intro: restrict_ord_iso ord_iso_sym ltI)
504 lemma ordertype_sum_Memrel:
505 "[| well_ord(A,r); k<j |]
506 ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =
507 ordertype(A+k, radd(A, r, k, Memrel(k)))"
509 apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
510 apply (erule OrdmemD [THEN id_ord_iso_Memrel, THEN ord_iso_sym])
511 apply (simp_all add: well_ord_radd well_ord_Memrel)
514 lemma oadd_lt_mono2: "k<j ==> i++k < i++j"
515 apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)
516 apply (simp add: raw_oadd_def)
517 apply (rule ltE, assumption)
518 apply (rule ordertype_pred_unfold [THEN equalityD2, THEN subsetD, THEN ltI])
519 apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
521 apply (erule_tac [2] InrI)
522 apply (simp add: ordertype_pred_Inr_eq well_ord_Memrel lt_pred_Memrel
523 leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)
526 lemma oadd_lt_cancel2: "[| i++j < i++k; Ord(j) |] ==> j<k"
527 apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm)
529 apply (frule_tac i = i and j = j in oadd_le_self)
530 apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
531 apply (rule Ord_linear_lt, auto)
532 apply (simp_all add: raw_oadd_eq_oadd)
533 apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
536 lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
537 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
539 lemma oadd_inject: "[| i++j = i++k; Ord(j); Ord(k) |] ==> j=k"
540 apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
541 apply (simp add: raw_oadd_eq_oadd)
542 apply (rule Ord_linear_lt, auto)
543 apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
546 lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
547 apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
548 split add: split_if_asm)
550 apply (simp add: Ord_in_Ord' [of _ j] lt_def)
551 apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
552 apply (erule ltD [THEN RepFunE])
553 apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI
554 lt_pred_Memrel le_ordertype_Memrel leI
555 ordertype_pred_Inr_eq ordertype_sum_Memrel)
559 subsubsection{*Ordinal addition with successor -- via associativity! *}
561 lemma oadd_assoc: "(i++j)++k = i++(j++k)"
562 apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
563 apply (simp add: raw_oadd_def)
564 apply (rule ordertype_eq [THEN trans])
565 apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
567 apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
568 apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
569 apply (rule_tac [2] ordertype_eq)
570 apply (rule_tac [2] sum_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso])
571 apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
574 lemma oadd_unfold: "[| Ord(i); Ord(j) |] ==> i++j = i Un (\<Union>k\<in>j. {i++k})"
575 apply (rule subsetI [THEN equalityI])
576 apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
577 apply (blast intro: Ord_oadd)
578 apply (blast elim!: ltE, blast)
579 apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
582 lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
583 apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
587 lemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"
588 apply (simp add: oadd_eq_if_raw_oadd, clarify)
589 apply (simp add: raw_oadd_eq_oadd)
590 apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]
595 text{*Ordinal addition with limit ordinals *}
598 "[| !!x. x:A ==> Ord(j(x)); a:A |]
599 ==> i ++ (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i++j(x))"
600 by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]
601 oadd_lt_mono2 [THEN ltD]
602 elim!: ltE dest!: ltI [THEN lt_oadd_disj])
604 lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k\<in>j. i++k)"
605 apply (frule Limit_has_0 [THEN ltD])
606 apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]
607 Union_eq_UN [symmetric] Limit_Union_eq)
610 lemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"
611 apply (erule trans_induct3 [of j])
612 apply (simp_all add: oadd_Limit)
613 apply (simp add: Union_empty_iff Limit_def lt_def, blast)
616 lemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"
617 by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)
619 lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"
620 apply (simp add: oadd_Limit)
621 apply (frule Limit_has_1 [THEN ltD])
622 apply (rule increasing_LimitI)
623 apply (rule Ord_0_lt)
624 apply (blast intro: Ord_in_Ord [OF Limit_is_Ord])
625 apply (force simp add: Union_empty_iff oadd_eq_0_iff
626 Limit_is_Ord [of j, THEN Ord_in_Ord], auto)
627 apply (rule_tac x="succ(y)" in bexI)
628 apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])
629 apply (simp add: Limit_def lt_def)
632 text{*Order/monotonicity properties of ordinal addition *}
634 lemma oadd_le_self2: "Ord(i) ==> i le j++i"
635 apply (erule_tac i = i in trans_induct3)
636 apply (simp (no_asm_simp) add: Ord_0_le)
637 apply (simp (no_asm_simp) add: oadd_succ succ_leI)
638 apply (simp (no_asm_simp) add: oadd_Limit)
639 apply (rule le_trans)
640 apply (rule_tac [2] le_implies_UN_le_UN)
641 apply (erule_tac [2] bspec)
642 prefer 2 apply assumption
643 apply (simp add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
646 lemma oadd_le_mono1: "k le j ==> k++i le j++i"
648 apply (frule le_Ord2)
649 apply (simp add: oadd_eq_if_raw_oadd, clarify)
650 apply (simp add: raw_oadd_eq_oadd)
651 apply (erule_tac i = i in trans_induct3)
652 apply (simp (no_asm_simp))
653 apply (simp (no_asm_simp) add: oadd_succ succ_le_iff)
654 apply (simp (no_asm_simp) add: oadd_Limit)
655 apply (rule le_implies_UN_le_UN, blast)
658 lemma oadd_lt_mono: "[| i' le i; j'<j |] ==> i'++j' < i++j"
659 by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
661 lemma oadd_le_mono: "[| i' le i; j' le j |] ==> i'++j' le i++j"
662 by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
664 lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
665 by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
667 lemma oadd_lt_self: "[| Ord(i); 0<j |] ==> i < i++j"
668 apply (rule lt_trans2)
669 apply (erule le_refl)
670 apply (simp only: lt_Ord2 oadd_1 [of i, symmetric])
671 apply (blast intro: succ_leI oadd_le_mono)
674 text{*Every ordinal is exceeded by some limit ordinal.*}
675 lemma Ord_imp_greater_Limit: "Ord(i) ==> \<exists>k. i<k & Limit(k)"
676 apply (rule_tac x="i ++ nat" in exI)
677 apply (blast intro: oadd_LimitI oadd_lt_self Limit_nat [THEN Limit_has_0])
680 lemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> \<exists>k. i<k & j<k & Limit(k)"
681 apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])
682 apply (simp add: Un_least_lt_iff)
686 subsection{*Ordinal Subtraction*}
688 text{*The difference is @{term "ordertype(j-i, Memrel(j))"}.
689 It's probably simpler to define the difference recursively!*}
692 "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
693 apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
694 apply (blast intro!: if_type)
695 apply (fast intro!: case_type)
696 apply (erule_tac [2] sumE)
697 apply (simp_all (no_asm_simp))
700 lemma ordertype_sum_Diff:
702 ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =
703 ordertype(j, Memrel(j))"
704 apply (safe dest!: le_subset_iff [THEN iffD1])
705 apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
706 apply (erule_tac [3] well_ord_Memrel, assumption)
707 apply (simp (no_asm_simp))
708 apply (frule_tac j = y in Ord_in_Ord, assumption)
709 apply (frule_tac j = x in Ord_in_Ord, assumption)
710 apply (simp (no_asm_simp) add: Ord_mem_iff_lt lt_Ord not_lt_iff_le)
711 apply (blast intro: lt_trans2 lt_trans)
714 lemma Ord_odiff [simp,TC]:
715 "[| Ord(i); Ord(j) |] ==> Ord(i--j)"
716 apply (unfold odiff_def)
717 apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
721 lemma raw_oadd_ordertype_Diff:
723 ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
724 apply (simp add: raw_oadd_def odiff_def)
725 apply (safe dest!: le_subset_iff [THEN iffD1])
726 apply (rule sum_ord_iso_cong [THEN ordertype_eq])
727 apply (erule id_ord_iso_Memrel)
728 apply (rule ordertype_ord_iso [THEN ord_iso_sym])
729 apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
732 lemma oadd_odiff_inverse: "i le j ==> i ++ (j--i) = j"
733 by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
734 ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
736 (*By oadd_inject, the difference between i and j is unique. Note that we get
737 i++j = k ==> j = k--i. *)
738 lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"
739 apply (rule oadd_inject)
740 apply (blast intro: oadd_odiff_inverse oadd_le_self)
741 apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
744 lemma odiff_lt_mono2: "[| i<j; k le i |] ==> i--k < j--k"
745 apply (rule_tac i = k in oadd_lt_cancel2)
746 apply (simp add: oadd_odiff_inverse)
747 apply (subst oadd_odiff_inverse)
748 apply (blast intro: le_trans leI, assumption)
749 apply (simp (no_asm_simp) add: lt_Ord le_Ord2)
753 subsection{*Ordinal Multiplication*}
755 lemma Ord_omult [simp,TC]:
756 "[| Ord(i); Ord(j) |] ==> Ord(i**j)"
757 apply (unfold omult_def)
758 apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
761 subsubsection{*A useful unfolding law *}
764 "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =
765 pred(A,a,r)*B Un ({a} * pred(B,b,s))"
766 apply (unfold pred_def, blast)
769 lemma ordertype_pred_Pair_eq:
770 "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==>
771 ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =
772 ordertype(pred(A,a,r)*B + pred(B,b,s),
773 radd(A*B, rmult(A,r,B,s), B, s))"
774 apply (simp (no_asm_simp) add: pred_Pair_eq)
775 apply (rule ordertype_eq [symmetric])
776 apply (rule prod_sum_singleton_ord_iso)
777 apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
778 apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]
782 lemma ordertype_pred_Pair_lemma:
784 ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),
785 rmult(i,Memrel(i),j,Memrel(j))) =
786 raw_oadd (j**i', j')"
787 apply (unfold raw_oadd_def omult_def)
788 apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2
791 apply (rule_tac [2] ordertype_ord_iso
792 [THEN sum_ord_iso_cong, THEN ordertype_eq])
793 apply (rule_tac [3] ord_iso_refl)
794 apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
795 apply (elim SigmaE sumE ltE ssubst)
796 apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
797 Ord_ordertype lt_Ord lt_Ord2)
798 apply (blast intro: Ord_trans)+
802 "[| Ord(i); Ord(j); k<j**i |]
803 ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
804 apply (unfold omult_def)
805 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
806 apply (safe elim!: ltE)
807 apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd
808 omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
809 apply (blast intro: ltI)
813 "[| j'<j; i'<i |] ==> j**i' ++ j' < j**i"
814 apply (unfold omult_def)
817 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
818 apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
819 apply (rule bexI [of _ i'])
820 apply (rule bexI [of _ j'])
821 apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
822 apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
823 apply (simp_all add: lt_def)
827 "[| Ord(i); Ord(j) |] ==> j**i = (\<Union>j'\<in>j. \<Union>i'\<in>i. {j**i' ++ j'})"
828 apply (rule subsetI [THEN equalityI])
829 apply (rule lt_omult [THEN exE])
830 apply (erule_tac [3] ltI)
831 apply (simp_all add: Ord_omult)
832 apply (blast elim!: ltE)
833 apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
836 subsubsection{*Basic laws for ordinal multiplication *}
838 text{*Ordinal multiplication by zero *}
840 lemma omult_0 [simp]: "i**0 = 0"
841 apply (unfold omult_def)
842 apply (simp (no_asm_simp))
845 lemma omult_0_left [simp]: "0**i = 0"
846 apply (unfold omult_def)
847 apply (simp (no_asm_simp))
850 text{*Ordinal multiplication by 1 *}
852 lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
853 apply (unfold omult_def)
854 apply (rule_tac s1="Memrel(i)"
855 in ord_isoI [THEN ordertype_eq, THEN trans])
856 apply (rule_tac c = snd and d = "%z.<0,z>" in lam_bijective)
857 apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
860 lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
861 apply (unfold omult_def)
862 apply (rule_tac s1="Memrel(i)"
863 in ord_isoI [THEN ordertype_eq, THEN trans])
864 apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
865 apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
868 text{*Distributive law for ordinal multiplication and addition *}
870 lemma oadd_omult_distrib:
871 "[| Ord(i); Ord(j); Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
872 apply (simp add: oadd_eq_if_raw_oadd)
873 apply (simp add: omult_def raw_oadd_def)
874 apply (rule ordertype_eq [THEN trans])
875 apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]
877 apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
879 apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
880 apply (rule_tac [2] ordertype_eq)
881 apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
882 apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
886 lemma omult_succ: "[| Ord(i); Ord(j) |] ==> i**succ(j) = (i**j)++i"
887 by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
889 text{*Associative law *}
892 "[| Ord(i); Ord(j); Ord(k) |] ==> (i**j)**k = i**(j**k)"
893 apply (unfold omult_def)
894 apply (rule ordertype_eq [THEN trans])
895 apply (rule prod_ord_iso_cong [OF ord_iso_refl
896 ordertype_ord_iso [THEN ord_iso_sym]])
897 apply (blast intro: well_ord_rmult well_ord_Memrel)+
898 apply (rule prod_assoc_ord_iso
899 [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
900 apply (rule_tac [2] ordertype_eq)
901 apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
902 apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+
906 text{*Ordinal multiplication with limit ordinals *}
909 "[| Ord(i); !!x. x:A ==> Ord(j(x)) |]
910 ==> i ** (\<Union>x\<in>A. j(x)) = (\<Union>x\<in>A. i**j(x))"
911 by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
913 lemma omult_Limit: "[| Ord(i); Limit(j) |] ==> i**j = (\<Union>k\<in>j. i**k)"
914 by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]
915 Union_eq_UN [symmetric] Limit_Union_eq)
918 subsubsection{*Ordering/monotonicity properties of ordinal multiplication *}
920 (*As a special case we have "[| 0<i; 0<j |] ==> 0 < i**j" *)
921 lemma lt_omult1: "[| k<i; 0<j |] ==> k < i**j"
922 apply (safe elim!: ltE intro!: ltI Ord_omult)
923 apply (force simp add: omult_unfold)
926 lemma omult_le_self: "[| Ord(i); 0<j |] ==> i le i**j"
927 by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
929 lemma omult_le_mono1: "[| k le j; Ord(i) |] ==> k**i le j**i"
931 apply (frule le_Ord2)
932 apply (erule trans_induct3)
933 apply (simp (no_asm_simp) add: le_refl Ord_0)
934 apply (simp (no_asm_simp) add: omult_succ oadd_le_mono)
935 apply (simp (no_asm_simp) add: omult_Limit)
936 apply (rule le_implies_UN_le_UN, blast)
939 lemma omult_lt_mono2: "[| k<j; 0<i |] ==> i**k < i**j"
941 apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)
942 apply (safe elim!: ltE intro!: Ord_omult)
943 apply (force simp add: Ord_omult)
946 lemma omult_le_mono2: "[| k le j; Ord(i) |] ==> i**k le i**j"
947 apply (rule subset_imp_le)
948 apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
949 apply (simp add: omult_unfold)
950 apply (blast intro: Ord_trans)
953 lemma omult_le_mono: "[| i' le i; j' le j |] ==> i'**j' le i**j"
954 by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
956 lemma omult_lt_mono: "[| i' le i; j'<j; 0<i |] ==> i'**j' < i**j"
957 by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
959 lemma omult_le_self2: "[| Ord(i); 0<j |] ==> i le j**i"
960 apply (frule lt_Ord2)
961 apply (erule_tac i = i in trans_induct3)
962 apply (simp (no_asm_simp))
963 apply (simp (no_asm_simp) add: omult_succ)
964 apply (erule lt_trans1)
965 apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2)
966 apply (blast intro: Ord_omult, assumption)
967 apply (simp (no_asm_simp) add: omult_Limit)
968 apply (rule le_trans)
969 apply (rule_tac [2] le_implies_UN_le_UN)
971 apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
975 text{*Further properties of ordinal multiplication *}
977 lemma omult_inject: "[| i**j = i**k; 0<i; Ord(j); Ord(k) |] ==> j=k"
978 apply (rule Ord_linear_lt)
979 prefer 4 apply assumption
981 apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
984 subsection{*The Relation @{term Lt}*}
986 lemma wf_Lt: "wf(Lt)"
987 apply (rule wf_subset)
988 apply (rule wf_Memrel)
989 apply (auto simp add: Lt_def Memrel_def lt_def)
992 lemma irrefl_Lt: "irrefl(A,Lt)"
993 by (auto simp add: Lt_def irrefl_def)
995 lemma trans_Lt: "trans[A](Lt)"
996 apply (simp add: Lt_def trans_on_def)
997 apply (blast intro: lt_trans)
1000 lemma part_ord_Lt: "part_ord(A,Lt)"
1001 by (simp add: part_ord_def irrefl_Lt trans_Lt)
1003 lemma linear_Lt: "linear(nat,Lt)"
1004 apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)
1005 apply (drule lt_asym, auto)
1008 lemma tot_ord_Lt: "tot_ord(nat,Lt)"
1009 by (simp add: tot_ord_def linear_Lt part_ord_Lt)
1011 lemma well_ord_Lt: "well_ord(nat,Lt)"
1012 by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt)