src/HOL/Isar_examples/Cantor.thy

subject to Multithreading.enabled;
raw_map: join sequentially, less overhead;

(*  Title:      HOL/Isar_examples/Cantor.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen
*)

header {* Cantor's Theorem *}

theory Cantor imports Main begin

text_raw {*
  \footnote{This is an Isar version of the final example of the
  Isabelle/HOL manual \cite{isabelle-HOL}.}
*}

text {*
  Cantor's Theorem states that every set has more subsets than it has
  elements.  It has become a favorite basic example in pure
  higher-order logic since it is so easily expressed: \[\all{f::\alpha
  \To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
  \all{x::\alpha} f \ap x \not= S\]

  Viewing types as sets, $\alpha \To \idt{bool}$ represents the
  powerset of $\alpha$.  This version of the theorem states that for
  every function from $\alpha$ to its powerset, some subset is outside
  its range.  The Isabelle/Isar proofs below uses HOL's set theory,
  with the type $\alpha \ap \idt{set}$ and the operator
  $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
*}

theorem "EX S. S ~: range (f :: 'a => 'a set)"
proof
  let ?S = "{x. x ~: f x}"
  show "?S ~: range f"
  proof
    assume "?S : range f"
    then obtain y where "?S = f y" ..
    then show False
    proof (rule equalityCE)
      assume "y : f y"
      assume "y : ?S" then have "y ~: f y" ..
      with `y : f y` show ?thesis by contradiction
    next
      assume "y ~: ?S"
      assume "y ~: f y" then have "y : ?S" ..
      with `y ~: ?S` show ?thesis by contradiction
    qed
  qed
qed

text {*
  How much creativity is required?  As it happens, Isabelle can prove
  this theorem automatically using best-first search.  Depth-first
  search would diverge, but best-first search successfully navigates
  through the large search space.  The context of Isabelle's classical
  prover contains rules for the relevant constructs of HOL's set
  theory.
*}

theorem "EX S. S ~: range (f :: 'a => 'a set)"
  by best

text {*
  While this establishes the same theorem internally, we do not get
  any idea of how the proof actually works.  There is currently no way
  to transform internal system-level representations of Isabelle
  proofs back into Isar text.  Writing intelligible proof documents
  really is a creative process, after all.
*}

end