Theory Word_Lib.More_Word
section ‹Lemmas on words›
theory More_Word
imports
"HOL-Library.Word"
More_Arithmetic
More_Divides
More_Bit_Ring
begin
context
includes bit_operations_syntax
begin
lemma sofl_test:
‹sint x + sint y = sint (x + y) ⟷
drop_bit (size x - 1) ((x + y XOR x) AND (x + y XOR y)) = 0›
for x y :: ‹'a::len word›
proof -
obtain n where n: ‹LENGTH('a) = Suc n›
by (cases ‹LENGTH('a)›) simp_all
have *: ‹sint x + sint y + 2 ^ Suc n > signed_take_bit n (sint x + sint y) ⟹ sint x + sint y ≥ - (2 ^ n)›
‹signed_take_bit n (sint x + sint y) > sint x + sint y - 2 ^ Suc n ⟹ 2 ^ n > sint x + sint y›
using signed_take_bit_int_greater_eq [of ‹sint x + sint y› n] signed_take_bit_int_less_eq [of n ‹sint x + sint y›]
by (auto intro: ccontr)
have ‹sint x + sint y = sint (x + y) ⟷
(sint (x + y) < 0 ⟷ sint x < 0) ∨
(sint (x + y) < 0 ⟷ sint y < 0)›
using sint_less [of x] sint_greater_eq [of x] sint_less [of y] sint_greater_eq [of y]
signed_take_bit_int_eq_self [of ‹LENGTH('a) - 1› ‹sint x + sint y›]
apply (auto simp add: not_less)
apply (unfold sint_word_ariths)
apply (subst signed_take_bit_int_eq_self)
prefer 4
apply (subst signed_take_bit_int_eq_self)
prefer 7
apply (subst signed_take_bit_int_eq_self)
prefer 10
apply (subst signed_take_bit_int_eq_self)
apply (auto simp add: signed_take_bit_int_eq_self signed_take_bit_eq_take_bit_minus take_bit_Suc_from_most n not_less intro!: *)
done
then show ?thesis
apply (simp only: One_nat_def word_size drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
apply (simp add: bit_last_iff)
done
qed
lemma unat_power_lower [simp]:
"unat ((2::'a::len word) ^ n) = 2 ^ n" if "n < LENGTH('a::len)"
using that by transfer simp
lemma unat_p2: "n < LENGTH('a :: len) ⟹ unat (2 ^ n :: 'a word) = 2 ^ n"
by (fact unat_power_lower)
lemma word_div_lt_eq_0:
"x < y ⟹ x div y = 0" for x :: "'a :: len word"
by (fact div_word_less)
lemma word_div_eq_1_iff: "n div m = 1 ⟷ n ≥ m ∧ unat n < 2 * unat (m :: 'a :: len word)"
apply (simp only: word_arith_nat_defs word_le_nat_alt word_of_nat_eq_iff flip: nat_div_eq_Suc_0_iff)
apply (simp flip: unat_div unsigned_take_bit_eq)
done
lemma AND_twice [simp]:
"(w AND m) AND m = w AND m"
by (fact and.right_idem)
lemma word_combine_masks:
"w AND m = z ⟹ w AND m' = z' ⟹ w AND (m OR m') = (z OR z')"
for w m m' z z' :: ‹'a::len word›
by (simp add: bit.conj_disj_distrib)
lemma p2_gt_0:
"(0 < (2 ^ n :: 'a :: len word)) = (n < LENGTH('a))"
by (simp add : word_gt_0 not_le)
lemma uint_2p_alt:
‹n < LENGTH('a::len) ⟹ uint ((2::'a::len word) ^ n) = 2 ^ n›
using p2_gt_0 [of n, where ?'a = 'a] by (simp add: uint_2p)
lemma p2_eq_0:
‹(2::'a::len word) ^ n = 0 ⟷ LENGTH('a::len) ≤ n›
by (fact exp_eq_zero_iff)
lemma p2len:
‹(2 :: 'a word) ^ LENGTH('a::len) = 0›
by (fact word_pow_0)
lemma neg_mask_is_div:
"w AND NOT (mask n) = (w div 2^n) * 2^n"
for w :: ‹'a::len word›
by (rule bit_word_eqI)
(auto simp add: bit_simps simp flip: push_bit_eq_mult drop_bit_eq_div)
lemma neg_mask_is_div':
"n < size w ⟹ w AND NOT (mask n) = ((w div (2 ^ n)) * (2 ^ n))"
for w :: ‹'a::len word›
by (rule neg_mask_is_div)
lemma and_mask_arith:
"w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
for w :: ‹'a::len word›
by (rule bit_word_eqI)
(auto simp add: bit_simps word_size simp flip: push_bit_eq_mult drop_bit_eq_div)
lemma and_mask_arith':
"0 < n ⟹ w AND mask n = (w * 2^(size w - n)) div 2^(size w - n)"
for w :: ‹'a::len word›
by (rule and_mask_arith)
lemma mask_2pm1: "mask n = 2 ^ n - (1 :: 'a::len word)"
by (fact mask_eq_decr_exp)
lemma add_mask_fold:
"x + 2 ^ n - 1 = x + mask n"
for x :: ‹'a::len word›
by (simp add: mask_eq_decr_exp)
lemma word_and_mask_le_2pm1: "w AND mask n ≤ 2 ^ n - 1"
for w :: ‹'a::len word›
by (simp add: mask_2pm1[symmetric] word_and_le1)
lemma is_aligned_AND_less_0:
"u AND mask n = 0 ⟹ v < 2^n ⟹ u AND v = 0"
for u v :: ‹'a::len word›
apply (drule less_mask_eq)
apply (simp flip: take_bit_eq_mask)
apply (simp add: bit_eq_iff)
apply (auto simp add: bit_simps)
done
lemma and_mask_eq_iff_le_mask:
‹w AND mask n = w ⟷ w ≤ mask n›
for w :: ‹'a::len word›
apply (simp flip: take_bit_eq_mask)
apply (cases ‹n ≥ LENGTH('a)›; transfer)
apply (simp_all add: not_le min_def)
apply (simp_all add: mask_eq_exp_minus_1)
apply auto
apply (metis take_bit_int_less_exp)
apply (metis min_def nat_less_le take_bit_int_eq_self_iff take_bit_take_bit)
done
lemma less_eq_mask_iff_take_bit_eq_self:
‹w ≤ mask n ⟷ take_bit n w = w›
for w :: ‹'a::len word›
by (simp add: and_mask_eq_iff_le_mask take_bit_eq_mask)
lemma NOT_eq:
"NOT (x :: 'a :: len word) = - x - 1"
by (fact not_eq_complement)
lemma NOT_mask: "NOT (mask n :: 'a::len word) = - (2 ^ n)"
by (simp add : NOT_eq mask_2pm1)
lemma le_m1_iff_lt: "(x > (0 :: 'a :: len word)) = ((y ≤ x - 1) = (y < x))"
by uint_arith
lemma gt0_iff_gem1:
‹0 < x ⟷ x - 1 < x›
for x :: ‹'a::len word›
by (metis add.right_neutral diff_add_cancel less_irrefl measure_unat unat_arith_simps(2) word_neq_0_conv word_sub_less_iff)
lemma power_2_ge_iff:
‹2 ^ n - (1 :: 'a::len word) < 2 ^ n ⟷ n < LENGTH('a)›
using gt0_iff_gem1 p2_gt_0 by blast
lemma le_mask_iff_lt_2n:
"n < len_of TYPE ('a) = (((w :: 'a :: len word) ≤ mask n) = (w < 2 ^ n))"
unfolding mask_2pm1 by (rule trans [OF p2_gt_0 [THEN sym] le_m1_iff_lt])
lemma mask_lt_2pn:
‹n < LENGTH('a) ⟹ mask n < (2 :: 'a::len word) ^ n›
by (simp add: mask_eq_exp_minus_1 power_2_ge_iff)
lemma word_unat_power:
"(2 :: 'a :: len word) ^ n = of_nat (2 ^ n)"
by simp
lemma of_nat_mono_maybe:
assumes xlt: "x < 2 ^ len_of TYPE ('a)"
shows "y < x ⟹ of_nat y < (of_nat x :: 'a :: len word)"
apply (subst word_less_nat_alt)
apply (subst unat_of_nat)+
apply (subst mod_less)
apply (erule order_less_trans [OF _ xlt])
apply (subst mod_less [OF xlt])
apply assumption
done
lemma word_and_max_word:
fixes a::"'a::len word"
shows "x = - 1 ⟹ a AND x = a"
by simp
lemma word_and_full_mask_simp:
‹x AND mask LENGTH('a) = x› for x :: ‹'a::len word›
by (simp add: bit_eq_iff bit_simps)
lemma of_int_uint:
"of_int (uint x) = x"
by (fact word_of_int_uint)
corollary word_plus_and_or_coroll:
"x AND y = 0 ⟹ x + y = x OR y"
for x y :: ‹'a::len word›
by (fact disjunctive_add2)
corollary word_plus_and_or_coroll2:
"(x AND w) + (x AND NOT w) = x"
for x w :: ‹'a::len word›
by (fact and_plus_not_and)
lemma unat_mask_eq:
‹unat (mask n :: 'a::len word) = mask (min LENGTH('a) n)›
by transfer (simp add: nat_mask_eq)
lemma word_plus_mono_left:
fixes x :: "'a :: len word"
shows "⟦y ≤ z; x ≤ x + z⟧ ⟹ y + x ≤ z + x"
by unat_arith
lemma less_Suc_unat_less_bound:
"n < Suc (unat (x :: 'a :: len word)) ⟹ n < 2 ^ LENGTH('a)"
by (auto elim!: order_less_le_trans intro: Suc_leI)
lemma up_ucast_inj:
"⟦ ucast x = (ucast y::'b::len word); LENGTH('a) ≤ len_of TYPE ('b) ⟧ ⟹ x = (y::'a::len word)"
by transfer (simp add: min_def split: if_splits)
lemmas ucast_up_inj = up_ucast_inj
lemma up_ucast_inj_eq:
"LENGTH('a) ≤ len_of TYPE ('b) ⟹ (ucast x = (ucast y::'b::len word)) = (x = (y::'a::len word))"
by (fastforce dest: up_ucast_inj)
lemma no_plus_overflow_neg:
"(x :: 'a :: len word) < -y ⟹ x ≤ x + y"
by (metis diff_minus_eq_add less_imp_le sub_wrap_lt)
lemma ucast_ucast_eq:
"⟦ ucast x = (ucast (ucast y::'a word)::'c::len word); LENGTH('a) ≤ LENGTH('b);
LENGTH('b) ≤ LENGTH('c) ⟧ ⟹
x = ucast y" for x :: "'a::len word" and y :: "'b::len word"
apply transfer
apply (cases ‹LENGTH('c) = LENGTH('a)›)
apply (auto simp add: min_def)
done
lemma ucast_0_I:
"x = 0 ⟹ ucast x = 0"
by simp
lemma word_add_offset_less:
fixes x :: "'a :: len word"
assumes yv: "y < 2 ^ n"
and xv: "x < 2 ^ m"
and mnv: "sz < LENGTH('a :: len)"
and xv': "x < 2 ^ (LENGTH('a :: len) - n)"
and mn: "sz = m + n"
shows "x * 2 ^ n + y < 2 ^ sz"
proof (subst mn)
from mnv mn have nv: "n < LENGTH('a)" and mv: "m < LENGTH('a)" by auto
have uy: "unat y < 2 ^ n"
by (rule order_less_le_trans [OF unat_mono [OF yv] order_eq_refl],
rule unat_power_lower[OF nv])
have ux: "unat x < 2 ^ m"
by (rule order_less_le_trans [OF unat_mono [OF xv] order_eq_refl],
rule unat_power_lower[OF mv])
then show "x * 2 ^ n + y < 2 ^ (m + n)" using ux uy nv mnv xv'
apply (subst word_less_nat_alt)
apply (subst unat_word_ariths)+
apply (subst mod_less)
apply simp
apply (subst mult.commute)
apply (rule nat_less_power_trans [OF _ order_less_imp_le [OF nv]])
apply (rule order_less_le_trans [OF unat_mono [OF xv']])
apply (cases "n = 0"; simp)
apply (subst unat_power_lower[OF nv])
apply (subst mod_less)
apply (erule order_less_le_trans [OF nat_add_offset_less], assumption)
apply (rule mn)
apply simp
apply (simp add: mn mnv)
apply (erule nat_add_offset_less; simp)
done
qed
lemma word_less_power_trans:
fixes n :: "'a :: len word"
assumes nv: "n < 2 ^ (m - k)"
and kv: "k ≤ m"
and mv: "m < len_of TYPE ('a)"
shows "2 ^ k * n < 2 ^ m"
using nv kv mv
apply -
apply (subst word_less_nat_alt)
apply (subst unat_word_ariths)
apply (subst mod_less)
apply simp
apply (rule nat_less_power_trans)
apply (erule order_less_trans [OF unat_mono])
apply simp
apply simp
apply simp
apply (rule nat_less_power_trans)
apply (subst unat_power_lower[where 'a = 'a, symmetric])
apply simp
apply (erule unat_mono)
apply simp
done
lemma word_less_power_trans2:
fixes n :: "'a::len word"
shows "⟦n < 2 ^ (m - k); k ≤ m; m < LENGTH('a)⟧ ⟹ n * 2 ^ k < 2 ^ m"
by (subst field_simps, rule word_less_power_trans)
lemma Suc_unat_diff_1:
fixes x :: "'a :: len word"
assumes lt: "1 ≤ x"
shows "Suc (unat (x - 1)) = unat x"
proof -
have "0 < unat x"
by (rule order_less_le_trans [where y = 1], simp, subst unat_1 [symmetric],
rule iffD1 [OF word_le_nat_alt lt])
then show ?thesis
by ((subst unat_sub [OF lt])+, simp only: unat_1)
qed
lemma word_eq_unatI:
‹v = w› if ‹unat v = unat w›
using that by transfer (simp add: nat_eq_iff)
lemma word_div_sub:
fixes x :: "'a :: len word"
assumes yx: "y ≤ x"
and y0: "0 < y"
shows "(x - y) div y = x div y - 1"
apply (rule word_eq_unatI)
apply (subst unat_div)
apply (subst unat_sub [OF yx])
apply (subst unat_sub)
apply (subst word_le_nat_alt)
apply (subst unat_div)
apply (subst le_div_geq)
apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
apply simp
apply (subst word_le_nat_alt [symmetric], rule yx)
apply simp
apply (subst unat_div)
apply (subst le_div_geq [OF _ iffD1 [OF word_le_nat_alt yx]])
apply (rule order_le_less_trans [OF _ unat_mono [OF y0]])
apply simp
apply simp
done
lemma word_mult_less_mono1:
fixes i :: "'a :: len word"
assumes ij: "i < j"
and knz: "0 < k"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "i * k < j * k"
proof -
from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
by (auto intro: order_less_subst2 simp: word_less_nat_alt elim: mult_less_mono1)
then show ?thesis using ujk knz ij
by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem])
qed
lemma word_mult_less_dest:
fixes i :: "'a :: len word"
assumes ij: "i * k < j * k"
and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "i < j"
using uik ujk ij
by (auto simp: word_less_nat_alt iffD1 [OF unat_mult_lem] elim: mult_less_mono1)
lemma word_mult_less_cancel:
fixes k :: "'a :: len word"
assumes knz: "0 < k"
and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "(i * k < j * k) = (i < j)"
by (rule iffI [OF word_mult_less_dest [OF _ uik ujk] word_mult_less_mono1 [OF _ knz ujk]])
lemma Suc_div_unat_helper:
assumes szv: "sz < LENGTH('a :: len)"
and usszv: "us ≤ sz"
shows "2 ^ (sz - us) = Suc (unat (((2::'a :: len word) ^ sz - 1) div 2 ^ us))"
proof -
note usv = order_le_less_trans [OF usszv szv]
from usszv obtain q where qv: "sz = us + q" by (auto simp: le_iff_add)
have "Suc (unat (((2:: 'a word) ^ sz - 1) div 2 ^ us)) =
(2 ^ us + unat ((2:: 'a word) ^ sz - 1)) div 2 ^ us"
apply (subst unat_div unat_power_lower[OF usv])+
apply (subst div_add_self1, simp+)
done
also have "… = ((2 ^ us - 1) + 2 ^ sz) div 2 ^ us" using szv
by (simp add: unat_minus_one)
also have "… = 2 ^ q + ((2 ^ us - 1) div 2 ^ us)"
apply (subst qv)
apply (subst power_add)
apply (subst div_mult_self2; simp)
done
also have "… = 2 ^ (sz - us)" using qv by simp
finally show ?thesis ..
qed
lemma enum_word_nth_eq:
‹(Enum.enum :: 'a::len word list) ! n = word_of_nat n›
if ‹n < 2 ^ LENGTH('a)›
for n
using that by (simp add: enum_word_def)
lemma length_enum_word_eq:
‹length (Enum.enum :: 'a::len word list) = 2 ^ LENGTH('a)›
by (simp add: enum_word_def)
lemma unat_lt2p [iff]:
‹unat x < 2 ^ LENGTH('a)› for x :: ‹'a::len word›
by transfer simp
lemma of_nat_unat [simp]:
"of_nat ∘ unat = id"
by (rule ext, simp)
lemma Suc_unat_minus_one [simp]:
"x ≠ 0 ⟹ Suc (unat (x - 1)) = unat x"
by (metis Suc_diff_1 unat_gt_0 unat_minus_one)
lemma word_add_le_dest:
fixes i :: "'a :: len word"
assumes le: "i + k ≤ j + k"
and uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "i ≤ j"
using uik ujk le
by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem] elim: add_le_mono1)
lemma word_add_le_mono1:
fixes i :: "'a :: len word"
assumes ij: "i ≤ j"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "i + k ≤ j + k"
proof -
from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: add_le_mono1)
then show ?thesis using ujk ij
by (auto simp: word_le_nat_alt iffD1 [OF unat_add_lem])
qed
lemma word_add_le_mono2:
fixes i :: "'a :: len word"
shows "⟦i ≤ j; unat j + unat k < 2 ^ LENGTH('a)⟧ ⟹ k + i ≤ k + j"
by (subst field_simps, subst field_simps, erule (1) word_add_le_mono1)
lemma word_add_le_iff:
fixes i :: "'a :: len word"
assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "(i + k ≤ j + k) = (i ≤ j)"
proof
assume "i ≤ j"
show "i + k ≤ j + k" by (rule word_add_le_mono1) fact+
next
assume "i + k ≤ j + k"
show "i ≤ j" by (rule word_add_le_dest) fact+
qed
lemma word_add_less_mono1:
fixes i :: "'a :: len word"
assumes ij: "i < j"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "i + k < j + k"
proof -
from ij ujk have jk: "unat i + unat k < 2 ^ len_of TYPE ('a)"
by (auto elim: order_le_less_subst2 simp: word_less_nat_alt elim: add_less_mono1)
then show ?thesis using ujk ij
by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem])
qed
lemma word_add_less_dest:
fixes i :: "'a :: len word"
assumes le: "i + k < j + k"
and uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "i < j"
using uik ujk le
by (auto simp: word_less_nat_alt iffD1 [OF unat_add_lem] elim: add_less_mono1)
lemma word_add_less_iff:
fixes i :: "'a :: len word"
assumes uik: "unat i + unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j + unat k < 2 ^ len_of TYPE ('a)"
shows "(i + k < j + k) = (i < j)"
proof
assume "i < j"
show "i + k < j + k" by (rule word_add_less_mono1) fact+
next
assume "i + k < j + k"
show "i < j" by (rule word_add_less_dest) fact+
qed
lemma word_mult_less_iff:
fixes i :: "'a :: len word"
assumes knz: "0 < k"
and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "(i * k < j * k) = (i < j)"
using assms by (rule word_mult_less_cancel)
lemma word_le_imp_diff_le:
fixes n :: "'a::len word"
shows "⟦k ≤ n; n ≤ m⟧ ⟹ n - k ≤ m"
by (auto simp: unat_sub word_le_nat_alt)
lemma word_less_imp_diff_less:
fixes n :: "'a::len word"
shows "⟦k ≤ n; n < m⟧ ⟹ n - k < m"
by (clarsimp simp: unat_sub word_less_nat_alt
intro!: less_imp_diff_less)
lemma word_mult_le_mono1:
fixes i :: "'a :: len word"
assumes ij: "i ≤ j"
and knz: "0 < k"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "i * k ≤ j * k"
proof -
from ij ujk knz have jk: "unat i * unat k < 2 ^ len_of TYPE ('a)"
by (auto elim: order_le_less_subst2 simp: word_le_nat_alt elim: mult_le_mono1)
then show ?thesis using ujk knz ij
by (auto simp: word_le_nat_alt iffD1 [OF unat_mult_lem])
qed
lemma word_mult_le_iff:
fixes i :: "'a :: len word"
assumes knz: "0 < k"
and uik: "unat i * unat k < 2 ^ len_of TYPE ('a)"
and ujk: "unat j * unat k < 2 ^ len_of TYPE ('a)"
shows "(i * k ≤ j * k) = (i ≤ j)"
proof
assume "i ≤ j"
show "i * k ≤ j * k" by (rule word_mult_le_mono1) fact+
next
assume p: "i * k ≤ j * k"
have "0 < unat k" using knz by (simp add: word_less_nat_alt)
then show "i ≤ j" using p
by (clarsimp simp: word_le_nat_alt iffD1 [OF unat_mult_lem uik]
iffD1 [OF unat_mult_lem ujk])
qed
lemma word_diff_less:
fixes n :: "'a :: len word"
shows "⟦0 < n; 0 < m; n ≤ m⟧ ⟹ m - n < m"
apply (subst word_less_nat_alt)
apply (subst unat_sub)
apply assumption
apply (rule diff_less)
apply (simp_all add: word_less_nat_alt)
done
lemma word_add_increasing:
fixes x :: "'a :: len word"
shows "⟦ p + w ≤ x; p ≤ p + w ⟧ ⟹ p ≤ x"
by unat_arith
lemma word_random:
fixes x :: "'a :: len word"
shows "⟦ p ≤ p + x'; x ≤ x' ⟧ ⟹ p ≤ p + x"
by unat_arith
lemma word_sub_mono:
"⟦ a ≤ c; d ≤ b; a - b ≤ a; c - d ≤ c ⟧
⟹ (a - b) ≤ (c - d :: 'a :: len word)"
by unat_arith
lemma power_not_zero:
"n < LENGTH('a::len) ⟹ (2 :: 'a word) ^ n ≠ 0"
by (metis p2_gt_0 word_neq_0_conv)
lemma word_gt_a_gt_0:
"a < n ⟹ (0 :: 'a::len word) < n"
apply (case_tac "n = 0")
apply clarsimp
apply (clarsimp simp: word_neq_0_conv)
done
lemma word_power_less_1 [simp]:
"sz < LENGTH('a::len) ⟹ (2::'a word) ^ sz - 1 < 2 ^ sz"
apply (simp add: word_less_nat_alt)
apply (subst unat_minus_one)
apply simp_all
done
lemma word_sub_1_le:
"x ≠ 0 ⟹ x - 1 ≤ (x :: 'a :: len word)"
apply (subst no_ulen_sub)
apply simp
apply (cases "uint x = 0")
apply (simp add: uint_0_iff)
apply (insert uint_ge_0[where x=x])
apply arith
done
lemma push_bit_word_eq_nonzero:
‹push_bit n w ≠ 0› if ‹w < 2 ^ m› ‹m + n < LENGTH('a)› ‹w ≠ 0›
for w :: ‹'a::len word›
using that
apply (simp only: word_neq_0_conv word_less_nat_alt
mod_0 unat_word_ariths
unat_power_lower word_le_nat_alt)
apply (metis add_diff_cancel_right' gr0I gr_implies_not0 less_or_eq_imp_le min_def push_bit_eq_0_iff take_bit_nat_eq_self_iff take_bit_push_bit take_bit_take_bit unsigned_push_bit_eq)
done
lemma unat_less_power:
fixes k :: "'a::len word"
assumes szv: "sz < LENGTH('a)"
and kv: "k < 2 ^ sz"
shows "unat k < 2 ^ sz"
using szv unat_mono [OF kv] by simp
lemma unat_mult_power_lem:
assumes kv: "k < 2 ^ (LENGTH('a::len) - sz)"
shows "unat (2 ^ sz * of_nat k :: (('a::len) word)) = 2 ^ sz * k"
proof (cases ‹sz < LENGTH('a)›)
case True
with assms show ?thesis
by (simp add: unat_word_ariths take_bit_eq_mod mod_simps unsigned_of_nat)
(simp add: take_bit_nat_eq_self_iff nat_less_power_trans flip: take_bit_eq_mod)
next
case False
with assms show ?thesis
by simp
qed
lemma word_plus_mcs_4:
"⟦v + x ≤ w + x; x ≤ v + x⟧ ⟹ v ≤ (w::'a::len word)"
by uint_arith
lemma word_plus_mcs_3:
"⟦v ≤ w; x ≤ w + x⟧ ⟹ v + x ≤ w + (x::'a::len word)"
by unat_arith
lemma word_le_minus_one_leq:
"x < y ⟹ x ≤ y - 1" for x :: "'a :: len word"
by transfer (metis le_less_trans less_irrefl take_bit_decr_eq take_bit_nonnegative zle_diff1_eq)
lemma word_less_sub_le[simp]:
fixes x :: "'a :: len word"
assumes nv: "n < LENGTH('a)"
shows "(x ≤ 2 ^ n - 1) = (x < 2 ^ n)"
using le_less_trans word_le_minus_one_leq nv power_2_ge_iff by blast
lemma unat_of_nat_len:
"x < 2 ^ LENGTH('a) ⟹ unat (of_nat x :: 'a::len word) = x"
by (simp add: unsigned_of_nat take_bit_nat_eq_self_iff)
lemma unat_of_nat_eq:
"x < 2 ^ LENGTH('a) ⟹ unat (of_nat x ::'a::len word) = x"
by (rule unat_of_nat_len)
lemma unat_eq_of_nat:
"n < 2 ^ LENGTH('a) ⟹ (unat (x :: 'a::len word) = n) = (x = of_nat n)"
by transfer
(auto simp add: take_bit_of_nat nat_eq_iff take_bit_nat_eq_self_iff intro: sym)
lemma alignUp_div_helper:
fixes a :: "'a::len word"
assumes kv: "k < 2 ^ (LENGTH('a) - n)"
and xk: "x = 2 ^ n * of_nat k"
and le: "a ≤ x"
and sz: "n < LENGTH('a)"
and anz: "a mod 2 ^ n ≠ 0"
shows "a div 2 ^ n < of_nat k"
proof -
have kn: "unat (of_nat k :: 'a word) * unat ((2::'a word) ^ n) < 2 ^ LENGTH('a)"
using xk kv sz
apply (subst unat_of_nat_eq)
apply (erule order_less_le_trans)
apply simp
apply (subst unat_power_lower, simp)
apply (subst mult.commute)
apply (rule nat_less_power_trans)
apply simp
apply simp
done
have "unat a div 2 ^ n * 2 ^ n ≠ unat a"
proof -
have "unat a = unat a div 2 ^ n * 2 ^ n + unat a mod 2 ^ n"
by (simp add: div_mult_mod_eq)
also have "… ≠ unat a div 2 ^ n * 2 ^ n" using sz anz
by (simp add: unat_arith_simps)
finally show ?thesis ..
qed
then have "a div 2 ^ n * 2 ^ n < a" using sz anz
apply (subst word_less_nat_alt)
apply (subst unat_word_ariths)
apply (subst unat_div)
apply simp
apply (rule order_le_less_trans [OF mod_less_eq_dividend])
apply (erule order_le_neq_trans [OF div_mult_le])
done
also from xk le have "… ≤ of_nat k * 2 ^ n" by (simp add: field_simps)
finally show ?thesis using sz kv
apply -
apply (erule word_mult_less_dest [OF _ _ kn])
apply (simp add: unat_div)
apply (rule order_le_less_trans [OF div_mult_le])
apply (rule unat_lt2p)
done
qed
lemma mask_out_sub_mask:
"(x AND NOT (mask n)) = x - (x AND (mask n))"
for x :: ‹'a::len word›
by (fact and_not_eq_minus_and)
lemma subtract_mask:
"p - (p AND mask n) = (p AND NOT (mask n))"
"p - (p AND NOT (mask n)) = (p AND mask n)"
for p :: ‹'a::len word›
by (auto simp: and_not_eq_minus_and)
lemma take_bit_word_eq_self_iff:
‹take_bit n w = w ⟷ n ≥ LENGTH('a) ∨ w < 2 ^ n›
for w :: ‹'a::len word›
using take_bit_int_eq_self_iff [of n ‹take_bit LENGTH('a) (uint w)›]
by (transfer fixing: n) auto
lemma word_power_increasing:
assumes x: "2 ^ x < (2 ^ y::'a::len word)" "x < LENGTH('a)" "y < LENGTH('a)"
shows "x < y" using x
using assms by transfer simp
lemma mask_twice:
"(x AND mask n) AND mask m = x AND mask (min m n)"
for x :: ‹'a::len word›
by (simp flip: take_bit_eq_mask)
lemma plus_one_helper[elim!]:
"x < n + (1 :: 'a :: len word) ⟹ x ≤ n"
apply (simp add: word_less_nat_alt word_le_nat_alt field_simps)
apply (case_tac "1 + n = 0")
apply simp_all
apply (subst(asm) unatSuc, assumption)
apply arith
done
lemma plus_one_helper2:
"⟦ x ≤ n; n + 1 ≠ 0 ⟧ ⟹ x < n + (1 :: 'a :: len word)"
by (simp add: word_less_nat_alt word_le_nat_alt field_simps
unatSuc)
lemma less_x_plus_1:
"x ≠ - 1 ⟹ (y < x + 1) = (y < x ∨ y = x)" for x :: "'a::len word"
by (meson max_word_wrap plus_one_helper plus_one_helper2 word_le_less_eq)
lemma word_Suc_leq:
fixes k::"'a::len word" shows "k ≠ - 1 ⟹ x < k + 1 ⟷ x ≤ k"
using less_x_plus_1 word_le_less_eq by auto
lemma word_Suc_le:
fixes k::"'a::len word" shows "x ≠ - 1 ⟹ x + 1 ≤ k ⟷ x < k"
by (meson not_less word_Suc_leq)
lemma word_lessThan_Suc_atMost:
‹{..< k + 1} = {..k}› if ‹k ≠ - 1› for k :: ‹'a::len word›
using that by (simp add: lessThan_def atMost_def word_Suc_leq)
lemma word_atLeastLessThan_Suc_atLeastAtMost:
‹{l ..< u + 1} = {l..u}› if ‹u ≠ - 1› for l :: ‹'a::len word›
using that by (simp add: atLeastAtMost_def atLeastLessThan_def word_lessThan_Suc_atMost)
lemma word_atLeastAtMost_Suc_greaterThanAtMost:
‹{m<..u} = {m + 1..u}› if ‹m ≠ - 1› for m :: ‹'a::len word›
using that by (simp add: greaterThanAtMost_def greaterThan_def atLeastAtMost_def atLeast_def word_Suc_le)
lemma word_atLeastLessThan_Suc_atLeastAtMost_union:
fixes l::"'a::len word"
assumes "m ≠ - 1" and "l ≤ m" and "m ≤ u"
shows "{l..m} ∪ {m+1..u} = {l..u}"
proof -
from ivl_disj_un_two(8)[OF assms(2) assms(3)] have "{l..u} = {l..m} ∪ {m<..u}" by blast
with assms show ?thesis by(simp add: word_atLeastAtMost_Suc_greaterThanAtMost)
qed
lemma max_word_less_eq_iff [simp]:
‹- 1 ≤ w ⟷ w = - 1› for w :: ‹'a::len word›
by (fact word_order.extremum_unique)
lemma word_or_zero:
"(a OR b = 0) = (a = 0 ∧ b = 0)"
for a b :: ‹'a::len word›
by (fact or_eq_0_iff)
lemma word_2p_mult_inc:
assumes x: "2 * 2 ^ n < (2::'a::len word) * 2 ^ m"
assumes suc_n: "Suc n < LENGTH('a::len)"
shows "2^n < (2::'a::len word)^m"
by (smt (verit) suc_n le_less_trans lessI nat_less_le nat_mult_less_cancel_disj p2_gt_0
power_Suc power_Suc unat_power_lower word_less_nat_alt x)
lemma power_overflow:
"n ≥ LENGTH('a) ⟹ 2 ^ n = (0 :: 'a::len word)"
by simp
lemmas [simp] =
word_sle_eq[where a=0 and b=1]
word_sle_eq[where a=0 and b="numeral n"]
word_sle_eq[where a=1 and b=0]
word_sle_eq[where a=1 and b="numeral n"]
word_sle_eq[where a="numeral n" and b=0]
word_sle_eq[where a="numeral n" and b=1]
word_sless_alt[where a=0 and b=1]
word_sless_alt[where a=0 and b="numeral n"]
word_sless_alt[where a=1 and b=0]
word_sless_alt[where a=1 and b="numeral n"]
word_sless_alt[where a="numeral n" and b=0]
word_sless_alt[where a="numeral n" and b=1]
for n
lemma word_sint_1:
"sint (1::'a::len word) = (if LENGTH('a) = 1 then -1 else 1)"
by (fact signed_1)
lemma ucast_of_nat:
"is_down (ucast :: 'a :: len word ⇒ 'b :: len word)
⟹ ucast (of_nat n :: 'a word) = (of_nat n :: 'b word)"
by transfer simp
lemma scast_1':
"(scast (1::'a::len word) :: 'b::len word) =
(word_of_int (signed_take_bit (LENGTH('a::len) - Suc 0) (1::int)))"
by transfer simp
lemma scast_1:
"(scast (1::'a::len word) :: 'b::len word) = (if LENGTH('a) = 1 then -1 else 1)"
by (fact signed_1)
lemma unat_minus_one_word:
"unat (-1 :: 'a :: len word) = 2 ^ LENGTH('a) - 1"
by (simp add: mask_eq_exp_minus_1 unsigned_minus_1_eq_mask)
lemmas word_diff_ls'' = word_diff_ls [where xa=x and x=x for x]
lemmas word_diff_ls' = word_diff_ls'' [simplified]
lemmas word_l_diffs' = word_l_diffs [where xa=x and x=x for x]
lemmas word_l_diffs = word_l_diffs' [simplified]
lemma two_power_increasing:
"⟦ n ≤ m; m < LENGTH('a) ⟧ ⟹ (2 :: 'a :: len word) ^ n ≤ 2 ^ m"
by (simp add: word_le_nat_alt)
lemma word_leq_le_minus_one:
"⟦ x ≤ y; x ≠ 0 ⟧ ⟹ x - 1 < (y :: 'a :: len word)"
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (subst unat_minus_one)
apply assumption
apply (cases "unat x")
apply (simp add: unat_eq_zero)
apply arith
done
lemma neg_mask_combine:
"NOT(mask a) AND NOT(mask b) = NOT(mask (max a b) :: 'a::len word)"
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma neg_mask_twice:
"x AND NOT(mask n) AND NOT(mask m) = x AND NOT(mask (max n m))"
for x :: ‹'a::len word›
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma multiple_mask_trivia:
"n ≥ m ⟹ (x AND NOT(mask n)) + (x AND mask n AND NOT(mask m)) = x AND NOT(mask m)"
for x :: ‹'a::len word›
apply (rule trans[rotated], rule_tac w="mask n" in word_plus_and_or_coroll2)
apply (simp add: word_bw_assocs word_bw_comms word_bw_lcs neg_mask_twice
max_absorb2)
done
lemma word_of_nat_less:
"⟦ n < unat x ⟧ ⟹ of_nat n < x"
apply (simp add: word_less_nat_alt)
apply (erule order_le_less_trans[rotated])
apply (simp add: unsigned_of_nat take_bit_eq_mod)
done
lemma unat_mask:
"unat (mask n :: 'a :: len word) = 2 ^ (min n (LENGTH('a))) - 1"
apply (subst min.commute)
apply (simp add: mask_eq_decr_exp not_less min_def split: if_split_asm)
apply (intro conjI impI)
apply (simp add: unat_sub_if_size)
apply (simp add: power_overflow word_size)
apply (simp add: unat_sub_if_size)
done
lemma mask_over_length:
"LENGTH('a) ≤ n ⟹ mask n = (-1::'a::len word)"
by (simp add: mask_eq_decr_exp)
lemma Suc_2p_unat_mask:
"n < LENGTH('a) ⟹ Suc (2 ^ n * k + unat (mask n :: 'a::len word)) = 2 ^ n * (k+1)"
by (simp add: unat_mask)
lemma sint_of_nat_ge_zero:
"x < 2 ^ (LENGTH('a) - 1) ⟹ sint (of_nat x :: 'a :: len word) ≥ 0"
by (simp add: bit_iff_odd signed_of_nat)
lemma int_eq_sint:
"x < 2 ^ (LENGTH('a) - 1) ⟹ sint (of_nat x :: 'a :: len word) = int x"
apply transfer
apply (rule signed_take_bit_int_eq_self)
apply simp_all
apply (metis negative_zle numeral_power_eq_of_nat_cancel_iff)
done
lemma sint_of_nat_le:
"⟦ b < 2 ^ (LENGTH('a) - 1); a ≤ b ⟧
⟹ sint (of_nat a :: 'a :: len word) ≤ sint (of_nat b :: 'a :: len word)"
apply (cases ‹LENGTH('a)›)
apply simp_all
apply transfer
apply (subst signed_take_bit_eq_if_positive)
apply (simp add: bit_simps)
apply (metis bit_take_bit_iff nat_less_le order_less_le_trans take_bit_nat_eq_self_iff)
apply (subst signed_take_bit_eq_if_positive)
apply (simp add: bit_simps)
apply (metis bit_take_bit_iff nat_less_le take_bit_nat_eq_self_iff)
apply (simp flip: of_nat_take_bit add: take_bit_nat_eq_self)
done
lemma word_le_not_less:
"((b::'a::len word) ≤ a) = (¬(a < b))"
by fastforce
lemma less_is_non_zero_p1:
fixes a :: "'a :: len word"
shows "a < k ⟹ a + 1 ≠ 0"
apply (erule contrapos_pn)
apply (drule max_word_wrap)
apply (simp add: not_less)
done
lemma unat_add_lem':
"(unat x + unat y < 2 ^ LENGTH('a)) ⟹
(unat (x + y :: 'a :: len word) = unat x + unat y)"
by (subst unat_add_lem[symmetric], assumption)
lemma word_less_two_pow_divI:
"⟦ (x :: 'a::len word) < 2 ^ (n - m); m ≤ n; n < LENGTH('a) ⟧ ⟹ x < 2 ^ n div 2 ^ m"
apply (simp add: word_less_nat_alt)
apply (subst unat_word_ariths)
apply (subst mod_less)
apply (rule order_le_less_trans [OF div_le_dividend])
apply (rule unat_lt2p)
apply (simp add: power_sub)
done
lemma word_less_two_pow_divD:
"⟦ (x :: 'a::len word) < 2 ^ n div 2 ^ m ⟧
⟹ n ≥ m ∧ (x < 2 ^ (n - m))"
apply (cases "n < LENGTH('a)")
apply (cases "m < LENGTH('a)")
apply (simp add: word_less_nat_alt)
apply (subst(asm) unat_word_ariths)
apply (subst(asm) mod_less)
apply (rule order_le_less_trans [OF div_le_dividend])
apply (rule unat_lt2p)
apply (clarsimp dest!: less_two_pow_divD)
apply (simp add: power_overflow)
apply (simp add: word_div_def)
apply (simp add: power_overflow word_div_def)
done
lemma of_nat_less_two_pow_div_set:
"⟦ n < LENGTH('a) ⟧ ⟹
{x. x < (2 ^ n div 2 ^ m :: 'a::len word)}
= of_nat ` {k. k < 2 ^ n div 2 ^ m}"
apply (simp add: image_def)
apply (safe dest!: word_less_two_pow_divD less_two_pow_divD
intro!: word_less_two_pow_divI)
apply (rule_tac x="unat x" in exI)
apply (simp add: power_sub[symmetric])
apply (subst unat_power_lower[symmetric, where 'a='a])
apply simp
apply (erule unat_mono)
apply (subst word_unat_power)
apply (rule of_nat_mono_maybe)
apply (rule power_strict_increasing)
apply simp
apply simp
apply assumption
done
lemma ucast_less:
"LENGTH('b) < LENGTH('a) ⟹
(ucast (x :: 'b :: len word) :: ('a :: len word)) < 2 ^ LENGTH('b)"
by transfer simp
lemma ucast_range_less:
"LENGTH('a :: len) < LENGTH('b :: len) ⟹
range (ucast :: 'a word ⇒ 'b word) = {x. x < 2 ^ len_of TYPE ('a)}"
apply safe
apply (erule ucast_less)
apply (simp add: image_def)
apply (rule_tac x="ucast x" in exI)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps)
apply (metis bit_take_bit_iff take_bit_word_eq_self_iff)
done
lemma word_power_less_diff:
"⟦2 ^ n * q < (2::'a::len word) ^ m; q < 2 ^ (LENGTH('a) - n)⟧ ⟹ q < 2 ^ (m - n)"
apply (case_tac "m ≥ LENGTH('a)")
apply (simp add: power_overflow)
apply (case_tac "n ≥ LENGTH('a)")
apply (simp add: power_overflow)
apply (cases "n = 0")
apply simp
apply (subst word_less_nat_alt)
apply (subst unat_power_lower)
apply simp
apply (rule nat_power_less_diff)
apply (simp add: word_less_nat_alt)
apply (subst (asm) iffD1 [OF unat_mult_lem])
apply (simp add:nat_less_power_trans)
apply simp
done
lemma word_less_sub_1:
"x < (y :: 'a :: len word) ⟹ x ≤ y - 1"
by (fact word_le_minus_one_leq)
lemma word_sub_mono2:
"⟦ a + b ≤ c + d; c ≤ a; b ≤ a + b; d ≤ c + d ⟧ ⟹ b ≤ (d :: 'a :: len word)"
by (drule(1) word_sub_mono; simp)
lemma word_not_le:
"(¬ x ≤ (y :: 'a :: len word)) = (y < x)"
by (fact not_le)
lemma word_subset_less:
"⟦ {x .. x + r - 1} ⊆ {y .. y + s - 1};
x ≤ x + r - 1; y ≤ y + (s :: 'a :: len word) - 1;
s ≠ 0 ⟧
⟹ r ≤ s"
apply (frule subsetD[where c=x])
apply simp
apply (drule subsetD[where c="x + r - 1"])
apply simp
apply (clarsimp simp: add_diff_eq[symmetric])
apply (drule(1) word_sub_mono2)
apply (simp_all add: olen_add_eqv[symmetric])
apply (erule word_le_minus_cancel)
apply (rule ccontr)
apply (simp add: word_not_le)
done
lemma uint_power_lower:
"n < LENGTH('a) ⟹ uint (2 ^ n :: 'a :: len word) = (2 ^ n :: int)"
by (rule uint_2p_alt)
lemma power_le_mono:
"⟦2 ^ n ≤ (2::'a::len word) ^ m; n < LENGTH('a); m < LENGTH('a)⟧
⟹ n ≤ m"
apply (clarsimp simp add: le_less)
apply safe
apply (simp add: word_less_nat_alt)
apply (simp only: uint_arith_simps(3))
apply (drule uint_power_lower)+
apply simp
done
lemma two_power_eq:
"⟦n < LENGTH('a); m < LENGTH('a)⟧
⟹ ((2::'a::len word) ^ n = 2 ^ m) = (n = m)"
apply safe
apply (rule order_antisym)
apply (simp add: power_le_mono[where 'a='a])+
done
lemma unat_less_helper:
"x < of_nat n ⟹ unat x < n"
apply (simp add: word_less_nat_alt)
apply (erule order_less_le_trans)
apply (simp add: take_bit_eq_mod unsigned_of_nat)
done
lemma nat_uint_less_helper:
"nat (uint y) = z ⟹ x < y ⟹ nat (uint x) < z"
apply (erule subst)
apply (subst unat_eq_nat_uint [symmetric])
apply (subst unat_eq_nat_uint [symmetric])
by (simp add: unat_mono)
lemma of_nat_0:
"⟦of_nat n = (0::'a::len word); n < 2 ^ LENGTH('a)⟧ ⟹ n = 0"
by (auto simp add: word_of_nat_eq_0_iff)
lemma of_nat_inj:
"⟦x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)⟧ ⟹
(of_nat x = (of_nat y :: 'a :: len word)) = (x = y)"
by (metis unat_of_nat_len)
lemma div_to_mult_word_lt:
"⟦ (x :: 'a :: len word) ≤ y div z ⟧ ⟹ x * z ≤ y"
apply (cases "z = 0")
apply simp
apply (simp add: word_neq_0_conv)
apply (rule order_trans)
apply (erule(1) word_mult_le_mono1)
apply (simp add: unat_div)
apply (rule order_le_less_trans [OF div_mult_le])
apply simp
apply (rule word_div_mult_le)
done
lemma ucast_ucast_mask:
"(ucast :: 'a :: len word ⇒ 'b :: len word) (ucast x) = x AND mask (len_of TYPE ('a))"
apply (simp flip: take_bit_eq_mask)
apply transfer
apply (simp add: ac_simps)
done
lemma ucast_ucast_len:
"⟦ x < 2 ^ LENGTH('b) ⟧ ⟹ ucast (ucast x::'b::len word) = (x::'a::len word)"
apply (subst ucast_ucast_mask)
apply (erule less_mask_eq)
done
lemma ucast_ucast_id:
"LENGTH('a) < LENGTH('b) ⟹ ucast (ucast (x::'a::len word)::'b::len word) = x"
by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size)
lemma unat_ucast:
"unat (ucast x :: ('a :: len) word) = unat x mod 2 ^ (LENGTH('a))"
proof -
have ‹2 ^ LENGTH('a) = nat (2 ^ LENGTH('a))›
by simp
moreover have ‹unat (ucast x :: 'a word) = unat x mod nat (2 ^ LENGTH('a))›
by transfer (simp flip: nat_mod_distrib take_bit_eq_mod)
ultimately show ?thesis
by (simp only:)
qed
lemma ucast_less_ucast:
"LENGTH('a) ≤ LENGTH('b) ⟹
(ucast x < ((ucast (y :: 'a::len word)) :: 'b::len word)) = (x < y)"
apply (simp add: word_less_nat_alt unat_ucast)
apply (subst mod_less)
apply(rule less_le_trans[OF unat_lt2p], simp)
apply (subst mod_less)
apply(rule less_le_trans[OF unat_lt2p], simp)
apply simp
done
lemmas ucast_less_ucast_weak = ucast_less_ucast[OF order.strict_implies_order]
lemma unat_Suc2:
fixes n :: "'a :: len word"
shows
"n ≠ -1 ⟹ unat (n + 1) = Suc (unat n)"
apply (subst add.commute, rule unatSuc)
apply (subst eq_diff_eq[symmetric], simp add: minus_equation_iff)
done
lemma word_div_1:
"(n :: 'a :: len word) div 1 = n"
by (fact div_by_1)
lemma word_minus_one_le:
"-1 ≤ (x :: 'a :: len word) = (x = -1)"
by (fact word_order.extremum_unique)
lemma up_scast_inj:
"⟦ scast x = (scast y :: 'b :: len word); size x ≤ LENGTH('b) ⟧ ⟹ x = y"
apply transfer
apply (cases ‹LENGTH('a)›; simp)
apply (metis order_refl take_bit_signed_take_bit take_bit_tightened)
done
lemma up_scast_inj_eq:
"LENGTH('a) ≤ len_of TYPE ('b) ⟹
(scast x = (scast y::'b::len word)) = (x = (y::'a::len word))"
by (fastforce dest: up_scast_inj simp: word_size)
lemma word_le_add:
fixes x :: "'a :: len word"
shows "x ≤ y ⟹ ∃n. y = x + of_nat n"
by (rule exI [where x = "unat (y - x)"]) simp
lemma word_plus_mcs_4':
"⟦x + v ≤ x + w; x ≤ x + v⟧ ⟹ v ≤ w" for x :: "'a::len word"
by (rule word_plus_mcs_4; simp add: add.commute)
lemma unat_eq_1:
‹unat x = Suc 0 ⟷ x = 1›
by (auto intro!: unsigned_word_eqI [where ?'a = nat])
lemma word_unat_Rep_inject1:
‹unat x = unat 1 ⟷ x = 1›
by (simp add: unat_eq_1)
lemma and_not_mask_twice:
"(w AND NOT (mask n)) AND NOT (mask m) = w AND NOT (mask (max m n))"
for w :: ‹'a::len word›
by (rule bit_word_eqI) (auto simp add: bit_simps)
lemma word_less_cases:
"x < y ⟹ x = y - 1 ∨ x < y - (1 ::'a::len word)"
apply (drule word_less_sub_1)
apply (drule order_le_imp_less_or_eq)
apply auto
done
lemma mask_and_mask:
"mask a AND mask b = (mask (min a b) :: 'a::len word)"
by (simp flip: take_bit_eq_mask ac_simps)
lemma mask_eq_0_eq_x:
"(x AND w = 0) = (x AND NOT w = x)"
for x w :: ‹'a::len word›
using word_plus_and_or_coroll2[where x=x and w=w]
by auto
lemma mask_eq_x_eq_0:
"(x AND w = x) = (x AND NOT w = 0)"
for x w :: ‹'a::len word›
using word_plus_and_or_coroll2[where x=x and w=w]
by auto
lemma compl_of_1: "NOT 1 = (-2 :: 'a :: len word)"
by (fact not_one_eq)
lemma split_word_eq_on_mask:
"(x = y) = (x AND m = y AND m ∧ x AND NOT m = y AND NOT m)"
for x y m :: ‹'a::len word›
apply transfer
apply (simp add: bit_eq_iff)
apply (auto simp add: bit_simps ac_simps)
done
lemma word_FF_is_mask:
"0xFF = (mask 8 :: 'a::len word)"
by (simp add: mask_eq_decr_exp)
lemma word_1FF_is_mask:
"0x1FF = (mask 9 :: 'a::len word)"
by (simp add: mask_eq_decr_exp)
lemma ucast_of_nat_small:
"x < 2 ^ LENGTH('a) ⟹ ucast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)"
apply transfer
apply (auto simp add: take_bit_of_nat min_def not_le)
apply (metis linorder_not_less min_def take_bit_nat_eq_self take_bit_take_bit)
done
lemma word_le_make_less:
fixes x :: "'a :: len word"
shows "y ≠ -1 ⟹ (x ≤ y) = (x < (y + 1))"
apply safe
apply (erule plus_one_helper2)
apply (simp add: eq_diff_eq[symmetric])
done
lemmas finite_word = finite [where 'a="'a::len word"]
lemma word_to_1_set:
"{0 ..< (1 :: 'a :: len word)} = {0}"
by fastforce
lemma word_leq_minus_one_le:
fixes x :: "'a::len word"
shows "⟦y ≠ 0; x ≤ y - 1 ⟧ ⟹ x < y"
using le_m1_iff_lt word_neq_0_conv by blast
lemma word_count_from_top:
"n ≠ 0 ⟹ {0 ..< n :: 'a :: len word} = {0 ..< n - 1} ∪ {n - 1}"
apply (rule set_eqI, rule iffI)
apply simp
apply (drule word_le_minus_one_leq)
apply (rule disjCI)
apply simp
apply simp
apply (erule word_leq_minus_one_le)
apply fastforce
done
lemma word_minus_one_le_leq:
"⟦ x - 1 < y ⟧ ⟹ x ≤ (y :: 'a :: len word)"
apply (cases "x = 0")
apply simp
apply (simp add: word_less_nat_alt word_le_nat_alt)
apply (subst(asm) unat_minus_one)
apply (simp add: word_less_nat_alt)
apply (cases "unat x")
apply (simp add: unat_eq_zero)
apply arith
done
lemma word_must_wrap:
"⟦ x ≤ n - 1; n ≤ x ⟧ ⟹ n = (0 :: 'a :: len word)"
using dual_order.trans sub_wrap word_less_1 by blast
lemma range_subset_card:
"⟦ {a :: 'a :: len word .. b} ⊆ {c .. d}; b ≥ a ⟧ ⟹ d ≥ c ∧ d - c ≥ b - a"
using word_sub_le word_sub_mono by fastforce
lemma less_1_simp:
"n - 1 < m = (n ≤ (m :: 'a :: len word) ∧ n ≠ 0)"
by unat_arith
lemma word_power_mod_div:
fixes x :: "'a::len word"
shows "⟦ n < LENGTH('a); m < LENGTH('a)⟧
⟹ x mod 2 ^ n div 2 ^ m = x div 2 ^ m mod 2 ^ (n - m)"
apply (simp add: word_arith_nat_div unat_mod power_mod_div)
apply (subst unat_arith_simps(3))
apply (subst unat_mod)
apply (subst unat_of_nat)+
apply (simp add: mod_mod_power min.commute)
done
lemma word_range_minus_1':
fixes a :: "'a :: len word"
shows "a ≠ 0 ⟹ {a - 1<..b} = {a..b}"
by (simp add: greaterThanAtMost_def atLeastAtMost_def greaterThan_def atLeast_def less_1_simp)
lemma word_range_minus_1:
fixes a :: "'a :: len word"
shows "b ≠ 0 ⟹ {a..b - 1} = {a..<b}"
apply (simp add: atLeastLessThan_def atLeastAtMost_def atMost_def lessThan_def)
apply (rule arg_cong [where f = "λx. {a..} ∩ x"])
apply rule
apply clarsimp
apply (erule contrapos_pp)
apply (simp add: linorder_not_less linorder_not_le word_must_wrap)
apply (clarsimp)
apply (drule word_le_minus_one_leq)
apply (auto simp: word_less_sub_1)
done
lemma ucast_nat_def:
"of_nat (unat x) = (ucast :: 'a :: len word ⇒ 'b :: len word) x"
by transfer simp
lemma overflow_plus_one_self:
"(1 + p ≤ p) = (p = (-1 :: 'a :: len word))"
apply rule
apply (rule ccontr)
apply (drule plus_one_helper2)
apply (rule notI)
apply (drule arg_cong[where f="λx. x - 1"])
apply simp
apply (simp add: field_simps)
apply simp
done
lemma plus_1_less:
"(x + 1 ≤ (x :: 'a :: len word)) = (x = -1)"
apply (rule iffI)
apply (rule ccontr)
apply (cut_tac plus_one_helper2[where x=x, OF order_refl])
apply simp
apply clarsimp
apply (drule arg_cong[where f="λx. x - 1"])
apply simp
apply simp
done
lemma pos_mult_pos_ge:
"[|x > (0::int); n>=0 |] ==> n * x >= n*1"
apply (simp only: mult_left_mono)
done
lemma word_plus_strict_mono_right:
fixes x :: "'a :: len word"
shows "⟦y < z; x ≤ x + z⟧ ⟹ x + y < x + z"
by unat_arith
lemma word_div_mult:
"0 < c ⟹ a < b * c ⟹ a div c < b" for a b c :: "'a::len word"
by (rule classical)
(use div_to_mult_word_lt [of b a c] in
‹auto simp add: word_less_nat_alt word_le_nat_alt unat_div›)
lemma word_less_power_trans_ofnat:
"⟦n < 2 ^ (m - k); k ≤ m; m < LENGTH('a)⟧
⟹ of_nat n * 2 ^ k < (2::'a::len word) ^ m"
apply (subst mult.commute)
apply (rule word_less_power_trans)
apply (simp_all add: word_less_nat_alt unsigned_of_nat)
using take_bit_nat_less_eq_self
apply (rule le_less_trans)
apply assumption
done
lemma word_1_le_power:
"n < LENGTH('a) ⟹ (1 :: 'a :: len word) ≤ 2 ^ n"
by (rule inc_le[where i=0, simplified], erule iffD2[OF p2_gt_0])
lemma unat_1_0:
"1 ≤ (x::'a::len word) = (0 < unat x)"
by (auto simp add: word_le_nat_alt)
lemma x_less_2_0_1':
fixes x :: "'a::len word"
shows "⟦LENGTH('a) ≠ 1; x < 2⟧ ⟹ x = 0 ∨ x = 1"
apply (cases ‹2 ≤ LENGTH('a)›; simp)
apply transfer
apply clarsimp
apply (metis add.commute add.right_neutral even_two_times_div_two mod_div_trivial
mod_pos_pos_trivial mult.commute mult_zero_left not_less not_take_bit_negative
odd_two_times_div_two_succ)
done
lemmas word_add_le_iff2 = word_add_le_iff [folded no_olen_add_nat]
lemma of_nat_power:
shows "⟦ p < 2 ^ x; x < len_of TYPE ('a) ⟧ ⟹ of_nat p < (2 :: 'a :: len word) ^ x"
apply (rule order_less_le_trans)
apply (rule of_nat_mono_maybe)
apply (erule power_strict_increasing)
apply simp
apply assumption
apply (simp add: word_unat_power del: of_nat_power)
done
lemma of_nat_n_less_equal_power_2:
"n < LENGTH('a::len) ⟹ ((of_nat n)::'a word) < 2 ^ n"
apply (induct n)
apply clarsimp
apply clarsimp
apply (metis of_nat_power n_less_equal_power_2 of_nat_Suc power_Suc)
done
lemma eq_mask_less:
fixes w :: "'a::len word"
assumes eqm: "w = w AND mask n"
and sz: "n < len_of TYPE ('a)"
shows "w < (2::'a word) ^ n"
by (subst eqm, rule and_mask_less' [OF sz])
lemma of_nat_mono_maybe':
fixes Y :: "nat"
assumes xlt: "x < 2 ^ len_of TYPE ('a)"
assumes ylt: "y < 2 ^ len_of TYPE ('a)"
shows "(y < x) = (of_nat y < (of_nat x :: 'a :: len word))"
apply (subst word_less_nat_alt)
apply (subst unat_of_nat)+
apply (subst mod_less)
apply (rule ylt)
apply (subst mod_less)
apply (rule xlt)
apply simp
done
lemma of_nat_mono_maybe_le:
"⟦x < 2 ^ LENGTH('a); y < 2 ^ LENGTH('a)⟧ ⟹
(y ≤ x) = ((of_nat y :: 'a :: len word) ≤ of_nat x)"
apply (clarsimp simp: le_less)
apply (rule disj_cong)
apply (rule of_nat_mono_maybe', assumption+)
apply auto
using of_nat_inj apply blast
done
lemma mask_AND_NOT_mask:
"(w AND NOT (mask n)) AND mask n = 0"
for w :: ‹'a::len word›
by (rule bit_word_eqI) (simp add: bit_simps)
lemma AND_NOT_mask_plus_AND_mask_eq:
"(w AND NOT (mask n)) + (w AND mask n) = w"
for w :: ‹'a::len word›
apply (subst disjunctive_add)
apply (auto simp add: bit_simps)
apply (rule bit_word_eqI)
apply (auto simp add: bit_simps)
done
lemma mask_eqI:
fixes x :: "'a :: len word"
assumes m1: "x AND mask n = y AND mask n"
and m2: "x AND NOT (mask n) = y AND NOT (mask n)"
shows "x = y"
proof -
have *: ‹x = x AND mask n OR x AND NOT (mask n)› for x