src/HOL/Isar_examples/Cantor.thy
 author wenzelm Fri Oct 08 15:09:14 1999 +0200 (1999-10-08) changeset 7800 8ee919e42174 parent 7748 5b9c45b21782 child 7819 6dd018b6cf3f 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@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@7800  9 header {* Cantor's Theorem *};  wenzelm@6444  10 wenzelm@7748  11 theory Cantor = Main:;  wenzelm@6505  12 wenzelm@6744  13 text {*  wenzelm@6505  14  Cantor's Theorem states that every set has more subsets than it has  wenzelm@7800  15  elements. It has become a favorite basic example in pure  wenzelm@7800  16  higher-order logic since it is so easily expressed: $\all{f::\alpha  wenzelm@7800  17  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}  wenzelm@7800  18  \all{x::\alpha}. f \ap x \not= S$  wenzelm@7748  19   wenzelm@7748  20  Viewing types as sets, $\alpha \To \idt{bool}$ represents the powerset of  wenzelm@7748  21  $\alpha$. This version of the theorem states that for every function from  wenzelm@7748  22  $\alpha$ to its powerset, some subset is outside its range. The  wenzelm@7748  23  Isabelle/Isar proofs below use HOL's set theory, with the type $\alpha \ap  wenzelm@7748  24  \idt{set}$ and the operator $\idt{range}$.  wenzelm@7748  25   wenzelm@7748  26  \bigskip We first consider a rather verbose version of the proof, with the  wenzelm@7748  27  reasoning expressed quite naively. We only make use of the pure core of the  wenzelm@7748  28  Isar proof language.  wenzelm@6744  29 *};  wenzelm@6505  30 wenzelm@6494  31 theorem "EX S. S ~: range(f :: 'a => 'a set)";  wenzelm@6494  32 proof;  wenzelm@7480  33  let ?S = "{x. x ~: f x}";  wenzelm@7480  34  show "?S ~: range f";  wenzelm@6494  35  proof;  wenzelm@7480  36  assume "?S : range f";  wenzelm@6494  37  then; show False;  wenzelm@6494  38  proof;  wenzelm@6494  39  fix y;  wenzelm@7480  40  assume "?S = f y";  wenzelm@7480  41  then; show ?thesis;  wenzelm@6494  42  proof (rule equalityCE);  wenzelm@7480  43  assume y_in_S: "y : ?S";  wenzelm@6494  44  assume y_in_fy: "y : f y";  wenzelm@6494  45  from y_in_S; have y_notin_fy: "y ~: f y"; ..;  wenzelm@7480  46  from y_notin_fy y_in_fy; show ?thesis; by contradiction;  wenzelm@6494  47  next;  wenzelm@7480  48  assume y_notin_S: "y ~: ?S";  wenzelm@6494  49  assume y_notin_fy: "y ~: f y";  wenzelm@6494  50  from y_notin_S; have y_in_fy: "y : f y"; ..;  wenzelm@7480  51  from y_notin_fy y_in_fy; show ?thesis; by contradiction;  wenzelm@6494  52  qed;  wenzelm@6494  53  qed;  wenzelm@6494  54  qed;  wenzelm@6494  55 qed;  wenzelm@6494  56 wenzelm@6744  57 text {*  wenzelm@7748  58  The following version of the proof essentially does the same reasoning, only  wenzelm@7748  59  that it is expressed more neatly, with some derived Isar language elements  wenzelm@7748  60  involved.  wenzelm@6744  61 *};  wenzelm@6494  62 wenzelm@6494  63 theorem "EX S. S ~: range(f :: 'a => 'a set)";  wenzelm@6494  64 proof;  wenzelm@7480  65  let ?S = "{x. x ~: f x}";  wenzelm@7480  66  show "?S ~: range f";  wenzelm@6494  67  proof;  wenzelm@7480  68  assume "?S : range f";  wenzelm@6505  69  thus False;  wenzelm@6494  70  proof;  wenzelm@6494  71  fix y;  wenzelm@7480  72  assume "?S = f y";  wenzelm@7480  73  thus ?thesis;  wenzelm@6494  74  proof (rule equalityCE);  wenzelm@6494  75  assume "y : f y";  wenzelm@7480  76  assume "y : ?S"; hence "y ~: f y"; ..;  wenzelm@7480  77  thus ?thesis; by contradiction;  wenzelm@6494  78  next;  wenzelm@6494  79  assume "y ~: f y";  wenzelm@7480  80  assume "y ~: ?S"; hence "y : f y"; ..;  wenzelm@7480  81  thus ?thesis; by contradiction;  wenzelm@6494  82  qed;  wenzelm@6494  83  qed;  wenzelm@6494  84  qed;  wenzelm@6494  85 qed;  wenzelm@6494  86 wenzelm@6744  87 text {*  wenzelm@7748  88  How much creativity is required? As it happens, Isabelle can prove this  wenzelm@7748  89  theorem automatically. The default classical set contains rules for most of  wenzelm@7748  90  the constructs of HOL's set theory. We must augment it with  wenzelm@7748  91  \name{equalityCE} to break up set equalities, and then apply best-first  wenzelm@7748  92  search. Depth-first search would diverge, but best-first search  wenzelm@7748  93  successfully navigates through the large search space.  wenzelm@6744  94 *};  wenzelm@6505  95 wenzelm@6494  96 theorem "EX S. S ~: range(f :: 'a => 'a set)";  wenzelm@6494  97  by (best elim: equalityCE);  wenzelm@6494  98 wenzelm@6744  99 text {*  wenzelm@7748  100  While this establishes the same theorem internally, we do not get any idea  wenzelm@7748  101  of how the proof actually works. There is currently no way to transform  wenzelm@7748  102  internal system-level representations of Isabelle proofs back into Isar  wenzelm@7748  103  documents. Note that writing Isabelle/Isar proof documents actually  wenzelm@7748  104  \emph{is} a creative process.  wenzelm@6744  105 *};  wenzelm@6444  106 wenzelm@6444  107 end;