new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
authorpaulson
Wed Jun 21 10:34:33 2000 +0200 (2000-06-21)
changeset 9099f713ef362ad0
parent 9098 3a0912a127ec
child 9100 9e081c812338
new theorems lepoll_Ord_imp_eqpoll, lesspoll_imp_eqpoll, lesspoll_nat_is_Finite
src/ZF/Cardinal.ML
     1.1 --- a/src/ZF/Cardinal.ML	Wed Jun 21 10:32:57 2000 +0200
     1.2 +++ b/src/ZF/Cardinal.ML	Wed Jun 21 10:34:33 2000 +0200
     1.3 @@ -130,8 +130,8 @@
     1.4  qed "eqpoll_0_iff";
     1.5  
     1.6  Goalw [eqpoll_def] 
     1.7 -    "[| A eqpoll B;  C eqpoll D;  A Int C = 0;  B Int D = 0 |] ==> \
     1.8 -\         A Un C eqpoll B Un D";
     1.9 +    "[| A eqpoll B;  C eqpoll D;  A Int C = 0;  B Int D = 0 |]  \
    1.10 +\    ==> A Un C eqpoll B Un D";
    1.11  by (blast_tac (claset() addIs [bij_disjoint_Un]) 1);
    1.12  qed "eqpoll_disjoint_Un";
    1.13  
    1.14 @@ -423,6 +423,22 @@
    1.15  by (etac Ord_cardinal_le 1);
    1.16  qed "lepoll_cardinal_le";
    1.17  
    1.18 +Goal "[| A lepoll i; Ord(i) |] ==> |A| eqpoll A";
    1.19 +by (blast_tac (claset() addIs [lepoll_cardinal_le, well_ord_Memrel,
    1.20 +                                well_ord_cardinal_eqpoll]
    1.21 +                        addSDs [lepoll_well_ord]) 1);
    1.22 +qed "lepoll_Ord_imp_eqpoll";
    1.23 +
    1.24 +Goalw [lesspoll_def]
    1.25 +     "[| A lesspoll i; Ord(i) |] ==> |A| eqpoll A";
    1.26 +by (blast_tac (claset() addIs [lepoll_Ord_imp_eqpoll]) 1);
    1.27 +qed "lesspoll_imp_eqpoll";
    1.28 +
    1.29 +Goalw [lesspoll_def]
    1.30 +     "[| A lesspoll i; Ord(i) |] ==> |A| eqpoll A";
    1.31 +by (blast_tac (claset() addIs [lepoll_Ord_imp_eqpoll]) 1);
    1.32 +qed "lesspoll_imp_eqpoll";
    1.33 +
    1.34  
    1.35  (*** The finite cardinals ***)
    1.36  
    1.37 @@ -487,7 +503,7 @@
    1.38  (** lepoll, lesspoll and natural numbers **)
    1.39  
    1.40  Goalw [lesspoll_def]
    1.41 -      "[| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
    1.42 +     "[| A lepoll m; m:nat |] ==> A lesspoll succ(m)";
    1.43  by (rtac conjI 1);
    1.44  by (blast_tac (claset() addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1);
    1.45  by (rtac notI 1);
    1.46 @@ -497,18 +513,17 @@
    1.47  qed "lepoll_imp_lesspoll_succ";
    1.48  
    1.49  Goalw [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
    1.50 -      "[| A lesspoll succ(m); m:nat |] ==> A lepoll m";
    1.51 +     "[| A lesspoll succ(m); m:nat |] ==> A lepoll m";
    1.52  by (Clarify_tac 1);
    1.53  by (blast_tac (claset() addSIs [inj_not_surj_succ]) 1);
    1.54  qed "lesspoll_succ_imp_lepoll";
    1.55  
    1.56  Goal "m:nat ==> A lesspoll succ(m) <-> A lepoll m";
    1.57  by (blast_tac (claset() addSIs [lepoll_imp_lesspoll_succ, 
    1.58 -                            lesspoll_succ_imp_lepoll]) 1);
    1.59 +				lesspoll_succ_imp_lepoll]) 1);
    1.60  qed "lesspoll_succ_iff";
    1.61  
    1.62 -Goal "[| A lepoll succ(m);  m:nat |] ==>  \
    1.63 -\                         A lepoll m | A eqpoll succ(m)";
    1.64 +Goal "[| A lepoll succ(m);  m:nat |] ==> A lepoll m | A eqpoll succ(m)";
    1.65  by (rtac disjCI 1);
    1.66  by (rtac lesspoll_succ_imp_lepoll 1);
    1.67  by (assume_tac 2);
    1.68 @@ -704,6 +719,12 @@
    1.69  qed "lepoll_nat_imp_Finite";
    1.70  
    1.71  Goalw [Finite_def]
    1.72 +     "A lesspoll nat ==> Finite(A)";
    1.73 +by (blast_tac (claset() addDs [ltD, lesspoll_cardinal_lt,
    1.74 +	       lesspoll_imp_eqpoll RS eqpoll_sym]) 1);;
    1.75 +qed "lesspoll_nat_is_Finite";
    1.76 +
    1.77 +Goalw [Finite_def]
    1.78       "[| Y lepoll X;  Finite(X) |] ==> Finite(Y)";
    1.79  by (blast_tac 
    1.80      (claset() addSEs [eqpollE]