author | paulson <lp15@cam.ac.uk> |
Wed, 01 Apr 2015 16:04:21 +0100 | |
changeset 59872 | db4000b71fdb |
parent 59720 | f893472fff31 |
child 60308 | f7e406aba90d |
permissions | -rw-r--r-- |
59720 | 1 |
(* Title: HOL/Library/ContNotDenum.thy |
56796 | 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 | 4 |
*) |
5 |
||
58881 | 6 |
section {* Non-denumerability of the Continuum. *} |
23461 | 7 |
|
8 |
theory ContNotDenum |
|
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 | 10 |
begin |
11 |
||
12 |
subsection {* Abstract *} |
|
13 |
||
14 |
text {* The following document presents a proof that the Continuum is |
|
15 |
uncountable. It is formalised in the Isabelle/Isar theorem proving |
|
16 |
system. |
|
17 |
||
18 |
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other |
|
56796 | 19 |
words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is |
23461 | 20 |
surjective. |
21 |
||
22 |
{\em Outline:} An elegant informal proof of this result uses Cantor's |
|
23 |
Diagonalisation argument. The proof presented here is not this |
|
24 |
one. First we formalise some properties of closed intervals, then we |
|
25 |
prove the Nested Interval Property. This property relies on the |
|
26 |
completeness of the Real numbers and is the foundation for our |
|
27 |
argument. Informally it states that an intersection of countable |
|
28 |
closed intervals (where each successive interval is a subset of the |
|
56796 | 29 |
last) is non-empty. We then assume a surjective function @{text |
30 |
"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f |
|
23461 | 31 |
by generating a sequence of closed intervals then using the NIP. *} |
32 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
33 |
theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
34 |
proof |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
35 |
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
|
36 |
then obtain f :: "nat \<Rightarrow> real" where "surj f" .. |
56796 | 37 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
38 |
txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *} |
23461 | 39 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
40 |
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})" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
41 |
using assms |
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) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
43 |
(metis dense le_less_linear less_linear less_trans order_refl) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
44 |
then obtain i j where ij: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
45 |
"\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
46 |
"\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
47 |
"\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
48 |
by metis |
23461 | 49 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
50 |
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)))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
51 |
def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}" |
23461 | 52 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
53 |
have ivl[simp]: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
54 |
"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
|
55 |
"\<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
|
56 |
unfolding ivl_def by simp_all |
56796 | 57 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
58 |
txt {* This is a decreasing sequence of non-empty intervals. *} |
23461 | 59 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
60 |
{ fix n have "fst (ivl n) < snd (ivl n)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
61 |
by (induct n) (auto intro!: ij) } |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
62 |
note less = this |
23461 | 63 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
64 |
have "decseq I" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
65 |
unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
66 |
|
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
67 |
txt {* Now we apply the finite intersection property of compact sets. *} |
23461 | 68 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
69 |
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
|
70 |
proof (rule compact_imp_fip_image) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
71 |
fix S :: "nat set" assume fin: "finite S" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
72 |
have "{} \<subset> I (Max (insert 0 S))" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
73 |
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
|
74 |
also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
75 |
using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
76 |
also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)" |
56796 | 77 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
78 |
finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}" |
53372 | 79 |
by auto |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
80 |
qed (auto simp: I_def) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
81 |
then obtain x where "\<And>n. x \<in> I n" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
82 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
83 |
moreover from `surj f` obtain j where "x = f j" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
84 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
85 |
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
|
86 |
by blast |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
87 |
with ij(3)[OF less] show False |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
88 |
unfolding I_def ivl fst_conv snd_conv by auto |
23461 | 89 |
qed |
90 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
91 |
lemma uncountable_UNIV_real: "uncountable (UNIV::real set)" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
92 |
using real_non_denum unfolding uncountable_def by auto |
23461 | 93 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
94 |
lemma bij_betw_open_intervals: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
95 |
fixes a b c d :: real |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
96 |
assumes "a < b" "c < d" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
97 |
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
|
98 |
proof - |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
99 |
def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
100 |
{ fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
101 |
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
|
102 |
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
|
103 |
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
|
104 |
by simp |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
105 |
ultimately have "f a b c d x < d" "c < f a b c d x" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
106 |
by (simp_all add: f_def field_simps) } |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
107 |
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
|
108 |
by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def) |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
109 |
thus ?thesis by auto |
23461 | 110 |
qed |
111 |
||
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
112 |
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
|
113 |
using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan arctan_tan) |
23461 | 114 |
|
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
115 |
lemma uncountable_open_interval: |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
116 |
fixes a b :: real assumes ab: "a < b" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
117 |
shows "uncountable {a<..<b}" |
23461 | 118 |
proof - |
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
119 |
obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}" |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
120 |
using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
121 |
then show ?thesis |
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
56796
diff
changeset
|
122 |
by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real) |
23461 | 123 |
qed |
124 |
||
125 |
end |
|
54797
be020ec8560c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
hoelzl
parents:
54263
diff
changeset
|
126 |