# HG changeset patch
# User paulson
# Date 1021273333 -7200
# Node ID 6d97dbb189a96366d867f4843ac4997452f0660c
# Parent  94648e0e4506fcbe311e4fb19fabf49f129e904a
converted Order.ML OrderType.ML OrderArith.ML to Isar format

diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/CardinalArith.ML	Mon May 13 09:02:13 2002 +0200
@@ -412,7 +412,7 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2])));
 qed "csquareD";
 
-Goalw [Order.pred_def]
+Goalw [thm "Order.pred_def"]
  "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
 by (safe_tac (claset() delrules [SigmaI, succCI]));  
 by (etac (csquareD RS conjE) 1);
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/IsaMakefile	Mon May 13 09:02:13 2002 +0200
@@ -38,8 +38,8 @@
   Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
   Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
   Main_ZFC.ML Main_ZFC.thy	\
-  Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML OrderArith.thy	\
-  OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy OrdQuant.ML OrdQuant.thy \
+  Nat.ML Nat.thy Order.thy OrderArith.thy	\
+  OrderType.thy Ordinal.ML Ordinal.thy OrdQuant.ML OrdQuant.thy \
   Perm.ML Perm.thy	\
   QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML Rel.ML Rel.thy Sum.ML	\
   Sum.thy Tools/cartprod.ML Tools/datatype_package.ML			\
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Sat May 11 20:40:31 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,638 +0,0 @@
-(*  Title:      ZF/Order.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Orders in Zermelo-Fraenkel Set Theory 
-
-Results from the book "Set Theory: an Introduction to Independence Proofs"
-        by Ken Kunen.  Chapter 1, section 6.
-*)
-
-(** Basic properties of the definitions **)
-
-(*needed?*)
-Goalw [part_ord_def, irrefl_def, trans_on_def, asym_def]
-    "part_ord(A,r) ==> asym(r Int A*A)";
-by (Blast_tac 1);
-qed "part_ord_Imp_asym";
-
-val major::premx::premy::prems = Goalw [linear_def]
-    "[| linear(A,r);  x:A;  y:A;  \
-\       <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |] ==> P";
-by (cut_facts_tac [major,premx,premy] 1);
-by (REPEAT_FIRST (eresolve_tac [ballE,disjE]));
-by (EVERY1 (map etac prems));
-by (ALLGOALS contr_tac);
-qed "linearE";
-
-(*Does the case analysis, deleting linear(A,r) and proving trivial subgoals*)
-val linear_case_tac =
-    SELECT_GOAL (EVERY [etac linearE 1, assume_tac 1, assume_tac 1,
-                        REPEAT_SOME (assume_tac ORELSE' contr_tac)]);
-
-(** General properties of well_ord **)
-
-Goalw [irrefl_def, part_ord_def, tot_ord_def, 
-                 trans_on_def, well_ord_def]
-    "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)";
-by (asm_simp_tac (simpset() addsimps [wf_on_not_refl]) 1);
-by (fast_tac (claset() addEs [linearE, wf_on_asym, wf_on_chain3]) 1);
-qed "well_ordI";
-
-Goalw [well_ord_def]
-    "well_ord(A,r) ==> wf[A](r)";
-by Safe_tac;
-qed "well_ord_is_wf";
-
-Goalw [well_ord_def, tot_ord_def, part_ord_def]
-    "well_ord(A,r) ==> trans[A](r)";
-by Safe_tac;
-qed "well_ord_is_trans_on";
-
-Goalw [well_ord_def, tot_ord_def]
-  "well_ord(A,r) ==> linear(A,r)";
-by (Blast_tac 1);
-qed "well_ord_is_linear";
-
-
-(** Derived rules for pred(A,x,r) **)
-
-Goalw [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
-by (Blast_tac 1);
-qed "pred_iff";
-
-bind_thm ("predI", conjI RS (pred_iff RS iffD2));
-
-val [major,minor] = Goalw [pred_def]
-    "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P";
-by (rtac (major RS CollectE) 1);
-by (REPEAT (ares_tac [minor] 1));
-qed "predE";
-
-Goalw [pred_def] "pred(A,x,r) <= r -`` {x}";
-by (Blast_tac 1);
-qed "pred_subset_under";
-
-Goalw [pred_def] "pred(A,x,r) <= A";
-by (Blast_tac 1);
-qed "pred_subset";
-
-Goalw [pred_def]
-    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
-by (Blast_tac 1);
-qed "pred_pred_eq";
-
-Goalw [trans_on_def, pred_def]
-    "[| trans[A](r);  <y,x>:r;  x:A;  y:A \
-\         |] ==> pred(pred(A,x,r), y, r) = pred(A,y,r)";
-by (Blast_tac 1);
-qed "trans_pred_pred_eq";
-
-
-(** The ordering's properties hold over all subsets of its domain 
-    [including initial segments of the form pred(A,x,r) **)
-
-(*Note: a relation s such that s<=r need not be a partial ordering*)
-Goalw [part_ord_def, irrefl_def, trans_on_def]
-    "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)";
-by (Blast_tac 1);
-qed "part_ord_subset";
-
-Goalw [linear_def]
-    "[| linear(A,r);  B<=A |] ==> linear(B,r)";
-by (Blast_tac 1);
-qed "linear_subset";
-
-Goalw [tot_ord_def]
-    "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)";
-by (fast_tac (claset() addSEs [part_ord_subset, linear_subset]) 1);
-qed "tot_ord_subset";
-
-Goalw [well_ord_def]
-    "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)";
-by (fast_tac (claset() addSEs [tot_ord_subset, wf_on_subset_A]) 1);
-qed "well_ord_subset";
-
-
-(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
-
-Goalw [irrefl_def] "irrefl(A,r Int A*A) <-> irrefl(A,r)";
-by (Blast_tac 1);
-qed "irrefl_Int_iff";
-
-Goalw [trans_on_def] "trans[A](r Int A*A) <-> trans[A](r)";
-by (Blast_tac 1);
-qed "trans_on_Int_iff";
-
-Goalw [part_ord_def] "part_ord(A,r Int A*A) <-> part_ord(A,r)";
-by (simp_tac (simpset() addsimps [irrefl_Int_iff, trans_on_Int_iff]) 1);
-qed "part_ord_Int_iff";
-
-Goalw [linear_def] "linear(A,r Int A*A) <-> linear(A,r)";
-by (Blast_tac 1);
-qed "linear_Int_iff";
-
-Goalw [tot_ord_def] "tot_ord(A,r Int A*A) <-> tot_ord(A,r)";
-by (simp_tac (simpset() addsimps [part_ord_Int_iff, linear_Int_iff]) 1);
-qed "tot_ord_Int_iff";
-
-Goalw [wf_on_def, wf_def] "wf[A](r Int A*A) <-> wf[A](r)";
-by (Fast_tac 1);   (*10 times faster than Blast_tac!*) 
-qed "wf_on_Int_iff";
-
-Goalw [well_ord_def] "well_ord(A,r Int A*A) <-> well_ord(A,r)";
-by (simp_tac (simpset() addsimps [tot_ord_Int_iff, wf_on_Int_iff]) 1);
-qed "well_ord_Int_iff";
-
-
-(** Relations over the Empty Set **)
-
-Goalw [irrefl_def] "irrefl(0,r)";
-by (Blast_tac 1);
-qed "irrefl_0";
-
-Goalw [trans_on_def] "trans[0](r)";
-by (Blast_tac 1);
-qed "trans_on_0";
-
-Goalw [part_ord_def] "part_ord(0,r)";
-by (simp_tac (simpset() addsimps [irrefl_0, trans_on_0]) 1);
-qed "part_ord_0";
-
-Goalw [linear_def] "linear(0,r)";
-by (Blast_tac 1);
-qed "linear_0";
-
-Goalw [tot_ord_def] "tot_ord(0,r)";
-by (simp_tac (simpset() addsimps [part_ord_0, linear_0]) 1);
-qed "tot_ord_0";
-
-Goalw [wf_on_def, wf_def] "wf[0](r)";
-by (Blast_tac 1);
-qed "wf_on_0";
-
-Goalw [well_ord_def] "well_ord(0,r)";
-by (simp_tac (simpset() addsimps [tot_ord_0, wf_on_0]) 1);
-qed "well_ord_0";
-
-
-(** The unit set is well-ordered by the empty relation (Grabczewski) **)
-
-Goalw [irrefl_def, trans_on_def, part_ord_def, linear_def, tot_ord_def]
-        "tot_ord({a},0)";
-by (Simp_tac 1);
-qed "tot_ord_unit";
-
-Goalw [wf_on_def, wf_def] "wf[{a}](0)";
-by (Fast_tac 1);
-qed "wf_on_unit";
-
-Goalw [well_ord_def] "well_ord({a},0)";
-by (simp_tac (simpset() addsimps [tot_ord_unit, wf_on_unit]) 1);
-qed "well_ord_unit";
-
-
-(** Order-preserving (monotone) maps **)
-
-Goalw [mono_map_def] 
-    "f: mono_map(A,r,B,s) ==> f: A->B";
-by (etac CollectD1 1);
-qed "mono_map_is_fun";
-
-Goalw [mono_map_def, inj_def] 
-    "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)";
-by (Clarify_tac 1);
-by (linear_case_tac 1);
-by (REPEAT 
-    (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1,
-            etac ssubst 2,
-            Fast_tac 2,
-            REPEAT (ares_tac [apply_type] 1)]));
-qed "mono_map_is_inj";
-
-
-(** Order-isomorphisms -- or similarities, as Suppes calls them **)
-
-val prems = Goalw [ord_iso_def]
-    "[| f: bij(A, B);   \
-\       !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s \
-\    |] ==> f: ord_iso(A,r,B,s)";
-by (blast_tac (claset() addSIs prems) 1);
-qed "ord_isoI";
-
-Goalw [ord_iso_def, mono_map_def]
-    "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)";
-by (blast_tac (claset() addSDs [bij_is_fun]) 1);
-qed "ord_iso_is_mono_map";
-
-Goalw [ord_iso_def] 
-    "f: ord_iso(A,r,B,s) ==> f: bij(A,B)";
-by (etac CollectD1 1);
-qed "ord_iso_is_bij";
-
-(*Needed?  But ord_iso_converse is!*)
-Goalw [ord_iso_def] 
-    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s";
-by (Blast_tac 1);
-qed "ord_iso_apply";
-
-(*Rewriting with bijections and converse (function inverse)*)
-val bij_inverse_ss = 
-    simpset() setSolver (mk_solver ""
-      (type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj, 
-				        inj_is_fun, comp_fun, comp_bij])))
-          addsimps [right_inverse_bij];
-
-Goalw [ord_iso_def] 
-    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |] \
-\    ==> <converse(f) ` x, converse(f) ` y> : r";
-by (etac CollectE 1);
-by (etac (bspec RS bspec RS iffD2) 1);
-by (REPEAT (eresolve_tac [asm_rl, 
-                          bij_converse_bij RS bij_is_fun RS apply_type] 1));
-by (asm_simp_tac bij_inverse_ss 1);
-qed "ord_iso_converse";
-
-
-(** Symmetry and Transitivity Rules **)
-
-(*Reflexivity of similarity*)
-Goal "id(A): ord_iso(A,r,A,r)";
-by (resolve_tac [id_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-qed "ord_iso_refl";
-
-(*Symmetry of similarity*)
-Goalw [ord_iso_def] "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "ord_iso_sym";
-
-(*Transitivity of similarity*)
-Goalw [mono_map_def] 
-    "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |] ==> \
-\         (f O g): mono_map(A,r,C,t)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "mono_map_trans";
-
-(*Transitivity of similarity: the order-isomorphism relation*)
-Goalw [ord_iso_def] 
-    "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |] ==> \
-\         (f O g): ord_iso(A,r,C,t)";
-by (force_tac (claset(), bij_inverse_ss) 1);
-qed "ord_iso_trans";
-
-(** Two monotone maps can make an order-isomorphism **)
-
-Goalw [ord_iso_def, mono_map_def]
-    "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);     \
-\       f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)";
-by Safe_tac;
-by (REPEAT_FIRST (ares_tac [fg_imp_bijective]));
-by (Blast_tac 1);
-by (subgoal_tac "<g`(f`x), g`(f`y)> : r" 1);
-by (blast_tac (claset() addIs [apply_funtype]) 2);
-by (asm_full_simp_tac (simpset() addsimps [comp_eq_id_iff RS iffD1]) 1);
-qed "mono_ord_isoI";
-
-Goal "[| well_ord(A,r);  well_ord(B,s);                           \
-\        f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |] \
-\     ==> f: ord_iso(A,r,B,s)";
-by (REPEAT (ares_tac [mono_ord_isoI] 1));
-by (forward_tac [mono_map_is_fun RS fun_is_rel] 1);
-by (etac (converse_converse RS subst) 1 THEN rtac left_comp_inverse 1);
-by (DEPTH_SOLVE (ares_tac [mono_map_is_inj, left_comp_inverse] 1
-          ORELSE eresolve_tac [well_ord_is_linear, well_ord_is_wf] 1));
-qed "well_ord_mono_ord_isoI";
-
-
-(** Order-isomorphisms preserve the ordering's properties **)
-
-Goalw [part_ord_def, irrefl_def, trans_on_def, ord_iso_def]
-    "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)";
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addIs [bij_is_fun RS apply_type]) 1);
-qed "part_ord_ord_iso";
-
-Goalw [linear_def, ord_iso_def]
-    "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)";
-by (Asm_simp_tac 1);
-by Safe_tac;
-by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
-by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
-by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
-by (asm_full_simp_tac bij_inverse_ss 1);
-qed "linear_ord_iso";
-
-Goalw [wf_on_def, wf_def, ord_iso_def]
-    "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)";
-(*reversed &-congruence rule handles context of membership in A*)
-by (asm_full_simp_tac (simpset() addcongs [conj_cong2]) 1);
-by Safe_tac;
-by (dres_inst_tac [("x", "{f`z. z:Z Int A}")] spec 1);
-by (safe_tac (claset() addSIs [equalityI]));
-by (ALLGOALS (blast_tac
-	      (claset() addSDs [equalityD1] addIs [bij_is_fun RS apply_type])));
-qed "wf_on_ord_iso";
-
-Goalw [well_ord_def, tot_ord_def]
-    "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)";
-by (fast_tac
-    (claset() addSEs [part_ord_ord_iso, linear_ord_iso, wf_on_ord_iso]) 1);
-qed "well_ord_ord_iso";
-
-
-(*** Main results of Kunen, Chapter 1 section 6 ***)
-
-(*Inductive argument for Kunen's Lemma 6.1, etc. 
-  Simple proof from Halmos, page 72*)
-Goalw [well_ord_def, ord_iso_def]
-  "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |] \
-\       ==> ~ <f`y, y>: r";
-by (REPEAT (eresolve_tac [conjE, CollectE] 1));
-by (wf_on_ind_tac "y" [] 1);
-by (dres_inst_tac [("a","y1")] (bij_is_fun RS apply_type) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "well_ord_iso_subset_lemma";
-
-(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
-                     of a well-ordering*)
-Goal "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P";
-by (metacut_tac well_ord_iso_subset_lemma 1);
-by (REPEAT_FIRST (ares_tac [pred_subset]));
-(*Now we know  f`x < x *)
-by (EVERY1 [dtac (ord_iso_is_bij RS bij_is_fun RS apply_type),
-             assume_tac]);
-(*Now we also know f`x : pred(A,x,r);  contradiction! *)
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, pred_def]) 1);
-qed "well_ord_iso_predE";
-
-(*Simple consequence of Lemma 6.1*)
-Goal "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);  \
-\        a:A;  c:A |] ==> a=c";
-by (ftac well_ord_is_trans_on 1);
-by (ftac well_ord_is_linear 1);
-by (linear_case_tac 1);
-by (dtac ord_iso_sym 1);
-(*two symmetric cases*)
-by (auto_tac (claset() addSEs [pred_subset RSN (2, well_ord_subset) RS
-			       well_ord_iso_predE]
-	               addSIs [predI], 
-	      simpset() addsimps [trans_pred_pred_eq]));
-qed "well_ord_iso_pred_eq";
-
-(*Does not assume r is a wellordering!*)
-Goalw [ord_iso_def, pred_def]
-     "[|f : ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)";
-by (etac CollectE 1);
-by (asm_simp_tac 
-    (simpset() addsimps [[bij_is_fun, Collect_subset] MRS image_fun]) 1);
-by (rtac equalityI 1);
-by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
-by (rtac RepFun_eqI 1);
-by (blast_tac (claset() addSIs [right_inverse_bij RS sym]) 1);
-by (asm_simp_tac bij_inverse_ss 1);
-qed "ord_iso_image_pred";
-
-(*But in use, A and B may themselves be initial segments.  Then use
-  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
-Goal "[| f : ord_iso(A,r,B,s);   a:A |] ==>    \
-\      restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)";
-by (asm_simp_tac (simpset() addsimps [ord_iso_image_pred RS sym]) 1);
-by (rewtac ord_iso_def); 
-by (etac CollectE 1);
-by (rtac CollectI 1);
-by (eresolve_tac [[bij_is_inj, pred_subset] MRS restrict_bij] 1);
-by (ftac bij_is_fun 1);
-by (auto_tac (claset(), simpset() addsimps [pred_def])); 
-qed "ord_iso_restrict_pred";
-
-(*Tricky; a lot of forward proof!*)
-Goal "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;     \
-\         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);  \
-\         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);  \
-\         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s";
-by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
-    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
-by (subgoal_tac "b = g`a" 1);
-by (Asm_simp_tac 1);
-by (rtac well_ord_iso_pred_eq 1);
-by (REPEAT_SOME assume_tac);
-by (ftac ord_iso_restrict_pred 1  THEN
-    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
-by (asm_full_simp_tac
-    (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1);
-by (eresolve_tac [ord_iso_sym RS ord_iso_trans] 1);
-by (assume_tac 1);
-qed "well_ord_iso_preserving";
-
-val  bij_apply_cs = claset() addSIs [bij_converse_bij]
-                            addIs  [ord_iso_is_bij, bij_is_fun, apply_funtype];
-
-(*See Halmos, page 72*)
-Goal "[| well_ord(A,r);  \
-\        f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |] \
-\     ==> ~ <g`y, f`y> : s";
-by (ftac well_ord_iso_subset_lemma 1);
-by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1);
-by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym]));
-by Safe_tac;
-by (ftac ord_iso_converse 1);
-by (EVERY (map (blast_tac bij_apply_cs) [1,1,1]));
-by (asm_full_simp_tac bij_inverse_ss 1);
-qed "well_ord_iso_unique_lemma";
-
-(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
-Goal "[| well_ord(A,r);  \
-\        f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g";
-by (rtac fun_extension 1);
-by (REPEAT (etac (ord_iso_is_bij RS bij_is_fun) 1));
-by (subgoals_tac ["f`x : B", "g`x : B", "linear(B,s)"] 1);
-by (REPEAT (blast_tac bij_apply_cs 3));
-by (dtac well_ord_ord_iso 2 THEN etac ord_iso_sym 2);
-by (asm_full_simp_tac (simpset() addsimps [tot_ord_def, well_ord_def]) 2);
-by (linear_case_tac 1);
-by (DEPTH_SOLVE (eresolve_tac [asm_rl, well_ord_iso_unique_lemma RS notE] 1));
-qed "well_ord_iso_unique";
-
-
-(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
-
-Goalw [ord_iso_map_def] "ord_iso_map(A,r,B,s) <= A*B";
-by (Blast_tac 1);
-qed "ord_iso_map_subset";
-
-Goalw [ord_iso_map_def] "domain(ord_iso_map(A,r,B,s)) <= A";
-by (Blast_tac 1);
-qed "domain_ord_iso_map";
-
-Goalw [ord_iso_map_def] "range(ord_iso_map(A,r,B,s)) <= B";
-by (Blast_tac 1);
-qed "range_ord_iso_map";
-
-Goalw [ord_iso_map_def]
-    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)";
-by (blast_tac (claset() addIs [ord_iso_sym]) 1);
-qed "converse_ord_iso_map";
-
-Goalw [ord_iso_map_def, function_def]
-    "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))";
-by (blast_tac (claset() addIs [well_ord_iso_pred_eq, 
-			      ord_iso_sym, ord_iso_trans]) 1);
-qed "function_ord_iso_map";
-
-Goal "well_ord(B,s) ==> ord_iso_map(A,r,B,s)        \
-\          : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))";
-by (asm_simp_tac 
-    (simpset() addsimps [Pi_iff, function_ord_iso_map,
-                     ord_iso_map_subset RS domain_times_range]) 1);
-qed "ord_iso_map_fun";
-
-Goalw [mono_map_def]
-    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
-\          : mono_map(domain(ord_iso_map(A,r,B,s)), r,  \
-\                     range(ord_iso_map(A,r,B,s)), s)";
-by (asm_simp_tac (simpset() addsimps [ord_iso_map_fun]) 1);
-by Safe_tac;
-by (subgoals_tac ["x:A", "ya:A", "y:B", "yb:B"] 1);
-by (REPEAT 
-    (blast_tac (claset() addSEs [ord_iso_map_subset RS subsetD RS SigmaE]) 2));
-by (asm_simp_tac 
-    (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
-by (rewtac ord_iso_map_def);
-by Safe_tac;
-by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
-qed "ord_iso_map_mono_map";
-
-Goalw [mono_map_def]
-    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)  \
-\          : ord_iso(domain(ord_iso_map(A,r,B,s)), r,   \
-\                     range(ord_iso_map(A,r,B,s)), s)";
-by (rtac well_ord_mono_ord_isoI 1);
-by (resolve_tac [converse_ord_iso_map RS subst] 4);
-by (asm_simp_tac 
-    (simpset() addsimps [ord_iso_map_subset RS converse_converse]) 4);
-by (REPEAT (ares_tac [ord_iso_map_mono_map] 3));
-by (ALLGOALS (etac well_ord_subset));
-by (ALLGOALS (resolve_tac [domain_ord_iso_map, range_ord_iso_map]));
-qed "ord_iso_map_ord_iso";
-
-(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
-Goalw [ord_iso_map_def]
-  "[| well_ord(A,r);  well_ord(B,s);               \
-\          a: A;  a ~: domain(ord_iso_map(A,r,B,s))     \
-\       |] ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)";
-by (safe_tac (claset() addSIs [predI]));
-(*Case analysis on  xaa vs a in r *)
-by (forw_inst_tac [("A","A")] well_ord_is_linear 1);
-by (linear_case_tac 1);
-(*Trivial case: a=xa*)
-by (Blast_tac 2);
-(*Harder case: <a, xa>: r*)
-by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1  THEN
-    REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1));
-by (ftac ord_iso_restrict_pred 1  THEN
-    REPEAT1 (eresolve_tac [asm_rl, predI] 1));
-by (asm_full_simp_tac
-    (simpset() addsplits [split_if_asm]
-	       addsimps [well_ord_is_trans_on, trans_pred_pred_eq,
-                         domain_UN, domain_Union]) 1);
-by (Blast_tac 1);
-qed "domain_ord_iso_map_subset";
-
-(*For the 4-way case analysis in the main result*)
-Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
-\       domain(ord_iso_map(A,r,B,s)) = A |      \
-\       (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))";
-by (ftac well_ord_is_wf 1);
-by (rewrite_goals_tac [wf_on_def, wf_def]);
-by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);
-by Safe_tac;
-(*The first case: the domain equals A*)
-by (rtac (domain_ord_iso_map RS equalityI) 1);
-by (etac (Diff_eq_0_iff RS iffD1) 1);
-(*The other case: the domain equals an initial segment*)
-by (swap_res_tac [bexI] 1);
-by (assume_tac 2);
-by (rtac equalityI 1);
-(*not (claset()) below; that would use rules like domainE!*)
-by (blast_tac (claset() addSEs [predE]) 2);
-by (REPEAT (ares_tac [domain_ord_iso_map_subset] 1));
-qed "domain_ord_iso_map_cases";
-
-(*As above, by duality*)
-Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
-\       range(ord_iso_map(A,r,B,s)) = B |       \
-\       (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))";
-by (resolve_tac [converse_ord_iso_map RS subst] 1);
-by (asm_simp_tac (simpset() addsimps [domain_ord_iso_map_cases]) 1);
-qed "range_ord_iso_map_cases";
-
-(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
-Goal "[| well_ord(A,r);  well_ord(B,s) |] ==>         \
-\       ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |    \
-\       (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) | \
-\       (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))";
-by (forw_inst_tac [("B","B")] domain_ord_iso_map_cases 1);
-by (forw_inst_tac [("B","B")] range_ord_iso_map_cases 2);
-by (REPEAT_FIRST (eresolve_tac [asm_rl, disjE, bexE]));
-by (ALLGOALS (dtac ord_iso_map_ord_iso THEN' assume_tac THEN' 
-              asm_full_simp_tac (simpset() addsimps [bexI])));
-by (resolve_tac [wf_on_not_refl RS notE] 1);
-by (etac well_ord_is_wf 1);
-by (assume_tac 1);
-by (subgoal_tac "<x,y>: ord_iso_map(A,r,B,s)" 1);
-by (dtac rangeI 1);
-by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
-by (rewtac ord_iso_map_def);
-by (Blast_tac 1);
-qed "well_ord_trichotomy";
-
-
-(*** Properties of converse(r), by Krzysztof Grabczewski ***)
-
-Goalw [irrefl_def] "irrefl(A,r) ==> irrefl(A,converse(r))";
-by (Blast_tac 1);
-qed "irrefl_converse";
-
-Goalw [trans_on_def] "trans[A](r) ==> trans[A](converse(r))";
-by (Blast_tac 1);
-qed "trans_on_converse";
-
-Goalw [part_ord_def] "part_ord(A,r) ==> part_ord(A,converse(r))";
-by (blast_tac (claset() addSIs [irrefl_converse, trans_on_converse]) 1);
-qed "part_ord_converse";
-
-Goalw [linear_def] "linear(A,r) ==> linear(A,converse(r))";
-by (Blast_tac 1);
-qed "linear_converse";
-
-Goalw [tot_ord_def] "tot_ord(A,r) ==> tot_ord(A,converse(r))";
-by (blast_tac (claset() addSIs [part_ord_converse, linear_converse]) 1);
-qed "tot_ord_converse";
-
-
-(** By Krzysztof Grabczewski.
-    Lemmas involving the first element of a well ordered set **)
-
-Goalw [first_def] "first(b,B,r) ==> b:B";
-by (Blast_tac 1);
-qed "first_is_elem";
-
-Goalw [well_ord_def, wf_on_def, wf_def,     first_def] 
-        "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))";
-by (REPEAT (eresolve_tac [conjE,allE,disjE] 1));
-by (contr_tac 1);
-by (etac bexE 1);
-by (res_inst_tac [("a","x")] ex1I 1);
-by (Blast_tac 2);
-by (rewrite_goals_tac [tot_ord_def, linear_def]);
-by (Blast.depth_tac (claset()) 7 1);
-qed "well_ord_imp_ex1_first";
-
-Goal "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B";
-by (dtac well_ord_imp_ex1_first 1 THEN REPEAT (assume_tac 1));
-by (rtac first_is_elem 1);
-by (etac theI 1);
-qed "the_first_in";
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/Order.thy
--- a/src/ZF/Order.thy	Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/Order.thy	Mon May 13 09:02:13 2002 +0200
@@ -3,47 +3,717 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Orders in Zermelo-Fraenkel Set Theory 
+Orders in Zermelo-Fraenkel Set Theory
+
+Results from the book "Set Theory: an Introduction to Independence Proofs"
+        by Kenneth Kunen.  Chapter 1, section 6.
 *)
 
-Order = WF + Perm + 
-consts
-  part_ord        :: [i,i]=>o           (*Strict partial ordering*)
-  linear, tot_ord :: [i,i]=>o           (*Strict total ordering*)
-  well_ord        :: [i,i]=>o           (*Well-ordering*)
-  mono_map        :: [i,i,i,i]=>i       (*Order-preserving maps*)
-  ord_iso         :: [i,i,i,i]=>i       (*Order isomorphisms*)
-  pred            :: [i,i,i]=>i		(*Set of predecessors*)
-  ord_iso_map     :: [i,i,i,i]=>i       (*Construction for linearity theorem*)
-
-defs
-  part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
-
-  linear_def   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
-
-  tot_ord_def  "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
-
-  well_ord_def "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
-
-  mono_map_def "mono_map(A,r,B,s) == 
-                   {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
-
-  ord_iso_def  "ord_iso(A,r,B,s) == 
-                   {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
-
-  pred_def     "pred(A,x,r) == {y:A. <y,x>:r}"
-
-  ord_iso_map_def
-     "ord_iso_map(A,r,B,s) == 
-       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
+theory Order = WF + Perm:
 
 constdefs
 
-  first :: [i, i, i] => o
+  part_ord :: "[i,i]=>o"          	(*Strict partial ordering*)
+   "part_ord(A,r) == irrefl(A,r) & trans[A](r)"
+
+  linear   :: "[i,i]=>o"          	(*Strict total ordering*)
+   "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)"
+
+  tot_ord  :: "[i,i]=>o"          	(*Strict total ordering*)
+   "tot_ord(A,r) == part_ord(A,r) & linear(A,r)"
+
+  well_ord :: "[i,i]=>o"          	(*Well-ordering*)
+   "well_ord(A,r) == tot_ord(A,r) & wf[A](r)"
+
+  mono_map :: "[i,i,i,i]=>i"      	(*Order-preserving maps*)
+   "mono_map(A,r,B,s) ==
+	      {f: A->B. ALL x:A. ALL y:A. <x,y>:r --> <f`x,f`y>:s}"
+
+  ord_iso  :: "[i,i,i,i]=>i"		(*Order isomorphisms*)
+   "ord_iso(A,r,B,s) ==
+	      {f: bij(A,B). ALL x:A. ALL y:A. <x,y>:r <-> <f`x,f`y>:s}"
+
+  pred     :: "[i,i,i]=>i"		(*Set of predecessors*)
+   "pred(A,x,r) == {y:A. <y,x>:r}"
+
+  ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)
+   "ord_iso_map(A,r,B,s) ==
+     UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
+
+  first :: "[i, i, i] => o"
     "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
 
+
 syntax (xsymbols)
-    ord_iso :: [i,i,i,i]=>i       ("(\\<langle>_, _\\<rangle> \\<cong>/ \\<langle>_, _\\<rangle>)" 51)
+    ord_iso :: "[i,i,i,i]=>i"      ("(\<langle>_, _\<rangle> \<cong>/ \<langle>_, _\<rangle>)" 51)
+
+
+(** Basic properties of the definitions **)
+
+(*needed?*)
+lemma part_ord_Imp_asym:
+    "part_ord(A,r) ==> asym(r Int A*A)"
+by (unfold part_ord_def irrefl_def trans_on_def asym_def, blast)
+
+lemma linearE:
+    "[| linear(A,r);  x:A;  y:A;
+        <x,y>:r ==> P;  x=y ==> P;  <y,x>:r ==> P |]
+     ==> P"
+by (simp add: linear_def, blast)
+
+
+(** General properties of well_ord **)
+
+lemma well_ordI:
+    "[| wf[A](r); linear(A,r) |] ==> well_ord(A,r)"
+apply (simp add: irrefl_def part_ord_def tot_ord_def
+                 trans_on_def well_ord_def wf_on_not_refl)
+apply (fast elim: linearE wf_on_asym wf_on_chain3)
+done
+
+lemma well_ord_is_wf:
+    "well_ord(A,r) ==> wf[A](r)"
+by (unfold well_ord_def, safe)
+
+lemma well_ord_is_trans_on:
+    "well_ord(A,r) ==> trans[A](r)"
+by (unfold well_ord_def tot_ord_def part_ord_def, safe)
+
+lemma well_ord_is_linear: "well_ord(A,r) ==> linear(A,r)"
+by (unfold well_ord_def tot_ord_def, blast)
+
+
+(** Derived rules for pred(A,x,r) **)
+
+lemma pred_iff: "y : pred(A,x,r) <-> <y,x>:r & y:A"
+by (unfold pred_def, blast)
+
+lemmas predI = conjI [THEN pred_iff [THEN iffD2]]
+
+lemma predE: "[| y: pred(A,x,r);  [| y:A; <y,x>:r |] ==> P |] ==> P"
+by (simp add: pred_def)
+
+lemma pred_subset_under: "pred(A,x,r) <= r -`` {x}"
+by (simp add: pred_def, blast)
+
+lemma pred_subset: "pred(A,x,r) <= A"
+by (simp add: pred_def, blast)
+
+lemma pred_pred_eq:
+    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)"
+by (simp add: pred_def, blast)
+
+lemma trans_pred_pred_eq:
+    "[| trans[A](r);  <y,x>:r;  x:A;  y:A |]
+     ==> pred(pred(A,x,r), y, r) = pred(A,y,r)"
+by (unfold trans_on_def pred_def, blast)
+
+
+(** The ordering's properties hold over all subsets of its domain
+    [including initial segments of the form pred(A,x,r) **)
+
+(*Note: a relation s such that s<=r need not be a partial ordering*)
+lemma part_ord_subset:
+    "[| part_ord(A,r);  B<=A |] ==> part_ord(B,r)"
+by (unfold part_ord_def irrefl_def trans_on_def, blast)
+
+lemma linear_subset:
+    "[| linear(A,r);  B<=A |] ==> linear(B,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_subset:
+    "[| tot_ord(A,r);  B<=A |] ==> tot_ord(B,r)"
+apply (unfold tot_ord_def)
+apply (fast elim!: part_ord_subset linear_subset)
+done
+
+lemma well_ord_subset:
+    "[| well_ord(A,r);  B<=A |] ==> well_ord(B,r)"
+apply (unfold well_ord_def)
+apply (fast elim!: tot_ord_subset wf_on_subset_A)
+done
+
+
+(** Relations restricted to a smaller domain, by Krzysztof Grabczewski **)
+
+lemma irrefl_Int_iff: "irrefl(A,r Int A*A) <-> irrefl(A,r)"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_Int_iff: "trans[A](r Int A*A) <-> trans[A](r)"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_Int_iff: "part_ord(A,r Int A*A) <-> part_ord(A,r)"
+apply (unfold part_ord_def)
+apply (simp add: irrefl_Int_iff trans_on_Int_iff)
+done
+
+lemma linear_Int_iff: "linear(A,r Int A*A) <-> linear(A,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_Int_iff: "tot_ord(A,r Int A*A) <-> tot_ord(A,r)"
+apply (unfold tot_ord_def)
+apply (simp add: part_ord_Int_iff linear_Int_iff)
+done
+
+lemma wf_on_Int_iff: "wf[A](r Int A*A) <-> wf[A](r)"
+apply (unfold wf_on_def wf_def, fast) (*10 times faster than Blast_tac!*)
+done
+
+lemma well_ord_Int_iff: "well_ord(A,r Int A*A) <-> well_ord(A,r)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_Int_iff wf_on_Int_iff)
+done
+
+
+(** Relations over the Empty Set **)
+
+lemma irrefl_0: "irrefl(0,r)"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_0: "trans[0](r)"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_0: "part_ord(0,r)"
+apply (unfold part_ord_def)
+apply (simp add: irrefl_0 trans_on_0)
+done
+
+lemma linear_0: "linear(0,r)"
+by (unfold linear_def, blast)
+
+lemma tot_ord_0: "tot_ord(0,r)"
+apply (unfold tot_ord_def)
+apply (simp add: part_ord_0 linear_0)
+done
+
+lemma wf_on_0: "wf[0](r)"
+by (unfold wf_on_def wf_def, blast)
+
+lemma well_ord_0: "well_ord(0,r)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_0 wf_on_0)
+done
+
+
+(** The unit set is well-ordered by the empty relation (Grabczewski) **)
+
+lemma tot_ord_unit: "tot_ord({a},0)"
+by (simp add: irrefl_def trans_on_def part_ord_def linear_def tot_ord_def)
+
+lemma wf_on_unit: "wf[{a}](0)"
+by (simp add: wf_on_def wf_def, fast)
+
+lemma well_ord_unit: "well_ord({a},0)"
+apply (unfold well_ord_def)
+apply (simp add: tot_ord_unit wf_on_unit)
+done
+
+
+(** Order-preserving (monotone) maps **)
+
+lemma mono_map_is_fun: "f: mono_map(A,r,B,s) ==> f: A->B"
+by (simp add: mono_map_def)
+
+lemma mono_map_is_inj:
+    "[| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)"
+apply (unfold mono_map_def inj_def, clarify)
+apply (erule_tac x=w and y=x in linearE, assumption+)
+apply (force intro: apply_type dest: wf_on_not_refl)+
+done
+
+
+(** Order-isomorphisms -- or similarities, as Suppes calls them **)
+
+lemma ord_isoI:
+    "[| f: bij(A, B);
+        !!x y. [| x:A; y:A |] ==> <x, y> : r <-> <f`x, f`y> : s |]
+     ==> f: ord_iso(A,r,B,s)"
+by (simp add: ord_iso_def)
+
+lemma ord_iso_is_mono_map:
+    "f: ord_iso(A,r,B,s) ==> f: mono_map(A,r,B,s)"
+apply (simp add: ord_iso_def mono_map_def)
+apply (blast dest!: bij_is_fun)
+done
+
+lemma ord_iso_is_bij:
+    "f: ord_iso(A,r,B,s) ==> f: bij(A,B)"
+by (simp add: ord_iso_def)
+
+(*Needed?  But ord_iso_converse is!*)
+lemma ord_iso_apply:
+    "[| f: ord_iso(A,r,B,s);  <x,y>: r;  x:A;  y:A |] ==> <f`x, f`y> : s"
+by (simp add: ord_iso_def, blast)
+
+lemma ord_iso_converse:
+    "[| f: ord_iso(A,r,B,s);  <x,y>: s;  x:B;  y:B |]
+     ==> <converse(f) ` x, converse(f) ` y> : r"
+apply (simp add: ord_iso_def, clarify)
+apply (erule bspec [THEN bspec, THEN iffD2])
+apply (erule asm_rl bij_converse_bij [THEN bij_is_fun, THEN apply_type])+
+apply (auto simp add: right_inverse_bij)
+done
+
+
+(** Symmetry and Transitivity Rules **)
+
+(*Reflexivity of similarity*)
+lemma ord_iso_refl: "id(A): ord_iso(A,r,A,r)"
+by (rule id_bij [THEN ord_isoI], simp)
+
+(*Symmetry of similarity*)
+lemma ord_iso_sym: "f: ord_iso(A,r,B,s) ==> converse(f): ord_iso(B,s,A,r)"
+apply (simp add: ord_iso_def)
+apply (auto simp add: right_inverse_bij bij_converse_bij
+                      bij_is_fun [THEN apply_funtype])
+done
+
+(*Transitivity of similarity*)
+lemma mono_map_trans:
+    "[| g: mono_map(A,r,B,s);  f: mono_map(B,s,C,t) |]
+     ==> (f O g): mono_map(A,r,C,t)"
+apply (unfold mono_map_def)
+apply (auto simp add: comp_fun)
+done
+
+(*Transitivity of similarity: the order-isomorphism relation*)
+lemma ord_iso_trans:
+    "[| g: ord_iso(A,r,B,s);  f: ord_iso(B,s,C,t) |]
+     ==> (f O g): ord_iso(A,r,C,t)"
+apply (unfold ord_iso_def, clarify)
+apply (frule bij_is_fun [of f])
+apply (frule bij_is_fun [of g])
+apply (auto simp add: comp_bij)
+done
+
+(** Two monotone maps can make an order-isomorphism **)
+
+lemma mono_ord_isoI:
+    "[| f: mono_map(A,r,B,s);  g: mono_map(B,s,A,r);
+        f O g = id(B);  g O f = id(A) |] ==> f: ord_iso(A,r,B,s)"
+apply (simp add: ord_iso_def mono_map_def, safe)
+apply (intro fg_imp_bijective, auto)
+apply (subgoal_tac "<g` (f`x), g` (f`y) > : r")
+apply (simp add: comp_eq_id_iff [THEN iffD1])
+apply (blast intro: apply_funtype)
+done
+
+lemma well_ord_mono_ord_isoI:
+     "[| well_ord(A,r);  well_ord(B,s);
+         f: mono_map(A,r,B,s);  converse(f): mono_map(B,s,A,r) |]
+      ==> f: ord_iso(A,r,B,s)"
+apply (intro mono_ord_isoI, auto)
+apply (frule mono_map_is_fun [THEN fun_is_rel])
+apply (erule converse_converse [THEN subst], rule left_comp_inverse)
+apply (blast intro: left_comp_inverse mono_map_is_inj well_ord_is_linear
+                    well_ord_is_wf)+
+done
+
+
+(** Order-isomorphisms preserve the ordering's properties **)
+
+lemma part_ord_ord_iso:
+    "[| part_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> part_ord(A,r)"
+apply (simp add: part_ord_def irrefl_def trans_on_def ord_iso_def)
+apply (fast intro: bij_is_fun [THEN apply_type])
+done
+
+lemma linear_ord_iso:
+    "[| linear(B,s);  f: ord_iso(A,r,B,s) |] ==> linear(A,r)"
+apply (simp add: linear_def ord_iso_def, safe)
+apply (drule_tac x1 = "f`x" and x = "f`xa" in bspec [THEN bspec])
+apply (safe elim!: bij_is_fun [THEN apply_type])
+apply (drule_tac t = "op ` (converse (f))" in subst_context)
+apply (simp add: left_inverse_bij)
+done
+
+lemma wf_on_ord_iso:
+    "[| wf[B](s);  f: ord_iso(A,r,B,s) |] ==> wf[A](r)"
+apply (simp add: wf_on_def wf_def ord_iso_def, safe)
+apply (drule_tac x = "{f`z. z:Z Int A}" in spec)
+apply (safe intro!: equalityI)
+apply (blast dest!: equalityD1 intro: bij_is_fun [THEN apply_type])+
+done
+
+lemma well_ord_ord_iso:
+    "[| well_ord(B,s);  f: ord_iso(A,r,B,s) |] ==> well_ord(A,r)"
+apply (unfold well_ord_def tot_ord_def)
+apply (fast elim!: part_ord_ord_iso linear_ord_iso wf_on_ord_iso)
+done
 
 
+(*** Main results of Kunen, Chapter 1 section 6 ***)
+
+(*Inductive argument for Kunen's Lemma 6.1, etc.
+  Simple proof from Halmos, page 72*)
+lemma well_ord_iso_subset_lemma:
+     "[| well_ord(A,r);  f: ord_iso(A,r, A',r);  A'<= A;  y: A |]
+      ==> ~ <f`y, y>: r"
+apply (simp add: well_ord_def ord_iso_def)
+apply (elim conjE CollectE)
+apply (rule_tac a=y in wf_on_induct, assumption+)
+apply (blast dest: bij_is_fun [THEN apply_type])
+done
+
+(*Kunen's Lemma 6.1: there's no order-isomorphism to an initial segment
+                     of a well-ordering*)
+lemma well_ord_iso_predE:
+     "[| well_ord(A,r);  f : ord_iso(A, r, pred(A,x,r), r);  x:A |] ==> P"
+apply (insert well_ord_iso_subset_lemma [of A r f "pred(A,x,r)" x])
+apply (simp add: pred_subset)
+(*Now we know  f`x < x *)
+apply (drule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], assumption)
+(*Now we also know f`x : pred(A,x,r);  contradiction! *)
+apply (simp add: well_ord_def pred_def)
+done
+
+(*Simple consequence of Lemma 6.1*)
+lemma well_ord_iso_pred_eq:
+     "[| well_ord(A,r);  f : ord_iso(pred(A,a,r), r, pred(A,c,r), r);
+         a:A;  c:A |] ==> a=c"
+apply (frule well_ord_is_trans_on)
+apply (frule well_ord_is_linear)
+apply (erule_tac x=a and y=c in linearE, assumption+)
+apply (drule ord_iso_sym)
+(*two symmetric cases*)
+apply (auto elim!: well_ord_subset [OF _ pred_subset, THEN well_ord_iso_predE]
+            intro!: predI
+            simp add: trans_pred_pred_eq)
+done
+
+(*Does not assume r is a wellordering!*)
+lemma ord_iso_image_pred:
+     "[|f : ord_iso(A,r,B,s);  a:A|] ==> f `` pred(A,a,r) = pred(B, f`a, s)"
+apply (unfold ord_iso_def pred_def)
+apply (erule CollectE)
+apply (simp (no_asm_simp) add: image_fun [OF bij_is_fun Collect_subset])
+apply (rule equalityI)
+apply (safe elim!: bij_is_fun [THEN apply_type])
+apply (rule RepFun_eqI)
+apply (blast intro!: right_inverse_bij [symmetric])
+apply (auto simp add: right_inverse_bij  bij_is_fun [THEN apply_funtype])
+done
+
+(*But in use, A and B may themselves be initial segments.  Then use
+  trans_pred_pred_eq to simplify the pred(pred...) terms.  See just below.*)
+lemma ord_iso_restrict_pred: "[| f : ord_iso(A,r,B,s);   a:A |] ==>
+       restrict(f, pred(A,a,r)) : ord_iso(pred(A,a,r), r, pred(B, f`a, s), s)"
+apply (simp add: ord_iso_image_pred [symmetric])
+apply (simp add: ord_iso_def, clarify)
+apply (rule conjI)
+apply (erule restrict_bij [OF bij_is_inj pred_subset])
+apply (frule bij_is_fun)
+apply (auto simp add: pred_def)
+done
+
+(*Tricky; a lot of forward proof!*)
+lemma well_ord_iso_preserving:
+     "[| well_ord(A,r);  well_ord(B,s);  <a,c>: r;
+         f : ord_iso(pred(A,a,r), r, pred(B,b,s), s);
+         g : ord_iso(pred(A,c,r), r, pred(B,d,s), s);
+         a:A;  c:A;  b:B;  d:B |] ==> <b,d>: s"
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type], (erule asm_rl predI predE)+)
+apply (subgoal_tac "b = g`a")
+apply (simp (no_asm_simp))
+apply (rule well_ord_iso_pred_eq, auto)
+apply (frule ord_iso_restrict_pred, (erule asm_rl predI)+)
+apply (simp add: well_ord_is_trans_on trans_pred_pred_eq)
+apply (erule ord_iso_sym [THEN ord_iso_trans], assumption)
+done
+
+(*See Halmos, page 72*)
+lemma well_ord_iso_unique_lemma:
+     "[| well_ord(A,r);
+         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s);  y: A |]
+      ==> ~ <g`y, f`y> : s"
+apply (frule well_ord_iso_subset_lemma)
+apply (rule_tac f = "converse (f) " and g = g in ord_iso_trans)
+apply auto
+apply (blast intro: ord_iso_sym)
+apply (frule ord_iso_is_bij [of f])
+apply (frule ord_iso_is_bij [of g])
+apply (frule ord_iso_converse)
+apply (blast intro!: bij_converse_bij
+             intro: bij_is_fun apply_funtype)+
+apply (erule notE)
+apply (simp add: left_inverse_bij bij_converse_bij bij_is_fun
+                 comp_fun_apply [of _ A B _ A])
+done
+
+
+(*Kunen's Lemma 6.2: Order-isomorphisms between well-orderings are unique*)
+lemma well_ord_iso_unique: "[| well_ord(A,r);
+         f: ord_iso(A,r, B,s);  g: ord_iso(A,r, B,s) |] ==> f = g"
+apply (rule fun_extension)
+apply (erule ord_iso_is_bij [THEN bij_is_fun])+
+apply (subgoal_tac "f`x : B & g`x : B & linear(B,s)")
+ apply (simp add: linear_def)
+ apply (blast dest: well_ord_iso_unique_lemma)
+apply (blast intro: ord_iso_is_bij bij_is_fun apply_funtype
+                    well_ord_is_linear well_ord_ord_iso ord_iso_sym)
+done
+
+(** Towards Kunen's Theorem 6.3: linearity of the similarity relation **)
+
+lemma ord_iso_map_subset: "ord_iso_map(A,r,B,s) <= A*B"
+by (unfold ord_iso_map_def, blast)
+
+lemma domain_ord_iso_map: "domain(ord_iso_map(A,r,B,s)) <= A"
+by (unfold ord_iso_map_def, blast)
+
+lemma range_ord_iso_map: "range(ord_iso_map(A,r,B,s)) <= B"
+by (unfold ord_iso_map_def, blast)
+
+lemma converse_ord_iso_map:
+    "converse(ord_iso_map(A,r,B,s)) = ord_iso_map(B,s,A,r)"
+apply (unfold ord_iso_map_def)
+apply (blast intro: ord_iso_sym)
+done
+
+lemma function_ord_iso_map:
+    "well_ord(B,s) ==> function(ord_iso_map(A,r,B,s))"
+apply (unfold ord_iso_map_def function_def)
+apply (blast intro: well_ord_iso_pred_eq ord_iso_sym ord_iso_trans)
+done
+
+lemma ord_iso_map_fun: "well_ord(B,s) ==> ord_iso_map(A,r,B,s)
+           : domain(ord_iso_map(A,r,B,s)) -> range(ord_iso_map(A,r,B,s))"
+by (simp add: Pi_iff function_ord_iso_map
+                 ord_iso_map_subset [THEN domain_times_range])
+
+lemma ord_iso_map_mono_map:
+    "[| well_ord(A,r);  well_ord(B,s) |]
+     ==> ord_iso_map(A,r,B,s)
+           : mono_map(domain(ord_iso_map(A,r,B,s)), r,
+                      range(ord_iso_map(A,r,B,s)), s)"
+apply (unfold mono_map_def)
+apply (simp (no_asm_simp) add: ord_iso_map_fun)
+apply safe
+apply (subgoal_tac "x:A & ya:A & y:B & yb:B")
+ apply (simp add: apply_equality [OF _  ord_iso_map_fun])
+ apply (unfold ord_iso_map_def)
+ apply (blast intro: well_ord_iso_preserving, blast)
+done
+
+lemma ord_iso_map_ord_iso:
+    "[| well_ord(A,r);  well_ord(B,s) |] ==> ord_iso_map(A,r,B,s)
+           : ord_iso(domain(ord_iso_map(A,r,B,s)), r,
+                      range(ord_iso_map(A,r,B,s)), s)"
+apply (rule well_ord_mono_ord_isoI)
+   prefer 4
+   apply (rule converse_ord_iso_map [THEN subst])
+   apply (simp add: ord_iso_map_mono_map
+		    ord_iso_map_subset [THEN converse_converse])
+apply (blast intro!: domain_ord_iso_map range_ord_iso_map
+             intro: well_ord_subset ord_iso_map_mono_map)+
+done
+
+
+(*One way of saying that domain(ord_iso_map(A,r,B,s)) is downwards-closed*)
+lemma domain_ord_iso_map_subset:
+     "[| well_ord(A,r);  well_ord(B,s);
+         a: A;  a ~: domain(ord_iso_map(A,r,B,s)) |]
+      ==>  domain(ord_iso_map(A,r,B,s)) <= pred(A, a, r)"
+apply (unfold ord_iso_map_def)
+apply (safe intro!: predI)
+(*Case analysis on  xa vs a in r *)
+apply (simp (no_asm_simp))
+apply (frule_tac A = A in well_ord_is_linear)
+apply (rename_tac b y f)
+apply (erule_tac x=b and y=a in linearE, assumption+)
+(*Trivial case: b=a*)
+apply clarify
+apply blast
+(*Harder case: <a, xa>: r*)
+apply (frule ord_iso_is_bij [THEN bij_is_fun, THEN apply_type],
+       (erule asm_rl predI predE)+)
+apply (frule ord_iso_restrict_pred)
+ apply (simp add: pred_iff)
+apply (simp split: split_if_asm
+          add: well_ord_is_trans_on trans_pred_pred_eq domain_UN domain_Union, blast)
+done
+
+(*For the 4-way case analysis in the main result*)
+lemma domain_ord_iso_map_cases:
+     "[| well_ord(A,r);  well_ord(B,s) |]
+      ==> domain(ord_iso_map(A,r,B,s)) = A |
+          (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"
+apply (frule well_ord_is_wf)
+apply (unfold wf_on_def wf_def)
+apply (drule_tac x = "A-domain (ord_iso_map (A,r,B,s))" in spec)
+apply safe
+(*The first case: the domain equals A*)
+apply (rule domain_ord_iso_map [THEN equalityI])
+apply (erule Diff_eq_0_iff [THEN iffD1])
+(*The other case: the domain equals an initial segment*)
+apply (blast del: domainI subsetI
+	     elim!: predE
+	     intro!: domain_ord_iso_map_subset
+             intro: subsetI)+
+done
+
+(*As above, by duality*)
+lemma range_ord_iso_map_cases:
+    "[| well_ord(A,r);  well_ord(B,s) |]
+     ==> range(ord_iso_map(A,r,B,s)) = B |
+         (EX y:B. range(ord_iso_map(A,r,B,s)) = pred(B,y,s))"
+apply (rule converse_ord_iso_map [THEN subst])
+apply (simp add: domain_ord_iso_map_cases)
+done
+
+(*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*)
+lemma well_ord_trichotomy:
+   "[| well_ord(A,r);  well_ord(B,s) |]
+    ==> ord_iso_map(A,r,B,s) : ord_iso(A, r, B, s) |
+        (EX x:A. ord_iso_map(A,r,B,s) : ord_iso(pred(A,x,r), r, B, s)) |
+        (EX y:B. ord_iso_map(A,r,B,s) : ord_iso(A, r, pred(B,y,s), s))"
+apply (frule_tac B = B in domain_ord_iso_map_cases, assumption)
+apply (frule_tac B = B in range_ord_iso_map_cases, assumption)
+apply (drule ord_iso_map_ord_iso, assumption)
+apply (elim disjE bexE)
+   apply (simp_all add: bexI)
+apply (rule wf_on_not_refl [THEN notE])
+  apply (erule well_ord_is_wf)
+ apply assumption
+apply (subgoal_tac "<x,y>: ord_iso_map (A,r,B,s) ")
+ apply (drule rangeI)
+ apply (simp add: pred_def)
+apply (unfold ord_iso_map_def, blast)
+done
+
+
+(*** Properties of converse(r), by Krzysztof Grabczewski ***)
+
+lemma irrefl_converse: "irrefl(A,r) ==> irrefl(A,converse(r))"
+by (unfold irrefl_def, blast)
+
+lemma trans_on_converse: "trans[A](r) ==> trans[A](converse(r))"
+by (unfold trans_on_def, blast)
+
+lemma part_ord_converse: "part_ord(A,r) ==> part_ord(A,converse(r))"
+apply (unfold part_ord_def)
+apply (blast intro!: irrefl_converse trans_on_converse)
+done
+
+lemma linear_converse: "linear(A,r) ==> linear(A,converse(r))"
+by (unfold linear_def, blast)
+
+lemma tot_ord_converse: "tot_ord(A,r) ==> tot_ord(A,converse(r))"
+apply (unfold tot_ord_def)
+apply (blast intro!: part_ord_converse linear_converse)
+done
+
+
+(** By Krzysztof Grabczewski.
+    Lemmas involving the first element of a well ordered set **)
+
+lemma first_is_elem: "first(b,B,r) ==> b:B"
+by (unfold first_def, blast)
+
+lemma well_ord_imp_ex1_first:
+        "[| well_ord(A,r); B<=A; B~=0 |] ==> (EX! b. first(b,B,r))"
+apply (unfold well_ord_def wf_on_def wf_def first_def)
+apply (elim conjE allE disjE, blast)
+apply (erule bexE)
+apply (rule_tac a = x in ex1I, auto)
+apply (unfold tot_ord_def linear_def, blast)
+done
+
+lemma the_first_in:
+     "[| well_ord(A,r); B<=A; B~=0 |] ==> (THE b. first(b,B,r)) : B"
+apply (drule well_ord_imp_ex1_first, assumption+)
+apply (rule first_is_elem)
+apply (erule theI)
+done
+
+ML {*
+val pred_def = thm "pred_def"
+val linear_def = thm "linear_def"
+val part_ord_def = thm "part_ord_def"
+val tot_ord_def = thm "tot_ord_def"
+val well_ord_def = thm "well_ord_def"
+val ord_iso_def = thm "ord_iso_def"
+val mono_map_def = thm "mono_map_def";
+
+val part_ord_Imp_asym = thm "part_ord_Imp_asym";
+val linearE = thm "linearE";
+val well_ordI = thm "well_ordI";
+val well_ord_is_wf = thm "well_ord_is_wf";
+val well_ord_is_trans_on = thm "well_ord_is_trans_on";
+val well_ord_is_linear = thm "well_ord_is_linear";
+val pred_iff = thm "pred_iff";
+val predI = thm "predI";
+val predE = thm "predE";
+val pred_subset_under = thm "pred_subset_under";
+val pred_subset = thm "pred_subset";
+val pred_pred_eq = thm "pred_pred_eq";
+val trans_pred_pred_eq = thm "trans_pred_pred_eq";
+val part_ord_subset = thm "part_ord_subset";
+val linear_subset = thm "linear_subset";
+val tot_ord_subset = thm "tot_ord_subset";
+val well_ord_subset = thm "well_ord_subset";
+val irrefl_Int_iff = thm "irrefl_Int_iff";
+val trans_on_Int_iff = thm "trans_on_Int_iff";
+val part_ord_Int_iff = thm "part_ord_Int_iff";
+val linear_Int_iff = thm "linear_Int_iff";
+val tot_ord_Int_iff = thm "tot_ord_Int_iff";
+val wf_on_Int_iff = thm "wf_on_Int_iff";
+val well_ord_Int_iff = thm "well_ord_Int_iff";
+val irrefl_0 = thm "irrefl_0";
+val trans_on_0 = thm "trans_on_0";
+val part_ord_0 = thm "part_ord_0";
+val linear_0 = thm "linear_0";
+val tot_ord_0 = thm "tot_ord_0";
+val wf_on_0 = thm "wf_on_0";
+val well_ord_0 = thm "well_ord_0";
+val tot_ord_unit = thm "tot_ord_unit";
+val wf_on_unit = thm "wf_on_unit";
+val well_ord_unit = thm "well_ord_unit";
+val mono_map_is_fun = thm "mono_map_is_fun";
+val mono_map_is_inj = thm "mono_map_is_inj";
+val ord_isoI = thm "ord_isoI";
+val ord_iso_is_mono_map = thm "ord_iso_is_mono_map";
+val ord_iso_is_bij = thm "ord_iso_is_bij";
+val ord_iso_apply = thm "ord_iso_apply";
+val ord_iso_converse = thm "ord_iso_converse";
+val ord_iso_refl = thm "ord_iso_refl";
+val ord_iso_sym = thm "ord_iso_sym";
+val mono_map_trans = thm "mono_map_trans";
+val ord_iso_trans = thm "ord_iso_trans";
+val mono_ord_isoI = thm "mono_ord_isoI";
+val well_ord_mono_ord_isoI = thm "well_ord_mono_ord_isoI";
+val part_ord_ord_iso = thm "part_ord_ord_iso";
+val linear_ord_iso = thm "linear_ord_iso";
+val wf_on_ord_iso = thm "wf_on_ord_iso";
+val well_ord_ord_iso = thm "well_ord_ord_iso";
+val well_ord_iso_subset_lemma = thm "well_ord_iso_subset_lemma";
+val well_ord_iso_predE = thm "well_ord_iso_predE";
+val well_ord_iso_pred_eq = thm "well_ord_iso_pred_eq";
+val ord_iso_image_pred = thm "ord_iso_image_pred";
+val ord_iso_restrict_pred = thm "ord_iso_restrict_pred";
+val well_ord_iso_preserving = thm "well_ord_iso_preserving";
+val well_ord_iso_unique_lemma = thm "well_ord_iso_unique_lemma";
+val well_ord_iso_unique = thm "well_ord_iso_unique";
+val ord_iso_map_subset = thm "ord_iso_map_subset";
+val domain_ord_iso_map = thm "domain_ord_iso_map";
+val range_ord_iso_map = thm "range_ord_iso_map";
+val converse_ord_iso_map = thm "converse_ord_iso_map";
+val function_ord_iso_map = thm "function_ord_iso_map";
+val ord_iso_map_fun = thm "ord_iso_map_fun";
+val ord_iso_map_mono_map = thm "ord_iso_map_mono_map";
+val ord_iso_map_ord_iso = thm "ord_iso_map_ord_iso";
+val domain_ord_iso_map_subset = thm "domain_ord_iso_map_subset";
+val domain_ord_iso_map_cases = thm "domain_ord_iso_map_cases";
+val range_ord_iso_map_cases = thm "range_ord_iso_map_cases";
+val well_ord_trichotomy = thm "well_ord_trichotomy";
+val irrefl_converse = thm "irrefl_converse";
+val trans_on_converse = thm "trans_on_converse";
+val part_ord_converse = thm "part_ord_converse";
+val linear_converse = thm "linear_converse";
+val tot_ord_converse = thm "tot_ord_converse";
+val first_is_elem = thm "first_is_elem";
+val well_ord_imp_ex1_first = thm "well_ord_imp_ex1_first";
+val the_first_in = thm "the_first_in";
+*}
+
 end
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/OrderArith.ML
--- a/src/ZF/OrderArith.ML	Sat May 11 20:40:31 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,434 +0,0 @@
-(*  Title:      ZF/OrderArith.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1994  University of Cambridge
-
-Towards ordinal arithmetic 
-*)
-
-(**** Addition of relations -- disjoint sum ****)
-
-(** Rewrite rules.  Can be used to obtain introduction rules **)
-
-Goalw [radd_def] 
-    "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B";
-by (Blast_tac 1);
-qed "radd_Inl_Inr_iff";
-
-Goalw [radd_def] 
-    "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r";
-by (Blast_tac 1);
-qed "radd_Inl_iff";
-
-Goalw [radd_def] 
-    "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s";
-by (Blast_tac 1);
-qed "radd_Inr_iff";
-
-Goalw [radd_def] 
-    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False";
-by (Blast_tac 1);
-qed "radd_Inr_Inl_iff";
-
-(** Elimination Rule **)
-
-val major::prems = Goalw [radd_def]
-    "[| <p',p> : radd(A,r,B,s);                 \
-\       !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;       \
-\       !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q; \
-\       !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q  \
-\    |] ==> Q";
-by (cut_facts_tac [major] 1);
-(*Split into the three cases*)
-by (REPEAT_FIRST  (*can't use safe_tac: don't want hyp_subst_tac*)
-    (eresolve_tac [CollectE, Pair_inject, conjE, exE, SigmaE, disjE]));
-(*Apply each premise to correct subgoal; can't just use fast_tac
-  because hyp_subst_tac would delete equalities too quickly*)
-by (EVERY (map (fn prem => 
-                EVERY1 [rtac prem, assume_tac, REPEAT o Fast_tac])
-           prems));
-qed "raddE";
-
-(** Type checking **)
-
-Goalw [radd_def] "radd(A,r,B,s) <= (A+B) * (A+B)";
-by (rtac Collect_subset 1);
-qed "radd_type";
-
-bind_thm ("field_radd", radd_type RS field_rel_subset);
-
-(** Linearity **)
-
-AddIffs [radd_Inl_iff, radd_Inr_iff, 
-	 radd_Inl_Inr_iff, radd_Inr_Inl_iff];
-
-Goalw [linear_def]
-    "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
-by (Force_tac 1);
-qed "linear_radd";
-
-
-(** Well-foundedness **)
-
-Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))";
-by (rtac wf_onI2 1);
-by (subgoal_tac "ALL x:A. Inl(x): Ba" 1);
-(*Proving the lemma, which is needed twice!*)
-by (thin_tac "y : A + B" 2);
-by (rtac ballI 2);
-by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
-by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
-(*Returning to main part of proof*)
-by Safe_tac;
-by (Blast_tac 1);
-by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
-by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
-qed "wf_on_radd";
-
-Goal "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))";
-by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
-by (rtac (field_radd RSN (2, wf_on_subset_A)) 1);
-by (REPEAT (ares_tac [wf_on_radd] 1));
-qed "wf_radd";
-
-Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
-\           well_ord(A+B, radd(A,r,B,s))";
-by (rtac well_ordI 1);
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_radd]) 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [well_ord_def, tot_ord_def, linear_radd]) 1);
-qed "well_ord_radd";
-
-(** An ord_iso congruence law **)
-
-Goal "[| f: bij(A,C);  g: bij(B,D) |] ==> \
-\        (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)";
-by (res_inst_tac 
-        [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] 
-    lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "sum_bij";
-
-Goalw [ord_iso_def]
-    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>     \
-\           (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))            \
-\           : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))";
-by (safe_tac (claset() addSIs [sum_bij]));
-(*Do the beta-reductions now*)
-by (ALLGOALS (Asm_full_simp_tac));
-by Safe_tac;
-(*8 subgoals!*)
-by (ALLGOALS
-    (asm_full_simp_tac 
-     (simpset() addcongs [conj_cong] addsimps [bij_is_fun RS apply_type])));
-qed "sum_ord_iso_cong";
-
-(*Could we prove an ord_iso result?  Perhaps 
-     ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
-Goal "A Int B = 0 ==>     \
-\           (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)";
-by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")] 
-    lam_bijective 1);
-by Auto_tac;
-qed "sum_disjoint_bij";
-
-(** Associativity **)
-
-Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
-\ : bij((A+B)+C, A+(B+C))";
-by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] 
-    lam_bijective 1);
-by Auto_tac;
-qed "sum_assoc_bij";
-
-Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \
-\ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),    \
-\           A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))";
-by (resolve_tac [sum_assoc_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "sum_assoc_ord_iso";
-
-
-(**** Multiplication of relations -- lexicographic product ****)
-
-(** Rewrite rule.  Can be used to obtain introduction rules **)
-
-Goalw [rmult_def] 
-    "<<a',b'>, <a,b>> : rmult(A,r,B,s) <->       \
-\           (<a',a>: r  & a':A & a:A & b': B & b: B) |  \
-\           (<b',b>: s  & a'=a & a:A & b': B & b: B)";
-by (Blast_tac 1);
-qed "rmult_iff";
-
-AddIffs [rmult_iff];
-
-val major::prems = Goal
-    "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);              \
-\       [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;        \
-\       [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q \
-\    |] ==> Q";
-by (rtac (major RS (rmult_iff RS iffD1) RS disjE) 1);
-by (DEPTH_SOLVE (eresolve_tac ([asm_rl, conjE] @ prems) 1));
-qed "rmultE";
-
-(** Type checking **)
-
-Goalw [rmult_def] "rmult(A,r,B,s) <= (A*B) * (A*B)";
-by (rtac Collect_subset 1);
-qed "rmult_type";
-
-bind_thm ("field_rmult", (rmult_type RS field_rel_subset));
-
-(** Linearity **)
-
-val [lina,linb] = goal (the_context ())
-    "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))";
-by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
-by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac SigmaE));
-by (Asm_simp_tac 1);
-by (res_inst_tac [("x","xa"), ("y","xb")] (lina RS linearE) 1);
-by (res_inst_tac [("x","ya"), ("y","yb")] (linb RS linearE) 4);
-by (REPEAT_SOME (Blast_tac));
-qed "linear_rmult";
-
-
-(** Well-foundedness **)
-
-Goal "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))";
-by (rtac wf_onI2 1);
-by (etac SigmaE 1);
-by (etac ssubst 1);
-by (subgoal_tac "ALL b:B. <x,b>: Ba" 1);
-by (Blast_tac 1);
-by (eres_inst_tac [("a","x")] wf_on_induct 1 THEN assume_tac 1);
-by (rtac ballI 1);
-by (eres_inst_tac [("a","b")] wf_on_induct 1 THEN assume_tac 1);
-by (best_tac (claset() addSEs [rmultE, bspec RS mp]) 1);
-qed "wf_on_rmult";
-
-
-Goal "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))";
-by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1);
-by (rtac (field_rmult RSN (2, wf_on_subset_A)) 1);
-by (REPEAT (ares_tac [wf_on_rmult] 1));
-qed "wf_rmult";
-
-Goal "[| well_ord(A,r);  well_ord(B,s) |] ==> \
-\           well_ord(A*B, rmult(A,r,B,s))";
-by (rtac well_ordI 1);
-by (asm_full_simp_tac (simpset() addsimps [well_ord_def, wf_on_rmult]) 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [well_ord_def, tot_ord_def, linear_rmult]) 1);
-qed "well_ord_rmult";
-
-
-(** An ord_iso congruence law **)
-
-Goal "[| f: bij(A,C);  g: bij(B,D) |]   \
-\     ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
-by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")] 
-    lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "prod_bij";
-
-Goalw [ord_iso_def]
-    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |]     \
-\    ==> (lam <x,y>:A*B. <f`x, g`y>)                                 \
-\        : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))";
-by (safe_tac (claset() addSIs [prod_bij]));
-by (ALLGOALS
-    (asm_full_simp_tac (simpset() addsimps [bij_is_fun RS apply_type])));
-by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1);
-qed "prod_ord_iso_cong";
-
-Goal "(lam z:A. <x,z>) : bij(A, {x}*A)";
-by (res_inst_tac [("d", "snd")] lam_bijective 1);
-by Auto_tac;
-qed "singleton_prod_bij";
-
-(*Used??*)
-Goal "well_ord({x},xr) ==>  \
-\         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
-by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addDs [well_ord_is_wf RS wf_on_not_refl]) 1);
-qed "singleton_prod_ord_iso";
-
-(*Here we build a complicated function term, then simplify it using
-  case_cong, id_conv, comp_lam, case_case.*)
-Goal "a~:C ==> \
-\      (lam x:C*B + D. case(%x. x, %y.<a,y>, x)) \
-\      : bij(C*B + D, C*B Un {a}*D)";
-by (rtac subst_elem 1);
-by (resolve_tac [id_bij RS sum_bij RS comp_bij] 1);
-by (rtac singleton_prod_bij 1);
-by (rtac sum_disjoint_bij 1);
-by (Blast_tac 1);
-by (asm_simp_tac (simpset() addcongs [case_cong]) 1);
-by (resolve_tac [comp_lam RS trans RS sym] 1);
-by (fast_tac (claset() addSEs [case_type]) 1);
-by (asm_simp_tac (simpset() addsimps [case_case]) 1);
-qed "prod_sum_singleton_bij";
-
-Goal "[| a:A;  well_ord(A,r) |] ==> \
-\   (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x)) \
-\   : ord_iso(pred(A,a,r)*B + pred(B,b,s),              \
-\                 radd(A*B, rmult(A,r,B,s), B, s),      \
-\             pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))";
-by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1);
-by (asm_simp_tac
-    (simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
-by (auto_tac (claset() addSEs [well_ord_is_wf RS wf_on_asym, predE], 
-	      simpset()));
-qed "prod_sum_singleton_ord_iso";
-
-(** Distributive law **)
-
-Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
-\ : bij((A+B)*C, (A*C)+(B*C))";
-by (res_inst_tac
-    [("d", "case(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
-by Auto_tac;
-qed "sum_prod_distrib_bij";
-
-Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x)) \
-\ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \
-\           (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))";
-by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "sum_prod_distrib_ord_iso";
-
-(** Associativity **)
-
-Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
-by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
-by Auto_tac;
-qed "prod_assoc_bij";
-
-Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                   \
-\ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),  \
-\           A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))";
-by (resolve_tac [prod_assoc_bij RS ord_isoI] 1);
-by Auto_tac;
-qed "prod_assoc_ord_iso";
-
-(**** Inverse image of a relation ****)
-
-(** Rewrite rule **)
-
-Goalw [rvimage_def] "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A";
-by (Blast_tac 1);
-qed "rvimage_iff";
-
-(** Type checking **)
-
-Goalw [rvimage_def] "rvimage(A,f,r) <= A*A";
-by (rtac Collect_subset 1);
-qed "rvimage_type";
-
-bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset));
-
-Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))";
-by (Blast_tac 1);
-qed "rvimage_converse";
-
-
-(** Partial Ordering Properties **)
-
-Goalw [irrefl_def, rvimage_def]
-    "[| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))";
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
-qed "irrefl_rvimage";
-
-Goalw [trans_on_def, rvimage_def] 
-    "[| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))";
-by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
-qed "trans_on_rvimage";
-
-Goalw [part_ord_def]
-    "[| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))";
-by (blast_tac (claset() addSIs [irrefl_rvimage, trans_on_rvimage]) 1);
-qed "part_ord_rvimage";
-
-(** Linearity **)
-
-val [finj,lin] = goalw (the_context ()) [inj_def]
-    "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))";
-by (rewtac linear_def);    (*Note! the premises are NOT rewritten*)
-by (REPEAT_FIRST (ares_tac [ballI]));
-by (asm_simp_tac (simpset() addsimps [rvimage_iff]) 1);
-by (cut_facts_tac [finj] 1);
-by (res_inst_tac [("x","f`x"), ("y","f`y")] (lin RS linearE) 1);
-by (REPEAT_SOME (blast_tac (claset() addIs [apply_funtype])));
-qed "linear_rvimage";
-
-Goalw [tot_ord_def] 
-    "[| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))";
-by (blast_tac (claset() addSIs [part_ord_rvimage, linear_rvimage]) 1);
-qed "tot_ord_rvimage";
-
-
-(** Well-foundedness **)
-
-(*Not sure if wf_on_rvimage could be proved from this!*)
-Goal "wf(r) ==> wf(rvimage(A,f,r))"; 
-by (full_simp_tac (simpset() addsimps [rvimage_def, wf_eq_minimal]) 1);
-by (Clarify_tac 1);
-by (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w)}" 1);
-by (blast_tac (claset() delrules [allE]) 2);
-by (etac allE 1);
-by (mp_tac 1);
-by (Blast_tac 1);
-qed "wf_rvimage";
-AddSIs [wf_rvimage];
-
-Goal "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))";
-by (rtac wf_onI2 1);
-by (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba" 1);
-by (Blast_tac 1);
-by (eres_inst_tac [("a","f`y")] wf_on_induct 1);
-by (blast_tac (claset() addSIs [apply_funtype]) 1);
-by (blast_tac (claset() addSIs [apply_funtype] 
-                        addSDs [rvimage_iff RS iffD1]) 1);
-qed "wf_on_rvimage";
-
-(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
-Goal "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))";
-by (rtac well_ordI 1);
-by (rewrite_goals_tac [well_ord_def, tot_ord_def]);
-by (blast_tac (claset() addSIs [wf_on_rvimage, inj_is_fun]) 1);
-by (blast_tac (claset() addSIs [linear_rvimage]) 1);
-qed "well_ord_rvimage";
-
-Goalw [ord_iso_def]
-    "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)";
-by (asm_full_simp_tac (simpset() addsimps [rvimage_iff]) 1);
-qed "ord_iso_rvimage";
-
-Goalw [ord_iso_def, rvimage_def]
-    "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A";
-by (Blast_tac 1);
-qed "ord_iso_rvimage_eq";
-
-
-(** The "measure" relation is useful with wfrec **)
-
-Goal "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))";
-by (simp_tac (simpset() addsimps [measure_def, rvimage_def, Memrel_iff]) 1);
-by (rtac equalityI 1);		 
-by Auto_tac;  
-by (auto_tac (claset() addIs [Ord_in_Ord], simpset() addsimps [lt_def]));  
-qed "measure_eq_rvimage_Memrel";
-
-Goal "wf(measure(A,f))";
-by (simp_tac (simpset() addsimps [measure_eq_rvimage_Memrel, wf_Memrel, 
-                                  wf_rvimage]) 1);
-qed "wf_measure";
-AddIffs [wf_measure];
-
-Goal "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)";
-by (simp_tac (simpset() addsimps [measure_def]) 1);
-qed "measure_iff";
-AddIffs [measure_iff];
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/OrderArith.thy
--- a/src/ZF/OrderArith.thy	Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/OrderArith.thy	Mon May 13 09:02:13 2002 +0200
@@ -6,31 +6,507 @@
 Towards ordinal arithmetic.  Also useful with wfrec.
 *)
 
-OrderArith = Order + Sum + Ordinal +
-consts
-  radd, rmult      :: [i,i,i,i]=>i
-  rvimage          :: [i,i,i]=>i
+theory OrderArith = Order + Sum + Ordinal:
+constdefs
 
-defs
   (*disjoint sum of two relations; underlies ordinal addition*)
-  radd_def "radd(A,r,B,s) == 
+  radd    :: "[i,i,i,i]=>i"
+    "radd(A,r,B,s) == 
                 {z: (A+B) * (A+B).  
                     (EX x y. z = <Inl(x), Inr(y)>)   |   
                     (EX x' x. z = <Inl(x'), Inl(x)> & <x',x>:r)   |      
                     (EX y' y. z = <Inr(y'), Inr(y)> & <y',y>:s)}"
 
   (*lexicographic product of two relations; underlies ordinal multiplication*)
-  rmult_def "rmult(A,r,B,s) == 
+  rmult   :: "[i,i,i,i]=>i"
+    "rmult(A,r,B,s) == 
                 {z: (A*B) * (A*B).  
                     EX x' y' x y. z = <<x',y'>, <x,y>> &         
                        (<x',x>: r | (x'=x & <y',y>: s))}"
 
   (*inverse image of a relation*)
-  rvimage_def "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
+  rvimage :: "[i,i,i]=>i"
+    "rvimage(A,f,r) == {z: A*A. EX x y. z = <x,y> & <f`x,f`y>: r}"
+
+  measure :: "[i, i\<Rightarrow>i] \<Rightarrow> i"
+    "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
+
+
+(**** Addition of relations -- disjoint sum ****)
+
+(** Rewrite rules.  Can be used to obtain introduction rules **)
+
+lemma radd_Inl_Inr_iff [iff]: 
+    "<Inl(a), Inr(b)> : radd(A,r,B,s)  <->  a:A & b:B"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inl_iff [iff]: 
+    "<Inl(a'), Inl(a)> : radd(A,r,B,s)  <->  a':A & a:A & <a',a>:r"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inr_iff [iff]: 
+    "<Inr(b'), Inr(b)> : radd(A,r,B,s) <->  b':B & b:B & <b',b>:s"
+apply (unfold radd_def)
+apply blast
+done
+
+lemma radd_Inr_Inl_iff [iff]: 
+    "<Inr(b), Inl(a)> : radd(A,r,B,s) <->  False"
+apply (unfold radd_def)
+apply blast
+done
+
+(** Elimination Rule **)
+
+lemma raddE:
+    "[| <p',p> : radd(A,r,B,s);                  
+        !!x y. [| p'=Inl(x); x:A; p=Inr(y); y:B |] ==> Q;        
+        !!x' x. [| p'=Inl(x'); p=Inl(x); <x',x>: r; x':A; x:A |] ==> Q;  
+        !!y' y. [| p'=Inr(y'); p=Inr(y); <y',y>: s; y':B; y:B |] ==> Q   
+     |] ==> Q"
+apply (unfold radd_def)
+apply (blast intro: elim:); 
+done
+
+(** Type checking **)
+
+lemma radd_type: "radd(A,r,B,s) <= (A+B) * (A+B)"
+apply (unfold radd_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_radd = radd_type [THEN field_rel_subset]
+
+(** Linearity **)
+
+lemma linear_radd: 
+    "[| linear(A,r);  linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"
+apply (unfold linear_def)
+apply (blast intro: elim:); 
+done
+
+
+(** Well-foundedness **)
+
+lemma wf_on_radd: "[| wf[A](r);  wf[B](s) |] ==> wf[A+B](radd(A,r,B,s))"
+apply (rule wf_onI2)
+apply (subgoal_tac "ALL x:A. Inl (x) : Ba")
+(*Proving the lemma, which is needed twice!*)
+ prefer 2
+ apply (erule_tac V = "y : A + B" in thin_rl)
+ apply (rule_tac ballI)
+ apply (erule_tac r = "r" and a = "x" in wf_on_induct, assumption)
+ apply (blast intro: elim:); 
+(*Returning to main part of proof*)
+apply safe
+apply blast
+apply (erule_tac r = "s" and a = "ya" in wf_on_induct , assumption)
+apply (blast intro: elim:); 
+done
+
+lemma wf_radd: "[| wf(r);  wf(s) |] ==> wf(radd(field(r),r,field(s),s))"
+apply (simp add: wf_iff_wf_on_field)
+apply (rule wf_on_subset_A [OF _ field_radd])
+apply (blast intro: wf_on_radd) 
+done
+
+lemma well_ord_radd:
+     "[| well_ord(A,r);  well_ord(B,s) |] ==> well_ord(A+B, radd(A,r,B,s))"
+apply (rule well_ordI)
+apply (simp add: well_ord_def wf_on_radd)
+apply (simp add: well_ord_def tot_ord_def linear_radd)
+done
+
+(** An ord_iso congruence law **)
 
-constdefs
-   measure :: "[i, i\\<Rightarrow>i] \\<Rightarrow> i"
-   "measure(A,f) == {<x,y>: A*A. f(x) < f(y)}"
+lemma sum_bij:
+     "[| f: bij(A,C);  g: bij(B,D) |]
+      ==> (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z)) : bij(A+B, C+D)"
+apply (rule_tac d = "case (%x. Inl (converse (f) `x) , %y. Inr (converse (g) `y))" in lam_bijective)
+apply (typecheck add: bij_is_inj inj_is_fun) 
+apply (auto simp add: left_inverse_bij right_inverse_bij) 
+done
+
+lemma sum_ord_iso_cong: 
+    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |] ==>      
+            (lam z:A+B. case(%x. Inl(f`x), %y. Inr(g`y), z))             
+            : ord_iso(A+B, radd(A,r,B,s), A'+B', radd(A',r',B',s'))"
+apply (unfold ord_iso_def)
+apply (safe intro!: sum_bij)
+(*Do the beta-reductions now*)
+apply (auto cong add: conj_cong simp add: bij_is_fun [THEN apply_type])
+done
+
+(*Could we prove an ord_iso result?  Perhaps 
+     ord_iso(A+B, radd(A,r,B,s), A Un B, r Un s) *)
+lemma sum_disjoint_bij: "A Int B = 0 ==>      
+            (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)"
+apply (rule_tac d = "%z. if z:A then Inl (z) else Inr (z) " in lam_bijective)
+apply auto
+done
+
+(** Associativity **)
+
+lemma sum_assoc_bij:
+     "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
+      : bij((A+B)+C, A+(B+C))"
+apply (rule_tac d = "case (%x. Inl (Inl (x)), case (%x. Inl (Inr (x)), Inr))" 
+       in lam_bijective)
+apply auto
+done
+
+lemma sum_assoc_ord_iso:
+     "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z))  
+      : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t),     
+                A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"
+apply (rule sum_assoc_bij [THEN ord_isoI])
+apply auto
+done
+
+
+(**** Multiplication of relations -- lexicographic product ****)
+
+(** Rewrite rule.  Can be used to obtain introduction rules **)
+
+lemma  rmult_iff [iff]: 
+    "<<a',b'>, <a,b>> : rmult(A,r,B,s) <->        
+            (<a',a>: r  & a':A & a:A & b': B & b: B) |   
+            (<b',b>: s  & a'=a & a:A & b': B & b: B)"
+
+apply (unfold rmult_def)
+apply blast
+done
+
+lemma rmultE: 
+    "[| <<a',b'>, <a,b>> : rmult(A,r,B,s);               
+        [| <a',a>: r;  a':A;  a:A;  b':B;  b:B |] ==> Q;         
+        [| <b',b>: s;  a:A;  a'=a;  b':B;  b:B |] ==> Q  
+     |] ==> Q"
+apply (blast intro: elim:); 
+done
+
+(** Type checking **)
+
+lemma rmult_type: "rmult(A,r,B,s) <= (A*B) * (A*B)"
+apply (unfold rmult_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_rmult = rmult_type [THEN field_rel_subset]
+
+(** Linearity **)
+
+lemma linear_rmult:
+    "[| linear(A,r);  linear(B,s) |] ==> linear(A*B,rmult(A,r,B,s))"
+apply (simp add: linear_def); 
+apply (blast intro: elim:); 
+done
+
+(** Well-foundedness **)
+
+lemma wf_on_rmult: "[| wf[A](r);  wf[B](s) |] ==> wf[A*B](rmult(A,r,B,s))"
+apply (rule wf_onI2)
+apply (erule SigmaE)
+apply (erule ssubst)
+apply (subgoal_tac "ALL b:B. <x,b>: Ba")
+apply blast
+apply (erule_tac a = "x" in wf_on_induct , assumption)
+apply (rule ballI)
+apply (erule_tac a = "b" in wf_on_induct , assumption)
+apply (best elim!: rmultE bspec [THEN mp])
+done
+
+
+lemma wf_rmult: "[| wf(r);  wf(s) |] ==> wf(rmult(field(r),r,field(s),s))"
+apply (simp add: wf_iff_wf_on_field)
+apply (rule wf_on_subset_A [OF _ field_rmult])
+apply (blast intro: wf_on_rmult) 
+done
+
+lemma well_ord_rmult:
+     "[| well_ord(A,r);  well_ord(B,s) |] ==> well_ord(A*B, rmult(A,r,B,s))"
+apply (rule well_ordI)
+apply (simp add: well_ord_def wf_on_rmult)
+apply (simp add: well_ord_def tot_ord_def linear_rmult)
+done
 
 
+(** An ord_iso congruence law **)
+
+lemma prod_bij:
+     "[| f: bij(A,C);  g: bij(B,D) |] 
+      ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)"
+apply (rule_tac d = "%<x,y>. <converse (f) `x, converse (g) `y>" 
+       in lam_bijective)
+apply (typecheck add: bij_is_inj inj_is_fun) 
+apply (auto simp add: left_inverse_bij right_inverse_bij) 
+done
+
+lemma prod_ord_iso_cong: 
+    "[| f: ord_iso(A,r,A',r');  g: ord_iso(B,s,B',s') |]      
+     ==> (lam <x,y>:A*B. <f`x, g`y>)                                  
+         : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))"
+apply (unfold ord_iso_def)
+apply (safe intro!: prod_bij)
+apply (simp_all add: bij_is_fun [THEN apply_type])
+apply (blast intro: bij_is_inj [THEN inj_apply_equality])
+done
+
+lemma singleton_prod_bij: "(lam z:A. <x,z>) : bij(A, {x}*A)"
+apply (rule_tac d = "snd" in lam_bijective)
+apply auto
+done
+
+(*Used??*)
+lemma singleton_prod_ord_iso:
+     "well_ord({x},xr) ==>   
+          (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"
+apply (rule singleton_prod_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply (blast dest: well_ord_is_wf [THEN wf_on_not_refl])
+done
+
+(*Here we build a complicated function term, then simplify it using
+  case_cong, id_conv, comp_lam, case_case.*)
+lemma prod_sum_singleton_bij:
+     "a~:C ==>  
+       (lam x:C*B + D. case(%x. x, %y.<a,y>, x))  
+       : bij(C*B + D, C*B Un {a}*D)"
+apply (rule subst_elem)
+apply (rule id_bij [THEN sum_bij, THEN comp_bij])
+apply (rule singleton_prod_bij)
+apply (rule sum_disjoint_bij)
+apply blast
+apply (simp (no_asm_simp) cong add: case_cong)
+apply (rule comp_lam [THEN trans, symmetric])
+apply (fast elim!: case_type)
+apply (simp (no_asm_simp) add: case_case)
+done
+
+lemma prod_sum_singleton_ord_iso:
+ "[| a:A;  well_ord(A,r) |] ==>  
+    (lam x:pred(A,a,r)*B + pred(B,b,s). case(%x. x, %y.<a,y>, x))  
+    : ord_iso(pred(A,a,r)*B + pred(B,b,s),               
+                  radd(A*B, rmult(A,r,B,s), B, s),       
+              pred(A,a,r)*B Un {a}*pred(B,b,s), rmult(A,r,B,s))"
+apply (rule prod_sum_singleton_bij [THEN ord_isoI])
+apply (simp (no_asm_simp) add: pred_iff well_ord_is_wf [THEN wf_on_not_refl])
+apply (auto elim!: well_ord_is_wf [THEN wf_on_asym] predE)
+done
+
+(** Distributive law **)
+
+lemma sum_prod_distrib_bij:
+     "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
+      : bij((A+B)*C, (A*C)+(B*C))"
+apply (rule_tac d = "case (%<x,y>.<Inl (x) ,y>, %<x,y>.<Inr (x) ,y>) " 
+       in lam_bijective)
+apply auto
+done
+
+lemma sum_prod_distrib_ord_iso:
+ "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), x))  
+  : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t),  
+            (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"
+apply (rule sum_prod_distrib_bij [THEN ord_isoI])
+apply auto
+done
+
+(** Associativity **)
+
+lemma prod_assoc_bij:
+     "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))"
+apply (rule_tac d = "%<x, <y,z>>. <<x,y>, z>" in lam_bijective)
+apply auto
+done
+
+lemma prod_assoc_ord_iso:
+ "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>)                    
+  : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t),   
+            A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"
+apply (rule prod_assoc_bij [THEN ord_isoI])
+apply auto
+done
+
+(**** Inverse image of a relation ****)
+
+(** Rewrite rule **)
+
+lemma rvimage_iff: "<a,b> : rvimage(A,f,r)  <->  <f`a,f`b>: r & a:A & b:A"
+apply (unfold rvimage_def)
+apply blast
+done
+
+(** Type checking **)
+
+lemma rvimage_type: "rvimage(A,f,r) <= A*A"
+apply (unfold rvimage_def)
+apply (rule Collect_subset)
+done
+
+lemmas field_rvimage = rvimage_type [THEN field_rel_subset]
+
+lemma rvimage_converse: "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"
+apply (unfold rvimage_def)
+apply blast
+done
+
+
+(** Partial Ordering Properties **)
+
+lemma irrefl_rvimage: 
+    "[| f: inj(A,B);  irrefl(B,r) |] ==> irrefl(A, rvimage(A,f,r))"
+apply (unfold irrefl_def rvimage_def)
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+lemma trans_on_rvimage: 
+    "[| f: inj(A,B);  trans[B](r) |] ==> trans[A](rvimage(A,f,r))"
+apply (unfold trans_on_def rvimage_def)
+apply (blast intro: inj_is_fun [THEN apply_type])
+done
+
+lemma part_ord_rvimage: 
+    "[| f: inj(A,B);  part_ord(B,r) |] ==> part_ord(A, rvimage(A,f,r))"
+apply (unfold part_ord_def)
+apply (blast intro!: irrefl_rvimage trans_on_rvimage)
+done
+
+(** Linearity **)
+
+lemma linear_rvimage:
+    "[| f: inj(A,B);  linear(B,r) |] ==> linear(A,rvimage(A,f,r))"
+apply (simp add: inj_def linear_def rvimage_iff) 
+apply (blast intro: apply_funtype); 
+done
+
+lemma tot_ord_rvimage: 
+    "[| f: inj(A,B);  tot_ord(B,r) |] ==> tot_ord(A, rvimage(A,f,r))"
+apply (unfold tot_ord_def)
+apply (blast intro!: part_ord_rvimage linear_rvimage)
+done
+
+
+(** Well-foundedness **)
+
+(*Not sure if wf_on_rvimage could be proved from this!*)
+lemma wf_rvimage [intro!]: "wf(r) ==> wf(rvimage(A,f,r))"
+apply (simp (no_asm_use) add: rvimage_def wf_eq_minimal)
+apply clarify
+apply (subgoal_tac "EX w. w : {w: {f`x. x:Q}. EX x. x: Q & (f`x = w) }")
+ apply (erule allE)
+ apply (erule impE)
+ apply assumption; 
+ apply blast
+apply (blast intro: elim:); 
+done
+
+lemma wf_on_rvimage: "[| f: A->B;  wf[B](r) |] ==> wf[A](rvimage(A,f,r))"
+apply (rule wf_onI2)
+apply (subgoal_tac "ALL z:A. f`z=f`y --> z: Ba")
+ apply blast
+apply (erule_tac a = "f`y" in wf_on_induct)
+ apply (blast intro!: apply_funtype)
+apply (blast intro!: apply_funtype dest!: rvimage_iff [THEN iffD1])
+done
+
+(*Note that we need only wf[A](...) and linear(A,...) to get the result!*)
+lemma well_ord_rvimage:
+     "[| f: inj(A,B);  well_ord(B,r) |] ==> well_ord(A, rvimage(A,f,r))"
+apply (rule well_ordI)
+apply (unfold well_ord_def tot_ord_def)
+apply (blast intro!: wf_on_rvimage inj_is_fun)
+apply (blast intro!: linear_rvimage)
+done
+
+lemma ord_iso_rvimage: 
+    "f: bij(A,B) ==> f: ord_iso(A, rvimage(A,f,s), B, s)"
+apply (unfold ord_iso_def)
+apply (simp add: rvimage_iff)
+done
+
+lemma ord_iso_rvimage_eq: 
+    "f: ord_iso(A,r, B,s) ==> rvimage(A,f,s) = r Int A*A"
+apply (unfold ord_iso_def rvimage_def)
+apply blast
+done
+
+
+(** The "measure" relation is useful with wfrec **)
+
+lemma measure_eq_rvimage_Memrel:
+     "measure(A,f) = rvimage(A,Lambda(A,f),Memrel(Collect(RepFun(A,f),Ord)))"
+apply (simp (no_asm) add: measure_def rvimage_def Memrel_iff)
+apply (rule equalityI)
+apply auto
+apply (auto intro: Ord_in_Ord simp add: lt_def)
+done
+
+lemma wf_measure [iff]: "wf(measure(A,f))"
+apply (simp (no_asm) add: measure_eq_rvimage_Memrel wf_Memrel wf_rvimage)
+done
+
+lemma measure_iff [iff]: "<x,y> : measure(A,f) <-> x:A & y:A & f(x)<f(y)"
+apply (simp (no_asm) add: measure_def)
+done
+
+ML {*
+val measure_def = thm "measure_def";
+val radd_Inl_Inr_iff = thm "radd_Inl_Inr_iff";
+val radd_Inl_iff = thm "radd_Inl_iff";
+val radd_Inr_iff = thm "radd_Inr_iff";
+val radd_Inr_Inl_iff = thm "radd_Inr_Inl_iff";
+val raddE = thm "raddE";
+val radd_type = thm "radd_type";
+val field_radd = thm "field_radd";
+val linear_radd = thm "linear_radd";
+val wf_on_radd = thm "wf_on_radd";
+val wf_radd = thm "wf_radd";
+val well_ord_radd = thm "well_ord_radd";
+val sum_bij = thm "sum_bij";
+val sum_ord_iso_cong = thm "sum_ord_iso_cong";
+val sum_disjoint_bij = thm "sum_disjoint_bij";
+val sum_assoc_bij = thm "sum_assoc_bij";
+val sum_assoc_ord_iso = thm "sum_assoc_ord_iso";
+val rmult_iff = thm "rmult_iff";
+val rmultE = thm "rmultE";
+val rmult_type = thm "rmult_type";
+val field_rmult = thm "field_rmult";
+val linear_rmult = thm "linear_rmult";
+val wf_on_rmult = thm "wf_on_rmult";
+val wf_rmult = thm "wf_rmult";
+val well_ord_rmult = thm "well_ord_rmult";
+val prod_bij = thm "prod_bij";
+val prod_ord_iso_cong = thm "prod_ord_iso_cong";
+val singleton_prod_bij = thm "singleton_prod_bij";
+val singleton_prod_ord_iso = thm "singleton_prod_ord_iso";
+val prod_sum_singleton_bij = thm "prod_sum_singleton_bij";
+val prod_sum_singleton_ord_iso = thm "prod_sum_singleton_ord_iso";
+val sum_prod_distrib_bij = thm "sum_prod_distrib_bij";
+val sum_prod_distrib_ord_iso = thm "sum_prod_distrib_ord_iso";
+val prod_assoc_bij = thm "prod_assoc_bij";
+val prod_assoc_ord_iso = thm "prod_assoc_ord_iso";
+val rvimage_iff = thm "rvimage_iff";
+val rvimage_type = thm "rvimage_type";
+val field_rvimage = thm "field_rvimage";
+val rvimage_converse = thm "rvimage_converse";
+val irrefl_rvimage = thm "irrefl_rvimage";
+val trans_on_rvimage = thm "trans_on_rvimage";
+val part_ord_rvimage = thm "part_ord_rvimage";
+val linear_rvimage = thm "linear_rvimage";
+val tot_ord_rvimage = thm "tot_ord_rvimage";
+val wf_rvimage = thm "wf_rvimage";
+val wf_on_rvimage = thm "wf_on_rvimage";
+val well_ord_rvimage = thm "well_ord_rvimage";
+val ord_iso_rvimage = thm "ord_iso_rvimage";
+val ord_iso_rvimage_eq = thm "ord_iso_rvimage_eq";
+val measure_eq_rvimage_Memrel = thm "measure_eq_rvimage_Memrel";
+val wf_measure = thm "wf_measure";
+val measure_iff = thm "measure_iff";
+*}
+
 end
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";
-
diff -r 94648e0e4506 -r 6d97dbb189a9 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Sat May 11 20:40:31 2002 +0200
+++ b/src/ZF/OrderType.thy	Mon May 13 09:02:13 2002 +0200
@@ -3,48 +3,1022 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Order types and ordinal arithmetic.
+Order types and ordinal arithmetic in Zermelo-Fraenkel Set Theory 
 
 The order type of a well-ordering is the least ordinal isomorphic to it.
+
+Ordinal arithmetic is traditionally defined in terms of order types, as here.
+But a definition by transfinite recursion would be much simpler!
 *)
 
-OrderType = OrderArith + OrdQuant + 
+theory OrderType = OrderArith + OrdQuant:
 constdefs
   
-  ordermap  :: [i,i]=>i
+  ordermap  :: "[i,i]=>i"
    "ordermap(A,r) == lam x:A. wfrec[A](r, x, %x f. f `` pred(A,x,r))"
 
-  ordertype :: [i,i]=>i
+  ordertype :: "[i,i]=>i"
    "ordertype(A,r) == ordermap(A,r)``A"
 
   (*alternative definition of ordinal numbers*)
-  Ord_alt   :: i => o   
+  Ord_alt   :: "i => o"
    "Ord_alt(X) == well_ord(X, Memrel(X)) & (ALL u:X. u=pred(X, u, Memrel(X)))"
 
   (*coercion to ordinal: if not, just 0*)
-  ordify    :: i=>i
+  ordify    :: "i=>i"
     "ordify(x) == if Ord(x) then x else 0"
 
   (*ordinal multiplication*)
-  omult      :: [i,i]=>i           (infixl "**" 70)
+  omult      :: "[i,i]=>i"           (infixl "**" 70)
    "i ** j == ordertype(j*i, rmult(j,Memrel(j),i,Memrel(i)))"
 
   (*ordinal addition*)
-  raw_oadd   :: [i,i]=>i
+  raw_oadd   :: "[i,i]=>i"
     "raw_oadd(i,j) == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))"
 
-  oadd      :: [i,i]=>i           (infixl "++" 65)
+  oadd      :: "[i,i]=>i"           (infixl "++" 65)
     "i ++ j == raw_oadd(ordify(i),ordify(j))"
 
   (*ordinal subtraction*)
-  odiff      :: [i,i]=>i           (infixl "--" 65)
+  odiff      :: "[i,i]=>i"           (infixl "--" 65)
     "i -- j == ordertype(i-j, Memrel(i))"
 
   
 syntax (xsymbols)
-  "op **"     :: [i,i] => i          (infixl "\\<times>\\<times>" 70)
+  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
 
 syntax (HTML output)
-  "op **"     :: [i,i] => i          (infixl "\\<times>\\<times>" 70)
+  "op **"     :: "[i,i] => i"          (infixl "\<times>\<times>" 70)
+
+
+(*??for Ordinal.ML*)
+(*suitable for rewriting PROVIDED i has been fixed*)
+lemma Ord_in_Ord': "[| j:i; Ord(i) |] ==> Ord(j)"
+by (blast intro: Ord_in_Ord)
+
+
+(**** Proofs needing the combination of Ordinal.thy and Order.thy ****)
+
+lemma le_well_ord_Memrel: "j le i ==> well_ord(j, Memrel(i))"
+apply (rule well_ordI)
+apply (rule wf_Memrel [THEN wf_imp_wf_on])
+apply (simp add: ltD lt_Ord linear_def
+                 ltI [THEN lt_trans2 [of _ j i]])
+apply (intro ballI Ord_linear)
+apply (blast intro: Ord_in_Ord lt_Ord)+
+done
+
+(*"Ord(i) ==> well_ord(i, Memrel(i))"*)
+lemmas well_ord_Memrel = le_refl [THEN le_well_ord_Memrel]
+
+(*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
+  The smaller ordinal is an initial segment of the larger *)
+lemma lt_pred_Memrel: 
+    "j<i ==> pred(i, j, Memrel(i)) = j"
+apply (unfold pred_def lt_def)
+apply (simp (no_asm_simp))
+apply (blast intro: Ord_trans)
+done
+
+lemma pred_Memrel: 
+      "x:A ==> pred(A, x, Memrel(A)) = A Int x"
+by (unfold pred_def Memrel_def, blast)
+
+lemma Ord_iso_implies_eq_lemma:
+     "[| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R"
+apply (frule lt_pred_Memrel)
+apply (erule ltE)
+apply (rule well_ord_Memrel [THEN well_ord_iso_predE, of i f j], auto) 
+apply (unfold ord_iso_def)
+(*Combining the two simplifications causes looping*)
+apply (simp (no_asm_simp))
+apply (blast intro: bij_is_fun [THEN apply_type] Ord_trans)
+done
+
+(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
+lemma Ord_iso_implies_eq:
+     "[| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j)) |]     
+      ==> i=j"
+apply (rule_tac i = i and j = j in Ord_linear_lt)
+apply (blast intro: ord_iso_sym Ord_iso_implies_eq_lemma)+
+done
+
+
+(**** Ordermap and ordertype ****)
+
+lemma ordermap_type: 
+    "ordermap(A,r) : A -> ordertype(A,r)"
+apply (unfold ordermap_def ordertype_def)
+apply (rule lam_type)
+apply (rule lamI [THEN imageI], assumption+)
+done
+
+(*** Unfolding of ordermap ***)
+
+(*Useful for cardinality reasoning; see CardinalArith.ML*)
+lemma ordermap_eq_image: 
+    "[| wf[A](r);  x:A |]
+     ==> ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)"
+apply (unfold ordermap_def pred_def)
+apply (simp (no_asm_simp))
+apply (erule wfrec_on [THEN trans], assumption)
+apply (simp (no_asm_simp) add: subset_iff image_lam vimage_singleton_iff)
+done
+
+(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
+lemma ordermap_pred_unfold:
+     "[| wf[A](r);  x:A |]
+      ==> ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}"
+by (simp add: ordermap_eq_image pred_subset ordermap_type [THEN image_fun])
+
+(*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
+lemmas ordermap_unfold = ordermap_pred_unfold [simplified pred_def] 
+
+(*The theorem above is 
+
+[| wf[A](r); x : A |]
+==> ordermap(A,r) ` x = {ordermap(A,r) ` y . y: {y: A . <y,x> : r}}
+
+NOTE: the definition of ordermap used here delivers ordinals only if r 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 ***)
+
+lemma Ord_ordermap: 
+    "[| well_ord(A,r);  x:A |] ==> Ord(ordermap(A,r) ` x)"
+apply (unfold well_ord_def tot_ord_def part_ord_def, safe)
+apply (rule_tac a=x in wf_on_induct, assumption+)
+apply (simp (no_asm_simp) add: ordermap_pred_unfold)
+apply (rule OrdI [OF _ Ord_is_Transset])
+apply (unfold pred_def Transset_def)
+apply (blast intro: trans_onD
+	     dest!: ordermap_unfold [THEN equalityD1])+ 
+done
+
+lemma Ord_ordertype: 
+    "well_ord(A,r) ==> Ord(ordertype(A,r))"
+apply (unfold ordertype_def)
+apply (subst image_fun [OF ordermap_type subset_refl])
+apply (rule OrdI [OF _ Ord_is_Transset])
+prefer 2 apply (blast intro: Ord_ordermap)
+apply (unfold Transset_def well_ord_def)
+apply (blast intro: trans_onD
+	     dest!: ordermap_unfold [THEN equalityD1])
+done
+
+
+(*** ordermap preserves the orderings in both directions ***)
+
+lemma ordermap_mono:
+     "[| <w,x>: r;  wf[A](r);  w: A; x: A |]
+      ==> ordermap(A,r)`w : ordermap(A,r)`x"
+apply (erule_tac x1 = x in ordermap_unfold [THEN ssubst], assumption)
+apply blast
+done
+
+(*linearity of r is crucial here*)
+lemma converse_ordermap_mono: 
+    "[| ordermap(A,r)`w : ordermap(A,r)`x;  well_ord(A,r); w: A; x: A |]
+     ==> <w,x>: r"
+apply (unfold well_ord_def tot_ord_def, safe)
+apply (erule_tac x=w and y=x in linearE, assumption+) 
+apply (blast elim!: mem_not_refl [THEN notE])
+apply (blast dest: ordermap_mono intro: mem_asym) 
+done
+
+lemmas ordermap_surj = 
+    ordermap_type [THEN surj_image, unfolded ordertype_def [symmetric]]
+
+lemma ordermap_bij: 
+    "well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))"
+apply (unfold well_ord_def tot_ord_def bij_def inj_def)
+apply (force intro!: ordermap_type ordermap_surj 
+             elim: linearE dest: ordermap_mono 
+             simp add: mem_not_refl)
+done
+
+(*** Isomorphisms involving ordertype ***)
+
+lemma ordertype_ord_iso: 
+ "well_ord(A,r)
+  ==> ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))"
+apply (unfold ord_iso_def)
+apply (safe elim!: well_ord_is_wf 
+            intro!: ordermap_type [THEN apply_type] ordermap_mono ordermap_bij)
+apply (blast dest!: converse_ordermap_mono)
+done
+
+lemma ordertype_eq:
+     "[| f: ord_iso(A,r,B,s);  well_ord(B,s) |]
+      ==> ordertype(A,r) = ordertype(B,s)"
+apply (frule well_ord_ord_iso, assumption)
+apply (rule Ord_iso_implies_eq, (erule Ord_ordertype)+)
+apply (blast intro: ord_iso_trans ord_iso_sym ordertype_ord_iso)
+done
+
+lemma ordertype_eq_imp_ord_iso:
+     "[| ordertype(A,r) = ordertype(B,s); well_ord(A,r);  well_ord(B,s) |] 
+      ==> EX f. f: ord_iso(A,r,B,s)"
+apply (rule exI)
+apply (rule ordertype_ord_iso [THEN ord_iso_trans], assumption)
+apply (erule ssubst)
+apply (erule ordertype_ord_iso [THEN ord_iso_sym])
+done
+
+(*** Basic equalities for ordertype ***)
+
+(*Ordertype of Memrel*)
+lemma le_ordertype_Memrel: "j le i ==> ordertype(j,Memrel(i)) = j"
+apply (rule Ord_iso_implies_eq [symmetric])
+apply (erule ltE, assumption)
+apply (blast intro: le_well_ord_Memrel Ord_ordertype)
+apply (rule ord_iso_trans)
+apply (erule_tac [2] le_well_ord_Memrel [THEN ordertype_ord_iso])
+apply (rule id_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply (fast elim: ltE Ord_in_Ord Ord_trans)
+done
+
+(*"Ord(i) ==> ordertype(i, Memrel(i)) = i"*)
+lemmas ordertype_Memrel = le_refl [THEN le_ordertype_Memrel]
+
+lemma ordertype_0 [simp]: "ordertype(0,r) = 0"
+apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq, THEN trans])
+apply (erule emptyE)
+apply (rule well_ord_0)
+apply (rule Ord_0 [THEN ordertype_Memrel])
+done
+
+(*Ordertype of rvimage:  [| f: bij(A,B);  well_ord(B,s) |] ==>
+                         ordertype(A, rvimage(A,f,s)) = ordertype(B,s) *)
+lemmas bij_ordertype_vimage = ord_iso_rvimage [THEN ordertype_eq]
+
+(*** A fundamental unfolding law for ordertype. ***)
+
+(*Ordermap returns the same result if applied to an initial segment*)
+lemma ordermap_pred_eq_ordermap:
+     "[| well_ord(A,r);  y:A;  z: pred(A,y,r) |]
+      ==> ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z"
+apply (frule wf_on_subset_A [OF well_ord_is_wf pred_subset])
+apply (rule_tac a=z in wf_on_induct, assumption+)
+apply (safe elim!: predE)
+apply (simp (no_asm_simp) add: ordermap_pred_unfold well_ord_is_wf pred_iff)
+(*combining these two simplifications LOOPS! *)
+apply (simp (no_asm_simp) add: pred_pred_eq)
+apply (simp add: pred_def)
+apply (rule RepFun_cong [OF _ refl])
+apply (drule well_ord_is_trans_on)
+apply (fast elim!: trans_onD)
+done
+
+lemma ordertype_unfold: 
+    "ordertype(A,r) = {ordermap(A,r)`y . y : A}"
+apply (unfold ordertype_def)
+apply (rule image_fun [OF ordermap_type subset_refl])
+done
+
+(** Theorems by Krzysztof Grabczewski; proofs simplified by lcp **)
+
+lemma ordertype_pred_subset: "[| well_ord(A,r);  x:A |] ==>              
+          ordertype(pred(A,x,r),r) <= ordertype(A,r)"
+apply (simp add: ordertype_unfold well_ord_subset [OF _ pred_subset])
+apply (fast intro: ordermap_pred_eq_ordermap elim: predE)
+done
+
+lemma ordertype_pred_lt:
+     "[| well_ord(A,r);  x:A |]
+      ==> ordertype(pred(A,x,r),r) < ordertype(A,r)"
+apply (rule ordertype_pred_subset [THEN subset_imp_le, THEN leE])
+apply (simp_all add: Ord_ordertype well_ord_subset [OF _ pred_subset])
+apply (erule sym [THEN ordertype_eq_imp_ord_iso, THEN exE])
+apply (erule_tac [3] well_ord_iso_predE)
+apply (simp_all add: well_ord_subset [OF _ pred_subset])
+done
+
+(*May rewrite with this -- provided no rules are supplied for proving that
+        well_ord(pred(A,x,r), r) *)
+lemma ordertype_pred_unfold:
+     "well_ord(A,r)
+      ==> ordertype(A,r) = {ordertype(pred(A,x,r),r). x:A}"
+apply (rule equalityI)
+apply (safe intro!: ordertype_pred_lt [THEN ltD])
+apply (auto simp add: ordertype_def well_ord_is_wf [THEN ordermap_eq_image]
+                      ordermap_type [THEN image_fun]
+                      ordermap_pred_eq_ordermap pred_subset)
+done
+
+
+(**** Alternative definition of ordinal ****)
+
+(*proof by Krzysztof Grabczewski*)
+lemma Ord_is_Ord_alt: "Ord(i) ==> Ord_alt(i)"
+apply (unfold Ord_alt_def)
+apply (rule conjI)
+apply (erule well_ord_Memrel)
+apply (unfold Ord_def Transset_def pred_def Memrel_def, blast) 
+done
+
+(*proof by lcp*)
+lemma Ord_alt_is_Ord: 
+    "Ord_alt(i) ==> Ord(i)"
+apply (unfold Ord_alt_def Ord_def Transset_def well_ord_def 
+                     tot_ord_def part_ord_def trans_on_def)
+apply (simp add: pred_Memrel)
+apply (blast elim!: equalityE)
+done
+
+
+(**** Ordinal Addition ****)
+
+(*** Order Type calculations for radd ***)
+
+(** Addition with 0 **)
+
+lemma bij_sum_0: "(lam z:A+0. case(%x. x, %y. y, z)) : bij(A+0, A)"
+apply (rule_tac d = Inl in lam_bijective, safe)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_sum_0_eq:
+     "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)"
+apply (rule bij_sum_0 [THEN ord_isoI, THEN ordertype_eq])
+prefer 2 apply assumption
+apply force
+done
+
+lemma bij_0_sum: "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)"
+apply (rule_tac d = Inr in lam_bijective, safe)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_0_sum_eq:
+     "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)"
+apply (rule bij_0_sum [THEN ord_isoI, THEN ordertype_eq])
+prefer 2 apply assumption
+apply force
+done
+
+(** Initial segments of radd.  Statements by Grabczewski **)
+
+(*In fact, pred(A+B, Inl(a), radd(A,r,B,s)) = pred(A,a,r)+0 *)
+lemma pred_Inl_bij: 
+ "a:A ==> (lam x:pred(A,a,r). Inl(x))     
+          : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))"
+apply (unfold pred_def)
+apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
+apply auto
+done
+
+lemma ordertype_pred_Inl_eq:
+     "[| a:A;  well_ord(A,r) |]
+      ==> ordertype(pred(A+B, Inl(a), radd(A,r,B,s)), radd(A,r,B,s)) =  
+          ordertype(pred(A,a,r), r)"
+apply (rule pred_Inl_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+apply (simp_all add: well_ord_subset [OF _ pred_subset])
+apply (simp add: pred_def)
+done
+
+lemma pred_Inr_bij: 
+ "b:B ==>   
+         id(A+pred(B,b,s))       
+         : bij(A+pred(B,b,s), pred(A+B, Inr(b), radd(A,r,B,s)))"
+apply (unfold pred_def id_def)
+apply (rule_tac d = "%z. z" in lam_bijective, auto) 
+done
+
+lemma ordertype_pred_Inr_eq:
+     "[| b:B;  well_ord(A,r);  well_ord(B,s) |]
+      ==> ordertype(pred(A+B, Inr(b), radd(A,r,B,s)), radd(A,r,B,s)) =  
+          ordertype(A+pred(B,b,s), radd(A,r,pred(B,b,s),s))"
+apply (rule pred_Inr_bij [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+prefer 2 apply (force simp add: pred_def id_def, assumption)
+apply (blast intro: well_ord_radd well_ord_subset [OF _ pred_subset])
+done
+
+
+(*** ordify: trivial coercion to an ordinal ***)
+
+lemma Ord_ordify [iff, TC]: "Ord(ordify(x))"
+by (simp add: ordify_def)
+
+(*Collapsing*)
+lemma ordify_idem [simp]: "ordify(ordify(x)) = ordify(x)"
+by (simp add: ordify_def)
+
+
+(*** Basic laws for ordinal addition ***)
+
+lemma Ord_raw_oadd: "[|Ord(i); Ord(j)|] ==> Ord(raw_oadd(i,j))"
+by (simp add: raw_oadd_def ordify_def Ord_ordertype well_ord_radd
+              well_ord_Memrel)
+
+lemma Ord_oadd [iff,TC]: "Ord(i++j)"
+by (simp add: oadd_def Ord_raw_oadd)
+
+
+(** Ordinal addition with zero **)
+
+lemma raw_oadd_0: "Ord(i) ==> raw_oadd(i,0) = i"
+by (simp add: raw_oadd_def ordify_def ordertype_sum_0_eq
+              ordertype_Memrel well_ord_Memrel)
+
+lemma oadd_0 [simp]: "Ord(i) ==> i++0 = i"
+apply (simp (no_asm_simp) add: oadd_def raw_oadd_0 ordify_def)
+done
+
+lemma raw_oadd_0_left: "Ord(i) ==> raw_oadd(0,i) = i"
+by (simp add: raw_oadd_def ordify_def ordertype_0_sum_eq ordertype_Memrel
+              well_ord_Memrel)
+
+lemma oadd_0_left [simp]: "Ord(i) ==> 0++i = i"
+by (simp add: oadd_def raw_oadd_0_left ordify_def)
+
+
+lemma oadd_eq_if_raw_oadd:
+     "i++j = (if Ord(i) then (if Ord(j) then raw_oadd(i,j) else i)  
+              else (if Ord(j) then j else 0))"
+by (simp add: oadd_def ordify_def raw_oadd_0_left raw_oadd_0)
+
+lemma raw_oadd_eq_oadd: "[|Ord(i); Ord(j)|] ==> raw_oadd(i,j) = i++j"
+by (simp add: oadd_def ordify_def)
+
+(*** Further properties of ordinal addition.  Statements by Grabczewski,
+    proofs by lcp. ***)
+
+(*Surely also provable by transfinite induction on j?*)
+lemma lt_oadd1: "k<i ==> k < i++j"
+apply (simp add: oadd_def ordify_def lt_Ord2 raw_oadd_0, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ltE, assumption)
+apply (rule ltI)
+apply (force simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel
+          ordertype_pred_Inl_eq lt_pred_Memrel leI [THEN le_ordertype_Memrel])
+apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)
+done
+
+(*Thus also we obtain the rule  i++j = k ==> i le k *)
+lemma oadd_le_self: "Ord(i) ==> i le i++j"
+apply (rule all_lt_imp_le)
+apply (auto simp add: Ord_oadd lt_oadd1) 
+done
+
+(** A couple of strange but necessary results! **)
+
+lemma id_ord_iso_Memrel: "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))"
+apply (rule id_bij [THEN ord_isoI])
+apply (simp (no_asm_simp))
+apply blast
+done
+
+lemma ordertype_sum_Memrel:
+     "[| well_ord(A,r);  k<j |]
+      ==> ordertype(A+k, radd(A, r, k, Memrel(j))) =  
+          ordertype(A+k, radd(A, r, k, Memrel(k)))"
+apply (erule ltE)
+apply (rule ord_iso_refl [THEN sum_ord_iso_cong, THEN ordertype_eq])
+apply (erule OrdmemD [THEN id_ord_iso_Memrel, THEN ord_iso_sym])
+apply (simp_all add: well_ord_radd well_ord_Memrel)
+done
+
+lemma oadd_lt_mono2: "k<j ==> i++k < i++j"
+apply (simp add: oadd_def ordify_def raw_oadd_0_left lt_Ord lt_Ord2, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ltE, assumption)
+apply (rule ordertype_pred_unfold [THEN equalityD2, THEN subsetD, THEN ltI])
+apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
+apply (rule bexI)
+apply (erule_tac [2] InrI)
+apply (simp add: ordertype_pred_Inr_eq well_ord_Memrel lt_pred_Memrel
+                 leI [THEN le_ordertype_Memrel] ordertype_sum_Memrel)
+done
+
+lemma oadd_lt_cancel2: "[| i++j < i++k;  Ord(j) |] ==> j<k"
+apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+ prefer 2
+ apply (frule_tac i = i and j = j in oadd_le_self)
+ apply (simp add: oadd_def ordify_def lt_Ord not_lt_iff_le [THEN iff_sym])
+apply (rule Ord_linear_lt, auto) 
+apply (simp_all add: raw_oadd_eq_oadd)
+apply (blast dest: oadd_lt_mono2 elim: lt_irrefl lt_asym)+
+done
+
+lemma oadd_lt_iff2: "Ord(j) ==> i++j < i++k <-> j<k"
+by (blast intro!: oadd_lt_mono2 dest!: oadd_lt_cancel2)
+
+lemma oadd_inject: "[| i++j = i++k;  Ord(j); Ord(k) |] ==> j=k"
+apply (simp add: oadd_eq_if_raw_oadd split add: split_if_asm)
+apply (simp add: raw_oadd_eq_oadd)
+apply (rule Ord_linear_lt, auto) 
+apply (force dest: oadd_lt_mono2 [of concl: i] simp add: lt_not_refl)+
+done
+
+lemma lt_oadd_disj: "k < i++j ==> k<i | (EX l:j. k = i++l )"
+apply (simp add: Ord_in_Ord' [of _ j] oadd_eq_if_raw_oadd
+            split add: split_if_asm)
+ prefer 2
+ apply (simp add: Ord_in_Ord' [of _ j] lt_def)
+apply (simp add: ordertype_pred_unfold well_ord_radd well_ord_Memrel raw_oadd_def)
+apply (erule ltD [THEN RepFunE])
+apply (force simp add: ordertype_pred_Inl_eq well_ord_Memrel ltI 
+                       lt_pred_Memrel le_ordertype_Memrel leI
+                       ordertype_pred_Inr_eq ordertype_sum_Memrel)
+done
+
+
+(*** Ordinal addition with successor -- via associativity! ***)
+
+lemma oadd_assoc: "(i++j)++k = i++(j++k)"
+apply (simp add: oadd_eq_if_raw_oadd Ord_raw_oadd raw_oadd_0 raw_oadd_0_left, clarify)
+apply (simp add: raw_oadd_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule sum_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
+                                 ord_iso_refl])
+apply (simp_all add: Ord_ordertype well_ord_radd well_ord_Memrel)
+apply (rule sum_assoc_ord_iso [THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] sum_ord_iso_cong [OF ord_iso_refl ordertype_ord_iso])
+apply (blast intro: Ord_ordertype well_ord_radd well_ord_Memrel)+
+done
+
+lemma oadd_unfold: "[| Ord(i);  Ord(j) |] ==> i++j = i Un (UN k:j. {i++k})"
+apply (rule subsetI [THEN equalityI])
+apply (erule ltI [THEN lt_oadd_disj, THEN disjE])
+apply (blast intro: Ord_oadd) 
+apply (blast elim!: ltE, blast) 
+apply (force intro: lt_oadd1 oadd_lt_mono2 simp add: Ord_mem_iff_lt)
+done
+
+lemma oadd_1: "Ord(i) ==> i++1 = succ(i)"
+apply (simp (no_asm_simp) add: oadd_unfold Ord_1 oadd_0)
+apply blast
+done
+
+lemma oadd_succ [simp]: "Ord(j) ==> i++succ(j) = succ(i++j)"
+apply (simp add: oadd_eq_if_raw_oadd, clarify)
+apply (simp add: raw_oadd_eq_oadd)
+apply (simp add: oadd_1 [of j, symmetric] oadd_1 [of "i++j", symmetric]
+                 oadd_assoc)
+done
+
+
+(** Ordinal addition with limit ordinals **)
+
+lemma oadd_UN:
+     "[| !!x. x:A ==> Ord(j(x));  a:A |]
+      ==> i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"
+by (blast intro: ltI Ord_UN Ord_oadd lt_oadd1 [THEN ltD] 
+                 oadd_lt_mono2 [THEN ltD] 
+          elim!: ltE dest!: ltI [THEN lt_oadd_disj])
+
+lemma oadd_Limit: "Limit(j) ==> i++j = (UN k:j. i++k)"
+apply (frule Limit_has_0 [THEN ltD])
+apply (simp (no_asm_simp) add: Limit_is_Ord [THEN Ord_in_Ord] oadd_UN [symmetric] Union_eq_UN [symmetric] Limit_Union_eq)
+done
+
+(** Order/monotonicity properties of ordinal addition **)
+
+lemma oadd_le_self2: "Ord(i) ==> i le j++i"
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp) add: Ord_0_le)
+apply (simp (no_asm_simp) add: oadd_succ succ_leI)
+apply (simp (no_asm_simp) add: oadd_Limit)
+apply (rule le_trans)
+apply (rule_tac [2] le_implies_UN_le_UN)
+apply (erule_tac [2] bspec)
+prefer 2 apply assumption
+apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq le_refl Limit_is_Ord)
+done
+
+lemma oadd_le_mono1: "k le j ==> k++i le j++i"
+apply (frule lt_Ord)
+apply (frule le_Ord2)
+apply (simp add: oadd_eq_if_raw_oadd, clarify)
+apply (simp add: raw_oadd_eq_oadd)
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp) add: oadd_succ succ_le_iff)
+apply (simp (no_asm_simp) add: oadd_Limit)
+apply (rule le_implies_UN_le_UN, blast)
+done
+
+lemma oadd_lt_mono: "[| i' le i;  j'<j |] ==> i'++j' < i++j"
+by (blast intro: lt_trans1 oadd_le_mono1 oadd_lt_mono2 Ord_succD elim: ltE)
+
+lemma oadd_le_mono: "[| i' le i;  j' le j |] ==> i'++j' le i++j"
+by (simp del: oadd_succ add: oadd_succ [symmetric] le_Ord2 oadd_lt_mono)
+
+lemma oadd_le_iff2: "[| Ord(j); Ord(k) |] ==> i++j le i++k <-> j le k"
+by (simp del: oadd_succ add: oadd_lt_iff2 oadd_succ [symmetric] Ord_succ)
+
+
+(** Ordinal subtraction; the difference is ordertype(j-i, Memrel(j)). 
+    Probably simpler to define the difference recursively!
+**)
+
+lemma bij_sum_Diff:
+     "A<=B ==> (lam y:B. if(y:A, Inl(y), Inr(y))) : bij(B, A+(B-A))"
+apply (rule_tac d = "case (%x. x, %y. y) " in lam_bijective)
+apply (blast intro!: if_type)
+apply (fast intro!: case_type)
+apply (erule_tac [2] sumE)
+apply (simp_all (no_asm_simp))
+done
+
+lemma ordertype_sum_Diff:
+     "i le j ==>   
+            ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j))) =        
+            ordertype(j, Memrel(j))"
+apply (safe dest!: le_subset_iff [THEN iffD1])
+apply (rule bij_sum_Diff [THEN ord_isoI, THEN ord_iso_sym, THEN ordertype_eq])
+apply (erule_tac [3] well_ord_Memrel, assumption)
+apply (simp (no_asm_simp))
+apply (frule_tac j = y in Ord_in_Ord, assumption)
+apply (frule_tac j = x in Ord_in_Ord, assumption)
+apply (simp (no_asm_simp) add: Ord_mem_iff_lt lt_Ord not_lt_iff_le)
+apply (blast intro: lt_trans2 lt_trans)
+done
+
+lemma Ord_odiff [simp,TC]: 
+    "[| Ord(i);  Ord(j) |] ==> Ord(i--j)"
+apply (unfold odiff_def)
+apply (blast intro: Ord_ordertype Diff_subset well_ord_subset well_ord_Memrel)
+done
+
+
+lemma raw_oadd_ordertype_Diff: 
+   "i le j   
+    ==> raw_oadd(i,j--i) = ordertype(i+(j-i), radd(i,Memrel(j),j-i,Memrel(j)))"
+apply (simp add: raw_oadd_def odiff_def)
+apply (safe dest!: le_subset_iff [THEN iffD1])
+apply (rule sum_ord_iso_cong [THEN ordertype_eq])
+apply (erule id_ord_iso_Memrel)
+apply (rule ordertype_ord_iso [THEN ord_iso_sym])
+apply (blast intro: well_ord_radd Diff_subset well_ord_subset well_ord_Memrel)+
+done
+
+lemma oadd_odiff_inverse: "i le j ==> i ++ (j--i) = j"
+by (simp add: lt_Ord le_Ord2 oadd_def ordify_def raw_oadd_ordertype_Diff
+              ordertype_sum_Diff ordertype_Memrel lt_Ord2 [THEN Ord_succD])
+
+(*By oadd_inject, the difference between i and j is unique.  Note that we get
+  i++j = k  ==>  j = k--i.  *)
+lemma odiff_oadd_inverse: "[| Ord(i); Ord(j) |] ==> (i++j) -- i = j"
+apply (rule oadd_inject)
+apply (blast intro: oadd_odiff_inverse oadd_le_self)
+apply (blast intro: Ord_ordertype Ord_oadd Ord_odiff)+
+done
+
+lemma odiff_lt_mono2: "[| i<j;  k le i |] ==> i--k < j--k"
+apply (rule_tac i = k in oadd_lt_cancel2)
+apply (simp add: oadd_odiff_inverse)
+apply (subst oadd_odiff_inverse)
+apply (blast intro: le_trans leI, assumption)
+apply (simp (no_asm_simp) add: lt_Ord le_Ord2)
+done
+
+
+(**** Ordinal Multiplication ****)
+
+lemma Ord_omult [simp,TC]: 
+    "[| Ord(i);  Ord(j) |] ==> Ord(i**j)"
+apply (unfold omult_def)
+apply (blast intro: Ord_ordertype well_ord_rmult well_ord_Memrel)
+done
+
+(*** A useful unfolding law ***)
+
+lemma pred_Pair_eq: 
+ "[| a:A;  b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) =      
+                      pred(A,a,r)*B Un ({a} * pred(B,b,s))"
+apply (unfold pred_def, blast)
+done
+
+lemma ordertype_pred_Pair_eq:
+     "[| a:A;  b:B;  well_ord(A,r);  well_ord(B,s) |] ==>            
+         ordertype(pred(A*B, <a,b>, rmult(A,r,B,s)), rmult(A,r,B,s)) =  
+         ordertype(pred(A,a,r)*B + pred(B,b,s),                         
+                  radd(A*B, rmult(A,r,B,s), B, s))"
+apply (simp (no_asm_simp) add: pred_Pair_eq)
+apply (rule ordertype_eq [symmetric])
+apply (rule prod_sum_singleton_ord_iso)
+apply (simp_all add: pred_subset well_ord_rmult [THEN well_ord_subset])
+apply (blast intro: pred_subset well_ord_rmult [THEN well_ord_subset] 
+             elim!: predE)
+done
+
+lemma ordertype_pred_Pair_lemma: 
+    "[| i'<i;  j'<j |]
+     ==> ordertype(pred(i*j, <i',j'>, rmult(i,Memrel(i),j,Memrel(j))),  
+                   rmult(i,Memrel(i),j,Memrel(j))) =                    
+         raw_oadd (j**i', j')"
+apply (unfold raw_oadd_def omult_def)
+apply (simp (no_asm_simp) add: ordertype_pred_Pair_eq lt_pred_Memrel ltD lt_Ord2 well_ord_Memrel)
+apply (rule trans)
+apply (rule_tac [2] ordertype_ord_iso [THEN sum_ord_iso_cong, THEN ordertype_eq])
+apply (rule_tac [3] ord_iso_refl)
+apply (rule id_bij [THEN ord_isoI, THEN ordertype_eq])
+apply (elim SigmaE sumE ltE ssubst)
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel
+                     Ord_ordertype lt_Ord lt_Ord2) 
+apply (blast intro: Ord_trans)+
+done
+
+lemma lt_omult: 
+ "[| Ord(i);  Ord(j);  k<j**i |]
+  ==> EX j' i'. k = j**i' ++ j' & j'<j & i'<i"
+apply (unfold omult_def)
+apply (simp add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel)
+apply (safe elim!: ltE)
+apply (simp add: ordertype_pred_Pair_lemma ltI raw_oadd_eq_oadd 
+            omult_def [symmetric] Ord_in_Ord' [of _ i] Ord_in_Ord' [of _ j])
+apply (blast intro: ltI)
+done
+
+lemma omult_oadd_lt: 
+     "[| j'<j;  i'<i |] ==> j**i' ++ j'  <  j**i"
+apply (unfold omult_def)
+apply (rule ltI)
+ prefer 2
+ apply (simp add: Ord_ordertype well_ord_rmult well_ord_Memrel lt_Ord2)
+apply (simp (no_asm_simp) add: ordertype_pred_unfold well_ord_rmult well_ord_Memrel lt_Ord2)
+apply (rule bexI)
+prefer 2 apply (blast elim!: ltE)
+apply (simp add: ordertype_pred_Pair_lemma ltI omult_def [symmetric])
+apply (simp add: lt_Ord lt_Ord2 raw_oadd_eq_oadd)
+done
+
+lemma omult_unfold:
+     "[| Ord(i);  Ord(j) |] ==> j**i = (UN j':j. UN i':i. {j**i' ++ j'})"
+apply (rule subsetI [THEN equalityI])
+apply (rule lt_omult [THEN exE])
+apply (erule_tac [3] ltI)
+apply (simp_all add: Ord_omult) 
+apply (blast elim!: ltE)
+apply (blast intro: omult_oadd_lt [THEN ltD] ltI)
+done
+
+(*** Basic laws for ordinal multiplication ***)
+
+(** Ordinal multiplication by zero **)
+
+lemma omult_0 [simp]: "i**0 = 0"
+apply (unfold omult_def)
+apply (simp (no_asm_simp))
+done
+
+lemma omult_0_left [simp]: "0**i = 0"
+apply (unfold omult_def)
+apply (simp (no_asm_simp))
+done
+
+(** Ordinal multiplication by 1 **)
+
+lemma omult_1 [simp]: "Ord(i) ==> i**1 = i"
+apply (unfold omult_def)
+apply (rule_tac s1="Memrel(i)" 
+       in ord_isoI [THEN ordertype_eq, THEN trans])
+apply (rule_tac c = snd and d = "%z.<0,z>"  in lam_bijective)
+apply (auto elim!: snd_type well_ord_Memrel ordertype_Memrel)
+done
+
+lemma omult_1_left [simp]: "Ord(i) ==> 1**i = i"
+apply (unfold omult_def)
+apply (rule_tac s1="Memrel(i)" 
+       in ord_isoI [THEN ordertype_eq, THEN trans])
+apply (rule_tac c = fst and d = "%z.<z,0>" in lam_bijective)
+apply (auto elim!: fst_type well_ord_Memrel ordertype_Memrel)
+done
+
+(** Distributive law for ordinal multiplication and addition **)
+
+lemma oadd_omult_distrib:
+     "[| Ord(i);  Ord(j);  Ord(k) |] ==> i**(j++k) = (i**j)++(i**k)"
+apply (simp add: oadd_eq_if_raw_oadd)
+apply (simp add: omult_def raw_oadd_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule prod_ord_iso_cong [OF ordertype_ord_iso [THEN ord_iso_sym] 
+                                  ord_iso_refl])
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
+                     Ord_ordertype)
+apply (rule sum_prod_distrib_ord_iso [THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] sum_ord_iso_cong [OF ordertype_ord_iso ordertype_ord_iso])
+apply (simp_all add: well_ord_rmult well_ord_radd well_ord_Memrel 
+                     Ord_ordertype)
+done
+
+lemma omult_succ: "[| Ord(i);  Ord(j) |] ==> i**succ(j) = (i**j)++i"
+by (simp del: oadd_succ add: oadd_1 [of j, symmetric] oadd_omult_distrib)
+
+(** Associative law **)
+
+lemma omult_assoc: 
+    "[| Ord(i);  Ord(j);  Ord(k) |] ==> (i**j)**k = i**(j**k)"
+apply (unfold omult_def)
+apply (rule ordertype_eq [THEN trans])
+apply (rule prod_ord_iso_cong [OF ord_iso_refl 
+                                  ordertype_ord_iso [THEN ord_iso_sym]])
+apply (blast intro: well_ord_rmult well_ord_Memrel)+
+apply (rule prod_assoc_ord_iso [THEN ord_iso_sym, THEN ordertype_eq, THEN trans])
+apply (rule_tac [2] ordertype_eq)
+apply (rule_tac [2] prod_ord_iso_cong [OF ordertype_ord_iso ord_iso_refl])
+apply (blast intro: well_ord_rmult well_ord_Memrel Ord_ordertype)+
+done
+
+
+(** Ordinal multiplication with limit ordinals **)
+
+lemma omult_UN: 
+     "[| Ord(i);  !!x. x:A ==> Ord(j(x)) |]
+      ==> i ** (UN x:A. j(x)) = (UN x:A. i**j(x))"
+by (simp (no_asm_simp) add: Ord_UN omult_unfold, blast)
+
+lemma omult_Limit: "[| Ord(i);  Limit(j) |] ==> i**j = (UN k:j. i**k)"
+by (simp add: Limit_is_Ord [THEN Ord_in_Ord] omult_UN [symmetric] 
+              Union_eq_UN [symmetric] Limit_Union_eq)
+
+
+(*** Ordering/monotonicity properties of ordinal multiplication ***)
+
+(*As a special case we have "[| 0<i;  0<j |] ==> 0 < i**j" *)
+lemma lt_omult1: "[| k<i;  0<j |] ==> k < i**j"
+apply (safe elim!: ltE intro!: ltI Ord_omult)
+apply (force simp add: omult_unfold)
+done
+
+lemma omult_le_self: "[| Ord(i);  0<j |] ==> i le i**j"
+by (blast intro: all_lt_imp_le Ord_omult lt_omult1 lt_Ord2)
+
+lemma omult_le_mono1: "[| k le j;  Ord(i) |] ==> k**i le j**i"
+apply (frule lt_Ord)
+apply (frule le_Ord2)
+apply (erule trans_induct3)
+apply (simp (no_asm_simp) add: le_refl Ord_0)
+apply (simp (no_asm_simp) add: omult_succ oadd_le_mono)
+apply (simp (no_asm_simp) add: omult_Limit)
+apply (rule le_implies_UN_le_UN, blast)
+done
+
+lemma omult_lt_mono2: "[| k<j;  0<i |] ==> i**k < i**j"
+apply (rule ltI)
+apply (simp (no_asm_simp) add: omult_unfold lt_Ord2)
+apply (safe elim!: ltE intro!: Ord_omult)
+apply (force simp add: Ord_omult)
+done
+
+lemma omult_le_mono2: "[| k le j;  Ord(i) |] ==> i**k le i**j"
+apply (rule subset_imp_le)
+apply (safe elim!: ltE dest!: Ord_succD intro!: Ord_omult)
+apply (simp add: omult_unfold)
+apply (blast intro: Ord_trans) 
+done
+
+lemma omult_le_mono: "[| i' le i;  j' le j |] ==> i'**j' le i**j"
+by (blast intro: le_trans omult_le_mono1 omult_le_mono2 Ord_succD elim: ltE)
+
+lemma omult_lt_mono: "[| i' le i;  j'<j;  0<i |] ==> i'**j' < i**j"
+by (blast intro: lt_trans1 omult_le_mono1 omult_lt_mono2 Ord_succD elim: ltE)
+
+lemma omult_le_self2: "[| Ord(i);  0<j |] ==> i le j**i"
+apply (frule lt_Ord2)
+apply (erule_tac i = i in trans_induct3)
+apply (simp (no_asm_simp))
+apply (simp (no_asm_simp) add: omult_succ)
+apply (erule lt_trans1)
+apply (rule_tac b = "j**x" in oadd_0 [THEN subst], rule_tac [2] oadd_lt_mono2)
+apply (blast intro: Ord_omult, assumption)
+apply (simp (no_asm_simp) add: omult_Limit)
+apply (rule le_trans)
+apply (rule_tac [2] le_implies_UN_le_UN)
+prefer 2 apply blast
+apply (simp (no_asm_simp) add: Union_eq_UN [symmetric] Limit_Union_eq Limit_is_Ord)
+done
+
+
+(** Further properties of ordinal multiplication **)
+
+lemma omult_inject: "[| i**j = i**k;  0<i;  Ord(j);  Ord(k) |] ==> j=k"
+apply (rule Ord_linear_lt)
+prefer 4 apply assumption
+apply auto 
+apply (force dest: omult_lt_mono2 simp add: lt_not_refl)+
+done
+
+ML {*
+val ordermap_def = thm "ordermap_def";
+val ordertype_def = thm "ordertype_def";
+val Ord_alt_def = thm "Ord_alt_def";
+val ordify_def = thm "ordify_def";
+
+val Ord_in_Ord' = thm "Ord_in_Ord'";
+val le_well_ord_Memrel = thm "le_well_ord_Memrel";
+val well_ord_Memrel = thm "well_ord_Memrel";
+val lt_pred_Memrel = thm "lt_pred_Memrel";
+val pred_Memrel = thm "pred_Memrel";
+val Ord_iso_implies_eq_lemma = thm "Ord_iso_implies_eq_lemma";
+val Ord_iso_implies_eq = thm "Ord_iso_implies_eq";
+val ordermap_type = thm "ordermap_type";
+val ordermap_eq_image = thm "ordermap_eq_image";
+val ordermap_pred_unfold = thm "ordermap_pred_unfold";
+val ordermap_unfold = thm "ordermap_unfold";
+val Ord_ordermap = thm "Ord_ordermap";
+val Ord_ordertype = thm "Ord_ordertype";
+val ordermap_mono = thm "ordermap_mono";
+val converse_ordermap_mono = thm "converse_ordermap_mono";
+val ordermap_surj = thm "ordermap_surj";
+val ordermap_bij = thm "ordermap_bij";
+val ordertype_ord_iso = thm "ordertype_ord_iso";
+val ordertype_eq = thm "ordertype_eq";
+val ordertype_eq_imp_ord_iso = thm "ordertype_eq_imp_ord_iso";
+val le_ordertype_Memrel = thm "le_ordertype_Memrel";
+val ordertype_Memrel = thm "ordertype_Memrel";
+val ordertype_0 = thm "ordertype_0";
+val bij_ordertype_vimage = thm "bij_ordertype_vimage";
+val ordermap_pred_eq_ordermap = thm "ordermap_pred_eq_ordermap";
+val ordertype_unfold = thm "ordertype_unfold";
+val ordertype_pred_subset = thm "ordertype_pred_subset";
+val ordertype_pred_lt = thm "ordertype_pred_lt";
+val ordertype_pred_unfold = thm "ordertype_pred_unfold";
+val Ord_is_Ord_alt = thm "Ord_is_Ord_alt";
+val Ord_alt_is_Ord = thm "Ord_alt_is_Ord";
+val bij_sum_0 = thm "bij_sum_0";
+val ordertype_sum_0_eq = thm "ordertype_sum_0_eq";
+val bij_0_sum = thm "bij_0_sum";
+val ordertype_0_sum_eq = thm "ordertype_0_sum_eq";
+val pred_Inl_bij = thm "pred_Inl_bij";
+val ordertype_pred_Inl_eq = thm "ordertype_pred_Inl_eq";
+val pred_Inr_bij = thm "pred_Inr_bij";
+val ordertype_pred_Inr_eq = thm "ordertype_pred_Inr_eq";
+val Ord_ordify = thm "Ord_ordify";
+val ordify_idem = thm "ordify_idem";
+val Ord_raw_oadd = thm "Ord_raw_oadd";
+val Ord_oadd = thm "Ord_oadd";
+val raw_oadd_0 = thm "raw_oadd_0";
+val oadd_0 = thm "oadd_0";
+val raw_oadd_0_left = thm "raw_oadd_0_left";
+val oadd_0_left = thm "oadd_0_left";
+val oadd_eq_if_raw_oadd = thm "oadd_eq_if_raw_oadd";
+val raw_oadd_eq_oadd = thm "raw_oadd_eq_oadd";
+val lt_oadd1 = thm "lt_oadd1";
+val oadd_le_self = thm "oadd_le_self";
+val id_ord_iso_Memrel = thm "id_ord_iso_Memrel";
+val ordertype_sum_Memrel = thm "ordertype_sum_Memrel";
+val oadd_lt_mono2 = thm "oadd_lt_mono2";
+val oadd_lt_cancel2 = thm "oadd_lt_cancel2";
+val oadd_lt_iff2 = thm "oadd_lt_iff2";
+val oadd_inject = thm "oadd_inject";
+val lt_oadd_disj = thm "lt_oadd_disj";
+val oadd_assoc = thm "oadd_assoc";
+val oadd_unfold = thm "oadd_unfold";
+val oadd_1 = thm "oadd_1";
+val oadd_succ = thm "oadd_succ";
+val oadd_UN = thm "oadd_UN";
+val oadd_Limit = thm "oadd_Limit";
+val oadd_le_self2 = thm "oadd_le_self2";
+val oadd_le_mono1 = thm "oadd_le_mono1";
+val oadd_lt_mono = thm "oadd_lt_mono";
+val oadd_le_mono = thm "oadd_le_mono";
+val oadd_le_iff2 = thm "oadd_le_iff2";
+val bij_sum_Diff = thm "bij_sum_Diff";
+val ordertype_sum_Diff = thm "ordertype_sum_Diff";
+val Ord_odiff = thm "Ord_odiff";
+val raw_oadd_ordertype_Diff = thm "raw_oadd_ordertype_Diff";
+val oadd_odiff_inverse = thm "oadd_odiff_inverse";
+val odiff_oadd_inverse = thm "odiff_oadd_inverse";
+val odiff_lt_mono2 = thm "odiff_lt_mono2";
+val Ord_omult = thm "Ord_omult";
+val pred_Pair_eq = thm "pred_Pair_eq";
+val ordertype_pred_Pair_eq = thm "ordertype_pred_Pair_eq";
+val ordertype_pred_Pair_lemma = thm "ordertype_pred_Pair_lemma";
+val lt_omult = thm "lt_omult";
+val omult_oadd_lt = thm "omult_oadd_lt";
+val omult_unfold = thm "omult_unfold";
+val omult_0 = thm "omult_0";
+val omult_0_left = thm "omult_0_left";
+val omult_1 = thm "omult_1";
+val omult_1_left = thm "omult_1_left";
+val oadd_omult_distrib = thm "oadd_omult_distrib";
+val omult_succ = thm "omult_succ";
+val omult_assoc = thm "omult_assoc";
+val omult_UN = thm "omult_UN";
+val omult_Limit = thm "omult_Limit";
+val lt_omult1 = thm "lt_omult1";
+val omult_le_self = thm "omult_le_self";
+val omult_le_mono1 = thm "omult_le_mono1";
+val omult_lt_mono2 = thm "omult_lt_mono2";
+val omult_le_mono2 = thm "omult_le_mono2";
+val omult_le_mono = thm "omult_le_mono";
+val omult_lt_mono = thm "omult_lt_mono";
+val omult_le_self2 = thm "omult_le_self2";
+val omult_inject = thm "omult_inject";
+*}
 
 end