src/HOL/Library/ContNotDenum.thy
 author hoelzl Wed Dec 18 11:53:40 2013 +0100 (2013-12-18) changeset 54797 be020ec8560c parent 54263 c4159fe6fa46 child 56796 9f84219715a7 permissions -rw-r--r--
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
     1 (*  Title       : HOL/ContNonDenum

     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 f:@{text "\<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 f:@{text

    29 "\<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 subsection {* Closed Intervals *}

    33

    34 subsection {* Nested Interval Property *}

    35

    36 theorem NIP:

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

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

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

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

    41 proof -

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

    43   { fix n

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

    45       by auto

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

    47       by auto }

    48   note f_eq = this

    49   { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"

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

    51   note subset' = this

    52

    53   have "compact (f 0)"

    54     by (subst f_eq) (rule compact_Icc)

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

    56   proof (rule compact_imp_fip_image)

    57     fix I :: "nat set" assume I: "finite I"

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

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

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

    61     proof (rule INF_greatest)

    62       fix i assume "i \<in> insert 0 I"

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

    64         by (intro subset') auto

    65     qed

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

    67       by auto

    68   qed (subst f_eq, auto)

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

    70     by auto

    71 qed

    72

    73 subsection {* Generating the intervals *}

    74

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

    76

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

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

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

    80 non-singleton itself. *}

    81

    82 lemma closed_subset_ex:

    83   fixes c::real

    84   assumes "a < b"

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

    86 proof (cases "c < b")

    87   case True

    88   show ?thesis

    89   proof (cases "c < a")

    90     case True

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

    92       by auto

    93     with a < b show ?thesis by auto

    94   next

    95     case False

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

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

    98

    99     from ka_def c < b have kalb: "ka < b" by auto

   100     moreover from ka_def c < b have kagc: "ka > c" by simp

   101     ultimately have "c\<notin>{ka..b}" by auto

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

   103     hence "{ka..b} \<subseteq> {a..b}" by auto

   104     ultimately have

   105       "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"

   106       using kalb by auto

   107     then show ?thesis

   108       by auto

   109   qed

   110 next

   111   case False

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

   113

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

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

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

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

   118     by auto

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

   120     by auto

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

   122     by simp

   123   then show ?thesis by auto

   124 qed

   125

   126 subsection {* newInt: Interval generation *}

   127

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

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

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

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

   132

   133 subsubsection {* Definition *}

   134

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

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

   137   | "newInt (Suc n) f =

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

   139        e1 < e2 \<and>

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

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

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

   143       )"

   144

   145

   146 subsubsection {* Properties *}

   147

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

   149 appropriate interval. *}

   150

   151 lemma newInt_ex:

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

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

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

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

   156 proof (induct n)

   157   case 0

   158

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

   160    e1 < e2 \<and>

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

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

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

   164

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

   166   moreover

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

   168   with closed_subset_ex have

   169     "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>

   170      f (Suc 0) \<notin> {ka..kb}" .

   171   hence

   172     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>

   173      e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp

   174   hence

   175     "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"

   176     by (rule someI_ex)

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

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

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

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

   181   thus

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

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

   184     by simp

   185 next

   186   case (Suc n)

   187   hence "\<exists>a b.

   188    a < b \<and>

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

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

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

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

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

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

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

   196   hence cab: "{a..b} = newInt (Suc n) f" by simp

   197

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

   199     e1 < e2 \<and>

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

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

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

   203   from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto

   204

   205   from ab have "a < b" by simp

   206   with closed_subset_ex have

   207     "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>

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

   209   hence

   210     "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>

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

   212     by simp

   213   hence

   214     "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>

   215      e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp

   216   hence

   217     "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>

   218      ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)

   219   with ab ni show

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

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

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

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

   224 qed

   225

   226 lemma newInt_subset:

   227   "newInt (Suc n) f \<subseteq> newInt n f"

   228   using newInt_ex by auto

   229

   230

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

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

   233 newInt. *}

   234

   235 lemma newInt_inter:

   236   "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"

   237 proof

   238   fix n::nat

   239   {

   240     assume n0: "n = 0"

   241     moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp

   242     ultimately have "f n \<notin> newInt n f" by simp

   243   }

   244   moreover

   245   {

   246     assume "\<not> n = 0"

   247     hence "n > 0" by simp

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

   249

   250     from newInt_ex have

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

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

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

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

   255   }

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

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

   258 qed

   259

   260

   261 lemma newInt_notempty:

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

   263 proof -

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

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

   266   proof

   267     fix n

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

   269   qed

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

   271   proof

   272     fix n::nat

   273     {

   274       assume "n = 0"

   275       then have

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

   277         by simp

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

   279     }

   280     moreover

   281     {

   282       assume "\<not> n = 0"

   283       then have "n > 0" by simp

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

   285

   286       have

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

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

   289         by (rule newInt_ex)

   290       then obtain a and b where

   291         "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto

   292       with nd have "?g n = {a..b} \<and> a \<le> b" by auto

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

   294     }

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

   296   qed

   297   ultimately show ?thesis by (rule NIP)

   298 qed

   299

   300

   301 subsection {* Final Theorem *}

   302

   303 theorem real_non_denum:

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

   305 proof -- "by contradiction"

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

   307   then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto

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

   309   have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast

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

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

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

   313   ultimately show False by blast

   314 qed

   315

   316 end

   317