# HG changeset patch
# User hoelzl
# Date 1387364020 -3600
# Node ID be020ec8560c598250174a1306c7345e24c7c8d8
# Parent  cdc6d8cbf7702d39336cff524cfe45fa07f226da
modernized ContNotDenum: use Set_Interval, and finite intersection property to show the nested interval property

diff -r cdc6d8cbf770 -r be020ec8560c src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Tue Dec 17 22:34:26 2013 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 18 11:53:40 2013 +0100
@@ -31,270 +31,43 @@
 
 subsection {* Closed Intervals *}
 
-text {* This section formalises some properties of closed intervals. *}
-
-subsubsection {* Definition *}
-
-definition
-  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set" where
-  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
-
-subsubsection {* Properties *}
-
-lemma closed_int_subset:
-  assumes xy: "x1 \<ge> x0" "y1 \<le> y0"
-  shows "closed_int x1 y1 \<subseteq> closed_int x0 y0"
-proof -
-  {
-    fix x::real
-    assume "x \<in> closed_int x1 y1"
-    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
-    with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
-    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
-  }
-  thus ?thesis by auto
-qed
-
-lemma closed_int_least:
-  assumes a: "a \<le> b"
-  shows "a \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. a \<le> x)"
-proof
-  from a have "a\<in>{x. a\<le>x \<and> x\<le>b}" by simp
-  thus "a \<in> closed_int a b" by (unfold closed_int_def)
-next
-  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. a\<le>x" by simp
-  thus "\<forall>x \<in> closed_int a b. a \<le> x" by (unfold closed_int_def)
-qed
-
-lemma closed_int_most:
-  assumes a: "a \<le> b"
-  shows "b \<in> closed_int a b \<and> (\<forall>x \<in> closed_int a b. x \<le> b)"
-proof
-  from a have "b\<in>{x. a\<le>x \<and> x\<le>b}" by simp
-  thus "b \<in> closed_int a b" by (unfold closed_int_def)
-next
-  have "\<forall>x\<in>{x. a\<le>x \<and> x\<le>b}. x\<le>b" by simp
-  thus "\<forall>x \<in> closed_int a b. x\<le>b" by (unfold closed_int_def)
-qed
-
-lemma closed_not_empty:
-  shows "a \<le> b \<Longrightarrow> \<exists>x. x \<in> closed_int a b" 
-  by (auto dest: closed_int_least)
-
-lemma closed_mem:
-  assumes "a \<le> c" and "c \<le> b"
-  shows "c \<in> closed_int a b"
-  using assms unfolding closed_int_def by auto
-
-lemma closed_subset:
-  assumes ac: "a \<le> b"  "c \<le> d" 
-  assumes closed: "closed_int a b \<subseteq> closed_int c d"
-  shows "b \<ge> c"
-proof -
-  from closed have "\<forall>x\<in>closed_int a b. x\<in>closed_int c d" by auto
-  hence "\<forall>x. a\<le>x \<and> x\<le>b \<longrightarrow> c\<le>x \<and> x\<le>d" by (unfold closed_int_def, auto)
-  with ac have "c\<le>b \<and> b\<le>d" by simp
-  thus ?thesis by auto
-qed
-
-
 subsection {* Nested Interval Property *}
 
 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 = closed_int 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 ?g = "\<lambda>n. (SOME c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x))"
-  have ne: "\<forall>n. \<exists>x. x\<in>(f n)"
-  proof
-    fix n
-    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" by simp
-    then obtain a and b where fn: "f n = closed_int a b \<and> a \<le> b" by auto
-    hence "a \<le> b" ..
-    with closed_not_empty have "\<exists>x. x\<in>closed_int a b" by simp
-    with fn show "\<exists>x. x\<in>(f n)" by simp
-  qed
-
-  have gdef: "\<forall>n. (?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)"
-  proof
-    fix n
-    from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
-    then obtain a and b where ff: "f n = closed_int a b" and "a \<le> b" by auto
-    hence "a \<le> b" by simp
-    hence "a\<in>closed_int a b \<and> (\<forall>x\<in>closed_int a b. a \<le> x)" by (rule closed_int_least)
-    with ff have "a\<in>(f n) \<and> (\<forall>x\<in>(f n). a \<le> x)" by simp
-    hence "\<exists>c. c\<in>(f n) \<and> (\<forall>x\<in>(f n). c \<le> x)" ..
-    thus "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by (rule someI_ex)
-  qed
-
-  -- "A denotes the set of all left-most points of all the intervals ..."
-  moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
-  ultimately have "A \<noteq> {}"
-  proof -
-    have "(0::nat) \<in> \<nat>" by simp
-    with Adef show ?thesis
-      by blast
-  qed
-
-  -- "Now show that A is bounded above ..."
-  moreover have "bdd_above A"
-  proof -
-    {
-      fix n
-      from ne have ex: "\<exists>x. x\<in>(f n)" ..
-      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
-      moreover
-      from closed have "\<exists>a b. f n = closed_int a b \<and> a \<le> b" ..
-      then obtain a and b where "f n = closed_int a b \<and> a \<le> b" by auto
-      hence "b\<in>(f n) \<and> (\<forall>x\<in>(f n). x \<le> b)" using closed_int_most by blast
-      ultimately have "\<forall>x\<in>(f n). (?g n) \<le> b" by simp
-      with ex have "(?g n) \<le> b" by auto
-      hence "\<exists>b. (?g n) \<le> b" by auto
-    }
-    hence aux: "\<forall>n. \<exists>b. (?g n) \<le> b" ..
-
-    have fs: "\<forall>n::nat. f n \<subseteq> f 0"
-    proof (rule allI, induct_tac n)
-      show "f 0 \<subseteq> f 0" by simp
-    next
-      fix n
-      assume "f n \<subseteq> f 0"
-      moreover from subset have "f (Suc n) \<subseteq> f n" ..
-      ultimately show "f (Suc n) \<subseteq> f 0" by simp
-    qed
-    have "\<forall>n. (?g n)\<in>(f 0)"
-    proof
-      fix n
-      from gdef have "(?g n)\<in>(f n) \<and> (\<forall>x\<in>(f n). (?g n)\<le>x)" by simp
-      hence "?g n \<in> f n" ..
-      with fs show "?g n \<in> f 0" by auto
-    qed
-    moreover from closed
-      obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
-    ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
-    with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
-    with Adef show "bdd_above A" by auto
-  qed
-
-  -- "denote this least upper bound as t ..."
-  def tdef: t == "Sup A"
-
-  -- "and finally show that this least upper bound is in all the intervals..."
-  have "\<forall>n. t \<in> f n"
-  proof
-    fix n::nat
-    from closed obtain a and b where
-      int: "f n = closed_int a b" and alb: "a \<le> b" by blast
+  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 "t \<ge> a"
-    proof -
-      have "a \<in> A"
-      proof -
-          (* by construction *)
-        from alb int have ain: "a\<in>f n \<and> (\<forall>x\<in>f n. a \<le> x)"
-          using closed_int_least by blast
-        moreover have "\<forall>e. e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<longrightarrow> e = a"
-        proof clarsimp
-          fix e
-          assume ein: "e \<in> f n" and lt: "\<forall>x\<in>f n. e \<le> x"
-          from lt ain have aux: "\<forall>x\<in>f n. a \<le> x \<and> e \<le> x" by auto
-  
-          from ein aux have "a \<le> e \<and> e \<le> e" by auto
-          moreover from ain aux have "a \<le> a \<and> e \<le> a" by auto
-          ultimately show "e = a" by simp
-        qed
-        hence "\<And>e.  e\<in>f n \<and> (\<forall>x\<in>f n. e \<le> x) \<Longrightarrow> e = a" by simp
-        ultimately have "(?g n) = a" by (rule some_equality)
-        moreover
-        {
-          have "n = of_nat n" by simp
-          moreover have "of_nat n \<in> \<nat>" by simp
-          ultimately have "n \<in> \<nat>"
-            apply -
-            apply (subst(asm) eq_sym_conv)
-            apply (erule subst)
-            .
-        }
-        with Adef have "(?g n) \<in> A" by auto
-        ultimately show ?thesis by simp
-      qed 
-      with `bdd_above A` show "a \<le> t"
-        unfolding tdef by (intro cSup_upper)
+  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
-    moreover have "t \<le> b"
-      unfolding tdef
-    proof (rule cSup_least)
-      {
-        from alb int have
-          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
-        
-        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
-        proof (rule allI, induct_tac m)
-          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
-        next
-          fix m n
-          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
-          {
-            fix p
-            from pp have "f (p + n) \<subseteq> f p" by simp
-            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
-            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
-            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
-          }
-          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
-        qed 
-        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
-        proof ((rule allI)+, rule impI)
-          fix \<alpha>::nat and \<beta>::nat
-          assume "\<beta> \<le> \<alpha>"
-          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
-          then obtain k where "\<alpha> = \<beta> + k" ..
-          moreover
-          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
-          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
-        qed 
-        
-        fix m   
-        {
-          assume "m \<ge> n"
-          with subsetm have "f m \<subseteq> f n" by simp
-          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
-          moreover
-          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
-          ultimately have "?g m \<le> b" by auto
-        }
-        moreover
-        {
-          assume "\<not>(m \<ge> n)"
-          hence "m < n" by simp
-          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
-          from closed obtain ma and mb where
-            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
-          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
-          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
-          moreover have "(?g m) = ma"
-          proof -
-            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
-            moreover from one have
-              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
-              by (rule closed_int_least)
-            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
-            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
-            thus "?g m = ma" by auto
-          qed
-          ultimately have "?g m \<le> b" by simp
-        } 
-        ultimately have "?g m \<le> b" by (rule case_split)
-      }
-      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
-    qed fact
-    ultimately have "t \<in> closed_int a b" by (rule closed_mem)
-    with int show "t \<in> f n" by simp
-  qed
-  hence "t \<in> (\<Inter>n. f n)" by auto
-  thus ?thesis by auto
+    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
 
 subsection {* Generating the intervals *}
@@ -309,14 +82,14 @@
 lemma closed_subset_ex:
   fixes c::real
   assumes "a < b"
-  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
+  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> closed_int a b"
-      unfolding closed_int_def by auto
+    with `a < b` `c < b` have "c \<notin> {a..b}"
+      by auto
     with `a < b` show ?thesis by auto
   next
     case False
@@ -325,11 +98,11 @@
 
     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>(closed_int ka b)" by (unfold closed_int_def, auto)
+    ultimately have "c\<notin>{ka..b}" by auto
     moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
-    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
+    hence "{ka..b} \<subseteq> {a..b}" by auto
     ultimately have
-      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+      "ka < b  \<and> {ka..b} \<subseteq> {a..b} \<and> c \<notin> {ka..b}"
       using kalb by auto
     then show ?thesis
       by auto
@@ -341,11 +114,11 @@
   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> closed_int a kb"
-    unfolding closed_int_def by auto
-  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
-    unfolding closed_int_def by auto
-  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
+  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
@@ -360,13 +133,13 @@
 subsubsection {* Definition *}
 
 primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
-  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+  "newInt 0 f = {f 0 + 1..f 0 + 2}"
   | "newInt (Suc n) f =
       (SOME e. (\<exists>e1 e2.
        e1 < e2 \<and>
-       e = closed_int e1 e2 \<and>
-       e \<subseteq> (newInt n f) \<and>
-       (f (Suc n)) \<notin> e)
+       e = {e1..e2} \<and>
+       e \<subseteq> newInt n f \<and>
+       f (Suc n) \<notin> e)
       )"
 
 
@@ -377,7 +150,7 @@
 
 lemma newInt_ex:
   "\<exists>a b. a < b \<and>
-   newInt (Suc n) f = closed_int 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)
@@ -385,68 +158,67 @@
 
   let ?e = "SOME e. \<exists>e1 e2.
    e1 < e2 \<and>
-   e = closed_int e1 e2 \<and>
-   e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<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> closed_int ka kb \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and>
-     f (Suc 0) \<notin> (closed_int ka kb)" .
+    "\<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 = closed_int ka kb \<and>
-     e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> e" by simp
+    "\<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 = closed_int ka kb \<and>
-     ?e \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<and> f (Suc 0) \<notin> ?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 (rule someI_ex)
   ultimately have "\<exists>e1 e2. e1 < e2 \<and>
-   newInt (Suc 0) f = closed_int e1 e2 \<and>
-   newInt (Suc 0) f \<subseteq> closed_int (f 0 + 1) (f 0 + 2) \<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 = closed_int a b \<and>
+    "\<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 = closed_int 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 = closed_int 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: "closed_int a b = newInt (Suc n) f" by simp
+  hence cab: "{a..b} = newInt (Suc n) f" by simp
 
   let ?e = "SOME e. \<exists>e1 e2.
     e1 < e2 \<and>
-    e = closed_int e1 e2 \<and>
-    e \<subseteq> closed_int a b \<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> closed_int ka kb \<subseteq> closed_int a b \<and>
-     f (Suc (Suc n)) \<notin> closed_int ka kb" .
+    "\<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 = closed_int ka kb \<and>
-     closed_int ka kb \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> closed_int ka kb"
+    "\<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
   hence
-    "\<exists>e.  \<exists>ka kb. ka < kb \<and> e = closed_int ka kb \<and>
-     e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> e" by simp
+    "\<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 = closed_int ka kb \<and>
-     ?e \<subseteq> closed_int a b \<and> f (Suc (Suc n)) \<notin> ?e" by (rule someI_ex)
+    "\<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 = closed_int 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
@@ -466,8 +238,8 @@
   fix n::nat
   {
     assume n0: "n = 0"
-    moreover have "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)" by simp
-    ultimately have "f n \<notin> newInt n f" by (unfold closed_int_def, simp)
+    moreover have "newInt 0 f = {f 0 + 1..f 0 + 2}" by simp
+    ultimately have "f n \<notin> newInt n f" by simp
   }
   moreover
   {
@@ -476,7 +248,7 @@
     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) = closed_int a b \<and>
+      "\<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
@@ -495,15 +267,15 @@
     fix n
     show "?g (Suc n) \<subseteq> ?g n" by (rule newInt_subset)
   qed
-  moreover have "\<forall>n. \<exists>a b. ?g n = closed_int a b \<and> a \<le> b"
+  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 = closed_int (f 0 + 1) (f 0 + 2) \<and> (f 0 + 1 \<le> f 0 + 2)"
+        "?g n = {f 0 + 1..f 0 + 2} \<and> (f 0 + 1 \<le> f 0 + 2)"
         by simp
-      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+      hence "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by blast
     }
     moreover
     {
@@ -512,15 +284,15 @@
       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) = closed_int a b \<and>
+        "\<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) = closed_int a b" by auto
-      with nd have "?g n = closed_int a b \<and> a \<le> b" by auto
-      hence "\<exists>a b. ?g n = closed_int a b \<and> a \<le> b" by blast
+        "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 = closed_int a b \<and> a \<le> b" by (rule case_split)
+    ultimately show "\<exists>a b. ?g n = {a..b} \<and> a \<le> b" by (rule case_split)
   qed
   ultimately show ?thesis by (rule NIP)
 qed
@@ -542,3 +314,4 @@
 qed
 
 end
+
diff -r cdc6d8cbf770 -r be020ec8560c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Dec 17 22:34:26 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Dec 18 11:53:40 2013 +0100
@@ -3031,43 +3031,6 @@
   shows "open s \<Longrightarrow> open (s - {x})"
   by (simp add: open_Diff)
 
-text{* Finite intersection property *}
-
-lemma inj_setminus: "inj_on uminus (A::'a set set)"
-  by (auto simp: inj_on_def)
-
-lemma compact_fip:
-  "compact U \<longleftrightarrow>
-    (\<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> {})"
-  (is "_ \<longleftrightarrow> ?R")
-proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
-  fix A
-  assume "compact U"
-    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
-    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
-  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
-    by auto
-  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
-    unfolding compact_eq_heine_borel by (metis subset_image_iff)
-  with fi[THEN spec, of B] show False
-    by (auto dest: finite_imageD intro: inj_setminus)
-next
-  fix A
-  assume ?R
-  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
-  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
-    by auto
-  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
-    by (metis subset_image_iff)
-  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
-    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
-qed
-
-lemma compact_imp_fip:
-  "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>
-    s \<inter> (\<Inter> f) \<noteq> {}"
-  unfolding compact_fip by auto
-
 text{*Compactness expressed with filters*}
 
 definition "filter_from_subbase B = Abs_filter (\<lambda>P. \<exists>X \<subseteq> B. finite X \<and> Inf X \<le> P)"
diff -r cdc6d8cbf770 -r be020ec8560c src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Dec 17 22:34:26 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Dec 18 11:53:40 2013 +0100
@@ -1906,6 +1906,47 @@
     by (intro exI[of _ "D - {-t}"]) auto
 qed
 
+lemma inj_setminus: "inj_on uminus (A::'a set set)"
+  by (auto simp: inj_on_def)
+
+lemma compact_fip:
+  "compact U \<longleftrightarrow>
+    (\<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> {})"
+  (is "_ \<longleftrightarrow> ?R")
+proof (safe intro!: compact_eq_heine_borel[THEN iffD2])
+  fix A
+  assume "compact U"
+    and A: "\<forall>a\<in>A. closed a" "U \<inter> \<Inter>A = {}"
+    and fi: "\<forall>B \<subseteq> A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}"
+  from A have "(\<forall>a\<in>uminus`A. open a) \<and> U \<subseteq> \<Union>(uminus`A)"
+    by auto
+  with `compact U` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<subseteq> \<Union>(uminus`B)"
+    unfolding compact_eq_heine_borel by (metis subset_image_iff)
+  with fi[THEN spec, of B] show False
+    by (auto dest: finite_imageD intro: inj_setminus)
+next
+  fix A
+  assume ?R
+  assume "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A"
+  then have "U \<inter> \<Inter>(uminus`A) = {}" "\<forall>a\<in>uminus`A. closed a"
+    by auto
+  with `?R` obtain B where "B \<subseteq> A" "finite (uminus`B)" "U \<inter> \<Inter>(uminus`B) = {}"
+    by (metis subset_image_iff)
+  then show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
+    by  (auto intro!: exI[of _ B] inj_setminus dest: finite_imageD)
+qed
+
+lemma compact_imp_fip:
+  "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>
+    s \<inter> (\<Inter> f) \<noteq> {}"
+  unfolding compact_fip by auto
+
+lemma compact_imp_fip_image:
+  "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>
+    s \<inter> (\<Inter>i\<in>I. f i) \<noteq> {}"
+  using finite_subset_image[of _ f I] compact_imp_fip[of s "f`I"] unfolding ball_simps[symmetric] INF_def
+  by (metis image_iff)
+
 end
 
 lemma (in t2_space) compact_imp_closed: