# HG changeset patch
# User hoelzl
# Date 1402486778 7200
# Node ID 596a499318ab81afc1ca79da4f8cd97d2e533029
# Parent 8fcbfce2a2a9cffb95ca0c50fc53383d8b57dc4c
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
diff r 8fcbfce2a2a9 r 596a499318ab src/HOL/Library/ContNotDenum.thy
 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 {* Nondenumerability of the Continuum. *}
theory ContNotDenum
imports Complex_Main
+imports Complex_Main Countable_Set
begin
subsection {* Abstract *}
@@ 29,295 +30,96 @@
"f: \ \ \"} 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: "\ (\f :: nat \ real. surj f)"
+proof
+ assume "\f::nat \ real. surj f"
+ then obtain f :: "nat \ 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 \ real set"
 assumes subset: "\n. f (Suc n) \ f n"
 and closed: "\n. \a b. f n = {a..b} \ a \ b"
 shows "(\n. f n) \ {}"
proof 
 let ?I = "\n. {Inf (f n) .. Sup (f n)}"
 {
 fix n
 from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \ b"
 by auto
 then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \ Sup (f n)"
 by auto
 }
 note f_eq = this
 {
 fix n m :: nat
 assume "n \ m"
 then have "f m \ f n"
 by (induct rule: dec_induct) (metis order_refl, metis order_trans subset)
 }
 note subset' = this
+ have "\a b c::real. a < b \ (\ka kb. ka < kb \ {ka..kb} \ {a..b} \ c \ {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:
+ "\a b c::real. a < b \ i a b c < j a b c"
+ "\a b c. a < b \ {i a b c .. j a b c} \ {a .. b}"
+ "\a b c. a < b \ c \ {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 \ (\i. f i) \ {}"
 proof (rule compact_imp_fip_image)
 fix I :: "nat set"
 assume I: "finite I"
 have "{} \ f (Max (insert 0 I))"
 using f_eq[of "Max (insert 0 I)"] by auto
 also have "\ \ (\i\insert 0 I. f i)"
 proof (rule INF_greatest)
 fix i
 assume "i \ insert 0 I"
 with I show "f (Max (insert 0 I)) \ f i"
 by (intro subset') auto
 qed
 finally show "f 0 \ (\i\I. f i) \ {}"
 by auto
 qed (subst f_eq, auto)
 then show "(\n. f n) \ {}"
 by auto
qed
+ def ivl \ "rec_nat (f 0 + 1, f 0 + 2) (\n x. (i (fst x) (snd x) (f n), j (fst x) (snd x) (f n)))"
+ def I \ "\n. {fst (ivl n) .. snd (ivl n)}"
+ have ivl[simp]:
+ "ivl 0 = (f 0 + 1, f 0 + 2)"
+ "\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 nonempty intervals. *}
subsubsection {* Existence of nonsingleton 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 nonsingleton 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
nonsingleton 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 "\ka kb. ka < kb \ {ka..kb} \ {a..b} \ c \ {ka..kb}"
proof (cases "c < b")
 case True
 show ?thesis
 proof (cases "c < a")
 case True
 with `a < b` `c < b` have "c \ {a..b}"
 by auto
 with `a < b` show ?thesis
 by auto
 next
 case False
 then have "a \ c" by simp
 def ka \ "(c + b)/2"
 from ka_def `c < b` have "ka < b"
+ have "I 0 \ (\i. I i) \ {}"
+ proof (rule compact_imp_fip_image)
+ fix S :: "nat set" assume fin: "finite S"
+ have "{} \ I (Max (insert 0 S))"
+ unfolding I_def using less[of "Max (insert 0 S)"] by auto
+ also have "I (Max (insert 0 S)) \ (\i\insert 0 S. I i)"
+ using fin decseqD[OF `decseq I`, of _ "Max (insert 0 S)"] by (auto simp: Max_ge_iff)
+ also have "(\i\insert 0 S. I i) = I 0 \ (\i\S. I i)"
by auto
 moreover from ka_def `c < b` have "ka > c"
 by simp
 ultimately have "c \ {ka..b}"
 by auto
 moreover from `a \ c` `ka > c` have "ka \ a"
 by simp
 then have "{ka..b} \ {a..b}"
 by auto
 ultimately have "ka < b \ {ka..b} \ {a..b} \ c \ {ka..b}"
 using `ka < b` by auto
 then show ?thesis
+ finally show "I 0 \ (\i\S. I i) \ {}"
by auto
 qed
next
 case False
 then have "c \ b" by simp
 def kb \ "(a + b)/2"
 with `a < b` have "kb < b" by auto
 with kb_def `c \ b` have "a < kb" "kb < c"
 by auto
 from `kb < c` have c: "c \ {a..kb}"
 by auto
 with `kb < b` have "{a..kb} \ {a..b}"
 by auto
 with `a < kb` c have "a < kb \ {a..kb} \ {a..b} \ c \ {a..kb}"
 by simp
 then show ?thesis
 by auto
+ qed (auto simp: I_def)
+ then obtain x where "\n. x \ I n"
+ by blast
+ moreover from `surj f` obtain j where "x = f j"
+ by blast
+ ultimately have "f j \ 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 "\\\"}, newInt (Suc n) f returns a
closed interval such that @{text "newInt (Suc n) f \ newInt n f"} and
does not contain @{text "f (Suc n)"}. With the base case defined such
that @{text "(f 0)\newInt 0 f"}. *}


subsubsection {* Definition *}

primrec newInt :: "nat \ (nat \ real) \ (real set)"
where
 "newInt 0 f = {f 0 + 1..f 0 + 2}"
 "newInt (Suc n) f =
 (SOME e.
 (\e1 e2.
 e1 < e2 \
 e = {e1..e2} \
 e \ newInt n f \
 f (Suc n) \ e))"


subsubsection {* Properties *}

text {* We now show that every application of newInt returns an
appropriate interval. *}

lemma newInt_ex:
 "\a b. a < b \
 newInt (Suc n) f = {a..b} \
 newInt (Suc n) f \ newInt n f \
 f (Suc n) \ newInt (Suc n) f"
proof (induct n)
 case 0
 let ?e = "SOME e. \e1 e2.
 e1 < e2 \
 e = {e1..e2} \
 e \ {f 0 + 1..f 0 + 2} \
 f (Suc 0) \ 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 "\ka kb. ka < kb \ {ka..kb} \ {f 0 + 1..f 0 + 2} \ f (Suc 0) \ {ka..kb}" .
 then have "\e. \ka kb. ka < kb \ e = {ka..kb} \ e \ {f 0 + 1..f 0 + 2} \ f (Suc 0) \ e"
 by simp
 then have "\ka kb. ka < kb \ ?e = {ka..kb} \ ?e \ {f 0 + 1..f 0 + 2} \ f (Suc 0) \ ?e"
 by (rule someI_ex)
 ultimately have "\e1 e2. e1 < e2 \
 newInt (Suc 0) f = {e1..e2} \
 newInt (Suc 0) f \ {f 0 + 1..f 0 + 2} \
 f (Suc 0) \ newInt (Suc 0) f"
 by simp
 then show "\a b. a < b \ newInt (Suc 0) f = {a..b} \
 newInt (Suc 0) f \ newInt 0 f \ f (Suc 0) \ newInt (Suc 0) f"
 by simp
next
 case (Suc n)
 then have "\a b.
 a < b \
 newInt (Suc n) f = {a..b} \
 newInt (Suc n) f \ newInt n f \
 f (Suc n) \ newInt (Suc n) f"
 by simp
 then obtain a and b where ab: "a < b \
 newInt (Suc n) f = {a..b} \
 newInt (Suc n) f \ newInt n f \
 f (Suc n) \ newInt (Suc n) f"
 by auto
 then have cab: "{a..b} = newInt (Suc n) f"
 by simp

 let ?e = "SOME e. \e1 e2.
 e1 < e2 \
 e = {e1..e2} \
 e \ {a..b} \
 f (Suc (Suc n)) \ 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 "\ka kb. ka < kb \ {ka..kb} \ {a..b} \
 f (Suc (Suc n)) \ {ka..kb}" .
 then have "\e. \ka kb. ka < kb \ e = {ka..kb} \
 {ka..kb} \ {a..b} \ f (Suc (Suc n)) \ {ka..kb}"
 by simp
 then have "\e. \ka kb. ka < kb \ e = {ka..kb} \ e \ {a..b} \ f (Suc (Suc n)) \ e"
 by simp
 then have "\ka kb. ka < kb \ ?e = {ka..kb} \ ?e \ {a..b} \ f (Suc (Suc n)) \ ?e"
 by (rule someI_ex)
 with ab ni show "\ka kb. ka < kb \
 newInt (Suc (Suc n)) f = {ka..kb} \
 newInt (Suc (Suc n)) f \ newInt (Suc n) f \
 f (Suc (Suc n)) \ newInt (Suc (Suc n)) f"
 by auto
+lemma bij_betw_open_intervals:
+ fixes a b c d :: real
+ assumes "a < b" "c < d"
+ shows "\f. bij_betw f {a<.. "\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<.. 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<..n. f n \ (\n. newInt n f)"
proof
 fix n :: nat
 have "f n \ 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 "\a b. a < b \ (newInt (Suc m) f) = {a..b} \
 newInt (Suc m) f \ newInt m f \ f (Suc m) \ newInt (Suc m) f" .
 then have "f (Suc m) \ newInt (Suc m) f"
 by auto
 with Suc show ?thesis by simp
 qed
 then show "f n \ (\n. newInt n f)" by auto
qed

lemma newInt_notempty: "(\n. newInt n f) \ {}"
+lemma uncountable_open_interval:
+ fixes a b :: real assumes ab: "a < b"
+ shows "uncountable {a<..n. newInt n f" have "\n. ?g (Suc n) \ ?g n"
 proof
 fix n
 show "?g (Suc n) \ ?g n" by (rule newInt_subset)
 qed
 moreover have "\n. \a b. ?g n = {a..b} \ a \ b"
 proof
 fix n :: nat
 show "\a b. ?g n = {a..b} \ a \ b"
 proof (cases n)
 case 0
 then have "?g n = {f 0 + 1..f 0 + 2} \ (f 0 + 1 \ f 0 + 2)"
 by simp
 then show ?thesis
 by blast
 next
 case (Suc m)
 have "\a b. a < b \ (newInt (Suc m) f) = {a..b} \
 (newInt (Suc m) f) \ (newInt m f) \ (f (Suc m)) \ (newInt (Suc m) f)"
 by (rule newInt_ex)
 then obtain a and b where "a < b \ (newInt (Suc m) f) = {a..b}"
 by auto
 with Suc have "?g n = {a..b} \ a \ b"
 by auto
 then show ?thesis
 by blast
 qed
 qed
 ultimately show ?thesis by (rule NIP)
qed


subsection {* Final Theorem *}

theorem real_non_denum: "\ (\f :: nat \ real. surj f)"
proof
 assume "\f :: nat \ real. surj f"
 then obtain f :: "nat \ 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 "\x. x \