# Theory Centered_Division

(*  Author:  Florian Haftmann, TU Muenchen
*)

section ‹Division with modulus centered towards zero.›

theory Centered_Division
imports Main
begin

lemma off_iff_abs_mod_2_eq_one:
‹odd l ⟷ ¦l¦ mod 2 = 1› for l :: int
by (simp flip: odd_iff_mod_2_eq_one)

text ‹
\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}.
›

definition centered_divide :: ‹int ⇒ int ⇒ int›  (infixl ‹cdiv› 70)
where ‹k cdiv l = sgn l * ((k + ¦l¦ div 2) div ¦l¦)›

definition centered_modulo :: ‹int ⇒ int ⇒ int›  (infixl ‹cmod› 70)
where ‹k cmod l = (k + ¦l¦ div 2) mod ¦l¦ - ¦l¦ div 2›

text ‹
\noindent Example: @{lemma ‹k cmod 5 ∈ {-2, -1, 0, 1, 2}› by (auto simp add: centered_modulo_def)}
›

lemma signed_take_bit_eq_cmod:
‹signed_take_bit n k = k cmod (2 ^ Suc n)›
by (simp only: centered_modulo_def power_abs abs_numeral flip: take_bit_eq_mod)

text ‹
\noindent Property @{thm signed_take_bit_eq_cmod [no_vars]} is the key to generalize
centered division to arbitrary structures satisfying \<^class>‹ring_bit_operations›,
but so far it is not clear what practical relevance that would have.
›

lemma cdiv_mult_cmod_eq:
‹k cdiv l * l + k cmod l = k›
proof -
have *: ‹l * (sgn l * j) = ¦l¦ * j› for j
show ?thesis
by (simp add: centered_divide_def centered_modulo_def algebra_simps *)
qed

lemma mult_cdiv_cmod_eq:
‹l * (k cdiv l) + k cmod l = k›
using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)

lemma cmod_cdiv_mult_eq:
‹k cmod l + k cdiv l * l = k›
using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)

lemma cmod_mult_cdiv_eq:
‹k cmod l + l * (k cdiv l) = k›
using cdiv_mult_cmod_eq [of k l] by (simp add: ac_simps)

lemma minus_cdiv_mult_eq_cmod:
‹k - k cdiv l * l = k cmod l›
by (rule add_implies_diff [symmetric]) (fact cmod_cdiv_mult_eq)

lemma minus_mult_cdiv_eq_cmod:
‹k - l * (k cdiv l) = k cmod l›
by (rule add_implies_diff [symmetric]) (fact cmod_mult_cdiv_eq)

lemma minus_cmod_eq_cdiv_mult:
‹k - k cmod l = k cdiv l * l›
by (rule add_implies_diff [symmetric]) (fact cdiv_mult_cmod_eq)

lemma minus_cmod_eq_mult_cdiv:
‹k - k cmod l = l * (k cdiv l)›
by (rule add_implies_diff [symmetric]) (fact mult_cdiv_cmod_eq)

lemma cdiv_0_eq [simp]:
‹k cdiv 0 = 0›

lemma cmod_0_eq [simp]:
‹k cmod 0 = k›

lemma cdiv_1_eq [simp]:
‹k cdiv 1 = k›

lemma cmod_1_eq [simp]:
‹k cmod 1 = 0›

lemma zero_cdiv_eq [simp]:
‹0 cdiv k = 0›
by (auto simp add: centered_divide_def not_less zdiv_eq_0_iff)

lemma zero_cmod_eq [simp]:
‹0 cmod k = 0›
by (auto simp add: centered_modulo_def not_less zmod_trivial_iff)

lemma cdiv_minus_eq:
‹k cdiv - l = - (k cdiv l)›

lemma cmod_minus_eq [simp]:
‹k cmod - l = k cmod l›

lemma cdiv_abs_eq:
‹k cdiv ¦l¦ = sgn l * (k cdiv l)›

lemma cmod_abs_eq [simp]:
‹k cmod ¦l¦ = k cmod l›

lemma nonzero_mult_cdiv_cancel_right:
‹k * l cdiv l = k› if ‹l ≠ 0›
proof -
have ‹sgn l * k * ¦l¦ cdiv l = k›
using that by (simp add: centered_divide_def)
with that show ?thesis
qed

lemma cdiv_self_eq [simp]:
‹k cdiv k = 1› if ‹k ≠ 0›
using that nonzero_mult_cdiv_cancel_right [of k 1] by simp

lemma cmod_self_eq [simp]:
‹k cmod k = 0›
proof -
have ‹(sgn k * ¦k¦ + ¦k¦ div 2) mod ¦k¦ = ¦k¦ div 2›
also have ‹sgn k * ¦k¦ = k›
finally show ?thesis
qed

lemma cmod_less_divisor:
‹k cmod l < ¦l¦ - ¦l¦ div 2› if ‹l ≠ 0›
using that pos_mod_bound [of ‹¦l¦›] by (simp add: centered_modulo_def)

lemma cmod_less_equal_divisor:
‹k cmod l ≤ ¦l¦ div 2› if ‹l ≠ 0›
proof -
from that cmod_less_divisor [of l k]
have ‹k cmod l < ¦l¦ - ¦l¦ div 2›
by simp
also have ‹¦l¦ - ¦l¦ div 2 = ¦l¦ div 2 + of_bool (odd l)›
by auto
finally show ?thesis
by (cases ‹even l›) simp_all
qed

lemma divisor_less_equal_cmod':
‹¦l¦ div 2 - ¦l¦ ≤ k cmod l› if ‹l ≠ 0›
proof -
have ‹0 ≤ (k + ¦l¦ div 2) mod ¦l¦›
using that pos_mod_sign [of ‹¦l¦›] by simp
then show ?thesis
qed

lemma divisor_less_equal_cmod:
‹- (¦l¦ div 2) ≤ k cmod l› if ‹l ≠ 0›
using that divisor_less_equal_cmod' [of l k]