src/HOL/Isar_examples/Cantor.thy
 author wenzelm Wed Jun 13 18:30:11 2007 +0200 (2007-06-13) changeset 23373 ead82c82da9e parent 16417 9bc16273c2d4 child 31758 3edd5f813f01 permissions -rw-r--r--
tuned proofs: avoid implicit prems;
 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 haftmann@16417  8 theory Cantor imports Main begin  wenzelm@7955  9 wenzelm@7955  10 text_raw {*  wenzelm@12388  11  \footnote{This is an Isar version of the final example of the  wenzelm@12388  12  Isabelle/HOL manual \cite{isabelle-HOL}.}  wenzelm@10007  13 *}  wenzelm@7819  14 wenzelm@7819  15 text {*  wenzelm@12388  16  Cantor's Theorem states that every set has more subsets than it has  wenzelm@12388  17  elements. It has become a favorite basic example in pure  wenzelm@12388  18  higher-order logic since it is so easily expressed: $\all{f::\alpha  wenzelm@12388  19  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}  wenzelm@12388  20  \all{x::\alpha} f \ap x \not= S$  wenzelm@12388  21 wenzelm@12388  22  Viewing types as sets, $\alpha \To \idt{bool}$ represents the  wenzelm@12388  23  powerset of $\alpha$. This version of the theorem states that for  wenzelm@12388  24  every function from $\alpha$ to its powerset, some subset is outside  wenzelm@12388  25  its range. The Isabelle/Isar proofs below uses HOL's set theory,  wenzelm@12388  26  with the type $\alpha \ap \idt{set}$ and the operator  wenzelm@12388  27  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.  wenzelm@10007  28 *}  wenzelm@6505  29 wenzelm@10007  30 theorem "EX S. S ~: range (f :: 'a => 'a set)"  wenzelm@10007  31 proof  wenzelm@10007  32  let ?S = "{x. x ~: f x}"  wenzelm@10007  33  show "?S ~: range f"  wenzelm@10007  34  proof  wenzelm@10007  35  assume "?S : range f"  wenzelm@12388  36  then obtain y where "?S = f y" ..  wenzelm@23373  37  then show False  wenzelm@12388  38  proof (rule equalityCE)  wenzelm@12388  39  assume "y : f y"  wenzelm@23373  40  assume "y : ?S" then have "y ~: f y" ..  wenzelm@23373  41  with y : f y show ?thesis by contradiction  wenzelm@12388  42  next  wenzelm@12388  43  assume "y ~: ?S"  wenzelm@23373  44  assume "y ~: f y" then have "y : ?S" ..  wenzelm@23373  45  with y ~: ?S show ?thesis by contradiction  wenzelm@10007  46  qed  wenzelm@10007  47  qed  wenzelm@10007  48 qed  wenzelm@6494  49 wenzelm@6744  50 text {*  wenzelm@12388  51  How much creativity is required? As it happens, Isabelle can prove  wenzelm@12388  52  this theorem automatically using best-first search. Depth-first  wenzelm@12388  53  search would diverge, but best-first search successfully navigates  wenzelm@12388  54  through the large search space. The context of Isabelle's classical  wenzelm@12388  55  prover contains rules for the relevant constructs of HOL's set  wenzelm@12388  56  theory.  wenzelm@10007  57 *}  wenzelm@6505  58 wenzelm@10007  59 theorem "EX S. S ~: range (f :: 'a => 'a set)"  wenzelm@10007  60  by best  wenzelm@6494  61 wenzelm@6744  62 text {*  wenzelm@12388  63  While this establishes the same theorem internally, we do not get  wenzelm@12388  64  any idea of how the proof actually works. There is currently no way  wenzelm@12388  65  to transform internal system-level representations of Isabelle  wenzelm@12388  66  proofs back into Isar text. Writing intelligible proof documents  wenzelm@12388  67  really is a creative process, after all.  wenzelm@10007  68 *}  wenzelm@6444  69 wenzelm@10007  70 end