Theory ContNotDenum

theory ContNotDenum
imports Complex_Main
(*  Title       : HOL/ContNonDenum    Author      : Benjamin Porter, Monash University, NICTA, 2005*)header {* Non-denumerability of the Continuum. *}theory ContNotDenumimports Complex_Mainbeginsubsection {* Abstract *}text {* The following document presents a proof that the Continuum isuncountable. It is formalised in the Isabelle/Isar theorem provingsystem.{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In otherwords, there does not exist a function f:@{text "\<nat>=>\<real>"} such that f issurjective.{\em Outline:} An elegant informal proof of this result uses Cantor'sDiagonalisation argument. The proof presented here is not thisone. First we formalise some properties of closed intervals, then weprove the Nested Interval Property. This property relies on thecompleteness of the Real numbers and is the foundation for ourargument. Informally it states that an intersection of countableclosed intervals (where each successive interval is a subset of thelast) 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 fby 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 autoqedlemma 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)qedlemma 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)qedlemma 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 autolemma 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 autoqedsubsection {* 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 autoqedsubsection {* Generating the intervals *}subsubsection {* Existence of non-singleton closed intervals *}text {* This lemma asserts that given any non-singleton closedinterval (a,b) and any element c, there exists a closed interval thatis a subset of (a,b) and that does not contain c and is anon-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  qednext  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 autoqedsubsection {* newInt: Interval generation *}text {* Given a function f:@{text "\<nat>=>\<real>"}, newInt (Suc n) f returns aclosed interval such that @{text "newInt (Suc n) f ⊆ newInt n f"} anddoes not contain @{text "f (Suc n)"}. With the base case defined suchthat @{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 anappropriate 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 simpnext  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 autoqedlemma newInt_subset:  "newInt (Suc n) f ⊆ newInt n f"  using newInt_ex by autotext {* Another fundamental property is that no element in the rangeof f is in the intersection of all closed intervals generated bynewInt. *}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 autoqedlemma 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)qedsubsection {* 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 blastqedend