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