src/HOL/Isar_examples/Cantor.thy
author wenzelm
Thu Oct 14 01:07:24 1999 +0200 (1999-10-14)
changeset 7860 7819547df4d8
parent 7833 f5288e4b95d1
child 7869 c007f801cd59
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@6444
     5
wenzelm@7800
     6
header {* Cantor's Theorem *};
wenzelm@6444
     7
wenzelm@7833
     8
theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
wenzelm@7833
     9
 the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
wenzelm@7819
    10
*};
wenzelm@7819
    11
wenzelm@7819
    12
text {*
wenzelm@7819
    13
 Cantor's Theorem states that every set has more subsets than it has
wenzelm@7819
    14
 elements.  It has become a favorite basic example in pure
wenzelm@7819
    15
 higher-order logic since it is so easily expressed: \[\all{f::\alpha
wenzelm@7819
    16
 \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
wenzelm@7819
    17
 \all{x::\alpha}. f \ap x \not= S\]
wenzelm@7748
    18
  
wenzelm@7819
    19
 Viewing types as sets, $\alpha \To \idt{bool}$ represents the
wenzelm@7819
    20
 powerset of $\alpha$.  This version of the theorem states that for
wenzelm@7819
    21
 every function from $\alpha$ to its powerset, some subset is outside
wenzelm@7860
    22
 its range.  The Isabelle/Isar proofs below uses HOL's set theory,
wenzelm@7860
    23
 with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
wenzelm@7748
    24
  
wenzelm@7860
    25
 \bigskip We first consider a slightly awkward version of the proof,
wenzelm@7860
    26
 with the reasoning expressed quite naively.
wenzelm@6744
    27
*};
wenzelm@6505
    28
wenzelm@6494
    29
theorem "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6494
    30
proof;
wenzelm@7480
    31
  let ?S = "{x. x ~: f x}";
wenzelm@7480
    32
  show "?S ~: range f";
wenzelm@6494
    33
  proof;
wenzelm@7480
    34
    assume "?S : range f";
wenzelm@7860
    35
    thus False;
wenzelm@6494
    36
    proof;
wenzelm@6494
    37
      fix y; 
wenzelm@7480
    38
      assume "?S = f y";
wenzelm@7860
    39
      thus ?thesis;
wenzelm@6494
    40
      proof (rule equalityCE);
wenzelm@7860
    41
        assume in_S: "y : ?S";
wenzelm@7860
    42
        assume in_fy: "y : f y";
wenzelm@7860
    43
        from in_S; have notin_fy: "y ~: f y"; ..;
wenzelm@7860
    44
        from notin_fy in_fy; show ?thesis; by contradiction;
wenzelm@6494
    45
      next;
wenzelm@7860
    46
        assume notin_S: "y ~: ?S";
wenzelm@7860
    47
        assume notin_fy: "y ~: f y";
wenzelm@7860
    48
        from notin_S; have in_fy: "y : f y"; ..;
wenzelm@7860
    49
        from notin_fy in_fy; show ?thesis; by contradiction;
wenzelm@6494
    50
      qed;
wenzelm@6494
    51
    qed;
wenzelm@6494
    52
  qed;
wenzelm@6494
    53
qed;
wenzelm@6494
    54
wenzelm@6744
    55
text {*
wenzelm@7819
    56
 The following version of the proof essentially does the same
wenzelm@7860
    57
 reasoning, only that it is expressed more neatly.  In particular, we
wenzelm@7860
    58
 change the order of assumptions introduced in the two cases of rule
wenzelm@7860
    59
 \name{equalityCE}, streamlining the flow of intermediate facts and
wenzelm@7860
    60
 avoiding explicit naming.\footnote{In general, neither the order of
wenzelm@7860
    61
 assumptions as introduced \isacommand{assume}, nor the order of goals
wenzelm@7860
    62
 as solved by \isacommand{show} matters.  The basic logical structure
wenzelm@7860
    63
 has to be left intact, though.  In particular, assumptions
wenzelm@7860
    64
 ``belonging'' to some goal have to be introduced \emph{before} its
wenzelm@7860
    65
 corresponding \isacommand{show}.}
wenzelm@6744
    66
*};
wenzelm@6494
    67
wenzelm@6494
    68
theorem "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6494
    69
proof;
wenzelm@7480
    70
  let ?S = "{x. x ~: f x}";
wenzelm@7480
    71
  show "?S ~: range f";
wenzelm@6494
    72
  proof;
wenzelm@7480
    73
    assume "?S : range f";
wenzelm@6505
    74
    thus False;
wenzelm@6494
    75
    proof;
wenzelm@6494
    76
      fix y; 
wenzelm@7480
    77
      assume "?S = f y";
wenzelm@7480
    78
      thus ?thesis;
wenzelm@6494
    79
      proof (rule equalityCE);
wenzelm@6494
    80
        assume "y : f y";
wenzelm@7480
    81
        assume "y : ?S"; hence "y ~: f y"; ..;
wenzelm@7480
    82
        thus ?thesis; by contradiction;
wenzelm@6494
    83
      next;
wenzelm@6494
    84
        assume "y ~: f y";
wenzelm@7480
    85
        assume "y ~: ?S"; hence "y : f y"; ..;
wenzelm@7480
    86
        thus ?thesis; by contradiction;
wenzelm@6494
    87
      qed;
wenzelm@6494
    88
    qed;
wenzelm@6494
    89
  qed;
wenzelm@6494
    90
qed;
wenzelm@6494
    91
wenzelm@6744
    92
text {*
wenzelm@7819
    93
 How much creativity is required?  As it happens, Isabelle can prove
wenzelm@7860
    94
 this theorem automatically.  The default context of the classical
wenzelm@7860
    95
 proof tools contains rules for most of the constructs of HOL's set
wenzelm@7860
    96
 theory.  We must augment it with \name{equalityCE} to break up set
wenzelm@7860
    97
 equalities, and then apply best-first search.  Depth-first search
wenzelm@7860
    98
 would diverge, but best-first search successfully navigates through
wenzelm@7860
    99
 the large search space.
wenzelm@6744
   100
*};
wenzelm@6505
   101
wenzelm@6494
   102
theorem "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6494
   103
  by (best elim: equalityCE);
wenzelm@6494
   104
wenzelm@6744
   105
text {*
wenzelm@7819
   106
 While this establishes the same theorem internally, we do not get any
wenzelm@7819
   107
 idea of how the proof actually works.  There is currently no way to
wenzelm@7819
   108
 transform internal system-level representations of Isabelle proofs
wenzelm@7819
   109
 back into Isar documents.  Writing proof documents really is a
wenzelm@7860
   110
 creative process, after all.
wenzelm@6744
   111
*};
wenzelm@6444
   112
wenzelm@6444
   113
end;