wenzelm@6444: (* Title: HOL/Isar_examples/Cantor.thy wenzelm@6444: ID: $Id$ wenzelm@6444: Author: Markus Wenzel, TU Muenchen wenzelm@6444: *) wenzelm@6444: wenzelm@10007: header {* Cantor's Theorem *} wenzelm@6444: haftmann@16417: theory Cantor imports Main begin wenzelm@7955: wenzelm@7955: text_raw {* wenzelm@12388: \footnote{This is an Isar version of the final example of the wenzelm@12388: Isabelle/HOL manual \cite{isabelle-HOL}.} wenzelm@10007: *} wenzelm@7819: wenzelm@7819: text {* wenzelm@12388: Cantor's Theorem states that every set has more subsets than it has wenzelm@12388: elements. It has become a favorite basic example in pure wenzelm@12388: higher-order logic since it is so easily expressed: $\all{f::\alpha wenzelm@12388: \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}} wenzelm@12388: \all{x::\alpha} f \ap x \not= S$ wenzelm@12388: wenzelm@12388: Viewing types as sets, $\alpha \To \idt{bool}$ represents the wenzelm@12388: powerset of $\alpha$. This version of the theorem states that for wenzelm@12388: every function from $\alpha$ to its powerset, some subset is outside wenzelm@12388: its range. The Isabelle/Isar proofs below uses HOL's set theory, wenzelm@12388: with the type $\alpha \ap \idt{set}$ and the operator wenzelm@12388: $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$. wenzelm@10007: *} wenzelm@6505: wenzelm@10007: theorem "EX S. S ~: range (f :: 'a => 'a set)" wenzelm@10007: proof wenzelm@10007: let ?S = "{x. x ~: f x}" wenzelm@10007: show "?S ~: range f" wenzelm@10007: proof wenzelm@10007: assume "?S : range f" wenzelm@12388: then obtain y where "?S = f y" .. wenzelm@23373: then show False wenzelm@12388: proof (rule equalityCE) wenzelm@12388: assume "y : f y" wenzelm@23373: assume "y : ?S" then have "y ~: f y" .. wenzelm@23373: with y : f y show ?thesis by contradiction wenzelm@12388: next wenzelm@12388: assume "y ~: ?S" wenzelm@23373: assume "y ~: f y" then have "y : ?S" .. wenzelm@23373: with y ~: ?S show ?thesis by contradiction wenzelm@10007: qed wenzelm@10007: qed wenzelm@10007: qed wenzelm@6494: wenzelm@6744: text {* wenzelm@12388: How much creativity is required? As it happens, Isabelle can prove wenzelm@12388: this theorem automatically using best-first search. Depth-first wenzelm@12388: search would diverge, but best-first search successfully navigates wenzelm@12388: through the large search space. The context of Isabelle's classical wenzelm@12388: prover contains rules for the relevant constructs of HOL's set wenzelm@12388: theory. wenzelm@10007: *} wenzelm@6505: wenzelm@10007: theorem "EX S. S ~: range (f :: 'a => 'a set)" wenzelm@10007: by best wenzelm@6494: wenzelm@6744: text {* wenzelm@12388: While this establishes the same theorem internally, we do not get wenzelm@12388: any idea of how the proof actually works. There is currently no way wenzelm@12388: to transform internal system-level representations of Isabelle wenzelm@12388: proofs back into Isar text. Writing intelligible proof documents wenzelm@12388: really is a creative process, after all. wenzelm@10007: *} wenzelm@6444: wenzelm@10007: end