# HG changeset patch
# User hoelzl
# Date 1452271259 -3600
# Node ID 26c0a70f78a3d4e5f2b10c13df1ee2ca49558de8
# Parent  7a5754afe170fd2216cb2ac213bb9ee0587ee0e6
add uniform spaces

diff -r 7a5754afe170 -r 26c0a70f78a3 NEWS
--- a/NEWS	Fri Jan 08 16:37:56 2016 +0100
+++ b/NEWS	Fri Jan 08 17:40:59 2016 +0100
@@ -606,6 +606,14 @@
 terms for sup and inf. For example, "sup x (sup y (- x))" simplifies to
 "top". INCOMPATIBILITY.
 
+* Class uniform_space introduces uniform spaces btw topological spaces
+and metric spaces. Minor INCOMPATIBILITY: open_<type>_def needs to be
+introduced in the form of an uniformity. Some constants are more
+general now, it may be necessary to add type class constraints.
+
+  open_real_def \<leadsto> open_dist
+  open_complex_def \<leadsto> open_dist
+
 * Library/Monad_Syntax: notation uses symbols \<bind> and \<then>. INCOMPATIBILITY.
 
 * Library/Multiset:
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Complex.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -264,8 +264,11 @@
 definition dist_complex_def:
   "dist x y = cmod (x - y)"
 
-definition open_complex_def:
-  "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+definition uniformity_complex_def [code del]:
+  "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition open_complex_def [code del]:
+  "open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
 
 instance proof
   fix r :: real and x y :: complex and S :: "complex set"
@@ -277,7 +280,7 @@
     by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
   show "norm (x * y) = norm x * norm y"
     by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
-qed (rule complex_sgn_def dist_complex_def open_complex_def)+
+qed (rule complex_sgn_def dist_complex_def open_complex_def uniformity_complex_def)+
 
 end
 
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Filter.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -529,6 +529,8 @@
     unfolding le_filter_def eventually_filtermap
     by (subst (1 2) eventually_INF) auto
 qed
+
+
 subsubsection \<open>Standard filters\<close>
 
 definition principal :: "'a set \<Rightarrow> 'a filter" where
@@ -743,6 +745,52 @@
     by (blast intro: finite_subset)
 qed
 
+subsubsection \<open>Product of filters\<close>
+
+lemma filtermap_sequentually_ne_bot: "filtermap f sequentially \<noteq> bot"
+  by (auto simp add: filter_eq_iff eventually_filtermap eventually_sequentially)
+
+definition prod_filter :: "'a filter \<Rightarrow> 'b filter \<Rightarrow> ('a \<times> 'b) filter" (infixr "\<times>\<^sub>F" 80) where
+  "prod_filter F G =
+    (INF (P, Q):{(P, Q). eventually P F \<and> eventually Q G}. principal {(x, y). P x \<and> Q y})"
+
+lemma eventually_prod_filter: "eventually P (F \<times>\<^sub>F G) \<longleftrightarrow>
+  (\<exists>Pf Pg. eventually Pf F \<and> eventually Pg G \<and> (\<forall>x y. Pf x \<longrightarrow> Pg y \<longrightarrow> P (x, y)))"
+  unfolding prod_filter_def
+proof (subst eventually_INF_base, goal_cases)
+  case 2
+  moreover have "eventually Pf F \<Longrightarrow> eventually Qf F \<Longrightarrow> eventually Pg G \<Longrightarrow> eventually Qg G \<Longrightarrow>
+    \<exists>P Q. eventually P F \<and> eventually Q G \<and>
+      Collect P \<times> Collect Q \<subseteq> Collect Pf \<times> Collect Pg \<inter> Collect Qf \<times> Collect Qg" for Pf Pg Qf Qg
+    by (intro conjI exI[of _ "inf Pf Qf"] exI[of _ "inf Pg Qg"])
+       (auto simp: inf_fun_def eventually_conj)
+  ultimately show ?case
+    by auto
+qed (auto simp: eventually_principal intro: eventually_True)
+
+lemma prod_filter_mono: "F \<le> F' \<Longrightarrow> G \<le> G' \<Longrightarrow> F \<times>\<^sub>F G \<le> F' \<times>\<^sub>F G'"
+  by (auto simp: le_filter_def eventually_prod_filter)
+
+lemma eventually_prod_same: "eventually P (F \<times>\<^sub>F F) \<longleftrightarrow>
+    (\<exists>Q. eventually Q F \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
+  unfolding eventually_prod_filter
+  apply safe
+  apply (rule_tac x="inf Pf Pg" in exI)
+  apply (auto simp: inf_fun_def intro!: eventually_conj)
+  done
+
+lemma eventually_prod_sequentially:
+  "eventually P (sequentially \<times>\<^sub>F sequentially) \<longleftrightarrow> (\<exists>N. \<forall>m \<ge> N. \<forall>n \<ge> N. P (n, m))"
+  unfolding eventually_prod_same eventually_sequentially by auto
+
+lemma principal_prod_principal: "principal A \<times>\<^sub>F principal B = principal (A \<times> B)"
+  apply (simp add: filter_eq_iff eventually_prod_filter eventually_principal)
+  apply safe
+  apply blast
+  apply (intro conjI exI[of _ "\<lambda>x. x \<in> A"] exI[of _ "\<lambda>x. x \<in> B"])
+  apply auto
+  done
+
 subsection \<open>Limits\<close>
 
 definition filterlim :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b filter \<Rightarrow> 'a filter \<Rightarrow> bool" where
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -2769,7 +2769,7 @@
   then have "open (ereal -` S)"
     unfolding open_ereal_def by auto
   with \<open>x \<in> S\<close> obtain r where "0 < r" and dist: "\<And>y. dist y rx < r \<Longrightarrow> ereal y \<in> S"
-    unfolding open_real_def rx by auto
+    unfolding open_dist rx by auto
   then obtain n where
     upper: "\<And>N. n \<le> N \<Longrightarrow> u N < x + ereal r" and
     lower: "\<And>N. n \<le> N \<Longrightarrow> x < u N + ereal r"
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -815,13 +815,14 @@
 instantiation fps :: (comm_ring_1) metric_space
 begin
 
-definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
-
+definition uniformity_fps_def [code del]:
+  "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition open_fps_def' [code del]:
+  "open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
 
 instance
 proof
-  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" for S :: "'a fps set"
-    by (auto simp add: open_fps_def ball_def subset_eq)
   show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps"
     by (simp add: dist_fps_def split: split_if_asm)
   then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp
@@ -853,10 +854,12 @@
     qed
     thus ?thesis by (auto simp add: not_le[symmetric])
   qed
-qed
+qed (rule open_fps_def' uniformity_fps_def)+
 
 end
 
+lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)"
+  unfolding open_dist ball_def subset_eq by simp
 
 text \<open>The infinite sums and justification of the notation in textbooks.\<close>
 
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -11,7 +11,7 @@
 subsection \<open>Real inner product spaces\<close>
 
 text \<open>
-  Temporarily relax type constraints for @{term "open"},
+  Temporarily relax type constraints for @{term "open"}, @{term "uniformity"},
   @{term dist}, and @{term norm}.
 \<close>
 
@@ -22,9 +22,12 @@
   (@{const_name dist}, SOME @{typ "'a::dist \<Rightarrow> 'a \<Rightarrow> real"})\<close>
 
 setup \<open>Sign.add_const_constraint
+  (@{const_name uniformity}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
+
+setup \<open>Sign.add_const_constraint
   (@{const_name norm}, SOME @{typ "'a::norm \<Rightarrow> real"})\<close>
 
-class real_inner = real_vector + sgn_div_norm + dist_norm + open_dist +
+class real_inner = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_add_left: "inner (x + y) z = inner x z + inner y z"
@@ -166,7 +169,7 @@
   by (metis inner_commute inner_divide_left)
 
 text \<open>
-  Re-enable constraints for @{term "open"},
+  Re-enable constraints for @{term "open"}, @{term "uniformity"},
   @{term dist}, and @{term norm}.
 \<close>
 
@@ -174,6 +177,9 @@
   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
 
 setup \<open>Sign.add_const_constraint
+  (@{const_name uniformity}, SOME @{typ "('a::uniform_space \<times> 'a) filter"})\<close>
+
+setup \<open>Sign.add_const_constraint
   (@{const_name dist}, SOME @{typ "'a::metric_space \<Rightarrow> 'a \<Rightarrow> real"})\<close>
 
 setup \<open>Sign.add_const_constraint
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -229,9 +229,6 @@
 
 subsubsection \<open>Separation axioms\<close>
 
-lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
-  by (induct x) simp (* TODO: move elsewhere *)
-
 instance prod :: (t0_space, t0_space) t0_space
 proof
   fix x y :: "'a \<times> 'b" assume "x \<noteq> y"
@@ -264,12 +261,31 @@
 
 subsection \<open>Product is a metric space\<close>
 
-instantiation prod :: (metric_space, metric_space) metric_space
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
+
+instantiation prod :: (metric_space, metric_space) dist
 begin
 
 definition dist_prod_def[code del]:
   "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)"
 
+instance ..
+end
+
+instantiation prod :: (metric_space, metric_space) uniformity_dist
+begin
+
+definition [code del]:
+  "(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) = 
+    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance 
+  by standard (rule uniformity_prod_def)
+end
+
+instantiation prod :: (metric_space, metric_space) metric_space
+begin
+
 lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)"
   unfolding dist_prod_def by simp
 
@@ -292,7 +308,7 @@
         real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist)
 next
   fix S :: "('a \<times> 'b) set"
-  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   proof
     assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
     proof
@@ -351,6 +367,9 @@
       ultimately show "\<exists>A B. open A \<and> open B \<and> x \<in> A \<times> B \<and> A \<times> B \<subseteq> S" by fast
     qed
   qed
+  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+    unfolding * eventually_uniformity_metric
+    by (simp del: split_paired_All add: dist_prod_def dist_commute)
 qed
 
 end
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Limits.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -1624,16 +1624,6 @@
   using tendsto_mult [OF tendsto_const LIMSEQ_inverse_real_of_nat_add_minus [of 1]]
   by auto
 
-lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
-proof (subst lim_sequentially, intro allI impI exI)
-  fix e :: real assume e: "e > 0"
-  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
-  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
-  also note n
-  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
-    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
-qed
-
 lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
   using lim_1_over_n by (simp add: inverse_eq_divide)
 
@@ -2236,7 +2226,7 @@
     then have "x \<in> \<Union>C" using C by auto
     with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
     then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
-      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
+      by (auto simp: open_dist dist_real_def subset_eq Ball_def abs_less_iff)
     with \<open>c \<in> C\<close> show ?case
       by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
   qed
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -36,14 +36,18 @@
   using Rep_bcontfun[of x]
   by (auto simp: bcontfun_def intro: continuous_on_subset)
 
+(* TODO: Generalize to uniform spaces? *)
 instantiation bcontfun :: (topological_space, metric_space) metric_space
 begin
 
 definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
   where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
 
+definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
+  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
 definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
-  where "open_bcontfun S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
 
 lemma dist_bounded:
   fixes f :: "('a, 'b) bcontfun"
@@ -126,7 +130,7 @@
     finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
       by simp
   qed
-qed (simp add: open_bcontfun_def)
+qed (rule open_bcontfun_def uniformity_bcontfun_def)+
 
 end
 
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -122,8 +122,11 @@
 definition dist_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> real"
   where "dist_blinfun a b = norm (a - b)"
 
+definition [code del]:
+  "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
 definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
-  where "open_blinfun S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
 
 lift_definition uminus_blinfun :: "'a \<Rightarrow>\<^sub>L 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b" is "\<lambda>f x. - f x"
   by (rule bounded_linear_minus)
@@ -143,8 +146,8 @@
 
 instance
   apply standard
-  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def
-  apply (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps)+
+  unfolding dist_blinfun_def open_blinfun_def sgn_blinfun_def uniformity_blinfun_def
+  apply (rule refl | (transfer, force simp: onorm_triangle onorm_scaleR onorm_eq_0 algebra_simps))+
   done
 
 end
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -4106,7 +4106,7 @@
       done
   } then
   show ?thesis
-    by (auto simp: Complex.open_complex_def)
+    by (auto simp: open_dist)
 qed
 
 subsection\<open>Winding number is zero "outside" a curve, in various senses\<close>
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -874,8 +874,7 @@
           unfolding eventually_at_topological
           by metis
         from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
-          by (force simp: dist_commute open_real_def ball_def
-            dest!: bspec[OF _ \<open>y \<in> S\<close>])
+          by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
         def d' \<equiv> "min ((y + b)/2) (y + (d/2))"
         have "d' \<in> A"
           unfolding A_def
@@ -939,8 +938,7 @@
       where S: "open S" "y \<in> S" "\<And>x. x\<in>S \<Longrightarrow> x \<in> {y..b} \<Longrightarrow> ?le x"
         by metis
       from \<open>open S\<close> obtain d where d: "\<And>x. dist x y < d \<Longrightarrow> x \<in> S" "d > 0"
-        by (force simp: dist_commute open_real_def ball_def
-          dest!: bspec[OF _ \<open>y \<in> S\<close>])
+        by (force simp: dist_commute open_dist ball_def dest!: bspec[OF _ \<open>y \<in> S\<close>])
       def d' \<equiv> "min b (y + (d/2))"
       have "d' \<in> A"
         unfolding A_def
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -142,7 +142,7 @@
 instantiation vec :: (topological_space, finite) topological_space
 begin
 
-definition
+definition [code del]:
   "open (S :: ('a ^ 'b) set) \<longleftrightarrow>
     (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and>
       (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))"
@@ -260,13 +260,31 @@
 
 
 subsection \<open>Metric space\<close>
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
 
-instantiation vec :: (metric_space, finite) metric_space
+instantiation vec :: (metric_space, finite) dist
 begin
 
 definition
   "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV"
 
+instance ..
+end
+
+instantiation vec :: (metric_space, finite) uniformity_dist
+begin
+
+definition [code del]:
+  "(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) = 
+    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance 
+  by standard (rule uniformity_vec_def)
+end
+
+instantiation vec :: (metric_space, finite) metric_space
+begin
+
 lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y"
   unfolding dist_vec_def by (rule member_le_setL2) simp_all
 
@@ -284,7 +302,7 @@
     done
 next
   fix S :: "('a ^ 'b) set"
-  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   proof
     assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S"
     proof
@@ -322,6 +340,9 @@
         (\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis
     qed
   qed
+  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+    unfolding * eventually_uniformity_metric
+    by (simp del: split_paired_All add: dist_vec_def dist_commute)
 qed
 
 end
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -13,7 +13,6 @@
   "~~/src/HOL/Library/FuncSet"
   Linear_Algebra
   Norm_Arith
-
 begin
 
 lemma image_affinity_interval:
@@ -4573,20 +4572,19 @@
 
 subsubsection \<open>Completeness\<close>
 
-definition complete :: "'a::metric_space set \<Rightarrow> bool"
-  where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f \<longlonglongrightarrow> l))"
-
-lemma completeI:
+lemma (in metric_space) completeI:
   assumes "\<And>f. \<forall>n. f n \<in> s \<Longrightarrow> Cauchy f \<Longrightarrow> \<exists>l\<in>s. f \<longlonglongrightarrow> l"
   shows "complete s"
   using assms unfolding complete_def by fast
 
-lemma completeE:
+lemma (in metric_space) completeE:
   assumes "complete s" and "\<forall>n. f n \<in> s" and "Cauchy f"
   obtains l where "l \<in> s" and "f \<longlonglongrightarrow> l"
   using assms unfolding complete_def by fast
 
+(* TODO: generalize to uniform spaces *)
 lemma compact_imp_complete:
+  fixes s :: "'a::metric_space set"
   assumes "compact s"
   shows "complete s"
 proof -
@@ -4816,6 +4814,7 @@
 qed
 
 lemma complete_imp_closed:
+  fixes s :: "'a::metric_space set"
   assumes "complete s"
   shows "closed s"
 proof (unfold closed_sequential_limits, clarify)
@@ -4831,6 +4830,7 @@
 qed
 
 lemma complete_inter_closed:
+  fixes s :: "'a::metric_space set"
   assumes "complete s" and "closed t"
   shows "complete (s \<inter> t)"
 proof (rule completeI)
@@ -4846,6 +4846,7 @@
 qed
 
 lemma complete_closed_subset:
+  fixes s :: "'a::metric_space set"
   assumes "closed s" and "s \<subseteq> t" and "complete t"
   shows "complete s"
   using assms complete_inter_closed [of t s] by (simp add: Int_absorb1)
@@ -5225,9 +5226,13 @@
   unfolding continuous_on_def Lim_within
   by (metis dist_pos_lt dist_self)
 
-definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::metric_space \<Rightarrow> 'b::metric_space) \<Rightarrow> bool"
-  where "uniformly_continuous_on s f \<longleftrightarrow>
+lemma uniformly_continuous_on_def:
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
+  shows "uniformly_continuous_on s f \<longleftrightarrow>
     (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e)"
+  unfolding uniformly_continuous_on_uniformity
+    uniformity_dist filterlim_INF filterlim_principal eventually_inf_principal
+  by (force simp: Ball_def uniformity_dist[symmetric] eventually_uniformity_metric)
 
 text\<open>Some simple consequential lemmas.\<close>
 
@@ -5242,10 +5247,6 @@
 using assms
 by (auto simp: uniformly_continuous_on_def)
 
-lemma uniformly_continuous_imp_continuous:
-  "uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
-  unfolding uniformly_continuous_on_def continuous_on_iff by blast
-
 lemma continuous_at_imp_continuous_within:
   "continuous (at x) f \<Longrightarrow> continuous (at x within s) f"
   unfolding continuous_within continuous_at using Lim_at_imp_Lim_at_within by auto
@@ -5331,8 +5332,7 @@
 
 lemma uniformly_continuous_on_sequentially:
   "uniformly_continuous_on s f \<longleftrightarrow> (\<forall>x y. (\<forall>n. x n \<in> s) \<and> (\<forall>n. y n \<in> s) \<and>
-                    ((\<lambda>n. dist (x n) (y n)) \<longlongrightarrow> 0) sequentially
-                    \<longrightarrow> ((\<lambda>n. dist (f(x n)) (f(y n))) \<longlongrightarrow> 0) sequentially)" (is "?lhs = ?rhs")
+    (\<lambda>n. dist (x n) (y n)) \<longlonglongrightarrow> 0 \<longrightarrow> (\<lambda>n. dist (f(x n)) (f(y n))) \<longlonglongrightarrow> 0)" (is "?lhs = ?rhs")
 proof
   assume ?lhs
   {
@@ -5421,7 +5421,7 @@
   using assms
   unfolding continuous_within
   by (force simp add: intro: Lim_transform_within)
- 
+
 
 subsubsection \<open>Structural rules for pointwise continuity\<close>
 
@@ -5462,14 +5462,6 @@
 
 subsubsection \<open>Structural rules for uniform continuity\<close>
 
-lemma uniformly_continuous_on_id[continuous_intros]:
-  "uniformly_continuous_on s (\<lambda>x. x)"
-  unfolding uniformly_continuous_on_def by auto
-
-lemma uniformly_continuous_on_const[continuous_intros]:
-  "uniformly_continuous_on s (\<lambda>x. c)"
-  unfolding uniformly_continuous_on_def by simp
-
 lemma uniformly_continuous_on_dist[continuous_intros]:
   fixes f g :: "'a::metric_space \<Rightarrow> 'b::metric_space"
   assumes "uniformly_continuous_on s f"
@@ -5497,12 +5489,14 @@
 qed
 
 lemma uniformly_continuous_on_norm[continuous_intros]:
+  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: real_normed_vector"
   assumes "uniformly_continuous_on s f"
   shows "uniformly_continuous_on s (\<lambda>x. norm (f x))"
   unfolding norm_conv_dist using assms
   by (intro uniformly_continuous_on_dist uniformly_continuous_on_const)
 
 lemma (in bounded_linear) uniformly_continuous_on[continuous_intros]:
+  fixes g :: "_::metric_space \<Rightarrow> _"
   assumes "uniformly_continuous_on s g"
   shows "uniformly_continuous_on s (\<lambda>x. f (g x))"
   using assms unfolding uniformly_continuous_on_sequentially
@@ -5544,30 +5538,9 @@
   using assms uniformly_continuous_on_add [of s f "- g"]
     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
 
-text\<open>Continuity of all kinds is preserved under composition.\<close>
-
 lemmas continuous_at_compose = isCont_o
 
-lemma uniformly_continuous_on_compose[continuous_intros]:
-  assumes "uniformly_continuous_on s f"  "uniformly_continuous_on (f ` s) g"
-  shows "uniformly_continuous_on s (g \<circ> f)"
-proof -
-  {
-    fix e :: real
-    assume "e > 0"
-    then obtain d where "d > 0"
-      and d: "\<forall>x\<in>f ` s. \<forall>x'\<in>f ` s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e"
-      using assms(2) unfolding uniformly_continuous_on_def by auto
-    obtain d' where "d'>0" "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d' \<longrightarrow> dist (f x') (f x) < d"
-      using \<open>d > 0\<close> using assms(1) unfolding uniformly_continuous_on_def by auto
-    then have "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist ((g \<circ> f) x') ((g \<circ> f) x) < e"
-      using \<open>d>0\<close> using d by auto
-  }
-  then show ?thesis
-    using assms unfolding uniformly_continuous_on_def by auto
-qed
-
-text\<open>Continuity in terms of open preimages.\<close>
+text \<open>Continuity in terms of open preimages.\<close>
 
 lemma continuous_at_open:
   "continuous (at x) f \<longleftrightarrow> (\<forall>t. open t \<and> f x \<in> t --> (\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x' \<in> s. (f x') \<in> t)))"
@@ -6124,6 +6097,7 @@
 text \<open>Continuity implies uniform continuity on a compact domain.\<close>
 
 lemma compact_uniformly_continuous:
+  fixes f :: "'a :: metric_space \<Rightarrow> 'b :: metric_space"
   assumes f: "continuous_on s f"
     and s: "compact s"
   shows "uniformly_continuous_on s f"
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -12,24 +12,24 @@
 morphisms of_discrete discrete
 ..
 
-instantiation discrete :: (type) topological_space
-begin
-
-definition open_discrete::"'a discrete set \<Rightarrow> bool"
-  where "open_discrete s = True"
-
-instance proof qed (auto simp: open_discrete_def)
-end
-
 instantiation discrete :: (type) metric_space
 begin
 
-definition dist_discrete::"'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
+definition dist_discrete :: "'a discrete \<Rightarrow> 'a discrete \<Rightarrow> real"
   where "dist_discrete n m = (if n = m then 0 else 1)"
 
-instance proof qed (auto simp: open_discrete_def dist_discrete_def intro: exI[where x=1])
+definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
+  "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
+  "(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
+
+instance proof qed (auto simp: uniformity_discrete_def open_discrete_def dist_discrete_def intro: exI[where x=1])
 end
 
+lemma open_discrete: "open (S :: 'a discrete set)"
+  unfolding open_dist dist_discrete_def by (auto intro!: exI[of _ "1 / 2"])
+
 instance discrete :: (type) complete_space
 proof
   fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
@@ -54,7 +54,7 @@
   have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
     by (intro generate_topology_Union) (auto intro: generate_topology.intros)
   then have "open = generate_topology ?B"
-    by (auto intro!: ext simp: open_discrete_def)
+    by (auto intro!: ext simp: open_discrete)
   moreover have "countable ?B" by simp
   ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
 qed
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -150,7 +150,7 @@
 begin
 
 definition open_finmap :: "('a \<Rightarrow>\<^sub>F 'b) set \<Rightarrow> bool" where
-  "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
+   [code del]: "open_finmap = generate_topology {Pi' a b|a b. \<forall>i\<in>a. open (b i)}"
 
 lemma open_Pi'I: "(\<And>i. i \<in> I \<Longrightarrow> open (A i)) \<Longrightarrow> open (Pi' I A)"
   by (auto intro: generate_topology.Basis simp: open_finmap_def)
@@ -254,12 +254,31 @@
 
 subsection \<open>Metric Space of Finite Maps\<close>
 
-instantiation finmap :: (type, metric_space) metric_space
+(* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
+
+instantiation finmap :: (type, metric_space) dist
 begin
 
 definition dist_finmap where
   "dist P Q = Max (range (\<lambda>i. dist ((P)\<^sub>F i) ((Q)\<^sub>F i))) + (if domain P = domain Q then 0 else 1)"
 
+instance ..
+end
+
+instantiation finmap :: (type, metric_space) uniformity_dist
+begin
+
+definition [code del]:
+  "(uniformity :: (('a, 'b) finmap \<times> ('a, 'b) finmap) filter) = 
+    (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
+instance 
+  by standard (rule uniformity_finmap_def)
+end
+
+instantiation finmap :: (type, metric_space) metric_space
+begin
+
 lemma finite_proj_image': "x \<notin> domain P \<Longrightarrow> finite ((P)\<^sub>F ` S)"
   by (rule finite_subset[of _ "proj P ` (domain P \<inter> S \<union> {x})"]) auto
 
@@ -308,7 +327,7 @@
 instance
 proof
   fix S::"('a \<Rightarrow>\<^sub>F 'b) set"
-  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
+  have *: "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" (is "_ = ?od")
   proof
     assume "open S"
     thus ?od
@@ -387,6 +406,9 @@
       by (intro generate_topology.UN) (auto intro: generate_topology.Basis)
     finally show "open S" .
   qed
+  show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
+    unfolding * eventually_uniformity_metric
+    by (simp del: split_paired_All add: dist_finmap_def dist_commute eq_commute)
 next
   fix P Q::"'a \<Rightarrow>\<^sub>F 'b"
   have Max_eq_iff: "\<And>A m. finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> (Max A = m) = (m \<in> A \<and> (\<forall>a\<in>A. a \<le> m))"
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Product_Type.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -1068,6 +1068,9 @@
 lemma mem_Sigma_iff [iff]: "((a,b): Sigma A B) = (a:A & b:B(a))"
   by blast
 
+lemma mem_Times_iff: "x \<in> A \<times> B \<longleftrightarrow> fst x \<in> A \<and> snd x \<in> B"
+  by (induct x) simp
+
 lemma Sigma_empty_iff: "(SIGMA i:I. X i) = {} \<longleftrightarrow> (\<forall>i\<in>I. X i = {})"
   by auto
 
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -191,7 +191,7 @@
   fixes x :: "'a::real_vector"
   shows "scaleR (-1) x = - x"
   using scaleR_minus_left [of 1 x] by simp
-  
+
 class real_algebra = real_vector + ring +
   assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
   and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
@@ -662,10 +662,19 @@
 class dist_norm = dist + norm + minus +
   assumes dist_norm: "dist x y = norm (x - y)"
 
-class open_dist = "open" + dist +
-  assumes open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+class uniformity_dist = dist + uniformity +
+  assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+begin
 
-class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
+lemma eventually_uniformity_metric:
+  "eventually P uniformity \<longleftrightarrow> (\<exists>e>0. \<forall>x y. dist x y < e \<longrightarrow> P (x, y))"
+  unfolding uniformity_dist
+  by (subst eventually_INF_base)
+     (auto simp: eventually_principal subset_eq intro: bexI[of _ "min _ _"])
+
+end
+
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm + uniformity_dist + open_uniformity +
   assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
@@ -686,8 +695,8 @@
 
 class real_normed_algebra_1 = real_algebra_1 + real_normed_algebra +
   assumes norm_one [simp]: "norm 1 = 1"
-  
-lemma (in real_normed_algebra_1) scaleR_power [simp]: 
+
+lemma (in real_normed_algebra_1) scaleR_power [simp]:
   "(scaleR x y) ^ n = scaleR (x^n) (y^n)"
   by (induction n) (simp_all add: scaleR_one scaleR_scaleR mult_ac)
 
@@ -1010,7 +1019,7 @@
 
 subsection \<open>Metric spaces\<close>
 
-class metric_space = open_dist +
+class metric_space = uniformity_dist + open_uniformity +
   assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
   assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
 begin
@@ -1074,26 +1083,23 @@
   shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
 by (rule dist_triangle_half_l, simp_all add: dist_commute)
 
-subclass topological_space
+subclass uniform_space
 proof
-  have "\<exists>e::real. 0 < e"
-    by (blast intro: zero_less_one)
-  then show "open UNIV"
-    unfolding open_dist by simp
-next
-  fix S T assume "open S" "open T"
-  then show "open (S \<inter> T)"
-    unfolding open_dist
-    apply clarify
-    apply (drule (1) bspec)+
-    apply (clarify, rename_tac r s)
-    apply (rule_tac x="min r s" in exI, simp)
-    done
-next
-  fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
-    unfolding open_dist by (meson UnionE UnionI) 
+  fix E x assume "eventually E uniformity"
+  then obtain e where E: "0 < e" "\<And>x y. dist x y < e \<Longrightarrow> E (x, y)"
+    unfolding eventually_uniformity_metric by auto
+  then show "E (x, x)" "\<forall>\<^sub>F (x, y) in uniformity. E (y, x)"
+    unfolding eventually_uniformity_metric by (auto simp: dist_commute)
+
+  show "\<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
+    using E dist_triangle_half_l[where e=e] unfolding eventually_uniformity_metric
+    by (intro exI[of _ "\<lambda>(x, y). dist x y < e / 2"] exI[of _ "e/2"] conjI)
+       (auto simp: dist_commute)
 qed
 
+lemma open_dist: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  unfolding open_uniformity eventually_uniformity_metric by (simp add: dist_commute)
+
 lemma open_ball: "open {y. dist x y < d}"
 proof (unfold open_dist, intro ballI)
   fix y assume *: "y \<in> {y. dist x y < d}"
@@ -1156,8 +1162,11 @@
 definition dist_real_def:
   "dist x y = \<bar>x - y\<bar>"
 
+definition uniformity_real_def [code del]:
+  "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+
 definition open_real_def [code del]:
-  "open (S :: real set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+  "open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
 
 definition real_norm_def [simp]:
   "norm r = \<bar>r\<bar>"
@@ -1165,8 +1174,9 @@
 instance
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
 apply (rule dist_real_def)
+apply (simp add: sgn_real_def)
+apply (rule uniformity_real_def)
 apply (rule open_real_def)
-apply (simp add: sgn_real_def)
 apply (rule abs_eq_0)
 apply (rule abs_triangle_ineq)
 apply (rule abs_mult)
@@ -1188,7 +1198,7 @@
   proof (rule ext, safe)
     fix S :: "real set" assume "open S"
     then obtain f where "\<forall>x\<in>S. 0 < f x \<and> (\<forall>y. dist y x < f x \<longrightarrow> y \<in> S)"
-      unfolding open_real_def bchoice_iff ..
+      unfolding open_dist bchoice_iff ..
     then have *: "S = (\<Union>x\<in>S. {x - f x <..} \<inter> {..< x + f x})"
       by (fastforce simp: dist_real_def)
     show "generate_topology (range lessThan \<union> range greaterThan) S"
@@ -1199,14 +1209,14 @@
   next
     fix S :: "real set" assume "generate_topology (range lessThan \<union> range greaterThan) S"
     moreover have "\<And>a::real. open {..<a}"
-      unfolding open_real_def dist_real_def
+      unfolding open_dist dist_real_def
     proof clarify
       fix x a :: real assume "x < a"
       hence "0 < a - x \<and> (\<forall>y. \<bar>y - x\<bar> < a - x \<longrightarrow> y \<in> {..<a})" by auto
       thus "\<exists>e>0. \<forall>y. \<bar>y - x\<bar> < e \<longrightarrow> y \<in> {..<a}" ..
     qed
     moreover have "\<And>a::real. open {a <..}"
-      unfolding open_real_def dist_real_def
+      unfolding open_dist dist_real_def
     proof clarify
       fix x a :: real assume "a < x"
       hence "0 < x - a \<and> (\<forall>y. \<bar>y - x\<bar> < x - a \<longrightarrow> y \<in> {a<..})" by auto
@@ -1233,6 +1243,11 @@
 setup \<open>Sign.add_const_constraint
   (@{const_name "open"}, SOME @{typ "'a::topological_space set \<Rightarrow> bool"})\<close>
 
+text \<open>Only allow @{term "uniformity"} in class \<open>uniform_space\<close>.\<close>
+
+setup \<open>Sign.add_const_constraint
+  (@{const_name "uniformity"}, SOME @{typ "('a::uniformity \<times> 'a) filter"})\<close>
+
 text \<open>Only allow @{term dist} in class \<open>metric_space\<close>.\<close>
 
 setup \<open>Sign.add_const_constraint
@@ -1786,10 +1801,22 @@
 
 subsection \<open>Cauchy sequences\<close>
 
-definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
-  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
+lemma (in metric_space) Cauchy_def: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
+proof -
+  have *: "eventually P (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) =
+    (\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. P (X m, X n))" for P
+  proof (subst eventually_INF_base, goal_cases)
+    case (2 a b) then show ?case
+      by (intro bexI[of _ "max a b"]) (auto simp: eventually_principal subset_eq)
+  qed (auto simp: eventually_principal, blast)
+  have "Cauchy X \<longleftrightarrow> (INF M. principal {(X m, X n) | n m. m \<ge> M \<and> n \<ge> M}) \<le> uniformity"
+    unfolding Cauchy_uniform_iff le_filter_def * ..
+  also have "\<dots> = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e)"
+    unfolding uniformity_dist le_INF_iff by (auto simp: * le_principal)
+  finally show ?thesis .
+qed
 
-lemma Cauchy_altdef:
+lemma (in metric_space) Cauchy_altdef:
   "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
 proof
   assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
@@ -1812,18 +1839,18 @@
   qed
 qed
 
-lemma metric_CauchyI:
+lemma (in metric_space) metric_CauchyI:
   "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   by (simp add: Cauchy_def)
 
-lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+lemma (in metric_space) CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   unfolding Cauchy_altdef by blast
 
-lemma metric_CauchyD:
+lemma (in metric_space) metric_CauchyD:
   "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   by (simp add: Cauchy_def)
 
-lemma metric_Cauchy_iff2:
+lemma (in metric_space) metric_Cauchy_iff2:
   "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < inverse(real (Suc j))))"
 apply (simp add: Cauchy_def, auto)
 apply (drule reals_Archimedean, safe)
@@ -1837,40 +1864,118 @@
   "Cauchy X = (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
   unfolding metric_Cauchy_iff2 dist_real_def ..
 
-lemma Cauchy_subseq_Cauchy:
-  "\<lbrakk> Cauchy X; subseq f \<rbrakk> \<Longrightarrow> Cauchy (X o f)"
-apply (auto simp add: Cauchy_def)
-apply (drule_tac x=e in spec, clarify)
-apply (rule_tac x=M in exI, clarify)
-apply (blast intro: le_trans [OF _ seq_suble] dest!: spec)
-done
-
-theorem LIMSEQ_imp_Cauchy:
-  assumes X: "X \<longlonglongrightarrow> a" shows "Cauchy X"
-proof (rule metric_CauchyI)
-  fix e::real assume "0 < e"
-  hence "0 < e/2" by simp
-  with X have "\<exists>N. \<forall>n\<ge>N. dist (X n) a < e/2" by (rule metric_LIMSEQ_D)
-  then obtain N where N: "\<forall>n\<ge>N. dist (X n) a < e/2" ..
-  show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
-  proof (intro exI allI impI)
-    fix m assume "N \<le> m"
-    hence m: "dist (X m) a < e/2" using N by blast
-    fix n assume "N \<le> n"
-    hence n: "dist (X n) a < e/2" using N by blast
-    have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
-      by (rule dist_triangle2)
-    also from m n have "\<dots> < e" by simp
-    finally show "dist (X m) (X n) < e" .
-  qed
+lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
+proof (subst lim_sequentially, intro allI impI exI)
+  fix e :: real assume e: "e > 0"
+  fix n :: nat assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
+  have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
+  also note n
+  finally show "dist (1 / of_nat n :: 'a) 0 < e" using e
+    by (simp add: divide_simps mult.commute norm_conv_dist[symmetric] norm_divide)
 qed
 
-lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
-unfolding convergent_def
-by (erule exE, erule LIMSEQ_imp_Cauchy)
+lemma (in metric_space) complete_def:
+  shows "complete S = (\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l))"
+  unfolding complete_uniform
+proof safe
+  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> S" "Cauchy f"
+    and *: "\<forall>F\<le>principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x)"
+  then show "\<exists>l\<in>S. f \<longlonglongrightarrow> l"
+    unfolding filterlim_def using f
+    by (intro *[rule_format])
+       (auto simp: filtermap_sequentually_ne_bot le_principal eventually_filtermap Cauchy_uniform)
+next
+  fix F :: "'a filter" assume "F \<le> principal S" "F \<noteq> bot" "cauchy_filter F"
+  assume seq: "\<forall>f. (\<forall>n. f n \<in> S) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>S. f \<longlonglongrightarrow> l)"
+
+  from \<open>F \<le> principal S\<close> \<open>cauchy_filter F\<close> have FF_le: "F \<times>\<^sub>F F \<le> uniformity_on S"
+    by (simp add: cauchy_filter_def principal_prod_principal[symmetric] prod_filter_mono)
+
+  let ?P = "\<lambda>P e. eventually P F \<and> (\<forall>x. P x \<longrightarrow> x \<in> S) \<and> (\<forall>x y. P x \<longrightarrow> P y \<longrightarrow> dist x y < e)"
+
+  { fix \<epsilon> :: real assume "0 < \<epsilon>"
+    then have "eventually (\<lambda>(x, y). x \<in> S \<and> y \<in> S \<and> dist x y < \<epsilon>) (uniformity_on S)"
+      unfolding eventually_inf_principal eventually_uniformity_metric by auto
+    from filter_leD[OF FF_le this] have "\<exists>P. ?P P \<epsilon>"
+      unfolding eventually_prod_same by auto }
+  note P = this
+
+  have "\<exists>P. \<forall>n. ?P (P n) (1 / Suc n) \<and> P (Suc n) \<le> P n"
+  proof (rule dependent_nat_choice)
+    show "\<exists>P. ?P P (1 / Suc 0)"
+      using P[of 1] by auto
+  next
+    fix P n assume "?P P (1/Suc n)"
+    moreover obtain Q where "?P Q (1 / Suc (Suc n))"
+      using P[of "1/Suc (Suc n)"] by auto
+    ultimately show "\<exists>Q. ?P Q (1 / Suc (Suc n)) \<and> Q \<le> P"
+      by (intro exI[of _ "\<lambda>x. P x \<and> Q x"]) (auto simp: eventually_conj_iff)
+  qed
+  then obtain P where P: "\<And>n. eventually (P n) F" "\<And>n x. P n x \<Longrightarrow> x \<in> S"
+    "\<And>n x y. P n x \<Longrightarrow> P n y \<Longrightarrow> dist x y < 1 / Suc n" "\<And>n. P (Suc n) \<le> P n"
+    by metis
+  have "antimono P"
+    using P(4) unfolding decseq_Suc_iff le_fun_def by blast
+
+  obtain X where X: "\<And>n. P n (X n)"
+    using P(1)[THEN eventually_happens'[OF \<open>F \<noteq> bot\<close>]] by metis
+  have "Cauchy X"
+    unfolding metric_Cauchy_iff2 inverse_eq_divide
+  proof (intro exI allI impI)
+    fix j m n :: nat assume "j \<le> m" "j \<le> n"
+    with \<open>antimono P\<close> X have "P j (X m)" "P j (X n)"
+      by (auto simp: antimono_def)
+    then show "dist (X m) (X n) < 1 / Suc j"
+      by (rule P)
+  qed
+  moreover have "\<forall>n. X n \<in> S"
+    using P(2) X by auto
+  ultimately obtain x where "X \<longlonglongrightarrow> x" "x \<in> S"
+    using seq by blast
+
+  show "\<exists>x\<in>S. F \<le> nhds x"
+  proof (rule bexI)
+    { fix e :: real assume "0 < e"
+      then have "(\<lambda>n. 1 / Suc n :: real) \<longlonglongrightarrow> 0 \<and> 0 < e / 2"
+        by (subst LIMSEQ_Suc_iff) (auto intro!: lim_1_over_n)
+      then have "\<forall>\<^sub>F n in sequentially. dist (X n) x < e / 2 \<and> 1 / Suc n < e / 2"
+        using \<open>X \<longlonglongrightarrow> x\<close> unfolding tendsto_iff order_tendsto_iff[where 'a=real] eventually_conj_iff by blast
+      then obtain n where "dist x (X n) < e / 2" "1 / Suc n < e / 2"
+        by (auto simp: eventually_sequentially dist_commute)
+      have "eventually (\<lambda>y. dist y x < e) F"
+        using \<open>eventually (P n) F\<close>
+      proof eventually_elim
+        fix y assume "P n y"
+        then have "dist y (X n) < 1 / Suc n"
+          by (intro X P)
+        also have "\<dots> < e / 2" by fact
+        finally show "dist y x < e"
+          by (rule dist_triangle_half_l) fact
+      qed }
+    then show "F \<le> nhds x"
+      unfolding nhds_metric le_INF_iff le_principal by auto
+  qed fact
+qed
+
+lemma (in metric_space) totally_bounded_metric:
+  "totally_bounded S \<longleftrightarrow> (\<forall>e>0. \<exists>k. finite k \<and> S \<subseteq> (\<Union>x\<in>k. {y. dist x y < e}))"
+  unfolding totally_bounded_def eventually_uniformity_metric imp_ex
+  apply (subst all_comm)
+  apply (intro arg_cong[where f=All] ext)
+  apply safe
+  subgoal for e
+    apply (erule allE[of _ "\<lambda>(x, y). dist x y < e"])
+    apply auto
+    done
+  subgoal for e P k
+    apply (intro exI[of _ k])
+    apply (force simp: subset_eq)
+    done
+  done
 
 subsubsection \<open>Cauchy Sequences are Convergent\<close>
 
+(* TODO: update to uniform_space *)
 class complete_space = metric_space +
   assumes Cauchy_convergent: "Cauchy X \<Longrightarrow> convergent X"
 
diff -r 7a5754afe170 -r 26c0a70f78a3 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Fri Jan 08 16:37:56 2016 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Jan 08 17:40:59 2016 +0100
@@ -11,7 +11,6 @@
 
 named_theorems continuous_intros "structural introduction rules for continuity"
 
-
 subsection \<open>Topological space\<close>
 
 class "open" =
@@ -693,8 +692,6 @@
   by (rule tendsto_le [OF F tendsto_const x a])
 
 
-
-
 subsubsection \<open>Rules about @{const Lim}\<close>
 
 lemma tendsto_Lim:
@@ -2435,4 +2432,173 @@
   qed
 qed (intro cSUP_least \<open>antimono f\<close>[THEN antimonoD] cInf_lower S)
 
+subsection \<open>Uniform spaces\<close>
+
+class uniformity = 
+  fixes uniformity :: "('a \<times> 'a) filter"
+begin
+
+abbreviation uniformity_on :: "'a set \<Rightarrow> ('a \<times> 'a) filter" where
+  "uniformity_on s \<equiv> inf uniformity (principal (s\<times>s))"
+
 end
+
+class open_uniformity = "open" + uniformity +
+  assumes open_uniformity: "\<And>U. open U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
+
+class uniform_space = open_uniformity +
+  assumes uniformity_refl: "eventually E uniformity \<Longrightarrow> E (x, x)"
+  assumes uniformity_sym: "eventually E uniformity \<Longrightarrow> eventually (\<lambda>(x, y). E (y, x)) uniformity"
+  assumes uniformity_trans: "eventually E uniformity \<Longrightarrow> \<exists>D. eventually D uniformity \<and> (\<forall>x y z. D (x, y) \<longrightarrow> D (y, z) \<longrightarrow> E (x, z))"
+begin
+
+subclass topological_space
+  proof qed (force elim: eventually_mono eventually_elim2 simp: split_beta' open_uniformity)+
+
+lemma uniformity_bot: "uniformity \<noteq> bot"
+  using uniformity_refl by auto
+
+lemma uniformity_trans':
+  "eventually E uniformity \<Longrightarrow> eventually (\<lambda>((x, y), (y', z)). y = y' \<longrightarrow> E (x, z)) (uniformity \<times>\<^sub>F uniformity)"
+  by (drule uniformity_trans) (auto simp add: eventually_prod_same)
+
+lemma uniformity_transE:
+  assumes E: "eventually E uniformity"
+  obtains D where "eventually D uniformity" "\<And>x y z. D (x, y) \<Longrightarrow> D (y, z) \<Longrightarrow> E (x, z)"
+  using uniformity_trans[OF E] by auto
+
+lemma eventually_nhds_uniformity:
+  "eventually P (nhds x) \<longleftrightarrow> eventually (\<lambda>(x', y). x' = x \<longrightarrow> P y) uniformity" (is "_ \<longleftrightarrow> ?N P x")
+  unfolding eventually_nhds
+proof safe
+  assume *: "?N P x"
+  { fix x assume "?N P x"
+    then guess D by (rule uniformity_transE) note D = this
+    from D(1) have "?N (?N P) x"
+      by eventually_elim (insert D, force elim: eventually_mono split: prod.split) }
+  then have "open {x. ?N P x}"
+    by (simp add: open_uniformity)
+  then show "\<exists>S. open S \<and> x \<in> S \<and> (\<forall>x\<in>S. P x)"
+    by (intro exI[of _ "{x. ?N P x}"]) (auto dest: uniformity_refl simp: *)
+qed (force simp add: open_uniformity elim: eventually_mono)
+
+subsubsection \<open>Totally bounded sets\<close>
+
+definition totally_bounded :: "'a set \<Rightarrow> bool" where
+  "totally_bounded S \<longleftrightarrow>
+    (\<forall>E. eventually E uniformity \<longrightarrow> (\<exists>X. finite X \<and> (\<forall>s\<in>S. \<exists>x\<in>X. E (x, s))))"
+
+lemma totally_bounded_empty[iff]: "totally_bounded {}"
+  by (auto simp add: totally_bounded_def)
+
+lemma totally_bounded_subset: "totally_bounded S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> totally_bounded T"
+  by (force simp add: totally_bounded_def)
+
+lemma totally_bounded_Union[intro]: 
+  assumes M: "finite M" "\<And>S. S \<in> M \<Longrightarrow> totally_bounded S" shows "totally_bounded (\<Union>M)"
+  unfolding totally_bounded_def
+proof safe
+  fix E assume "eventually E uniformity"
+  with M obtain X where "\<forall>S\<in>M. finite (X S) \<and> (\<forall>s\<in>S. \<exists>x\<in>X S. E (x, s))"
+    by (metis totally_bounded_def)
+  with `finite M` show "\<exists>X. finite X \<and> (\<forall>s\<in>\<Union>M. \<exists>x\<in>X. E (x, s))"
+    by (intro exI[of _ "\<Union>S\<in>M. X S"]) force
+qed
+
+subsubsection \<open>Cauchy filter\<close>
+
+definition cauchy_filter :: "'a filter \<Rightarrow> bool" where
+  "cauchy_filter F \<longleftrightarrow> F \<times>\<^sub>F F \<le> uniformity"
+
+definition Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
+  Cauchy_uniform: "Cauchy X = cauchy_filter (filtermap X sequentially)"
+
+lemma Cauchy_uniform_iff:
+  "Cauchy X \<longleftrightarrow> (\<forall>P. eventually P uniformity \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)))"
+  unfolding Cauchy_uniform cauchy_filter_def le_filter_def eventually_prod_same
+    eventually_filtermap eventually_sequentially
+proof safe
+  let ?U = "\<lambda>P. eventually P uniformity"
+  { fix P assume "?U P" "\<forall>P. ?U P \<longrightarrow> (\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y)))"
+    then obtain Q N where "\<And>n. n \<ge> N \<Longrightarrow> Q (X n)" "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> P (x, y)"
+      by metis
+    then show "\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m)"
+      by blast }
+  { fix P assume "?U P" and P: "\<forall>P. ?U P \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. \<forall>m\<ge>N. P (X n, X m))"
+    then obtain Q where "?U Q" and Q: "\<And>x y z. Q (x, y) \<Longrightarrow> Q (y, z) \<Longrightarrow> P (x, z)"
+      by (auto elim: uniformity_transE)
+    then have "?U (\<lambda>x. Q x \<and> (\<lambda>(x, y). Q (y, x)) x)"
+      unfolding eventually_conj_iff by (simp add: uniformity_sym)
+    from P[rule_format, OF this]
+    obtain N where N: "\<And>n m. n \<ge> N \<Longrightarrow> m \<ge> N \<Longrightarrow> Q (X n, X m) \<and> Q (X m, X n)"
+      by auto
+    show "\<exists>Q. (\<exists>N. \<forall>n\<ge>N. Q (X n)) \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
+    proof (safe intro!: exI[of _ "\<lambda>x. \<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)"] exI[of _ N] N)
+      fix x y assume "\<forall>n\<ge>N. Q (x, X n) \<and> Q (X n, x)" "\<forall>n\<ge>N. Q (y, X n) \<and> Q (X n, y)"
+      then have "Q (x, X N)" "Q (X N, y)" by auto
+      then show "P (x, y)"
+        by (rule Q)
+    qed }
+qed
+
+lemma nhds_imp_cauchy_filter:
+  assumes *: "F \<le> nhds x" shows "cauchy_filter F"
+proof -
+  have "F \<times>\<^sub>F F \<le> nhds x \<times>\<^sub>F nhds x"
+    by (intro prod_filter_mono *)
+  also have "\<dots> \<le> uniformity"
+    unfolding le_filter_def eventually_nhds_uniformity eventually_prod_same
+  proof safe
+    fix P assume "eventually P uniformity"
+    then guess Ql by (rule uniformity_transE) note Ql = this
+    moreover note Ql(1)[THEN uniformity_sym]
+    ultimately show "\<exists>Q. eventually (\<lambda>(x', y). x' = x \<longrightarrow> Q y) uniformity \<and> (\<forall>x y. Q x \<longrightarrow> Q y \<longrightarrow> P (x, y))"
+      by (rule_tac exI[of _ "\<lambda>y. Ql (y, x) \<and> Ql (x, y)"]) (fastforce elim: eventually_elim2)
+  qed
+  finally show ?thesis
+    by (simp add: cauchy_filter_def)
+qed
+
+lemma LIMSEQ_imp_Cauchy: "X \<longlonglongrightarrow> x \<Longrightarrow> Cauchy X"
+  unfolding Cauchy_uniform filterlim_def by (intro nhds_imp_cauchy_filter)
+
+lemma Cauchy_subseq_Cauchy: assumes "Cauchy X" "subseq f" shows "Cauchy (X \<circ> f)"
+  unfolding Cauchy_uniform comp_def filtermap_filtermap[symmetric] cauchy_filter_def
+  by (rule order_trans[OF _ \<open>Cauchy X\<close>[unfolded Cauchy_uniform cauchy_filter_def]])
+     (intro prod_filter_mono filtermap_mono filterlim_subseq[OF \<open>subseq f\<close>, unfolded filterlim_def])
+
+lemma convergent_Cauchy: "convergent X \<Longrightarrow> Cauchy X"
+  unfolding convergent_def by (erule exE, erule LIMSEQ_imp_Cauchy)
+
+definition complete :: "'a set \<Rightarrow> bool" where
+  complete_uniform: "complete S \<longleftrightarrow> (\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
+
+end
+
+subsubsection \<open>Uniformly continuous functions\<close>
+
+definition uniformly_continuous_on :: "'a set \<Rightarrow> ('a::uniform_space \<Rightarrow> 'b::uniform_space) \<Rightarrow> bool" where
+  uniformly_continuous_on_uniformity: "uniformly_continuous_on s f \<longleftrightarrow> 
+    (LIM (x, y) (uniformity_on s). (f x, f y) :> uniformity)"
+
+lemma uniformly_continuous_onD:
+  "uniformly_continuous_on s f \<Longrightarrow> eventually E uniformity
+    \<Longrightarrow> eventually (\<lambda>(x, y). x \<in> s \<longrightarrow> y \<in> s \<longrightarrow> E (f x, f y)) uniformity"
+  by (simp add: uniformly_continuous_on_uniformity filterlim_iff eventually_inf_principal split_beta' mem_Times_iff imp_conjL)
+
+lemma uniformly_continuous_on_const[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. c)"
+  by (auto simp: uniformly_continuous_on_uniformity filterlim_iff uniformity_refl)
+
+lemma uniformly_continuous_on_id[continuous_intros]: "uniformly_continuous_on s (\<lambda>x. x)"
+  by (auto simp: uniformly_continuous_on_uniformity filterlim_def)
+
+lemma uniformly_continuous_on_compose[continuous_intros]:
+  "uniformly_continuous_on s g \<Longrightarrow> uniformly_continuous_on (g`s) f \<Longrightarrow> uniformly_continuous_on s (\<lambda>x. f (g x))"
+  using filterlim_compose[of "\<lambda>(x, y). (f x, f y)" uniformity "uniformity_on (g`s)"  "\<lambda>(x, y). (g x, g y)" "uniformity_on s"]
+  by (simp add: split_beta' uniformly_continuous_on_uniformity filterlim_inf filterlim_principal eventually_inf_principal mem_Times_iff)
+
+lemma uniformly_continuous_imp_continuous: assumes f: "uniformly_continuous_on s f" shows "continuous_on s f"
+  by (auto simp: filterlim_iff eventually_at_filter eventually_nhds_uniformity continuous_on_def
+           elim: eventually_mono dest!: uniformly_continuous_onD[OF f])
+
+end