src/HOL/Isar_examples/Cantor.thy
 changeset 6494 ab1442d2e4e1 parent 6444 2ebe9e630cab child 6505 2863855a6902
```--- 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;```