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 ?;
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@6444
     9
theory Cantor = Main:;
wenzelm@6444
    10
wenzelm@6494
    11
wenzelm@6746
    12
section {* Example: Cantor's Theorem *};
wenzelm@6505
    13
wenzelm@6744
    14
text {*
wenzelm@6505
    15
  Cantor's Theorem states that every set has more subsets than it has
wenzelm@6505
    16
  elements.  It has become a favourite example in higher-order logic
wenzelm@6505
    17
  since it is so easily expressed: @{display term[show_types] "ALL f
wenzelm@6505
    18
  :: 'a => 'a => bool. EX S :: 'a => bool. ALL x::'a. f x ~= S"}
wenzelm@6505
    19
wenzelm@6505
    20
  Viewing types as sets, @{type "'a => bool"} represents the powerset
wenzelm@6505
    21
  of @{type 'a}.  This version states that for every function from
wenzelm@6505
    22
  @{type 'a} to its powerset, some subset is outside its range.
wenzelm@6505
    23
wenzelm@6505
    24
  The Isabelle/Isar proofs below use HOL's set theory, with the type
wenzelm@6505
    25
  @{type "'a set"} and the operator @{term range}.
wenzelm@6744
    26
*};
wenzelm@6505
    27
wenzelm@6506
    28
wenzelm@6744
    29
text {*
wenzelm@6505
    30
  We first consider a rather verbose version of the proof, with the
wenzelm@6505
    31
  reasoning expressed quite naively.  We only make use of the pure
wenzelm@6505
    32
  core of the Isar proof language.
wenzelm@6744
    33
*};
wenzelm@6505
    34
wenzelm@6494
    35
theorem "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6494
    36
proof;
wenzelm@7480
    37
  let ?S = "{x. x ~: f x}";
wenzelm@7480
    38
  show "?S ~: range f";
wenzelm@6494
    39
  proof;
wenzelm@7480
    40
    assume "?S : range f";
wenzelm@6494
    41
    then; show False;
wenzelm@6494
    42
    proof;
wenzelm@6494
    43
      fix y; 
wenzelm@7480
    44
      assume "?S = f y";
wenzelm@7480
    45
      then; show ?thesis;
wenzelm@6494
    46
      proof (rule equalityCE);
wenzelm@7480
    47
        assume y_in_S: "y : ?S";
wenzelm@6494
    48
        assume y_in_fy: "y : f y";
wenzelm@6494
    49
        from y_in_S; have y_notin_fy: "y ~: f y"; ..;
wenzelm@7480
    50
        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
wenzelm@6494
    51
      next;
wenzelm@7480
    52
        assume y_notin_S: "y ~: ?S";
wenzelm@6494
    53
        assume y_notin_fy: "y ~: f y";
wenzelm@6494
    54
        from y_notin_S; have y_in_fy: "y : f y"; ..;
wenzelm@7480
    55
        from y_notin_fy y_in_fy; show ?thesis; by contradiction;
wenzelm@6494
    56
      qed;
wenzelm@6494
    57
    qed;
wenzelm@6494
    58
  qed;
wenzelm@6494
    59
qed;
wenzelm@6494
    60
wenzelm@6506
    61
wenzelm@6744
    62
text {*
wenzelm@6505
    63
  The following version essentially does the same reasoning, only that
wenzelm@6505
    64
  it is expressed more neatly, with some derived Isar language
wenzelm@6505
    65
  elements involved.
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@6494
    92
wenzelm@6744
    93
text {*
wenzelm@6505
    94
  How much creativity is required?  As it happens, Isabelle can prove
wenzelm@6505
    95
  this theorem automatically.  The default classical set contains
wenzelm@6505
    96
  rules for most of the constructs of HOL's set theory.  We must
wenzelm@6505
    97
  augment it with @{thm equalityCE} to break up set equalities, and
wenzelm@6505
    98
  then apply best-first search.  Depth-first search would diverge, but
wenzelm@6505
    99
  best-first search successfully navigates through the large search
wenzelm@6505
   100
  space.
wenzelm@6744
   101
*};
wenzelm@6505
   102
wenzelm@6494
   103
theorem "EX S. S ~: range(f :: 'a => 'a set)";
wenzelm@6494
   104
  by (best elim: equalityCE);
wenzelm@6494
   105
wenzelm@6744
   106
text {*
wenzelm@6505
   107
  While this establishes the same theorem internally, we do not get
wenzelm@6506
   108
  any idea of how the proof actually works.  There is currently no way
wenzelm@6506
   109
  to transform internal system-level representations of Isabelle
wenzelm@6506
   110
  proofs back into Isar documents.  Writing Isabelle/Isar proof
wenzelm@6507
   111
  documents actually \emph{is} a creative process.
wenzelm@6744
   112
*};
wenzelm@6444
   113
wenzelm@6506
   114
wenzelm@6444
   115
end;