src/HOL/Library/ContNotDenum.thy
 author wenzelm Tue Apr 29 22:50:55 2014 +0200 (2014-04-29) changeset 56796 9f84219715a7 parent 54797 be020ec8560c child 57234 596a499318ab permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/ContNonDenum.thy

     2     Author:     Benjamin Porter, Monash University, NICTA, 2005

     3 *)

     4

     5 header {* Non-denumerability of the Continuum. *}

     6

     7 theory ContNotDenum

     8 imports Complex_Main

     9 begin

    10

    11 subsection {* Abstract *}

    12

    13 text {* The following document presents a proof that the Continuum is

    14 uncountable. It is formalised in the Isabelle/Isar theorem proving

    15 system.

    16

    17 {\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other

    18 words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is

    19 surjective.

    20

    21 {\em Outline:} An elegant informal proof of this result uses Cantor's

    22 Diagonalisation argument. The proof presented here is not this

    23 one. First we formalise some properties of closed intervals, then we

    24 prove the Nested Interval Property. This property relies on the

    25 completeness of the Real numbers and is the foundation for our

    26 argument. Informally it states that an intersection of countable

    27 closed intervals (where each successive interval is a subset of the

    28 last) is non-empty. We then assume a surjective function @{text

    29 "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f

    30 by generating a sequence of closed intervals then using the NIP. *}

    31

    32

    33 subsection {* Closed Intervals *}

    34

    35 subsection {* Nested Interval Property *}

    36

    37 theorem NIP:

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

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

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

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

    42 proof -

    43   let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"

    44   {

    45     fix n

    46     from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"

    47       by auto

    48     then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"

    49       by auto

    50   }

    51   note f_eq = this

    52   {

    53     fix n m :: nat

    54     assume "n \<le> m"

    55     then have "f m \<subseteq> f n"

    56       by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)

    57   }

    58   note subset' = this

    59

    60   have "compact (f 0)"

    61     by (subst f_eq) (rule compact_Icc)

    62   then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"

    63   proof (rule compact_imp_fip_image)

    64     fix I :: "nat set"

    65     assume I: "finite I"

    66     have "{} \<subset> f (Max (insert 0 I))"

    67       using f_eq[of "Max (insert 0 I)"] by auto

    68     also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"

    69     proof (rule INF_greatest)

    70       fix i

    71       assume "i \<in> insert 0 I"

    72       with I show "f (Max (insert 0 I)) \<subseteq> f i"

    73         by (intro subset') auto

    74     qed

    75     finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"

    76       by auto

    77   qed (subst f_eq, auto)

    78   then show "(\<Inter>n. f n) \<noteq> {}"

    79     by auto

    80 qed

    81

    82

    83 subsection {* Generating the intervals *}

    84

    85 subsubsection {* Existence of non-singleton closed intervals *}

    86

    87 text {* This lemma asserts that given any non-singleton closed

    88 interval (a,b) and any element c, there exists a closed interval that

    89 is a subset of (a,b) and that does not contain c and is a

    90 non-singleton itself. *}

    91

    92 lemma closed_subset_ex:

    93   fixes c :: real

    94   assumes "a < b"

    95   shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"

    96 proof (cases "c < b")

    97   case True

    98   show ?thesis

    99   proof (cases "c < a")

   100     case True

   101     with a < b c < b have "c \<notin> {a..b}"

   102       by auto

   103     with a < b show ?thesis

   104       by auto

   105   next

   106     case False

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

   108     def ka \<equiv> "(c + b)/2"

   109     from ka_def c < b have "ka < b"

   110       by auto

   111     moreover from ka_def c < b have "ka > c"

   112       by simp

   113     ultimately have "c \<notin> {ka..b}"

   114       by auto

   115     moreover from a \<le> c ka > c have "ka \<ge> a"

   116       by simp

   117     then have "{ka..b} \<subseteq> {a..b}"

   118       by auto

   119     ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"

   120       using ka < b by auto

   121     then show ?thesis

   122       by auto

   123   qed

   124 next

   125   case False

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

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

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

   129   with kb_def c \<ge> b have "a < kb" "kb < c"

   130     by auto

   131   from kb < c have c: "c \<notin> {a..kb}"

   132     by auto

   133   with kb < b have "{a..kb} \<subseteq> {a..b}"

   134     by auto

   135   with a < kb c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"

   136     by simp

   137   then show ?thesis

   138     by auto

   139 qed

   140

   141

   142 subsection {* newInt: Interval generation *}

   143

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

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

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

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

   148

   149

   150 subsubsection {* Definition *}

   151

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

   153 where

   154   "newInt 0 f = {f 0 + 1..f 0 + 2}"

   155 | "newInt (Suc n) f =

   156     (SOME e.

   157       (\<exists>e1 e2.

   158          e1 < e2 \<and>

   159          e = {e1..e2} \<and>

   160          e \<subseteq> newInt n f \<and>

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

   162

   163

   164 subsubsection {* Properties *}

   165

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

   167 appropriate interval. *}

   168

   169 lemma newInt_ex:

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

   171     newInt (Suc n) f = {a..b} \<and>

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

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

   174 proof (induct n)

   175   case 0

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

   177     e1 < e2 \<and>

   178     e = {e1..e2} \<and>

   179     e \<subseteq> {f 0 + 1..f 0 + 2} \<and>

   180     f (Suc 0) \<notin> e"

   181

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

   183   moreover

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

   185   with closed_subset_ex

   186   have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .

   187   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"

   188     by simp

   189   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"

   190     by (rule someI_ex)

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

   192       newInt (Suc 0) f = {e1..e2} \<and>

   193       newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>

   194       f (Suc 0) \<notin> newInt (Suc 0) f"

   195     by simp

   196   then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>

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

   198     by simp

   199 next

   200   case (Suc n)

   201   then have "\<exists>a b.

   202       a < b \<and>

   203       newInt (Suc n) f = {a..b} \<and>

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

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

   206     by simp

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

   208       newInt (Suc n) f = {a..b} \<and>

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

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

   211     by auto

   212   then have cab: "{a..b} = newInt (Suc n) f"

   213     by simp

   214

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

   216       e1 < e2 \<and>

   217       e = {e1..e2} \<and>

   218       e \<subseteq> {a..b} \<and>

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

   220   from cab have ni: "newInt (Suc (Suc n)) f = ?e"

   221     by auto

   222

   223   from ab have "a < b" by simp

   224   with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>

   225     f (Suc (Suc n)) \<notin> {ka..kb}" .

   226   then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>

   227       {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"

   228     by simp

   229   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"

   230     by simp

   231   then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"

   232     by (rule someI_ex)

   233   with ab ni show "\<exists>ka kb. ka < kb \<and>

   234       newInt (Suc (Suc n)) f = {ka..kb} \<and>

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

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

   237     by auto

   238 qed

   239

   240 lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"

   241   using newInt_ex by auto

   242

   243

   244 text {* Another fundamental property is that no element in the range

   245 of f is in the intersection of all closed intervals generated by

   246 newInt. *}

   247

   248 lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"

   249 proof

   250   fix n :: nat

   251   have "f n \<notin> newInt n f"

   252   proof (cases n)

   253     case 0

   254     moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"

   255       by simp

   256     ultimately show ?thesis by simp

   257   next

   258     case (Suc m)

   259     from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>

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

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

   262       by auto

   263     with Suc show ?thesis by simp

   264   qed

   265   then show "f n \<notin> (\<Inter>n. newInt n f)" by auto

   266 qed

   267

   268 lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"

   269 proof -

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

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

   272   proof

   273     fix n

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

   275   qed

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

   277   proof

   278     fix n :: nat

   279     show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"

   280     proof (cases n)

   281       case 0

   282       then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"

   283         by simp

   284       then show ?thesis

   285         by blast

   286     next

   287       case (Suc m)

   288       have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>

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

   290         by (rule newInt_ex)

   291       then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"

   292         by auto

   293       with Suc have "?g n = {a..b} \<and> a \<le> b"

   294         by auto

   295       then show ?thesis

   296         by blast

   297     qed

   298   qed

   299   ultimately show ?thesis by (rule NIP)

   300 qed

   301

   302

   303 subsection {* Final Theorem *}

   304

   305 theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"

   306 proof

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

   308   then obtain f :: "nat \<Rightarrow> real" where "surj f"

   309     by auto

   310   txt "We now produce a real number x that is not in the range of f, using the properties of newInt."

   311   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"

   312     using newInt_notempty by blast

   313   moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"

   314     by (rule newInt_inter)

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

   316     by blast

   317   moreover from surj f have "x \<in> range f"

   318     by simp

   319   ultimately show False

   320     by blast

   321 qed

   322

   323 end

   324