--- a/src/ZF/ZF.ML Fri Nov 25 10:43:50 1994 +0100
+++ b/src/ZF/ZF.ML Fri Nov 25 11:02:39 1994 +0100
@@ -20,6 +20,7 @@
val bexI : thm
val bex_cong : thm
val bspec : thm
+ val cantor : thm
val CollectD1 : thm
val CollectD2 : thm
val CollectE : thm
@@ -480,6 +481,17 @@
(*Standard claset*)
val lemmas_cs = subset0_cs addSIs [subsetI] addEs [subsetCE];
+(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
+
+val cantor_cs = FOL_cs (*precisely the rules needed for the proof*)
+ addSIs [ballI, CollectI, PowI, subsetI] addIs [bexI]
+ addSEs [CollectE, equalityCE];
+
+(*The search is undirected; similar proof attempts may fail.
+ b represents ANY map, such as (lam x:A.b(x)): A->Pow(A). *)
+val cantor = prove_goal ZF.thy "EX S: Pow(A). ALL x:A. b(x) ~= S"
+ (fn _ => [best_tac cantor_cs 1]);
+
(*Lemma for the inductive definition in Zorn.thy*)
val Union_in_Pow = prove_goal ZF.thy
"!!Y. Y : Pow(Pow(A)) ==> Union(Y) : Pow(A)"