modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
authorhoelzl
Wed Dec 18 11:53:40 2013 +0100 (2013-12-18)
changeset 54797be020ec8560c
parent 54796 cdc6d8cbf770
child 54798 287e569eebb2
child 54806 a0f024caa04c
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property
src/HOL/Library/ContNotDenum.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Dec 17 22:34:26 2013 +0100
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 18 11:53:40 2013 +0100
     1.3 @@ -31,270 +31,43 @@
     1.4  
     1.5  subsection {* Closed Intervals *}
     1.6  
     1.7 -text {* This section formalises some properties of closed intervals. *}
     1.8 -
     1.9 -subsubsection {* Definition *}
    1.10 -
    1.11 -definition
    1.12 -  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
    1.13 -  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
    1.14 -
    1.15 -subsubsection {* Properties *}
    1.16 -
    1.17 -lemma closed_int_subset:
    1.18 -  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
    1.19 -  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
    1.20 -proof -
    1.21 -  {
    1.22 -    fix x::real
    1.23 -    assume "x \<in> closed_int x1 y1"
    1.24 -    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
    1.25 -    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
    1.26 -    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
    1.27 -  }
    1.28 -  thus ?thesis by auto
    1.29 -qed
    1.30 -
    1.31 -lemma closed_int_least:
    1.32 -  assumes a: "a \<le> b"
    1.33 -  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
    1.34 -proof
    1.35 -  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    1.36 -  thus "a \<in> closed_int a b" by (unfold closed_int_def)
    1.37 -next
    1.38 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
    1.39 -  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
    1.40 -qed
    1.41 -
    1.42 -lemma closed_int_most:
    1.43 -  assumes a: "a \<le> b"
    1.44 -  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
    1.45 -proof
    1.46 -  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
    1.47 -  thus "b \<in> closed_int a b" by (unfold closed_int_def)
    1.48 -next
    1.49 -  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
    1.50 -  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
    1.51 -qed
    1.52 -
    1.53 -lemma closed_not_empty:
    1.54 -  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
    1.55 -  by (auto dest: closed_int_least)
    1.56 -
    1.57 -lemma closed_mem:
    1.58 -  assumes "a \<le> c" and "c \<le> b"
    1.59 -  shows "c \<in> closed_int a b"
    1.60 -  using assms unfolding closed_int_def by auto
    1.61 -
    1.62 -lemma closed_subset:
    1.63 -  assumes ac: "a \<le> b"  "c \<le> d" 
    1.64 -  assumes closed: "closed_int a b \<subseteq> closed_int c d"
    1.65 -  shows "b \<ge> c"
    1.66 -proof -
    1.67 -  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
    1.68 -  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
    1.69 -  with ac have "c\<le>b \<and> b\<le>d" by simp
    1.70 -  thus ?thesis by auto
    1.71 -qed
    1.72 -
    1.73 -
    1.74  subsection {* Nested Interval Property *}
    1.75  
    1.76  theorem NIP:
    1.77    fixes f::"nat \<Rightarrow> real set"
    1.78    assumes subset: "\<forall>n. f (Suc n) \<subseteq> f n"
    1.79 -  and closed: "\<forall>n. \<exists>a b. f n = closed_int a b \<and> a \<le> b"
    1.80 +  and closed: "\<forall>n. \<exists>a b. f n = {a..b} \<and> a \<le> b"
    1.81    shows "(\<Inter>n. f n) \<noteq> {}"
    1.82  proof -
    1.83 -  let ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
    1.84 -  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
    1.85 -  proof
    1.86 -    fix n
    1.87 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
    1.88 -    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
    1.89 -    hence "a \<le> b" ..
    1.90 -    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
    1.91 -    with fn show "\<exists>x. x\<in>(f n)" by simp
    1.92 -  qed
    1.93 -
    1.94 -  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
    1.95 -  proof
    1.96 -    fix n
    1.97 -    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
    1.98 -    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
    1.99 -    hence "a \<le> b" by simp
   1.100 -    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
   1.101 -    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
   1.102 -    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
   1.103 -    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
   1.104 -  qed
   1.105 -
   1.106 -  -- "A denotes the set of all left-most points of all the intervals ..."
   1.107 -  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
   1.108 -  ultimately have "A \<noteq> {}"
   1.109 -  proof -
   1.110 -    have "(0::nat) \<in> \<nat>" by simp
   1.111 -    with Adef show ?thesis
   1.112 -      by blast
   1.113 -  qed
   1.114 -
   1.115 -  -- "Now show that A is bounded above ..."
   1.116 -  moreover have "bdd_above A"
   1.117 -  proof -
   1.118 -    {
   1.119 -      fix n
   1.120 -      from ne have ex: "\<exists>x. x\<in>(f n)" ..
   1.121 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   1.122 -      moreover
   1.123 -      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
   1.124 -      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
   1.125 -      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
   1.126 -      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
   1.127 -      with ex have "(?g n) \<le> b" by auto
   1.128 -      hence "\<exists>b. (?g n) \<le> b" by auto
   1.129 -    }
   1.130 -    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
   1.131 -
   1.132 -    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
   1.133 -    proof (rule allI, induct_tac n)
   1.134 -      show "f 0 \<subseteq> f 0" by simp
   1.135 -    next
   1.136 -      fix n
   1.137 -      assume "f n \<subseteq> f 0"
   1.138 -      moreover from subset have "f (Suc n) \<subseteq> f n" ..
   1.139 -      ultimately show "f (Suc n) \<subseteq> f 0" by simp
   1.140 -    qed
   1.141 -    have "\<forall>n. (?g n)\<in>(f 0)"
   1.142 -    proof
   1.143 -      fix n
   1.144 -      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
   1.145 -      hence "?g n \<in> f n" ..
   1.146 -      with fs show "?g n \<in> f 0" by auto
   1.147 -    qed
   1.148 -    moreover from closed
   1.149 -      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
   1.150 -    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
   1.151 -    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
   1.152 -    with Adef show "bdd_above A" by auto
   1.153 -  qed
   1.154 -
   1.155 -  -- "denote this least upper bound as t ..."
   1.156 -  def tdef: t == "Sup A"
   1.157 -
   1.158 -  -- "and finally show that this least upper bound is in all the intervals..."
   1.159 -  have "\<forall>n. t \<in> f n"
   1.160 -  proof
   1.161 -    fix n::nat
   1.162 -    from closed obtain a and b where
   1.163 -      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
   1.164 +  let ?I = "\<lambda>n. {Inf (f n) .. Sup (f n)}"
   1.165 +  { fix n 
   1.166 +    from closed[rule_format, of n] obtain a b where "f n = {a .. b}" "a \<le> b"
   1.167 +      by auto
   1.168 +    then have "f n = {Inf (f n) .. Sup (f n)}" and "Inf (f n) \<le> Sup (f n)"
   1.169 +      by auto }
   1.170 +  note f_eq = this
   1.171 +  { fix n m :: nat assume "n \<le> m" then have "f m \<subseteq> f n"
   1.172 +      by (induct rule: dec_induct) (metis order_refl, metis order_trans subset) }
   1.173 +  note subset' = this
   1.174  
   1.175 -    have "t \<ge> a"
   1.176 -    proof -
   1.177 -      have "a \<in> A"
   1.178 -      proof -
   1.179 -          (* by construction *)
   1.180 -        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
   1.181 -          using closed_int_least by blast
   1.182 -        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
   1.183 -        proof clarsimp
   1.184 -          fix e
   1.185 -          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
   1.186 -          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
   1.187 -  
   1.188 -          from ein aux have "a \<le> e \<and> e \<le> e" by auto
   1.189 -          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
   1.190 -          ultimately show "e = a" by simp
   1.191 -        qed
   1.192 -        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
   1.193 -        ultimately have "(?g n) = a" by (rule some_equality)
   1.194 -        moreover
   1.195 -        {
   1.196 -          have "n = of_nat n" by simp
   1.197 -          moreover have "of_nat n \<in> \<nat>" by simp
   1.198 -          ultimately have "n \<in> \<nat>"
   1.199 -            apply -
   1.200 -            apply (subst(asm) eq_sym_conv)
   1.201 -            apply (erule subst)
   1.202 -            .
   1.203 -        }
   1.204 -        with Adef have "(?g n) \<in> A" by auto
   1.205 -        ultimately show ?thesis by simp
   1.206 -      qed 
   1.207 -      with `bdd_above A` show "a \<le> t"
   1.208 -        unfolding tdef by (intro cSup_upper)
   1.209 +  have "compact (f 0)"
   1.210 +    by (subst f_eq) (rule compact_Icc)
   1.211 +  then have "f 0 \<inter> (\<Inter>i. f i) \<noteq> {}"
   1.212 +  proof (rule compact_imp_fip_image)
   1.213 +    fix I :: "nat set" assume I: "finite I"
   1.214 +    have "{} \<subset> f (Max (insert 0 I))"
   1.215 +      using f_eq[of "Max (insert 0 I)"] by auto
   1.216 +    also have "\<dots> \<subseteq> (\<Inter>i\<in>insert 0 I. f i)"
   1.217 +    proof (rule INF_greatest)
   1.218 +      fix i assume "i \<in> insert 0 I"
   1.219 +      with I show "f (Max (insert 0 I)) \<subseteq> f i"
   1.220 +        by (intro subset') auto
   1.221      qed
   1.222 -    moreover have "t \<le> b"
   1.223 -      unfolding tdef
   1.224 -    proof (rule cSup_least)
   1.225 -      {
   1.226 -        from alb int have
   1.227 -          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
   1.228 -        
   1.229 -        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
   1.230 -        proof (rule allI, induct_tac m)
   1.231 -          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
   1.232 -        next
   1.233 -          fix m n
   1.234 -          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   1.235 -          {
   1.236 -            fix p
   1.237 -            from pp have "f (p + n) \<subseteq> f p" by simp
   1.238 -            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   1.239 -            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   1.240 -            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   1.241 -          }
   1.242 -          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   1.243 -        qed 
   1.244 -        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   1.245 -        proof ((rule allI)+, rule impI)
   1.246 -          fix \<alpha>::nat and \<beta>::nat
   1.247 -          assume "\<beta> \<le> \<alpha>"
   1.248 -          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   1.249 -          then obtain k where "\<alpha> = \<beta> + k" ..
   1.250 -          moreover
   1.251 -          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   1.252 -          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   1.253 -        qed 
   1.254 -        
   1.255 -        fix m   
   1.256 -        {
   1.257 -          assume "m \<ge> n"
   1.258 -          with subsetm have "f m \<subseteq> f n" by simp
   1.259 -          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   1.260 -          moreover
   1.261 -          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   1.262 -          ultimately have "?g m \<le> b" by auto
   1.263 -        }
   1.264 -        moreover
   1.265 -        {
   1.266 -          assume "\<not>(m \<ge> n)"
   1.267 -          hence "m < n" by simp
   1.268 -          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   1.269 -          from closed obtain ma and mb where
   1.270 -            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   1.271 -          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   1.272 -          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   1.273 -          moreover have "(?g m) = ma"
   1.274 -          proof -
   1.275 -            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   1.276 -            moreover from one have
   1.277 -              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   1.278 -              by (rule closed_int_least)
   1.279 -            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   1.280 -            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   1.281 -            thus "?g m = ma" by auto
   1.282 -          qed
   1.283 -          ultimately have "?g m \<le> b" by simp
   1.284 -        } 
   1.285 -        ultimately have "?g m \<le> b" by (rule case_split)
   1.286 -      }
   1.287 -      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
   1.288 -    qed fact
   1.289 -    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   1.290 -    with int show "t \<in> f n" by simp
   1.291 -  qed
   1.292 -  hence "t \<in> (\<Inter>n. f n)" by auto
   1.293 -  thus ?thesis by auto
   1.294 +    finally show "f 0 \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
   1.295 +      by auto
   1.296 +  qed (subst f_eq, auto)
   1.297 +  then show "(\<Inter>n. f n) \<noteq> {}"
   1.298 +    by auto
   1.299  qed
   1.300  
   1.301  subsection {* Generating the intervals *}
   1.302 @@ -309,14 +82,14 @@
   1.303  lemma closed_subset_ex:
   1.304    fixes c::real
   1.305    assumes "a < b"
   1.306 -  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
   1.307 +  shows "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and> c \<notin> {ka..kb}"
   1.308  proof (cases "c < b")
   1.309    case True
   1.310    show ?thesis
   1.311    proof (cases "c < a")
   1.312      case True
   1.313 -    with `a < b` `c < b` have "c \<notin> closed_int a b"
   1.314 -      unfolding closed_int_def by auto
   1.315 +    with `a < b` `c < b` have "c \<notin> {a..b}"
   1.316 +      by auto
   1.317      with `a < b` show ?thesis by auto
   1.318    next
   1.319      case False
   1.320 @@ -325,11 +98,11 @@
   1.321  
   1.322      from ka_def `c < b` have kalb: "ka < b" by auto
   1.323      moreover from ka_def `c < b` have kagc: "ka > c" by simp
   1.324 -    ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
   1.325 +    ultimately have "c\<notin>{ka..b}" by auto
   1.326      moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
   1.327 -    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
   1.328 +    hence "{ka..b} \<subseteq> {a..b}" by auto
   1.329      ultimately have
   1.330 -      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
   1.331 +      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
   1.332        using kalb by auto
   1.333      then show ?thesis
   1.334        by auto
   1.335 @@ -341,11 +114,11 @@
   1.336    def kb \<equiv> "(a + b)/2"
   1.337    with `a < b` have "kb < b" by auto
   1.338    with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
   1.339 -  from `kb < c` have c: "c \<notin> closed_int a kb"
   1.340 -    unfolding closed_int_def by auto
   1.341 -  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
   1.342 -    unfolding closed_int_def by auto
   1.343 -  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
   1.344 +  from `kb < c` have c: "c \<notin> {a..kb}"
   1.345 +    by auto
   1.346 +  with `kb < b` have "{a..kb} \<subseteq> {a..b}"
   1.347 +    by auto
   1.348 +  with `a < kb` c have "a < kb \<and> {a..kb} \<subseteq> {a..b} \<and> c \<notin> {a..kb}"
   1.349      by simp
   1.350    then show ?thesis by auto
   1.351  qed
   1.352 @@ -360,13 +133,13 @@
   1.353  subsubsection {* Definition *}
   1.354  
   1.355  primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
   1.356 -  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
   1.357 +  "newInt 0 f = {f 0 + 1..f 0 + 2}"
   1.358    | "newInt (Suc n) f =
   1.359        (SOME e. (\<exists>e1 e2.
   1.360         e1 < e2 \<and>
   1.361 -       e = closed_int e1 e2 \<and>
   1.362 -       e \<subseteq> (newInt n f) \<and>
   1.363 -       (f (Suc n)) \<notin> e)
   1.364 +       e = {e1..e2} \<and>
   1.365 +       e \<subseteq> newInt n f \<and>
   1.366 +       f (Suc n) \<notin> e)
   1.367        )"
   1.368  
   1.369  
   1.370 @@ -377,7 +150,7 @@
   1.371  
   1.372  lemma newInt_ex:
   1.373    "\<exists>a b. a < b \<and>
   1.374 -   newInt (Suc n) f = closed_int a b \<and>
   1.375 +   newInt (Suc n) f = {a..b} \<and>
   1.376     newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.377     f (Suc n) \<notin> newInt (Suc n) f"
   1.378  proof (induct n)
   1.379 @@ -385,68 +158,67 @@
   1.380  
   1.381    let ?e = "SOME e. \<exists>e1 e2.
   1.382     e1 < e2 \<and>
   1.383 -   e = closed_int e1 e2 \<and>
   1.384 -   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.385 +   e = {e1..e2} \<and>
   1.386 +   e \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.387     f (Suc 0) \<notin> e"
   1.388  
   1.389    have "newInt (Suc 0) f = ?e" by auto
   1.390    moreover
   1.391    have "f 0 + 1 < f 0 + 2" by simp
   1.392    with closed_subset_ex have
   1.393 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.394 -     f (Suc 0) \<notin> (closed_int ka kb)" .
   1.395 +    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.396 +     f (Suc 0) \<notin> {ka..kb}" .
   1.397    hence
   1.398 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.399 -     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
   1.400 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.401 +     e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> e" by simp
   1.402    hence
   1.403 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   1.404 -     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?e"
   1.405 +    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and> ?e \<subseteq> {f 0 + 1..f 0 + 2} \<and> f (Suc 0) \<notin> ?e"
   1.406      by (rule someI_ex)
   1.407    ultimately have "\<exists>e1 e2. e1 < e2 \<and>
   1.408 -   newInt (Suc 0) f = closed_int e1 e2 \<and>
   1.409 -   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
   1.410 +   newInt (Suc 0) f = {e1..e2} \<and>
   1.411 +   newInt (Suc 0) f \<subseteq> {f 0 + 1..f 0 + 2} \<and>
   1.412     f (Suc 0) \<notin> newInt (Suc 0) f" by simp
   1.413    thus
   1.414 -    "\<exists>a b. a < b \<and> newInt (Suc 0) f = closed_int a b \<and>
   1.415 +    "\<exists>a b. a < b \<and> newInt (Suc 0) f = {a..b} \<and>
   1.416       newInt (Suc 0) f \<subseteq> newInt 0 f \<and> f (Suc 0) \<notin> newInt (Suc 0) f"
   1.417      by simp
   1.418  next
   1.419    case (Suc n)
   1.420    hence "\<exists>a b.
   1.421     a < b \<and>
   1.422 -   newInt (Suc n) f = closed_int a b \<and>
   1.423 +   newInt (Suc n) f = {a..b} \<and>
   1.424     newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.425     f (Suc n) \<notin> newInt (Suc n) f" by simp
   1.426    then obtain a and b where ab: "a < b \<and>
   1.427 -   newInt (Suc n) f = closed_int a b \<and>
   1.428 +   newInt (Suc n) f = {a..b} \<and>
   1.429     newInt (Suc n) f \<subseteq> newInt n f \<and>
   1.430     f (Suc n) \<notin> newInt (Suc n) f" by auto
   1.431 -  hence cab: "closed_int a b = newInt (Suc n) f" by simp
   1.432 +  hence cab: "{a..b} = newInt (Suc n) f" by simp
   1.433  
   1.434    let ?e = "SOME e. \<exists>e1 e2.
   1.435      e1 < e2 \<and>
   1.436 -    e = closed_int e1 e2 \<and>
   1.437 -    e \<subseteq> closed_int a b \<and>
   1.438 +    e = {e1..e2} \<and>
   1.439 +    e \<subseteq> {a..b} \<and>
   1.440      f (Suc (Suc n)) \<notin> e"
   1.441    from cab have ni: "newInt (Suc (Suc n)) f = ?e" by auto
   1.442  
   1.443    from ab have "a < b" by simp
   1.444    with closed_subset_ex have
   1.445 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and>
   1.446 -     f (Suc (Suc n)) \<notin> closed_int ka kb" .
   1.447 +    "\<exists>ka kb. ka < kb \<and> {ka..kb} \<subseteq> {a..b} \<and>
   1.448 +     f (Suc (Suc n)) \<notin> {ka..kb}" .
   1.449    hence
   1.450 -    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.451 -     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
   1.452 +    "\<exists>e. \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.453 +     {ka..kb} \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> {ka..kb}"
   1.454      by simp
   1.455    hence
   1.456 -    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
   1.457 -     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
   1.458 +    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = {ka..kb} \<and>
   1.459 +     e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> e" by simp
   1.460    hence
   1.461 -    "\<exists>ka kb. ka < kb \<and> ?e = closed_int ka kb \<and>
   1.462 -     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   1.463 +    "\<exists>ka kb. ka < kb \<and> ?e = {ka..kb} \<and>
   1.464 +     ?e \<subseteq> {a..b} \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
   1.465    with ab ni show
   1.466      "\<exists>ka kb. ka < kb \<and>
   1.467 -     newInt (Suc (Suc n)) f = closed_int ka kb \<and>
   1.468 +     newInt (Suc (Suc n)) f = {ka..kb} \<and>
   1.469       newInt (Suc (Suc n)) f \<subseteq> newInt (Suc n) f \<and>
   1.470       f (Suc (Suc n)) \<notin> newInt (Suc (Suc n)) f" by auto
   1.471  qed
   1.472 @@ -466,8 +238,8 @@
   1.473    fix n::nat
   1.474    {
   1.475      assume n0: "n = 0"
   1.476 -    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
   1.477 -    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
   1.478 +    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
   1.479 +    ultimately have "f n \<notin> newInt n f" by simp
   1.480    }
   1.481    moreover
   1.482    {
   1.483 @@ -476,7 +248,7 @@
   1.484      then obtain m where ndef: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.485  
   1.486      from newInt_ex have
   1.487 -      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   1.488 +      "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.489         newInt (Suc m) f \<subseteq> newInt m f \<and> f (Suc m) \<notin> newInt (Suc m) f" .
   1.490      then have "f (Suc m) \<notin> newInt (Suc m) f" by auto
   1.491      with ndef have "f n \<notin> newInt n f" by simp
   1.492 @@ -495,15 +267,15 @@
   1.493      fix n
   1.494      show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   1.495    qed
   1.496 -  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
   1.497 +  moreover have "\<forall>n. \<exists>a b. ?g n = {a..b} \<and> a \<le> b"
   1.498    proof
   1.499      fix n::nat
   1.500      {
   1.501        assume "n = 0"
   1.502        then have
   1.503 -        "?g n = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.504 +        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
   1.505          by simp
   1.506 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   1.507 +      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   1.508      }
   1.509      moreover
   1.510      {
   1.511 @@ -512,15 +284,15 @@
   1.512        then obtain m where nd: "n = Suc m" by (auto simp add: gr0_conv_Suc)
   1.513  
   1.514        have
   1.515 -        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = closed_int a b \<and>
   1.516 +        "\<exists>a b. a < b \<and> (newInt (Suc m) f) = {a..b} \<and>
   1.517          (newInt (Suc m) f) \<subseteq> (newInt m f) \<and> (f (Suc m)) \<notin> (newInt (Suc m) f)"
   1.518          by (rule newInt_ex)
   1.519        then obtain a and b where
   1.520 -        "a < b \<and> (newInt (Suc m) f) = closed_int a b" by auto
   1.521 -      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
   1.522 -      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
   1.523 +        "a < b \<and> (newInt (Suc m) f) = {a..b}" by auto
   1.524 +      with nd have "?g n = {a..b} \<and> a \<le> b" by auto
   1.525 +      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
   1.526      }
   1.527 -    ultimately show "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by (rule case_split)
   1.528 +    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
   1.529    qed
   1.530    ultimately show ?thesis by (rule NIP)
   1.531  qed
   1.532 @@ -542,3 +314,4 @@
   1.533  qed
   1.534  
   1.535  end
   1.536 +
     2.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 17 22:34:26 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 18 11:53:40 2013 +0100
     2.3 @@ -3031,43 +3031,6 @@
     2.4    shows "open s \<Longrightarrow> open (s - {x})"
     2.5    by (simp add: open_Diff)
     2.6  
     2.7 -text{* Finite intersection property *}
     2.8 -
     2.9 -lemma inj_setminus: "inj_on uminus (A::'a set set)"
    2.10 -  by (auto simp: inj_on_def)
    2.11 -
    2.12 -lemma compact_fip:
    2.13 -  "compact U \<longleftrightarrow>
    2.14 -    (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
    2.15 -  (is "_ \<longleftrightarrow> ?R")
    2.16 -proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
    2.17 -  fix A
    2.18 -  assume "compact U"
    2.19 -    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
    2.20 -    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
    2.21 -  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
    2.22 -    by auto
    2.23 -  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
    2.24 -    unfolding compact_eq_heine_borel by (metis subset_image_iff)
    2.25 -  with fi[THEN spec, of B] show False
    2.26 -    by (auto dest: finite_imageD intro: inj_setminus)
    2.27 -next
    2.28 -  fix A
    2.29 -  assume ?R
    2.30 -  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
    2.31 -  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
    2.32 -    by auto
    2.33 -  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
    2.34 -    by (metis subset_image_iff)
    2.35 -  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
    2.36 -    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
    2.37 -qed
    2.38 -
    2.39 -lemma compact_imp_fip:
    2.40 -  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
    2.41 -    s \<inter> (\<Inter> f) \<noteq> {}"
    2.42 -  unfolding compact_fip by auto
    2.43 -
    2.44  text{*Compactness expressed with filters*}
    2.45  
    2.46  definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
     3.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 17 22:34:26 2013 +0100
     3.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Dec 18 11:53:40 2013 +0100
     3.3 @@ -1906,6 +1906,47 @@
     3.4      by (intro exI[of _ "D - {-t}"]) auto
     3.5  qed
     3.6  
     3.7 +lemma inj_setminus: "inj_on uminus (A::'a set set)"
     3.8 +  by (auto simp: inj_on_def)
     3.9 +
    3.10 +lemma compact_fip:
    3.11 +  "compact U \<longleftrightarrow>
    3.12 +    (\<forall>A. (\<forall>a\<in>A. closed a) \<longrightarrow> (\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}) \<longrightarrow> U \<inter> \<Inter>A \<noteq> {})"
    3.13 +  (is "_ \<longleftrightarrow> ?R")
    3.14 +proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
    3.15 +  fix A
    3.16 +  assume "compact U"
    3.17 +    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
    3.18 +    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
    3.19 +  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
    3.20 +    by auto
    3.21 +  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
    3.22 +    unfolding compact_eq_heine_borel by (metis subset_image_iff)
    3.23 +  with fi[THEN spec, of B] show False
    3.24 +    by (auto dest: finite_imageD intro: inj_setminus)
    3.25 +next
    3.26 +  fix A
    3.27 +  assume ?R
    3.28 +  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
    3.29 +  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
    3.30 +    by auto
    3.31 +  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
    3.32 +    by (metis subset_image_iff)
    3.33 +  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
    3.34 +    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
    3.35 +qed
    3.36 +
    3.37 +lemma compact_imp_fip:
    3.38 +  "compact s \<Longrightarrow> \<forall>t \<in> f. closed t \<Longrightarrow> \<forall>f'. finite f' \<and> f' \<subseteq> f \<longrightarrow> (s \<inter> (\<Inter> f') \<noteq> {}) \<Longrightarrow>
    3.39 +    s \<inter> (\<Inter> f) \<noteq> {}"
    3.40 +  unfolding compact_fip by auto
    3.41 +
    3.42 +lemma compact_imp_fip_image:
    3.43 +  "compact s \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> closed (f i)) \<Longrightarrow> (\<And>I'. finite I' \<Longrightarrow> I' \<subseteq> I \<Longrightarrow> (s \<inter> (\<Inter>i\<in>I'. f i) \<noteq> {})) \<Longrightarrow>
    3.44 +    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
    3.45 +  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
    3.46 +  by (metis image_iff)
    3.47 +
    3.48  end
    3.49  
    3.50  lemma (in t2_space) compact_imp_closed: