--- a/src/HOL/Library/ContNotDenum.thy Thu Jun 12 08:48:59 2014 +0200
+++ b/src/HOL/Library/ContNotDenum.thy Wed Jun 11 13:39:38 2014 +0200
@@ -1,11 +1,12 @@
(* Title: HOL/Library/ContNonDenum.thy
Author: Benjamin Porter, Monash University, NICTA, 2005
+ Author: Johannes Hölzl, TU München
*)
header {* Non-denumerability of the Continuum. *}
theory ContNotDenum
-imports Complex_Main
+imports Complex_Main Countable_Set
begin
subsection {* Abstract *}
@@ -29,295 +30,96 @@
"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. *}
+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" ..
-subsection {* Closed Intervals *}
-
-subsection {* Nested Interval Property *}
+ txt {* First we construct a sequence of nested intervals, ignoring @{term "range f"}. *}
-theorem NIP:
- 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"
- shows "(\<Inter>n. f n) \<noteq> {}"
-proof -
- let ?I = "\<lambda>n. {Inf (f n) .. Sup (f 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
- }
- 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)
- }
- note subset' = this
+ 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})"
+ using assms
+ by (auto simp add: not_le cong: conj_cong)
+ (metis dense le_less_linear less_linear less_trans order_refl)
+ then obtain i j where ij:
+ "\<And>a b c::real. a < b \<Longrightarrow> i a b c < j a b c"
+ "\<And>a b c. a < b \<Longrightarrow> {i a b c .. j a b c} \<subseteq> {a .. b}"
+ "\<And>a b c. a < b \<Longrightarrow> c \<notin> {i a b c .. j a b c}"
+ by metis
- 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"
- 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"
- with I show "f (Max (insert 0 I)) \<subseteq> f i"
- by (intro subset') auto
- qed
- finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
- by auto
- qed (subst f_eq, auto)
- then show "(\<Inter>n. f n) \<noteq> {}"
- by auto
-qed
+ 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)))"
+ def I \<equiv> "\<lambda>n. {fst (ivl n) .. snd (ivl n)}"
+ have ivl[simp]:
+ "ivl 0 = (f 0 + 1, f 0 + 2)"
+ "\<And>n. ivl (Suc n) = (i (fst (ivl n)) (snd (ivl n)) (f n), j (fst (ivl n)) (snd (ivl n)) (f n))"
+ unfolding ivl_def by simp_all
-subsection {* Generating the intervals *}
+ txt {* This is a decreasing sequence of non-empty intervals. *}
-subsubsection {* Existence of non-singleton closed intervals *}
+ { fix n have "fst (ivl n) < snd (ivl n)"
+ by (induct n) (auto intro!: ij) }
+ note less = this
-text {* This lemma asserts that given any non-singleton closed
-interval (a,b) and any element c, there exists a closed interval that
-is a subset of (a,b) and that does not contain c and is a
-non-singleton itself. *}
+ have "decseq I"
+ unfolding I_def decseq_Suc_iff ivl fst_conv snd_conv by (intro ij allI less)
+
+ txt {* Now we apply the finite intersection property of compact sets. *}
-lemma closed_subset_ex:
- 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")
- case True
- show ?thesis
- proof (cases "c < a")
- case True
- with `a < b` `c < b` have "c \<notin> {a..b}"
- 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 "ka < b"
+ have "I 0 \<inter> (\<Inter>i. I i) \<noteq> {}"
+ proof (rule compact_imp_fip_image)
+ fix S :: "nat set" assume fin: "finite S"
+ have "{} \<subset> I (Max (insert 0 S))"
+ unfolding I_def using less[of "Max (insert 0 S)"] by auto
+ also have "I (Max (insert 0 S)) \<subseteq> (\<Inter>i\<in>insert 0 S. I i)"
+ using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
+ also have "(\<Inter>i\<in>insert 0 S. I i) = I 0 \<inter> (\<Inter>i\<in>S. I i)"
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
+ finally show "I 0 \<inter> (\<Inter>i\<in>S. I i) \<noteq> {}"
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
- 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
+ qed (auto simp: I_def)
+ then obtain x where "\<And>n. x \<in> I n"
+ by blast
+ moreover from `surj f` obtain j where "x = f j"
+ by blast
+ ultimately have "f j \<in> I (Suc j)"
+ by blast
+ with ij(3)[OF less] show False
+ unfolding I_def ivl fst_conv snd_conv by auto
qed
-
-subsection {* newInt: Interval generation *}
-
-text {* Given a function f:@{text "\<nat>\<Rightarrow>\<real>"}, newInt (Suc n) f returns a
-closed interval such that @{text "newInt (Suc n) f \<subseteq> newInt n f"} and
-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
- "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))"
-
-
-subsubsection {* Properties *}
-
-text {* We now show that every application of newInt returns an
-appropriate interval. *}
-
-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"
-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"
+lemma uncountable_UNIV_real: "uncountable (UNIV::real set)"
+ using real_non_denum unfolding uncountable_def by auto
- 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}" .
- 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
- 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)
- 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
- 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
-
- 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}" .
- 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
- 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
+lemma bij_betw_open_intervals:
+ fixes a b c d :: real
+ assumes "a < b" "c < d"
+ shows "\<exists>f. bij_betw f {a<..<b} {c<..<d}"
+proof -
+ def f \<equiv> "\<lambda>a b c d x::real. (d - c)/(b - a) * (x - a) + c"
+ { fix a b c d x :: real assume *: "a < b" "c < d" "a < x" "x < b"
+ moreover from * have "(d - c) * (x - a) < (d - c) * (b - a)"
+ by (intro mult_strict_left_mono) simp_all
+ moreover from * have "0 < (d - c) * (x - a) / (b - a)"
+ by simp
+ ultimately have "f a b c d x < d" "c < f a b c d x"
+ by (simp_all add: f_def field_simps) }
+ with assms have "bij_betw (f a b c d) {a<..<b} {c<..<d}"
+ by (intro bij_betw_byWitness[where f'="f c d a b"]) (auto simp: f_def)
+ thus ?thesis by auto
qed
-lemma newInt_subset: "newInt (Suc n) f \<subseteq> newInt n f"
- using newInt_ex by auto
-
-
-text {* Another fundamental property is that no element in the range
-of f is in the intersection of all closed intervals generated by
-newInt. *}
+lemma bij_betw_tan: "bij_betw tan {-pi/2<..<pi/2} UNIV"
+ using arctan_ubound by (intro bij_betw_byWitness[where f'=arctan]) (auto simp: arctan_tan)
-lemma newInt_inter: "\<forall>n. f n \<notin> (\<Inter>n. newInt n f)"
-proof
- 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 uncountable_open_interval:
+ fixes a b :: real assumes ab: "a < b"
+ shows "uncountable {a<..<b}"
proof -
- let ?g = "\<lambda>n. newInt n f"
- have "\<forall>n. ?g (Suc n) \<subseteq> ?g n"
- proof
- fix n
- show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
- qed
- moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
- proof
- 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
- 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 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
-
-
-subsection {* Final Theorem *}
-
-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
+ obtain f where "bij_betw f {a <..< b} {-pi/2<..<pi/2}"
+ using bij_betw_open_intervals[OF `a < b`, of "-pi/2" "pi/2"] by auto
+ then show ?thesis
+ by (metis bij_betw_tan uncountable_bij_betw uncountable_UNIV_real)
qed
end
--- a/src/HOL/Library/Countable_Set.thy Thu Jun 12 08:48:59 2014 +0200
+++ b/src/HOL/Library/Countable_Set.thy Wed Jun 11 13:39:38 2014 +0200
@@ -296,4 +296,23 @@
qed
qed
+subsection {* Uncountable *}
+
+abbreviation uncountable where
+ "uncountable A \<equiv> \<not> countable A"
+
+lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
+ by (auto intro: inj_on_inv_into simp: countable_def)
+ (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
+
+lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
+ unfolding bij_betw_def by (metis countable_image)
+
+lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
+ by (metis countable_finite)
+
+lemma uncountable_minus_countable:
+ "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
+ using countable_Un[of B "A - B"] assms by auto
+
end