src/HOL/Isar_examples/Cantor.thy

 
 Cantor's theorem -- Isar'ized version of the final section of the HOL
 chapter of "Isabelle's Object-Logics" (Larry Paulson).
 *)
 
+header {* More classical proofs: Cantor's Theorem *};
+
 theory Cantor = Main:;
-
-
-section {* Example: Cantor's Theorem *};
 
 text {*
   Cantor's Theorem states that every set has more subsets than it has
-  elements.  It has become a favourite example in higher-order logic
-  since it is so easily expressed: @{display term[show_types] "ALL f
-  :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"}
-
-  Viewing types as sets, @{type "'a => bool"} represents the powerset
-  of @{type 'a}.  This version states that for every function from
-  @{type 'a} to its powerset, some subset is outside its range.
-
-  The Isabelle/Isar proofs below use HOL's set theory, with the type
-  @{type "'a set"} and the operator @{term range}.
-*};
-
-
-text {*
-  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.
+  elements.  It has become a favourite basic example in 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\]
+  
+  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}$.
+  
+  \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.
 *};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
   let ?S = "{x. x ~: f x}";

       qed;
     qed;
   qed;
 qed;
 
-
 text {*
-  The following version essentially does the same reasoning, only that
-  it is expressed more neatly, with some derived Isar language
-  elements involved.
+  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.
 *};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
 proof;
   let ?S = "{x. x ~: f x}";

       qed;
     qed;
   qed;
 qed;
 
-
 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 @{thm 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.
+  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.
 *};
 
 theorem "EX S. S ~: range(f :: 'a => 'a set)";
   by (best elim: equalityCE);
 
 text {*
-  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 Isabelle/Isar proof
-  documents actually \emph{is} a creative process.
+  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.  Note that writing Isabelle/Isar proof documents actually
+  \emph{is} a creative process.
 *};
 
-
 end;