# HG changeset patch
# User paulson
# Date 827855649 -3600
# Node ID 6d7278c3f6868cc1049e2d165a708cfe287795e0
# Parent  ec04389ddcd300f713aa8a3f1624f948469ee408
Moved some proofs to Cardinal.ML; simplified others

diff -r ec04389ddcd3 -r 6d7278c3f686 src/ZF/AC/Cardinal_aux.ML
--- a/src/ZF/AC/Cardinal_aux.ML	Tue Mar 26 16:26:55 1996 +0100
+++ b/src/ZF/AC/Cardinal_aux.ML	Tue Mar 26 16:54:09 1996 +0100
@@ -12,7 +12,19 @@
 (* concerning AC16 and DC                                                 *)
 (* ********************************************************************** *)
 
-val nat_0_in_2 =  Ord_0 RS le_refl RS leI RS ltD;
+(* j=|A| *)
+goal Cardinal.thy
+    "!!A. [| A lepoll i; Ord(i) |] ==> EX j. j le i & A eqpoll j";
+by (fast_tac (ZF_cs addIs [lepoll_cardinal_le, well_ord_Memrel,
+			    well_ord_cardinal_eqpoll RS eqpoll_sym]
+		    addDs [lepoll_well_ord]) 1);
+qed "lepoll_imp_ex_le_eqpoll";
+
+(* j=|A| *)
+goalw Cardinal.thy [lesspoll_def]
+    "!!A a. [| A lesspoll i; Ord(i) |] ==> EX j. j<i & A eqpoll j";
+by (fast_tac (ZF_cs addSDs [lepoll_imp_ex_le_eqpoll] addSEs [leE]) 1);
+qed "lesspoll_imp_ex_lt_eqpoll";
 
 goalw thy [InfCard_def] "!!i. [| ~Finite(i); Ord(i) |] ==> InfCard(|i|)";
 by (rtac conjI 1);
@@ -23,21 +35,6 @@
     THEN REPEAT (assume_tac 1));
 val Inf_Ord_imp_InfCard_cardinal = result();
 
-goalw thy [lepoll_def] "A Un B lepoll A+B";
-by (res_inst_tac [("x","lam x: A Un B. if (x:A,Inl(x),Inr(x))")] exI 1);
-by (res_inst_tac [("d","%z. snd(z)")] lam_injective 1);
-by (split_tac [expand_if] 1);
-by (fast_tac (AC_cs addSIs [InlI, InrI]) 1);
-by (split_tac [expand_if] 1);
-by (asm_full_simp_tac (AC_ss addsimps [Inl_def, Inr_def]) 1);
-val Un_lepoll_sum = result();
-
-goalw thy [sum_def] "A+A = 2*A";
-by (fast_tac (AC_cs addIs [equalityI]
-        addSIs [singletonI, nat_0_in_2, succI1]
-        addSEs [succE, singletonE]) 1);
-val sum_eq_2_times = result();
-
 val sum_lepoll_prod = [sum_eq_2_times RS equalityD1 RS subset_imp_lepoll,
         asm_rl, lepoll_refl] MRS (prod_lepoll_mono RSN (2, lepoll_trans))
         |> standard;
@@ -231,103 +228,6 @@
 val lepoll_imp_eqpoll_subset = result();
 
 (* ********************************************************************** *)
-(* Some other lemmas                                                      *)
-(* ********************************************************************** *)
-
-goal thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
-by (rtac eqpoll_trans 1);
-by (eresolve_tac [nat_implies_well_ord RS (
-                  nat_implies_well_ord RSN (2,
-                  well_ord_radd RS well_ord_cardinal_eqpoll)) RS eqpoll_sym] 1 
-    THEN (assume_tac 1));
-by (eresolve_tac [nat_cadd_eq_add RS subst] 1 THEN (assume_tac 1));
-by (asm_full_simp_tac (AC_ss addsimps [cadd_def, eqpoll_refl]) 1);
-val nat_sum_eqpoll_sum = result();
-
-val eqpoll_ordertype =
-        ordermap_bij RS (exI RS (eqpoll_def RS (def_imp_iff RS iffD2)));
-
-goalw thy [lesspoll_def]
-        "!!a. [| b lesspoll a; well_ord(a,r); well_ord(b,s) |]  \
-\               ==> ordertype(b,s) < ordertype(a,r)";
-by (forw_inst_tac [("A2","b")]
-        ([Ord_ordertype, Ord_ordertype] MRS Ord_linear) 1
-        THEN REPEAT (assume_tac 1));
-by (etac disjE 1);
-by (etac ltI 1);
-by (etac Ord_ordertype 1);
-by (etac disjE 1);
-by (REPEAT (eresolve_tac [conjE,notE] 1));
-by (resolve_tac [exI RS (eqpoll_def RS (def_imp_iff RS iffD2))] 1);
-by (eresolve_tac [ordermap_bij RS comp_bij] 1);
-by (etac ssubst 1);
-by (eresolve_tac [ordermap_bij RS bij_converse_bij] 1);
-by (REPEAT (eresolve_tac [conjE,notE] 1));
-by (etac eqpollI 1);
-by (resolve_tac [Ord_ordertype RSN (2, OrdmemD RS subset_imp_lepoll) RSN (2, 
-                 eqpoll_ordertype RS eqpoll_imp_lepoll RS (
-                 eqpoll_ordertype RS eqpoll_sym RS eqpoll_imp_lepoll RSN (3, 
-                 lepoll_trans RS lepoll_trans)))] 1 
-    THEN (REPEAT (assume_tac 1)));
-val lesspoll_ordertype_lt = result();
-
-goalw thy [lesspoll_def] "!!A. A lesspoll B ==> A lepoll B";
-by (fast_tac AC_cs 1);
-val lesspoll_imp_lepoll = result();
-
-goalw thy [lepoll_def]
-        "!!A. [| A lepoll B; well_ord(B,r) |] ==> EX s. well_ord(A,s)";
-by (fast_tac (AC_cs addSEs [well_ord_rvimage]) 1);
-val lepoll_well_ord = result();
-
-goal thy "!!A a. [| A lesspoll a; Ord(a) |] ==> EX b. b<a & A eqpoll b";
-by (resolve_tac [well_ord_Memrel RSN (2,
-        lesspoll_imp_lepoll RS lepoll_well_ord) RS exE] 1
-        THEN (REPEAT (assume_tac 1)));
-by (dresolve_tac [well_ord_Memrel RSN (2, lesspoll_ordertype_lt)] 1
-        THEN (REPEAT (assume_tac 1)));
-by (fast_tac (AC_cs addSEs [eqpoll_ordertype]
-                addEs [ordertype_Memrel RS subst]) 1);
-val lesspoll_imp_ex_lt_eqpoll = result();
-
-goalw thy [lesspoll_def] "A lepoll B <-> A lesspoll B | A eqpoll B";
-by (fast_tac (AC_cs addSIs [eqpollI] addSEs [eqpollE]) 1);
-val lepoll_iff_leqpoll = result();
-
-goal thy "!!A. [| A lepoll a; Ord(a) |] ==> EX b. b le a & A eqpoll b";
-by (eresolve_tac [lepoll_iff_leqpoll RS iffD1 RS disjE] 1);
-by (fast_tac (AC_cs addSDs [lesspoll_imp_ex_lt_eqpoll] addSIs [leI]) 1);
-by (fast_tac (AC_cs addSIs [le_refl]) 1);
-val lepoll_imp_ex_le_eqpoll = result();
-
-goal thy "!!m. [| m le n; n:nat |] ==> m:nat";
-by (fast_tac (AC_cs addSDs [nat_succI RS (Ord_nat RSN (2, OrdmemD))]
-        addSEs [ltE]) 1);
-val le_in_nat = result();
-
-goalw thy [Finite_def] "!!A. [| Finite(A); Finite(B) |] ==> Finite(A Un B)";
-by (REPEAT (etac bexE 1));
-by (REPEAT (dtac eqpoll_imp_lepoll 1));
-by (dtac sum_lepoll_mono 1 THEN (assume_tac 1));
-by (dresolve_tac [nat_sum_eqpoll_sum RS eqpoll_imp_lepoll RSN (2, 
-                  Un_lepoll_sum RS lepoll_trans RS lepoll_trans)] 1 
-        THEN (REPEAT (assume_tac 1)));
-by (forw_inst_tac [("n2","na")]
-        (add_type RS nat_into_Ord RSN (2, lepoll_imp_ex_le_eqpoll)) 1 
-        THEN (REPEAT (assume_tac 1)));
-by (fast_tac (AC_cs addSEs [add_type RSN (2, le_in_nat)]) 1);
-val Finite_Un = result();
-
-goal thy "A <= B Un (A - B)";
-by (fast_tac AC_cs 1);
-val subset_Un_Diff = result();
-
-goalw thy [lesspoll_def] "!!a. [| Card(a); i<a |] ==> i lesspoll a";
-by (dresolve_tac [Card_iff_initial RS iffD1] 1);
-by (fast_tac (AC_cs addSEs [leI RS le_imp_lepoll]) 1);
-val lt_Card_imp_lesspoll = result();
-
-(* ********************************************************************** *)
 (* Diff_lesspoll_eqpoll_Card                                              *)
 (* ********************************************************************** *)