diff -r 6c8c980e777a -r 8c093a4b8ccf src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Thu Feb 09 13:36:53 2023 +0000
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Feb 09 15:36:06 2023 +0000
@@ -131,7 +131,10 @@
 instance..
 end
 
-instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space begin
+subsubsection \<open>Uniform spaces\<close>
+
+instantiation\<^marker>\<open>tag unimportant\<close> prod :: (uniform_space, uniform_space) uniform_space 
+begin
 instance 
 proof standard
   fix U :: \<open>('a \<times> 'b) set\<close>
@@ -216,6 +219,133 @@
 qed
 end
 
+
+lemma (in uniform_space) nhds_eq_comap_uniformity: "nhds x = filtercomap (\<lambda>y. (x, y)) uniformity"
+proof -
+  have *: "eventually P (filtercomap (\<lambda>y. (x, y)) F) \<longleftrightarrow>
+           eventually (\<lambda>z. fst z = x \<longrightarrow> P (snd z)) F" for P :: "'a \<Rightarrow> bool" and F
+    unfolding eventually_filtercomap  
+    by (smt (verit) eventually_elim2 fst_conv prod.collapse snd_conv)
+  thus ?thesis
+    unfolding filter_eq_iff
+    by (subst *) (auto simp: eventually_nhds_uniformity case_prod_unfold)
+qed
+
+lemma uniformity_of_uniform_continuous_invariant:
+  fixes f :: "'a :: uniform_space \<Rightarrow> 'a \<Rightarrow> 'a"
+  assumes "filterlim (\<lambda>((a,b),(c,d)). (f a c, f b d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+  assumes "eventually P uniformity"
+  obtains Q where "eventually Q uniformity" "\<And>a b c. Q (a, b) \<Longrightarrow> P (f a c, f b c)"
+  using eventually_compose_filterlim[OF assms(2,1)] uniformity_refl
+    by (fastforce simp: case_prod_unfold eventually_filtercomap eventually_prod_same)
+
+class uniform_topological_monoid_add = topological_monoid_add + uniform_space +
+  assumes uniformly_continuous_add':
+    "filterlim (\<lambda>((a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+
+lemma uniformly_continuous_add:
+  "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_monoid_add,y). x + y)"
+  using uniformly_continuous_add'[where ?'a = 'a]
+  by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+lemma filterlim_fst: "filterlim fst F (F \<times>\<^sub>F G)"
+  by (simp add: filterlim_def filtermap_fst_prod_filter)
+
+lemma filterlim_snd: "filterlim snd G (F \<times>\<^sub>F G)"
+  by (simp add: filterlim_def filtermap_snd_prod_filter)
+
+class uniform_topological_group_add = topological_group_add + uniform_topological_monoid_add +
+  assumes uniformly_continuous_uminus': "filterlim (\<lambda>(a, b). (-a, -b)) uniformity uniformity"
+begin
+
+lemma uniformly_continuous_minus':
+  "filterlim (\<lambda>((a,b), (c,d)). (a - c, b - d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+proof -
+  have "filterlim ((\<lambda>((a,b), (c,d)). (a + c, b + d)) \<circ> (\<lambda>((a,b), (c,d)). ((a, b), (-c, -d))))
+          uniformity (uniformity \<times>\<^sub>F uniformity)"
+    unfolding o_def using uniformly_continuous_uminus'
+    by (intro filterlim_compose[OF uniformly_continuous_add'])
+       (auto simp: case_prod_unfold intro!: filterlim_Pair
+          filterlim_fst filterlim_compose[OF _ filterlim_snd])
+  thus ?thesis
+    by (simp add: o_def case_prod_unfold)
+qed
+
+end
+
+lemma uniformly_continuous_uminus:
+  "uniformly_continuous_on UNIV (\<lambda>x :: 'a :: uniform_topological_group_add. -x)"
+  using uniformly_continuous_uminus'[where ?'a = 'a]
+  by (simp add: uniformly_continuous_on_uniformity)
+
+lemma uniformly_continuous_minus:
+  "uniformly_continuous_on UNIV (\<lambda>(x :: 'a :: uniform_topological_group_add,y). x - y)"
+  using uniformly_continuous_minus'[where ?'a = 'a]
+  by (simp add: uniformly_continuous_on_uniformity case_prod_unfold uniformity_prod_def filterlim_filtermap)
+
+
+
+lemma real_normed_vector_is_uniform_topological_group_add [Pure.intro]:
+  "OFCLASS('a :: real_normed_vector, uniform_topological_group_add_class)"
+proof
+  show "filterlim (\<lambda>((a::'a,b), (c,d)). (a + c, b + d)) uniformity (uniformity \<times>\<^sub>F uniformity)"
+    unfolding filterlim_def le_filter_def eventually_filtermap case_prod_unfold
+  proof safe
+    fix P :: "'a \<times> 'a \<Rightarrow> bool"
+    assume "eventually P uniformity"
+    then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+      by (auto simp: eventually_uniformity_metric)
+    define Q where "Q = (\<lambda>(x::'a,y). dist x y < \<epsilon> / 2)"
+    have Q: "eventually Q uniformity"
+      unfolding eventually_uniformity_metric Q_def using \<open>\<epsilon> > 0\<close>
+      by (meson case_prodI divide_pos_pos zero_less_numeral)
+    have "P (a + c, b + d)" if "Q (a, b)" "Q (c, d)" for a b c d
+    proof -
+      have "dist (a + c) (b + d) \<le> dist a b + dist c d"
+        by (simp add: dist_norm norm_diff_triangle_ineq)
+      also have "\<dots> < \<epsilon>"
+        using that by (auto simp: Q_def)
+      finally show ?thesis
+        by (intro \<epsilon>)
+    qed
+    thus "\<forall>\<^sub>F x in uniformity \<times>\<^sub>F uniformity. P (fst (fst x) + fst (snd x), snd (fst x) + snd (snd x))"
+      unfolding eventually_prod_filter by (intro exI[of _ Q] conjI Q) auto
+  qed
+next
+  show "filterlim (\<lambda>((a::'a), b). (-a, -b)) uniformity uniformity"
+    unfolding filterlim_def le_filter_def eventually_filtermap
+  proof safe
+    fix P :: "'a \<times> 'a \<Rightarrow> bool"
+    assume "eventually P uniformity"
+    then obtain \<epsilon> where \<epsilon>: "\<epsilon> > 0" "\<And>x y. dist x y < \<epsilon> \<Longrightarrow> P (x, y)"
+      by (auto simp: eventually_uniformity_metric)
+    show "\<forall>\<^sub>F x in uniformity. P (case x of (a, b) \<Rightarrow> (- a, - b))"
+      unfolding eventually_uniformity_metric
+      by (intro exI[of _ \<epsilon>]) (auto intro!: \<epsilon> simp: dist_norm norm_minus_commute)
+  qed
+qed
+
+instance real :: uniform_topological_group_add ..
+instance complex :: uniform_topological_group_add ..
+
+lemma cauchy_seq_finset_iff_vanishing:
+  "uniformity = filtercomap (\<lambda>(x,y). y - x :: 'a :: uniform_topological_group_add) (nhds 0)"
+proof -
+  have "filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity \<le> uniformity"
+    apply (simp add: le_filter_def eventually_filtercomap)
+    using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_add']
+    by (metis diff_self eq_diff_eq)
+  moreover
+  have "uniformity \<le> filtercomap (\<lambda>x. (0, case x of (x, y) \<Rightarrow> y - (x :: 'a))) uniformity"
+    apply (simp add: le_filter_def eventually_filtercomap)
+    using uniformity_of_uniform_continuous_invariant[OF uniformly_continuous_minus']
+    by (metis (mono_tags) diff_self eventually_mono surjective_pairing)
+  ultimately show ?thesis
+    by (simp add: nhds_eq_comap_uniformity filtercomap_filtercomap)
+qed
+
+subsubsection \<open>Metric spaces\<close>
+
 instantiation\<^marker>\<open>tag unimportant\<close> prod :: (metric_space, metric_space) uniformity_dist begin
 instance
 proof
@@ -422,7 +552,7 @@
   using uniformly_continuous_on_prod_metric[of UNIV UNIV]
   by auto
 
-text \<open>This logically belong with the real vector spaces by we only have the necessary lemmas now.\<close>
+text \<open>This logically belong with the real vector spaces but we only have the necessary lemmas now.\<close>
 lemma isUCont_plus[simp]:
   shows \<open>isUCont (\<lambda>(x::'a::real_normed_vector,y). x+y)\<close>
 proof (rule isUCont_prod_metric[THEN iffD2], intro allI impI, simp)