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