Theory Cantor

```(*  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.
›

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 \<^cite>‹‹\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
```