# HG changeset patch
# User lcp
# Date 774029103 -7200
# Node ID 92868dab2939064e9391a2f455c108b63aa3f107
# Parent  08d1cce222e1be1833bddecc073715e6da68530a
new cardinal arithmetic developments

diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Cardinal.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -181,7 +181,7 @@
 by (rtac LeastI 1);
 by (etac Ord_ordertype 2);
 by (rtac exI 1);
-by (etac (ordertype_bij RS bij_converse_bij) 1);
+by (etac (ordermap_bij RS bij_converse_bij) 1);
 val well_ord_cardinal_eqpoll = result();
 
 val Ord_cardinal_eqpoll = well_ord_Memrel RS well_ord_cardinal_eqpoll 
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -8,6 +8,27 @@
 
 open CardinalArith;
 
+goalw CardinalArith.thy [jump_cardinal_def]
+    "Ord(jump_cardinal(K))";
+by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+
+bw Transset_def;
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+br (ordertype_subset RS exE) 1;
+ba 1;
+ba 1;
+by (safe_tac (ZF_cs addSIs [Ord_ordertype]));
+fr UN_I;
+br ReplaceI 2;
+by (fast_tac ZF_cs 4);
+by (fast_tac ZF_cs 1);
+
+(****************************************************************)
+
+
+
+
 (*Use AC to discharge first premise*)
 goal CardinalArith.thy
     "!!A B. [| well_ord(B,r);  A lepoll B |] ==> |A| le |B|";
@@ -341,7 +362,7 @@
     "!!A. [| well_ord(A,r);  x:A |] ==> ordermap(A,r)`x eqpoll pred(A,x,r)";
 by (rtac exI 1);
 by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, well_ord_is_wf]) 1);
-by (etac (ordertype_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
+by (etac (ordermap_bij RS bij_is_inj RS restrict_bij RS bij_converse_bij) 1);
 by (rtac pred_subset 1);
 val ordermap_eqpoll_pred = result();
 
@@ -420,7 +441,7 @@
 by (etac (InfCard_is_Card RS Card_is_Ord RS well_ord_csquare) 2);
 by (fast_tac (ZF_cs addSIs [Un_least_lt, InfCard_is_Limit, Limit_has_succ]) 2);
 by (rtac (OrdmemD RS subset_imp_lepoll) 1);
-by (res_inst_tac [("z1","z")] (csquare_ltI RS less_imp_ordermap_in) 1);
+by (res_inst_tac [("z1","z")] (csquare_ltI RS ordermap_mono) 1);
 by (etac well_ord_is_wf 4);
 by (ALLGOALS 
     (fast_tac (ZF_cs addSIs [Un_upper1_le, Un_upper2_le, Ord_ordermap] 
@@ -487,7 +508,7 @@
 by (rtac cardinal_cong 1);
 by (rewtac eqpoll_def);
 by (rtac exI 1);
-by (etac (well_ord_csquare RS ordertype_bij) 1);
+by (etac (well_ord_csquare RS ordermap_bij) 1);
 val csquare_eq_ordertype = result();
 
 (*Main result: Kunen's Theorem 10.12*)
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/CardinalArith.thy	Tue Jul 12 18:05:03 1994 +0200
@@ -8,6 +8,8 @@
 
 CardinalArith = Cardinal + OrderArith + Arith + 
 consts
+  jump_cardinal :: "i=>i"
+
   InfCard     :: "i=>o"
   "|*|"       :: "[i,i]=>i"       (infixl 70)
   "|+|"       :: "[i,i]=>i"       (infixl 65)
@@ -15,6 +17,11 @@
 
 rules
 
+  jump_cardinal_def
+      "jump_cardinal(K) ==   \
+\         UN X:Pow(K). {z. r: Pow(X*X), well_ord(X,r) & z = ordertype(X,r)}"
+
+
   InfCard_def  "InfCard(i) == Card(i) & nat le i"
 
   cadd_def     "i |+| j == | i+j |"
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/Makefile
--- a/src/ZF/Makefile	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Makefile	Tue Jul 12 18:05:03 1994 +0200
@@ -24,7 +24,7 @@
 	ind_syntax.ML intr_elim.ML indrule.ML inductive.ML coinductive.ML \
 	equalities.ML Perm.thy Perm.ML Rel.thy Rel.ML Trancl.thy Trancl.ML \
 	WF.thy WF.ML Order.thy Order.ML Ordinal.thy Ordinal.ML \
-	OrderType.thy OrderType.ML OrderArith.thy OrderArith.ML \
+	OrderArith.thy OrderArith.ML OrderType.thy OrderType.ML \
 	Cardinal.thy Cardinal.ML CardinalArith.thy CardinalArith.ML \
 	Nat.thy Nat.ML \
 	Epsilon.thy Epsilon.ML Arith.thy Arith.ML Univ.thy Univ.ML \
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/Order.ML
--- a/src/ZF/Order.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/Order.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -164,6 +164,11 @@
 by (safe_tac ZF_cs);
 val well_ord_is_wf = result();
 
+goalw Order.thy [well_ord_def, tot_ord_def, part_ord_def]
+    "!!r. well_ord(A,r) ==> trans[A](r)";
+by (safe_tac ZF_cs);
+val well_ord_is_trans_on = result();
+
 
 (*** Derived rules for pred(A,x,r) ***)
 
@@ -180,3 +185,12 @@
 goalw Order.thy [pred_def] "pred(A,x,r) <= A";
 by (fast_tac ZF_cs 1);
 val pred_subset = result();
+
+goalw Order.thy [pred_def] "y : pred(A,x,r) <-> <y,x>:r & y:A";
+by (fast_tac ZF_cs 1);
+val pred_iff = result();
+
+goalw Order.thy [pred_def]
+    "pred(pred(A,x,r), y, r) = pred(A,x,r) Int pred(A,y,r)";
+by (fast_tac eq_cs 1);
+val pred_pred_eq = result();
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -7,15 +7,6 @@
 *)
 
 
-(*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));;
-val well_ord_Memrel = result();
-
 open OrderType;
 
 goalw OrderType.thy [ordermap_def,ordertype_def]
@@ -38,6 +29,7 @@
                                   vimage_singleton_iff]) 1);
 val ordermap_eq_image = result();
 
+(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
 goal OrderType.thy 
     "!!r. [| wf[A](r);  x:A |] ==> \
 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
@@ -87,7 +79,7 @@
 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
 by (assume_tac 1);
 by (fast_tac ZF_cs 1);
-val less_imp_ordermap_in = result();
+val ordermap_mono = result();
 
 (*linearity of r is crucial here*)
 goalw OrderType.thy [well_ord_def, tot_ord_def]
@@ -96,11 +88,11 @@
 by (safe_tac ZF_cs);
 by (linear_case_tac 1);
 by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
-by (dtac less_imp_ordermap_in 1);
+by (dtac ordermap_mono 1);
 by (REPEAT_SOME assume_tac);
 by (etac mem_asym 1);
 by (assume_tac 1);
-val ordermap_in_imp_less = result();
+val converse_ordermap_mono = result();
 
 val ordermap_surj = 
     (ordermap_type RS surj_image) |>
@@ -114,20 +106,20 @@
 by (rtac ordermap_surj 2);
 by (linear_case_tac 1);
 (*The two cases yield similar contradictions*)
-by (ALLGOALS (dtac less_imp_ordermap_in));
+by (ALLGOALS (dtac ordermap_mono));
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
-val ordertype_bij = result();
+val ordermap_bij = result();
 
 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)))";
 by (safe_tac ZF_cs);
-by (rtac ordertype_bij 1);
+by (rtac ordermap_bij 1);
 by (assume_tac 1);
-by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
+by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
 by (rewtac well_ord_def);
-by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
+by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
 			    ordermap_type RS apply_type]) 1);
 val ordertype_ord_iso = result();
 
@@ -138,3 +130,90 @@
     "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
 by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
 val ordertype_unfold = result();
+
+
+(** 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));;
+val well_ord_Memrel = result();
+
+goal OrderType.thy "!!i. [| Ord(i);  j:i |] ==> ordermap(i,Memrel(i)) ` j = j";
+by (eresolve_tac [Ord_induct] 1);
+ba 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 (dresolve_tac [OrdmemD] 1);
+by (assume_tac 1);
+by (fast_tac eq_cs 1);
+val ordermap_Memrel = result();
+
+goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1);
+val ordertype_Memrel = result();
+
+(** Ordertype of rvimage **)
+
+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));
+val bij_ordermap_vimage = result();
+
+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));
+val bij_ordertype_vimage = result();
+
+
+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";
+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 (ZF_cs addSEs [predE]));
+by (asm_simp_tac
+    (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
+(*combining these two simplifications LOOPS! *)
+by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
+br (refl RSN (2,RepFun_cong)) 1;
+bd well_ord_is_trans_on 1;
+by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+val ordermap_pred_eq_ordermap = result();
+
+
+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);
+val ordertype_subset = result();
+
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/OrderType.thy
--- a/src/ZF/OrderType.thy	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.thy	Tue Jul 12 18:05:03 1994 +0200
@@ -8,7 +8,7 @@
 The order type of a well-ordering is the least ordinal isomorphic to it.
 *)
 
-OrderType = Order + Ordinal + 
+OrderType = OrderArith + Ordinal + 
 consts
   ordermap  :: "[i,i]=>i"
   ordertype :: "[i,i]=>i"
diff -r 08d1cce222e1 -r 92868dab2939 src/ZF/simpdata.ML
--- a/src/ZF/simpdata.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/simpdata.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -19,6 +19,10 @@
    "<a,b>: Sigma(A,B) <-> a:A & b:B(a)",
    "a : Collect(A,P)  <-> a:A & P(a)" ];
 
+goal ZF.thy "{x.x:A} = A";
+by (fast_tac eq_cs 1);
+val triv_RepFun = result();
+
 (*INCLUDED: should be??*)
 val bquant_simps = map prove_fun
  [ "(ALL x:0.P(x)) <-> True",
@@ -90,7 +94,8 @@
   end;
 
 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, 
-		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff];
+		beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff,
+		triv_RepFun];
 
 (*Sigma_cong, Pi_cong NOT included by default since they cause
   flex-flex pairs and the "Check your prover" error -- because most