src/HOL/Library/Rounded_Division.thy

 theory Rounded_Division
   imports Main
 begin
 
 definition rounded_divide :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>rdiv\<close> 70)
-  where \<open>k rdiv l = (k + l div 2 + of_bool (l < 0)) div l\<close>
+  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 - k rdiv l * l\<close>
+  where \<open>k rmod l = (k + \<bar>l\<bar> div 2) mod \<bar>l\<bar> - \<bar>l\<bar> div 2\<close>
 
 lemma rdiv_mult_rmod_eq:
   \<open>k rdiv l * l + k rmod l = k\<close>
-  by (simp add: rounded_divide_def rounded_modulo_def)
+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)
 

   \<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>
-  using that by (auto simp add: rounded_divide_def ac_simps)
+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>
-  by (cases \<open>k = 0\<close>) (simp_all add: rounded_modulo_def)
+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 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)
 
 end