--- 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;