Theory Word_Lemmas_Internal
section "More Word Lemmas"
text ‹
This is a holding area for Word utility lemmas that are too specific or unpolished for the
AFP, but which are reusable enough to be collected together for the rest of L4V. New
utility lemmas that only prove facts about words should be added here (in preference to being
kept where they were first needed).
›
theory Word_Lemmas_Internal
imports
Word_Lib.Word_Lemmas
Word_Lib.More_Word_Operations
Word_Lib.Many_More
Word_Lib.Word_Syntax
Word_Lib.Syntax_Bundles
begin
unbundle bit_operations_syntax
unbundle bit_projection_infix_syntax
lemmas shiftl_nat_def = push_bit_eq_mult[of _ a for a::nat, folded shiftl_def]
lemmas shiftr_nat_def = drop_bit_eq_div[of _ a for a::nat, folded shiftr_def]
declare bit_simps[simp]
lemma signed_ge_zero_scast_eq_ucast:
"0 <=s x ⟹ scast x = ucast x"
by (simp add: scast_eq_ucast word_sle_msb_le)
lemma disjCI2:
"(¬ P ⟹ Q) ⟹ P ∨ Q"
by blast
lemma nat_diff_diff_le_lhs:
"a + c - b ≤ d ⟹ a - (b - c) ≤ (d :: nat)"
by arith
lemma is_aligned_obvious_no_wrap':
"⟦ is_aligned ptr sz; x = 2 ^ sz - 1 ⟧
⟹ ptr ≤ ptr + x"
by (fastforce simp: field_simps intro: is_aligned_no_overflow)
lemmas add_ge0_weak = add_increasing[where 'a=int and b=0]
lemmas aligned_sub_aligned = Aligned.aligned_sub_aligned'
lemma minus_minus_swap:
"⟦ a ≤ c; b ≤ d; b ≤ a; d ≤ c ; (d :: nat) - b = c - a ⟧
⟹ a - b = c - d"
by arith
lemma minus_minus_swap':
"⟦ c ≤ a; d ≤ b; b ≤ a; d ≤ c ; (b :: nat) - d = a - c ⟧
⟹ a - b = c - d"
by arith
lemmas word_le_mask_eq = le_mask_imp_and_mask
lemma int_and_leR:
"0 ≤ b ⟹ a AND b ≤ (b :: int)"
by (rule AND_upper2)
lemma int_and_leL:
"0 ≤ a ⟹ a AND b ≤ (a :: int)"
by (rule AND_upper1)
lemma if_then_1_else_0:
"(if P then 1 else 0) = (0 :: 'a :: zero_neq_one) ⟷ ¬P"
by (simp split: if_split)
lemma if_then_0_else_1:
"(if P then 0 else 1) = (0 :: 'a :: zero_neq_one) ⟷ P"
by simp
lemmas if_then_simps = if_then_0_else_1 if_then_1_else_0
lemma createNewCaps_guard:
fixes x :: "'a :: len word"
shows "⟦ unat x = c; b < 2 ^ LENGTH('a) ⟧
⟹ (n < of_nat b ∧ n < x) = (n < of_nat (min (min b c) c))"
by (metis (no_types) min_less_iff_conj nat_neq_iff unat_less_helper unat_ucast_less_no_overflow
unsigned_less word_unat.Rep_inverse)
lemma bits_2_subtract_ineq:
"i < (n :: ('a :: len) word)
⟹ 2 ^ bits + 2 ^ bits * unat (n - (1 + i)) = unat (n - i) * 2 ^ bits"
apply (simp add: unat_sub word_minus_one_le_leq)
apply (subst unatSuc)
apply clarsimp
apply unat_arith
apply (simp only: mult_Suc_right[symmetric])
apply (rule trans[OF mult.commute], rule arg_cong2[where f="(*)"], simp_all)
apply (simp add: word_less_nat_alt)
done
lemmas double_neg_mask = neg_mask_combine
lemmas int_unat = uint_nat[symmetric]
lemmas word_sub_mono3 = word_plus_mcs_4'
lemma shift_distinct_helper:
"⟦ (x :: 'a :: len word) < bnd; y < bnd; x ≠ y; x << n = y << n; n < LENGTH('a);
bnd - 1 ≤ 2 ^ (LENGTH('a) - n) - 1 ⟧
⟹ P"
apply (cases "n = 0")
apply simp
apply (drule word_plus_mono_right[where x=1])
apply simp_all
apply (subst word_le_sub1)
apply (rule power_not_zero)
apply simp
apply simp
apply (drule(1) order_less_le_trans)+
apply (clarsimp simp: bang_eq)
subgoal for na
apply (drule_tac x="na + n" in spec)
apply (simp add: nth_shiftl)
apply (cases "na + n < LENGTH('a)", simp_all)
apply safe
apply (drule(1) nth_bounded)
apply simp
apply simp
apply (drule(1) nth_bounded)
apply simp
apply simp
done
done
lemma of_nat_shift_distinct_helper:
"⟦ x < bnd; y < bnd; x ≠ y; (of_nat x :: 'a :: len word) << n = of_nat y << n;
n < LENGTH('a); bnd ≤ 2 ^ (LENGTH('a) - n) ⟧
⟹ P"
apply (cases "n = 0")
apply (simp add: word_unat.Abs_inject unats_def)
apply (subgoal_tac "bnd < 2 ^ LENGTH('a)")
apply (erule(1) shift_distinct_helper[rotated, rotated, rotated])
defer
apply (erule(1) of_nat_mono_maybe[rotated])
apply (erule(1) of_nat_mono_maybe[rotated])
apply (simp add: word_unat.Abs_inject unats_def)
apply (erule order_le_less_trans)
apply (rule power_strict_increasing)
apply simp
apply simp
apply (fastforce simp: unat_of_nat_minus_1 word_less_nat_alt)
done
lemmas pre_helper2 = add_mult_in_mask_range[folded add_mask_fold]
lemma ptr_add_distinct_helper:
"⟦ ptr_add (p :: 'a :: len word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x ≠ y;
x < bnd; y < bnd; n < LENGTH('a);
bnd ≤ 2 ^ (LENGTH('a) - n) ⟧
⟹ P"
apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
shiftl_t2n[symmetric, simplified mult.commute])
using of_nat_shift_distinct_helper
by blast
lemma unat_sub_le_strg:
"unat v ≤ v2 ∧ x ≤ v ∧ y ≤ v ∧ y < (x :: ('a :: len) word)
⟶ unat (x + (- 1 - y)) ≤ v2"
apply clarsimp
apply (erule order_trans[rotated])
apply (fold word_le_nat_alt)
apply (rule order_trans[rotated], assumption)
apply (rule order_trans[rotated], rule word_sub_le[where y="y + 1"])
apply (erule Word.inc_le)
apply (simp add: field_simps)
done
lemma multi_lessD:
"⟦ (a :: nat) * b < c; 0 < a; 0 < b ⟧
⟹ a < c ∧ b < c"
by (cases a, simp_all,cases b,simp_all)
lemmas leq_high_bits_shiftr_low_bits_leq_bits =
leq_high_bits_shiftr_low_bits_leq_bits_mask[unfolded mask_2pm1[of high_bits]]
lemmas unat_le_helper = word_unat_less_le
lemmas word_of_nat_plus = of_nat_add[where 'a="'a :: len word"]
lemmas word_of_nat_minus = of_nat_diff[where 'a="'a :: len word"]
lemma word_up_bound:
"(ptr :: 'a :: len word) ≤ 2 ^ LENGTH('a) - 1 "
by auto
lemma base_length_minus_one_inequality:
assumes foo: "wbase ≤ 2 ^ sz - 1"
"1 ≤ (wlength :: ('a :: len) word)"
"wlength ≤ 2 ^ sz - wbase"
"sz < LENGTH ('a)"
shows "wbase ≤ wbase + wlength - 1"
proof -
note sz_less = power_strict_increasing[OF foo(4), where a=2]
from foo have plus: "unat wbase + unat wlength < 2 ^ LENGTH('a)"
apply -
apply (rule order_le_less_trans[rotated], rule sz_less, simp)
apply (simp add: unat_arith_simps split: if_split_asm)
done
from foo show ?thesis
by (simp add: unat_arith_simps plus)
qed
lemmas from_bool_to_bool_and_1 = from_to_bool_last_bit[where x=r for r]
lemmas max_word_neq_0 = max_word_not_0
lemmas word_le_p2m1 = word_up_bound[where ptr=w for w]
lemma inj_ucast:
"⟦ uc = ucast; is_up uc ⟧
⟹ inj uc"
using down_ucast_inj is_up_down by blast
lemma ucast_eq_0[OF refl]:
"⟦ c = ucast; is_up c ⟧
⟹ (c x = 0) = (x = 0)"
by (metis uint_0_iff uint_up_ucast)
lemmas is_up_compose' = is_up_compose
lemma uint_is_up_compose:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
assumes "uc = ucast"
and "uc' = ucast"
and " uuc = uc' ∘ uc"
shows "⟦ is_up uc; is_up uc' ⟧
⟹ uint (uuc b) = uint b"
apply (simp add: assms)
apply (frule is_up_compose)
apply simp_all
apply (simp only: Word.uint_up_ucast)
done
lemma uint_is_up_compose_pred:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
assumes "uc = ucast" and "uc' = ucast" and " uuc = uc' ∘ uc"
shows "⟦ is_up uc; is_up uc' ⟧
⟹ P (uint (uuc b)) ⟷ P( uint b)"
apply (simp add: assms)
apply (frule is_up_compose)
apply simp_all
apply (simp only: Word.uint_up_ucast)
done
lemma is_down_up_sword:
fixes uc :: "'a :: len word ⇒ 'b :: len sword"
shows "⟦ uc = ucast; LENGTH('a) < LENGTH('b) ⟧
⟹ is_up uc = (¬ is_down uc)"
by (simp add: target_size source_size is_up_def is_down_def )
lemma is_not_down_compose:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
shows "⟦ uc = ucast; uc' = ucast; LENGTH('a) < LENGTH('c) ⟧
⟹ ¬ is_down (uc' ∘ uc)"
unfolding is_down_def
by (simp add: Word.target_size Word.source_size)
lemma sint_ucast_uint:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' ∘ uc "
and "LENGTH('a) < LENGTH('c signed)"
shows "⟦ is_up uc; is_up uc'⟧
⟹ sint (uuc b) = uint b"
apply (simp add: assms)
apply (frule is_up_compose')
apply simp_all
apply (simp add: ucast_ucast_b)
apply (rule sint_ucast_eq_uint)
apply (insert assms)
apply (simp add: is_down_def target_size source_size)
done
lemma sint_ucast_uint_pred:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
and uuc :: "'a word ⇒ 'c sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' ∘ uc "
and "LENGTH('a) < LENGTH('c )"
shows "⟦ is_up uc; is_up uc' ⟧
⟹ P (uint b) ⟷ P (sint (uuc b))"
apply (simp add: assms)
apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b])
apply (simp add: assms)
done
lemma sint_uucast_uint_uucast_pred:
fixes uc :: "'a :: len word ⇒ 'b :: len word"
and uc' :: "'b word ⇒ 'c :: len sword"
assumes "uc = ucast" and " uc' = ucast" and "uuc=uc' ∘ uc "
and "LENGTH('a) < LENGTH('c )"
shows "⟦ is_up uc; is_up uc' ⟧
⟹ P (uint(uuc b)) ⟷ P (sint (uuc b))"
apply (simp add: assms)
apply (insert sint_ucast_uint[where uc=uc and uc'=uc' and uuc=uuc and b = b])
apply (insert uint_is_up_compose_pred[where uc=uc and uc'=uc' and uuc=uuc and b=b])
apply (simp add: assms uint_is_up_compose_pred)
done
lemma unat_minus':
fixes x :: "'a :: len word"
shows "x ≠ 0 ⟹ unat (-x) = 2 ^ LENGTH('a) - unat x"
by (simp add: unat_minus wsst_TYs(3))
lemma word_nth_neq:
"n < LENGTH('a) ⟹ (~~ x :: 'a :: len word) !! n = (¬ x !! n)"
by (simp add: word_size word_ops_nth_size)
lemma word_wrap_of_natD:
fixes x :: "'a :: len word"
assumes wraps: "¬ x ≤ x + of_nat n"
shows "∃k. x + of_nat k = 0 ∧ k ≤ n"
proof -
show ?thesis
proof (rule exI [where x = "unat (- x)"], intro conjI)
show "x + of_nat (unat (-x)) = 0"
by simp
next
show "unat (-x) ≤ n"
proof (subst unat_minus')
from wraps show "x ≠ 0"
by (rule contrapos_pn, simp add: not_le)
next
show "2 ^ LENGTH('a) - unat x ≤ n" using wraps
apply (simp add: no_olen_add_nat le_diff_conv not_less)
apply (erule order_trans)
apply (simp add: unat_of_nat)
done
qed
qed
qed
lemma two_bits_cases:
"⟦ LENGTH('a) > 2; (x :: 'a :: len word) && 3 = 0 ⟹ P; x && 3 = 1 ⟹ P;
x && 3 = 2 ⟹ P; x && 3 = 3 ⟹ P ⟧
⟹ P"
apply (frule and_mask_cases[where n=2 and x=x, simplified mask_eq])
using upt_conv_Cons by auto[1]
lemma zero_OR_eq:
"y = 0 ⟹ (x || y) = x"
by simp
declare is_aligned_neg_mask_eq[simp]
declare is_aligned_neg_mask_weaken[simp]
lemmas mask_in_range = neg_mask_in_mask_range[folded add_mask_fold]
lemmas aligned_range_offset_mem = aligned_offset_in_range[folded add_mask_fold]
lemmas range_to_bl' = mask_range_to_bl'[folded add_mask_fold]
lemmas range_to_bl = mask_range_to_bl[folded add_mask_fold]
lemmas aligned_ranges_subset_or_disjoint = aligned_mask_range_cases[folded add_mask_fold]
lemmas aligned_range_offset_subset = aligned_mask_range_offset_subset[folded add_mask_fold]
lemmas aligned_diff = aligned_mask_diff[unfolded mask_2pm1]
lemmas aligned_ranges_subset_or_disjoint_coroll = aligned_mask_ranges_disjoint[folded add_mask_fold]
lemmas distinct_aligned_addresses_accumulate = aligned_mask_ranges_disjoint2[folded add_mask_fold]
lemmas bang_big = test_bit_over
lemma unat_and_mask_le:
"n < LENGTH('a) ⟹ unat (x && mask n) ≤ 2^n" for x::"'a::len word"
by (simp add: and_mask_less' order_less_imp_le unat_less_power)
lemma sign_extend_less_mask_idem:
"⟦ w ≤ mask n; n < size w ⟧ ⟹ sign_extend n w = w"
by (simp add: sign_extend_def le_mask_imp_and_mask le_mask_high_bits)
lemma word_and_le:
"a ≤ c ⟹ (a :: 'a :: len word) && b ≤ c"
by (subst and.commute) (erule word_and_le')
lemma le_smaller_mask:
"⟦ x ≤ mask n; n ≤ m ⟧ ⟹ x ≤ mask m" for x :: "'a::len word"
by (erule (1) order.trans[OF _ mask_mono])
lemma upcast_less_unat_less:
assumes less: "UCAST('a → 'b) x < UCAST('a → 'b) (of_nat y)"
assumes len: "LENGTH('a::len) ≤ LENGTH('b::len)"
assumes bound: "y < 2 ^ LENGTH('a)"
shows "unat x < y"
by (rule unat_mono[OF less, simplified unat_ucast_up_simp[OF len] unat_of_nat_eq[OF bound]])
lemma word_ctz_max:
"word_ctz w ≤ size w"
unfolding word_ctz_def
by (rule order_trans[OF List.length_takeWhile_le], clarsimp simp: word_size)
lemma scast_of_nat_small:
"x < 2 ^ (LENGTH('a) - 1) ⟹ scast (of_nat x :: 'a :: len word) = (of_nat x :: 'b :: len word)"
apply transfer
apply simp
by (metis One_nat_def id_apply int_eq_sint of_int_eq_id signed_of_nat)
lemmas casts_of_nat_small = ucast_of_nat_small scast_of_nat_small
definition list_while_len where
"list_while_len P n xs ≡ (∀i. i < n ⟶ i < length xs ⟶ P (xs ! i))
∧ (n < length xs ⟶ ¬ P (xs ! n))"
lemma list_while_len_iff_takeWhile_eq_take:
"list_while_len P n xs ⟷ takeWhile P xs = take n xs"
unfolding list_while_len_def
apply (rule iffI[OF takeWhile_eq_take_P_nth], simp+)
apply (intro conjI allI impI)
apply (rule takeWhile_take_has_property_nth, clarsimp)
apply (drule_tac f=length in arg_cong, simp)
apply (induct xs arbitrary: n; clarsimp split: if_splits)
done
lemma list_while_len_exists:
"∃n. list_while_len P n xs"
apply (induction xs; simp add: list_while_len_def)
apply (erule exE)
subgoal for x xs n
apply (cases "P x")
apply (rule exI[where x="Suc n"], clarsimp)
subgoal for i by (cases i; simp)
subgoal by (rule exI[where x=0], simp)
done
done
lemma takeWhile_truncate:
"length (takeWhile P xs) ≤ m
⟹ takeWhile P (take m xs) = takeWhile P xs"
apply (cut_tac list_while_len_exists[where P=P and xs=xs], clarsimp)
subgoal for n
apply (cases "n ≤ m")
apply (subgoal_tac "list_while_len P n (take m xs)")
apply(simp add: list_while_len_iff_takeWhile_eq_take)
apply (clarsimp simp: list_while_len_def)
apply (simp add: list_while_len_iff_takeWhile_eq_take)
done
done
lemma word_clz_shiftr_1:
fixes z::"'a::len word"
assumes wordsize: "1 < LENGTH('a)"
shows "z ≠ 0 ⟹ word_clz (z >> 1) = word_clz z + 1"
supply word_size [simp]
apply (clarsimp simp: word_clz_def)
using wordsize apply (subst bl_shiftr, simp)
apply (subst takeWhile_append2; simp add: wordsize)
apply (subst takeWhile_truncate)
using word_clz_nonzero_max[where w=z]
apply (clarsimp simp: word_clz_def)
apply simp+
done
lemma shiftr_Suc:
fixes x::"'a::len word"
shows "x >> (Suc n) = x >> n >> 1"
by (clarsimp simp: shiftr_shiftr)
lemma word_clz_shiftr:
fixes z :: "'a::len word"
shows "n < LENGTH('a) ⟹ mask n < z ⟹ word_clz (z >> n) = word_clz z + n"
apply (simp add: le_mask_iff Not_eq_iff[THEN iffD2, OF le_mask_iff, simplified not_le]
word_neq_0_conv)
apply (induction n; simp)
subgoal for n
apply (subgoal_tac "0 < z >> n")
apply (subst shiftr_Suc)
apply (subst word_clz_shiftr_1; simp)
apply (clarsimp simp: word_less_nat_alt shiftr_div_2n' div_mult2_eq)
apply (cases "unat z div 2 ^ n = 0"; simp)
apply (clarsimp simp: div_eq_0_iff)
done
done
lemma mask_to_bl_exists_True:
"x && mask n ≠ 0 ⟹ ∃m. (rev (to_bl x)) ! m ∧ m < n"
apply (subgoal_tac "¬(∀m. m < n ⟶ ¬(rev (to_bl x)) ! m)", fastforce)
apply (intro notI)
apply (subgoal_tac "x && mask n = 0", clarsimp)
apply (clarsimp simp: eq_zero_set_bl in_set_conv_nth)
apply (subst (asm) to_bl_nth, clarsimp simp: word_size)
apply (clarsimp simp: word_size)
by (meson nth_mask test_bit_bl word_and_nth)
lemma word_ctz_shiftr_1:
fixes z::"'a::len word"
assumes wordsize: "1 < LENGTH('a)"
shows "z ≠ 0 ⟹ 1 ≤ word_ctz z ⟹ word_ctz (z >> 1) = word_ctz z - 1"
supply word_size [simp]
apply (clarsimp simp: word_ctz_def)
using wordsize apply (subst bl_shiftr, simp)
apply (simp add: rev_take )
apply (subgoal_tac
"length (takeWhile Not (rev (to_bl z))) - Suc 0
= length (takeWhile Not (take 1 (rev (to_bl z)) @ drop 1 (rev (to_bl z)))) - Suc 0")
apply (subst (asm) takeWhile_append2)
apply clarsimp
apply (cases "rev (to_bl z)"; simp)
apply clarsimp
apply (subgoal_tac "∃m. (rev (to_bl z)) ! m ∧ m < LENGTH('a)", clarsimp)
subgoal for m
apply (cases m)
apply (cases "rev (to_bl z)"; simp)
subgoal for nat
apply (subst takeWhile_append1, subst in_set_conv_nth)
apply (rule exI[where x=nat])
apply (intro conjI)
apply (clarsimp simp: wordsize)
using wordsize apply linarith
apply (rule refl, clarsimp)
apply simp
done
done
apply (rule mask_to_bl_exists_True, simp)
apply simp
done
lemma word_ctz_bound_below_helper:
fixes x :: "'a::len word"
assumes sz: "n ≤ LENGTH('a)"
shows "x && mask n = 0
⟹ to_bl x = (take (LENGTH('a) - n) (to_bl x) @ replicate n False)"
apply (subgoal_tac "replicate n False = drop (LENGTH('a) - n) (to_bl x)")
apply (subgoal_tac "True ∉ set (drop (LENGTH('a) - n) (to_bl x))")
apply (drule list_of_false, clarsimp simp: sz)
apply (drule_tac sym[where t="drop n x" for n x], clarsimp)
apply (rule sym)
apply (rule is_aligned_drop; clarsimp simp: is_aligned_mask sz)
done
lemma word_ctz_bound_below:
fixes x :: "'a::len word"
assumes sz[simp]: "n ≤ LENGTH('a)"
shows "x && mask n = 0 ⟹ n ≤ word_ctz x"
apply (clarsimp simp: word_ctz_def)
apply (subst word_ctz_bound_below_helper[OF sz]; simp)
apply (subst takeWhile_append2; clarsimp)
done
lemma word_ctz_bound_above:
fixes x :: "'a::len word"
shows "x && mask n ≠ 0 ⟹ word_ctz x < n"
apply (cases "n ≤ LENGTH('a)")
apply (frule mask_to_bl_exists_True, clarsimp)
subgoal for m
apply (clarsimp simp: word_ctz_def)
apply (subgoal_tac "m < length ((rev (to_bl x)))")
apply (subst id_take_nth_drop[where xs="rev (to_bl x)"], assumption)
apply (subst takeWhile_tail, simp)
apply (rule order.strict_trans1)
apply (rule List.length_takeWhile_le)
apply simp
apply (erule order.strict_trans2, clarsimp)
done
apply (simp add: not_le)
apply (erule le_less_trans[OF word_ctz_max, simplified word_size])
done
lemma word_ctz_shiftr:
fixes z::"'a::len word"
assumes nz: "z ≠ 0"
shows "n < LENGTH('a) ⟹ n ≤ word_ctz z ⟹ word_ctz (z >> n) = word_ctz z - n"
apply (induction n; simp)
subgoal for n
apply (subst shiftr_Suc)
apply (subst word_ctz_shiftr_1, simp)
apply clarsimp
apply (subgoal_tac "word_ctz z < n", clarsimp)
apply (rule word_ctz_bound_above, clarsimp simp: word_size)
apply (subst (asm) and_mask_eq_iff_shiftr_0[symmetric], clarsimp simp: nz)
apply (rule word_ctz_bound_below, clarsimp simp: word_size)
apply (rule mask_zero)
apply (rule is_aligned_shiftr, simp add: is_aligned_mask)
apply (cases "z && mask (Suc n) = 0", simp)
apply (frule word_ctz_bound_above[rotated]; clarsimp simp: word_size)
apply simp
done
done
lemma word_less_max_simp:
fixes w :: "'a::len word"
assumes "max_w = -1"
shows "w ≤ max_w"
unfolding assms by simp
lemma word_and_mask_word_ctz_zero:
assumes "l = word_ctz w"
shows "w && mask l = 0"
unfolding word_ctz_def assms
apply (word_eqI)
apply (drule takeWhile_take_has_property_nth)
apply (simp add: test_bit_bl)
done
lemma word_ctz_len_word_and_mask_zero:
fixes w :: "'a::len word"
shows "word_ctz w = LENGTH('a) ⟹ w = 0"
by (drule sym, drule word_and_mask_word_ctz_zero, simp)
lemma word_le_1:
fixes w :: "'a::len word"
shows "w ≤ 1 ⟷ w = 0 ∨ w = 1"
using dual_order.antisym lt1_neq0 word_zero_le by blast
lemma less_ucast_ucast_less':
"x < UCAST('b → 'a) y ⟹ UCAST('a → 'b) x < y"
for x :: "'a::len word" and y :: "'b::len word"
by (clarsimp simp: order.strict_iff_order dual_order.antisym le_ucast_ucast_le)
lemma ucast_up_less_bounded_implies_less_ucast_down':
assumes len: "LENGTH('a::len) < LENGTH('b::len)"
assumes bound: "y < 2 ^ LENGTH('a)"
assumes less: "UCAST('a → 'b) x < y"
shows "x < UCAST('b → 'a) y"
apply (rule le_less_trans[OF _ ucast_mono[OF less bound]])
using len by (simp add: is_down ucast_down_ucast_id)
lemma ucast_up_less_bounded_iff_less_ucast_down':
assumes len: "LENGTH('a::len) < LENGTH('b::len)"
assumes bound: "y < 2 ^ LENGTH('a)"
shows "UCAST('a → 'b) x < y ⟷ x < UCAST('b → 'a) y"
apply (rule iffI)
prefer 2
apply (simp add: less_ucast_ucast_less')
using assms by (rule ucast_up_less_bounded_implies_less_ucast_down')
lemma word_of_int_word_of_nat_eqD:
"⟦ word_of_int x = (word_of_nat y :: 'a :: len word); 0 ≤ x; x < 2^LENGTH('a); y < 2^LENGTH('a) ⟧
⟹ nat x = y"
by (metis nat_eq_numeral_power_cancel_iff of_nat_inj word_of_int_nat zless2p zless_nat_conj)
lemma ucast_down_0:
"⟦ UCAST('a::len → 'b::len) x = 0; unat x < 2^LENGTH('b) ⟧ ⟹ x = 0"
by (metis Word.of_nat_unat unat_0 unat_eq_of_nat word_unat_eq_iff)
lemma uint_minus_1_eq:
‹uint (- 1 :: 'a word) = 2 ^ LENGTH('a::len) - 1›
by transfer (simp add: mask_eq_exp_minus_1)
lemma FF_eq_minus_1:
‹0xFF = (- 1 :: 8 word)›
by simp
lemma shiftl_t2n':
"w << n = w * (2 ^ n)" for w :: "'a::len word"
by (simp add: shiftl_t2n)
end