src/ZF/CardinalArith.ML
changeset 488 52f7447d4f1b
parent 484 70b789956bd3
child 516 1957113f0d7d
--- a/src/ZF/CardinalArith.ML	Wed Jul 27 15:14:31 1994 +0200
+++ b/src/ZF/CardinalArith.ML	Wed Jul 27 15:33:42 1994 +0200
@@ -334,6 +334,10 @@
 by (rtac (subset_succI RS subset_imp_lepoll) 1);
 val nat_succ_eqpoll = result();
 
+goalw CardinalArith.thy [InfCard_def] "InfCard(nat)";
+by (fast_tac (ZF_cs addIs [Card_nat, le_refl, Card_is_Ord]) 1);
+val InfCard_nat = result();
+
 goalw CardinalArith.thy [InfCard_def] "!!K. InfCard(K) ==> Card(K)";
 by (etac conjunct1 1);
 val InfCard_is_Card = result();
@@ -635,3 +639,9 @@
 by (asm_simp_tac 
     (ZF_ss addsimps [lt_csucc_iff, Card_cardinal_eq, Card_is_Ord]) 1);
 val Card_lt_csucc_iff = result();
+
+goalw CardinalArith.thy [InfCard_def]
+    "!!K. InfCard(K) ==> InfCard(csucc(K))";
+by (asm_simp_tac (ZF_ss addsimps [Card_csucc, Card_is_Ord, 
+				  lt_csucc RS leI RSN (2,le_trans)]) 1);
+val InfCard_csucc = result();