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

author | wenzelm |

Sat, 26 Dec 2015 12:28:47 +0100 | |

changeset 61930 | 380cbe15cca5 |

parent 61929 | b8e242e52c97 |

child 61931 | ed47044ee6a6 |

modernized example;

src/HOL/Isar_Examples/Cantor.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_Examples/document/root.bib | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Isar_Examples/Cantor.thy Thu Dec 24 09:42:49 2015 +0100 +++ b/src/HOL/Isar_Examples/Cantor.thy Sat Dec 26 12:28:47 2015 +0100 @@ -1,5 +1,5 @@ (* Title: HOL/Isar_Examples/Cantor.thy - Author: Markus Wenzel, TU Muenchen + Author: Makarius *) section \<open>Cantor's Theorem\<close> @@ -8,12 +8,49 @@ imports Main begin -text_raw \<open>\footnote{This is an Isar version of the final example of - the Isabelle/HOL manual @{cite "isabelle-HOL"}.}\<close> +text \<open> + Cantor's Theorem states that there is no surjection from + a set to its powerset. The proof works by diagonalization. E.g.\ see + \<^item> @{url "http://mathworld.wolfram.com/CantorDiagonalMethod.html"} + \<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"} +\<close> + +theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A :: 'a set. \<exists>x :: 'a. f x = A)" +proof + assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A" + then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. f x = A" .. + let ?D = "{x. x \<notin> f x}" + from * obtain a where "f a = ?D" by blast + moreover have "a \<in> ?D \<longleftrightarrow> a \<notin> f a" by blast + ultimately show False by blast +qed + -text \<open>Cantor's Theorem states that every set has more subsets than - it has elements. It has become a favourite basic example in pure - higher-order logic since it is so easily expressed: +text \<open> + Here are shorter proofs via automated proof tools, but without any hints why + and how it works. +\<close> + +theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)" + by best + +theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)" + by force + + +subsection \<open>Classic Isabelle/HOL example\<close> + +text \<open> + The following treatment of Cantor's Theorem follows the classic from the + early 1990s, e.g.\ see the file @{verbatim "92/HOL/ex/set.ML"} in Isabelle92 + or @{cite \<open>\S18.7\<close> "paulson-isa-book"}. The old tactic scripts synthesize + key information of the proof by refinement of schematic goal states. In + contrast, the Isar proof needs to say explicitly what is proven. + + \<^bigskip> + Cantor's Theorem states that every set has more subsets than it has + elements. It has become a favourite basic example in pure higher-order logic + since it is so easily expressed: @{text [display] \<open>\<forall>f::\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool. \<exists>S::\<alpha> \<Rightarrow> bool. \<forall>x::\<alpha>. f x \<noteq> S\<close>} @@ -21,8 +58,9 @@ Viewing types as sets, \<open>\<alpha> \<Rightarrow> bool\<close> represents the powerset of \<open>\<alpha>\<close>. This version of the theorem states that for every function from \<open>\<alpha>\<close> to its powerset, some subset is outside its range. The Isabelle/Isar proofs below - uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator - \<open>range :: (\<alpha> \<Rightarrow> \<beta>) \<Rightarrow> \<beta> set\<close>.\<close> + uses HOL's set theory, with the type \<open>\<alpha> set\<close> and the operator \<open>range :: (\<alpha> \<Rightarrow> + \<beta>) \<Rightarrow> \<beta> set\<close>. +\<close> theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" proof @@ -36,7 +74,7 @@ assume "y \<in> f y" assume "y \<in> ?S" then have "y \<notin> f y" .. - with \<open>y : f y\<close> show ?thesis by contradiction + with \<open>y \<in> f y\<close> show ?thesis by contradiction next assume "y \<notin> ?S" assume "y \<notin> f y" @@ -46,19 +84,15 @@ qed qed -text \<open>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.\<close> +text \<open> + 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. +\<close> theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" by best -text \<open>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.\<close> - end

--- a/src/HOL/Isar_Examples/document/root.bib Thu Dec 24 09:42:49 2015 +0100 +++ b/src/HOL/Isar_Examples/document/root.bib Sat Dec 26 12:28:47 2015 +0100 @@ -65,6 +65,13 @@ title = {The {Isabelle} Reference Manual}, institution = CUCL} +@Book{paulson-isa-book, + author = {Lawrence C. Paulson}, + title = {Isabelle: A Generic Theorem Prover}, + publisher = {Springer}, + year = 1994, + note = {LNCS 828}} + @TechReport{paulson-mutilated-board, author = {Lawrence C. Paulson}, title = {A Simple Formalization and Proof for the Mutilated Chess Board},