--- a/src/ZF/Cardinal.ML Tue Dec 25 10:02:01 2001 +0100
+++ b/src/ZF/Cardinal.ML Tue Dec 25 10:02:20 2001 +0100
@@ -488,6 +488,10 @@
by (blast_tac (claset() addSEs [lt_irrefl]) 1);
qed "nat_into_Card";
+bind_thm ("cardinal_0", nat_0I RS nat_into_Card RS Card_cardinal_eq);
+bind_thm ("cardinal_1", nat_1I RS nat_into_Card RS Card_cardinal_eq);
+AddIffs [cardinal_0, cardinal_1];
+
(*Part of Kunen's Lemma 10.6*)
Goal "[| succ(n) lepoll n; n:nat |] ==> P";
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1);
@@ -624,6 +628,15 @@
by (simp_tac (simpset() addsimps [nat_into_Card RS Card_cardinal_eq]) 1);
qed "cardinal_singleton";
+Goal "A ~= 0 ==> 1 lepoll A";
+by (etac not_emptyE 1);
+by (res_inst_tac [("a", "cons(x, A-{x})")] subst 1);
+by (res_inst_tac [("a", "cons(0,0)"),
+ ("P", "%y. y lepoll cons(x, A-{x})")] subst 2);
+by (blast_tac (claset() addIs [cons_lepoll_cong, subset_imp_lepoll]) 3);
+by Auto_tac;
+qed "not_0_is_lepoll_1";
+
(*Congruence law for succ under equipollence*)
Goalw [succ_def]
"A eqpoll B ==> succ(A) eqpoll succ(B)";
@@ -823,3 +836,5 @@
Goalw [Finite_def] "n:nat ==> Finite(n)";
by (fast_tac (claset() addSIs [eqpoll_refl]) 1);
qed "nat_into_Finite";
+
+