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