Theory Word_Lib.Signed_Division_Word
section ‹Signed division on word›
theory Signed_Division_Word
imports "HOL-Library.Signed_Division" "HOL-Library.Word"
begin
text ‹
The following specification of division follows ISO C99, which in turn adopted the typical
behavior of hardware modern in the beginning of the 1990ies.
The underlying integer division is named ``T-division'' in \cite{leijen01}.
›
instantiation word :: (len) signed_division
begin
lift_definition signed_divide_word :: ‹'a::len word ⇒ 'a word ⇒ 'a word›
is ‹λk l. signed_take_bit (LENGTH('a) - Suc 0) k sdiv signed_take_bit (LENGTH('a) - Suc 0) l›
by (simp flip: signed_take_bit_decr_length_iff)
lift_definition signed_modulo_word :: ‹'a::len word ⇒ 'a word ⇒ 'a word›
is ‹λk l. signed_take_bit (LENGTH('a) - Suc 0) k smod signed_take_bit (LENGTH('a) - Suc 0) l›
by (simp flip: signed_take_bit_decr_length_iff)
lemma sdiv_word_def [code]:
‹v sdiv w = word_of_int (sint v sdiv sint w)›
for v w :: ‹'a::len word›
by transfer simp
lemma smod_word_def [code]:
‹v smod w = word_of_int (sint v smod sint w)›
for v w :: ‹'a::len word›
by transfer simp
instance proof
fix v w :: ‹'a word›
have ‹sint v sdiv sint w * sint w + sint v smod sint w = sint v›
by (fact sdiv_mult_smod_eq)
then have ‹word_of_int (sint v sdiv sint w * sint w + sint v smod sint w) = (word_of_int (sint v) :: 'a word)›
by simp
then show ‹v sdiv w * w + v smod w = v›
by (simp add: sdiv_word_def smod_word_def)
qed
end
lemma sdiv_smod_id:
‹(a sdiv b) * b + (a smod b) = a›
for a b :: ‹'a::len word›
by (fact sdiv_mult_smod_eq)
lemma signed_div_arith:
"sint ((a::('a::len) word) sdiv b) = signed_take_bit (LENGTH('a) - 1) (sint a sdiv sint b)"
by (simp add: sdiv_word_def sint_sbintrunc')
lemma signed_mod_arith:
"sint ((a::('a::len) word) smod b) = signed_take_bit (LENGTH('a) - 1) (sint a smod sint b)"
by (simp add: sint_sbintrunc' smod_word_def)
lemma word_sdiv_div0 [simp]:
"(a :: ('a::len) word) sdiv 0 = 0"
by (auto simp: sdiv_word_def signed_divide_int_def sgn_if)
lemma smod_word_zero [simp]:
‹w smod 0 = w› for w :: ‹'a::len word›
by transfer (simp add: take_bit_signed_take_bit)
lemma word_sdiv_div1 [simp]:
"(a :: ('a::len) word) sdiv 1 = a"
proof -
have "sint (- (1::'a word)) = - 1"
by simp
then show ?thesis
by (metis int_sdiv_simps(1) mult_1 mult_minus_left scast_eq scast_id
sdiv_minus_eq sdiv_word_def signed_1 wi_hom_neg)
qed
lemma smod_word_one [simp]:
‹w smod 1 = 0› for w :: ‹'a::len word›
by (simp add: smod_word_def signed_modulo_int_def)
lemma word_sdiv_div_minus1 [simp]:
"(a :: ('a::len) word) sdiv -1 = -a"
by (simp add: sdiv_word_def)
lemma smod_word_minus_one [simp]:
‹w smod - 1 = 0› for w :: ‹'a::len word›
by (simp add: smod_word_def signed_modulo_int_def)
lemma one_sdiv_word_eq [simp]:
‹1 sdiv w = of_bool (w = 1 ∨ w = - 1) * w› for w :: ‹'a::len word›
proof (cases ‹1 < ¦sint w¦›)
case True
then show ?thesis
by (auto simp add: sdiv_word_def signed_divide_int_def split: if_splits)
next
case False
then have ‹¦sint w¦ ≤ 1›
by simp
then have ‹sint w ∈ {- 1, 0, 1}›
by auto
then have ‹(word_of_int (sint w) :: 'a::len word) ∈ word_of_int ` {- 1, 0, 1}›
by blast
then have ‹w ∈ {- 1, 0, 1}›
by simp
then show ?thesis by auto
qed
lemma one_smod_word_eq [simp]:
‹1 smod w = 1 - of_bool (w = 1 ∨ w = - 1)› for w :: ‹'a::len word›
using sdiv_smod_id [of 1 w] by auto
lemma minus_one_sdiv_word_eq [simp]:
‹- 1 sdiv w = - (1 sdiv w)› for w :: ‹'a::len word›
by (metis (mono_tags, opaque_lifting) minus_sdiv_eq of_int_minus sdiv_word_def signed_1 sint_n1
word_sdiv_div1 word_sdiv_div_minus1)
lemma minus_one_smod_word_eq [simp]:
‹- 1 smod w = - (1 smod w)› for w :: ‹'a::len word›
using sdiv_smod_id [of ‹- 1› w] by auto
lemma smod_word_alt_def:
"(a :: ('a::len) word) smod b = a - (a sdiv b) * b"
by (simp add: minus_sdiv_mult_eq_smod)
lemmas sdiv_word_numeral_numeral [simp] =
sdiv_word_def [of ‹numeral a› ‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_minus_numeral_numeral [simp] =
sdiv_word_def [of ‹- numeral a› ‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_numeral_minus_numeral [simp] =
sdiv_word_def [of ‹numeral a› ‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas sdiv_word_minus_numeral_minus_numeral [simp] =
sdiv_word_def [of ‹- numeral a› ‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_numeral_numeral [simp] =
smod_word_def [of ‹numeral a› ‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_minus_numeral_numeral [simp] =
smod_word_def [of ‹- numeral a› ‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_numeral_minus_numeral [simp] =
smod_word_def [of ‹numeral a› ‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas smod_word_minus_numeral_minus_numeral [simp] =
smod_word_def [of ‹- numeral a› ‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg]
for a b
lemmas word_sdiv_0 = word_sdiv_div0
lemma sdiv_word_min:
"- (2 ^ (size a - 1)) ≤ sint (a :: ('a::len) word) sdiv sint (b :: ('a::len) word)"
by (smt (verit, ccfv_SIG) atLeastAtMost_iff sdiv_int_range sint_ge sint_lt wsst_TYs(3))
lemma sdiv_word_max:
‹sint a sdiv sint b ≤ 2 ^ (size a - Suc 0)›
for a b :: ‹'a::len word›
proof (cases ‹sint a = 0 ∨ sint b = 0 ∨ sgn (sint a) ≠ sgn (sint b)›)
case True then show ?thesis
proof -
have "⋀i j::int. i sdiv j ≤ ¦i¦"
by (meson atLeastAtMost_iff sdiv_int_range)
then show ?thesis
by (smt (verit) sint_range_size)
qed
next
case False
then have ‹¦sint a¦ div ¦sint b¦ ≤ ¦sint a¦›
by (subst nat_le_eq_zle [symmetric]) (simp_all add: div_abs_eq_div_nat)
also have ‹¦sint a¦ ≤ 2 ^ (size a - Suc 0)›
using sint_range_size [of a] by auto
finally show ?thesis
using False by (simp add: signed_divide_int_def)
qed
lemmas word_sdiv_numerals_lhs = sdiv_word_def[where v="numeral x" for x]
sdiv_word_def[where v=0] sdiv_word_def[where v=1]
lemmas word_sdiv_numerals = word_sdiv_numerals_lhs[where w="numeral y" for y]
word_sdiv_numerals_lhs[where w=0] word_sdiv_numerals_lhs[where w=1]
lemma smod_word_mod_0:
"x smod (0 :: ('a::len) word) = x"
by (fact smod_word_zero)
lemma smod_word_0_mod [simp]:
"0 smod (x :: ('a::len) word) = 0"
by (clarsimp simp: smod_word_def)
lemma smod_word_max:
"sint (a::'a word) smod sint (b::'a word) < 2 ^ (LENGTH('a::len) - Suc 0)"
proof (cases ‹sint b = 0 ∨ LENGTH('a) = 0›)
case True
then show ?thesis
by (force simp: sint_less)
next
case False
then show ?thesis
by (smt (verit) sint_greater_eq sint_less smod_int_compares)
qed
lemma smod_word_min:
"- (2 ^ (LENGTH('a::len) - Suc 0)) ≤ sint (a::'a word) smod sint (b::'a word)"
by (smt (verit) sint_greater_eq sint_less smod_int_compares smod_int_mod_0)
lemmas word_smod_numerals_lhs = smod_word_def[where v="numeral x" for x]
smod_word_def[where v=0] smod_word_def[where v=1]
lemmas word_smod_numerals = word_smod_numerals_lhs[where w="numeral y" for y]
word_smod_numerals_lhs[where w=0] word_smod_numerals_lhs[where w=1]
end