src/HOL/Isar_examples/Cantor.thy
 author wenzelm Wed Jun 13 18:30:11 2007 +0200 (2007-06-13) changeset 23373 ead82c82da9e parent 16417 9bc16273c2d4 child 31758 3edd5f813f01 permissions -rw-r--r--
tuned proofs: avoid implicit prems;
     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     then show False

    38     proof (rule equalityCE)

    39       assume "y : f y"

    40       assume "y : ?S" then have "y ~: f y" ..

    41       with y : f y show ?thesis by contradiction

    42     next

    43       assume "y ~: ?S"

    44       assume "y ~: f y" then have "y : ?S" ..

    45       with y ~: ?S show ?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