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