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

author | wenzelm |

Wed, 05 Dec 2001 13:16:34 +0100 | |

changeset 12388 | c845fec1ac94 |

parent 12387 | fe2353a8d1e8 |

child 12389 | 23bd419144eb |

simplified proof (no longer use swapped rules);

--- a/src/HOL/Isar_examples/Cantor.thy Wed Dec 05 03:19:47 2001 +0100 +++ b/src/HOL/Isar_examples/Cantor.thy Wed Dec 05 13:16:34 2001 +0100 @@ -8,26 +8,23 @@ theory Cantor = Main: text_raw {* - \footnote{This is an Isar version of the final example of the - Isabelle/HOL manual \cite{isabelle-HOL}.} + \footnote{This is an Isar 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 uses HOL's set theory, - 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 innermost reasoning expressed quite naively. + 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 uses HOL's set theory, + with the type $\alpha \ap \idt{set}$ and the operator + $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. *} theorem "EX S. S ~: range (f :: 'a => 'a set)" @@ -36,81 +33,38 @@ show "?S ~: range f" proof assume "?S : range f" + then obtain y where "?S = f y" .. thus False - proof - fix y - assume "?S = f y" - thus ?thesis - proof (rule equalityCE) - 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 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 + proof (rule equalityCE) + assume "y : f y" + assume "y : ?S" hence "y ~: f y" .. + thus ?thesis by contradiction + next + assume "y ~: ?S" + assume "y ~: f y" hence "y : ?S" .. + thus ?thesis by contradiction qed qed qed text {* - The following version of the proof essentially does the same - 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 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)" -proof - let ?S = "{x. x ~: f x}" - show "?S ~: range f" - proof - assume "?S : range f" - thus False - proof - fix y - assume "?S = f y" - thus ?thesis - proof (rule equalityCE) - assume "y : f y" - assume "y : ?S" hence "y ~: f y" .. - thus ?thesis by contradiction - next - assume "y ~: f y" - assume "y ~: ?S" hence "y : f y" .. - thus ?thesis by contradiction - qed - qed - qed -qed - -text {* - How much creativity is required? As it happens, Isabelle can prove - this theorem automatically using best-first search. Depth-first - search would diverge, but best-first search successfully navigates - through the large search space. The context of Isabelle's classical - prover contains rules for the relevant constructs of HOL's set - theory. + How much creativity is required? As it happens, Isabelle can prove + this theorem automatically using best-first search. Depth-first + search would diverge, but best-first search successfully navigates + through the large search space. The context of Isabelle's classical + prover contains rules for the relevant constructs of HOL's set + theory. *} theorem "EX S. S ~: range (f :: 'a => 'a set)" by best 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 text. Writing intelligible proof documents - really is a creative process, after all. + 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 text. Writing intelligible proof documents + really is a creative process, after all. *} end