src/HOL/Isar_examples/Cantor.thy
 author wenzelm Fri Oct 15 16:44:37 1999 +0200 (1999-10-15) changeset 7874 180364256231 parent 7869 c007f801cd59 child 7955 f30e08579481 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@6444  5 wenzelm@7800  6 header {* Cantor's Theorem *};  wenzelm@6444  7 wenzelm@7869  8 theory Cantor = Main:;text_raw {* \footnote{This is an Isar version of  wenzelm@7833  9  the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}  wenzelm@7819  10 *};  wenzelm@7819  11 wenzelm@7819  12 text {*  wenzelm@7819  13  Cantor's Theorem states that every set has more subsets than it has  wenzelm@7819  14  elements. It has become a favorite basic example in pure  wenzelm@7819  15  higher-order logic since it is so easily expressed: $\all{f::\alpha  wenzelm@7819  16  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}  wenzelm@7874  17  \all{x::\alpha} f \ap x \not= S$  wenzelm@7748  18   wenzelm@7819  19  Viewing types as sets, $\alpha \To \idt{bool}$ represents the  wenzelm@7819  20  powerset of $\alpha$. This version of the theorem states that for  wenzelm@7819  21  every function from $\alpha$ to its powerset, some subset is outside  wenzelm@7860  22  its range. The Isabelle/Isar proofs below uses HOL's set theory,  wenzelm@7874  23  with the type $\alpha \ap \idt{set}$ and the operator  wenzelm@7874  24  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.  wenzelm@7748  25   wenzelm@7860  26  \bigskip We first consider a slightly awkward version of the proof,  wenzelm@7874  27  with the innermost reasoning expressed quite naively.  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@7860  36  thus False;  wenzelm@6494  37  proof;  wenzelm@6494  38  fix y;  wenzelm@7480  39  assume "?S = f y";  wenzelm@7860  40  thus ?thesis;  wenzelm@6494  41  proof (rule equalityCE);  wenzelm@7860  42  assume in_S: "y : ?S";  wenzelm@7860  43  assume in_fy: "y : f y";  wenzelm@7860  44  from in_S; have notin_fy: "y ~: f y"; ..;  wenzelm@7860  45  from notin_fy in_fy; show ?thesis; by contradiction;  wenzelm@6494  46  next;  wenzelm@7860  47  assume notin_S: "y ~: ?S";  wenzelm@7860  48  assume notin_fy: "y ~: f y";  wenzelm@7860  49  from notin_S; have in_fy: "y : f y"; ..;  wenzelm@7860  50  from notin_fy 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@7819  57  The following version of the proof essentially does the same  wenzelm@7860  58  reasoning, only that it is expressed more neatly. In particular, we  wenzelm@7860  59  change the order of assumptions introduced in the two cases of rule  wenzelm@7860  60  \name{equalityCE}, streamlining the flow of intermediate facts and  wenzelm@7860  61  avoiding explicit naming.\footnote{In general, neither the order of  wenzelm@7874  62  assumptions as introduced by \isacommand{assume}, nor the order of  wenzelm@7874  63  goals as solved by \isacommand{show} is of any significance. The  wenzelm@7874  64  basic logical structure has to be left intact, though. In  wenzelm@7874  65  particular, assumptions belonging'' to some goal have to be  wenzelm@7874  66  introduced \emph{before} its corresponding \isacommand{show}.}  wenzelm@6744  67 *};  wenzelm@6494  68 wenzelm@6494  69 theorem "EX S. S ~: range(f :: 'a => 'a set)";  wenzelm@6494  70 proof;  wenzelm@7480  71  let ?S = "{x. x ~: f x}";  wenzelm@7480  72  show "?S ~: range f";  wenzelm@6494  73  proof;  wenzelm@7480  74  assume "?S : range f";  wenzelm@6505  75  thus False;  wenzelm@6494  76  proof;  wenzelm@6494  77  fix y;  wenzelm@7480  78  assume "?S = f y";  wenzelm@7480  79  thus ?thesis;  wenzelm@6494  80  proof (rule equalityCE);  wenzelm@6494  81  assume "y : f y";  wenzelm@7480  82  assume "y : ?S"; hence "y ~: f y"; ..;  wenzelm@7480  83  thus ?thesis; by contradiction;  wenzelm@6494  84  next;  wenzelm@6494  85  assume "y ~: f y";  wenzelm@7480  86  assume "y ~: ?S"; hence "y : f y"; ..;  wenzelm@7480  87  thus ?thesis; by contradiction;  wenzelm@6494  88  qed;  wenzelm@6494  89  qed;  wenzelm@6494  90  qed;  wenzelm@6494  91 qed;  wenzelm@6494  92 wenzelm@6744  93 text {*  wenzelm@7819  94  How much creativity is required? As it happens, Isabelle can prove  wenzelm@7874  95  this theorem automatically. The default context of the Isabelle's  wenzelm@7874  96  classical prover contains rules for most of the constructs of HOL's  wenzelm@7874  97  set theory. We must augment it with \name{equalityCE} to break up  wenzelm@7874  98  set equalities, and then apply best-first search. Depth-first search  wenzelm@7860  99  would diverge, but best-first search successfully navigates through  wenzelm@7860  100  the large search 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@7819  107  While this establishes the same theorem internally, we do not get any  wenzelm@7819  108  idea of how the proof actually works. There is currently no way to  wenzelm@7819  109  transform internal system-level representations of Isabelle proofs  wenzelm@7874  110  back into Isar documents. Writing intelligible proof documents  wenzelm@7874  111  really is a creative process, after all.  wenzelm@6744  112 *};  wenzelm@6444  113 wenzelm@6444  114 end;