Theory Signed_Modulo

section ‹Signed Modulo Operation›

theory Signed_Modulo
  imports 
    Berlekamp_Zassenhaus.Poly_Mod
    Sqrt_Babylonian.Sqrt_Babylonian_Auxiliary
begin

text ‹The upcoming definition of symmetric modulo 
  is different to the HOL-Library-Signed\_Division.smod, since
  here the modulus will be in range $\{-m/2,...,m/2\}$, 
  whereas there -1 symmod m = m - 1.

  The advantage of have range $\{-m/2,...,m/2\}$ is that small negative
  numbers are represented by small numbers.

  One limitation is that the symmetric modulo is only working properly,
  if the modulus is a positive number.›

definition sym_mod :: "int ⇒ int ⇒ int" (infixl ‹symmod› 70) where
  "sym_mod x y = poly_mod.inv_M y (x mod y)"

lemma sym_mod_code[code]: "sym_mod x y = (let m = x mod y
   in if m + m ≤ y then m else m - y)" 
  unfolding sym_mod_def poly_mod.inv_M_def Let_def ..

lemma sym_mod_zero[simp]: "n symmod 0 = n" "n > 0 ⟹ 0 symmod n = 0"
  unfolding sym_mod_def poly_mod.inv_M_def by auto

lemma sym_mod_range:
  ‹x symmod y ∈ {- ((y - 1) div 2) .. y div 2}› if ‹y > 0›
proof -
  from that have ‹x mod y < y›
    by (rule pos_mod_bound)
  then have ‹x mod y - y < 0›
    by simp
  moreover from that have ‹- ((y - 1) div 2) ≤ 0› ‹0 ≤ x mod y›
    by simp_all
  then have ‹- ((y - 1) div 2) ≤ x mod y›
    by (rule order_trans)
  ultimately show ?thesis
    by (auto simp add: sym_mod_def poly_mod.inv_M_def)
qed

text ‹The range is optimal in the sense that exactly y elements can be represented.›
lemma card_sym_mod_range: "y > 0 ⟹ card {- ((y - 1) div 2) .. y div 2} = y" 
  by simp

lemma sym_mod_abs: "y > 0 ⟹ ¦x symmod y¦ < y"
  "y ≥ 1 ⟹ ¦x symmod y¦ ≤ y div 2"
  using sym_mod_range[of y x] by auto

lemma sym_mod_sym_mod[simp]: "x symmod y symmod y = x symmod (y :: int)" 
  unfolding sym_mod_def using poly_mod.M_def poly_mod.M_inv_M_id by auto

lemma sym_mod_diff_eq: "(a symmod c - b symmod c) symmod c = (a - b) symmod c" 
  unfolding sym_mod_def
  by (metis mod_diff_cong mod_mod_trivial poly_mod.M_def poly_mod.M_inv_M_id)

lemma sym_mod_sym_mod_cancel: "c dvd b ⟹ a symmod b symmod c = a symmod c" 
  using mod_mod_cancel[of c b] unfolding sym_mod_def
  by (metis poly_mod.M_def poly_mod.M_inv_M_id)

lemma sym_mod_diff_right_eq: "(a - b symmod c) symmod c = (a - b) symmod c" 
  using sym_mod_diff_eq by (metis sym_mod_sym_mod)

lemma sym_mod_mult_right_eq: "a * (b symmod c) symmod c = a * b symmod c" 
  unfolding sym_mod_def by (metis poly_mod.M_def poly_mod.M_inv_M_id mod_mult_right_eq)

lemma dvd_imp_sym_mod_0 [simp]:
  "b symmod a = 0" if "a > 0" "a dvd b"
  unfolding sym_mod_def poly_mod.inv_M_def using that by simp

lemma sym_mod_0_imp_dvd [dest!]:
  "b dvd a" if "a symmod b = 0"
  using that apply (simp add: sym_mod_def poly_mod.inv_M_def not_le split: if_splits)
  using pos_mod_bound [of b a] apply auto
  done

definition sym_div :: "int ⇒ int ⇒ int" (infixl ‹symdiv› 70) where
  "sym_div x y = (let d = x div y; m = x mod y in 
       if m + m ≤ y then d else d + 1)"

lemma of_int_mod_integer: "(of_int (x mod y) :: integer) = (of_int x :: integer) mod (of_int y)" 
  using integer_of_int_eq_of_int modulo_integer.abs_eq by presburger

lemma sym_div_code[code]: 
  "sym_div x y = (let yy = integer_of_int y in 
     (case divmod_integer (integer_of_int x) yy
     of (d, m) ⇒ if m + m ≤ yy then int_of_integer d else (int_of_integer (d + 1))))"
  unfolding sym_div_def Let_def divmod_integer_def split
  apply (rule if_cong, subst of_int_le_iff[symmetric], unfold of_int_add)
  by (subst (1 2) of_int_mod_integer, auto)

lemma sym_mod_sym_div: assumes y: "y > 0" shows "x symmod y = x - sym_div x y * y"
proof -
  let ?z = "x - y * (x div y)" 
  let ?u = "y * (x div y)" 
  have "x = y * (x div y) + x mod y" using y by simp
  hence id: "x mod y = ?z" by linarith
  have "x symmod y = poly_mod.inv_M y ?z" unfolding sym_mod_def id by auto
  also have "… = (if ?z + ?z ≤ y then ?z else ?z - y)" unfolding poly_mod.inv_M_def ..
  also have "… = x - (if (x mod y) + (x mod y) ≤ y then x div y else x div y + 1) * y" 
    by (simp add: algebra_simps id)
  also have "(if (x mod y) + (x mod y) ≤ y then x div y else x div y + 1) = sym_div x y" 
    unfolding sym_div_def Let_def ..
  finally show ?thesis .
qed
  
lemma dvd_sym_div_mult_right [simp]:
  "(a symdiv b) * b = a" if "b > 0" "b dvd a"
  using sym_mod_sym_div[of b a] that by simp

lemma dvd_sym_div_mult_left [simp]:
  "b * (a symdiv b) = a" if "b > 0" "b dvd a"
  using dvd_sym_div_mult_right[OF that] by (simp add: ac_simps)


end