Theory HOL-Library.Signed_Division
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"
by (auto simp: signed_divide_int_def sgn_if)
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]:
assumes "a ≠ 0"
shows "((a :: int) sdiv b = a) = (b = 1)"
proof -
have "b = 1" if "a sdiv b = a"
proof -
have "b>0"
by (smt (verit, ccfv_threshold) assms mult_cancel_left2 sgn_if sgn_mult
sgn_sdiv_eq_sgn_mult that)
then show ?thesis
by (smt (verit) assms dvd_eq_mod_eq_0 int_div_less_self of_bool_eq(1,2) sgn_if
signed_divide_int_eq_divide_int that zdiv_zminus1_eq_if)
qed
then show ?thesis
by auto
qed
lemma int_sdiv_negated_is_minus1 [simp]:
"a ≠ 0 ⟹ ((a :: int) sdiv b = - a) = (b = -1)"
using int_sdiv_same_is_1 [of _ "-b"]
using signed_divide_int_def by fastforce
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"
using smod_int_range [where a=a and b=b]
by (auto simp: add1_zle_eq smod_int_alt_def sgn_if)
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