src/HOL/Isar_Examples/Cantor.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 37671 fa53d267dab3
child 55640 abc140f21caa
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     1 (*  Title:      HOL/Isar_Examples/Cantor.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Cantor's Theorem *}
     6 
     7 theory Cantor
     8 imports Main
     9 begin
    10 
    11 text_raw {* \footnote{This is an Isar version of the final example of
    12   the Isabelle/HOL manual \cite{isabelle-HOL}.}  *}
    13 
    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\]
    19 
    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}$. *}
    26 
    27 theorem "EX S. S ~: range (f :: 'a => 'a set)"
    28 proof
    29   let ?S = "{x. x ~: f x}"
    30   show "?S ~: range f"
    31   proof
    32     assume "?S : range f"
    33     then obtain y where "?S = f y" ..
    34     then show False
    35     proof (rule equalityCE)
    36       assume "y : f y"
    37       assume "y : ?S" then have "y ~: f y" ..
    38       with `y : f y` show ?thesis by contradiction
    39     next
    40       assume "y ~: ?S"
    41       assume "y ~: f y" then have "y : ?S" ..
    42       with `y ~: ?S` show ?thesis by contradiction
    43     qed
    44   qed
    45 qed
    46 
    47 text {* How much creativity is required?  As it happens, Isabelle can
    48   prove this theorem automatically using best-first search.
    49   Depth-first search would diverge, but best-first search successfully
    50   navigates through the large search space.  The context of Isabelle's
    51   classical prover contains rules for the relevant constructs of HOL's
    52   set theory.  *}
    53 
    54 theorem "EX S. S ~: range (f :: 'a => 'a set)"
    55   by best
    56 
    57 text {* While this establishes the same theorem internally, we do not
    58   get any idea of how the proof actually works.  There is currently no
    59   way to transform internal system-level representations of Isabelle
    60   proofs back into Isar text.  Writing intelligible proof documents
    61   really is a creative process, after all. *}
    62 
    63 end