Theory Cantor

theory Cantor
imports Main
(*  Title:      HOL/Isar_Examples/Cantor.thy
    Author:     Makarius

section ‹Cantor's Theorem›

theory Cantor
  imports Main

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
  ▪ 🌐‹›
  ▪ 🌐‹'s_diagonal_argument›

theorem Cantor: "∄f :: 'a ⇒ 'a set. ∀A. ∃x. A = f x"
  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

subsection ‹Automated proofs›

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

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"
    assume A
    with * have "¬ A" ..
    from this and ‹A› show False ..
  with * show A ..

theorem Cantor': "∄f :: 'a ⇒ 'a ⇒ bool. ∀A. ∃x. A = f x"
  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)

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 @{verbatim "92/HOL/ex/set.ML"} in
  Isabelle92 or @{cite ‹\S18.7› "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)"
  let ?S = "{x. x ∉ f x}"
  show "?S ∉ range f"
    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
      assume "y ∉ ?S"
      assume "y ∉ f y"
      then have "y ∈ ?S" ..
      with ‹y ∉ ?S› show ?thesis by contradiction

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