src/HOL/Library/ContNotDenum.thy
author hoelzl
Wed, 18 Dec 2013 11:53:40 +0100
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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28562
diff changeset
     1
(*  Title       : HOL/ContNonDenum
23461
wenzelm
parents: 23389
diff changeset
     2
    Author      : Benjamin Porter, Monash University, NICTA, 2005
wenzelm
parents: 23389
diff changeset
     3
*)
wenzelm
parents: 23389
diff changeset
     4
wenzelm
parents: 23389
diff changeset
     5
header {* Non-denumerability of the Continuum. *}
wenzelm
parents: 23389
diff changeset
     6
wenzelm
parents: 23389
diff changeset
     7
theory ContNotDenum
30663
0b6aff7451b2 Main is (Complex_Main) base entry point in library theories
haftmann
parents: 29026
diff changeset
     8
imports Complex_Main
23461
wenzelm
parents: 23389
diff changeset
     9
begin
wenzelm
parents: 23389
diff changeset
    10
wenzelm
parents: 23389
diff changeset
    11
subsection {* Abstract *}
wenzelm
parents: 23389
diff changeset
    12
wenzelm
parents: 23389
diff changeset
    13
text {* The following document presents a proof that the Continuum is
wenzelm
parents: 23389
diff changeset
    14
uncountable. It is formalised in the Isabelle/Isar theorem proving
wenzelm
parents: 23389
diff changeset
    15
system.
wenzelm
parents: 23389
diff changeset
    16
wenzelm
parents: 23389
diff changeset
    17
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
wenzelm
parents: 23389
diff changeset
    18
words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
wenzelm
parents: 23389
diff changeset
    19
surjective.
wenzelm
parents: 23389
diff changeset
    20
wenzelm
parents: 23389
diff changeset
    21
{\em Outline:} An elegant informal proof of this result uses Cantor's
wenzelm
parents: 23389
diff changeset
    22
Diagonalisation argument. The proof presented here is not this
wenzelm
parents: 23389
diff changeset
    23
one. First we formalise some properties of closed intervals, then we
wenzelm
parents: 23389
diff changeset
    24
prove the Nested Interval Property. This property relies on the
wenzelm
parents: 23389
diff changeset
    25
completeness of the Real numbers and is the foundation for our
wenzelm
parents: 23389
diff changeset
    26
argument. Informally it states that an intersection of countable
wenzelm
parents: 23389
diff changeset
    27
closed intervals (where each successive interval is a subset of the
wenzelm
parents: 23389
diff changeset
    28
last) is non-empty. We then assume a surjective function f:@{text
wenzelm
parents: 23389
diff changeset
    29
"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
wenzelm
parents: 23389
diff changeset
    30
by generating a sequence of closed intervals then using the NIP. *}
wenzelm
parents: 23389
diff changeset
    31
wenzelm
parents: 23389
diff changeset
    32
subsection {* Closed Intervals *}
wenzelm
parents: 23389
diff changeset
    33
wenzelm
parents: 23389
diff changeset
    34
subsection {* Nested Interval Property *}
wenzelm
parents: 23389
diff changeset
    35
wenzelm
parents: 23389
diff changeset
    36
theorem NIP:
wenzelm
parents: 23389
diff changeset
    37
  fixes f::"nat \<Rightarrow> real set"
wenzelm
parents: 23389
diff changeset
    38
  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    39
  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
23461
wenzelm
parents: 23389
diff changeset
    40
  shows "(\<Inter>n. f n) \<noteq> {}"
wenzelm
parents: 23389
diff changeset
    41
proof -
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    42
  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    43
  { fix n 
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    44
    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    45
      by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    46
    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    47
      by auto }
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    48
  note f_eq = this
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    49
  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    50
      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    51
  note subset' = this
23461
wenzelm
parents: 23389
diff changeset
    52
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    53
  have "compact (f 0)"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    54
    by (subst f_eq) (rule compact_Icc)
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    55
  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    56
  proof (rule compact_imp_fip_image)
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    57
    fix I :: "nat set" assume I: "finite I"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    58
    have "{} \<subset> f (Max (insert 0 I))"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    59
      using f_eq[of "Max (insert 0 I)"] by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    60
    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    61
    proof (rule INF_greatest)
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    62
      fix i assume "i \<in> insert 0 I"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    63
      with I show "f (Max (insert 0 I)) \<subseteq> f i"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    64
        by (intro subset') auto
23461
wenzelm
parents: 23389
diff changeset
    65
    qed
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    66
    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    67
      by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    68
  qed (subst f_eq, auto)
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    69
  then show "(\<Inter>n. f n) \<noteq> {}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    70
    by auto
23461
wenzelm
parents: 23389
diff changeset
    71
qed
wenzelm
parents: 23389
diff changeset
    72
wenzelm
parents: 23389
diff changeset
    73
subsection {* Generating the intervals *}
wenzelm
parents: 23389
diff changeset
    74
wenzelm
parents: 23389
diff changeset
    75
subsubsection {* Existence of non-singleton closed intervals *}
wenzelm
parents: 23389
diff changeset
    76
wenzelm
parents: 23389
diff changeset
    77
text {* This lemma asserts that given any non-singleton closed
wenzelm
parents: 23389
diff changeset
    78
interval (a,b) and any element c, there exists a closed interval that
wenzelm
parents: 23389
diff changeset
    79
is a subset of (a,b) and that does not contain c and is a
wenzelm
parents: 23389
diff changeset
    80
non-singleton itself. *}
wenzelm
parents: 23389
diff changeset
    81
wenzelm
parents: 23389
diff changeset
    82
lemma closed_subset_ex:
wenzelm
parents: 23389
diff changeset
    83
  fixes c::real
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    84
  assumes "a < b"
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    85
  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    86
proof (cases "c < b")
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    87
  case True
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    88
  show ?thesis
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    89
  proof (cases "c < a")
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    90
    case True
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    91
    with `a < b` `c < b` have "c \<notin> {a..b}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
    92
      by auto
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    93
    with `a < b` show ?thesis by auto
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    94
  next
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    95
    case False
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    96
    then have "a \<le> c" by simp
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    97
    def ka \<equiv> "(c + b)/2"
23461
wenzelm
parents: 23389
diff changeset
    98
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    99
    from ka_def `c < b` have kalb: "ka < b" by auto
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   100
    moreover from ka_def `c < b` have kagc: "ka > c" by simp
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   101
    ultimately have "c\<notin>{ka..b}" by auto
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   102
    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   103
    hence "{ka..b} \<subseteq> {a..b}" by auto
23461
wenzelm
parents: 23389
diff changeset
   104
    ultimately have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   105
      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   106
      using kalb by auto
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   107
    then show ?thesis
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   108
      by auto
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   109
  qed
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   110
next
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   111
  case False
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   112
  then have "c \<ge> b" by simp
23461
wenzelm
parents: 23389
diff changeset
   113
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   114
  def kb \<equiv> "(a + b)/2"
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   115
  with `a < b` have "kb < b" by auto
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   116
  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   117
  from `kb < c` have c: "c \<notin> {a..kb}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   118
    by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   119
  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   120
    by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   121
  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   122
    by simp
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
   123
  then show ?thesis by auto
23461
wenzelm
parents: 23389
diff changeset
   124
qed
wenzelm
parents: 23389
diff changeset
   125
wenzelm
parents: 23389
diff changeset
   126
subsection {* newInt: Interval generation *}
wenzelm
parents: 23389
diff changeset
   127
wenzelm
parents: 23389
diff changeset
   128
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
wenzelm
parents: 23389
diff changeset
   129
closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
wenzelm
parents: 23389
diff changeset
   130
does not contain @{text "f (Suc n)"}. With the base case defined such
wenzelm
parents: 23389
diff changeset
   131
that @{text "(f 0)\<notin>newInt 0 f"}. *}
wenzelm
parents: 23389
diff changeset
   132
wenzelm
parents: 23389
diff changeset
   133
subsubsection {* Definition *}
wenzelm
parents: 23389
diff changeset
   134
27435
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   135
primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   136
  "newInt 0 f = {f 0 + 1..f 0 + 2}"
27435
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   137
  | "newInt (Suc n) f =
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   138
      (SOME e. (\<exists>e1 e2.
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   139
       e1 < e2 \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   140
       e = {e1..e2} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   141
       e \<subseteq> newInt n f \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   142
       f (Suc n) \<notin> e)
27435
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   143
      )"
b3f8e9bdf9a7 cleaned up some code generator configuration
haftmann
parents: 27368
diff changeset
   144
23461
wenzelm
parents: 23389
diff changeset
   145
wenzelm
parents: 23389
diff changeset
   146
subsubsection {* Properties *}
wenzelm
parents: 23389
diff changeset
   147
wenzelm
parents: 23389
diff changeset
   148
text {* We now show that every application of newInt returns an
wenzelm
parents: 23389
diff changeset
   149
appropriate interval. *}
wenzelm
parents: 23389
diff changeset
   150
wenzelm
parents: 23389
diff changeset
   151
lemma newInt_ex:
wenzelm
parents: 23389
diff changeset
   152
  "\<exists>a b. a < b \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   153
   newInt (Suc n) f = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   154
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm
parents: 23389
diff changeset
   155
   f (Suc n) \<notin> newInt (Suc n) f"
wenzelm
parents: 23389
diff changeset
   156
proof (induct n)
wenzelm
parents: 23389
diff changeset
   157
  case 0
wenzelm
parents: 23389
diff changeset
   158
wenzelm
parents: 23389
diff changeset
   159
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm
parents: 23389
diff changeset
   160
   e1 < e2 \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   161
   e = {e1..e2} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   162
   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
23461
wenzelm
parents: 23389
diff changeset
   163
   f (Suc 0) \<notin> e"
wenzelm
parents: 23389
diff changeset
   164
wenzelm
parents: 23389
diff changeset
   165
  have "newInt (Suc 0) f = ?e" by auto
wenzelm
parents: 23389
diff changeset
   166
  moreover
wenzelm
parents: 23389
diff changeset
   167
  have "f 0 + 1 < f 0 + 2" by simp
wenzelm
parents: 23389
diff changeset
   168
  with closed_subset_ex have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   169
    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   170
     f (Suc 0) \<notin> {ka..kb}" .
23461
wenzelm
parents: 23389
diff changeset
   171
  hence
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   172
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   173
     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
23461
wenzelm
parents: 23389
diff changeset
   174
  hence
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   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"
23461
wenzelm
parents: 23389
diff changeset
   176
    by (rule someI_ex)
wenzelm
parents: 23389
diff changeset
   177
  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   178
   newInt (Suc 0) f = {e1..e2} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   179
   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
23461
wenzelm
parents: 23389
diff changeset
   180
   f (Suc 0) \<notin> newInt (Suc 0) f" by simp
wenzelm
parents: 23389
diff changeset
   181
  thus
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   182
    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   183
     newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
wenzelm
parents: 23389
diff changeset
   184
    by simp
wenzelm
parents: 23389
diff changeset
   185
next
wenzelm
parents: 23389
diff changeset
   186
  case (Suc n)
wenzelm
parents: 23389
diff changeset
   187
  hence "\<exists>a b.
wenzelm
parents: 23389
diff changeset
   188
   a < b \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   189
   newInt (Suc n) f = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   190
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm
parents: 23389
diff changeset
   191
   f (Suc n) \<notin> newInt (Suc n) f" by simp
wenzelm
parents: 23389
diff changeset
   192
  then obtain a and b where ab: "a < b \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   193
   newInt (Suc n) f = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   194
   newInt (Suc n) f \<subseteq> newInt n f \<and>
wenzelm
parents: 23389
diff changeset
   195
   f (Suc n) \<notin> newInt (Suc n) f" by auto
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   196
  hence cab: "{a..b} = newInt (Suc n) f" by simp
23461
wenzelm
parents: 23389
diff changeset
   197
wenzelm
parents: 23389
diff changeset
   198
  let ?e = "SOME e. \<exists>e1 e2.
wenzelm
parents: 23389
diff changeset
   199
    e1 < e2 \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   200
    e = {e1..e2} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   201
    e \<subseteq> {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   202
    f (Suc (Suc n)) \<notin> e"
wenzelm
parents: 23389
diff changeset
   203
  from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
wenzelm
parents: 23389
diff changeset
   204
wenzelm
parents: 23389
diff changeset
   205
  from ab have "a < b" by simp
wenzelm
parents: 23389
diff changeset
   206
  with closed_subset_ex have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   207
    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   208
     f (Suc (Suc n)) \<notin> {ka..kb}" .
23461
wenzelm
parents: 23389
diff changeset
   209
  hence
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   210
    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   211
     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
23461
wenzelm
parents: 23389
diff changeset
   212
    by simp
wenzelm
parents: 23389
diff changeset
   213
  hence
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   214
    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   215
     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
23461
wenzelm
parents: 23389
diff changeset
   216
  hence
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   217
    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   218
     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
23461
wenzelm
parents: 23389
diff changeset
   219
  with ab ni show
wenzelm
parents: 23389
diff changeset
   220
    "\<exists>ka kb. ka < kb \<and>
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   221
     newInt (Suc (Suc n)) f = {ka..kb} \<and>
23461
wenzelm
parents: 23389
diff changeset
   222
     newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
wenzelm
parents: 23389
diff changeset
   223
     f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
wenzelm
parents: 23389
diff changeset
   224
qed
wenzelm
parents: 23389
diff changeset
   225
wenzelm
parents: 23389
diff changeset
   226
lemma newInt_subset:
wenzelm
parents: 23389
diff changeset
   227
  "newInt (Suc n) f \<subseteq> newInt n f"
wenzelm
parents: 23389
diff changeset
   228
  using newInt_ex by auto
wenzelm
parents: 23389
diff changeset
   229
wenzelm
parents: 23389
diff changeset
   230
wenzelm
parents: 23389
diff changeset
   231
text {* Another fundamental property is that no element in the range
wenzelm
parents: 23389
diff changeset
   232
of f is in the intersection of all closed intervals generated by
wenzelm
parents: 23389
diff changeset
   233
newInt. *}
wenzelm
parents: 23389
diff changeset
   234
wenzelm
parents: 23389
diff changeset
   235
lemma newInt_inter:
wenzelm
parents: 23389
diff changeset
   236
  "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
wenzelm
parents: 23389
diff changeset
   237
proof
wenzelm
parents: 23389
diff changeset
   238
  fix n::nat
wenzelm
parents: 23389
diff changeset
   239
  {
wenzelm
parents: 23389
diff changeset
   240
    assume n0: "n = 0"
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   241
    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   242
    ultimately have "f n \<notin> newInt n f" by simp
23461
wenzelm
parents: 23389
diff changeset
   243
  }
wenzelm
parents: 23389
diff changeset
   244
  moreover
wenzelm
parents: 23389
diff changeset
   245
  {
wenzelm
parents: 23389
diff changeset
   246
    assume "\<not> n = 0"
wenzelm
parents: 23389
diff changeset
   247
    hence "n > 0" by simp
wenzelm
parents: 23389
diff changeset
   248
    then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm
parents: 23389
diff changeset
   249
wenzelm
parents: 23389
diff changeset
   250
    from newInt_ex have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   251
      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   252
       newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
wenzelm
parents: 23389
diff changeset
   253
    then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
wenzelm
parents: 23389
diff changeset
   254
    with ndef have "f n \<notin> newInt n f" by simp
wenzelm
parents: 23389
diff changeset
   255
  }
wenzelm
parents: 23389
diff changeset
   256
  ultimately have "f n \<notin> newInt n f" by (rule case_split)
wenzelm
parents: 23389
diff changeset
   257
  thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
wenzelm
parents: 23389
diff changeset
   258
qed
wenzelm
parents: 23389
diff changeset
   259
wenzelm
parents: 23389
diff changeset
   260
wenzelm
parents: 23389
diff changeset
   261
lemma newInt_notempty:
wenzelm
parents: 23389
diff changeset
   262
  "(\<Inter>n. newInt n f) \<noteq> {}"
wenzelm
parents: 23389
diff changeset
   263
proof -
wenzelm
parents: 23389
diff changeset
   264
  let ?g = "\<lambda>n. newInt n f"
wenzelm
parents: 23389
diff changeset
   265
  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
wenzelm
parents: 23389
diff changeset
   266
  proof
wenzelm
parents: 23389
diff changeset
   267
    fix n
wenzelm
parents: 23389
diff changeset
   268
    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
wenzelm
parents: 23389
diff changeset
   269
  qed
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   270
  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
23461
wenzelm
parents: 23389
diff changeset
   271
  proof
wenzelm
parents: 23389
diff changeset
   272
    fix n::nat
wenzelm
parents: 23389
diff changeset
   273
    {
wenzelm
parents: 23389
diff changeset
   274
      assume "n = 0"
wenzelm
parents: 23389
diff changeset
   275
      then have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   276
        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
23461
wenzelm
parents: 23389
diff changeset
   277
        by simp
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   278
      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
23461
wenzelm
parents: 23389
diff changeset
   279
    }
wenzelm
parents: 23389
diff changeset
   280
    moreover
wenzelm
parents: 23389
diff changeset
   281
    {
wenzelm
parents: 23389
diff changeset
   282
      assume "\<not> n = 0"
wenzelm
parents: 23389
diff changeset
   283
      then have "n > 0" by simp
wenzelm
parents: 23389
diff changeset
   284
      then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
wenzelm
parents: 23389
diff changeset
   285
wenzelm
parents: 23389
diff changeset
   286
      have
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   287
        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
23461
wenzelm
parents: 23389
diff changeset
   288
        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
wenzelm
parents: 23389
diff changeset
   289
        by (rule newInt_ex)
wenzelm
parents: 23389
diff changeset
   290
      then obtain a and b where
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   291
        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   292
      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   293
      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
23461
wenzelm
parents: 23389
diff changeset
   294
    }
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   295
    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
23461
wenzelm
parents: 23389
diff changeset
   296
  qed
wenzelm
parents: 23389
diff changeset
   297
  ultimately show ?thesis by (rule NIP)
wenzelm
parents: 23389
diff changeset
   298
qed
wenzelm
parents: 23389
diff changeset
   299
wenzelm
parents: 23389
diff changeset
   300
wenzelm
parents: 23389
diff changeset
   301
subsection {* Final Theorem *}
wenzelm
parents: 23389
diff changeset
   302
wenzelm
parents: 23389
diff changeset
   303
theorem real_non_denum:
wenzelm
parents: 23389
diff changeset
   304
  shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
wenzelm
parents: 23389
diff changeset
   305
proof -- "by contradiction"
wenzelm
parents: 23389
diff changeset
   306
  assume "\<exists>f::nat\<Rightarrow>real. surj f"
40702
cf26dd7395e4 Replace surj by abbreviation; remove surj_on.
hoelzl
parents: 37765
diff changeset
   307
  then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
23461
wenzelm
parents: 23389
diff changeset
   308
  -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
wenzelm
parents: 23389
diff changeset
   309
  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
wenzelm
parents: 23389
diff changeset
   310
  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
wenzelm
parents: 23389
diff changeset
   311
  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
wenzelm
parents: 23389
diff changeset
   312
  moreover from rangeF have "x \<in> range f" by simp
wenzelm
parents: 23389
diff changeset
   313
  ultimately show False by blast
wenzelm
parents: 23389
diff changeset
   314
qed
wenzelm
parents: 23389
diff changeset
   315
wenzelm
parents: 23389
diff changeset
   316
end
54797
be020ec8560c modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents: 54263
diff changeset
   317