author hoelzl Wed Jun 11 13:39:38 2014 +0200 (2014-06-11) changeset 57234 596a499318ab parent 57233 8fcbfce2a2a9 child 57235 b0b9a10e4bf4
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
```     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Thu Jun 12 08:48:59 2014 +0200
1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Jun 11 13:39:38 2014 +0200
1.3 @@ -1,11 +1,12 @@
1.4  (*  Title:      HOL/Library/ContNonDenum.thy
1.5      Author:     Benjamin Porter, Monash University, NICTA, 2005
1.6 +    Author:     Johannes Hölzl, TU München
1.7  *)
1.8
1.9  header {* Non-denumerability of the Continuum. *}
1.10
1.11  theory ContNotDenum
1.12 -imports Complex_Main
1.13 +imports Complex_Main Countable_Set
1.14  begin
1.15
1.16  subsection {* Abstract *}
1.17 @@ -29,295 +30,96 @@
1.18  "f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
1.19  by generating a sequence of closed intervals then using the NIP. *}
1.20
1.21 +theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
1.22 +proof
1.23 +  assume "\<exists>f::nat \<Rightarrow> real. surj f"
1.24 +  then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
1.25
1.26 -subsection {* Closed Intervals *}
1.27 -
1.28 -subsection {* Nested Interval Property *}
1.29 +  txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
1.30
1.31 -theorem NIP:
1.32 -  fixes f :: "nat \<Rightarrow> real set"
1.33 -  assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
1.34 -    and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
1.35 -  shows "(\<Inter>n. f n) \<noteq> {}"
1.36 -proof -
1.37 -  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
1.38 -  {
1.39 -    fix n
1.40 -    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
1.41 -      by auto
1.42 -    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
1.43 -      by auto
1.44 -  }
1.45 -  note f_eq = this
1.46 -  {
1.47 -    fix n m :: nat
1.48 -    assume "n \<le> m"
1.49 -    then have "f m \<subseteq> f n"
1.50 -      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
1.51 -  }
1.52 -  note subset' = this
1.53 +  have "\<forall>a b c::real. a < b \<longrightarrow> (\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb})"
1.54 +    using assms
1.55 +    by (auto simp add: not_le cong: conj_cong)
1.56 +       (metis dense le_less_linear less_linear less_trans order_refl)
1.57 +  then obtain i j where ij:
1.58 +    "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
1.59 +    "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
1.60 +    "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
1.61 +    by metis
1.62
1.63 -  have "compact (f 0)"
1.64 -    by (subst f_eq) (rule compact_Icc)
1.65 -  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
1.66 -  proof (rule compact_imp_fip_image)
1.67 -    fix I :: "nat set"
1.68 -    assume I: "finite I"
1.69 -    have "{} \<subset> f (Max (insert 0 I))"
1.70 -      using f_eq[of "Max (insert 0 I)"] by auto
1.71 -    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
1.72 -    proof (rule INF_greatest)
1.73 -      fix i
1.74 -      assume "i \<in> insert 0 I"
1.75 -      with I show "f (Max (insert 0 I)) \<subseteq> f i"
1.76 -        by (intro subset') auto
1.77 -    qed
1.78 -    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
1.79 -      by auto
1.80 -  qed (subst f_eq, auto)
1.81 -  then show "(\<Inter>n. f n) \<noteq> {}"
1.82 -    by auto
1.83 -qed
1.84 +  def ivl \<equiv> "rec_nat (f 0 + 1, f 0 + 2) (\<lambda>n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
1.85 +  def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
1.86
1.87 +  have ivl[simp]:
1.88 +    "ivl 0 = (f 0 + 1, f 0 + 2)"
1.89 +    "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
1.90 +    unfolding ivl_def by simp_all
1.91
1.92 -subsection {* Generating the intervals *}
1.93 +  txt {* This is a decreasing sequence of non-empty intervals. *}
1.94
1.95 -subsubsection {* Existence of non-singleton closed intervals *}
1.96 +  { fix n have "fst (ivl n) < snd (ivl n)"
1.97 +      by (induct n) (auto intro!: ij) }
1.98 +  note less = this
1.99
1.100 -text {* This lemma asserts that given any non-singleton closed
1.101 -interval (a,b) and any element c, there exists a closed interval that
1.102 -is a subset of (a,b) and that does not contain c and is a
1.103 -non-singleton itself. *}
1.104 +  have "decseq I"
1.105 +    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
1.106 +
1.107 +  txt {* Now we apply the finite intersection property of compact sets. *}
1.108
1.109 -lemma closed_subset_ex:
1.110 -  fixes c :: real
1.111 -  assumes "a < b"
1.112 -  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
1.113 -proof (cases "c < b")
1.114 -  case True
1.115 -  show ?thesis
1.116 -  proof (cases "c < a")
1.117 -    case True
1.118 -    with `a < b` `c < b` have "c \<notin> {a..b}"
1.119 -      by auto
1.120 -    with `a < b` show ?thesis
1.121 -      by auto
1.122 -  next
1.123 -    case False
1.124 -    then have "a \<le> c" by simp
1.125 -    def ka \<equiv> "(c + b)/2"
1.126 -    from ka_def `c < b` have "ka < b"
1.127 +  have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
1.128 +  proof (rule compact_imp_fip_image)
1.129 +    fix S :: "nat set" assume fin: "finite S"
1.130 +    have "{} \<subset> I (Max (insert 0 S))"
1.131 +      unfolding I_def using less[of "Max (insert 0 S)"] by auto
1.132 +    also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
1.133 +      using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
1.134 +    also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
1.135        by auto
1.136 -    moreover from ka_def `c < b` have "ka > c"
1.137 -      by simp
1.138 -    ultimately have "c \<notin> {ka..b}"
1.139 -      by auto
1.140 -    moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
1.141 -      by simp
1.142 -    then have "{ka..b} \<subseteq> {a..b}"
1.143 -      by auto
1.144 -    ultimately have "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
1.145 -      using `ka < b` by auto
1.146 -    then show ?thesis
1.147 +    finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
1.148        by auto
1.149 -  qed
1.150 -next
1.151 -  case False
1.152 -  then have "c \<ge> b" by simp
1.153 -  def kb \<equiv> "(a + b)/2"
1.154 -  with `a < b` have "kb < b" by auto
1.155 -  with kb_def `c \<ge> b` have "a < kb" "kb < c"
1.156 -    by auto
1.157 -  from `kb < c` have c: "c \<notin> {a..kb}"
1.158 -    by auto
1.159 -  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
1.160 -    by auto
1.161 -  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
1.162 -    by simp
1.163 -  then show ?thesis
1.164 -    by auto
1.165 +  qed (auto simp: I_def)
1.166 +  then obtain x where "\<And>n. x \<in> I n"
1.167 +    by blast
1.168 +  moreover from `surj f` obtain j where "x = f j"
1.169 +    by blast
1.170 +  ultimately have "f j \<in> I (Suc j)"
1.171 +    by blast
1.172 +  with ij(3)[OF less] show False
1.173 +    unfolding I_def ivl fst_conv snd_conv by auto
1.174  qed
1.175
1.176 -
1.177 -subsection {* newInt: Interval generation *}
1.178 -
1.179 -text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
1.180 -closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
1.181 -does not contain @{text "f (Suc n)"}. With the base case defined such
1.182 -that @{text "(f 0)\<notin>newInt 0 f"}. *}
1.183 -
1.184 -
1.185 -subsubsection {* Definition *}
1.186 -
1.187 -primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
1.188 -where
1.189 -  "newInt 0 f = {f 0 + 1..f 0 + 2}"
1.190 -| "newInt (Suc n) f =
1.191 -    (SOME e.
1.192 -      (\<exists>e1 e2.
1.193 -         e1 < e2 \<and>
1.194 -         e = {e1..e2} \<and>
1.195 -         e \<subseteq> newInt n f \<and>
1.196 -         f (Suc n) \<notin> e))"
1.197 -
1.198 -
1.199 -subsubsection {* Properties *}
1.200 -
1.201 -text {* We now show that every application of newInt returns an
1.202 -appropriate interval. *}
1.203 -
1.204 -lemma newInt_ex:
1.205 -  "\<exists>a b. a < b \<and>
1.206 -    newInt (Suc n) f = {a..b} \<and>
1.207 -    newInt (Suc n) f \<subseteq> newInt n f \<and>
1.208 -    f (Suc n) \<notin> newInt (Suc n) f"
1.209 -proof (induct n)
1.210 -  case 0
1.211 -  let ?e = "SOME e. \<exists>e1 e2.
1.212 -    e1 < e2 \<and>
1.213 -    e = {e1..e2} \<and>
1.214 -    e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
1.215 -    f (Suc 0) \<notin> e"
1.216 +lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
1.217 +  using real_non_denum unfolding uncountable_def by auto
1.218
1.219 -  have "newInt (Suc 0) f = ?e" by auto
1.220 -  moreover
1.221 -  have "f 0 + 1 < f 0 + 2" by simp
1.222 -  with closed_subset_ex
1.223 -  have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
1.224 -  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"
1.225 -    by simp
1.226 -  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"
1.227 -    by (rule someI_ex)
1.228 -  ultimately have "\<exists>e1 e2. e1 < e2 \<and>
1.229 -      newInt (Suc 0) f = {e1..e2} \<and>
1.230 -      newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
1.231 -      f (Suc 0) \<notin> newInt (Suc 0) f"
1.232 -    by simp
1.233 -  then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
1.234 -      newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
1.235 -    by simp
1.236 -next
1.237 -  case (Suc n)
1.238 -  then have "\<exists>a b.
1.239 -      a < b \<and>
1.240 -      newInt (Suc n) f = {a..b} \<and>
1.241 -      newInt (Suc n) f \<subseteq> newInt n f \<and>
1.242 -      f (Suc n) \<notin> newInt (Suc n) f"
1.243 -    by simp
1.244 -  then obtain a and b where ab: "a < b \<and>
1.245 -      newInt (Suc n) f = {a..b} \<and>
1.246 -      newInt (Suc n) f \<subseteq> newInt n f \<and>
1.247 -      f (Suc n) \<notin> newInt (Suc n) f"
1.248 -    by auto
1.249 -  then have cab: "{a..b} = newInt (Suc n) f"
1.250 -    by simp
1.251 -
1.252 -  let ?e = "SOME e. \<exists>e1 e2.
1.253 -      e1 < e2 \<and>
1.254 -      e = {e1..e2} \<and>
1.255 -      e \<subseteq> {a..b} \<and>
1.256 -      f (Suc (Suc n)) \<notin> e"
1.257 -  from cab have ni: "newInt (Suc (Suc n)) f = ?e"
1.258 -    by auto
1.259 -
1.260 -  from ab have "a < b" by simp
1.261 -  with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
1.262 -    f (Suc (Suc n)) \<notin> {ka..kb}" .
1.263 -  then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
1.264 -      {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
1.265 -    by simp
1.266 -  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"
1.267 -    by simp
1.268 -  then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
1.269 -    by (rule someI_ex)
1.270 -  with ab ni show "\<exists>ka kb. ka < kb \<and>
1.271 -      newInt (Suc (Suc n)) f = {ka..kb} \<and>
1.272 -      newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
1.273 -      f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
1.274 -    by auto
1.275 +lemma bij_betw_open_intervals:
1.276 +  fixes a b c d :: real
1.277 +  assumes "a < b" "c < d"
1.278 +  shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
1.279 +proof -
1.280 +  def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
1.281 +  { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
1.282 +    moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
1.283 +      by (intro mult_strict_left_mono) simp_all
1.284 +    moreover from * have "0 < (d - c) * (x - a) / (b - a)"
1.285 +      by simp
1.286 +    ultimately have "f a b c d x < d" "c < f a b c d x"
1.287 +      by (simp_all add: f_def field_simps) }
1.288 +  with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
1.289 +    by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
1.290 +  thus ?thesis by auto
1.291  qed
1.292
1.293 -lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
1.294 -  using newInt_ex by auto
1.295 -
1.296 -
1.297 -text {* Another fundamental property is that no element in the range
1.298 -of f is in the intersection of all closed intervals generated by
1.299 -newInt. *}
1.300 +lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
1.301 +  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
1.302
1.303 -lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
1.304 -proof
1.305 -  fix n :: nat
1.306 -  have "f n \<notin> newInt n f"
1.307 -  proof (cases n)
1.308 -    case 0
1.309 -    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
1.310 -      by simp
1.311 -    ultimately show ?thesis by simp
1.312 -  next
1.313 -    case (Suc m)
1.314 -    from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
1.315 -      newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
1.316 -    then have "f (Suc m) \<notin> newInt (Suc m) f"
1.317 -      by auto
1.318 -    with Suc show ?thesis by simp
1.319 -  qed
1.320 -  then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
1.321 -qed
1.322 -
1.323 -lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
1.324 +lemma uncountable_open_interval:
1.325 +  fixes a b :: real assumes ab: "a < b"
1.326 +  shows "uncountable {a<..<b}"
1.327  proof -
1.328 -  let ?g = "\<lambda>n. newInt n f"
1.329 -  have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
1.330 -  proof
1.331 -    fix n
1.332 -    show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
1.333 -  qed
1.334 -  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
1.335 -  proof
1.336 -    fix n :: nat
1.337 -    show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
1.338 -    proof (cases n)
1.339 -      case 0
1.340 -      then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
1.341 -        by simp
1.342 -      then show ?thesis
1.343 -        by blast
1.344 -    next
1.345 -      case (Suc m)
1.346 -      have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
1.347 -        (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
1.348 -        by (rule newInt_ex)
1.349 -      then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
1.350 -        by auto
1.351 -      with Suc have "?g n = {a..b} \<and> a \<le> b"
1.352 -        by auto
1.353 -      then show ?thesis
1.354 -        by blast
1.355 -    qed
1.356 -  qed
1.357 -  ultimately show ?thesis by (rule NIP)
1.358 -qed
1.359 -
1.360 -
1.361 -subsection {* Final Theorem *}
1.362 -
1.363 -theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
1.364 -proof
1.365 -  assume "\<exists>f :: nat \<Rightarrow> real. surj f"
1.366 -  then obtain f :: "nat \<Rightarrow> real" where "surj f"
1.367 -    by auto
1.368 -  txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
1.369 -  have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
1.370 -    using newInt_notempty by blast
1.371 -  moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
1.372 -    by (rule newInt_inter)
1.373 -  ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
1.374 -    by blast
1.375 -  moreover from `surj f` have "x \<in> range f"
1.376 -    by simp
1.377 -  ultimately show False
1.378 -    by blast
1.379 +  obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
1.380 +    using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
1.381 +  then show ?thesis
1.382 +    by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
1.383  qed
1.384
1.385  end
```
```     2.1 --- a/src/HOL/Library/Countable_Set.thy	Thu Jun 12 08:48:59 2014 +0200
2.2 +++ b/src/HOL/Library/Countable_Set.thy	Wed Jun 11 13:39:38 2014 +0200
2.3 @@ -296,4 +296,23 @@
2.4    qed
2.5  qed
2.6
2.7 +subsection {* Uncountable *}
2.8 +
2.9 +abbreviation uncountable where
2.10 +  "uncountable A \<equiv> \<not> countable A"
2.11 +
2.12 +lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
2.13 +  by (auto intro: inj_on_inv_into simp: countable_def)
2.14 +     (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
2.15 +
2.16 +lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
2.17 +  unfolding bij_betw_def by (metis countable_image)
2.18 +
2.19 +lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
2.20 +  by (metis countable_finite)
2.21 +
2.22 +lemma uncountable_minus_countable:
2.23 +  "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
2.24 +  using countable_Un[of B "A - B"] assms by auto
2.25 +
2.26  end
```