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