(*  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>\<Rightarrow>\<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>\<Rightarrow>\<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 \<Rightarrow> real \<Rightarrow> real set" where

  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"

subsubsection {* Properties *}

lemma closed_int_subset:

  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"

  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"

proof -

  {

    fix x::real

    assume "x \<in> closed_int x1 y1"

    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)

    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto

    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)

  }

  thus ?thesis by auto

qed

lemma closed_int_least:

  assumes a: "a \<le> b"

  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"

proof

  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp

  thus "a \<in> closed_int a b" by (unfold closed_int_def)

next

  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp

  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)

qed

lemma closed_int_most:

  assumes a: "a \<le> b"

  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"

proof

  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp

  thus "b \<in> closed_int a b" by (unfold closed_int_def)

next

  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp

  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)

qed

lemma closed_not_empty:

  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 

  by (auto dest: closed_int_least)

lemma closed_mem:

  assumes "a \<le> c" and "c \<le> b"

  shows "c \<in> closed_int a b"

  using assms unfolding closed_int_def by auto

lemma closed_subset:

  assumes ac: "a \<le> b"  "c \<le> d" 

  assumes closed: "closed_int a b \<subseteq> closed_int c d"

  shows "b \<ge> c"

proof -

  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto

  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)

  with ac have "c\<le>b \<and> b\<le>d" by simp

  thus ?thesis by auto

qed

subsection {* Nested Interval Property *}

theorem NIP:

  fixes f::"nat \<Rightarrow> real set"

  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"

  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"

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

proof -

  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"

  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"

  proof

    fix n

    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp

    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto

    hence "a \<le> b" ..

    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp

    with fn show "\<exists>x. x\<in>(f n)" by simp

  qed

  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"

  proof

    fix n

    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..

    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto

    hence "a \<le> b" by simp

    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)

    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp

    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..

    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>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 "A \<noteq> {}"

  proof -

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

    with Adef show ?thesis

      by blast

  qed

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

  moreover have "bdd_above A"

  proof -

    {

      fix n

      from ne have ex: "\<exists>x. x\<in>(f n)" ..

      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

      moreover

      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..

      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto

      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast

      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp

      with ex have "(?g n) \<le> b" by auto

      hence "\<exists>b. (?g n) \<le> b" by auto

    }

    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..

    have fs: "\<forall>n::nat. f n \<subseteq> f 0"

    proof (rule allI, induct_tac n)

      show "f 0 \<subseteq> f 0" by simp

    next

      fix n

      assume "f n \<subseteq> f 0"

      moreover from subset have "f (Suc n) \<subseteq> f n" ..

      ultimately show "f (Suc n) \<subseteq> f 0" by simp

    qed

    have "\<forall>n. (?g n)\<in>(f 0)"

    proof

      fix n

      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp

      hence "?g n \<in> f n" ..

      with fs show "?g n \<in> f 0" by auto

    qed

    moreover from closed

      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast

    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto

    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast

    with Adef show "bdd_above A" by auto

  qed

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

  def tdef: t == "Sup A"

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

  have "\<forall>n. t \<in> f n"

  proof

    fix n::nat

    from closed obtain a and b where

      int: "f n = closed_int a b" and alb: "a \<le> b" by blast

    have "t \<ge> a"

    proof -

      have "a \<in> A"

      proof -

          (* by construction *)

        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"

          using closed_int_least by blast

        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"

        proof clarsimp

          fix e

          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"

          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto

          from ein aux have "a \<le> e \<and> e \<le> e" by auto

          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto

          ultimately show "e = a" by simp

        qed

        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> 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 \<in> \<nat>" by simp

          ultimately have "n \<in> \<nat>"

            apply -

            apply (subst(asm) eq_sym_conv)

            apply (erule subst)

            .

        }

        with Adef have "(?g n) \<in> A" by auto

        ultimately show ?thesis by simp

      qed 

      with `bdd_above A` show "a \<le> t"

        unfolding tdef by (intro cSup_upper)

    qed

    moreover have "t \<le> b"

      unfolding tdef

    proof (rule cSup_least)

      {

        from alb int have

          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast

        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"

        proof (rule allI, induct_tac m)

          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp

        next

          fix m n

          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"

          {

            fix p

            from pp have "f (p + n) \<subseteq> f p" by simp

            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto

            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp

            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp

          }

          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..

        qed 

        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"

        proof ((rule allI)+, rule impI)

          fix \<alpha>::nat and \<beta>::nat

          assume "\<beta> \<le> \<alpha>"

          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)

          then obtain k where "\<alpha> = \<beta> + k" ..

          moreover

          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp

          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto

        qed 

        fix m   

        {

          assume "m \<ge> n"

          with subsetm have "f m \<subseteq> f n" by simp

          with ain have "\<forall>x\<in>f m. x \<le> b" by auto

          moreover

          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp

          ultimately have "?g m \<le> b" by auto

        }

        moreover

        {

          assume "\<not>(m \<ge> n)"

          hence "m < n" by simp

          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp

          from closed obtain ma and mb where

            "f m = closed_int ma mb \<and> ma \<le> mb" by blast

          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 

          from one alb sub fm int have "ma \<le> b" using closed_subset by blast

          moreover have "(?g m) = ma"

          proof -

            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..

            moreover from one have

              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"

              by (rule closed_int_least)

            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp

            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto

            thus "?g m = ma" by auto

          qed

          ultimately have "?g m \<le> b" by simp

        } 

        ultimately have "?g m \<le> b" by (rule case_split)

      }

      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto

    qed fact

    ultimately have "t \<in> closed_int a b" by (rule closed_mem)

    with int show "t \<in> f n" by simp

  qed

  hence "t \<in> (\<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 "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> 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 \<notin> closed_int a b"

      unfolding closed_int_def by auto

    with `a < b` show ?thesis by auto

  next

    case False

    then have "a \<le> c" by simp

    def ka \<equiv> "(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\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)

    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp

    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)

    ultimately have

      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"

      using kalb by auto

    then show ?thesis

      by auto

  qed

next

  case False

  then have "c \<ge> b" by simp

  def kb \<equiv> "(a + b)/2"

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

  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto

  from `kb < c` have c: "c \<notin> closed_int a kb"

    unfolding closed_int_def by auto

  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"

    unfolding closed_int_def by auto

  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"

    by simp

  then show ?thesis by auto

qed

subsection {* newInt: Interval generation *}

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

closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and

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

that @{text "(f 0)\<notin>newInt 0 f"}. *}

subsubsection {* Definition *}

primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where

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

  | "newInt (Suc n) f =

      (SOME e. (\<exists>e1 e2.

       e1 < e2 \<and>

       e = closed_int e1 e2 \<and>

       e \<subseteq> (newInt n f) \<and>

       (f (Suc n)) \<notin> e)

      )"

subsubsection {* Properties *}

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

appropriate interval. *}

lemma newInt_ex:

  "\<exists>a b. a < b \<and>

   newInt (Suc n) f = closed_int a b \<and>

   newInt (Suc n) f \<subseteq> newInt n f \<and>

   f (Suc n) \<notin> newInt (Suc n) f"

proof (induct n)

  case 0

  let ?e = "SOME e. \<exists>e1 e2.

   e1 < e2 \<and>

   e = closed_int e1 e2 \<and>

   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

   f (Suc 0) \<notin> e"

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

  moreover

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

  with closed_subset_ex have

    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

     f (Suc 0) \<notin> (closed_int ka kb)" .

  hence

    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp

  hence

    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"

    by (rule someI_ex)

  ultimately have "\<exists>e1 e2. e1 < e2 \<and>

   newInt (Suc 0) f = closed_int e1 e2 \<and>

   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>

   f (Suc 0) \<notin> newInt (Suc 0) f" by simp

  thus

    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>

     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"

    by simp

next

  case (Suc n)

  hence "\<exists>a b.

   a < b \<and>

   newInt (Suc n) f = closed_int a b \<and>

   newInt (Suc n) f \<subseteq> newInt n f \<and>

   f (Suc n) \<notin> newInt (Suc n) f" by simp

  then obtain a and b where ab: "a < b \<and>

   newInt (Suc n) f = closed_int a b \<and>

   newInt (Suc n) f \<subseteq> newInt n f \<and>

   f (Suc n) \<notin> newInt (Suc n) f" by auto

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

  let ?e = "SOME e. \<exists>e1 e2.

    e1 < e2 \<and>

    e = closed_int e1 e2 \<and>

    e \<subseteq> closed_int a b \<and>

    f (Suc (Suc n)) \<notin> 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

    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>

     f (Suc (Suc n)) \<notin> closed_int ka kb" .

  hence

    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"

    by simp

  hence

    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>

     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp

  hence

    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>

     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)

  with ab ni show

    "\<exists>ka kb. ka < kb \<and>

     newInt (Suc (Suc n)) f = closed_int ka kb \<and>

     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>

     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto

qed

lemma newInt_subset:

  "newInt (Suc n) f \<subseteq> 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:

  "\<forall>n. f n \<notin> (\<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 \<notin> newInt n f" by (unfold closed_int_def, simp)

  }

  moreover

  {

    assume "\<not> 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

      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .

    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto

    with ndef have "f n \<notin> newInt n f" by simp

  }

  ultimately have "f n \<notin> newInt n f" by (rule case_split)

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

qed

lemma newInt_notempty:

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

proof -

  let ?g = "\<lambda>n. newInt n f"

  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"

  proof

    fix n

    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)

  qed

  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"

  proof

    fix n::nat

    {

      assume "n = 0"

      then have

        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"

        by simp

      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

    }

    moreover

    {

      assume "\<not> n = 0"

      then have "n > 0" by simp

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

      have

        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>

        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"

        by (rule newInt_ex)

      then obtain a and b where

        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto

      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto

      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast

    }

    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)

  qed

  ultimately show ?thesis by (rule NIP)

qed

subsection {* Final Theorem *}

theorem real_non_denum:

  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"

proof -- "by contradiction"

  assume "\<exists>f::nat\<Rightarrow>real. surj f"

  then obtain f::"nat\<Rightarrow>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 "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast

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

  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast

  moreover from rangeF have "x \<in> range f" by simp

  ultimately show False by blast

qed

end