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

src/HOL/Isar_examples/Cantor.thy

changeset 7874 | 180364256231 |

parent 7869 | c007f801cd59 |

child 7955 | f30e08579481 |

--- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:43:05 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:44:37 1999 +0200 @@ -14,16 +14,17 @@ 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\] + \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 uses HOL's set theory, - with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$. + with the type $\alpha \ap \idt{set}$ and the operator + $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. \bigskip We first consider a slightly awkward version of the proof, - with the reasoning expressed quite naively. + with the innermost reasoning expressed quite naively. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -58,11 +59,11 @@ change the order of assumptions introduced in the two cases of rule \name{equalityCE}, streamlining the flow of intermediate facts and avoiding explicit naming.\footnote{In general, neither the order of - assumptions as introduced \isacommand{assume}, nor the order of goals - as solved by \isacommand{show} matters. The basic logical structure - has to be left intact, though. In particular, assumptions - ``belonging'' to some goal have to be introduced \emph{before} its - corresponding \isacommand{show}.} + assumptions as introduced by \isacommand{assume}, nor the order of + goals as solved by \isacommand{show} is of any significance. The + basic logical structure has to be left intact, though. In + particular, assumptions ``belonging'' to some goal have to be + introduced \emph{before} its corresponding \isacommand{show}.} *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -91,10 +92,10 @@ text {* How much creativity is required? As it happens, Isabelle can prove - this theorem automatically. The default context of the classical - proof tools 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 + this theorem automatically. The default context of the Isabelle's + classical prover 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. *}; @@ -106,8 +107,8 @@ 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, after all. + back into Isar documents. Writing intelligible proof documents + really is a creative process, after all. *}; end;