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