# HG changeset patch
# User lcp
# Date 787935532 -3600
# Node ID a32b420c33d44aef3c4756caeb4568f8541a5457
# Parent  4a266c3d4cc0f4f3af74dd1cdfadd358bc617499
Moved well_ord_Memrel, lt_eq_pred, Ord_iso_implies_eq_lemma,
Ord_iso_implies_eq to top of file, as they do not require the other
material.  Simplified proof of ordertype_subset.

Proved ordertype_eq: a short proof using deepen_tac!  Deleted
bij_ordermap_vimage and ordermap_Memrel
    "bij_ordermap_vimage and ordermap_Memrelf. [| f: bij(A,B);  well_ord(B,r);  x:A |] ==>\
\         ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";
    "\         ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";i. [| Ord(i);  j:i |] ==> ordermap(i,Memrel(i)) ` j = j"
because ordertype_eq serves the same purpose.  Proofs of bij_ordertype_vimage
and ordertype_Memrel are now trivial.

diff -r 4a266c3d4cc0 -r a32b420c33d4 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Tue Dec 20 13:24:04 1994 +0100
+++ b/src/ZF/OrderType.ML	Tue Dec 20 15:58:52 1994 +0100
@@ -3,12 +3,53 @@
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-For OrderType.thy.  Order types in Zermelo-Fraenkel Set Theory 
+Order types in Zermelo-Fraenkel Set Theory 
 *)
 
 
 open OrderType;
 
+(*** Proofs needing the combination of Ordinal.thy and Order.thy ***)
+
+goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
+by (rtac well_ordI 1);
+by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
+by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
+by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
+by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
+qed "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 OrderType.thy [pred_def, lt_def]
+    "!!i j. j<i ==> j = pred(i, j, Memrel(i))";
+by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
+by (fast_tac (eq_cs addEs [Ord_trans]) 1);
+qed "lt_eq_pred";
+
+goal OrderType.thy
+    "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j)) |] ==> R";
+by (forward_tac [lt_eq_pred] 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 (etac subst 1);
+by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
+(*Combining the two simplifications causes looping*)
+by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
+by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
+qed "Ord_iso_implies_eq_lemma";
+
+(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
+goal OrderType.thy
+    "!!i. [| 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 OrderType.thy [ordermap_def,ordertype_def]
     "ordermap(A,r) : A -> ordertype(A,r)";
 by (rtac lam_type 1);
@@ -110,6 +151,8 @@
 by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
 qed "ordermap_bij";
 
+(** Isomorphisms involving ordertype **)
+
 goalw OrderType.thy [ord_iso_def]
  "!!r. well_ord(A,r) ==> \
 \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
@@ -122,6 +165,16 @@
 			    ordermap_type RS apply_type]) 1);
 qed "ordertype_ord_iso";
 
+goal OrderType.thy
+    "!!f. [| f: ord_iso(A,r,B,s);  well_ord(B,s) |] ==>	\
+\    ordertype(A,r) = ordertype(B,s)";
+by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1);
+by (resolve_tac [Ord_iso_implies_eq] 1
+    THEN REPEAT (eresolve_tac [Ord_ordertype] 1));
+by (deepen_tac (ZF_cs addIs [ord_iso_trans, ord_iso_sym]
+                    addSEs [ordertype_ord_iso]) 0 1);
+qed "ordertype_eq";
+
 
 (** Unfolding of ordertype **)
 
@@ -130,62 +183,17 @@
 by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
 qed "ordertype_unfold";
 
-
-(** Ordertype of Memrel **)
-
-(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
-goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
-by (rtac well_ordI 1);
-by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
-by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
-by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
-by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
-qed "well_ord_Memrel";
-
-goal OrderType.thy "!!i. [| Ord(i);  j:i |] ==> ordermap(i,Memrel(i)) ` j = j";
-by (etac Ord_induct 1);
-by (assume_tac 1);
-by (asm_simp_tac (ZF_ss addsimps
-	     [well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1);
-by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1);
-by (dtac OrdmemD 1);
-by (assume_tac 1);
-by (fast_tac eq_cs 1);
-qed "ordermap_Memrel";
-
+(*Ordertype of Memrel*)
 goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
-by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1);
+by (resolve_tac [Ord_iso_implies_eq RS sym] 1);
+by (resolve_tac [ordertype_ord_iso] 3);
+by (REPEAT (ares_tac [well_ord_Memrel, Ord_ordertype] 1));
 qed "ordertype_Memrel";
 
-(** Ordertype of rvimage **)
+(*Ordertype of rvimage*)
+bind_thm ("bij_ordertype_vimage", ord_iso_rvimage RS ordertype_eq);
 
-goal OrderType.thy
-    "!!f. [| f: bij(A,B);  well_ord(B,r);  x:A |] ==>	\
-\         ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";
-by (metacut_tac well_ord_rvimage 1 THEN 
-    etac bij_is_inj 2 THEN assume_tac 2);
-by (res_inst_tac [("A","A"), ("a","x")] wf_on_induct 1 THEN
-    REPEAT (ares_tac [well_ord_is_wf] 1));
-by (asm_simp_tac
-    (bij_inverse_ss addsimps [ordermap_pred_unfold, well_ord_is_wf]) 1);
-by (asm_simp_tac (ZF_ss addsimps [pred_def, rvimage_iff]) 1);
-by (safe_tac eq_cs);
-by (fast_tac bij_apply_cs 1);
-by (res_inst_tac [("a", "converse(f)`xb")] RepFun_eqI 1);
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "bij_ordermap_vimage";
-
-goal OrderType.thy
-    "!!f. [| f: bij(A,B);  well_ord(B,r) |] ==>	\
-\    ordertype(A,rvimage(A,f,r)) = ordertype(B,r)";
-by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, bij_ordermap_vimage]) 1);
-by (safe_tac eq_cs);
-by (fast_tac bij_apply_cs 1);
-by (res_inst_tac [("a", "converse(f)`xa")] RepFun_eqI 1);
-by (ALLGOALS (asm_simp_tac bij_inverse_ss));
-qed "bij_ordertype_vimage";
-
-
+(*Ordermap returns the same result if applied to an initial segment*)
 goal OrderType.thy
     "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>	\
 \	  ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
@@ -202,48 +210,15 @@
 by (fast_tac (eq_cs addSEs [trans_onD]) 1);
 qed "ordermap_pred_eq_ordermap";
 
-
+(*Lemma for proving there exist ever larger cardinals*)
 goal OrderType.thy
     "!!r. [| well_ord(A,r);  i: ordertype(A,r) |] ==>	\
 \	  EX B. B<=A & i = ordertype(B,r)";
 by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1);
-by (res_inst_tac [("x", "pred(A, converse(ordermap(A,r))`i, r)")]  exI  1);
-by (safe_tac (ZF_cs addSEs [predE]));
-by (asm_simp_tac (ZF_ss addsimps [ordermap_bij RS left_inverse_bij]) 1);
-by (asm_simp_tac (ZF_ss addsimps
-		  [well_ord_is_wf RS ordermap_pred_unfold]) 1);
-by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
-				  ordermap_pred_eq_ordermap]) 1);
+by (etac RepFunE 1);
+by (res_inst_tac [("x", "pred(A,y,r)")] exI 1);
+by (asm_simp_tac
+    (ZF_ss addsimps [pred_subset, well_ord_is_wf RS ordermap_pred_unfold, 
+		     ordertype_unfold, ordermap_pred_eq_ordermap]) 1);
 qed "ordertype_subset";
 
-
-(*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 OrderType.thy [pred_def, lt_def]
-    "!!i j. j<i ==> j = pred(i, j, Memrel(i))";
-by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
-by (fast_tac (eq_cs addEs [Ord_trans]) 1);
-qed "lt_eq_pred";
-
-goal OrderType.thy
-    "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j))	\
-\         |] ==> R";
-by (forward_tac [lt_eq_pred] 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 (etac subst 1);
-by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
-(*Combining the two simplifications causes looping*)
-by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
-by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]  
-                    addEs  [Ord_trans]) 1);
-qed "Ord_iso_implies_eq_lemma";
-
-(*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
-goal OrderType.thy
-    "!!i. [| 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";