src/HOL/Library/ContNotDenum.thy

tuned proofs;

(*  Title:      HOL/Library/ContNonDenum.thy
    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 @{text "f: \<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 @{text
"f: \<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 *}

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 = {a..b} \<and> a \<le> b"
  shows "(\<Inter>n. f n) \<noteq> {}"
proof -
  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
  {
    fix n
    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
      by auto
    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
      by auto
  }
  note f_eq = this
  {
    fix n m :: nat
    assume "n \<le> m"
    then have "f m \<subseteq> f n"
      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
  }
  note subset' = this

  have "compact (f 0)"
    by (subst f_eq) (rule compact_Icc)
  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
  proof (rule compact_imp_fip_image)
    fix I :: "nat set"
    assume I: "finite I"
    have "{} \<subset> f (Max (insert 0 I))"
      using f_eq[of "Max (insert 0 I)"] by auto
    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
    proof (rule INF_greatest)
      fix i
      assume "i \<in> insert 0 I"
      with I show "f (Max (insert 0 I)) \<subseteq> f i"
        by (intro subset') auto
    qed
    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
      by auto
  qed (subst f_eq, auto)
  then show "(\<Inter>n. f n) \<noteq> {}"
    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> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
proof (cases "c < b")
  case True
  show ?thesis
  proof (cases "c < a")
    case True
    with `a < b` `c < b` have "c \<notin> {a..b}"
      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 "ka < b"
      by auto
    moreover from ka_def `c < b` have "ka > c"
      by simp
    ultimately have "c \<notin> {ka..b}"
      by auto
    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
      by simp
    then have "{ka..b} \<subseteq> {a..b}"
      by auto
    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
      using `ka < b` 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> {a..kb}"
    by auto
  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
    by auto
  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {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 = {f 0 + 1..f 0 + 2}"
| "newInt (Suc n) f =
    (SOME e.
      (\<exists>e1 e2.
         e1 < e2 \<and>
         e = {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 = {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 = {e1..e2} \<and>
    e \<subseteq> {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> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e"
    by simp
  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {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 = {e1..e2} \<and>
      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
      f (Suc 0) \<notin> newInt (Suc 0) f"
    by simp
  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {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)
  then have "\<exists>a b.
      a < b \<and>
      newInt (Suc n) f = {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 = {a..b} \<and>
      newInt (Suc n) f \<subseteq> newInt n f \<and>
      f (Suc n) \<notin> newInt (Suc n) f"
    by auto
  then have cab: "{a..b} = newInt (Suc n) f"
    by simp

  let ?e = "SOME e. \<exists>e1 e2.
      e1 < e2 \<and>
      e = {e1..e2} \<and>
      e \<subseteq> {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> {ka..kb} \<subseteq> {a..b} \<and>
    f (Suc (Suc n)) \<notin> {ka..kb}" .
  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
    by simp
  then have "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and> e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e"
    by simp
  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {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 = {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
  have "f n \<notin> newInt n f"
  proof (cases n)
    case 0
    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
      by simp
    ultimately show ?thesis by simp
  next
    case (Suc m)
    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {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 Suc show ?thesis by simp
  qed
  then show "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 = {a..b} \<and> a \<le> b"
  proof
    fix n :: nat
    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
    proof (cases n)
      case 0
      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
        by simp
      then show ?thesis
        by blast
    next
      case (Suc m)
      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {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) = {a..b}"
        by auto
      with Suc have "?g n = {a..b} \<and> a \<le> b"
        by auto
      then show ?thesis
        by blast
    qed
  qed
  ultimately show ?thesis by (rule NIP)
qed


subsection {* Final Theorem *}

theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
proof
  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
  then obtain f :: "nat \<Rightarrow> real" where "surj f"
    by auto
  txt "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 `surj f` have "x \<in> range f"
    by simp
  ultimately show False
    by blast
qed

end