diff --git a/src/HOL/Examples/Gauss_Numbers.thy b/src/HOL/Examples/Gauss_Numbers.thy
--- a/src/HOL/Examples/Gauss_Numbers.thy
+++ b/src/HOL/Examples/Gauss_Numbers.thy
@@ -1,405 +1,405 @@
 (*   Author:      Florian Haftmann, TU Muenchen; based on existing material on complex numbers\<close>
 *)
 
 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)
 
 lemma gauss_eqI [intro?]:
   \<open>x = y\<close> if \<open>Re x = Re y\<close> \<open>Im x = Im y\<close>
   by (rule gauss.expand) (use that in simp)
 
 lemma gauss_eq_iff:
   \<open>x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y\<close>
   by (auto intro: gauss_eqI)
 
 
 subsection \<open>Basic arithmetic\<close>
 
 instantiation gauss :: comm_ring_1
 begin
 
 primcorec zero_gauss :: \<open>gauss\<close>
   where
     \<open>Re 0 = 0\<close>
   | \<open>Im 0 = 0\<close>
 
 primcorec one_gauss :: \<open>gauss\<close>
   where
     \<open>Re 1 = 1\<close>
   | \<open>Im 1 = 0\<close>
 
 primcorec plus_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (x + y) = Re x + Re y\<close>
   | \<open>Im (x + y) = Im x + Im y\<close>
 
 primcorec uminus_gauss :: \<open>gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (- x) = - Re x\<close>
   | \<open>Im (- x) = - Im x\<close>
 
 primcorec minus_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (x - y) = Re x - Re y\<close>
   | \<open>Im (x - y) = Im x - Im y\<close>
 
 primcorec times_gauss :: \<open>gauss \<Rightarrow> gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (x * y) = Re x * Re y - Im x * Im y\<close>
   | \<open>Im (x * y) = Re x * Im y + Im x * Re y\<close>
 
 instance
   by standard (simp_all add: gauss_eq_iff algebra_simps)
 
 end
 
 lemma of_nat_gauss:
   \<open>of_nat n = Gauss (int n) 0\<close>
   by (induction n) (simp_all add: gauss_eq_iff)
 
 lemma numeral_gauss:
   \<open>numeral n = Gauss (numeral n) 0\<close>
 proof -
   have \<open>numeral n = (of_nat (numeral n) :: gauss)\<close>
     by simp
   also have \<open>\<dots> = Gauss (of_nat (numeral n)) 0\<close>
     by (simp add: of_nat_gauss)
   finally show ?thesis
     by simp
 qed
 
 lemma of_int_gauss:
   \<open>of_int k = Gauss k 0\<close>
   by (simp add: gauss_eq_iff of_int_of_nat of_nat_gauss)
 
 lemma conversion_simps [simp]:
   \<open>Re (numeral m) = numeral m\<close>
   \<open>Im (numeral m) = 0\<close>
   \<open>Re (of_nat n) = int n\<close>
   \<open>Im (of_nat n) = 0\<close>
   \<open>Re (of_int k) = k\<close>
   \<open>Im (of_int k) = 0\<close>
   by (simp_all add: numeral_gauss of_nat_gauss of_int_gauss)
 
 lemma gauss_eq_0:
   \<open>z = 0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0\<close>
   by (simp add: gauss_eq_iff sum_power2_eq_zero_iff)
 
 lemma gauss_neq_0:
   \<open>z \<noteq> 0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0\<close>
   by (simp add: gauss_eq_0 sum_power2_ge_zero less_le)
 
 lemma Re_sum [simp]:
   \<open>Re (sum f s) = (\<Sum>x\<in>s. Re (f x))\<close>
   by (induct s rule: infinite_finite_induct) auto
 
 lemma Im_sum [simp]:
   \<open>Im (sum f s) = (\<Sum>x\<in>s. Im (f x))\<close>
   by (induct s rule: infinite_finite_induct) auto
 
 instance gauss :: idom
 proof
   fix x y :: gauss
   assume \<open>x \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
   then show \<open>x * y \<noteq> 0\<close>
     by (simp_all add: gauss_eq_iff)
       (smt (verit, best) mult_eq_0_iff mult_neg_neg mult_neg_pos mult_pos_neg mult_pos_pos)
 qed
 
 
 
 subsection \<open>The Gauss Number $i$\<close>
 
 primcorec imaginary_unit :: gauss  (\<open>\<i>\<close>)
   where
     \<open>Re \<i> = 0\<close>
   | \<open>Im \<i> = 1\<close>
 
 lemma Gauss_eq:
   \<open>Gauss a b = of_int a + \<i> * of_int b\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_eq:
   \<open>a = of_int (Re a) + \<i> * of_int (Im a)\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_i_not_zero [simp]:
   \<open>\<i> \<noteq> 0\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_i_not_one [simp]:
   \<open>\<i> \<noteq> 1\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_i_not_numeral [simp]:
   \<open>\<i> \<noteq> numeral n\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_i_not_neg_numeral [simp]:
   \<open>\<i> \<noteq> - numeral n\<close>
   by (simp add: gauss_eq_iff)
 
 lemma i_mult_i_eq [simp]:
   \<open>\<i> * \<i> = - 1\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_i_mult_minus [simp]:
   \<open>\<i> * (\<i> * x) = - x\<close>
   by (simp flip: mult.assoc)
 
 lemma i_squared [simp]:
   \<open>\<i>\<^sup>2 = - 1\<close>
   by (simp add: power2_eq_square)
 
 lemma i_even_power [simp]:
   \<open>\<i> ^ (n * 2) = (- 1) ^ n\<close>
   unfolding mult.commute [of n] power_mult by simp
 
 lemma Re_i_times [simp]:
   \<open>Re (\<i> * z) = - Im z\<close>
   by simp
 
 lemma Im_i_times [simp]:
   \<open>Im (\<i> * z) = Re z\<close>
   by simp
 
 lemma i_times_eq_iff:
   \<open>\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)\<close>
   by auto
 
 lemma is_unit_i [simp]:
   \<open>\<i> dvd 1\<close>
   by (rule dvdI [of _ _ \<open>- \<i>\<close>]) simp
 
 lemma gauss_numeral [code_post]:
   \<open>Gauss 0 0 = 0\<close>
   \<open>Gauss 1 0 = 1\<close>
   \<open>Gauss (- 1) 0 = - 1\<close>
   \<open>Gauss (numeral n) 0 = numeral n\<close>
   \<open>Gauss (- numeral n) 0 = - numeral n\<close>
   \<open>Gauss 0 1 = \<i>\<close>
   \<open>Gauss 0 (- 1) = - \<i>\<close>
   \<open>Gauss 0 (numeral n) = numeral n * \<i>\<close>
   \<open>Gauss 0 (- numeral n) = - numeral n * \<i>\<close>
   \<open>Gauss 1 1 = 1 + \<i>\<close>
   \<open>Gauss (- 1) 1 = - 1 + \<i>\<close>
   \<open>Gauss (numeral n) 1 = numeral n + \<i>\<close>
   \<open>Gauss (- numeral n) 1 = - numeral n + \<i>\<close>
   \<open>Gauss 1 (- 1) = 1 - \<i>\<close>
   \<open>Gauss 1 (numeral n) = 1 + numeral n * \<i>\<close>
   \<open>Gauss 1 (- numeral n) = 1 - numeral n * \<i>\<close>
   \<open>Gauss (- 1) (- 1) = - 1 - \<i>\<close>
   \<open>Gauss (numeral n) (- 1) = numeral n - \<i>\<close>
   \<open>Gauss (- numeral n) (- 1) = - numeral n - \<i>\<close>
   \<open>Gauss (- 1) (numeral n) = - 1 + numeral n * \<i>\<close>
   \<open>Gauss (- 1) (- numeral n) = - 1 - numeral n * \<i>\<close>
   \<open>Gauss (numeral m) (numeral n) = numeral m + numeral n * \<i>\<close>
   \<open>Gauss (- numeral m) (numeral n) = - numeral m + numeral n * \<i>\<close>
   \<open>Gauss (numeral m) (- numeral n) = numeral m - numeral n * \<i>\<close>
   \<open>Gauss (- numeral m) (- numeral n) = - numeral m - numeral n * \<i>\<close>
   by (simp_all add: gauss_eq_iff)
 
 
 subsection \<open>Gauss Conjugation\<close>
 
 primcorec cnj :: \<open>gauss \<Rightarrow> gauss\<close>
   where
     \<open>Re (cnj z) = Re z\<close>
   | \<open>Im (cnj z) = - Im z\<close>
 
 lemma gauss_cnj_cancel_iff [simp]:
   \<open>cnj x = cnj y \<longleftrightarrow> x = y\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_cnj [simp]:
   \<open>cnj (cnj z) = z\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_zero [simp]:
   \<open>cnj 0 = 0\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_zero_iff [iff]:
   \<open>cnj z = 0 \<longleftrightarrow> z = 0\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_one_iff [simp]:
   \<open>cnj z = 1 \<longleftrightarrow> z = 1\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_add [simp]:
   \<open>cnj (x + y) = cnj x + cnj y\<close>
   by (simp add: gauss_eq_iff)
 
 lemma cnj_sum [simp]:
   \<open>cnj (sum f s) = (\<Sum>x\<in>s. cnj (f x))\<close>
   by (induct s rule: infinite_finite_induct) auto
 
 lemma gauss_cnj_diff [simp]:
   \<open>cnj (x - y) = cnj x - cnj y\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_minus [simp]:
   \<open>cnj (- x) = - cnj x\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_one [simp]:
   \<open>cnj 1 = 1\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_mult [simp]:
   \<open>cnj (x * y) = cnj x * cnj y\<close>
   by (simp add: gauss_eq_iff)
 
 lemma cnj_prod [simp]:
   \<open>cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))\<close>
   by (induct s rule: infinite_finite_induct) auto
 
 lemma gauss_cnj_power [simp]:
   \<open>cnj (x ^ n) = cnj x ^ n\<close>
   by (induct n) simp_all
 
 lemma gauss_cnj_numeral [simp]:
   \<open>cnj (numeral w) = numeral w\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_of_nat [simp]:
   \<open>cnj (of_nat n) = of_nat n\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_of_int [simp]:
   \<open>cnj (of_int z) = of_int z\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_cnj_i [simp]:
   \<open>cnj \<i> = - \<i>\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_add_cnj:
   \<open>z + cnj z = of_int (2 * Re z)\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_diff_cnj:
   \<open>z - cnj z = of_int (2 * Im z) * \<i>\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_mult_cnj:
   \<open>z * cnj z = of_int ((Re z)\<^sup>2 + (Im z)\<^sup>2)\<close>
   by (simp add: gauss_eq_iff power2_eq_square)
 
 lemma cnj_add_mult_eq_Re:
   \<open>z * cnj w + cnj z * w = of_int (2 * Re (z * cnj w))\<close>
   by (simp add: gauss_eq_iff)
 
 lemma gauss_In_mult_cnj_zero [simp]:
   \<open>Im (z * cnj z) = 0\<close>
   by simp
 
 
 subsection \<open>Algebraic division\<close>
 
 instantiation gauss :: idom_modulo
 begin
 
 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
   show \<open>x div 0 = 0\<close>
     by (simp add: gauss_eq_iff)
   show \<open>x * y div y = x\<close> if \<open>y \<noteq> 0\<close>
   proof -
     define Y where \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
     moreover have \<open>Y > 0\<close>
       using that by (simp add: gauss_eq_0 less_le Y_def)
     have *: \<open>Im y * (Im y * Re x) + Re x * (Re y * Re y) = Re x * Y\<close>
       \<open>Im x * (Im y * Im y) + Im x * (Re y * Re y) = Im x * Y\<close>
       \<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)
 qed
 
 end
 
 instantiation gauss :: euclidean_ring
 begin
 
 definition euclidean_size_gauss :: \<open>gauss \<Rightarrow> nat\<close>
   where \<open>euclidean_size x = nat ((Re x)\<^sup>2 + (Im x)\<^sup>2)\<close>
 
 instance proof
   show \<open>euclidean_size (0::gauss) = 0\<close>
     by (simp add: euclidean_size_gauss_def)
   show \<open>euclidean_size (x mod y) < euclidean_size y\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
   proof-
     define X and Y and R and I
       where \<open>X = (Re x)\<^sup>2 + (Im x)\<^sup>2\<close> and \<open>Y = (Re y)\<^sup>2 + (Im y)\<^sup>2\<close>
         and \<open>R = Re x * Re y + Im x * Im y\<close> and \<open>I = Im x * Re y - Re x * Im y\<close>
     with that have \<open>0 < Y\<close> and rhs: \<open>int (euclidean_size y) = Y\<close>
       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> .
     with \<open>Y > 0\<close> have \<open>?lhs < Y\<close>
       by (simp add: power2_eq_square)
     then have \<open>int (euclidean_size (x mod y)) < int (euclidean_size y)\<close>
       by (simp only: lhs rhs)
     then show ?thesis
       by simp
   qed
   show \<open>euclidean_size x \<le> euclidean_size (x * y)\<close> if \<open>y \<noteq> 0\<close> for x y :: gauss
   proof -
     from that have \<open>euclidean_size y > 0\<close>
       by (simp add: euclidean_size_gauss_def gauss_neq_0)
     then have \<open>euclidean_size x \<le> euclidean_size x * euclidean_size y\<close>
       by simp
     also have \<open>\<dots> = nat (((Re x)\<^sup>2 + (Im x)\<^sup>2) * ((Re y)\<^sup>2 + (Im y)\<^sup>2))\<close>
       by (simp add: euclidean_size_gauss_def nat_mult_distrib)
     also have \<open>\<dots> = euclidean_size (x * y)\<close>
       by (simp add: euclidean_size_gauss_def eq_nat_nat_iff) (simp add: algebra_simps power2_eq_square)
     finally show ?thesis .
   qed
 qed
 
 end
 
 end
diff --git a/src/HOL/Library/Rounded_Division.thy b/src/HOL/Library/Centered_Division.thy
rename from src/HOL/Library/Rounded_Division.thy
rename to src/HOL/Library/Centered_Division.thy
--- a/src/HOL/Library/Rounded_Division.thy
+++ b/src/HOL/Library/Centered_Division.thy
@@ -1,178 +1,178 @@
 (*  Author:  Florian Haftmann, TU Muenchen
 *)
 
-section \<open>Rounded division: modulus centered towards zero.\<close>
+section \<open>Division with modulus centered towards zero.\<close>
 
-theory Rounded_Division
+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 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 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 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>
+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 rmod 5 \<in> {-2, -1, 0, 1, 2}\<close> by (auto simp add: rounded_modulo_def)}
+  \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_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)
+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_rmod [no_vars]} is the key to generalize
-  rounded division to arbitrary structures satisfying \<^class>\<open>ring_bit_operations\<close>,
+  \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 rdiv_mult_rmod_eq:
-  \<open>k rdiv l * l + k rmod l = k\<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: rounded_divide_def rounded_modulo_def algebra_simps *)
+    by (simp add: centered_divide_def centered_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 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 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 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 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 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 rdiv_abs_eq:
-  \<open>k rdiv \<bar>l\<bar> = sgn l * (k rdiv l)\<close>
-  by (simp add: rounded_divide_def)
+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 rmod_abs_eq [simp]:
-  \<open>k rmod \<bar>l\<bar> = k rmod l\<close>
-  by (simp add: rounded_modulo_def)
+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 nonzero_mult_rdiv_cancel_right:
-  \<open>k * l rdiv l = k\<close> if \<open>l \<noteq> 0\<close>
+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> rdiv l = k\<close>
-    using that by (simp add: rounded_divide_def)
+  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 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 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 rmod_self_eq [simp]:
-  \<open>k rmod k = 0\<close>
+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: rounded_modulo_def algebra_simps)
+    by (simp add: centered_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 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 rmod_less_equal_divisor:
-  \<open>k rmod l \<le> \<bar>l\<bar> div 2\<close> if \<open>l \<noteq> 0\<close>
+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 rmod_less_divisor [of l k]
-  have \<open>k rmod l < \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
+  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_rmod':
-  \<open>\<bar>l\<bar> div 2 - \<bar>l\<bar> \<le> k rmod l\<close> if \<open>l \<noteq> 0\<close>
+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: rounded_modulo_def)
+    by (simp_all add: centered_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 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_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)
+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 --git a/src/HOL/Library/Library.thy b/src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy
+++ b/src/HOL/Library/Library.thy
@@ -1,101 +1,101 @@
 (*<*)
 theory Library
 imports
   AList
   Adhoc_Overloading
   BNF_Axiomatization
   BNF_Corec
   Bourbaki_Witt_Fixpoint
+  Centered_Division
   Char_ord
   Code_Cardinality
   Code_Lazy
   Code_Test
   Combine_PER
   Complete_Partial_Order2
   Conditional_Parametricity
   Confluence
   Confluent_Quotient
   Countable
   Countable_Complete_Lattices
   Countable_Set_Type
   Debug
   Diagonal_Subsequence
   Discrete
   Disjoint_Sets
   Disjoint_FSets
   Dlist
   Dual_Ordered_Lattice
   Equipollence
   Extended
   Extended_Nat
   Extended_Nonnegative_Real
   Extended_Real
   Finite_Map
   Float
   FSet
   FuncSet
   Function_Division
   Fun_Lexorder
   Going_To_Filter
   Groups_Big_Fun
   Indicator_Function
   Infinite_Set
   Interval
   Interval_Float
   IArray
   Landau_Symbols
   Lattice_Algebras
   Lattice_Constructions
   Linear_Temporal_Logic_on_Streams
   ListVector
   Lub_Glb
   Mapping
   Monad_Syntax
   More_List
   Multiset_Order
   NList
   Nonpos_Ints
   Numeral_Type
   Omega_Words_Fun
   Open_State_Syntax
   Option_ord
   Order_Continuity
   Parallel
   Pattern_Aliases
   Periodic_Fun
   Poly_Mapping
   Power_By_Squaring
   Preorder
   Product_Plus
   Quadratic_Discriminant
   Quotient_List
   Quotient_Option
   Quotient_Product
   Quotient_Set
   Quotient_Sum
   Quotient_Syntax
   Quotient_Type
   Ramsey
   Reflection
   Rewrite
-  Rounded_Division
   Saturated
   Set_Algebras
   Set_Idioms
   Signed_Division
   State_Monad
   Stream
   Sorting_Algorithms
   Sublist
   Sum_of_Squares
   Transitive_Closure_Table
   Tree_Multiset
   Tree_Real
   Type_Length
   Uprod
   While_Combinator
   Word
   Z2
 begin
 end
 (*>*)
diff --git a/src/HOL/ex/Note_on_signed_division_on_words.thy b/src/HOL/ex/Note_on_signed_division_on_words.thy
--- a/src/HOL/ex/Note_on_signed_division_on_words.thy
+++ b/src/HOL/ex/Note_on_signed_division_on_words.thy
@@ -1,50 +1,50 @@
 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
 
 context semiring_bit_operations
 begin
 
 lemma take_bit_Suc_from_most:
   \<open>take_bit (Suc n) a = 2 ^ n * of_bool (bit a n) OR take_bit n a\<close>
   by (rule bit_eqI) (auto simp add: bit_simps less_Suc_eq)
 
 end
 
 context ring_bit_operations
 begin
 
 lemma signed_take_bit_exp_eq_int:
   \<open>signed_take_bit m (2 ^ n) =
     (if n < m then 2 ^ n else if n = m then - (2 ^ n) else 0)\<close>
   by (rule bit_eqI) (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
 
 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
 
 end