summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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;