src/ZF/OrderType.thy
author wenzelm
Fri Jun 10 12:51:29 2011 +0200 (2011-06-10)
changeset 43348 3e153e719039
parent 32960 69916a850301
child 46820 c656222c4dc1
permissions -rw-r--r--
uniform use of flexflex_rule;
     1 (*  Title:      ZF/OrderType.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1994  University of Cambridge
     4 *)
     5 
     6 header{*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) == lam x: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)) & (ALL u: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 (unfold pred_def lt_def)
    78 apply (simp (no_asm_simp))
    79 apply (blast intro: Ord_trans)
    80 done
    81 
    82 lemma pred_Memrel: 
    83       "x:A ==> pred(A, x, Memrel(A)) = A Int x"
    84 by (unfold pred_def Memrel_def, blast)
    85 
    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)
    89 apply (erule ltE)
    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)
    95 done
    96 
    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)) |]     
   100       ==> i=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)+
   103 done
   104 
   105 
   106 subsection{*Ordermap and ordertype*}
   107 
   108 lemma ordermap_type: 
   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+)
   113 done
   114 
   115 subsubsection{*Unfolding of ordermap *}
   116 
   117 (*Useful for cardinality reasoning; see CardinalArith.ML*)
   118 lemma ordermap_eq_image: 
   119     "[| wf[A](r);  x:A |]
   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)
   125 done
   126 
   127 (*Useful for rewriting PROVIDED pred is not unfolded until later!*)
   128 lemma ordermap_pred_unfold:
   129      "[| wf[A](r);  x:A |]
   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])
   132 
   133 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
   134 lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def] 
   135 
   136 (*The theorem above is 
   137 
   138 [| wf[A](r); x : A |]
   139 ==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
   140 
   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,
   144 like
   145 
   146   ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
   147 
   148 might eliminate the need for r to be transitive.
   149 *)
   150 
   151 
   152 subsubsection{*Showing that ordermap, ordertype yield ordinals *}
   153 
   154 lemma Ord_ordermap: 
   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])+ 
   163 done
   164 
   165 lemma Ord_ordertype: 
   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])
   174 done
   175 
   176 
   177 subsubsection{*ordermap preserves the orderings in both directions *}
   178 
   179 lemma ordermap_mono:
   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)
   183 done
   184 
   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 |]
   188      ==> <w,x>: r"
   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) 
   193 done
   194 
   195 lemmas ordermap_surj = 
   196     ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
   197 
   198 lemma ordermap_bij: 
   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)
   204 done
   205 
   206 subsubsection{*Isomorphisms involving ordertype *}
   207 
   208 lemma ordertype_ord_iso: 
   209  "well_ord(A,r)
   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)
   215 done
   216 
   217 lemma ordertype_eq:
   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)
   223 done
   224 
   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)"
   228 apply (rule exI)
   229 apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
   230 apply (erule ssubst)
   231 apply (erule ordertype_ord_iso [THEN ord_iso_sym])
   232 done
   233 
   234 subsubsection{*Basic equalities for ordertype *}
   235 
   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)
   246 done
   247 
   248 (*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
   249 lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
   250 
   251 lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
   252 apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])
   253 apply (erule emptyE)
   254 apply (rule well_ord_0)
   255 apply (rule Ord_0 [THEN ordertype_Memrel])
   256 done
   257 
   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]
   261 
   262 subsubsection{*A fundamental unfolding law for ordertype. *}
   263 
   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)
   278 done
   279 
   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])
   284 done
   285 
   286 text{*Theorems by Krzysztof Grabczewski; proofs simplified by lcp *}
   287 
   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)
   292 done
   293 
   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])
   302 done
   303 
   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:
   307      "well_ord(A,r)
   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)
   314 done
   315 
   316 
   317 subsection{*Alternative definition of ordinal*}
   318 
   319 (*proof by Krzysztof Grabczewski*)
   320 lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
   321 apply (unfold Ord_alt_def)
   322 apply (rule conjI)
   323 apply (erule well_ord_Memrel)
   324 apply (unfold Ord_def Transset_def pred_def Memrel_def, blast) 
   325 done
   326 
   327 (*proof by lcp*)
   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)
   334 done
   335 
   336 
   337 subsection{*Ordinal Addition*}
   338 
   339 subsubsection{*Order Type calculations for radd *}
   340 
   341 text{*Addition with 0 *}
   342 
   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))
   346 done
   347 
   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
   352 apply force
   353 done
   354 
   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))
   358 done
   359 
   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
   364 apply force
   365 done
   366 
   367 text{*Initial segments of radd.  Statements by Grabczewski *}
   368 
   369 (*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
   370 lemma pred_Inl_bij: 
   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)
   375 apply auto
   376 done
   377 
   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)
   385 done
   386 
   387 lemma pred_Inr_bij: 
   388  "b:B ==>   
   389          id(A+pred(B,b,s))       
   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) 
   393 done
   394 
   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])
   402 done
   403 
   404 
   405 subsubsection{*ordify: trivial coercion to an ordinal *}
   406 
   407 lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
   408 by (simp add: ordify_def)
   409 
   410 (*Collapsing*)
   411 lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"
   412 by (simp add: ordify_def)
   413 
   414 
   415 subsubsection{*Basic laws for ordinal addition *}
   416 
   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
   419               well_ord_Memrel)
   420 
   421 lemma Ord_oadd [iff,TC]: "Ord(i++j)"
   422 by (simp add: oadd_def Ord_raw_oadd)
   423 
   424 
   425 text{*Ordinal addition with zero *}
   426 
   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)
   430 
   431 lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
   432 apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
   433 done
   434 
   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
   437               well_ord_Memrel)
   438 
   439 lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
   440 by (simp add: oadd_def raw_oadd_0_left ordify_def)
   441 
   442 
   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)
   447 
   448 lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
   449 by (simp add: oadd_def ordify_def)
   450 
   451 (*** Further properties of ordinal addition.  Statements by Grabczewski,
   452     proofs by lcp. ***)
   453 
   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)
   459 apply (rule ltI)
   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)
   463 done
   464 
   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) 
   469 done
   470 
   471 text{*Various other results *}
   472 
   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))
   476 apply blast
   477 done
   478 
   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) 
   484 done
   485 
   486 lemma restrict_ord_iso:
   487      "[| f \<in> ord_iso(i, Memrel(i), Order.pred(A,a,r), r);  a \<in> A; j < i; 
   488        trans[A](r) |]
   489       ==> restrict(f,j) \<in> ord_iso(j, Memrel(j), Order.pred(A,f`j,r), r)"
   490 apply (frule ltD) 
   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]) 
   495 done
   496 
   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)
   503 
   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)))"
   508 apply (erule ltE)
   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)
   512 done
   513 
   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)
   520 apply (rule bexI)
   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)
   524 done
   525 
   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)
   528  prefer 2
   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)+
   534 done
   535 
   536 lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
   537 by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
   538 
   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)+
   544 done
   545 
   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)
   549  prefer 2
   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)
   556 done
   557 
   558 
   559 subsubsection{*Ordinal addition with successor -- via associativity! *}
   560 
   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] 
   566                                  ord_iso_refl])
   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)+
   572 done
   573 
   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)
   580 done
   581 
   582 lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
   583 apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
   584 apply blast
   585 done
   586 
   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]
   591                  oadd_assoc)
   592 done
   593 
   594 
   595 text{*Ordinal addition with limit ordinals *}
   596 
   597 lemma oadd_UN:
   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])
   603 
   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)
   608 done
   609 
   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)
   614 done
   615 
   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)
   618 
   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) 
   630 done
   631 
   632 text{*Order/monotonicity properties of ordinal addition *}
   633 
   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)
   644 done
   645 
   646 lemma oadd_le_mono1: "k le j ==> k++i le j++i"
   647 apply (frule lt_Ord)
   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)
   656 done
   657 
   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)
   660 
   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)
   663 
   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)
   666 
   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)
   672 done
   673 
   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])
   678 done
   679 
   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) 
   683 done
   684 
   685 
   686 subsection{*Ordinal Subtraction*}
   687 
   688 text{*The difference is @{term "ordertype(j-i, Memrel(j))"}.
   689     It's probably simpler to define the difference recursively!*}
   690 
   691 lemma bij_sum_Diff:
   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))
   698 done
   699 
   700 lemma ordertype_sum_Diff:
   701      "i le j ==>   
   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)
   712 done
   713 
   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)
   718 done
   719 
   720 
   721 lemma raw_oadd_ordertype_Diff: 
   722    "i le j   
   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)+
   730 done
   731 
   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])
   735 
   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)+
   742 done
   743 
   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)
   750 done
   751 
   752 
   753 subsection{*Ordinal Multiplication*}
   754 
   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)
   759 done
   760 
   761 subsubsection{*A useful unfolding law *}
   762 
   763 lemma pred_Pair_eq: 
   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)
   767 done
   768 
   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] 
   779              elim!: predE)
   780 done
   781 
   782 lemma ordertype_pred_Pair_lemma: 
   783     "[| i'<i;  j'<j |]
   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 
   789                  well_ord_Memrel)
   790 apply (rule trans)
   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)+
   799 done
   800 
   801 lemma lt_omult: 
   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)
   810 done
   811 
   812 lemma omult_oadd_lt: 
   813      "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i"
   814 apply (unfold omult_def)
   815 apply (rule ltI)
   816  prefer 2
   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) 
   824 done
   825 
   826 lemma omult_unfold:
   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)
   834 done
   835 
   836 subsubsection{*Basic laws for ordinal multiplication *}
   837 
   838 text{*Ordinal multiplication by zero *}
   839 
   840 lemma omult_0 [simp]: "i**0 = 0"
   841 apply (unfold omult_def)
   842 apply (simp (no_asm_simp))
   843 done
   844 
   845 lemma omult_0_left [simp]: "0**i = 0"
   846 apply (unfold omult_def)
   847 apply (simp (no_asm_simp))
   848 done
   849 
   850 text{*Ordinal multiplication by 1 *}
   851 
   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)
   858 done
   859 
   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)
   866 done
   867 
   868 text{*Distributive law for ordinal multiplication and addition *}
   869 
   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] 
   876                                   ord_iso_refl])
   877 apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
   878                      Ord_ordertype)
   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 
   883                      Ord_ordertype)
   884 done
   885 
   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)
   888 
   889 text{*Associative law *}
   890 
   891 lemma omult_assoc: 
   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)+
   903 done
   904 
   905 
   906 text{*Ordinal multiplication with limit ordinals *}
   907 
   908 lemma omult_UN: 
   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)
   912 
   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)
   916 
   917 
   918 subsubsection{*Ordering/monotonicity properties of ordinal multiplication *}
   919 
   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)
   924 done
   925 
   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)
   928 
   929 lemma omult_le_mono1: "[| k le j;  Ord(i) |] ==> k**i le j**i"
   930 apply (frule lt_Ord)
   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)
   937 done
   938 
   939 lemma omult_lt_mono2: "[| k<j;  0<i |] ==> i**k < i**j"
   940 apply (rule ltI)
   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)
   944 done
   945 
   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) 
   951 done
   952 
   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)
   955 
   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)
   958 
   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)
   970 prefer 2 apply blast
   971 apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
   972 done
   973 
   974 
   975 text{*Further properties of ordinal multiplication *}
   976 
   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
   980 apply auto 
   981 apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
   982 done
   983 
   984 subsection{*The Relation @{term Lt}*}
   985 
   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) 
   990 done
   991 
   992 lemma irrefl_Lt: "irrefl(A,Lt)"
   993 by (auto simp add: Lt_def irrefl_def)
   994 
   995 lemma trans_Lt: "trans[A](Lt)"
   996 apply (simp add: Lt_def trans_on_def) 
   997 apply (blast intro: lt_trans) 
   998 done
   999 
  1000 lemma part_ord_Lt: "part_ord(A,Lt)"
  1001 by (simp add: part_ord_def irrefl_Lt trans_Lt)
  1002 
  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) 
  1006 done
  1007 
  1008 lemma tot_ord_Lt: "tot_ord(nat,Lt)"
  1009 by (simp add: tot_ord_def linear_Lt part_ord_Lt)
  1010 
  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)
  1013 
  1014 end