src/HOL/Isar_examples/Cantor.thy
changeset 7874 180364256231
parent 7869 c007f801cd59
child 7955 f30e08579481
--- a/src/HOL/Isar_examples/Cantor.thy	Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Fri Oct 15 16:44:37 1999 +0200
@@ -14,16 +14,17 @@
  elements.  It has become a favorite basic example in pure
  higher-order logic since it is so easily expressed: \[\all{f::\alpha
  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
- \all{x::\alpha}. f \ap x \not= S\]
+ \all{x::\alpha} f \ap x \not= S\]
   
  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 uses HOL's set theory,
- with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
+ with the type $\alpha \ap \idt{set}$ and the operator
+ $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
   
  \bigskip We first consider a slightly awkward version of the proof,
- with the reasoning expressed quite naively.
+ with the innermost reasoning expressed quite naively.
 *};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -58,11 +59,11 @@
  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}.}
+ assumptions as introduced by \isacommand{assume}, nor the order of
+ goals as solved by \isacommand{show} is of any significance.  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)";
@@ -91,10 +92,10 @@
 
 text {*
  How much creativity is required?  As it happens, Isabelle can prove
- 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
+ this theorem automatically.  The default context of the Isabelle's
+ classical prover 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.
 *};
@@ -106,8 +107,8 @@
  While this establishes the same theorem internally, we do not get any
  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, after all.
+ back into Isar documents.  Writing intelligible proof documents
+ really is a creative process, after all.
 *};
 
 end;