src/HOL/Isar_examples/Cantor.thy
author wenzelm
Sun Sep 17 22:19:02 2000 +0200 (2000-09-17)
changeset 10007 64bf7da1994a
parent 9474 b0ce3b7c9c26
child 12388 c845fec1ac94
permissions -rw-r--r--
isar-strip-terminators;
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@10007
     6
header {* Cantor's Theorem *}
wenzelm@6444
     7
wenzelm@10007
     8
theory Cantor = Main:
wenzelm@7955
     9
wenzelm@7955
    10
text_raw {*
wenzelm@7955
    11
 \footnote{This is an Isar version of the final example of the
wenzelm@7955
    12
 Isabelle/HOL manual \cite{isabelle-HOL}.}
wenzelm@10007
    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@7874
    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@7860
    25
 its range.  The Isabelle/Isar proofs below uses HOL's set theory,
wenzelm@7874
    26
 with the type $\alpha \ap \idt{set}$ and the operator
wenzelm@7874
    27
 $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
wenzelm@7748
    28
  
wenzelm@7860
    29
 \bigskip We first consider a slightly awkward version of the proof,
wenzelm@7874
    30
 with the innermost reasoning expressed quite naively.
wenzelm@10007
    31
*}
wenzelm@6505
    32
wenzelm@10007
    33
theorem "EX S. S ~: range (f :: 'a => 'a set)"
wenzelm@10007
    34
proof
wenzelm@10007
    35
  let ?S = "{x. x ~: f x}"
wenzelm@10007
    36
  show "?S ~: range f"
wenzelm@10007
    37
  proof
wenzelm@10007
    38
    assume "?S : range f"
wenzelm@10007
    39
    thus False
wenzelm@10007
    40
    proof
wenzelm@10007
    41
      fix y 
wenzelm@10007
    42
      assume "?S = f y"
wenzelm@10007
    43
      thus ?thesis
wenzelm@10007
    44
      proof (rule equalityCE)
wenzelm@10007
    45
        assume in_S: "y : ?S"
wenzelm@10007
    46
        assume in_fy: "y : f y"
wenzelm@10007
    47
        from in_S have notin_fy: "y ~: f y" ..
wenzelm@10007
    48
        from notin_fy in_fy show ?thesis by contradiction
wenzelm@10007
    49
      next
wenzelm@10007
    50
        assume notin_S: "y ~: ?S"
wenzelm@10007
    51
        assume notin_fy: "y ~: f y"
wenzelm@10007
    52
        from notin_S have in_fy: "y : f y" ..
wenzelm@10007
    53
        from notin_fy in_fy show ?thesis by contradiction
wenzelm@10007
    54
      qed
wenzelm@10007
    55
    qed
wenzelm@10007
    56
  qed
wenzelm@10007
    57
qed
wenzelm@6494
    58
wenzelm@6744
    59
text {*
wenzelm@7819
    60
 The following version of the proof essentially does the same
wenzelm@7860
    61
 reasoning, only that it is expressed more neatly.  In particular, we
wenzelm@7860
    62
 change the order of assumptions introduced in the two cases of rule
wenzelm@7860
    63
 \name{equalityCE}, streamlining the flow of intermediate facts and
wenzelm@7860
    64
 avoiding explicit naming.\footnote{In general, neither the order of
wenzelm@7874
    65
 assumptions as introduced by \isacommand{assume}, nor the order of
wenzelm@7874
    66
 goals as solved by \isacommand{show} is of any significance.  The
wenzelm@7874
    67
 basic logical structure has to be left intact, though.  In
wenzelm@7874
    68
 particular, assumptions ``belonging'' to some goal have to be
wenzelm@7874
    69
 introduced \emph{before} its corresponding \isacommand{show}.}
wenzelm@10007
    70
*}
wenzelm@6494
    71
wenzelm@10007
    72
theorem "EX S. S ~: range (f :: 'a => 'a set)"
wenzelm@10007
    73
proof
wenzelm@10007
    74
  let ?S = "{x. x ~: f x}"
wenzelm@10007
    75
  show "?S ~: range f"
wenzelm@10007
    76
  proof
wenzelm@10007
    77
    assume "?S : range f"
wenzelm@10007
    78
    thus False
wenzelm@10007
    79
    proof
wenzelm@10007
    80
      fix y 
wenzelm@10007
    81
      assume "?S = f y"
wenzelm@10007
    82
      thus ?thesis
wenzelm@10007
    83
      proof (rule equalityCE)
wenzelm@10007
    84
        assume "y : f y"
wenzelm@10007
    85
        assume "y : ?S" hence "y ~: f y" ..
wenzelm@10007
    86
        thus ?thesis by contradiction
wenzelm@10007
    87
      next
wenzelm@10007
    88
        assume "y ~: f y"
wenzelm@10007
    89
        assume "y ~: ?S" hence "y : f y" ..
wenzelm@10007
    90
        thus ?thesis by contradiction
wenzelm@10007
    91
      qed
wenzelm@10007
    92
    qed
wenzelm@10007
    93
  qed
wenzelm@10007
    94
qed
wenzelm@6494
    95
wenzelm@6744
    96
text {*
wenzelm@7819
    97
 How much creativity is required?  As it happens, Isabelle can prove
wenzelm@9474
    98
 this theorem automatically using best-first search.  Depth-first
wenzelm@9474
    99
 search would diverge, but best-first search successfully navigates
wenzelm@9474
   100
 through the large search space.  The context of Isabelle's classical
wenzelm@9474
   101
 prover contains rules for the relevant constructs of HOL's set
wenzelm@9474
   102
 theory.
wenzelm@10007
   103
*}
wenzelm@6505
   104
wenzelm@10007
   105
theorem "EX S. S ~: range (f :: 'a => 'a set)"
wenzelm@10007
   106
  by best
wenzelm@6494
   107
wenzelm@6744
   108
text {*
wenzelm@7819
   109
 While this establishes the same theorem internally, we do not get any
wenzelm@7819
   110
 idea of how the proof actually works.  There is currently no way to
wenzelm@7819
   111
 transform internal system-level representations of Isabelle proofs
wenzelm@7982
   112
 back into Isar text.  Writing intelligible proof documents
wenzelm@7874
   113
 really is a creative process, after all.
wenzelm@10007
   114
*}
wenzelm@6444
   115
wenzelm@10007
   116
end