author paulson Tue, 25 Dec 2001 10:02:20 +0100 changeset 12596 34265656f0b4 parent 12595 0480d02221b8 child 12597 14822e4436bf
some new theorems
 src/ZF/Cardinal.ML file | annotate | diff | comparison | revisions
```--- 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);
+
(*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";
+
+```