Theory Signed_Division

(*  Author:  Stefan Berghofer et al.
*)

section ‹Signed division: negative results rounded towards zero rather than minus infinity.›

theory Signed_Division
  imports Main
begin

class signed_divide =
  fixes signed_divide :: 'a  'a  'a (infixl sdiv 70)

class signed_modulo =
  fixes signed_modulo :: 'a  'a  'a (infixl smod 70)

class signed_division = comm_semiring_1_cancel + signed_divide + signed_modulo +
  assumes sdiv_mult_smod_eq: a sdiv b * b + a smod b = a
begin

lemma mult_sdiv_smod_eq:
  b * (a sdiv b) + a smod b = a
  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)

lemma smod_sdiv_mult_eq:
  a smod b + a sdiv b * b = a
  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)

lemma smod_mult_sdiv_eq:
  a smod b + b * (a sdiv b) = a
  using sdiv_mult_smod_eq [of a b] by (simp add: ac_simps)

lemma minus_sdiv_mult_eq_smod:
  a - a sdiv b * b = a smod b
  by (rule add_implies_diff [symmetric]) (fact smod_sdiv_mult_eq)

lemma minus_mult_sdiv_eq_smod:
  a - b * (a sdiv b) = a smod b
  by (rule add_implies_diff [symmetric]) (fact smod_mult_sdiv_eq)

lemma minus_smod_eq_sdiv_mult:
  a - a smod b = a sdiv b * b
  by (rule add_implies_diff [symmetric]) (fact sdiv_mult_smod_eq)

lemma minus_smod_eq_mult_sdiv:
  a - a smod b = b * (a sdiv b)
  by (rule add_implies_diff [symmetric]) (fact mult_sdiv_smod_eq)

end

text ‹
  \noindent The following specification of division is named ``T-division'' in cite"leijen01".
  It is motivated by ISO C99, which in turn adopted the typical behavior of
  hardware modern in the beginning of the 1990ies; but note ISO C99 describes
  the instance on machine words, not mathematical integers.
›

instantiation int :: signed_division
begin

definition signed_divide_int :: int  int  int
  where k sdiv l = sgn k * sgn l * (¦k¦ div ¦l¦) for k l :: int

definition signed_modulo_int :: int  int  int
  where k smod l = sgn k * (¦k¦ mod ¦l¦) for k l :: int

instance by standard
  (simp add: signed_divide_int_def signed_modulo_int_def div_abs_eq mod_abs_eq algebra_simps)

end

lemma divide_int_eq_signed_divide_int:
  k div l = k sdiv l - of_bool (l  0  sgn k  sgn l  ¬ l dvd k)
  for k l :: int
  by (simp add: div_eq_div_abs [of k l] signed_divide_int_def)

lemma signed_divide_int_eq_divide_int:
  k sdiv l = k div l + of_bool (l  0  sgn k  sgn l  ¬ l dvd k)
  for k l :: int
  by (simp add: divide_int_eq_signed_divide_int)

lemma modulo_int_eq_signed_modulo_int:
  k mod l = k smod l + l * of_bool (sgn k  sgn l  ¬ l dvd k)
  for k l :: int
  by (simp add: mod_eq_mod_abs [of k l] signed_modulo_int_def)

lemma signed_modulo_int_eq_modulo_int:
  k smod l = k mod l - l * of_bool (sgn k  sgn l  ¬ l dvd k)
  for k l :: int
  by (simp add: modulo_int_eq_signed_modulo_int)

lemma sdiv_int_div_0:
  "(x :: int) sdiv 0 = 0"
  by (clarsimp simp: signed_divide_int_def)

lemma sdiv_int_0_div [simp]:
  "0 sdiv (x :: int) = 0"
  by (clarsimp simp: signed_divide_int_def)

lemma smod_int_alt_def:
     "(a::int) smod b = sgn (a) * (abs a mod abs b)"
  by (fact signed_modulo_int_def)

lemma int_sdiv_simps [simp]:
    "(a :: int) sdiv 1 = a"
    "(a :: int) sdiv 0 = 0"
    "(a :: int) sdiv -1 = -a"
  apply (auto simp: signed_divide_int_def sgn_if)
  done

lemma smod_int_mod_0 [simp]:
  "x smod (0 :: int) = x"
  by (clarsimp simp: signed_modulo_int_def abs_mult_sgn ac_simps)

lemma smod_int_0_mod [simp]:
  "0 smod (x :: int) = 0"
  by (clarsimp simp: smod_int_alt_def)

lemma sgn_sdiv_eq_sgn_mult:
  "a sdiv b  0  sgn ((a :: int) sdiv b) = sgn (a * b)"
  by (auto simp: signed_divide_int_def sgn_div_eq_sgn_mult sgn_mult)

lemma int_sdiv_same_is_1 [simp]:
    "a  0  ((a :: int) sdiv b = a) = (b = 1)"
  apply (rule iffI)
   apply (clarsimp simp: signed_divide_int_def)
   apply (subgoal_tac "b > 0")
    apply (case_tac "a > 0")
     apply (clarsimp simp: sgn_if)
  apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
  using int_div_less_self [of a b] apply linarith
    apply (metis add.commute add.inverse_inverse group_cancel.rule0 int_div_less_self linorder_neqE_linordered_idom neg_0_le_iff_le not_less verit_comp_simplify1(1) zless_imp_add1_zle)
   apply (metis div_minus_right neg_imp_zdiv_neg_iff neg_le_0_iff_le not_less order.not_eq_order_implies_strict)
  apply (metis abs_le_zero_iff abs_of_nonneg neg_imp_zdiv_nonneg_iff order.not_eq_order_implies_strict)
  done

lemma int_sdiv_negated_is_minus1 [simp]:
    "a  0  ((a :: int) sdiv b = - a) = (b = -1)"
  apply (clarsimp simp: signed_divide_int_def)
  apply (rule iffI)
   apply (subgoal_tac "b < 0")
    apply (case_tac "a > 0")
     apply (clarsimp simp: sgn_if algebra_split_simps not_less)
     apply (case_tac "sgn (a * b) = -1")
      apply (simp_all add: not_less algebra_split_simps sgn_if split: if_splits)
     apply (metis add.inverse_inverse int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
    apply (metis add.inverse_inverse div_minus_right int_div_less_self int_one_le_iff_zero_less less_le neg_0_less_iff_less)
   apply (metis less_le neg_less_0_iff_less not_less pos_imp_zdiv_neg_iff)
  apply (metis div_minus_right dual_order.eq_iff neg_imp_zdiv_nonneg_iff neg_less_0_iff_less)
  done

lemma sdiv_int_range:
  a sdiv b  {- ¦a¦..¦a¦} for a b :: int
  using zdiv_mono2 [of ¦a¦ 1 ¦b¦]
  by (cases b = 0; cases sgn b = sgn a)
     (auto simp add: signed_divide_int_def pos_imp_zdiv_nonneg_iff
     dest!: sgn_not_eq_imp intro: order_trans [of _ 0])

lemma smod_int_range:
  a smod b  {- ¦b¦ + 1..¦b¦ - 1}
  if b  0 for a b :: int
proof -
  define m n where m = nat ¦a¦ n = nat ¦b¦
  then have ¦a¦ = int m ¦b¦ = int n
    by simp_all
  with that have n > 0
    by simp
  with signed_modulo_int_def [of a b] ¦a¦ = int m ¦b¦ = int n
  show ?thesis
    by (auto simp add: sgn_if diff_le_eq int_one_le_iff_zero_less simp flip: of_nat_mod of_nat_diff)
qed

lemma smod_int_compares:
   " 0  a; 0 < b   (a :: int) smod b < b"
   " 0  a; 0 < b   0  (a :: int) smod b"
   " a  0; 0 < b   -b < (a :: int) smod b"
   " a  0; 0 < b   (a :: int) smod b  0"
   " 0  a; b < 0   (a :: int) smod b < - b"
   " 0  a; b < 0   0  (a :: int) smod b"
   " a  0; b < 0   (a :: int) smod b  0"
   " a  0; b < 0   b  (a :: int) smod b"
  apply (insert smod_int_range [where a=a and b=b])
  apply (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
  done

lemma smod_mod_positive:
    " 0  (a :: int); 0  b   a smod b = a mod b"
  by (clarsimp simp: smod_int_alt_def zsgn_def)

lemma minus_sdiv_eq [simp]:
  - k sdiv l = - (k sdiv l) for k l :: int
  by (simp add: signed_divide_int_def)

lemma sdiv_minus_eq [simp]:
  k sdiv - l = - (k sdiv l) for k l :: int
  by (simp add: signed_divide_int_def)

lemma sdiv_int_numeral_numeral [simp]:
  numeral m sdiv numeral n = numeral m div (numeral n :: int)
  by (simp add: signed_divide_int_def)

lemma minus_smod_eq [simp]:
  - k smod l = - (k smod l) for k l :: int
  by (simp add: smod_int_alt_def)

lemma smod_minus_eq [simp]:
  k smod - l = k smod l for k l :: int
  by (simp add: smod_int_alt_def)

lemma smod_int_numeral_numeral [simp]:
  numeral m smod numeral n = numeral m mod (numeral n :: int)
  by (simp add: smod_int_alt_def) 

end