src/HOL/Isar_examples/Cantor.thy
 author wenzelm Sun Sep 17 22:19:02 2000 +0200 (2000-09-17) changeset 10007 64bf7da1994a parent 9474 b0ce3b7c9c26 child 12388 c845fec1ac94 permissions -rw-r--r--
isar-strip-terminators;
 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@10007  6 header {* Cantor's Theorem *}  wenzelm@6444  7 wenzelm@10007  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@10007  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@10007  31 *}  wenzelm@6505  32 wenzelm@10007  33 theorem "EX S. S ~: range (f :: 'a => 'a set)"  wenzelm@10007  34 proof  wenzelm@10007  35  let ?S = "{x. x ~: f x}"  wenzelm@10007  36  show "?S ~: range f"  wenzelm@10007  37  proof  wenzelm@10007  38  assume "?S : range f"  wenzelm@10007  39  thus False  wenzelm@10007  40  proof  wenzelm@10007  41  fix y  wenzelm@10007  42  assume "?S = f y"  wenzelm@10007  43  thus ?thesis  wenzelm@10007  44  proof (rule equalityCE)  wenzelm@10007  45  assume in_S: "y : ?S"  wenzelm@10007  46  assume in_fy: "y : f y"  wenzelm@10007  47  from in_S have notin_fy: "y ~: f y" ..  wenzelm@10007  48  from notin_fy in_fy show ?thesis by contradiction  wenzelm@10007  49  next  wenzelm@10007  50  assume notin_S: "y ~: ?S"  wenzelm@10007  51  assume notin_fy: "y ~: f y"  wenzelm@10007  52  from notin_S have in_fy: "y : f y" ..  wenzelm@10007  53  from notin_fy in_fy show ?thesis by contradiction  wenzelm@10007  54  qed  wenzelm@10007  55  qed  wenzelm@10007  56  qed  wenzelm@10007  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@10007  70 *}  wenzelm@6494  71 wenzelm@10007  72 theorem "EX S. S ~: range (f :: 'a => 'a set)"  wenzelm@10007  73 proof  wenzelm@10007  74  let ?S = "{x. x ~: f x}"  wenzelm@10007  75  show "?S ~: range f"  wenzelm@10007  76  proof  wenzelm@10007  77  assume "?S : range f"  wenzelm@10007  78  thus False  wenzelm@10007  79  proof  wenzelm@10007  80  fix y  wenzelm@10007  81  assume "?S = f y"  wenzelm@10007  82  thus ?thesis  wenzelm@10007  83  proof (rule equalityCE)  wenzelm@10007  84  assume "y : f y"  wenzelm@10007  85  assume "y : ?S" hence "y ~: f y" ..  wenzelm@10007  86  thus ?thesis by contradiction  wenzelm@10007  87  next  wenzelm@10007  88  assume "y ~: f y"  wenzelm@10007  89  assume "y ~: ?S" hence "y : f y" ..  wenzelm@10007  90  thus ?thesis by contradiction  wenzelm@10007  91  qed  wenzelm@10007  92  qed  wenzelm@10007  93  qed  wenzelm@10007  94 qed  wenzelm@6494  95 wenzelm@6744  96 text {*  wenzelm@7819  97  How much creativity is required? As it happens, Isabelle can prove  wenzelm@9474  98  this theorem automatically using best-first search. Depth-first  wenzelm@9474  99  search would diverge, but best-first search successfully navigates  wenzelm@9474  100  through the large search space. The context of Isabelle's classical  wenzelm@9474  101  prover contains rules for the relevant constructs of HOL's set  wenzelm@9474  102  theory.  wenzelm@10007  103 *}  wenzelm@6505  104 wenzelm@10007  105 theorem "EX S. S ~: range (f :: 'a => 'a set)"  wenzelm@10007  106  by best  wenzelm@6494  107 wenzelm@6744  108 text {*  wenzelm@7819  109  While this establishes the same theorem internally, we do not get any  wenzelm@7819  110  idea of how the proof actually works. There is currently no way to  wenzelm@7819  111  transform internal system-level representations of Isabelle proofs  wenzelm@7982  112  back into Isar text. Writing intelligible proof documents  wenzelm@7874  113  really is a creative process, after all.  wenzelm@10007  114 *}  wenzelm@6444  115 wenzelm@10007  116 end