1.1 --- a/src/ZF/Cardinal.ML	Tue Dec 25 10:02:01 2001 +0100
     1.2 +++ b/src/ZF/Cardinal.ML	Tue Dec 25 10:02:20 2001 +0100
     1.3 @@ -488,6 +488,10 @@
     1.4  by (blast_tac (claset() addSEs [lt_irrefl]) 1);
     1.5  qed "nat_into_Card";
     1.6  
     1.7 +bind_thm ("cardinal_0", nat_0I RS nat_into_Card RS Card_cardinal_eq);
     1.8 +bind_thm ("cardinal_1", nat_1I RS nat_into_Card RS Card_cardinal_eq);
     1.9 +AddIffs [cardinal_0, cardinal_1];
    1.10 +
    1.11  (*Part of Kunen's Lemma 10.6*)
    1.12  Goal "[| succ(n) lepoll n;  n:nat |] ==> P";
    1.13  by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);
    1.14 @@ -624,6 +628,15 @@
    1.15  by (simp_tac (simpset() addsimps [nat_into_Card RS Card_cardinal_eq]) 1);
    1.16  qed "cardinal_singleton";
    1.17  
    1.18 +Goal "A ~= 0 ==> 1 lepoll A";
    1.19 +by (etac not_emptyE 1);
    1.20 +by (res_inst_tac [("a", "cons(x, A-{x})")] subst 1);
    1.21 +by (res_inst_tac [("a", "cons(0,0)"), 
    1.22 +                  ("P", "%y. y lepoll cons(x, A-{x})")] subst 2);
    1.23 +by (blast_tac (claset() addIs [cons_lepoll_cong, subset_imp_lepoll]) 3);
    1.24 +by Auto_tac;
    1.25 +qed "not_0_is_lepoll_1";
    1.26 +
    1.27  (*Congruence law for  succ  under equipollence*)
    1.28  Goalw [succ_def]
    1.29      "A eqpoll B ==> succ(A) eqpoll succ(B)";
    1.30 @@ -823,3 +836,5 @@
    1.31  Goalw [Finite_def] "n:nat ==> Finite(n)";
    1.32  by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
    1.33  qed "nat_into_Finite";
    1.34 +
    1.35 +