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