(* Title : HOL/ContNonDenum

Author : Benjamin Porter, Monash University, NICTA, 2005

*)

header {* Non-denumerability of the Continuum. *}

theory ContNotDenum

imports Complex_Main

begin

subsection {* Abstract *}

text {* The following document presents a proof that the Continuum is

uncountable. It is formalised in the Isabelle/Isar theorem proving

system.

{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other

words, there does not exist a function f:@{text "\<nat>=>\<real>"} such that f is

surjective.

{\em Outline:} An elegant informal proof of this result uses Cantor's

Diagonalisation argument. The proof presented here is not this

one. First we formalise some properties of closed intervals, then we

prove the Nested Interval Property. This property relies on the

completeness of the Real numbers and is the foundation for our

argument. Informally it states that an intersection of countable

closed intervals (where each successive interval is a subset of the

last) is non-empty. We then assume a surjective function f:@{text

"\<nat>=>\<real>"} exists and find a real x such that x is not in the range of f

by generating a sequence of closed intervals then using the NIP. *}

subsection {* Closed Intervals *}

text {* This section formalises some properties of closed intervals. *}

subsubsection {* Definition *}

definition

closed_int :: "real => real => real set" where

"closed_int x y = {z. x ≤ z ∧ z ≤ y}"

subsubsection {* Properties *}

lemma closed_int_subset:

assumes xy: "x1 ≥ x0" "y1 ≤ y0"

shows "closed_int x1 y1 ⊆ closed_int x0 y0"

proof -

{

fix x::real

assume "x ∈ closed_int x1 y1"

hence "x ≥ x1 ∧ x ≤ y1" by (simp add: closed_int_def)

with xy have "x ≥ x0 ∧ x ≤ y0" by auto

hence "x ∈ closed_int x0 y0" by (simp add: closed_int_def)

}

thus ?thesis by auto

qed

lemma closed_int_least:

assumes a: "a ≤ b"

shows "a ∈ closed_int a b ∧ (∀x ∈ closed_int a b. a ≤ x)"

proof

from a have "a∈{x. a≤x ∧ x≤b}" by simp

thus "a ∈ closed_int a b" by (unfold closed_int_def)

next

have "∀x∈{x. a≤x ∧ x≤b}. a≤x" by simp

thus "∀x ∈ closed_int a b. a ≤ x" by (unfold closed_int_def)

qed

lemma closed_int_most:

assumes a: "a ≤ b"

shows "b ∈ closed_int a b ∧ (∀x ∈ closed_int a b. x ≤ b)"

proof

from a have "b∈{x. a≤x ∧ x≤b}" by simp

thus "b ∈ closed_int a b" by (unfold closed_int_def)

next

have "∀x∈{x. a≤x ∧ x≤b}. x≤b" by simp

thus "∀x ∈ closed_int a b. x≤b" by (unfold closed_int_def)

qed

lemma closed_not_empty:

shows "a ≤ b ==> ∃x. x ∈ closed_int a b"

by (auto dest: closed_int_least)

lemma closed_mem:

assumes "a ≤ c" and "c ≤ b"

shows "c ∈ closed_int a b"

using assms unfolding closed_int_def by auto

lemma closed_subset:

assumes ac: "a ≤ b" "c ≤ d"

assumes closed: "closed_int a b ⊆ closed_int c d"

shows "b ≥ c"

proof -

from closed have "∀x∈closed_int a b. x∈closed_int c d" by auto

hence "∀x. a≤x ∧ x≤b --> c≤x ∧ x≤d" by (unfold closed_int_def, auto)

with ac have "c≤b ∧ b≤d" by simp

thus ?thesis by auto

qed

subsection {* Nested Interval Property *}

theorem NIP:

fixes f::"nat => real set"

assumes subset: "∀n. f (Suc n) ⊆ f n"

and closed: "∀n. ∃a b. f n = closed_int a b ∧ a ≤ b"

shows "(\<Inter>n. f n) ≠ {}"

proof -

let ?g = "λn. (SOME c. c∈(f n) ∧ (∀x∈(f n). c ≤ x))"

have ne: "∀n. ∃x. x∈(f n)"

proof

fix n

from closed have "∃a b. f n = closed_int a b ∧ a ≤ b" by simp

then obtain a and b where fn: "f n = closed_int a b ∧ a ≤ b" by auto

hence "a ≤ b" ..

with closed_not_empty have "∃x. x∈closed_int a b" by simp

with fn show "∃x. x∈(f n)" by simp

qed

have gdef: "∀n. (?g n)∈(f n) ∧ (∀x∈(f n). (?g n)≤x)"

proof

fix n

from closed have "∃a b. f n = closed_int a b ∧ a ≤ b" ..

then obtain a and b where ff: "f n = closed_int a b" and "a ≤ b" by auto

hence "a ≤ b" by simp

hence "a∈closed_int a b ∧ (∀x∈closed_int a b. a ≤ x)" by (rule closed_int_least)

with ff have "a∈(f n) ∧ (∀x∈(f n). a ≤ x)" by simp

hence "∃c. c∈(f n) ∧ (∀x∈(f n). c ≤ x)" ..

thus "(?g n)∈(f n) ∧ (∀x∈(f n). (?g n)≤x)" by (rule someI_ex)

qed

-- "A denotes the set of all left-most points of all the intervals ..."

moreover obtain A where Adef: "A = ?g ` \<nat>" by simp

ultimately have "∃x. x∈A"

proof -

have "(0::nat) ∈ \<nat>" by simp

moreover have "?g 0 = ?g 0" by simp

ultimately have "?g 0 ∈ ?g ` \<nat>" by (rule rev_image_eqI)

with Adef have "?g 0 ∈ A" by simp

thus ?thesis ..

qed

-- "Now show that A is bounded above ..."

moreover have "∃y. isUb (UNIV::real set) A y"

proof -

{

fix n

from ne have ex: "∃x. x∈(f n)" ..

from gdef have "(?g n)∈(f n) ∧ (∀x∈(f n). (?g n)≤x)" by simp

moreover

from closed have "∃a b. f n = closed_int a b ∧ a ≤ b" ..

then obtain a and b where "f n = closed_int a b ∧ a ≤ b" by auto

hence "b∈(f n) ∧ (∀x∈(f n). x ≤ b)" using closed_int_most by blast

ultimately have "∀x∈(f n). (?g n) ≤ b" by simp

with ex have "(?g n) ≤ b" by auto

hence "∃b. (?g n) ≤ b" by auto

}

hence aux: "∀n. ∃b. (?g n) ≤ b" ..

have fs: "∀n::nat. f n ⊆ f 0"

proof (rule allI, induct_tac n)

show "f 0 ⊆ f 0" by simp

next

fix n

assume "f n ⊆ f 0"

moreover from subset have "f (Suc n) ⊆ f n" ..

ultimately show "f (Suc n) ⊆ f 0" by simp

qed

have "∀n. (?g n)∈(f 0)"

proof

fix n

from gdef have "(?g n)∈(f n) ∧ (∀x∈(f n). (?g n)≤x)" by simp

hence "?g n ∈ f n" ..

with fs show "?g n ∈ f 0" by auto

qed

moreover from closed

obtain a and b where "f 0 = closed_int a b" and alb: "a ≤ b" by blast

ultimately have "∀n. ?g n ∈ closed_int a b" by auto

with alb have "∀n. ?g n ≤ b" using closed_int_most by blast

with Adef have "∀y∈A. y≤b" by auto

hence "A *<= b" by (unfold setle_def)

moreover have "b ∈ (UNIV::real set)" by simp

ultimately have "A *<= b ∧ b ∈ (UNIV::real set)" by simp

hence "isUb (UNIV::real set) A b" by (unfold isUb_def)

thus ?thesis by auto

qed

-- "by the Axiom Of Completeness, A has a least upper bound ..."

ultimately have "∃t. isLub UNIV A t" by (rule reals_complete)

-- "denote this least upper bound as t ..."

then obtain t where tdef: "isLub UNIV A t" ..

-- "and finally show that this least upper bound is in all the intervals..."

have "∀n. t ∈ f n"

proof

fix n::nat

from closed obtain a and b where

int: "f n = closed_int a b" and alb: "a ≤ b" by blast

have "t ≥ a"

proof -

have "a ∈ A"

proof -

(* by construction *)

from alb int have ain: "a∈f n ∧ (∀x∈f n. a ≤ x)"

using closed_int_least by blast

moreover have "∀e. e∈f n ∧ (∀x∈f n. e ≤ x) --> e = a"

proof clarsimp

fix e

assume ein: "e ∈ f n" and lt: "∀x∈f n. e ≤ x"

from lt ain have aux: "∀x∈f n. a ≤ x ∧ e ≤ x" by auto

from ein aux have "a ≤ e ∧ e ≤ e" by auto

moreover from ain aux have "a ≤ a ∧ e ≤ a" by auto

ultimately show "e = a" by simp

qed

hence "!!e. e∈f n ∧ (∀x∈f n. e ≤ x) ==> e = a" by simp

ultimately have "(?g n) = a" by (rule some_equality)

moreover

{

have "n = of_nat n" by simp

moreover have "of_nat n ∈ \<nat>" by simp

ultimately have "n ∈ \<nat>"

apply -

apply (subst(asm) eq_sym_conv)

apply (erule subst)

.

}

with Adef have "(?g n) ∈ A" by auto

ultimately show ?thesis by simp

qed

with tdef show "a ≤ t" by (rule isLubD2)

qed

moreover have "t ≤ b"

proof -

have "isUb UNIV A b"

proof -

{

from alb int have

ain: "b∈f n ∧ (∀x∈f n. x ≤ b)" using closed_int_most by blast

have subsetd: "∀m. ∀n. f (n + m) ⊆ f n"

proof (rule allI, induct_tac m)

show "∀n. f (n + 0) ⊆ f n" by simp

next

fix m n

assume pp: "∀p. f (p + n) ⊆ f p"

{

fix p

from pp have "f (p + n) ⊆ f p" by simp

moreover from subset have "f (Suc (p + n)) ⊆ f (p + n)" by auto

hence "f (p + (Suc n)) ⊆ f (p + n)" by simp

ultimately have "f (p + (Suc n)) ⊆ f p" by simp

}

thus "∀p. f (p + Suc n) ⊆ f p" ..

qed

have subsetm: "∀α β. α ≥ β --> (f α) ⊆ (f β)"

proof ((rule allI)+, rule impI)

fix α::nat and β::nat

assume "β ≤ α"

hence "∃k. α = β + k" by (simp only: le_iff_add)

then obtain k where "α = β + k" ..

moreover

from subsetd have "f (β + k) ⊆ f β" by simp

ultimately show "f α ⊆ f β" by auto

qed

fix m

{

assume "m ≥ n"

with subsetm have "f m ⊆ f n" by simp

with ain have "∀x∈f m. x ≤ b" by auto

moreover

from gdef have "?g m ∈ f m ∧ (∀x∈f m. ?g m ≤ x)" by simp

ultimately have "?g m ≤ b" by auto

}

moreover

{

assume "¬(m ≥ n)"

hence "m < n" by simp

with subsetm have sub: "(f n) ⊆ (f m)" by simp

from closed obtain ma and mb where

"f m = closed_int ma mb ∧ ma ≤ mb" by blast

hence one: "ma ≤ mb" and fm: "f m = closed_int ma mb" by auto

from one alb sub fm int have "ma ≤ b" using closed_subset by blast

moreover have "(?g m) = ma"

proof -

from gdef have "?g m ∈ f m ∧ (∀x∈f m. ?g m ≤ x)" ..

moreover from one have

"ma ∈ closed_int ma mb ∧ (∀x∈closed_int ma mb. ma ≤ x)"

by (rule closed_int_least)

with fm have "ma∈f m ∧ (∀x∈f m. ma ≤ x)" by simp

ultimately have "ma ≤ ?g m ∧ ?g m ≤ ma" by auto

thus "?g m = ma" by auto

qed

ultimately have "?g m ≤ b" by simp

}

ultimately have "?g m ≤ b" by (rule case_split)

}

with Adef have "∀y∈A. y≤b" by auto

hence "A *<= b" by (unfold setle_def)

moreover have "b ∈ (UNIV::real set)" by simp

ultimately have "A *<= b ∧ b ∈ (UNIV::real set)" by simp

thus "isUb (UNIV::real set) A b" by (unfold isUb_def)

qed

with tdef show "t ≤ b" by (rule isLub_le_isUb)

qed

ultimately have "t ∈ closed_int a b" by (rule closed_mem)

with int show "t ∈ f n" by simp

qed

hence "t ∈ (\<Inter>n. f n)" by auto

thus ?thesis by auto

qed

subsection {* Generating the intervals *}

subsubsection {* Existence of non-singleton closed intervals *}

text {* This lemma asserts that given any non-singleton closed

interval (a,b) and any element c, there exists a closed interval that

is a subset of (a,b) and that does not contain c and is a

non-singleton itself. *}

lemma closed_subset_ex:

fixes c::real

assumes "a < b"

shows "∃ka kb. ka < kb ∧ closed_int ka kb ⊆ closed_int a b ∧ c ∉ closed_int ka kb"

proof (cases "c < b")

case True

show ?thesis

proof (cases "c < a")

case True

with `a < b` `c < b` have "c ∉ closed_int a b"

unfolding closed_int_def by auto

with `a < b` show ?thesis by auto

next

case False

then have "a ≤ c" by simp

def ka ≡ "(c + b)/2"

from ka_def `c < b` have kalb: "ka < b" by auto

moreover from ka_def `c < b` have kagc: "ka > c" by simp

ultimately have "c∉(closed_int ka b)" by (unfold closed_int_def, auto)

moreover from `a ≤ c` kagc have "ka ≥ a" by simp

hence "closed_int ka b ⊆ closed_int a b" by (unfold closed_int_def, auto)

ultimately have

"ka < b ∧ closed_int ka b ⊆ closed_int a b ∧ c ∉ closed_int ka b"

using kalb by auto

then show ?thesis

by auto

qed

next

case False

then have "c ≥ b" by simp

def kb ≡ "(a + b)/2"

with `a < b` have "kb < b" by auto

with kb_def `c ≥ b` have "a < kb" "kb < c" by auto

from `kb < c` have c: "c ∉ closed_int a kb"

unfolding closed_int_def by auto

with `kb < b` have "closed_int a kb ⊆ closed_int a b"

unfolding closed_int_def by auto

with `a < kb` c have "a < kb ∧ closed_int a kb ⊆ closed_int a b ∧ c ∉ closed_int a kb"

by simp

then show ?thesis by auto

qed

subsection {* newInt: Interval generation *}

text {* Given a function f:@{text "\<nat>=>\<real>"}, newInt (Suc n) f returns a

closed interval such that @{text "newInt (Suc n) f ⊆ newInt n f"} and

does not contain @{text "f (Suc n)"}. With the base case defined such

that @{text "(f 0)∉newInt 0 f"}. *}

subsubsection {* Definition *}

primrec newInt :: "nat => (nat => real) => (real set)" where

"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"

| "newInt (Suc n) f =

(SOME e. (∃e1 e2.

e1 < e2 ∧

e = closed_int e1 e2 ∧

e ⊆ (newInt n f) ∧

(f (Suc n)) ∉ e)

)"

subsubsection {* Properties *}

text {* We now show that every application of newInt returns an

appropriate interval. *}

lemma newInt_ex:

"∃a b. a < b ∧

newInt (Suc n) f = closed_int a b ∧

newInt (Suc n) f ⊆ newInt n f ∧

f (Suc n) ∉ newInt (Suc n) f"

proof (induct n)

case 0

let ?e = "SOME e. ∃e1 e2.

e1 < e2 ∧

e = closed_int e1 e2 ∧

e ⊆ closed_int (f 0 + 1) (f 0 + 2) ∧

f (Suc 0) ∉ e"

have "newInt (Suc 0) f = ?e" by auto

moreover

have "f 0 + 1 < f 0 + 2" by simp

with closed_subset_ex have

"∃ka kb. ka < kb ∧ closed_int ka kb ⊆ closed_int (f 0 + 1) (f 0 + 2) ∧

f (Suc 0) ∉ (closed_int ka kb)" .

hence

"∃e. ∃ka kb. ka < kb ∧ e = closed_int ka kb ∧

e ⊆ closed_int (f 0 + 1) (f 0 + 2) ∧ f (Suc 0) ∉ e" by simp

hence

"∃ka kb. ka < kb ∧ ?e = closed_int ka kb ∧

?e ⊆ closed_int (f 0 + 1) (f 0 + 2) ∧ f (Suc 0) ∉ ?e"

by (rule someI_ex)

ultimately have "∃e1 e2. e1 < e2 ∧

newInt (Suc 0) f = closed_int e1 e2 ∧

newInt (Suc 0) f ⊆ closed_int (f 0 + 1) (f 0 + 2) ∧

f (Suc 0) ∉ newInt (Suc 0) f" by simp

thus

"∃a b. a < b ∧ newInt (Suc 0) f = closed_int a b ∧

newInt (Suc 0) f ⊆ newInt 0 f ∧ f (Suc 0) ∉ newInt (Suc 0) f"

by simp

next

case (Suc n)

hence "∃a b.

a < b ∧

newInt (Suc n) f = closed_int a b ∧

newInt (Suc n) f ⊆ newInt n f ∧

f (Suc n) ∉ newInt (Suc n) f" by simp

then obtain a and b where ab: "a < b ∧

newInt (Suc n) f = closed_int a b ∧

newInt (Suc n) f ⊆ newInt n f ∧

f (Suc n) ∉ newInt (Suc n) f" by auto

hence cab: "closed_int a b = newInt (Suc n) f" by simp

let ?e = "SOME e. ∃e1 e2.

e1 < e2 ∧

e = closed_int e1 e2 ∧

e ⊆ closed_int a b ∧

f (Suc (Suc n)) ∉ e"

from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto

from ab have "a < b" by simp

with closed_subset_ex have

"∃ka kb. ka < kb ∧ closed_int ka kb ⊆ closed_int a b ∧

f (Suc (Suc n)) ∉ closed_int ka kb" .

hence

"∃e. ∃ka kb. ka < kb ∧ e = closed_int ka kb ∧

closed_int ka kb ⊆ closed_int a b ∧ f (Suc (Suc n)) ∉ closed_int ka kb"

by simp

hence

"∃e. ∃ka kb. ka < kb ∧ e = closed_int ka kb ∧

e ⊆ closed_int a b ∧ f (Suc (Suc n)) ∉ e" by simp

hence

"∃ka kb. ka < kb ∧ ?e = closed_int ka kb ∧

?e ⊆ closed_int a b ∧ f (Suc (Suc n)) ∉ ?e" by (rule someI_ex)

with ab ni show

"∃ka kb. ka < kb ∧

newInt (Suc (Suc n)) f = closed_int ka kb ∧

newInt (Suc (Suc n)) f ⊆ newInt (Suc n) f ∧

f (Suc (Suc n)) ∉ newInt (Suc (Suc n)) f" by auto

qed

lemma newInt_subset:

"newInt (Suc n) f ⊆ newInt n f"

using newInt_ex by auto

text {* Another fundamental property is that no element in the range

of f is in the intersection of all closed intervals generated by

newInt. *}

lemma newInt_inter:

"∀n. f n ∉ (\<Inter>n. newInt n f)"

proof

fix n::nat

{

assume n0: "n = 0"

moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp

ultimately have "f n ∉ newInt n f" by (unfold closed_int_def, simp)

}

moreover

{

assume "¬ n = 0"

hence "n > 0" by simp

then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)

from newInt_ex have

"∃a b. a < b ∧ (newInt (Suc m) f) = closed_int a b ∧

newInt (Suc m) f ⊆ newInt m f ∧ f (Suc m) ∉ newInt (Suc m) f" .

then have "f (Suc m) ∉ newInt (Suc m) f" by auto

with ndef have "f n ∉ newInt n f" by simp

}

ultimately have "f n ∉ newInt n f" by (rule case_split)

thus "f n ∉ (\<Inter>n. newInt n f)" by auto

qed

lemma newInt_notempty:

"(\<Inter>n. newInt n f) ≠ {}"

proof -

let ?g = "λn. newInt n f"

have "∀n. ?g (Suc n) ⊆ ?g n"

proof

fix n

show "?g (Suc n) ⊆ ?g n" by (rule newInt_subset)

qed

moreover have "∀n. ∃a b. ?g n = closed_int a b ∧ a ≤ b"

proof

fix n::nat

{

assume "n = 0"

then have

"?g n = closed_int (f 0 + 1) (f 0 + 2) ∧ (f 0 + 1 ≤ f 0 + 2)"

by simp

hence "∃a b. ?g n = closed_int a b ∧ a ≤ b" by blast

}

moreover

{

assume "¬ n = 0"

then have "n > 0" by simp

then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)

have

"∃a b. a < b ∧ (newInt (Suc m) f) = closed_int a b ∧

(newInt (Suc m) f) ⊆ (newInt m f) ∧ (f (Suc m)) ∉ (newInt (Suc m) f)"

by (rule newInt_ex)

then obtain a and b where

"a < b ∧ (newInt (Suc m) f) = closed_int a b" by auto

with nd have "?g n = closed_int a b ∧ a ≤ b" by auto

hence "∃a b. ?g n = closed_int a b ∧ a ≤ b" by blast

}

ultimately show "∃a b. ?g n = closed_int a b ∧ a ≤ b" by (rule case_split)

qed

ultimately show ?thesis by (rule NIP)

qed

subsection {* Final Theorem *}

theorem real_non_denum:

shows "¬ (∃f::nat=>real. surj f)"

proof -- "by contradiction"

assume "∃f::nat=>real. surj f"

then obtain f::"nat=>real" where rangeF: "surj f" by auto

-- "We now produce a real number x that is not in the range of f, using the properties of newInt. "

have "∃x. x ∈ (\<Inter>n. newInt n f)" using newInt_notempty by blast

moreover have "∀n. f n ∉ (\<Inter>n. newInt n f)" by (rule newInt_inter)

ultimately obtain x where "x ∈ (\<Inter>n. newInt n f)" and "∀n. f n ≠ x" by blast

moreover from rangeF have "x ∈ range f" by simp

ultimately show False by blast

qed

end