New proofs also some slightly faster existing proofs

--- a/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Mon Oct 02 11:28:23 2023 +0200
+++ b/src/HOL/Analysis/Abstract_Metric_Spaces.thy	Tue Oct 03 15:01:54 2023 +0100
@@ -2562,12 +2562,12 @@
 lemma derived_set_of_infinite_mball:
   "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mball x e)}"
   unfolding derived_set_of_infinite_openin_metric
-  by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
 
 lemma derived_set_of_infinite_mcball:
   "mtopology derived_set_of S = {x \<in> M. \<forall>e>0. infinite(S \<inter> mcball x e)}"
   unfolding derived_set_of_infinite_openin_metric
-  by (meson centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
+  by (metis (no_types, opaque_lifting) centre_in_mball_iff openin_mball derived_set_of_infinite_1 derived_set_of_infinite_2)
 
 end
 
@@ -2671,7 +2671,8 @@
 proof -
   have "\<And>x. x \<in> topspace X \<Longrightarrow> \<exists>l. limitin mtopology (\<lambda>n. f n x) l sequentially"
     using \<open>mcomplete\<close> [unfolded mcomplete, rule_format] assms
-    by (smt (verit) contf continuous_map_def eventually_mono topspace_mtopology Pi_iff)
+    unfolding continuous_map_def Pi_iff topspace_mtopology
+    by (smt (verit, del_insts) eventually_mono)
   then obtain g where g: "\<And>x. x \<in> topspace X \<Longrightarrow> limitin mtopology (\<lambda>n. f n x) (g x) sequentially"
     by metis
   show thesis
@@ -3992,7 +3993,8 @@
 lemma uniformly_continuous_map_compose:
   assumes f: "uniformly_continuous_map m1 m2 f" and g: "uniformly_continuous_map m2 m3 g"
   shows "uniformly_continuous_map m1 m3 (g \<circ> f)"
-  by (smt (verit, ccfv_threshold) comp_apply f g Pi_iff uniformly_continuous_map_def)
+  using f g unfolding uniformly_continuous_map_def comp_apply Pi_iff
+  by metis
 
 lemma uniformly_continuous_map_real_const [simp]:
    "uniformly_continuous_map m euclidean_metric (\<lambda>x. c)"
@@ -5109,7 +5111,6 @@
     by (metis (full_types) completely_metrizable_space_def)
 qed
 
-
 proposition metrizable_space_product_topology:
   "metrizable_space (product_topology X I) \<longleftrightarrow>
         (product_topology X I) = trivial_topology \<or>

--- a/src/HOL/Archimedean_Field.thy	Mon Oct 02 11:28:23 2023 +0200
+++ b/src/HOL/Archimedean_Field.thy	Tue Oct 03 15:01:54 2023 +0100
@@ -719,6 +719,57 @@
   by (simp add: frac_def)
 
 
+subsection \<open>Fractional part arithmetic\<close>
+text \<open>Many thanks to Stepan Holub\<close>
+
+lemma frac_non_zero: "frac x \<noteq> 0 \<Longrightarrow> frac (-x) =  1 - frac x"
+  using frac_eq_0_iff frac_neg by metis
+
+lemma frac_add_simps [simp]: 
+   "frac (frac a + b) = frac (a + b)"
+   "frac (a + frac b) = frac (a + b)"      
+  by (simp_all add: frac_add)
+
+lemma frac_neg_frac:  "frac (- frac x) = frac (-x)"
+  unfolding frac_neg frac_frac by force
+
+lemma frac_diff_simp: "frac (y - frac x) = frac (y - x)"
+    unfolding diff_conv_add_uminus frac_add frac_neg_frac..
+
+lemma frac_diff: "frac (a - b) = frac (frac a + (- frac b))" 
+  unfolding frac_add_simps(1) 
+  unfolding ab_group_add_class.ab_diff_conv_add_uminus[symmetric] frac_diff_simp..
+
+lemma frac_diff_pos: "frac x \<le> frac y \<Longrightarrow> frac (y - x) = frac y - frac x"
+  unfolding diff_conv_add_uminus frac_add frac_neg
+  using frac_lt_1 by force 
+   
+lemma frac_diff_neg: assumes "frac y < frac x" 
+  shows "frac (y - x) = frac y + 1 - frac x"
+proof-
+  have "x \<notin> \<int>"
+    unfolding frac_gt_0_iff[symmetric]
+    using assms frac_ge_0[of y] by order
+  have "frac y + (1 + - frac x) < 1"
+    using frac_lt_1[of x] assms by fastforce
+  show ?thesis
+    unfolding diff_conv_add_uminus frac_add frac_neg 
+    if_not_P[OF \<open>x \<notin> \<int>\<close>] if_P[OF \<open>frac y + (1 + - frac x) < 1\<close>]
+    by simp
+qed
+
+lemma frac_diff_eq: assumes "frac y = frac x" 
+  shows "frac (y - x) = 0"
+  by (simp add: assms frac_diff_pos)
+
+lemma frac_diff_zero: assumes "frac (x - y) = 0"
+  shows "frac x = frac y"
+  using frac_add_simps(1)[of "x - y" y, symmetric]
+  unfolding assms add.group_left_neutral diff_add_cancel.
+
+lemma frac_neg_eq_iff: "frac (-x) = frac (-y) \<longleftrightarrow> frac x = frac y"
+  using add.inverse_inverse frac_neg_frac by metis
+
 subsection \<open>Rounding to the nearest integer\<close>
 
 definition round :: "'a::floor_ceiling \<Rightarrow> int"