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