summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 09 Oct 1999 23:20:02 +0200 | |

changeset 7819 | 6dd018b6cf3f |

parent 7818 | 1acfb8cc3720 |

child 7820 | cad7cc30fa40 |

tuned presentation;

--- a/src/HOL/Isar_examples/Cantor.thy Sat Oct 09 23:19:20 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Sat Oct 09 23:20:02 1999 +0200 @@ -1,9 +1,6 @@ (* Title: HOL/Isar_examples/Cantor.thy ID: $Id$ Author: Markus Wenzel, TU Muenchen - -Cantor's theorem -- Isar'ized version of the final section of the HOL -chapter of "Isabelle's Object-Logics" (Larry Paulson). *) header {* Cantor's Theorem *}; @@ -11,21 +8,26 @@ theory Cantor = Main:; text {* - Cantor's Theorem states that every set has more subsets than it has - 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\] + This is an Isar'ized version of the final example of the Isabelle/HOL + manual \cite{isabelle-HOL}. +*}; + +text {* + Cantor's Theorem states that every set has more subsets than it has + 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\] - 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}$. + 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. + \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)"; @@ -55,9 +57,9 @@ qed; text {* - 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. + 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)"; @@ -85,23 +87,23 @@ 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 - \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. + 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. Note that 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. Writing proof documents really is a + creative process. *}; end;