src/HOL/Isar_examples/Cantor.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7955 f30e08579481
child 9474 b0ce3b7c9c26
permissions -rw-r--r--
improved presentation;
     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 = Main:;
     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  \bigskip We first consider a slightly awkward version of the proof,
    30  with the innermost reasoning expressed quite naively.
    31 *};
    32 
    33 theorem "EX S. S ~: range (f :: 'a => 'a set)";
    34 proof;
    35   let ?S = "{x. x ~: f x}";
    36   show "?S ~: range f";
    37   proof;
    38     assume "?S : range f";
    39     thus False;
    40     proof;
    41       fix y; 
    42       assume "?S = f y";
    43       thus ?thesis;
    44       proof (rule equalityCE);
    45         assume in_S: "y : ?S";
    46         assume in_fy: "y : f y";
    47         from in_S; have notin_fy: "y ~: f y"; ..;
    48         from notin_fy in_fy; show ?thesis; by contradiction;
    49       next;
    50         assume notin_S: "y ~: ?S";
    51         assume notin_fy: "y ~: f y";
    52         from notin_S; have in_fy: "y : f y"; ..;
    53         from notin_fy in_fy; show ?thesis; by contradiction;
    54       qed;
    55     qed;
    56   qed;
    57 qed;
    58 
    59 text {*
    60  The following version of the proof essentially does the same
    61  reasoning, only that it is expressed more neatly.  In particular, we
    62  change the order of assumptions introduced in the two cases of rule
    63  \name{equalityCE}, streamlining the flow of intermediate facts and
    64  avoiding explicit naming.\footnote{In general, neither the order of
    65  assumptions as introduced by \isacommand{assume}, nor the order of
    66  goals as solved by \isacommand{show} is of any significance.  The
    67  basic logical structure has to be left intact, though.  In
    68  particular, assumptions ``belonging'' to some goal have to be
    69  introduced \emph{before} its corresponding \isacommand{show}.}
    70 *};
    71 
    72 theorem "EX S. S ~: range (f :: 'a => 'a set)";
    73 proof;
    74   let ?S = "{x. x ~: f x}";
    75   show "?S ~: range f";
    76   proof;
    77     assume "?S : range f";
    78     thus False;
    79     proof;
    80       fix y; 
    81       assume "?S = f y";
    82       thus ?thesis;
    83       proof (rule equalityCE);
    84         assume "y : f y";
    85         assume "y : ?S"; hence "y ~: f y"; ..;
    86         thus ?thesis; by contradiction;
    87       next;
    88         assume "y ~: f y";
    89         assume "y ~: ?S"; hence "y : f y"; ..;
    90         thus ?thesis; by contradiction;
    91       qed;
    92     qed;
    93   qed;
    94 qed;
    95 
    96 text {*
    97  How much creativity is required?  As it happens, Isabelle can prove
    98  this theorem automatically.  The context of Isabelle's classical
    99  prover contains rules for most of the constructs of HOL's set theory.
   100  We must augment it with \name{equalityCE} to break up set equalities,
   101  and then apply best-first search.  Depth-first search would diverge,
   102  but best-first search successfully navigates through the large search
   103  space.
   104 *};
   105 
   106 theorem "EX S. S ~: range (f :: 'a => 'a set)";
   107   by (best elim: equalityCE);
   108 
   109 text {*
   110  While this establishes the same theorem internally, we do not get any
   111  idea of how the proof actually works.  There is currently no way to
   112  transform internal system-level representations of Isabelle proofs
   113  back into Isar text.  Writing intelligible proof documents
   114  really is a creative process, after all.
   115 *};
   116 
   117 end;