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