Quelle  Cantor.thy   Sprache: Isabelle

(*  Title:      HOL/Examples/Cantor.thy
    Author:     Makarius
*)

section ‹Cantor's Theorem\

theory Cantor
  imports Main
begin

subsection ‹Mathematical statement and proof›

text ‹
  Cantor's Theorem states that there is no surjection from
  a set to its powerset.  The proof works by diagonalization.  E.g.\ see
  🚫 🚫‹http://mathworld.wolfram.com/CantorDiagonalMethod.html›
  🚫 🚫‹https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\
›

theorem Cantor: "\f :: 'a \ 'a set. \A. \x. A = f x"
proof
  assume "\f :: 'a \ 'a set. \A. \x. A = f x"
  then obtain f :: "'a \ 'a set" where *: "\A. \x. A = f x" ..
  let ?D = "{x. x \ f x}"
  from * obtain a where "?D = f a" by blast
  moreover have "a \ ?D \ a \ f a" by blast
  ultimately show False by blast
qed


subsection ‹Automated proofs›

text ‹
  These automated proofs are much shorter, but lack information why and how it
  works.
›

theorem "\f :: 'a \ 'a set. \A. \x. f x = A"
  by best

theorem "\f :: 'a \ 'a set. \A. \x. f x = A"
  by force


subsection ‹Elementary version in higher-order predicate logic›

text ‹
  The subsequent formulation bypasses set notation of HOL; it uses elementary
  ‹λ›-calculus and predicate logic, with standard introduction and elimination
  rules. This also shows that the proof does not require classical reasoning.
›

lemma iff_contradiction:
  assumes *: "\ A \ A"
  shows False
proof (rule notE)
  show "\ A"
  proof
    assume A
    with * have "\ A" ..
    from this and ‹A› show False ..
  qed
  with * show A ..
qed

theorem Cantor': "\f :: 'a ==> 'a \ bool. \A. \x. A = f x"
proof
  assume "\f :: 'a \ 'a \ bool. \A. \x. A = f x"
  then obtain f :: "'a \ 'a \ bool" where *: "\A. \x. A = f x" ..
  let ?D = "\x. \ f x x"
  from * have "\x. ?D = f x" ..
  then obtain a where "?D = f a" ..
  then have "?D a \ f a a" by (rule arg_cong)
  then have "\ f a a \ f a a" .
  then show False by (rule iff_contradiction)
qed


subsection ‹Classic Isabelle/HOL example›

text ‹
  The following treatment of Cantor's Theorem follows the classic example from
  the early 1990s, e.g.\ see the file 🍋‹92/HOL/ex/set.ML› in
  Isabelle92 or 🍋‹‹\S18.7› in "paulson-isa-book"›. The old tactic scripts
  synthesize key information of the proof by refinement of schematic goal
  states. In contrast, the Isar proof needs to say explicitly what is proven.

  🚫
  Cantor's Theorem states that every set has more subsets than it has
  elements. It has become a favourite basic example in pure higher-order logic
  since it is so easily expressed:

  @{text [display]
  ‹∀f::α ==> α ==> bool. ∃S::α ==> bool. ∀x::α. f x ≠ S›}

  Viewing types as sets, ‹α ==> bool› represents the powerset of ‹α›. This
  version of the theorem states that for every function from ‹α› to its
  powerset, some subset is outside its range. The Isabelle/Isar proofs below
  uses HOL's set theory, with the type \\ set\ and the operator \range :: (\ \
  β) ==> β set›.
›

theorem "\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 "\S. S \ range (f :: 'a \ 'a set)"
  by best

end