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;
     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