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