src/HOL/Isar_examples/Cantor.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 6746 cf6ad8d22793
child 7748 5b9c45b21782
permissions -rw-r--r--
replaced ?? by ?;
     1 (*  Title:      HOL/Isar_examples/Cantor.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Cantor's theorem -- Isar'ized version of the final section of the HOL
     6 chapter of "Isabelle's Object-Logics" (Larry Paulson).
     7 *)
     8 
     9 theory Cantor = Main:;
    10 
    11 
    12 section {* Example: Cantor's Theorem *};
    13 
    14 text {*
    15   Cantor's Theorem states that every set has more subsets than it has
    16   elements.  It has become a favourite example in higher-order logic
    17   since it is so easily expressed: @{display term[show_types] "ALL f
    18   :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"}
    19 
    20   Viewing types as sets, @{type "'a => bool"} represents the powerset
    21   of @{type 'a}.  This version states that for every function from
    22   @{type 'a} to its powerset, some subset is outside its range.
    23 
    24   The Isabelle/Isar proofs below use HOL's set theory, with the type
    25   @{type "'a set"} and the operator @{term range}.
    26 *};
    27 
    28 
    29 text {*
    30   We first consider a rather verbose version of the proof, with the
    31   reasoning expressed quite naively.  We only make use of the pure
    32   core of the Isar proof language.
    33 *};
    34 
    35 theorem "EX S. S ~: range(f :: 'a => 'a set)";
    36 proof;
    37   let ?S = "{x. x ~: f x}";
    38   show "?S ~: range f";
    39   proof;
    40     assume "?S : range f";
    41     then; show False;
    42     proof;
    43       fix y; 
    44       assume "?S = f y";
    45       then; show ?thesis;
    46       proof (rule equalityCE);
    47         assume y_in_S: "y : ?S";
    48         assume y_in_fy: "y : f y";
    49         from y_in_S; have y_notin_fy: "y ~: f y"; ..;
    50         from y_notin_fy y_in_fy; show ?thesis; by contradiction;
    51       next;
    52         assume y_notin_S: "y ~: ?S";
    53         assume y_notin_fy: "y ~: f y";
    54         from y_notin_S; have y_in_fy: "y : f y"; ..;
    55         from y_notin_fy y_in_fy; show ?thesis; by contradiction;
    56       qed;
    57     qed;
    58   qed;
    59 qed;
    60 
    61 
    62 text {*
    63   The following version essentially does the same reasoning, only that
    64   it is expressed more neatly, with some derived Isar language
    65   elements involved.
    66 *};
    67 
    68 theorem "EX S. S ~: range(f :: 'a => 'a set)";
    69 proof;
    70   let ?S = "{x. x ~: f x}";
    71   show "?S ~: range f";
    72   proof;
    73     assume "?S : range f";
    74     thus False;
    75     proof;
    76       fix y; 
    77       assume "?S = f y";
    78       thus ?thesis;
    79       proof (rule equalityCE);
    80         assume "y : f y";
    81         assume "y : ?S"; hence "y ~: f y"; ..;
    82         thus ?thesis; by contradiction;
    83       next;
    84         assume "y ~: f y";
    85         assume "y ~: ?S"; hence "y : f y"; ..;
    86         thus ?thesis; by contradiction;
    87       qed;
    88     qed;
    89   qed;
    90 qed;
    91 
    92 
    93 text {*
    94   How much creativity is required?  As it happens, Isabelle can prove
    95   this theorem automatically.  The default classical set contains
    96   rules for most of the constructs of HOL's set theory.  We must
    97   augment it with @{thm equalityCE} to break up set equalities, and
    98   then apply best-first search.  Depth-first search would diverge, but
    99   best-first search successfully navigates through the large search
   100   space.
   101 *};
   102 
   103 theorem "EX S. S ~: range(f :: 'a => 'a set)";
   104   by (best elim: equalityCE);
   105 
   106 text {*
   107   While this establishes the same theorem internally, we do not get
   108   any idea of how the proof actually works.  There is currently no way
   109   to transform internal system-level representations of Isabelle
   110   proofs back into Isar documents.  Writing Isabelle/Isar proof
   111   documents actually \emph{is} a creative process.
   112 *};
   113 
   114 
   115 end;