src/HOL/Library/ContNotDenum.thy

move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

(*  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