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

src/HOL/Isar_examples/Cantor.thy

changeset 7860 | 7819547df4d8 |

parent 7833 | f5288e4b95d1 |

child 7869 | c007f801cd59 |

--- a/src/HOL/Isar_examples/Cantor.thy Wed Oct 13 19:44:33 1999 +0200 +++ b/src/HOL/Isar_examples/Cantor.thy Thu Oct 14 01:07:24 1999 +0200 @@ -19,12 +19,11 @@ 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}$. + its range. The Isabelle/Isar proofs below uses 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 slightly awkward version of the proof, + with the reasoning expressed quite naively. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -33,21 +32,21 @@ show "?S ~: range f"; proof; assume "?S : range f"; - then; show False; + thus False; proof; fix y; assume "?S = f y"; - then; show ?thesis; + thus ?thesis; proof (rule equalityCE); - assume y_in_S: "y : ?S"; - assume y_in_fy: "y : f y"; - from y_in_S; have y_notin_fy: "y ~: f y"; ..; - from y_notin_fy y_in_fy; show ?thesis; by contradiction; + assume in_S: "y : ?S"; + assume in_fy: "y : f y"; + from in_S; have notin_fy: "y ~: f y"; ..; + from notin_fy in_fy; show ?thesis; by contradiction; next; - assume y_notin_S: "y ~: ?S"; - assume y_notin_fy: "y ~: f y"; - from y_notin_S; have y_in_fy: "y : f y"; ..; - from y_notin_fy y_in_fy; show ?thesis; by contradiction; + assume notin_S: "y ~: ?S"; + assume notin_fy: "y ~: f y"; + from notin_S; have in_fy: "y : f y"; ..; + from notin_fy in_fy; show ?thesis; by contradiction; qed; qed; qed; @@ -55,8 +54,15 @@ 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. + reasoning, only that it is expressed more neatly. In particular, we + 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}.} *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -85,11 +91,12 @@ 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. + 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 + would diverge, but best-first search successfully navigates through + the large search space. *}; theorem "EX S. S ~: range(f :: 'a => 'a set)"; @@ -100,7 +107,7 @@ 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. + creative process, after all. *}; end;