src/HOL/Isar_examples/Cantor.thy
 changeset 7748 5b9c45b21782 parent 7480 0a0e0dbe1269 child 7800 8ee919e42174
--- a/src/HOL/Isar_examples/Cantor.thy	Tue Oct 05 21:20:28 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Wed Oct 06 00:31:40 1999 +0200
@@ -6,30 +6,25 @@
chapter of "Isabelle's Object-Logics" (Larry Paulson).
*)

-theory Cantor = Main:;
+header {* More classical proofs: Cantor's Theorem *};

-
-section {* Example: Cantor's Theorem *};
+theory Cantor = Main:;

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)";
@@ -58,11 +53,10 @@
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)";
@@ -89,27 +83,24 @@
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;