# HG changeset patch
# User paulson
# Date 961576473 -7200
# Node ID f713ef362ad075c78a811df44dc8451eb66be113
# Parent  3a0912a127ec839758f667965dcb06a43a3b9469
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite

diff -r 3a0912a127ec -r f713ef362ad0 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Wed Jun 21 10:32:57 2000 +0200
+++ b/src/ZF/Cardinal.ML	Wed Jun 21 10:34:33 2000 +0200
@@ -130,8 +130,8 @@
 qed "eqpoll_0_iff";
 
 Goalw [eqpoll_def] 
-    "[| A eqpoll B;  C eqpoll D;  A Int C = 0;  B Int D = 0 |] ==> \
-\         A Un C eqpoll B Un D";
+    "[| A eqpoll B;  C eqpoll D;  A Int C = 0;  B Int D = 0 |]  \
+\    ==> A Un C eqpoll B Un D";
 by (blast_tac (claset() addIs [bij_disjoint_Un]) 1);
 qed "eqpoll_disjoint_Un";
 
@@ -423,6 +423,22 @@
 by (etac Ord_cardinal_le 1);
 qed "lepoll_cardinal_le";
 
+Goal "[| A lepoll i; Ord(i) |] ==> |A| eqpoll A";
+by (blast_tac (claset() addIs [lepoll_cardinal_le, well_ord_Memrel,
+                                well_ord_cardinal_eqpoll]
+                        addSDs [lepoll_well_ord]) 1);
+qed "lepoll_Ord_imp_eqpoll";
+
+Goalw [lesspoll_def]
+     "[| A lesspoll i; Ord(i) |] ==> |A| eqpoll A";
+by (blast_tac (claset() addIs [lepoll_Ord_imp_eqpoll]) 1);
+qed "lesspoll_imp_eqpoll";
+
+Goalw [lesspoll_def]
+     "[| A lesspoll i; Ord(i) |] ==> |A| eqpoll A";
+by (blast_tac (claset() addIs [lepoll_Ord_imp_eqpoll]) 1);
+qed "lesspoll_imp_eqpoll";
+
 
 (*** The finite cardinals ***)
 
@@ -487,7 +503,7 @@
 (** lepoll, lesspoll and natural numbers **)
 
 Goalw [lesspoll_def]
-      "[| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
+     "[| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
 by (rtac conjI 1);
 by (blast_tac (claset() addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
 by (rtac notI 1);
@@ -497,18 +513,17 @@
 qed "lepoll_imp_lesspoll_succ";
 
 Goalw [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
-      "[| A lesspoll succ(m); m:nat |] ==> A lepoll m";
+     "[| A lesspoll succ(m); m:nat |] ==> A lepoll m";
 by (Clarify_tac 1);
 by (blast_tac (claset() addSIs [inj_not_surj_succ]) 1);
 qed "lesspoll_succ_imp_lepoll";
 
 Goal "m:nat ==> A lesspoll succ(m) <-> A lepoll m";
 by (blast_tac (claset() addSIs [lepoll_imp_lesspoll_succ, 
-                            lesspoll_succ_imp_lepoll]) 1);
+				lesspoll_succ_imp_lepoll]) 1);
 qed "lesspoll_succ_iff";
 
-Goal "[| A lepoll succ(m);  m:nat |] ==>  \
-\                         A lepoll m | A eqpoll succ(m)";
+Goal "[| A lepoll succ(m);  m:nat |] ==> A lepoll m | A eqpoll succ(m)";
 by (rtac disjCI 1);
 by (rtac lesspoll_succ_imp_lepoll 1);
 by (assume_tac 2);
@@ -704,6 +719,12 @@
 qed "lepoll_nat_imp_Finite";
 
 Goalw [Finite_def]
+     "A lesspoll nat ==> Finite(A)";
+by (blast_tac (claset() addDs [ltD, lesspoll_cardinal_lt,
+	       lesspoll_imp_eqpoll RS eqpoll_sym]) 1);;
+qed "lesspoll_nat_is_Finite";
+
+Goalw [Finite_def]
      "[| Y lepoll X;  Finite(X) |] ==> Finite(Y)";
 by (blast_tac 
     (claset() addSEs [eqpollE]