diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Sat May 11 20:40:31 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,967 +0,0 @@
-(*  Title:      ZF/OrderType.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
-
-Ordinal arithmetic is traditionally defined in terms of order types, as here.
-But a definition by transfinite recursion would be much simpler!
-*)
-
-
-(*??for Ordinal.ML*)
-(*suitable for rewriting PROVIDED i has been fixed*)
-Goal "[| j:i; Ord(i) |] ==> Ord(j)";
-by (blast_tac (claset() addIs [Ord_in_Ord]) 1);
-qed "Ord_in_Ord'";
-
-
-(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
-
-val [prem] = goal (the_context ()) "j le i ==> well_ord(j, Memrel(i))";
-by (rtac well_ordI 1);
-by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
-by (resolve_tac [prem RS ltE] 1);
-by (asm_simp_tac (simpset() addsimps [linear_def, 
-				      [ltI, prem] MRS lt_trans2 RS ltD]) 1);
-by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
-by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
-qed "le_well_ord_Memrel";
-
-(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
-bind_thm ("well_ord_Memrel", le_refl RS le_well_ord_Memrel);
-
-(*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
-  The smaller ordinal is an initial segment of the larger *)
-Goalw [pred_def, lt_def]
-    "j<i ==> pred(i, j, Memrel(i)) = j";
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [Ord_trans]) 1);
-qed "lt_pred_Memrel";
-
-Goalw [pred_def,Memrel_def] 
-      "x:A ==> pred(A, x, Memrel(A)) = A Int x";
-by (Blast_tac 1);
-qed "pred_Memrel";
-
-Goal "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
-by (ftac lt_pred_Memrel 1);
-by (etac ltE 1);
-by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
-    assume_tac 3 THEN assume_tac 1);
-by (rewtac ord_iso_def);
-(*Combining the two simplifications causes looping*)
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs [bij_is_fun RS apply_type, Ord_trans]) 1);
-qed "Ord_iso_implies_eq_lemma";
-
-(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
-Goal "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j)) |]    \
-\     ==> i=j";
-by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
-by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
-qed "Ord_iso_implies_eq";
-
-
-(**** Ordermap and ordertype ****)
-
-Goalw [ordermap_def,ordertype_def]
-    "ordermap(A,r) : A -> ordertype(A,r)";
-by (rtac lam_type 1);
-by (rtac (lamI RS imageI) 1);
-by (REPEAT (assume_tac 1));
-qed "ordermap_type";
-
-(*** Unfolding of ordermap ***)
-
-(*Useful for cardinality reasoning; see CardinalArith.ML*)
-Goalw [ordermap_def, pred_def]
-    "[| wf[A](r);  x:A |] ==> \
-\         ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
-by (Asm_simp_tac 1);
-by (etac (wfrec_on RS trans) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [subset_iff, image_lam,
-                                  vimage_singleton_iff]) 1);
-qed "ordermap_eq_image";
-
-(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
-Goal "[| wf[A](r);  x:A |] ==> \
-\         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
-by (asm_simp_tac (simpset() addsimps [ordermap_eq_image, pred_subset, 
-                                  ordermap_type RS image_fun]) 1);
-qed "ordermap_pred_unfold";
-
-(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
-bind_thm ("ordermap_unfold", rewrite_rule [pred_def] ordermap_pred_unfold);
-
-(*The theorem above is 
-
-[| wf[A](r); x : A |]
-==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
-
-NOTE: the definition of ordermap used here delivers ordinals only if r is
-transitive.  If r is the predecessor relation on the naturals then
-ordermap(nat,predr) ` n equals {n-1} and not n.  A more complicated definition,
-like
-
-  ordermap(A,r) ` x = Union{succ(ordermap(A,r) ` y) . y: {y: A . <y,x> : r}},
-
-might eliminate the need for r to be transitive.
-*)
-
-
-(*** Showing that ordermap, ordertype yield ordinals ***)
-
-fun ordermap_elim_tac i =
-    EVERY [etac (ordermap_unfold RS equalityD1 RS subsetD RS RepFunE) i,
-           assume_tac (i+1),
-           assume_tac i];
-
-Goalw [well_ord_def, tot_ord_def, part_ord_def]
-    "[| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)";
-by Safe_tac;
-by (wf_on_ind_tac "x" [] 1);
-by (asm_simp_tac (simpset() addsimps [ordermap_pred_unfold]) 1);
-by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (rewrite_goals_tac [pred_def,Transset_def]);
-by (Blast_tac 2);
-by Safe_tac;
-by (ordermap_elim_tac 1);
-by (fast_tac (claset() addSEs [trans_onD]) 1);
-qed "Ord_ordermap";
-
-Goalw [ordertype_def]
-    "well_ord(A,r) ==> Ord(ordertype(A,r))";
-by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
-by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-by (blast_tac (claset() addIs [Ord_ordermap]) 2);
-by (rewrite_goals_tac [Transset_def,well_ord_def]);
-by Safe_tac;
-by (ordermap_elim_tac 1);
-by (Blast_tac 1);
-qed "Ord_ordertype";
-
-(*** ordermap preserves the orderings in both directions ***)
-
-Goal "[| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>    \
-\         ordermap(A,r)`w : ordermap(A,r)`x";
-by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "ordermap_mono";
-
-(*linearity of r is crucial here*)
-Goalw [well_ord_def, tot_ord_def]
-    "[| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r);  \
-\            w: A; x: A |] ==> <w,x>: r";
-by Safe_tac;
-by (linear_case_tac 1);
-by (blast_tac (claset() addSEs [mem_not_refl RS notE]) 1);
-by (dtac ordermap_mono 1);
-by (REPEAT_SOME assume_tac);
-by (etac mem_asym 1);
-by (assume_tac 1);
-qed "converse_ordermap_mono";
-
-bind_thm ("ordermap_surj", 
-          rewrite_rule [symmetric ordertype_def] 
-              (ordermap_type RS surj_image));
-
-Goalw [well_ord_def, tot_ord_def, bij_def, inj_def]
-    "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
-by (force_tac (claset() addSIs [ordermap_type, ordermap_surj]
-		       addEs [linearE]
-		       addDs [ordermap_mono],
-	       simpset() addsimps [mem_not_refl]) 1);
-qed "ordermap_bij";
-
-(*** Isomorphisms involving ordertype ***)
-
-Goalw [ord_iso_def]
- "well_ord(A,r) ==> \
-\      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
-by (safe_tac (claset() addSEs [well_ord_is_wf]
-		      addSIs [ordermap_type RS apply_type,
-			      ordermap_mono, ordermap_bij]));
-by (blast_tac (claset() addSDs [converse_ordermap_mono]) 1);
-qed "ordertype_ord_iso";
-
-Goal "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==> \
-\    ordertype(A,r) = ordertype(B,s)";
-by (ftac well_ord_ord_iso 1 THEN assume_tac 1);
-by (rtac Ord_iso_implies_eq 1
-    THEN REPEAT (etac Ord_ordertype 1));
-by (deepen_tac (claset() addIs  [ord_iso_trans, ord_iso_sym]
-                      addSEs [ordertype_ord_iso]) 0 1);
-qed "ordertype_eq";
-
-Goal "[| ordertype(A,r) = ordertype(B,s); \
-\              well_ord(A,r);  well_ord(B,s) \
-\           |] ==> EX f. f: ord_iso(A,r,B,s)";
-by (rtac exI 1);
-by (resolve_tac [ordertype_ord_iso RS ord_iso_trans] 1);
-by (assume_tac 1);
-by (etac ssubst 1);
-by (eresolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
-qed "ordertype_eq_imp_ord_iso";
-
-(*** Basic equalities for ordertype ***)
-
-(*Ordertype of Memrel*)
-Goal "j le i ==> ordertype(j,Memrel(i)) = j";
-by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
-by (etac ltE 1);
-by (REPEAT (ares_tac [le_well_ord_Memrel, Ord_ordertype] 1));
-by (rtac ord_iso_trans 1);
-by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
-qed "le_ordertype_Memrel";
-
-(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
-bind_thm ("ordertype_Memrel", le_refl RS le_ordertype_Memrel);
-
-Goal "ordertype(0,r) = 0";
-by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq RS trans] 1);
-by (etac emptyE 1);
-by (rtac well_ord_0 1);
-by (resolve_tac [Ord_0 RS ordertype_Memrel] 1);
-qed "ordertype_0";
-
-Addsimps [ordertype_0];
-
-(*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
-                         ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
-bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq);
-
-(*** A fundamental unfolding law for ordertype. ***)
-
-(*Ordermap returns the same result if applied to an initial segment*)
-Goal "[| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>        \
-\         ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
-by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
-by (wf_on_ind_tac "z" [] 1);
-by (safe_tac (claset() addSEs [predE]));
-by (asm_simp_tac
-    (simpset() addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
-(*combining these two simplifications LOOPS! *)
-by (asm_simp_tac (simpset() addsimps [pred_pred_eq]) 1);
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-by (rtac (refl RSN (2,RepFun_cong)) 1);
-by (dtac well_ord_is_trans_on 1);
-by (fast_tac (claset() addSEs [trans_onD]) 1);
-qed "ordermap_pred_eq_ordermap";
-
-Goalw [ordertype_def]
-    "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
-by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
-qed "ordertype_unfold";
-
-(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
-
-Goal "[| well_ord(A,r);  x:A |] ==>             \
-\         ordertype(pred(A,x,r),r) <= ordertype(A,r)";
-by (asm_simp_tac (simpset() addsimps [ordertype_unfold, 
-                  pred_subset RSN (2, well_ord_subset)]) 1);
-by (fast_tac (claset() addIs [ordermap_pred_eq_ordermap]
-                      addEs [predE]) 1);
-qed "ordertype_pred_subset";
-
-Goal "[| well_ord(A,r);  x:A |] ==>  \
-\         ordertype(pred(A,x,r),r) < ordertype(A,r)";
-by (resolve_tac [ordertype_pred_subset RS subset_imp_le RS leE] 1);
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_subset, pred_subset] 1));
-by (eresolve_tac [sym RS ordertype_eq_imp_ord_iso RS exE] 1);
-by (etac well_ord_iso_predE 3);
-by (REPEAT (ares_tac [pred_subset, well_ord_subset] 1));
-qed "ordertype_pred_lt";
-
-(*May rewrite with this -- provided no rules are supplied for proving that
-        well_ord(pred(A,x,r), r) *)
-Goal "well_ord(A,r) ==>  \
-\           ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}";
-by (rtac equalityI 1);
-by (safe_tac (claset() addSIs [ordertype_pred_lt RS ltD]));
-by (auto_tac (claset(), 
-              simpset() addsimps [ordertype_def, 
-                      well_ord_is_wf RS ordermap_eq_image, 
-                      ordermap_type RS image_fun, 
-                      ordermap_pred_eq_ordermap, 
-                      pred_subset])); 
-qed "ordertype_pred_unfold";
-
-
-(**** Alternative definition of ordinal ****)
-
-(*proof by Krzysztof Grabczewski*)
-Goalw [Ord_alt_def] "Ord(i) ==> Ord_alt(i)";
-by (rtac conjI 1);
-by (etac well_ord_Memrel 1);
-by (rewrite_goals_tac [Ord_def, Transset_def, pred_def, Memrel_def]);
-by (Blast.depth_tac (claset()) 8 1);
-qed "Ord_is_Ord_alt";
-
-(*proof by lcp*)
-Goalw [Ord_alt_def, Ord_def, Transset_def, well_ord_def, 
-                     tot_ord_def, part_ord_def, trans_on_def] 
-    "Ord_alt(i) ==> Ord(i)";
-by (asm_full_simp_tac (simpset() addsimps [pred_Memrel]) 1);
-by (blast_tac (claset() addSEs [equalityE]) 1);
-qed "Ord_alt_is_Ord";
-
-
-(**** Ordinal Addition ****)
-
-(*** Order Type calculations for radd ***)
-
-(** Addition with 0 **)
-
-Goal "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)";
-by (res_inst_tac [("d", "Inl")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-qed "bij_sum_0";
-
-Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
-by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
-by (assume_tac 2);
-by (Force_tac 1);
-qed "ordertype_sum_0_eq";
-
-Goal "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
-by (res_inst_tac [("d", "Inr")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-qed "bij_0_sum";
-
-Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
-by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
-by (assume_tac 2);
-by (Force_tac 1);
-qed "ordertype_0_sum_eq";
-
-(** Initial segments of radd.  Statements by Grabczewski **)
-
-(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
-Goalw [pred_def]
- "a:A ==>  \
-\        (lam x:pred(A,a,r). Inl(x))    \
-\        : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by Auto_tac;
-qed "pred_Inl_bij";
-
-Goal "[| a:A;  well_ord(A,r) |] ==>  \
-\        ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) = \
-\        ordertype(pred(A,a,r), r)";
-by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset]));
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-qed "ordertype_pred_Inl_eq";
-
-Goalw [pred_def, id_def]
- "b:B ==>  \
-\        id(A+pred(B,b,s))      \
-\        : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))";
-by (res_inst_tac [("d", "%z. z")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (Asm_full_simp_tac));
-qed "pred_Inr_bij";
-
-Goal "[| b:B;  well_ord(A,r);  well_ord(B,s) |] ==>  \
-\        ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) = \
-\        ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))";
-by (resolve_tac [pred_Inr_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (force_tac (claset(), simpset() addsimps [pred_def, id_def]) 2);
-by (REPEAT_FIRST (ares_tac [well_ord_radd, pred_subset, well_ord_subset]));
-qed "ordertype_pred_Inr_eq";
-
-
-(*** ordify: trivial coercion to an ordinal ***)
-
-Goal "Ord(ordify(x))";
-by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1); 
-qed "Ord_ordify";
-AddIffs [Ord_ordify];
-AddTCs [Ord_ordify];
-
-(*Collapsing*)
-Goal "ordify(ordify(x)) = ordify(x)";
-by (asm_full_simp_tac (simpset() addsimps [ordify_def]) 1);
-qed "ordify_idem";
-Addsimps [ordify_idem];
-
-
-(*** Basic laws for ordinal addition ***)
-
-Goal "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))";
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Ord_ordertype, well_ord_radd, well_ord_Memrel]) 1); 
-qed "Ord_raw_oadd";
-
-Goal "Ord(i++j)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, Ord_raw_oadd]) 1); 
-qed "Ord_oadd";
-AddIffs [Ord_oadd]; AddTCs [Ord_oadd];
-
-
-(** Ordinal addition with zero **)
-
-Goal "Ord(i) ==> raw_oadd(i,0) = i";
-by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_sum_0_eq, 
-                                  ordertype_Memrel, well_ord_Memrel]) 1);
-qed "raw_oadd_0";
-
-Goal "Ord(i) ==> i++0 = i";
-by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0, ordify_def]) 1);
-qed "oadd_0";
-Addsimps [oadd_0];
-
-Goal "Ord(i) ==> raw_oadd(0,i) = i";
-by (asm_simp_tac (simpset() addsimps [raw_oadd_def, ordify_def, Memrel_0, ordertype_0_sum_eq, 
-                                  ordertype_Memrel, well_ord_Memrel]) 1);
-qed "raw_oadd_0_left";
-
-Goal "Ord(i) ==> 0++i = i";
-by (asm_simp_tac (simpset() addsimps [oadd_def, raw_oadd_0_left, ordify_def]) 1);
-qed "oadd_0_left";
-Addsimps [oadd_0_left];
-
-
-Goal "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i) \
-\                       else (if Ord(j) then j else 0))";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, raw_oadd_0]) 1);
-qed "oadd_eq_if_raw_oadd";
-
-
-Goal "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def]) 1);
-qed "raw_oadd_eq_oadd";
-
-(*** Further properties of ordinal addition.  Statements by Grabczewski,
-    proofs by lcp. ***)
-
-(*Surely also provable by transfinite induction on j?*)
-Goal "k<i ==> k < i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord2, raw_oadd_0]) 1);
-by (Clarify_tac 1);  
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); 
-by (rtac ltE 1 THEN assume_tac 1);
-by (rtac ltI 1);
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel] 2));
-by (force_tac 
-    (claset(),
-     simpset() addsimps [ordertype_pred_unfold, 
-                        well_ord_radd, well_ord_Memrel,
-                        ordertype_pred_Inl_eq, 
-                        lt_pred_Memrel, leI RS le_ordertype_Memrel]) 1);
-qed "lt_oadd1";
-
-(*Thus also we obtain the rule  i++j = k ==> i le k *)
-Goal "Ord(i) ==> i le i++j";
-by (rtac all_lt_imp_le 1);
-by (REPEAT (ares_tac [Ord_oadd, lt_oadd1] 1));
-qed "oadd_le_self";
-
-(** A couple of strange but necessary results! **)
-
-Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (Blast_tac 1);
-qed "id_ord_iso_Memrel";
-
-Goal "[| well_ord(A,r);  k<j |] ==>                 \
-\            ordertype(A+k, radd(A, r, k, Memrel(j))) = \
-\            ordertype(A+k, radd(A, r, k, Memrel(k)))";
-by (etac ltE 1);
-by (resolve_tac [ord_iso_refl RS sum_ord_iso_cong RS ordertype_eq] 1);
-by (eresolve_tac [OrdmemD RS id_ord_iso_Memrel RS ord_iso_sym] 1);
-by (REPEAT_FIRST (ares_tac [well_ord_radd, well_ord_Memrel]));
-qed "ordertype_sum_Memrel";
-
-Goal "k<j ==> i++k < i++j";
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, raw_oadd_0_left, lt_Ord, lt_Ord2]) 1);
-by (Clarify_tac 1);  
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); 
-by (rtac ltE 1 THEN assume_tac 1);
-by (resolve_tac [ordertype_pred_unfold RS equalityD2 RS subsetD RS ltI] 1);
-by (REPEAT_FIRST (ares_tac [Ord_ordertype, well_ord_radd, well_ord_Memrel]));
-by (rtac RepFun_eqI 1);
-by (etac InrI 2);
-by (asm_simp_tac 
-    (simpset() addsimps [ordertype_pred_Inr_eq, well_ord_Memrel, 
-                     lt_pred_Memrel, leI RS le_ordertype_Memrel,
-                     ordertype_sum_Memrel]) 1);
-qed "oadd_lt_mono2";
-
-Goal "[| i++j < i++k;  Ord(j) |] ==> j<k";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); 
-by (forw_inst_tac [("i","i"),("j","j")] oadd_le_self 2); 
-by (asm_full_simp_tac (simpset() addsimps [oadd_def, ordify_def, lt_Ord, not_lt_iff_le RS iff_sym]) 2);
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]))); 
-by (ALLGOALS
-    (blast_tac (claset() addDs [oadd_lt_mono2] addEs [lt_irrefl, lt_asym])));
-qed "oadd_lt_cancel2";
-
-Goal "Ord(j) ==> i++j < i++k <-> j<k";
-by (blast_tac (claset() addSIs [oadd_lt_mono2] addSDs [oadd_lt_cancel2]) 1);
-qed "oadd_lt_iff2";
-
-Goal "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); 
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); 
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS
-    (force_tac (claset() addDs [inst "i" "i" oadd_lt_mono2],
-                simpset() addsimps [lt_not_refl])));
-qed "oadd_inject";
-
-Goal "k < i++j ==> k<i | (EX l:j. k = i++l )";
-by (asm_full_simp_tac (simpset() addsimps [inst "i" "j" Ord_in_Ord', oadd_eq_if_raw_oadd] addsplits [split_if_asm]) 1); 
-by (asm_full_simp_tac 
-    (simpset() addsimps [inst "i" "j" Ord_in_Ord', lt_def]) 2);
-by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, well_ord_radd,
-                     well_ord_Memrel, raw_oadd_def]) 1); 
-by (eresolve_tac [ltD RS RepFunE] 1);
-by (force_tac (claset(),
-              simpset() addsimps [ordertype_pred_Inl_eq, well_ord_Memrel, 
-                               ltI, lt_pred_Memrel, le_ordertype_Memrel, leI,
-                               ordertype_pred_Inr_eq, 
-                               ordertype_sum_Memrel]) 1);
-qed "lt_oadd_disj";
-
-
-(*** Ordinal addition with successor -- via associativity! ***)
-
-Goal "(i++j)++k = i++(j++k)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd, Ord_raw_oadd, raw_oadd_0, raw_oadd_0_left]) 1); 
-by (Clarify_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def]) 1); 
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
-          sum_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
-by (resolve_tac [sum_assoc_ord_iso RS ordertype_eq RS trans] 1);
-by (rtac ([ord_iso_refl, ordertype_ord_iso] MRS sum_ord_iso_cong RS 
-          ordertype_eq) 2);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel, Ord_ordertype] 1));
-qed "oadd_assoc";
-
-Goal "[| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})";
-by (rtac (subsetI RS equalityI) 1);
-by (eresolve_tac [ltI RS lt_oadd_disj RS disjE] 1);
-by (REPEAT (ares_tac [Ord_oadd] 1));
-by (force_tac (claset() addIs [lt_oadd1, oadd_lt_mono2],
-              simpset() addsimps [Ord_mem_iff_lt]) 3);
-by (Blast_tac 2);
-by (blast_tac (claset() addSEs [ltE]) 1);
-qed "oadd_unfold";
-
-Goal "Ord(i) ==> i++1 = succ(i)";
-by (asm_simp_tac (simpset() addsimps [oadd_unfold, Ord_1, oadd_0]) 1);
-by (Blast_tac 1);
-qed "oadd_1";
-
-Goal "Ord(j) ==> i++succ(j) = succ(i++j)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); 
-by (Clarify_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); 
-by (asm_simp_tac (simpset() 
-		 addsimps [inst "i" "j" oadd_1 RS sym, inst "i" "i++j" oadd_1 RS sym, oadd_assoc]) 1);
-qed "oadd_succ";
-Addsimps [oadd_succ];
-
-
-(** Ordinal addition with limit ordinals **)
-
-val prems = 
-Goal "[| !!x. x:A ==> Ord(j(x));  a:A |] ==> \
-\     i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
-by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, 
-				       lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]
-                        addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1);
-qed "oadd_UN";
-
-Goal "Limit(j) ==> i++j = (UN k:j. i++k)";
-by (forward_tac [Limit_has_0 RS ltD] 1);
-by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
-				      oadd_UN RS sym, Union_eq_UN RS sym, 
-				      Limit_Union_eq]) 1);
-qed "oadd_Limit";
-
-(** Order/monotonicity properties of ordinal addition **)
-
-Goal "Ord(i) ==> i le j++i";
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (asm_simp_tac (simpset() addsimps [Ord_0_le]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_leI]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
-by (rtac le_trans 1);
-by (rtac le_implies_UN_le_UN 2);
-by (etac bspec 2); 
-by (assume_tac 2); 
-by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-                                     le_refl, Limit_is_Ord]) 1);
-qed "oadd_le_self2";
-
-Goal "k le j ==> k++i le j++i";
-by (ftac lt_Ord 1);
-by (ftac le_Ord2 1);
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1);
-by (Clarify_tac 1); 
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_eq_oadd]) 1); 
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1);
-by (asm_simp_tac (simpset() addsimps [oadd_Limit]) 1);
-by (rtac le_implies_UN_le_UN 1);
-by (Blast_tac 1);
-qed "oadd_le_mono1";
-
-Goal "[| i' le i;  j'<j |] ==> i'++j' < i++j";
-by (rtac lt_trans1 1);
-by (REPEAT (eresolve_tac [asm_rl, oadd_le_mono1, oadd_lt_mono2, ltE,
-                          Ord_succD] 1));
-qed "oadd_lt_mono";
-
-Goal "[| i' le i;  j' le j |] ==> i'++j' le i++j";
-by (asm_simp_tac (simpset() delsimps [oadd_succ]
-		   addsimps [oadd_succ RS sym, le_Ord2, oadd_lt_mono]) 1);
-qed "oadd_le_mono";
-
-Goal "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k";
-by (asm_simp_tac (simpset() delsimps [oadd_succ]
-			    addsimps [oadd_lt_iff2, oadd_succ RS sym, Ord_succ]) 1);
-qed "oadd_le_iff2";
-
-
-(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
-    Probably simpler to define the difference recursively!
-**)
-
-Goal "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))";
-by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by (blast_tac (claset() addSIs [if_type]) 1);
-by (fast_tac (claset() addSIs [case_type]) 1);
-by (etac sumE 2);
-by (ALLGOALS Asm_simp_tac);
-qed "bij_sum_Diff";
-
-Goal "i le j ==>  \
-\           ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =       \
-\           ordertype(j, Memrel(j))";
-by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
-by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
-by (etac well_ord_Memrel 3);
-by (assume_tac 1);
-by (Asm_simp_tac 1);
-by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
-by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
-by (blast_tac (claset() addIs [lt_trans2, lt_trans]) 1);
-qed "ordertype_sum_Diff";
-
-Goalw [odiff_def] 
-    "[| Ord(i);  Ord(j) |] ==> Ord(i--j)";
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_Memrel RS well_ord_subset, 
-                      Diff_subset] 1));
-qed "Ord_odiff";
-Addsimps [Ord_odiff]; AddTCs [Ord_odiff];
-
-
-Goal
-    "i le j  \
-\    ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))";
-by (asm_full_simp_tac (simpset() addsimps [raw_oadd_def, odiff_def]) 1); 
-by (safe_tac (claset() addSDs [le_subset_iff RS iffD1]));
-by (resolve_tac [sum_ord_iso_cong RS ordertype_eq] 1);
-by (etac id_ord_iso_Memrel 1);
-by (resolve_tac [ordertype_ord_iso RS ord_iso_sym] 1);
-by (REPEAT (ares_tac [well_ord_radd, well_ord_Memrel RS well_ord_subset,
-                      Diff_subset] 1));
-qed "raw_oadd_ordertype_Diff";
-
-Goal "i le j ==> i ++ (j--i) = j";
-by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2, oadd_def, ordify_def, raw_oadd_ordertype_Diff, ordertype_sum_Diff, 
-                                  ordertype_Memrel, lt_Ord2 RS Ord_succD]) 1);
-qed "oadd_odiff_inverse";
-
-(*By oadd_inject, the difference between i and j is unique.  Note that we get
-  i++j = k  ==>  j = k--i.  *)
-Goal "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j";
-by (rtac oadd_inject 1);
-by (REPEAT (ares_tac [Ord_ordertype, Ord_oadd, Ord_odiff] 2));
-by (blast_tac (claset() addIs [oadd_odiff_inverse, oadd_le_self]) 1); 
-qed "odiff_oadd_inverse";
-
-Goal "[| i<j;  k le i |] ==> i--k < j--k";
-by (res_inst_tac [("i","k")] oadd_lt_cancel2 1);
-by (asm_full_simp_tac (simpset() addsimps [oadd_odiff_inverse]) 1); 
-by (stac oadd_odiff_inverse 1); 
-by (blast_tac (claset() addIs [le_trans, leI]) 1); 
-by (assume_tac 1); 
-by (asm_simp_tac (simpset() addsimps [lt_Ord, le_Ord2]) 1);
-qed "odiff_lt_mono2";
-
-
-(**** Ordinal Multiplication ****)
-
-Goalw [omult_def] 
-    "[| Ord(i);  Ord(j) |] ==> Ord(i**j)";
-by (REPEAT (ares_tac [Ord_ordertype, well_ord_rmult, well_ord_Memrel] 1));
-qed "Ord_omult";
-Addsimps [Ord_omult]; AddTCs [Ord_omult];
-
-(*** A useful unfolding law ***)
-
-Goalw [pred_def]
- "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =     \
-\                     pred(A,a,r)*B Un ({a} * pred(B,b,s))";
-by (Blast_tac 1);
-qed "pred_Pair_eq";
-
-Goal "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>           \
-\        ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) = \
-\        ordertype(pred(A,a,r)*B + pred(B,b,s),                        \
-\                 radd(A*B, rmult(A,r,B,s), B, s))";
-by (asm_simp_tac (simpset() addsimps [pred_Pair_eq]) 1);
-by (resolve_tac [ordertype_eq RS sym] 1);
-by (rtac prod_sum_singleton_ord_iso 1);
-by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_rmult RS well_ord_subset]));
-by (blast_tac (claset() addSEs [predE]) 1);
-qed "ordertype_pred_Pair_eq";
-
-Goalw [raw_oadd_def, omult_def]
- "[| i'<i;  j'<j |] ==>                                         \
-\        ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))), \
-\                  rmult(i,Memrel(i),j,Memrel(j))) =                   \
-\        raw_oadd (j**i', j')";
-by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_eq, lt_pred_Memrel, 
-				     ltD, lt_Ord2, well_ord_Memrel]) 1);
-by (rtac trans 1);
-by (resolve_tac [ordertype_ord_iso RS sum_ord_iso_cong RS ordertype_eq] 2);
-by (rtac ord_iso_refl 3);
-by (resolve_tac [id_bij RS ord_isoI RS ordertype_eq] 1);
-by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
-by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
-                            Ord_ordertype]));
-by (ALLGOALS Asm_simp_tac);
-by Safe_tac;
-by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
-qed "ordertype_pred_Pair_lemma";
-
-Goalw [omult_def]
- "[| Ord(i);  Ord(j);  k<j**i |] ==>  \
-\        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
-by (asm_full_simp_tac (simpset() addsimps [ordertype_pred_unfold, 
-                                       well_ord_rmult, well_ord_Memrel]) 1);
-by (safe_tac (claset() addSEs [ltE]));
-by (asm_simp_tac (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
-				     symmetric omult_def, 
-           inst "i" "i" Ord_in_Ord', inst "i" "j" Ord_in_Ord', raw_oadd_eq_oadd]) 1);
-by (blast_tac (claset() addIs [ltI]) 1);
-qed "lt_omult";
-
-Goalw [omult_def]
- "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i";
-by (rtac ltI 1);
-by (asm_simp_tac
-    (simpset() addsimps [Ord_ordertype, well_ord_rmult, well_ord_Memrel, 
-                        lt_Ord2]) 2);
-by (asm_simp_tac 
-    (simpset() addsimps [ordertype_pred_unfold, 
-                     well_ord_rmult, well_ord_Memrel, lt_Ord2]) 1);
-by (rtac bexI 1);
-by (blast_tac (claset() addSEs [ltE]) 2);
-by (asm_simp_tac 
-    (simpset() addsimps [ordertype_pred_Pair_lemma, ltI,
-                        symmetric omult_def]) 1);
-by (asm_simp_tac (simpset() addsimps [
-           lt_Ord, lt_Ord2, raw_oadd_eq_oadd]) 1);
-qed "omult_oadd_lt";
-
-Goal "[| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})";
-by (rtac (subsetI RS equalityI) 1);
-by (resolve_tac [lt_omult RS exE] 1);
-by (etac ltI 3);
-by (REPEAT (ares_tac [Ord_omult] 1));
-by (blast_tac (claset() addSEs [ltE]) 1);
-by (blast_tac (claset() addIs [omult_oadd_lt RS ltD, ltI]) 1);
-qed "omult_unfold";
-
-(*** Basic laws for ordinal multiplication ***)
-
-(** Ordinal multiplication by zero **)
-
-Goalw [omult_def] "i**0 = 0";
-by (Asm_simp_tac 1);
-qed "omult_0";
-
-Goalw [omult_def] "0**i = 0";
-by (Asm_simp_tac 1);
-qed "omult_0_left";
-
-Addsimps [omult_0, omult_0_left];
-
-(** Ordinal multiplication by 1 **)
-
-Goalw [omult_def] "Ord(i) ==> i**1 = i";
-by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
-by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
-by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE, 
-                                well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS Asm_simp_tac);
-qed "omult_1";
-
-Goalw [omult_def] "Ord(i) ==> 1**i = i";
-by (resolve_tac [ord_isoI RS ordertype_eq RS trans] 1);
-by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
-by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE, 
-                                well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS Asm_simp_tac);
-qed "omult_1_left";
-
-Addsimps [omult_1, omult_1_left];
-
-(** Distributive law for ordinal multiplication and addition **)
-
-Goal "[| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)";
-by (asm_full_simp_tac (simpset() addsimps [oadd_eq_if_raw_oadd]) 1); 
-by (asm_full_simp_tac (simpset() addsimps [omult_def, raw_oadd_def]) 1); 
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso RS ord_iso_sym, ord_iso_refl] MRS 
-          prod_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
-                      Ord_ordertype] 1));
-by (rtac (sum_prod_distrib_ord_iso RS ordertype_eq RS trans) 1);
-by (rtac ordertype_eq 2);
-by (rtac ([ordertype_ord_iso, ordertype_ord_iso] MRS sum_ord_iso_cong) 2);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel, 
-                      Ord_ordertype] 1));
-qed "oadd_omult_distrib";
-
-Goal "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i";
-by (asm_simp_tac (simpset() 
-		 delsimps [oadd_succ]
-		 addsimps [inst "i" "j" oadd_1 RS sym, oadd_omult_distrib]) 1);
-qed "omult_succ";
-
-(** Associative law **)
-
-Goalw [omult_def]
-    "[| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)";
-by (resolve_tac [ordertype_eq RS trans] 1);
-by (rtac ([ord_iso_refl, ordertype_ord_iso RS ord_iso_sym] MRS 
-          prod_ord_iso_cong) 1);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
-by (resolve_tac [prod_assoc_ord_iso RS ord_iso_sym RS 
-                 ordertype_eq RS trans] 1);
-by (rtac ([ordertype_ord_iso, ord_iso_refl] MRS prod_ord_iso_cong RS
-          ordertype_eq) 2);
-by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel, Ord_ordertype] 1));
-qed "omult_assoc";
-
-
-(** Ordinal multiplication with limit ordinals **)
-
-val prems = 
-Goal "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |] ==> \
-\     i ** (UN x:A. j(x)) = (UN x:A. i**j(x))";
-by (asm_simp_tac (simpset() addsimps prems @ [Ord_UN, omult_unfold]) 1);
-by (Blast_tac 1);
-qed "omult_UN";
-
-Goal "[| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)";
-by (asm_simp_tac 
-    (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, omult_UN RS sym, 
-                     Union_eq_UN RS sym, Limit_Union_eq]) 1);
-qed "omult_Limit";
-
-
-(*** Ordering/monotonicity properties of ordinal multiplication ***)
-
-(*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
-Goal "[| k<i;  0<j |] ==> k < i**j";
-by (safe_tac (claset() addSEs [ltE] addSIs [ltI, Ord_omult]));
-by (asm_simp_tac (simpset() addsimps [omult_unfold]) 1);
-by (REPEAT_FIRST (ares_tac [bexI]));
-by (Asm_simp_tac 1);
-qed "lt_omult1";
-
-Goal "[| Ord(i);  0<j |] ==> i le i**j";
-by (rtac all_lt_imp_le 1);
-by (REPEAT (ares_tac [Ord_omult, lt_omult1, lt_Ord2] 1));
-qed "omult_le_self";
-
-Goal "[| k le j;  Ord(i) |] ==> k**i le j**i";
-by (ftac lt_Ord 1);
-by (ftac le_Ord2 1);
-by (etac trans_induct3 1);
-by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1);
-by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1);
-by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
-by (rtac le_implies_UN_le_UN 1);
-by (Blast_tac 1);
-qed "omult_le_mono1";
-
-Goal "[| k<j;  0<i |] ==> i**k < i**j";
-by (rtac ltI 1);
-by (asm_simp_tac (simpset() addsimps [omult_unfold, lt_Ord2]) 1);
-by (safe_tac (claset() addSEs [ltE] addSIs [Ord_omult]));
-by (REPEAT_FIRST (ares_tac [bexI]));
-by (asm_simp_tac (simpset() addsimps [Ord_omult]) 1);
-qed "omult_lt_mono2";
-
-Goal "[| k le j;  Ord(i) |] ==> i**k le i**j";
-by (rtac subset_imp_le 1);
-by (safe_tac (claset() addSEs [ltE, make_elim Ord_succD] addSIs [Ord_omult]));
-by (asm_full_simp_tac (simpset() addsimps [omult_unfold]) 1);
-by (deepen_tac (claset() addEs [Ord_trans]) 0 1);
-qed "omult_le_mono2";
-
-Goal "[| i' le i;  j' le j |] ==> i'**j' le i**j";
-by (rtac le_trans 1);
-by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_le_mono2, ltE,
-                          Ord_succD] 1));
-qed "omult_le_mono";
-
-Goal "[| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j";
-by (rtac lt_trans1 1);
-by (REPEAT (eresolve_tac [asm_rl, omult_le_mono1, omult_lt_mono2, ltE,
-                          Ord_succD] 1));
-qed "omult_lt_mono";
-
-Goal "[| Ord(i);  0<j |] ==> i le j**i";
-by (ftac lt_Ord2 1);
-by (eres_inst_tac [("i","i")] trans_induct3 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [omult_succ]) 1);
-by (etac lt_trans1 1);
-by (res_inst_tac [("b", "j**x")] (oadd_0 RS subst) 1 THEN 
-    rtac oadd_lt_mono2 2);
-by (REPEAT (ares_tac [Ord_omult] 1));
-by (asm_simp_tac (simpset() addsimps [omult_Limit]) 1);
-by (rtac le_trans 1);
-by (rtac le_implies_UN_le_UN 2);
-by (Blast_tac 2);
-by (asm_simp_tac (simpset() addsimps [Union_eq_UN RS sym, Limit_Union_eq, 
-                                     Limit_is_Ord]) 1);
-qed "omult_le_self2";
-
-
-(** Further properties of ordinal multiplication **)
-
-Goal "[| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k";
-by (rtac Ord_linear_lt 1);
-by (REPEAT_SOME assume_tac);
-by (ALLGOALS
-    (force_tac (claset() addDs [omult_lt_mono2],
-                simpset() addsimps [lt_not_refl])));
-qed "omult_inject";
-