src/HOL/Isar_examples/Cantor.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 12388 c845fec1ac94
child 23373 ead82c82da9e
permissions -rw-r--r--
migrated theory headers to new format
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@10007
    37
    thus False
wenzelm@12388
    38
    proof (rule equalityCE)
wenzelm@12388
    39
      assume "y : f y"
wenzelm@12388
    40
      assume "y : ?S" hence "y ~: f y" ..
wenzelm@12388
    41
      thus ?thesis by contradiction
wenzelm@12388
    42
    next
wenzelm@12388
    43
      assume "y ~: ?S"
wenzelm@12388
    44
      assume "y ~: f y" hence "y : ?S" ..
wenzelm@12388
    45
      thus ?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