(* Title : HOL/ContNonDenum Author : Benjamin Porter, Monash University, NICTA, 2005 *) header {* Non-denumerability of the Continuum. *} theory ContNotDenum imports RComplete Hilbert_Choice 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 \ 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 \ (\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 alb: "a < b" shows "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" proof - { assume clb: "c < b" { assume cla: "c < a" from alb cla clb have "c \ closed_int a b" by (unfold closed_int_def, auto) with alb have "a < b \ closed_int a b \ closed_int a b \ c \ closed_int a b" by auto hence "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" by auto } moreover { assume ncla: "\(c < a)" with clb have cdef: "a \ c \ c < b" by simp obtain ka where kadef: "ka = (c + b)/2" by blast from kadef clb have kalb: "ka < b" by auto moreover from kadef cdef have kagc: "ka > c" by simp ultimately have "c\(closed_int ka b)" by (unfold closed_int_def, auto) moreover from cdef 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 hence "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" by auto } ultimately have "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" by (rule case_split) } moreover { assume "\ (c < b)" hence cgeb: "c \ b" by simp obtain kb where kbdef: "kb = (a + b)/2" by blast with alb have kblb: "kb < b" by auto with kbdef cgeb have "a < kb \ kb < c" by auto moreover hence "c \ (closed_int a kb)" by (unfold closed_int_def, auto) moreover from kblb have "closed_int a kb \ closed_int a b" by (unfold closed_int_def, auto) ultimately have "a < kb \ closed_int a kb \ closed_int a b \ c\closed_int a kb" by simp hence "\ka kb. ka < kb \ closed_int ka kb \ closed_int a b \ c \ (closed_int ka kb)" by auto } ultimately show ?thesis by (rule case_split) qed subsection {* newInt: Interval generation *} text {* Given a function f:@{text "\\\"}, 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) )" declare newInt.simps [code del] 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 \ (\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 \ (\n. newInt n f)" by auto qed lemma newInt_notempty: "(\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 "surj f" by auto hence rangeF: "range f = UNIV" by (rule surj_range) -- "We now produce a real number x that is not in the range of f, using the properties of newInt. " have "\x. x \ (\n. newInt n f)" using newInt_notempty by blast moreover have "\n. f n \ (\n. newInt n f)" by (rule newInt_inter) ultimately obtain x where "x \ (\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