# Theory OrderType

Up to index of Isabelle/ZF

theory OrderType
imports OrderArith Nat_ZF
`(*  Title:      ZF/OrderType.thy    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory    Copyright   1994  University of Cambridge*)header{*Order Types and Ordinal Arithmetic*}theory OrderType imports OrderArith OrdQuant Nat_ZF begintext{*The order type of a well-ordering is the least ordinal isomorphic to it.Ordinal arithmetic is traditionally defined in terms of order types, as it ishere.  But a definition by transfinite recursion would be much simpler!*}definition  ordermap  :: "[i,i]=>i"  where   "ordermap(A,r) == λx∈A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"definition  ordertype :: "[i,i]=>i"  where   "ordertype(A,r) == ordermap(A,r)``A"definition  (*alternative definition of ordinal numbers*)  Ord_alt   :: "i => o"  where   "Ord_alt(X) == well_ord(X, Memrel(X)) & (∀u∈X. u=pred(X, u, Memrel(X)))"definition  (*coercion to ordinal: if not, just 0*)  ordify    :: "i=>i"  where    "ordify(x) == if Ord(x) then x else 0"definition  (*ordinal multiplication*)  omult      :: "[i,i]=>i"           (infixl "**" 70)  where   "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"definition  (*ordinal addition*)  raw_oadd   :: "[i,i]=>i"  where    "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"definition  oadd      :: "[i,i]=>i"           (infixl "++" 65)  where    "i ++ j == raw_oadd(ordify(i),ordify(j))"definition  (*ordinal subtraction*)  odiff      :: "[i,i]=>i"           (infixl "--" 65)  where    "i -- j == ordertype(i-j, Memrel(i))"notation (xsymbols)  omult  (infixl "××" 70)notation (HTML output)  omult  (infixl "××" 70)subsection{*Proofs needing the combination of Ordinal.thy and Order.thy*}lemma le_well_ord_Memrel: "j ≤ i ==> well_ord(j, Memrel(i))"apply (rule well_ordI)apply (rule wf_Memrel [THEN wf_imp_wf_on])apply (simp add: ltD lt_Ord linear_def                 ltI [THEN lt_trans2 [of _ j i]])apply (intro ballI Ord_linear)apply (blast intro: Ord_in_Ord lt_Ord)+done(*"Ord(i) ==> well_ord(i, Memrel(i))"*)lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel](*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord  The smaller ordinal is an initial segment of the larger *)lemma lt_pred_Memrel:    "j<i ==> pred(i, j, Memrel(i)) = j"apply (simp add: pred_def lt_def)apply (blast intro: Ord_trans)donelemma pred_Memrel:      "x ∈ A ==> pred(A, x, Memrel(A)) = A ∩ x"by (unfold pred_def Memrel_def, blast)lemma Ord_iso_implies_eq_lemma:     "[| j<i;  f ∈ ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"apply (frule lt_pred_Memrel)apply (erule ltE)apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto)apply (unfold ord_iso_def)(*Combining the two simplifications causes looping*)apply (simp (no_asm_simp))apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)done(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)lemma Ord_iso_implies_eq:     "[| Ord(i);  Ord(j);  f ∈ ord_iso(i,Memrel(i),j,Memrel(j)) |]      ==> i=j"apply (rule_tac i = i and j = j in Ord_linear_lt)apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+donesubsection{*Ordermap and ordertype*}lemma ordermap_type:    "ordermap(A,r) ∈ A -> ordertype(A,r)"apply (unfold ordermap_def ordertype_def)apply (rule lam_type)apply (rule lamI [THEN imageI], assumption+)donesubsubsection{*Unfolding of ordermap *}(*Useful for cardinality reasoning; see CardinalArith.ML*)lemma ordermap_eq_image:    "[| wf[A](r);  x ∈ A |]     ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"apply (unfold ordermap_def pred_def)apply (simp (no_asm_simp))apply (erule wfrec_on [THEN trans], assumption)apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)done(*Useful for rewriting PROVIDED pred is not unfolded until later!*)lemma ordermap_pred_unfold:     "[| wf[A](r);  x ∈ A |]      ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y ∈ pred(A,x,r)}"by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def](*The theorem above is[| wf[A](r); x ∈ A |]==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y ∈ A . <y,x> ∈ r}}NOTE: the definition of ordermap used here delivers ordinals only if r istransitive.  If r is the predecessor relation on the naturals thenordermap(nat,predr) ` n equals {n-1} and not n.  A more complicated definition,like  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y ∈ A . <y,x> ∈ r}},might eliminate the need for r to be transitive.*)subsubsection{*Showing that ordermap, ordertype yield ordinals *}lemma Ord_ordermap:    "[| well_ord(A,r);  x ∈ A |] ==> Ord(ordermap(A,r) ` x)"apply (unfold well_ord_def tot_ord_def part_ord_def, safe)apply (rule_tac a=x in wf_on_induct, assumption+)apply (simp (no_asm_simp) add: ordermap_pred_unfold)apply (rule OrdI [OF _ Ord_is_Transset])apply (unfold pred_def Transset_def)apply (blast intro: trans_onD             dest!: ordermap_unfold [THEN equalityD1])+donelemma Ord_ordertype:    "well_ord(A,r) ==> Ord(ordertype(A,r))"apply (unfold ordertype_def)apply (subst image_fun [OF ordermap_type subset_refl])apply (rule OrdI [OF _ Ord_is_Transset])prefer 2 apply (blast intro: Ord_ordermap)apply (unfold Transset_def well_ord_def)apply (blast intro: trans_onD             dest!: ordermap_unfold [THEN equalityD1])donesubsubsection{*ordermap preserves the orderings in both directions *}lemma ordermap_mono:     "[| <w,x>: r;  wf[A](r);  w ∈ A; x ∈ A |]      ==> ordermap(A,r)`w ∈ ordermap(A,r)`x"apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption, blast)done(*linearity of r is crucial here*)lemma converse_ordermap_mono:    "[| ordermap(A,r)`w ∈ ordermap(A,r)`x;  well_ord(A,r); w ∈ A; x ∈ A |]     ==> <w,x>: r"apply (unfold well_ord_def tot_ord_def, safe)apply (erule_tac x=w and y=x in linearE, assumption+)apply (blast elim!: mem_not_refl [THEN notE])apply (blast dest: ordermap_mono intro: mem_asym)donelemmas ordermap_surj =    ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]lemma ordermap_bij:    "well_ord(A,r) ==> ordermap(A,r) ∈ bij(A, ordertype(A,r))"apply (unfold well_ord_def tot_ord_def bij_def inj_def)apply (force intro!: ordermap_type ordermap_surj             elim: linearE dest: ordermap_mono             simp add: mem_not_refl)donesubsubsection{*Isomorphisms involving ordertype *}lemma ordertype_ord_iso: "well_ord(A,r)  ==> ordermap(A,r) ∈ ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"apply (unfold ord_iso_def)apply (safe elim!: well_ord_is_wf            intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)apply (blast dest!: converse_ordermap_mono)donelemma ordertype_eq:     "[| f ∈ ord_iso(A,r,B,s);  well_ord(B,s) |]      ==> ordertype(A,r) = ordertype(B,s)"apply (frule well_ord_ord_iso, assumption)apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)donelemma ordertype_eq_imp_ord_iso:     "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r);  well_ord(B,s) |]      ==> ∃f. f ∈ ord_iso(A,r,B,s)"apply (rule exI)apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)apply (erule ssubst)apply (erule ordertype_ord_iso [THEN ord_iso_sym])donesubsubsection{*Basic equalities for ordertype *}(*Ordertype of Memrel*)lemma le_ordertype_Memrel: "j ≤ i ==> ordertype(j,Memrel(i)) = j"apply (rule Ord_iso_implies_eq [symmetric])apply (erule ltE, assumption)apply (blast intro: le_well_ord_Memrel Ord_ordertype)apply (rule ord_iso_trans)apply (erule_tac [2] le_well_ord_Memrel [THEN ordertype_ord_iso])apply (rule id_bij [THEN ord_isoI])apply (simp (no_asm_simp))apply (fast elim: ltE Ord_in_Ord Ord_trans)done(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]lemma ordertype_0 [simp]: "ordertype(0,r) = 0"apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])apply (erule emptyE)apply (rule well_ord_0)apply (rule Ord_0 [THEN ordertype_Memrel])done(*Ordertype of rvimage:  [| f ∈ bij(A,B);  well_ord(B,s) |] ==>                         ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]subsubsection{*A fundamental unfolding law for ordertype. *}(*Ordermap returns the same result if applied to an initial segment*)lemma ordermap_pred_eq_ordermap:     "[| well_ord(A,r);  y ∈ A;  z ∈ pred(A,y,r) |]      ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])apply (rule_tac a=z in wf_on_induct, assumption+)apply (safe elim!: predE)apply (simp (no_asm_simp) add: ordermap_pred_unfold well_ord_is_wf pred_iff)(*combining these two simplifications LOOPS! *)apply (simp (no_asm_simp) add: pred_pred_eq)apply (simp add: pred_def)apply (rule RepFun_cong [OF _ refl])apply (drule well_ord_is_trans_on)apply (fast elim!: trans_onD)donelemma ordertype_unfold:    "ordertype(A,r) = {ordermap(A,r)`y . y ∈ A}"apply (unfold ordertype_def)apply (rule image_fun [OF ordermap_type subset_refl])donetext{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}lemma ordertype_pred_subset: "[| well_ord(A,r);  x ∈ A |] ==>          ordertype(pred(A,x,r),r) ⊆ ordertype(A,r)"apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])apply (fast intro: ordermap_pred_eq_ordermap elim: predE)donelemma ordertype_pred_lt:     "[| well_ord(A,r);  x ∈ A |]      ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])apply (erule_tac [3] well_ord_iso_predE)apply (simp_all add: well_ord_subset [OF _ pred_subset])done(*May rewrite with this -- provided no rules are supplied for proving that        well_ord(pred(A,x,r), r) *)lemma ordertype_pred_unfold:     "well_ord(A,r)      ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x ∈ A}"apply (rule equalityI)apply (safe intro!: ordertype_pred_lt [THEN ltD])apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]                      ordermap_type [THEN image_fun]                      ordermap_pred_eq_ordermap pred_subset)donesubsection{*Alternative definition of ordinal*}(*proof by Krzysztof Grabczewski*)lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"apply (unfold Ord_alt_def)apply (rule conjI)apply (erule well_ord_Memrel)apply (unfold Ord_def Transset_def pred_def Memrel_def, blast)done(*proof by lcp*)lemma Ord_alt_is_Ord:    "Ord_alt(i) ==> Ord(i)"apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def                     tot_ord_def part_ord_def trans_on_def)apply (simp add: pred_Memrel)apply (blast elim!: equalityE)donesubsection{*Ordinal Addition*}subsubsection{*Order Type calculations for radd *}text{*Addition with 0 *}lemma bij_sum_0: "(λz∈A+0. case(%x. x, %y. y, z)) ∈ bij(A+0, A)"apply (rule_tac d = Inl in lam_bijective, safe)apply (simp_all (no_asm_simp))donelemma ordertype_sum_0_eq:     "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])prefer 2 apply assumptionapply forcedonelemma bij_0_sum: "(λz∈0+A. case(%x. x, %y. y, z)) ∈ bij(0+A, A)"apply (rule_tac d = Inr in lam_bijective, safe)apply (simp_all (no_asm_simp))donelemma ordertype_0_sum_eq:     "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])prefer 2 apply assumptionapply forcedonetext{*Initial segments of radd.  Statements by Grabczewski *}(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)lemma pred_Inl_bij: "a ∈ A ==> (λx∈pred(A,a,r). Inl(x))          ∈ bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"apply (unfold pred_def)apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)apply autodonelemma ordertype_pred_Inl_eq:     "[| a ∈ A;  well_ord(A,r) |]      ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =          ordertype(pred(A,a,r), r)"apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])apply (simp_all add: well_ord_subset [OF _ pred_subset])apply (simp add: pred_def)donelemma pred_Inr_bij: "b ∈ B ==>         id(A+pred(B,b,s))         ∈ bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"apply (unfold pred_def id_def)apply (rule_tac d = "%z. z" in lam_bijective, auto)donelemma ordertype_pred_Inr_eq:     "[| b ∈ B;  well_ord(A,r);  well_ord(B,s) |]      ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =          ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])prefer 2 apply (force simp add: pred_def id_def, assumption)apply (blast intro: well_ord_radd well_ord_subset [OF _ pred_subset])donesubsubsection{*ordify: trivial coercion to an ordinal *}lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"by (simp add: ordify_def)(*Collapsing*)lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"by (simp add: ordify_def)subsubsection{*Basic laws for ordinal addition *}lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd              well_ord_Memrel)lemma Ord_oadd [iff,TC]: "Ord(i++j)"by (simp add: oadd_def Ord_raw_oadd)text{*Ordinal addition with zero *}lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq              ordertype_Memrel well_ord_Memrel)lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)donelemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel              well_ord_Memrel)lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"by (simp add: oadd_def raw_oadd_0_left ordify_def)lemma oadd_eq_if_raw_oadd:     "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)              else (if Ord(j) then j else 0))"by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"by (simp add: oadd_def ordify_def)(*** Further properties of ordinal addition.  Statements by Grabczewski,    proofs by lcp. ***)(*Surely also provable by transfinite induction on j?*)lemma lt_oadd1: "k<i ==> k < i++j"apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)apply (simp add: raw_oadd_def)apply (rule ltE, assumption)apply (rule ltI)apply (force simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel          ordertype_pred_Inl_eq lt_pred_Memrel leI [THEN le_ordertype_Memrel])apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)done(*Thus also we obtain the rule  @{term"i++j = k ==> i ≤ k"} *)lemma oadd_le_self: "Ord(i) ==> i ≤ i++j"apply (rule all_lt_imp_le)apply (auto simp add: Ord_oadd lt_oadd1)donetext{*Various other results *}lemma id_ord_iso_Memrel: "A<=B ==> id(A) ∈ ord_iso(A, Memrel(A), A, Memrel(B))"apply (rule id_bij [THEN ord_isoI])apply (simp (no_asm_simp))apply blastdonelemma subset_ord_iso_Memrel:     "[| f ∈ ord_iso(A,Memrel(B),C,r); A<=B |] ==> f ∈ ord_iso(A,Memrel(A),C,r)"apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN fun_is_rel])apply (frule ord_iso_trans [OF id_ord_iso_Memrel], assumption)apply (simp add: right_comp_id)donelemma restrict_ord_iso:     "[| f ∈ ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a ∈ A; j < i;       trans[A](r) |]      ==> restrict(f,j) ∈ ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"apply (frule ltD)apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)apply (frule ord_iso_restrict_pred, assumption)apply (simp add: pred_iff trans_pred_pred_eq lt_pred_Memrel)apply (blast intro!: subset_ord_iso_Memrel le_imp_subset [OF leI])donelemma restrict_ord_iso2:     "[| f ∈ ord_iso(Order.pred(A,a,r), r, i, Memrel(i));  a ∈ A;       j < i; trans[A](r) |]      ==> converse(restrict(converse(f), j))          ∈ ord_iso(Order.pred(A, converse(f)`j, r), r, j, Memrel(j))"by (blast intro: restrict_ord_iso ord_iso_sym ltI)lemma ordertype_sum_Memrel:     "[| well_ord(A,r);  k<j |]      ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =          ordertype(A+k, radd(A, r, k, Memrel(k)))"apply (erule ltE)apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])apply (erule OrdmemD [THEN id_ord_iso_Memrel, THEN ord_iso_sym])apply (simp_all add: well_ord_radd well_ord_Memrel)donelemma oadd_lt_mono2: "k<j ==> i++k < i++j"apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)apply (simp add: raw_oadd_def)apply (rule ltE, assumption)apply (rule ordertype_pred_unfold [THEN equalityD2, THEN subsetD, THEN ltI])apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)apply (rule bexI)apply (erule_tac [2] InrI)apply (simp add: ordertype_pred_Inr_eq well_ord_Memrel lt_pred_Memrel                 leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)donelemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"apply (simp (asm_lr) add: oadd_eq_if_raw_oadd split add: split_if_asm) prefer 2 apply (frule_tac i = i and j = j in oadd_le_self) apply (simp (asm_lr) add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])apply (rule Ord_linear_lt, auto)apply (simp_all add: raw_oadd_eq_oadd)apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+donelemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)apply (simp add: raw_oadd_eq_oadd)apply (rule Ord_linear_lt, auto)apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+donelemma lt_oadd_disj: "k < i++j ==> k<i | (∃l∈j. k = i++l )"apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd            split add: split_if_asm) prefer 2 apply (simp add: Ord_in_Ord' [of _ j] lt_def)apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)apply (erule ltD [THEN RepFunE])apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI                       lt_pred_Memrel le_ordertype_Memrel leI                       ordertype_pred_Inr_eq ordertype_sum_Memrel)donesubsubsection{*Ordinal addition with successor -- via associativity! *}lemma oadd_assoc: "(i++j)++k = i++(j++k)"apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)apply (simp add: raw_oadd_def)apply (rule ordertype_eq [THEN trans])apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]                                 ord_iso_refl])apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])apply (rule_tac [2] ordertype_eq)apply (rule_tac [2] sum_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso])apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+donelemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i ∪ (\<Union>k∈j. {i++k})"apply (rule subsetI [THEN equalityI])apply (erule ltI [THEN lt_oadd_disj, THEN disjE])apply (blast intro: Ord_oadd)apply (blast elim!: ltE, blast)apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)donelemma oadd_1: "Ord(i) ==> i++1 = succ(i)"apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)apply blastdonelemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"apply (simp add: oadd_eq_if_raw_oadd, clarify)apply (simp add: raw_oadd_eq_oadd)apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]                 oadd_assoc)donetext{*Ordinal addition with limit ordinals *}lemma oadd_UN:     "[| !!x. x ∈ A ==> Ord(j(x));  a ∈ A |]      ==> i ++ (\<Union>x∈A. j(x)) = (\<Union>x∈A. i++j(x))"by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD]                 oadd_lt_mono2 [THEN ltD]          elim!: ltE dest!: ltI [THEN lt_oadd_disj])lemma oadd_Limit: "Limit(j) ==> i++j = (\<Union>k∈j. i++k)"apply (frule Limit_has_0 [THEN ltD])apply (simp add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric]                 Union_eq_UN [symmetric] Limit_Union_eq)donelemma oadd_eq_0_iff: "[| Ord(i); Ord(j) |] ==> (i ++ j) = 0 <-> i=0 & j=0"apply (erule trans_induct3 [of j])apply (simp_all add: oadd_Limit)apply (simp add: Union_empty_iff Limit_def lt_def, blast)donelemma oadd_eq_lt_iff: "[| Ord(i); Ord(j) |] ==> 0 < (i ++ j) <-> 0<i | 0<j"by (simp add: Ord_0_lt_iff [symmetric] oadd_eq_0_iff)lemma oadd_LimitI: "[| Ord(i); Limit(j) |] ==> Limit(i ++ j)"apply (simp add: oadd_Limit)apply (frule Limit_has_1 [THEN ltD])apply (rule increasing_LimitI) apply (rule Ord_0_lt)  apply (blast intro: Ord_in_Ord [OF Limit_is_Ord]) apply (force simp add: Union_empty_iff oadd_eq_0_iff                        Limit_is_Ord [of j, THEN Ord_in_Ord], auto)apply (rule_tac x="succ(y)" in bexI) apply (simp add: ltI Limit_is_Ord [of j, THEN Ord_in_Ord])apply (simp add: Limit_def lt_def)donetext{*Order/monotonicity properties of ordinal addition *}lemma oadd_le_self2: "Ord(i) ==> i ≤ j++i"proof (induct i rule: trans_induct3)  case 0 thus ?case by (simp add: Ord_0_le)next  case (succ i) thus ?case by (simp add: oadd_succ succ_leI)next  case (limit l)  hence "l = (\<Union>x∈l. x)"    by (simp add: Union_eq_UN [symmetric] Limit_Union_eq)  also have "... ≤ (\<Union>x∈l. j++x)"    by (rule le_implies_UN_le_UN) (rule limit.hyps)  finally have "l ≤ (\<Union>x∈l. j++x)" .  thus ?case using limit.hyps by (simp add: oadd_Limit)qedlemma oadd_le_mono1: "k ≤ j ==> k++i ≤ j++i"apply (frule lt_Ord)apply (frule le_Ord2)apply (simp add: oadd_eq_if_raw_oadd, clarify)apply (simp add: raw_oadd_eq_oadd)apply (erule_tac i = i in trans_induct3)apply (simp (no_asm_simp))apply (simp (no_asm_simp) add: oadd_succ succ_le_iff)apply (simp (no_asm_simp) add: oadd_Limit)apply (rule le_implies_UN_le_UN, blast)donelemma oadd_lt_mono: "[| i' ≤ i;  j'<j |] ==> i'++j' < i++j"by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)lemma oadd_le_mono: "[| i' ≤ i;  j' ≤ j |] ==> i'++j' ≤ i++j"by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j ≤ i++k <-> j ≤ k"by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)lemma oadd_lt_self: "[| Ord(i);  0<j |] ==> i < i++j"apply (rule lt_trans2)apply (erule le_refl)apply (simp only: lt_Ord2  oadd_1 [of i, symmetric])apply (blast intro: succ_leI oadd_le_mono)donetext{*Every ordinal is exceeded by some limit ordinal.*}lemma Ord_imp_greater_Limit: "Ord(i) ==> ∃k. i<k & Limit(k)"apply (rule_tac x="i ++ nat" in exI)apply (blast intro: oadd_LimitI  oadd_lt_self  Limit_nat [THEN Limit_has_0])donelemma Ord2_imp_greater_Limit: "[|Ord(i); Ord(j)|] ==> ∃k. i<k & j<k & Limit(k)"apply (insert Ord_Un [of i j, THEN Ord_imp_greater_Limit])apply (simp add: Un_least_lt_iff)donesubsection{*Ordinal Subtraction*}text{*The difference is @{term "ordertype(j-i, Memrel(j))"}.    It's probably simpler to define the difference recursively!*}lemma bij_sum_Diff:     "A<=B ==> (λy∈B. if(y ∈ A, Inl(y), Inr(y))) ∈ bij(B, A+(B-A))"apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)apply (blast intro!: if_type)apply (fast intro!: case_type)apply (erule_tac [2] sumE)apply (simp_all (no_asm_simp))donelemma ordertype_sum_Diff:     "i ≤ j ==>            ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =            ordertype(j, Memrel(j))"apply (safe dest!: le_subset_iff [THEN iffD1])apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])apply (erule_tac [3] well_ord_Memrel, assumption)apply (simp (no_asm_simp))apply (frule_tac j = y in Ord_in_Ord, assumption)apply (frule_tac j = x in Ord_in_Ord, assumption)apply (simp (no_asm_simp) add: Ord_mem_iff_lt lt_Ord not_lt_iff_le)apply (blast intro: lt_trans2 lt_trans)donelemma Ord_odiff [simp,TC]:    "[| Ord(i);  Ord(j) |] ==> Ord(i--j)"apply (unfold odiff_def)apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)donelemma raw_oadd_ordertype_Diff:   "i ≤ j    ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"apply (simp add: raw_oadd_def odiff_def)apply (safe dest!: le_subset_iff [THEN iffD1])apply (rule sum_ord_iso_cong [THEN ordertype_eq])apply (erule id_ord_iso_Memrel)apply (rule ordertype_ord_iso [THEN ord_iso_sym])apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+donelemma oadd_odiff_inverse: "i ≤ j ==> i ++ (j--i) = j"by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff              ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])(*By oadd_inject, the difference between i and j is unique.  Note that we get  i++j = k  ==>  j = k--i.  *)lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"apply (rule oadd_inject)apply (blast intro: oadd_odiff_inverse oadd_le_self)apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+donelemma odiff_lt_mono2: "[| i<j;  k ≤ i |] ==> i--k < j--k"apply (rule_tac i = k in oadd_lt_cancel2)apply (simp add: oadd_odiff_inverse)apply (subst oadd_odiff_inverse)apply (blast intro: le_trans leI, assumption)apply (simp (no_asm_simp) add: lt_Ord le_Ord2)donesubsection{*Ordinal Multiplication*}lemma Ord_omult [simp,TC]:    "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"apply (unfold omult_def)apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)donesubsubsection{*A useful unfolding law *}lemma pred_Pair_eq: "[| a ∈ A;  b ∈ B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =                      pred(A,a,r)*B ∪ ({a} * pred(B,b,s))"apply (unfold pred_def, blast)donelemma ordertype_pred_Pair_eq:     "[| a ∈ A;  b ∈ B;  well_ord(A,r);  well_ord(B,s) |] ==>         ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =         ordertype(pred(A,a,r)*B + pred(B,b,s),                  radd(A*B, rmult(A,r,B,s), B, s))"apply (simp (no_asm_simp) add: pred_Pair_eq)apply (rule ordertype_eq [symmetric])apply (rule prod_sum_singleton_ord_iso)apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset]             elim!: predE)donelemma ordertype_pred_Pair_lemma:    "[| i'<i;  j'<j |]     ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),                   rmult(i,Memrel(i),j,Memrel(j))) =         raw_oadd (j**i', j')"apply (unfold raw_oadd_def omult_def)apply (simp add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2                 well_ord_Memrel)apply (rule trans) apply (rule_tac [2] ordertype_ord_iso                      [THEN sum_ord_iso_cong, THEN ordertype_eq])  apply (rule_tac [3] ord_iso_refl)apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])apply (elim SigmaE sumE ltE ssubst)apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel                     Ord_ordertype lt_Ord lt_Ord2)apply (blast intro: Ord_trans)+donelemma lt_omult: "[| Ord(i);  Ord(j);  k<j**i |]  ==> ∃j' i'. k = j**i' ++ j' & j'<j & i'<i"apply (unfold omult_def)apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)apply (safe elim!: ltE)apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd            omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])apply (blast intro: ltI)donelemma omult_oadd_lt:     "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i"apply (unfold omult_def)apply (rule ltI) prefer 2 apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)apply (rule bexI [of _ i'])apply (rule bexI [of _ j'])apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)apply (simp_all add: lt_def)donelemma omult_unfold:     "[| Ord(i);  Ord(j) |] ==> j**i = (\<Union>j'∈j. \<Union>i'∈i. {j**i' ++ j'})"apply (rule subsetI [THEN equalityI])apply (rule lt_omult [THEN exE])apply (erule_tac [3] ltI)apply (simp_all add: Ord_omult)apply (blast elim!: ltE)apply (blast intro: omult_oadd_lt [THEN ltD] ltI)donesubsubsection{*Basic laws for ordinal multiplication *}text{*Ordinal multiplication by zero *}lemma omult_0 [simp]: "i**0 = 0"apply (unfold omult_def)apply (simp (no_asm_simp))donelemma omult_0_left [simp]: "0**i = 0"apply (unfold omult_def)apply (simp (no_asm_simp))donetext{*Ordinal multiplication by 1 *}lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"apply (unfold omult_def)apply (rule_tac s1="Memrel(i)"       in ord_isoI [THEN ordertype_eq, THEN trans])apply (rule_tac c = snd and d = "%z.<0,z>"  in lam_bijective)apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)donelemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"apply (unfold omult_def)apply (rule_tac s1="Memrel(i)"       in ord_isoI [THEN ordertype_eq, THEN trans])apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)donetext{*Distributive law for ordinal multiplication and addition *}lemma oadd_omult_distrib:     "[| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"apply (simp add: oadd_eq_if_raw_oadd)apply (simp add: omult_def raw_oadd_def)apply (rule ordertype_eq [THEN trans])apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym]                                  ord_iso_refl])apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel                     Ord_ordertype)apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])apply (rule_tac [2] ordertype_eq)apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel                     Ord_ordertype)donelemma omult_succ: "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i"by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)text{*Associative law *}lemma omult_assoc:    "[| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)"apply (unfold omult_def)apply (rule ordertype_eq [THEN trans])apply (rule prod_ord_iso_cong [OF ord_iso_refl                                  ordertype_ord_iso [THEN ord_iso_sym]])apply (blast intro: well_ord_rmult well_ord_Memrel)+apply (rule prod_assoc_ord_iso             [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])apply (rule_tac [2] ordertype_eq)apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+donetext{*Ordinal multiplication with limit ordinals *}lemma omult_UN:     "[| Ord(i);  !!x. x ∈ A ==> Ord(j(x)) |]      ==> i ** (\<Union>x∈A. j(x)) = (\<Union>x∈A. i**j(x))"by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (\<Union>k∈j. i**k)"by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric]              Union_eq_UN [symmetric] Limit_Union_eq)subsubsection{*Ordering/monotonicity properties of ordinal multiplication *}(*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)lemma lt_omult1: "[| k<i;  0<j |] ==> k < i**j"apply (safe elim!: ltE intro!: ltI Ord_omult)apply (force simp add: omult_unfold)donelemma omult_le_self: "[| Ord(i);  0<j |] ==> i ≤ i**j"by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)lemma omult_le_mono1:  assumes kj: "k ≤ j" and i: "Ord(i)" shows "k**i ≤ j**i"proof -  have o: "Ord(k)" "Ord(j)" by (rule lt_Ord [OF kj] le_Ord2 [OF kj])+  show ?thesis using i  proof (induct i rule: trans_induct3)    case 0 thus ?case      by simp  next    case (succ i) thus ?case      by (simp add: o kj omult_succ oadd_le_mono)  next    case (limit l)    thus ?case      by (auto simp add: o kj omult_Limit le_implies_UN_le_UN)  qedqedlemma omult_lt_mono2: "[| k<j;  0<i |] ==> i**k < i**j"apply (rule ltI)apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)apply (safe elim!: ltE intro!: Ord_omult)apply (force simp add: Ord_omult)donelemma omult_le_mono2: "[| k ≤ j;  Ord(i) |] ==> i**k ≤ i**j"apply (rule subset_imp_le)apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)apply (simp add: omult_unfold)apply (blast intro: Ord_trans)donelemma omult_le_mono: "[| i' ≤ i;  j' ≤ j |] ==> i'**j' ≤ i**j"by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)lemma omult_lt_mono: "[| i' ≤ i;  j'<j;  0<i |] ==> i'**j' < i**j"by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)lemma omult_le_self2:  assumes i: "Ord(i)" and j: "0<j" shows "i ≤ j**i"proof -  have oj: "Ord(j)" by (rule lt_Ord2 [OF j])  show ?thesis using i  proof (induct i rule: trans_induct3)    case 0 thus ?case      by simp  next    case (succ i)    have "j ×× i ++ 0 < j ×× i ++ j"      by (rule oadd_lt_mono2 [OF j])    with succ.hyps show ?case      by (simp add: oj j omult_succ ) (rule lt_trans1)  next    case (limit l)    hence "l = (\<Union>x∈l. x)"      by (simp add: Union_eq_UN [symmetric] Limit_Union_eq)    also have "... ≤ (\<Union>x∈l. j**x)"      by (rule le_implies_UN_le_UN) (rule limit.hyps)    finally have "l ≤ (\<Union>x∈l. j**x)" .    thus ?case using limit.hyps by (simp add: oj omult_Limit)  qedqedtext{*Further properties of ordinal multiplication *}lemma omult_inject: "[| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k"apply (rule Ord_linear_lt)prefer 4 apply assumptionapply autoapply (force dest: omult_lt_mono2 simp add: lt_not_refl)+donesubsection{*The Relation @{term Lt}*}lemma wf_Lt: "wf(Lt)"apply (rule wf_subset)apply (rule wf_Memrel)apply (auto simp add: Lt_def Memrel_def lt_def)donelemma irrefl_Lt: "irrefl(A,Lt)"by (auto simp add: Lt_def irrefl_def)lemma trans_Lt: "trans[A](Lt)"apply (simp add: Lt_def trans_on_def)apply (blast intro: lt_trans)donelemma part_ord_Lt: "part_ord(A,Lt)"by (simp add: part_ord_def irrefl_Lt trans_Lt)lemma linear_Lt: "linear(nat,Lt)"apply (auto dest!: not_lt_imp_le simp add: Lt_def linear_def le_iff)apply (drule lt_asym, auto)donelemma tot_ord_Lt: "tot_ord(nat,Lt)"by (simp add: tot_ord_def linear_Lt part_ord_Lt)lemma well_ord_Lt: "well_ord(nat,Lt)"by (simp add: well_ord_def wf_Lt wf_imp_wf_on tot_ord_Lt)end`