# HG changeset patch
# User wenzelm
# Date 924861035 -7200
# Node ID ab1442d2e4e1f2136fc032b75e780ad223e95da2
# Parent  3489490c948d069383beb2d6d6d725bab0f5d038
detailed proofs;

diff -r 3489490c948d -r ab1442d2e4e1 src/HOL/Isar_examples/Cantor.thy
--- 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;