--- a/src/HOL/Library/ContNotDenum.thy Tue Apr 29 21:54:26 2014 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Tue Apr 29 22:50:55 2014 +0200
@@ -1,5 +1,5 @@
-(* Title : HOL/ContNonDenum
- Author : Benjamin Porter, Monash University, NICTA, 2005
+(* Title: HOL/Library/ContNonDenum.thy
+ Author: Benjamin Porter, Monash University, NICTA, 2005
*)
header {* Non-denumerability of the Continuum. *}
@@ -15,7 +15,7 @@
system.
{\em Theorem:} The Continuum @{text "\<real>"} is not denumerable. In other
-words, there does not exist a function f:@{text "\<nat>\<Rightarrow>\<real>"} such that f is
+words, there does not exist a function @{text "f: \<nat> \<Rightarrow> \<real>"} such that f is
surjective.
{\em Outline:} An elegant informal proof of this result uses Cantor's
@@ -25,41 +25,50 @@
completeness of the Real numbers and is the foundation for our
argument. Informally it states that an intersection of countable
closed intervals (where each successive interval is a subset of the
-last) is non-empty. We then assume a surjective function f:@{text
-"\<nat>\<Rightarrow>\<real>"} exists and find a real x such that x is not in the range of f
+last) is non-empty. We then assume a surjective function @{text
+"f: \<nat> \<Rightarrow> \<real>"} exists and find a real x such that x is not in the range of f
by generating a sequence of closed intervals then using the NIP. *}
+
subsection {* Closed Intervals *}
subsection {* Nested Interval Property *}
theorem NIP:
- fixes f::"nat \<Rightarrow> real set"
+ fixes f :: "nat \<Rightarrow> real set"
assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
- and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
+ and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
shows "(\<Inter>n. f n) \<noteq> {}"
proof -
let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
- { fix n
+ {
+ fix n
from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
by auto
then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
- by auto }
+ by auto
+ }
note f_eq = this
- { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
- by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
+ {
+ fix n m :: nat
+ assume "n \<le> m"
+ then have "f m \<subseteq> f n"
+ by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
+ }
note subset' = this
have "compact (f 0)"
by (subst f_eq) (rule compact_Icc)
then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
proof (rule compact_imp_fip_image)
- fix I :: "nat set" assume I: "finite I"
+ fix I :: "nat set"
+ assume I: "finite I"
have "{} \<subset> f (Max (insert 0 I))"
using f_eq[of "Max (insert 0 I)"] by auto
also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
proof (rule INF_greatest)
- fix i assume "i \<in> insert 0 I"
+ fix i
+ assume "i \<in> insert 0 I"
with I show "f (Max (insert 0 I)) \<subseteq> f i"
by (intro subset') auto
qed
@@ -70,6 +79,7 @@
by auto
qed
+
subsection {* Generating the intervals *}
subsubsection {* Existence of non-singleton closed intervals *}
@@ -80,7 +90,7 @@
non-singleton itself. *}
lemma closed_subset_ex:
- fixes c::real
+ fixes c :: real
assumes "a < b"
shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
proof (cases "c < b")
@@ -90,39 +100,45 @@
case True
with `a < b` `c < b` have "c \<notin> {a..b}"
by auto
- with `a < b` show ?thesis by auto
+ with `a < b` show ?thesis
+ by auto
next
case False
then have "a \<le> c" by simp
def ka \<equiv> "(c + b)/2"
-
- from ka_def `c < b` have kalb: "ka < b" by auto
- moreover from ka_def `c < b` have kagc: "ka > c" by simp
- ultimately have "c\<notin>{ka..b}" by auto
- moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
- hence "{ka..b} \<subseteq> {a..b}" by auto
- ultimately have
- "ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
- using kalb by auto
+ from ka_def `c < b` have "ka < b"
+ by auto
+ moreover from ka_def `c < b` have "ka > c"
+ by simp
+ ultimately have "c \<notin> {ka..b}"
+ by auto
+ moreover from `a \<le> c` `ka > c` have "ka \<ge> a"
+ by simp
+ then have "{ka..b} \<subseteq> {a..b}"
+ by auto
+ ultimately have "ka < b \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
+ using `ka < b` by auto
then show ?thesis
by auto
qed
next
case False
then have "c \<ge> b" by simp
-
def kb \<equiv> "(a + b)/2"
with `a < b` have "kb < b" by auto
- with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
+ with kb_def `c \<ge> b` have "a < kb" "kb < c"
+ by auto
from `kb < c` have c: "c \<notin> {a..kb}"
by auto
with `kb < b` have "{a..kb} \<subseteq> {a..b}"
by auto
with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
by simp
- then show ?thesis by auto
+ then show ?thesis
+ by auto
qed
+
subsection {* newInt: Interval generation *}
text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
@@ -130,17 +146,19 @@
does not contain @{text "f (Suc n)"}. With the base case defined such
that @{text "(f 0)\<notin>newInt 0 f"}. *}
+
subsubsection {* Definition *}
-primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
+where
"newInt 0 f = {f 0 + 1..f 0 + 2}"
- | "newInt (Suc n) f =
- (SOME e. (\<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> e)
- )"
+| "newInt (Suc n) f =
+ (SOME e.
+ (\<exists>e1 e2.
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> e))"
subsubsection {* Properties *}
@@ -150,81 +168,76 @@
lemma newInt_ex:
"\<exists>a b. a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f"
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
proof (induct n)
case 0
-
let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> e"
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+ f (Suc 0) \<notin> e"
have "newInt (Suc 0) f = ?e" by auto
moreover
have "f 0 + 1 < f 0 + 2" by simp
- with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> {ka..kb}" .
- hence
- "\<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" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
+ with closed_subset_ex
+ have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> {ka..kb}" .
+ 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"
+ by simp
+ 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"
by (rule someI_ex)
ultimately have "\<exists>e1 e2. e1 < e2 \<and>
- newInt (Suc 0) f = {e1..e2} \<and>
- newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
- f (Suc 0) \<notin> newInt (Suc 0) f" by simp
- thus
- "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
- newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
+ newInt (Suc 0) f = {e1..e2} \<and>
+ newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
+ f (Suc 0) \<notin> newInt (Suc 0) f"
+ by simp
+ then show "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
+ newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
by simp
next
case (Suc n)
- hence "\<exists>a b.
- a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by simp
+ then have "\<exists>a b.
+ a < b \<and>
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+ by simp
then obtain a and b where ab: "a < b \<and>
- newInt (Suc n) f = {a..b} \<and>
- newInt (Suc n) f \<subseteq> newInt n f \<and>
- f (Suc n) \<notin> newInt (Suc n) f" by auto
- hence cab: "{a..b} = newInt (Suc n) f" by simp
+ newInt (Suc n) f = {a..b} \<and>
+ newInt (Suc n) f \<subseteq> newInt n f \<and>
+ f (Suc n) \<notin> newInt (Suc n) f"
+ by auto
+ then have cab: "{a..b} = newInt (Suc n) f"
+ by simp
let ?e = "SOME e. \<exists>e1 e2.
- e1 < e2 \<and>
- e = {e1..e2} \<and>
- e \<subseteq> {a..b} \<and>
- f (Suc (Suc n)) \<notin> e"
- from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
+ e1 < e2 \<and>
+ e = {e1..e2} \<and>
+ e \<subseteq> {a..b} \<and>
+ f (Suc (Suc n)) \<notin> e"
+ from cab have ni: "newInt (Suc (Suc n)) f = ?e"
+ by auto
from ab have "a < b" by simp
- with closed_subset_ex have
- "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
- f (Suc (Suc n)) \<notin> {ka..kb}" .
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
- {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+ with closed_subset_ex have "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
+ f (Suc (Suc n)) \<notin> {ka..kb}" .
+ then have "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
+ {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
+ by simp
+ 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"
by simp
- hence
- "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
- e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
- hence
- "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
- ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
- with ab ni show
- "\<exists>ka kb. ka < kb \<and>
- newInt (Suc (Suc n)) f = {ka..kb} \<and>
- newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
- f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
+ then have "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e"
+ by (rule someI_ex)
+ with ab ni show "\<exists>ka kb. ka < kb \<and>
+ newInt (Suc (Suc n)) f = {ka..kb} \<and>
+ newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
+ f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f"
+ by auto
qed
-lemma newInt_subset:
- "newInt (Suc n) f \<subseteq> newInt n f"
+lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
using newInt_ex by auto
@@ -232,34 +245,27 @@
of f is in the intersection of all closed intervals generated by
newInt. *}
-lemma newInt_inter:
- "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
proof
- fix n::nat
- {
- assume n0: "n = 0"
- moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
- ultimately have "f n \<notin> newInt n f" by simp
- }
- moreover
- {
- assume "\<not> n = 0"
- hence "n > 0" by simp
- then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
- from newInt_ex have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
- newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
- then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
- with ndef have "f n \<notin> newInt n f" by simp
- }
- ultimately have "f n \<notin> newInt n f" by (rule case_split)
- thus "f n \<notin> (\<Inter>n. newInt n f)" by auto
+ fix n :: nat
+ have "f n \<notin> newInt n f"
+ proof (cases n)
+ case 0
+ moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}"
+ by simp
+ ultimately show ?thesis by simp
+ next
+ case (Suc m)
+ from newInt_ex have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+ newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
+ then have "f (Suc m) \<notin> newInt (Suc m) f"
+ by auto
+ with Suc show ?thesis by simp
+ qed
+ then show "f n \<notin> (\<Inter>n. newInt n f)" by auto
qed
-
-lemma newInt_notempty:
- "(\<Inter>n. newInt n f) \<noteq> {}"
+lemma newInt_notempty: "(\<Inter>n. newInt n f) \<noteq> {}"
proof -
let ?g = "\<lambda>n. newInt n f"
have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
@@ -269,30 +275,26 @@
qed
moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
proof
- fix n::nat
- {
- assume "n = 0"
- then have
- "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
+ fix n :: nat
+ show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b"
+ proof (cases n)
+ case 0
+ then have "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
by simp
- hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
- }
- moreover
- {
- assume "\<not> n = 0"
- then have "n > 0" by simp
- then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
-
- have
- "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
+ then show ?thesis
+ by blast
+ next
+ case (Suc m)
+ have "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
(newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
by (rule newInt_ex)
- then obtain a and b where
- "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
- with nd have "?g n = {a..b} \<and> a \<le> b" by auto
- hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
- }
- ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
+ then obtain a and b where "a < b \<and> (newInt (Suc m) f) = {a..b}"
+ by auto
+ with Suc have "?g n = {a..b} \<and> a \<le> b"
+ by auto
+ then show ?thesis
+ by blast
+ qed
qed
ultimately show ?thesis by (rule NIP)
qed
@@ -300,17 +302,22 @@
subsection {* Final Theorem *}
-theorem real_non_denum:
- shows "\<not> (\<exists>f::nat\<Rightarrow>real. surj f)"
-proof -- "by contradiction"
- assume "\<exists>f::nat\<Rightarrow>real. surj f"
- then obtain f::"nat\<Rightarrow>real" where rangeF: "surj f" by auto
- -- "We now produce a real number x that is not in the range of f, using the properties of newInt. "
- have "\<exists>x. x \<in> (\<Inter>n. newInt n f)" using newInt_notempty by blast
- moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)" by (rule newInt_inter)
- ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x" by blast
- moreover from rangeF have "x \<in> range f" by simp
- ultimately show False by blast
+theorem real_non_denum: "\<not> (\<exists>f :: nat \<Rightarrow> real. surj f)"
+proof
+ assume "\<exists>f :: nat \<Rightarrow> real. surj f"
+ then obtain f :: "nat \<Rightarrow> real" where "surj f"
+ by auto
+ txt "We now produce a real number x that is not in the range of f, using the properties of newInt."
+ have "\<exists>x. x \<in> (\<Inter>n. newInt n f)"
+ using newInt_notempty by blast
+ moreover have "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
+ by (rule newInt_inter)
+ ultimately obtain x where "x \<in> (\<Inter>n. newInt n f)" and "\<forall>n. f n \<noteq> x"
+ by blast
+ moreover from `surj f` have "x \<in> range f"
+ by simp
+ ultimately show False
+ by blast
qed
end