# 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 {* 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
diff -r 8fcbfce2a2a9 -r 596a499318ab src/HOL/Library/Countable_Set.thy
--- 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