src/HOL/Library/Continuum_Not_Denumerable.thy
author wenzelm
Tue, 19 Jul 2016 09:55:03 +0200
changeset 63520 2803d2b8f85d
parent 63465 d7610beb98bc
child 63540 f8652d0534fa
permissions -rw-r--r--
Linux platform base-line is Ubuntu 12.04 LTS;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63464
9d4dbb7a548a more standard name;
wenzelm
parents: 63092
diff changeset
     1
(*  Title:      HOL/Library/Continuum_Not_Denumerable.thy
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
     2
    Author:     Benjamin Porter, Monash University, NICTA, 2005
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
     3
    Author:     Johannes Hölzl, TU München
23461
wenzelm
parents: 23389
diff changeset
     4
*)
wenzelm
parents: 23389
diff changeset
     5
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
     6
section \<open>Non-denumerability of the Continuum.\<close>
23461
wenzelm
parents: 23389
diff changeset
     7
63464
9d4dbb7a548a more standard name;
wenzelm
parents: 63092
diff changeset
     8
theory Continuum_Not_Denumerable
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
     9
imports Complex_Main Countable_Set
23461
wenzelm
parents: 23389
diff changeset
    10
begin
wenzelm
parents: 23389
diff changeset
    11
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    12
subsection \<open>Abstract\<close>
23461
wenzelm
parents: 23389
diff changeset
    13
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    14
text \<open>
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    15
  The following document presents a proof that the Continuum is uncountable.
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    16
  It is formalised in the Isabelle/Isar theorem proving system.
23461
wenzelm
parents: 23389
diff changeset
    17
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    18
  \<^bold>\<open>Theorem:\<close> The Continuum \<open>\<real>\<close> is not denumerable. In other words, there does
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    19
  not exist a function \<open>f: \<nat> \<Rightarrow> \<real>\<close> such that f is surjective.
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    20
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    21
  \<^bold>\<open>Outline:\<close> An elegant informal proof of this result uses Cantor's
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    22
  Diagonalisation argument. The proof presented here is not this one.
23461
wenzelm
parents: 23389
diff changeset
    23
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    24
  First we formalise some properties of closed intervals, then we prove the
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    25
  Nested Interval Property. This property relies on the completeness of the
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    26
  Real numbers and is the foundation for our argument. Informally it states
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    27
  that an intersection of countable closed intervals (where each successive
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    28
  interval is a subset of the last) is non-empty. We then assume a surjective
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    29
  function \<open>f: \<nat> \<Rightarrow> \<real>\<close> exists and find a real \<open>x\<close> such that \<open>x\<close> is not in the
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    30
  range of \<open>f\<close> by generating a sequence of closed intervals then using the
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    31
  NIP.
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    32
\<close>
23461
wenzelm
parents: 23389
diff changeset
    33
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    34
theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    35
proof
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    36
  assume "\<exists>f::nat \<Rightarrow> real. surj f"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    37
  then obtain f :: "nat \<Rightarrow> real" where "surj f" ..
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    38
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    39
  txt \<open>First we construct a sequence of nested intervals, ignoring @{term "range f"}.\<close>
23461
wenzelm
parents: 23389
diff changeset
    40
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    41
  have "a < b \<Longrightarrow> \<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}" for a b c :: real
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    42
    by (auto simp add: not_le cong: conj_cong)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    43
      (metis dense le_less_linear less_linear less_trans order_refl)
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    44
  then obtain i j where ij:
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    45
    "a < b \<Longrightarrow> i a b c < j a b c"
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 63040
diff changeset
    46
      "a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 63040
diff changeset
    47
      "a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 63040
diff changeset
    48
    for a b c :: real
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    49
    by metis
23461
wenzelm
parents: 23389
diff changeset
    50
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62083
diff changeset
    51
  define ivl where "ivl =
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62083
diff changeset
    52
    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)))"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62083
diff changeset
    53
  define I where "I n = {fst (ivl n) .. snd (ivl n)}" for n
23461
wenzelm
parents: 23389
diff changeset
    54
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    55
  have ivl [simp]:
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    56
    "ivl 0 = (f 0 + 1, f 0 + 2)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    57
    "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    58
    unfolding ivl_def by simp_all
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    59
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    60
  txt \<open>This is a decreasing sequence of non-empty intervals.\<close>
23461
wenzelm
parents: 23389
diff changeset
    61
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    62
  have less: "fst (ivl n) < snd (ivl n)" for n
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    63
    by (induct n) (auto intro!: ij)
23461
wenzelm
parents: 23389
diff changeset
    64
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    65
  have "decseq I"
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    66
    unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    67
    by (intro ij allI less)
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    68
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    69
  txt \<open>Now we apply the finite intersection property of compact sets.\<close>
23461
wenzelm
parents: 23389
diff changeset
    70
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    71
  have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    72
  proof (rule compact_imp_fip_image)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    73
    fix S :: "nat set"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    74
    assume fin: "finite S"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    75
    have "{} \<subset> I (Max (insert 0 S))"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    76
      unfolding I_def using less[of "Max (insert 0 S)"] by auto
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    77
    also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    78
      using fin decseqD[OF \<open>decseq I\<close>, of _ "Max (insert 0 S)"]
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    79
      by (auto simp: Max_ge_iff)
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    80
    also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
56796
9f84219715a7 tuned proofs;
wenzelm
parents: 54797
diff changeset
    81
      by auto
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    82
    finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
53372
f5a6313c7fe4 tuned proof;
wenzelm
parents: 40702
diff changeset
    83
      by auto
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    84
  qed (auto simp: I_def)
63060
293ede07b775 some uses of 'obtain' with structure statement;
wenzelm
parents: 63040
diff changeset
    85
  then obtain x where "x \<in> I n" for n
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    86
    by blast
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
    87
  moreover from \<open>surj f\<close> obtain j where "x = f j"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    88
    by blast
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    89
  ultimately have "f j \<in> I (Suc j)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    90
    by blast
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    91
  with ij(3)[OF less] show False
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    92
    unfolding I_def ivl fst_conv snd_conv by auto
23461
wenzelm
parents: 23389
diff changeset
    93
qed
wenzelm
parents: 23389
diff changeset
    94
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
    95
lemma uncountable_UNIV_real: "uncountable (UNIV :: real set)"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    96
  using real_non_denum unfolding uncountable_def by auto
23461
wenzelm
parents: 23389
diff changeset
    97
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    98
lemma bij_betw_open_intervals:
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
    99
  fixes a b c d :: real
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   100
  assumes "a < b" "c < d"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   101
  shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   102
proof -
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62083
diff changeset
   103
  define f where "f a b c d x = (d - c)/(b - a) * (x - a) + c" for a b c d x :: real
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   104
  {
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   105
    fix a b c d x :: real
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   106
    assume *: "a < b" "c < d" "a < x" "x < b"
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   107
    moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   108
      by (intro mult_strict_left_mono) simp_all
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   109
    moreover from * have "0 < (d - c) * (x - a) / (b - a)"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   110
      by simp
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   111
    ultimately have "f a b c d x < d" "c < f a b c d x"
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   112
      by (simp_all add: f_def field_simps)
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   113
  }
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   114
  with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   115
    by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   116
  then show ?thesis by auto
23461
wenzelm
parents: 23389
diff changeset
   117
qed
wenzelm
parents: 23389
diff changeset
   118
57234
596a499318ab clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents: 56796
diff changeset
   119
lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
59872
db4000b71fdb Theorem "arctan" is no longer a default simprule
paulson <lp15@cam.ac.uk>
parents: 59720
diff changeset
   120
  using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan)
23461
wenzelm
parents: 23389
diff changeset
   121
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   122
lemma uncountable_open_interval: "uncountable {a<..<b} \<longleftrightarrow> a < b" for a b :: real
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   123
proof
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   124
  show "a < b" if "uncountable {a<..<b}"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   125
    using uncountable_def that by force
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   126
  show "uncountable {a<..<b}" if "a < b"
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   127
  proof -
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   128
    obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 60308
diff changeset
   129
      using bij_betw_open_intervals[OF \<open>a < b\<close>, of "-pi/2" "pi/2"] by auto
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   130
    then show ?thesis
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   131
      by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   132
  qed
23461
wenzelm
parents: 23389
diff changeset
   133
qed
wenzelm
parents: 23389
diff changeset
   134
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   135
lemma uncountable_half_open_interval_1: "uncountable {a..<b} \<longleftrightarrow> a < b" for a b :: real
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   136
  apply auto
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   137
  using atLeastLessThan_empty_iff
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   138
  apply fastforce
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   139
  using uncountable_open_interval [of a b]
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   140
  apply (metis countable_Un_iff ivl_disj_un_singleton(3))
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   141
  done
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   142
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   143
lemma uncountable_half_open_interval_2: "uncountable {a<..b} \<longleftrightarrow> a < b" for a b :: real
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   144
  apply auto
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   145
  using atLeastLessThan_empty_iff
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   146
  apply fastforce
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   147
  using uncountable_open_interval [of a b]
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   148
  apply (metis countable_Un_iff ivl_disj_un_singleton(4))
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   149
  done
60308
f7e406aba90d uncountability: open interval equivalences
paulson <lp15@cam.ac.uk>
parents: 59872
diff changeset
   150
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   151
lemma real_interval_avoid_countable_set:
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   152
  fixes a b :: real and A :: "real set"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   153
  assumes "a < b" and "countable A"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   154
  shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   155
proof -
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   156
  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   157
    by auto
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   158
  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   159
    by (simp add: uncountable_open_interval)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   160
  ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   161
    by auto
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   162
  then have "A \<inter> {a<..<b} \<subset> {a<..<b}"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   163
    by (intro psubsetI) auto
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   164
  then have "\<exists>x. x \<in> {a<..<b} - A \<inter> {a<..<b}"
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   165
    by (rule psubset_imp_ex_mem)
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   166
  then show ?thesis
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   167
    by auto
61880
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   168
qed
ff4d33058566 moved some theorems from the CLT proof; reordered some theorems / notation
hoelzl
parents: 61585
diff changeset
   169
62083
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   170
lemma open_minus_countable:
63465
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   171
  fixes S A :: "real set"
d7610beb98bc misc tuning and modernization;
wenzelm
parents: 63464
diff changeset
   172
  assumes "countable A" "S \<noteq> {}" "open S"
62083
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   173
  shows "\<exists>x\<in>S. x \<notin> A"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   174
proof -
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   175
  obtain x where "x \<in> S"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   176
    using \<open>S \<noteq> {}\<close> by auto
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   177
  then obtain e where "0 < e" "{y. dist y x < e} \<subseteq> S"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   178
    using \<open>open S\<close> by (auto simp: open_dist subset_eq)
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   179
  moreover have "{y. dist y x < e} = {x - e <..< x + e}"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   180
    by (auto simp: dist_real_def)
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   181
  ultimately have "uncountable (S - A)"
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   182
    using uncountable_open_interval[of "x - e" "x + e"] \<open>countable A\<close>
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   183
    by (intro uncountable_minus_countable) (auto dest: countable_subset)
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   184
  then show ?thesis
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   185
    unfolding uncountable_def by auto
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   186
qed
7582b39f51ed add the proof of the central limit theorem
hoelzl
parents: 61975
diff changeset
   187
23461
wenzelm
parents: 23389
diff changeset
   188
end