src/HOL/Isar_Examples/Cantor.thy
 author haftmann Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) changeset 37659 14cabf5fa710 parent 33026 8f35633c4922 child 37671 fa53d267dab3 permissions -rw-r--r--
more speaking names
 wenzelm@33026 1 (* Title: HOL/Isar_Examples/Cantor.thy wenzelm@6444 2 Author: Markus Wenzel, TU Muenchen wenzelm@6444 3 *) wenzelm@6444 4 wenzelm@10007 5 header {* Cantor's Theorem *} wenzelm@6444 6 wenzelm@31758 7 theory Cantor wenzelm@31758 8 imports Main wenzelm@31758 9 begin wenzelm@7955 10 wenzelm@7955 11 text_raw {* wenzelm@12388 12 \footnote{This is an Isar version of the final example of the wenzelm@12388 13 Isabelle/HOL manual \cite{isabelle-HOL}.} wenzelm@10007 14 *} wenzelm@7819 15 wenzelm@7819 16 text {* wenzelm@12388 17 Cantor's Theorem states that every set has more subsets than it has wenzelm@12388 18 elements. It has become a favorite basic example in pure wenzelm@12388 19 higher-order logic since it is so easily expressed: $\all{f::\alpha wenzelm@12388 20 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} wenzelm@12388 21 \all{x::\alpha} f \ap x \not= S$ wenzelm@12388 22 wenzelm@12388 23 Viewing types as sets, $\alpha \To \idt{bool}$ represents the wenzelm@12388 24 powerset of $\alpha$. This version of the theorem states that for wenzelm@12388 25 every function from $\alpha$ to its powerset, some subset is outside wenzelm@12388 26 its range. The Isabelle/Isar proofs below uses HOL's set theory, wenzelm@12388 27 with the type $\alpha \ap \idt{set}$ and the operator wenzelm@12388 28 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. wenzelm@10007 29 *} wenzelm@6505 30 wenzelm@10007 31 theorem "EX S. S ~: range (f :: 'a => 'a set)" wenzelm@10007 32 proof wenzelm@10007 33 let ?S = "{x. x ~: f x}" wenzelm@10007 34 show "?S ~: range f" wenzelm@10007 35 proof wenzelm@10007 36 assume "?S : range f" wenzelm@12388 37 then obtain y where "?S = f y" .. wenzelm@23373 38 then show False wenzelm@12388 39 proof (rule equalityCE) wenzelm@12388 40 assume "y : f y" wenzelm@23373 41 assume "y : ?S" then have "y ~: f y" .. wenzelm@23373 42 with y : f y show ?thesis by contradiction wenzelm@12388 43 next wenzelm@12388 44 assume "y ~: ?S" wenzelm@23373 45 assume "y ~: f y" then have "y : ?S" .. wenzelm@23373 46 with y ~: ?S show ?thesis by contradiction wenzelm@10007 47 qed wenzelm@10007 48 qed wenzelm@10007 49 qed wenzelm@6494 50 wenzelm@6744 51 text {* wenzelm@12388 52 How much creativity is required? As it happens, Isabelle can prove wenzelm@12388 53 this theorem automatically using best-first search. Depth-first wenzelm@12388 54 search would diverge, but best-first search successfully navigates wenzelm@12388 55 through the large search space. The context of Isabelle's classical wenzelm@12388 56 prover contains rules for the relevant constructs of HOL's set wenzelm@12388 57 theory. wenzelm@10007 58 *} wenzelm@6505 59 wenzelm@10007 60 theorem "EX S. S ~: range (f :: 'a => 'a set)" wenzelm@10007 61 by best wenzelm@6494 62 wenzelm@6744 63 text {* wenzelm@12388 64 While this establishes the same theorem internally, we do not get wenzelm@12388 65 any idea of how the proof actually works. There is currently no way wenzelm@12388 66 to transform internal system-level representations of Isabelle wenzelm@12388 67 proofs back into Isar text. Writing intelligible proof documents wenzelm@12388 68 really is a creative process, after all. wenzelm@10007 69 *} wenzelm@6444 70 wenzelm@10007 71 end