src/HOL/Isar_examples/Cantor.thy
 changeset 7860 7819547df4d8 parent 7833 f5288e4b95d1 child 7869 c007f801cd59
--- a/src/HOL/Isar_examples/Cantor.thy	Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Thu Oct 14 01:07:24 1999 +0200
@@ -19,12 +19,11 @@
Viewing types as sets, $\alpha \To \idt{bool}$ represents the
powerset of $\alpha$.  This version of the theorem states that for
every function from $\alpha$ to its powerset, some subset is outside
- its range.  The Isabelle/Isar proofs below use HOL's set theory, with
- the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
+ its range.  The Isabelle/Isar proofs below uses HOL's set theory,
+ with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.

- \bigskip We first consider a rather verbose version of the proof,
- with the reasoning expressed quite naively.  We only make use of the
- pure core of the Isar proof language.
+ \bigskip We first consider a slightly awkward version of the proof,
+ with the reasoning expressed quite naively.
*};

theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -33,21 +32,21 @@
show "?S ~: range f";
proof;
assume "?S : range f";
-    then; show False;
+    thus False;
proof;
fix y;
assume "?S = f y";
-      then; show ?thesis;
+      thus ?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; by contradiction;
+        assume in_S: "y : ?S";
+        assume in_fy: "y : f y";
+        from in_S; have notin_fy: "y ~: f y"; ..;
+        from notin_fy in_fy; show ?thesis; by contradiction;
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; by contradiction;
+        assume notin_S: "y ~: ?S";
+        assume notin_fy: "y ~: f y";
+        from notin_S; have in_fy: "y : f y"; ..;
+        from notin_fy in_fy; show ?thesis; by contradiction;
qed;
qed;
qed;
@@ -55,8 +54,15 @@

text {*
The following version of the proof essentially does the same
- reasoning, only that it is expressed more neatly, with some derived
- Isar language elements involved.
+ reasoning, only that it is expressed more neatly.  In particular, we
+ change the order of assumptions introduced in the two cases of rule
+ \name{equalityCE}, streamlining the flow of intermediate facts and
+ avoiding explicit naming.\footnote{In general, neither the order of
+ assumptions as introduced \isacommand{assume}, nor the order of goals
+ as solved by \isacommand{show} matters.  The basic logical structure
+ has to be left intact, though.  In particular, assumptions
+ belonging'' to some goal have to be introduced \emph{before} its
+ corresponding \isacommand{show}.}
*};

theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -85,11 +91,12 @@

text {*
How much creativity is required?  As it happens, Isabelle can prove
- this theorem automatically.  The default classical set contains rules
- for most of the constructs of HOL's set theory.  We must augment it
- with \name{equalityCE} to break up set equalities, and then apply
- best-first search.  Depth-first search would diverge, but best-first
- search successfully navigates through the large search space.
+ this theorem automatically.  The default context of the classical
+ proof tools contains rules for most of the constructs of HOL's set
+ theory.  We must augment it with \name{equalityCE} to break up set
+ equalities, and then apply best-first search.  Depth-first search
+ would diverge, but best-first search successfully navigates through
+ the large search space.
*};

theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -100,7 +107,7 @@
idea of how the proof actually works.  There is currently no way to
transform internal system-level representations of Isabelle proofs
back into Isar documents.  Writing proof documents really is a
- creative process.
+ creative process, after all.
*};

end;