# HG changeset patch
# User haftmann
# Date 1681928490 0
# Node ID 0e054e6e7f5ee11601c1709d8329aaae33f7edc8
# Parent  2cd00c4054abca45dab94bf891f421ab547f913e
clarified terminology

diff -r 2cd00c4054ab -r 0e054e6e7f5e src/HOL/Examples/Gauss_Numbers.thy
--- a/src/HOL/Examples/Gauss_Numbers.thy	Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/Examples/Gauss_Numbers.thy	Wed Apr 19 18:21:30 2023 +0000
@@ -4,7 +4,7 @@
 section \<open>Gauss Numbers: integral gauss numbers\<close>
 
 theory Gauss_Numbers
-  imports "HOL-Library.Rounded_Division"
+  imports "HOL-Library.Centered_Division"
 begin
 
 codatatype gauss = Gauss (Re: int) (Im: int)
@@ -308,17 +308,17 @@
 
 primcorec divide_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
-    \<open>Re (x div y) = (Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
-  | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
+    \<open>Re (x div y) = (Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
+  | \<open>Im (x div y) = (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2)\<close>
 
 primcorec modulo_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (x mod y) = Re x -
-      ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y -
-       (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y)\<close>
+      ((Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y -
+       (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y)\<close>
   | \<open>Im (x mod y) = Im x -
-      ((Re x * Re y + Im x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y +
-       (Im x * Re y - Re x * Im y) rdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y)\<close>
+      ((Re x * Re y + Im x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Im y +
+       (Im x * Re y - Re x * Im y) cdiv ((Re y)\<^sup>2 + (Im y)\<^sup>2) * Re y)\<close>
 
 instance proof
   fix x y :: gauss
@@ -334,7 +334,7 @@
       \<open>(Im y)\<^sup>2 + (Re y)\<^sup>2 = Y\<close>
       by (simp_all add: power2_eq_square algebra_simps Y_def)
     from \<open>Y > 0\<close> show ?thesis
-      by (simp add: gauss_eq_iff algebra_simps) (simp add: * nonzero_mult_rdiv_cancel_right)
+      by (simp add: gauss_eq_iff algebra_simps) (simp add: * nonzero_mult_cdiv_cancel_right)
   qed
   show \<open>x div y * y + x mod y = x\<close>
     by (simp add: gauss_eq_iff)
@@ -360,22 +360,22 @@
       by (simp_all add: gauss_neq_0 euclidean_size_gauss_def)
     have \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>
       by (simp add: R_def I_def X_def Y_def power2_eq_square algebra_simps)
-    let ?lhs = \<open>X - I * (I rdiv Y) - R * (R rdiv Y)
-        - I rdiv Y * (I rmod Y) - R rdiv Y * (R rmod Y)\<close>
-    have \<open>?lhs = X + Y * (R rdiv Y) * (R rdiv Y) + Y * (I rdiv Y) * (I rdiv Y)
-        - 2 * (R rdiv Y * R + I rdiv Y * I)\<close>
-      by (simp flip: minus_rmod_eq_mult_rdiv add: algebra_simps)
+    let ?lhs = \<open>X - I * (I cdiv Y) - R * (R cdiv Y)
+        - I cdiv Y * (I cmod Y) - R cdiv Y * (R cmod Y)\<close>
+    have \<open>?lhs = X + Y * (R cdiv Y) * (R cdiv Y) + Y * (I cdiv Y) * (I cdiv Y)
+        - 2 * (R cdiv Y * R + I cdiv Y * I)\<close>
+      by (simp flip: minus_cmod_eq_mult_cdiv add: algebra_simps)
     also have \<open>\<dots> = (Re (x mod y))\<^sup>2 + (Im (x mod y))\<^sup>2\<close>
       by (simp add: X_def Y_def R_def I_def algebra_simps power2_eq_square)
     finally have lhs: \<open>int (euclidean_size (x mod y)) = ?lhs\<close>
       by (simp add: euclidean_size_gauss_def)
-    have \<open>?lhs * Y = (I rmod Y)\<^sup>2 + (R rmod Y)\<^sup>2\<close>
+    have \<open>?lhs * Y = (I cmod Y)\<^sup>2 + (R cmod Y)\<^sup>2\<close>
       apply (simp add: algebra_simps power2_eq_square \<open>X * Y = R\<^sup>2 + I\<^sup>2\<close>)
-      apply (simp flip: mult.assoc add.assoc minus_rmod_eq_mult_rdiv)
+      apply (simp flip: mult.assoc add.assoc minus_cmod_eq_mult_cdiv)
       apply (simp add: algebra_simps)
       done
     also have \<open>\<dots> \<le> (Y div 2)\<^sup>2 + (Y div 2)\<^sup>2\<close>
-      by (rule add_mono) (use \<open>Y > 0\<close> abs_rmod_less_equal [of Y] in \<open>simp_all add: power2_le_iff_abs_le\<close>)
+      by (rule add_mono) (use \<open>Y > 0\<close> abs_cmod_less_equal [of Y] in \<open>simp_all add: power2_le_iff_abs_le\<close>)
     also have \<open>\<dots> < Y\<^sup>2\<close>
       using \<open>Y > 0\<close> by (cases \<open>Y = 1\<close>) (simp_all add: power2_eq_square mult_le_less_imp_less flip: mult.assoc)
     finally have \<open>?lhs * Y < Y\<^sup>2\<close> .
diff -r 2cd00c4054ab -r 0e054e6e7f5e src/HOL/Library/Centered_Division.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Centered_Division.thy	Wed Apr 19 18:21:30 2023 +0000
@@ -0,0 +1,178 @@
+(*  Author:  Florian Haftmann, TU Muenchen
+*)
+
+section \<open>Division with modulus centered towards zero.\<close>
+
+theory Centered_Division
+  imports Main
+begin
+
+lemma off_iff_abs_mod_2_eq_one:
+  \<open>odd l \<longleftrightarrow> \<bar>l\<bar> mod 2 = 1\<close> for l :: int
+  by (simp flip: odd_iff_mod_2_eq_one)
+
+text \<open>
+  \noindent The following specification of division on integers centers
+  the modulus around zero.  This is useful e.g.~to define division
+  on Gauss numbers.
+  N.b.: This is not mentioned \cite{leijen01}.
+\<close>
+
+definition centered_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>cdiv\<close> 70)
+  where \<open>k cdiv l = sgn l * ((k + \<bar>l\<bar> div 2) div \<bar>l\<bar>)\<close>
+
+definition centered_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>cmod\<close> 70)
+  where \<open>k cmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+
+text \<open>
+  \noindent Example: @{lemma \<open>k cmod 5 \<in> {-2, -1, 0, 1, 2}\<close> by (auto simp add: centered_modulo_def)}
+\<close>
+
+lemma signed_take_bit_eq_cmod:
+  \<open>signed_take_bit n k = k cmod (2 ^ Suc n)\<close>
+  by (simp only: centered_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)
+    (simp add: signed_take_bit_eq_take_bit_shift)
+
+text \<open>
+  \noindent Property @{thm signed_take_bit_eq_cmod [no_vars]} is the key to generalize
+  centered division to arbitrary structures satisfying \<^class>\<open>ring_bit_operations\<close>,
+  but so far it is not clear what practical relevance that would have.
+\<close>
+
+lemma cdiv_mult_cmod_eq:
+  \<open>k cdiv l * l + k cmod l = k\<close>
+proof -
+  have *: \<open>l * (sgn l * j) = \<bar>l\<bar> * j\<close> for j
+    by (simp add: ac_simps abs_sgn)
+  show ?thesis
+    by (simp add: centered_divide_def centered_modulo_def algebra_simps *)
+qed
+
+lemma mult_cdiv_cmod_eq:
+  \<open>l * (k cdiv l) + k cmod l = k\<close>
+  using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma cmod_cdiv_mult_eq:
+  \<open>k cmod l + k cdiv l * l = k\<close>
+  using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma cmod_mult_cdiv_eq:
+  \<open>k cmod l + l * (k cdiv l) = k\<close>
+  using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)
+
+lemma minus_cdiv_mult_eq_cmod:
+  \<open>k - k cdiv l * l = k cmod l\<close>
+  by (rule add_implies_diff [symmetric]) (fact cmod_cdiv_mult_eq)
+
+lemma minus_mult_cdiv_eq_cmod:
+  \<open>k - l * (k cdiv l) = k cmod l\<close>
+  by (rule add_implies_diff [symmetric]) (fact cmod_mult_cdiv_eq)
+
+lemma minus_cmod_eq_cdiv_mult:
+  \<open>k - k cmod l = k cdiv l * l\<close>
+  by (rule add_implies_diff [symmetric]) (fact cdiv_mult_cmod_eq)
+
+lemma minus_cmod_eq_mult_cdiv:
+  \<open>k - k cmod l = l * (k cdiv l)\<close>
+  by (rule add_implies_diff [symmetric]) (fact mult_cdiv_cmod_eq)
+
+lemma cdiv_0_eq [simp]:
+  \<open>k cdiv 0 = 0\<close>
+  by (simp add: centered_divide_def)
+
+lemma cmod_0_eq [simp]:
+  \<open>k cmod 0 = k\<close>
+  by (simp add: centered_modulo_def)
+
+lemma cdiv_1_eq [simp]:
+  \<open>k cdiv 1 = k\<close>
+  by (simp add: centered_divide_def)
+
+lemma cmod_1_eq [simp]:
+  \<open>k cmod 1 = 0\<close>
+  by (simp add: centered_modulo_def)
+
+lemma zero_cdiv_eq [simp]:
+  \<open>0 cdiv k = 0\<close>
+  by (auto simp add: centered_divide_def not_less zdiv_eq_0_iff)
+
+lemma zero_cmod_eq [simp]:
+  \<open>0 cmod k = 0\<close>
+  by (auto simp add: centered_modulo_def not_less zmod_trivial_iff)
+
+lemma cdiv_minus_eq:
+  \<open>k cdiv - l = - (k cdiv l)\<close>
+  by (simp add: centered_divide_def)
+
+lemma cmod_minus_eq [simp]:
+  \<open>k cmod - l = k cmod l\<close>
+  by (simp add: centered_modulo_def)
+
+lemma cdiv_abs_eq:
+  \<open>k cdiv \<bar>l\<bar> = sgn l * (k cdiv l)\<close>
+  by (simp add: centered_divide_def)
+
+lemma cmod_abs_eq [simp]:
+  \<open>k cmod \<bar>l\<bar> = k cmod l\<close>
+  by (simp add: centered_modulo_def)
+
+lemma nonzero_mult_cdiv_cancel_right:
+  \<open>k * l cdiv l = k\<close> if \<open>l \<noteq> 0\<close>
+proof -
+  have \<open>sgn l * k * \<bar>l\<bar> cdiv l = k\<close>
+    using that by (simp add: centered_divide_def)
+  with that show ?thesis
+    by (simp add: ac_simps abs_sgn)
+qed
+
+lemma cdiv_self_eq [simp]:
+  \<open>k cdiv k = 1\<close> if \<open>k \<noteq> 0\<close>
+  using that nonzero_mult_cdiv_cancel_right [of k 1] by simp
+
+lemma cmod_self_eq [simp]:
+  \<open>k cmod k = 0\<close>
+proof -
+  have \<open>(sgn k * \<bar>k\<bar> + \<bar>k\<bar> div 2) mod \<bar>k\<bar> = \<bar>k\<bar> div 2\<close>
+    by (auto simp add: zmod_trivial_iff)
+  also have \<open>sgn k * \<bar>k\<bar> = k\<close>
+    by (simp add: abs_sgn)
+  finally show ?thesis
+    by (simp add: centered_modulo_def algebra_simps)
+qed
+
+lemma cmod_less_divisor:
+  \<open>k cmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+  using that pos_mod_bound [of \<open>\<bar>l\<bar>\<close>] by (simp add: centered_modulo_def)
+
+lemma cmod_less_equal_divisor:
+  \<open>k cmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+proof -
+  from that cmod_less_divisor [of l k]
+  have \<open>k cmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+    by simp
+  also have \<open>\<bar>l\<bar> - \<bar>l\<bar> div 2 = \<bar>l\<bar> div 2 + of_bool (odd l)\<close>
+    by auto
+  finally show ?thesis
+    by (cases \<open>even l\<close>) simp_all
+qed
+
+lemma divisor_less_equal_cmod':
+  \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k cmod l\<close> if \<open>l \<noteq> 0\<close>
+proof -
+  have \<open>0 \<le> (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar>\<close>
+    using that pos_mod_sign [of \<open>\<bar>l\<bar>\<close>] by simp
+  then show ?thesis
+    by (simp_all add: centered_modulo_def)
+qed
+
+lemma divisor_less_equal_cmod:
+  \<open>- (\<bar>l\<bar> div 2) \<le> k cmod l\<close> if \<open>l \<noteq> 0\<close>
+  using that divisor_less_equal_cmod' [of l k]
+  by (simp add: centered_modulo_def)
+
+lemma abs_cmod_less_equal:
+  \<open>\<bar>k cmod l\<bar> \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+  using that divisor_less_equal_cmod [of l k]
+  by (simp add: abs_le_iff cmod_less_equal_divisor)
+
+end
diff -r 2cd00c4054ab -r 0e054e6e7f5e src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/Library/Library.thy	Wed Apr 19 18:21:30 2023 +0000
@@ -6,6 +6,7 @@
   BNF_Axiomatization
   BNF_Corec
   Bourbaki_Witt_Fixpoint
+  Centered_Division
   Char_ord
   Code_Cardinality
   Code_Lazy
@@ -78,7 +79,6 @@
   Ramsey
   Reflection
   Rewrite
-  Rounded_Division
   Saturated
   Set_Algebras
   Set_Idioms
diff -r 2cd00c4054ab -r 0e054e6e7f5e src/HOL/Library/Rounded_Division.thy
--- a/src/HOL/Library/Rounded_Division.thy	Wed Apr 19 14:48:43 2023 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,178 +0,0 @@
-(*  Author:  Florian Haftmann, TU Muenchen
-*)
-
-section \<open>Rounded division: modulus centered towards zero.\<close>
-
-theory Rounded_Division
-  imports Main
-begin
-
-lemma off_iff_abs_mod_2_eq_one:
-  \<open>odd l \<longleftrightarrow> \<bar>l\<bar> mod 2 = 1\<close> for l :: int
-  by (simp flip: odd_iff_mod_2_eq_one)
-
-text \<open>
-  \noindent The following specification of division on integers centers
-  the modulus around zero.  This is useful e.g.~to define division
-  on Gauss numbers.
-  N.b.: This is not mentioned \cite{leijen01}.
-\<close>
-
-definition rounded_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rdiv\<close> 70)
-  where \<open>k rdiv l = sgn l * ((k + \<bar>l\<bar> div 2) div \<bar>l\<bar>)\<close>
-
-definition rounded_modulo :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rmod\<close> 70)
-  where \<open>k rmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
-
-text \<open>
-  \noindent Example: @{lemma \<open>k rmod 5 \<in> {-2, -1, 0, 1, 2}\<close> by (auto simp add: rounded_modulo_def)}
-\<close>
-
-lemma signed_take_bit_eq_rmod:
-  \<open>signed_take_bit n k = k rmod (2 ^ Suc n)\<close>
-  by (simp only: rounded_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)
-    (simp add: signed_take_bit_eq_take_bit_shift)
-
-text \<open>
-  \noindent Property @{thm signed_take_bit_eq_rmod [no_vars]} is the key to generalize
-  rounded division to arbitrary structures satisfying \<^class>\<open>ring_bit_operations\<close>,
-  but so far it is not clear what practical relevance that would have.
-\<close>
-
-lemma rdiv_mult_rmod_eq:
-  \<open>k rdiv l * l + k rmod l = k\<close>
-proof -
-  have *: \<open>l * (sgn l * j) = \<bar>l\<bar> * j\<close> for j
-    by (simp add: ac_simps abs_sgn)
-  show ?thesis
-    by (simp add: rounded_divide_def rounded_modulo_def algebra_simps *)
-qed
-
-lemma mult_rdiv_rmod_eq:
-  \<open>l * (k rdiv l) + k rmod l = k\<close>
-  using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma rmod_rdiv_mult_eq:
-  \<open>k rmod l + k rdiv l * l = k\<close>
-  using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma rmod_mult_rdiv_eq:
-  \<open>k rmod l + l * (k rdiv l) = k\<close>
-  using rdiv_mult_rmod_eq [of k l] by (simp add: ac_simps)
-
-lemma minus_rdiv_mult_eq_rmod:
-  \<open>k - k rdiv l * l = k rmod l\<close>
-  by (rule add_implies_diff [symmetric]) (fact rmod_rdiv_mult_eq)
-
-lemma minus_mult_rdiv_eq_rmod:
-  \<open>k - l * (k rdiv l) = k rmod l\<close>
-  by (rule add_implies_diff [symmetric]) (fact rmod_mult_rdiv_eq)
-
-lemma minus_rmod_eq_rdiv_mult:
-  \<open>k - k rmod l = k rdiv l * l\<close>
-  by (rule add_implies_diff [symmetric]) (fact rdiv_mult_rmod_eq)
-
-lemma minus_rmod_eq_mult_rdiv:
-  \<open>k - k rmod l = l * (k rdiv l)\<close>
-  by (rule add_implies_diff [symmetric]) (fact mult_rdiv_rmod_eq)
-
-lemma rdiv_0_eq [simp]:
-  \<open>k rdiv 0 = 0\<close>
-  by (simp add: rounded_divide_def)
-
-lemma rmod_0_eq [simp]:
-  \<open>k rmod 0 = k\<close>
-  by (simp add: rounded_modulo_def)
-
-lemma rdiv_1_eq [simp]:
-  \<open>k rdiv 1 = k\<close>
-  by (simp add: rounded_divide_def)
-
-lemma rmod_1_eq [simp]:
-  \<open>k rmod 1 = 0\<close>
-  by (simp add: rounded_modulo_def)
-
-lemma zero_rdiv_eq [simp]:
-  \<open>0 rdiv k = 0\<close>
-  by (auto simp add: rounded_divide_def not_less zdiv_eq_0_iff)
-
-lemma zero_rmod_eq [simp]:
-  \<open>0 rmod k = 0\<close>
-  by (auto simp add: rounded_modulo_def not_less zmod_trivial_iff)
-
-lemma rdiv_minus_eq:
-  \<open>k rdiv - l = - (k rdiv l)\<close>
-  by (simp add: rounded_divide_def)
-
-lemma rmod_minus_eq [simp]:
-  \<open>k rmod - l = k rmod l\<close>
-  by (simp add: rounded_modulo_def)
-
-lemma rdiv_abs_eq:
-  \<open>k rdiv \<bar>l\<bar> = sgn l * (k rdiv l)\<close>
-  by (simp add: rounded_divide_def)
-
-lemma rmod_abs_eq [simp]:
-  \<open>k rmod \<bar>l\<bar> = k rmod l\<close>
-  by (simp add: rounded_modulo_def)
-
-lemma nonzero_mult_rdiv_cancel_right:
-  \<open>k * l rdiv l = k\<close> if \<open>l \<noteq> 0\<close>
-proof -
-  have \<open>sgn l * k * \<bar>l\<bar> rdiv l = k\<close>
-    using that by (simp add: rounded_divide_def)
-  with that show ?thesis
-    by (simp add: ac_simps abs_sgn)
-qed
-
-lemma rdiv_self_eq [simp]:
-  \<open>k rdiv k = 1\<close> if \<open>k \<noteq> 0\<close>
-  using that nonzero_mult_rdiv_cancel_right [of k 1] by simp
-
-lemma rmod_self_eq [simp]:
-  \<open>k rmod k = 0\<close>
-proof -
-  have \<open>(sgn k * \<bar>k\<bar> + \<bar>k\<bar> div 2) mod \<bar>k\<bar> = \<bar>k\<bar> div 2\<close>
-    by (auto simp add: zmod_trivial_iff)
-  also have \<open>sgn k * \<bar>k\<bar> = k\<close>
-    by (simp add: abs_sgn)
-  finally show ?thesis
-    by (simp add: rounded_modulo_def algebra_simps)
-qed
-
-lemma rmod_less_divisor:
-  \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
-  using that pos_mod_bound [of \<open>\<bar>l\<bar>\<close>] by (simp add: rounded_modulo_def)
-
-lemma rmod_less_equal_divisor:
-  \<open>k rmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
-proof -
-  from that rmod_less_divisor [of l k]
-  have \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
-    by simp
-  also have \<open>\<bar>l\<bar> - \<bar>l\<bar> div 2 = \<bar>l\<bar> div 2 + of_bool (odd l)\<close>
-    by auto
-  finally show ?thesis
-    by (cases \<open>even l\<close>) simp_all
-qed
-
-lemma divisor_less_equal_rmod':
-  \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
-proof -
-  have \<open>0 \<le> (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar>\<close>
-    using that pos_mod_sign [of \<open>\<bar>l\<bar>\<close>] by simp
-  then show ?thesis
-    by (simp_all add: rounded_modulo_def)
-qed
-
-lemma divisor_less_equal_rmod:
-  \<open>- (\<bar>l\<bar> div 2) \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
-  using that divisor_less_equal_rmod' [of l k]
-  by (simp add: rounded_modulo_def)
-
-lemma abs_rmod_less_equal:
-  \<open>\<bar>k rmod l\<bar> \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
-  using that divisor_less_equal_rmod [of l k]
-  by (simp add: abs_le_iff rmod_less_equal_divisor)
-
-end
diff -r 2cd00c4054ab -r 0e054e6e7f5e src/HOL/ex/Note_on_signed_division_on_words.thy
--- a/src/HOL/ex/Note_on_signed_division_on_words.thy	Wed Apr 19 14:48:43 2023 +0200
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy	Wed Apr 19 18:21:30 2023 +0000
@@ -1,5 +1,5 @@
 theory Note_on_signed_division_on_words
-  imports "HOL-Library.Word" "HOL-Library.Rounded_Division"
+  imports "HOL-Library.Word" "HOL-Library.Centered_Division"
 begin
 
 unbundle bit_operations_syntax
@@ -24,26 +24,26 @@
 end
 
 lift_definition signed_divide_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wdiv\<close> 70)
-  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cdiv signed_take_bit (LENGTH('a) - Suc 0) b\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
 
 lift_definition signed_modulo_word :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>  (infixl \<open>wmod\<close> 70)
-  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a rmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
+  is \<open>\<lambda>a b. signed_take_bit (LENGTH('a) - Suc 0) a cmod signed_take_bit (LENGTH('a) - Suc 0) b\<close>
   by (simp flip: signed_take_bit_decr_length_iff)
 
 lemma signed_take_bit_eq_wmod:
   \<open>signed_take_bit n w = w wmod (2 ^ Suc n)\<close>
 proof (transfer fixing: n)
   show \<open>take_bit LENGTH('a) (signed_take_bit n (take_bit LENGTH('a) k)) =
-    take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k rmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
+    take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - Suc 0) k cmod signed_take_bit (LENGTH('a) - Suc 0) (2 ^ Suc n))\<close> for k :: int
   proof (cases \<open>LENGTH('a) = Suc (Suc n)\<close>)
     case True
     then show ?thesis
-      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit rmod_minus_eq flip: power_Suc signed_take_bit_eq_rmod)
+      by (simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit cmod_minus_eq flip: power_Suc signed_take_bit_eq_cmod)
   next
     case False
     then show ?thesis
-      by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_rmod)
+      by (auto simp add: signed_take_bit_exp_eq_int signed_take_bit_take_bit take_bit_signed_take_bit simp flip: power_Suc signed_take_bit_eq_cmod)
   qed
 qed