--- a/src/HOL/Isar_examples/Cantor.thy Fri Apr 23 11:50:17 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Fri Apr 23 11:50:35 1999 +0200
@@ -7,7 +7,61 @@
theory Cantor = Main:;
-theorem cantor: "EX S. S ~: range(f :: 'a => 'a set)";
-by (best elim: equalityCE);
+
+theorem "EX S. S ~: range(f :: 'a => 'a set)";
+proof;
+ let ??S = "{x. x ~: f x}";
+ show "??S ~: range f";
+ proof;
+ assume "??S : range f";
+ then; show False;
+ proof;
+ fix y;
+ assume "??S = f y";
+ then; show ??thesis;
+ proof (rule equalityCE);
+ assume y_in_S: "y : ??S";
+ assume y_in_fy: "y : f y";
+ from y_in_S; have y_notin_fy: "y ~: f y"; ..;
+ from y_notin_fy y_in_fy; show ??thesis; ..;
+ next;
+ assume y_notin_S: "y ~: ??S";
+ assume y_notin_fy: "y ~: f y";
+ from y_notin_S; have y_in_fy: "y : f y"; ..;
+ from y_notin_fy y_in_fy; show ??thesis; ..;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+theorem "EX S. S ~: range(f :: 'a => 'a set)";
+proof;
+ let ??S = "{x. x ~: f x}";
+ show "??S ~: range f";
+ proof;
+ assume "??S : range f";
+ then; show False;
+ proof;
+ fix y;
+ assume "??S = f y";
+ then; show ??thesis;
+ proof (rule equalityCE);
+ assume "y : ??S"; then; have y_notin_fy: "y ~: f y"; ..;
+ assume "y : f y";
+ from y_notin_fy it; show ??thesis; ..;
+ next;
+ assume "y ~: ??S"; then; have y_in_fy: "y : f y"; ..;
+ assume "y ~: f y";
+ from it y_in_fy; show ??thesis; ..;
+ qed;
+ qed;
+ qed;
+qed;
+
+
+theorem "EX S. S ~: range(f :: 'a => 'a set)";
+ by (best elim: equalityCE);
+
end;