src/HOL/Library/ContNotDenum.thy

proper position for decode_pos, which is relevant for completion;

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

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 kalb: "ka < b" by auto
    moreover from ka_def `c < b` have kagc: "ka > c" by simp
    ultimately have "c\<notin>{ka..b}" by auto
    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
    hence "{ka..b} \<subseteq> {a..b}" by auto
    ultimately have
      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {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> {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}" .
  hence
    "\<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
  hence
    "\<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
  thus
    "\<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)
  hence "\<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
  hence 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}" .
  hence
    "\<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
  hence
    "\<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
  hence
    "\<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
  {
    assume n0: "n = 0"
    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
    ultimately have "f n \<notin> newInt n f" by 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) = {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 = {a..b} \<and> a \<le> b"
  proof
    fix n::nat
    {
      assume "n = 0"
      then have
        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
        by simp
      hence "\<exists>a b. ?g n = {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) = {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 nd have "?g n = {a..b} \<and> a \<le> b" by auto
      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
    }
    ultimately show "\<exists>a b. ?g n = {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