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