(* 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 "\"} is not denumerable. In other
words, there does not exist a function f:@{text "\\\"} 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
"\\\"} 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 "(\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 ` \" by simp
ultimately have "\x. x\A"
proof -
have "(0::nat) \ \" by simp
moreover have "?g 0 = ?g 0" by simp
ultimately have "?g 0 \ ?g ` \" 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 \ \" by simp
ultimately have "n \ \"
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 \