(* Title: HOL/Library/Word.thy Author: Jeremy Dawson and Gerwin Klein, NICTA, et. al. *)
section‹A type of finite bit strings›
theory Word imports "HOL-Library.Type_Length" begin
subsection‹Preliminaries›
lemma signed_take_bit_decr_length_iff: ‹signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l ⟷ take_bit LENGTH('a) k = take_bit LENGTH('a) l› by (simp add: signed_take_bit_eq_iff_take_bit_eq)
subsection‹Fundamentals›
subsubsection ‹Type definition›
quotient_type (overloaded) 'a word = int / ‹λk l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l› morphisms rep Word by (auto intro!: equivpI reflpI sympI transpI)
hide_const (open) rep 🍋‹only for foundational purpose›
hide_const (open) Word 🍋‹only for code generation›
subsubsection ‹Basic arithmetic›
instantiation word :: (len) comm_ring_1 begin
lift_definition zero_word :: ‹'a word› is 0 .
lift_definition one_word :: ‹'a word› is 1 .
lift_definition plus_word :: ‹'a word ==> 'a word ==> 'a word› is‹(+)› by (auto simp: take_bit_eq_mod intro: mod_add_cong)
lift_definition minus_word :: ‹'a word ==> 'a word ==> 'a word› is‹(-)› by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
lift_definition uminus_word :: ‹'a word ==> 'a word› is uminus by (auto simp: take_bit_eq_mod intro: mod_minus_cong)
lift_definition times_word :: ‹'a word ==> 'a word ==> 'a word› is‹(*)\ by (auto simp: take_bit_eq_mod intro: mod_mult_cong) instance by (standard; transfer) (simp_all add: algebra_simps) end context includes lifting_syntax notes power_transfer [transfer_rule] transfer_rule_of_bool [transfer_rule] transfer_rule_numeral [transfer_rule] transfer_rule_of_nat [transfer_rule] transfer_rule_of_int [transfer_rule] begin lemma power_transfer_word [transfer_rule]: ‹(pcr_word ===> (=) ===> pcr_word) (^) (^)› by transfer_prover lemma [transfer_rule]: ‹((=) ===> pcr_word) of_bool of_bool› by transfer_prover lemma [transfer_rule]: ‹((=) ===> pcr_word) numeral numeral› by transfer_prover lemma [transfer_rule]: ‹((=) ===> pcr_word) int of_nat› by transfer_prover lemma [transfer_rule]: ‹((=) ===> pcr_word) (λk. k) of_int› proof - have ‹((=) ===> pcr_word) of_int of_int› by transfer_prover then show ?thesis by (simp add: id_def) qed lemma [transfer_rule]: ‹(pcr_word ===> (⟷)) even ((dvd) 2 :: 'a::len word ==> bool)› proof - have even_word_unfold: "even k ⟷ (∃l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P ⟷ ?Q") for k :: int by (metis dvd_triv_left evenE even_take_bit_eq len_not_eq_0) show ?thesis unfolding even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def] by transfer_prover qed end lemma exp_eq_zero_iff [simp]: ‹2 ^ n = (0 :: 'a::len word) ⟷ n ≥ LENGTH('a)› by transfer auto lemma word_exp_length_eq_0 [simp]: ‹(2 :: 'a::len word) ^ LENGTH('a) = 0› by simp subsubsection ‹Basic tool setup› ML_file ‹Tools/word_lib.ML› subsubsection ‹Basic code generation setup› context begin qualified lift_definition the_int :: ‹'a::len word ==> int› is ‹take_bit LENGTH('a)›. end lemma [code abstype]: ‹Word.Word (Word.the_int w) = w› by transfer simp lemma Word_eq_word_of_int [code_post, simp]: ‹Word.Word = of_int› by (rule; transfer) simp quickcheck_generator word constructors: ‹0 :: 'a::len word›, ‹numeral :: num ==> 'a::len word› instantiation word :: (len) equal begin lift_definition equal_word :: ‹'a word ==> 'a word ==> bool› is ‹λk l. take_bit LENGTH('a) k = take_bit LENGTH('a) l› by simp instance by (standard; transfer) rule end lemma [code]: ‹HOL.equal v w ⟷ HOL.equal (Word.the_int v) (Word.the_int w)› by transfer (simp add: equal) lemma [code]: ‹Word.the_int 0 = 0› by transfer simp lemma [code]: ‹Word.the_int 1 = 1› by transfer simp lemma [code]: ‹Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)› for v w :: ‹'a::len word› by transfer (simp add: take_bit_add) lemma [code]: ‹Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)› for w :: ‹'a::len word› by transfer (auto simp: take_bit_eq_mod zmod_zminus1_eq_if) lemma [code]: ‹Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)› for v w :: ‹'a::len word› by transfer (simp add: take_bit_diff) lemma [code]: ‹Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)› for v w :: ‹'a::len word› by transfer (simp add: take_bit_mult) subsubsection ‹Basic conversions› abbreviation word_of_nat :: ‹nat ==> 'a::len word› where ‹word_of_nat ≡ of_nat› abbreviation word_of_int :: ‹int ==> 'a::len word› where ‹word_of_int ≡ of_int› lemma word_of_nat_eq_iff: ‹word_of_nat m = (word_of_nat n :: 'a::len word) ⟷ take_bit LENGTH('a) m = take_bit LENGTH('a) n› by transfer (simp add: take_bit_of_nat) lemma word_of_int_eq_iff: ‹word_of_int k = (word_of_int l :: 'a::len word) ⟷ take_bit LENGTH('a) k = take_bit LENGTH('a) l› by transfer rule lemma word_of_nat_eq_0_iff: ‹word_of_nat n = (0 :: 'a::len word) ⟷ 2 ^ LENGTH('a) dvd n› using word_of_nat_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) lemma word_of_int_eq_0_iff: ‹word_of_int k = (0 :: 'a::len word) ⟷ 2 ^ LENGTH('a) dvd k› using word_of_int_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) context semiring_1 begin lift_definition unsigned :: ‹'b::len word ==> 'a› is ‹of_nat ∘ nat ∘ take_bit LENGTH('b)› by simp lemma unsigned_0 [simp]: ‹unsigned 0 = 0› by transfer simp lemma unsigned_1 [simp]: ‹unsigned 1 = 1› by transfer simp lemma unsigned_numeral [simp]: ‹unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))› by transfer (simp add: nat_take_bit_eq) lemma unsigned_neg_numeral [simp]: ‹unsigned (- numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) (- numeral n)))› by transfer simp end context semiring_1 begin lemma unsigned_of_nat: ‹unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)› by transfer (simp add: nat_eq_iff take_bit_of_nat) lemma unsigned_of_int: ‹unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))› by transfer simp end context semiring_char_0 begin lemma unsigned_word_eqI: ‹v = w›if ‹unsigned v = unsigned w› using that by transfer (simp add: eq_nat_nat_iff) lemma word_eq_iff_unsigned: ‹v = w ⟷ unsigned v = unsigned w› by (auto intro: unsigned_word_eqI) lemma inj_unsigned [simp]: ‹inj unsigned› by (rule injI) (simp add: unsigned_word_eqI) lemma unsigned_eq_0_iff: ‹unsigned w = 0 ⟷ w = 0› using word_eq_iff_unsigned [of w 0] by simp end context ring_1 begin lift_definition signed :: ‹'b::len word ==> 'a› is ‹of_int ∘ signed_take_bit (LENGTH('b) - Suc 0)› by (simp flip: signed_take_bit_decr_length_iff) lemma signed_0 [simp]: ‹signed 0 = 0› by transfer simp lemma signed_1 [simp]: ‹signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)› by (transfer fixing: uminus; cases ‹LENGTH('b)›) (auto dest: gr0_implies_Suc) lemma signed_minus_1 [simp]: ‹signed (- 1 :: 'b::len word) = - 1› by (transfer fixing: uminus) simp lemma signed_numeral [simp]: ‹signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (numeral n))› by transfer simp lemma signed_neg_numeral [simp]: ‹signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))› by transfer simp lemma signed_of_nat: ‹signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))› by transfer simp lemma signed_of_int: ‹signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)› by transfer simp end context ring_char_0 begin lemma signed_word_eqI: ‹v = w›if ‹signed v = signed w› using that by transfer (simp flip: signed_take_bit_decr_length_iff) lemma word_eq_iff_signed: ‹v = w ⟷ signed v = signed w› by (auto intro: signed_word_eqI) lemma inj_signed [simp]: ‹inj signed› by (rule injI) (simp add: signed_word_eqI) lemma signed_eq_0_iff: ‹signed w = 0 ⟷ w = 0› using word_eq_iff_signed [of w 0] by simp end abbreviation unat :: ‹'a::len word ==> nat› where ‹unat ≡ unsigned› abbreviation uint :: ‹'a::len word ==> int› where ‹uint ≡ unsigned› abbreviation sint :: ‹'a::len word ==> int› where ‹sint ≡ signed› abbreviation ucast :: ‹'a::len word ==> 'b::len word› where ‹ucast ≡ unsigned› abbreviation scast :: ‹'a::len word ==> 'b::len word› where ‹scast ≡ signed› context includes lifting_syntax begin lemma [transfer_rule]: ‹(pcr_word ===> (=)) (nat ∘ take_bit LENGTH('a)) (unat :: 'a::len word ==> nat)› using unsigned.transfer [where ?'a = nat] by simp lemma [transfer_rule]: ‹(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word ==> int)› using unsigned.transfer [where ?'a = int] by (simp add: comp_def) lemma [transfer_rule]: ‹(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word ==> int)› using signed.transfer [where ?'a = int] by simp lemma [transfer_rule]: ‹(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word ==> 'b::len word)› proof (rule rel_funI) fix k :: int and w :: ‹'a word› assume ‹pcr_word k w› then have ‹w = word_of_int k› by (simp add: pcr_word_def cr_word_def relcompp_apply) moreover have ‹pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))› by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) ultimately show ‹pcr_word (take_bit LENGTH('a) k) (ucast w)› by simp qed lemma [transfer_rule]: ‹(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word ==> 'b::len word)› proof (rule rel_funI) fix k :: int and w :: ‹'a word› assume ‹pcr_word k w› then have ‹w = word_of_int k› by (simp add: pcr_word_def cr_word_def relcompp_apply) moreover have ‹pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))› by transfer (simp add: pcr_word_def cr_word_def relcompp_apply) ultimately show ‹pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)› by simp qed end lemma of_nat_unat [simp]: ‹of_nat (unat w) = unsigned w› by transfer simp lemma of_int_uint [simp]: ‹of_int (uint w) = unsigned w› by transfer simp lemma of_int_sint [simp]: ‹of_int (sint a) = signed a› by transfer (simp_all add: take_bit_signed_take_bit) lemma nat_uint_eq [simp]: ‹nat (uint w) = unat w› by transfer simp lemma nat_of_natural_unsigned_eq [simp]: ‹nat_of_natural (unsigned w) = unat w› by transfer simp lemma int_of_integer_unsigned_eq [simp]: ‹int_of_integer (unsigned w) = uint w› by transfer simp lemma int_of_integer_signed_eq [simp]: ‹int_of_integer (signed w) = sint w› by transfer simp lemma sgn_uint_eq [simp]: ‹sgn (uint w) = of_bool (w ≠ 0)› by transfer (simp add: less_le) text ‹Aliasses only for code generation› context begin qualified lift_definition of_int :: ‹int ==> 'a::len word› is ‹take_bit LENGTH('a)›. qualified lift_definition of_nat :: ‹nat ==> 'a::len word› is ‹int ∘ take_bit LENGTH('a)›. qualified lift_definition the_nat :: ‹'a::len word ==> nat› is ‹nat ∘ take_bit LENGTH('a)›by simp qualified lift_definition the_signed_int :: ‹'a::len word ==> int› is ‹signed_take_bit (LENGTH('a) - Suc 0)›by (simp add: signed_take_bit_decr_length_iff) qualified lift_definition cast :: ‹'a::len word ==> 'b::len word› is ‹take_bit LENGTH('a)›by simp qualified lift_definition signed_cast :: ‹'a::len word ==> 'b::len word› is ‹signed_take_bit (LENGTH('a) - Suc 0)›by (metis signed_take_bit_decr_length_iff) end lemma [code_abbrev, simp]: ‹Word.the_int = uint› by transfer rule lemma [code]: ‹Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k› by transfer simp lemma [code_abbrev, simp]: ‹Word.of_int = word_of_int› by (rule; transfer) simp lemma [code]: ‹Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int n)› by transfer (simp add: take_bit_of_nat) lemma [code_abbrev, simp]: ‹Word.of_nat = word_of_nat› by (rule; transfer) (simp add: take_bit_of_nat) lemma [code]: ‹Word.the_nat w = nat (Word.the_int w)› by transfer simp lemma [code_abbrev, simp]: ‹Word.the_nat = unat› by (rule; transfer) simp lemma [code]: ‹Word.the_signed_int w = (let k = Word.the_int w in if bit k (LENGTH('a) - Suc 0) then k + push_bit LENGTH('a) (- 1) else k)› for w :: ‹'a::len word› by transfer (simp add: bit_simps signed_take_bit_eq_take_bit_add) lemma [code_abbrev, simp]: ‹Word.the_signed_int = sint› by (rule; transfer) simp lemma [code]: ‹Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)› for w :: ‹'a::len word› by transfer simp lemma [code_abbrev, simp]: ‹Word.cast = ucast› by (rule; transfer) simp lemma [code]: ‹Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)› for w :: ‹'a::len word› by transfer simp lemma [code_abbrev, simp]: ‹Word.signed_cast = scast› by (rule; transfer) simp lemma [code]: ‹unsigned w = of_nat (nat (Word.the_int w))› by transfer simp lemma [code]: ‹signed w = of_int (Word.the_signed_int w)› by transfer simp subsection ‹Elementary case distinctions› lemma word_length_one [case_names zero minus_one length_beyond]: fixes w :: ‹'a::len word› obtains (zero) ‹LENGTH('a) = Suc 0›‹w = 0› | (minus_one) ‹LENGTH('a) = Suc 0›‹w = - 1› | (length_beyond) ‹2 ≤ LENGTH('a)› proof (cases ‹2 ≤ LENGTH('a)›) case True with length_beyond show ?thesis . next case False then have ‹LENGTH('a) = Suc 0› by simp then have ‹w = 0 ∨ w = - 1› by transfer auto with ‹LENGTH('a) = Suc 0›zero minus_one show ?thesis by blast qed subsubsection ‹Basic ordering› instantiation word :: (len) linorder begin lift_definition less_eq_word :: "'a word ==> 'a word ==> bool" is "λa b. take_bit LENGTH('a) a ≤ take_bit LENGTH('a) b" by simp lift_definition less_word :: "'a word ==> 'a word ==> bool" is "λa b. take_bit LENGTH('a) a 🚫 LENGTH('a) b" by simp instance by (standard; transfer) auto end interpretation word_order: ordering_top ‹(≤)›‹(🚫›‹- 1 :: 'a::len word› by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1) interpretation word_coorder: ordering_top ‹(≥)›‹(>)›‹0 :: 'a::len word› by (standard; transfer) simp lemma word_of_nat_less_eq_iff: ‹word_of_nat m ≤ (word_of_nat n :: 'a::len word) ⟷ take_bit LENGTH('a) m ≤ take_bit LENGTH('a) n› by transfer (simp add: take_bit_of_nat) lemma word_of_int_less_eq_iff: ‹word_of_int k ≤ (word_of_int l :: 'a::len word) ⟷ take_bit LENGTH('a) k ≤ take_bit LENGTH('a) l› by transfer rule lemma word_of_nat_less_iff: ‹word_of_nat m 🚫word_of_nat n :: 'a::len word) ⟷ take_bit LENGTH('a) m 🚫 LENGTH('a) n› by transfer (simp add: take_bit_of_nat) lemma word_of_int_less_iff: ‹word_of_int k 🚫word_of_int l :: 'a::len word) ⟷ take_bit LENGTH('a) k 🚫 LENGTH('a) l› by transfer rule lemma word_le_def [code]: "a ≤ b ⟷ uint a ≤ uint b" by transfer rule lemma word_less_def [code]: "a 🚫⟷ uint a 🚫 b" by transfer rule lemma word_greater_zero_iff: ‹a > 0 ⟷ a ≠ 0›for a :: ‹'a::len word› by transfer (simp add: less_le) lemma of_nat_word_less_eq_iff: ‹of_nat m ≤ (of_nat n :: 'a::len word) ⟷ take_bit LENGTH('a) m ≤ take_bit LENGTH('a) n› by transfer (simp add: take_bit_of_nat) lemma of_nat_word_less_iff: ‹of_nat m 🚫of_nat n :: 'a::len word) ⟷ take_bit LENGTH('a) m 🚫 LENGTH('a) n› by transfer (simp add: take_bit_of_nat) lemma of_int_word_less_eq_iff: ‹of_int k ≤ (of_int l :: 'a::len word) ⟷ take_bit LENGTH('a) k ≤ take_bit LENGTH('a) l› by transfer rule lemma of_int_word_less_iff: ‹of_int k 🚫of_int l :: 'a::len word) ⟷ take_bit LENGTH('a) k 🚫 LENGTH('a) l› by transfer rule instantiation word :: (len) order_bot begin lift_definition bot_word :: ‹'a word› is 0 . instance by (standard; transfer) simp end lemma bot_word_eq: ‹bot = (0 :: 'a::len word)› by transfer rule instantiation word :: (len) order_top begin lift_definition top_word :: ‹'a word› is ‹- 1›. instance by (standard; transfer) (simp add: take_bit_int_less_eq_mask) end lemma top_word_eq: ‹top = (- 1 :: 'a::len word)› by transfer rule subsection ‹Enumeration› lemma inj_on_word_of_nat: ‹inj_on (word_of_nat :: nat ==> 'a::len word) {0..🚫^ LENGTH('a)}› by (rule inj_onI; transfer) (simp_all add: take_bit_int_eq_self) lemma UNIV_word_eq_word_of_nat: ‹(UNIV :: 'a::len word set) = word_of_nat ` {0..🚫^ LENGTH('a)}›(is ‹_ = ?A›) proof show ‹word_of_nat ` {0..🚫^ LENGTH('a)} ⊆ UNIV› by simp show ‹UNIV ⊆ ?A› proof fix w :: ‹'a word› show ‹w ∈ (word_of_nat ` {0..🚫^ LENGTH('a)} :: 'a word set)› by (rule image_eqI [of _ _ ‹unat w›]; transfer) simp_all qed qed instantiation word :: (len) enum begin definition enum_word :: ‹'a word list› where ‹enum_word = map word_of_nat [0..🚫^ LENGTH('a)]› definition enum_all_word :: ‹('a word ==> bool) ==> bool› where ‹enum_all_word = All› definition enum_ex_word :: ‹('a word ==> bool) ==> bool› where ‹enum_ex_word = Ex› instance by standard (simp_all add: enum_all_word_def enum_ex_word_def enum_word_def distinct_map inj_on_word_of_nat flip: UNIV_word_eq_word_of_nat) end lemma [code]: ‹Enum.enum_all P ⟷ list_all P Enum.enum› ‹Enum.enum_ex P ⟷ list_ex P Enum.enum›for P :: ‹'a::len word ==> bool› by (simp_all add: enum_all_word_def enum_ex_word_def enum_UNIV list_all_iff list_ex_iff) subsection ‹Bit-wise operations› text ‹ The following specification of word division just lifts the pre-existing division on integers named ``F-Division'' in 🍋‹"leijen01"›. › instantiation word :: (len) semiring_modulo begin lift_definition divide_word :: ‹'a word ==> 'a word ==> 'a word› is ‹λa b. take_bit LENGTH('a) a div take_bit LENGTH('a) b› by simp lift_definition modulo_word :: ‹'a word ==> 'a word ==> 'a word› is ‹λa b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b› by simp instance proof show "a div b * b + a mod b = a" for a b :: "'a word" proof transfer fix k l :: int define r :: int where "r = 2 ^ LENGTH('a)" then have r: "take_bit LENGTH('a) k = k mod r" for k by (simp add: take_bit_eq_mod) have "k mod r = ((k mod r) div (l mod r) * (l mod r) + (k mod r) mod (l mod r)) mod r" by (simp add: div_mult_mod_eq) also have "… = (((k mod r) div (l mod r) * (l mod r)) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_add_left_eq) also have "… = (((k mod r) div (l mod r) * l) mod r + (k mod r) mod (l mod r)) mod r" by (simp add: mod_mult_right_eq) finally have "k mod r = ((k mod r) div (l mod r) * l + (k mod r) mod (l mod r)) mod r" by (simp add: mod_simps) with r show "take_bit LENGTH('a) (take_bit LENGTH('a) k div take_bit LENGTH('a) l * l + take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = take_bit LENGTH('a) k" by simp qed qed end lemma unat_div_distrib: ‹unat (v div w) = unat v div unat w› proof transfer fix k l have ‹nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) ≤ nat (take_bit LENGTH('a) k)› by (rule div_le_dividend) also have ‹nat (take_bit LENGTH('a) k) 🚫 ^ LENGTH('a)› by (simp add: nat_less_iff) finally show ‹(nat ∘ take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) = (nat ∘ take_bit LENGTH('a)) k div (nat ∘ take_bit LENGTH('a)) l› by (simp add: nat_take_bit_eq div_int_pos_iff nat_div_distrib take_bit_nat_eq_self_iff) qed lemma unat_mod_distrib: ‹unat (v mod w) = unat v mod unat w› proof transfer fix k l have ‹nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) ≤ nat (take_bit LENGTH('a) k)› by (rule mod_less_eq_dividend) also have ‹nat (take_bit LENGTH('a) k) 🚫 ^ LENGTH('a)› by (simp add: nat_less_iff) finally show ‹(nat ∘ take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) = (nat ∘ take_bit LENGTH('a)) k mod (nat ∘ take_bit LENGTH('a)) l› by (simp add: nat_take_bit_eq mod_int_pos_iff less_le nat_mod_distrib take_bit_nat_eq_self_iff) qed instance word :: (len) semiring_parity by (standard; transfer) (auto simp: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex) lemma word_bit_induct [case_names zero even odd]: ‹P a›if word_zero: ‹P 0› and word_even: ‹∧a. P a ==> 0 🚫==> a 🚫 ^ (LENGTH('a) - Suc 0) ==> P (2 * a)› and word_odd: ‹∧a. P a ==> a 🚫 ^ (LENGTH('a) - Suc 0) ==> P (1 + 2 * a)› for P and a :: ‹'a::len word› proof - define m :: nat where ‹m = LENGTH('a) - Suc 0› then have l: ‹LENGTH('a) = Suc m› by simp define n :: nat where ‹n = unat a› then have ‹n 🚫 ^ LENGTH('a)› by transfer (simp add: take_bit_eq_mod) then have ‹n 🚫 * 2 ^ m› by (simp add: l) then have ‹P (of_nat n)› proof (induction n rule: nat_bit_induct) case zero show ?case by simp (rule word_zero) next case (even n) then have ‹n 🚫 ^ m› by simp with even.IH have ‹P (of_nat n)› by simp moreover from ‹n 🚫 ^ m›even.hyps have ‹0 🚫of_nat n :: 'a word)› by (auto simp: word_greater_zero_iff l word_of_nat_eq_0_iff) moreover from ‹n 🚫 ^ m›have ‹(of_nat n :: 'a word) 🚫 ^ (LENGTH('a) - Suc 0)› using of_nat_word_less_iff [where ?'a = 'a, of n ‹2 ^ m›] by (simp add: l take_bit_eq_mod) ultimately have ‹P (2 * of_nat n)› by (rule word_even) then show ?case by simp next case (odd n) then have ‹Suc n ≤ 2 ^ m› by simp with odd.IH have ‹P (of_nat n)› by simp moreover from ‹Suc n ≤ 2 ^ m›have ‹(of_nat n :: 'a word) 🚫 ^ (LENGTH('a) - Suc 0)› using of_nat_word_less_iff [where ?'a = 'a, of n ‹2 ^ m›] by (simp add: l take_bit_eq_mod) ultimately have ‹P (1 + 2 * of_nat n)› by (rule word_odd) then show ?case by simp qed moreover have ‹of_nat (nat (uint a)) = a› by transfer simp ultimately show ?thesis by (simp add: n_def) qed lemma bit_word_half_eq: ‹(of_bool b + a * 2) div 2 = a› if ‹a 🚫 ^ (LENGTH('a) - Suc 0)› for a :: ‹'a::len word› proof (cases ‹2 ≤ LENGTH('a::len)›) case False with that show ?thesis by transfer simp next case True obtain n where length: ‹LENGTH('a) = Suc n› by (cases ‹LENGTH('a)›) simp_all show ?thesis proof (cases b) case False moreover have ‹a * 2 div 2 = a› using that proof transfer fix k :: int from length have ‹k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2› by simp moreover assume ‹take_bit LENGTH('a) k 🚫 LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))› with ‹LENGTH('a) = Suc n›have ‹take_bit LENGTH('a) k = take_bit n k› by (auto simp: take_bit_Suc_from_most) ultimately have ‹take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2› by (simp add: take_bit_eq_mod) with True show ‹take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k› by simp qed ultimately show ?thesis by simp next case True moreover have ‹(1 + a * 2) div 2 = a› using that proof transfer fix k :: int from length have ‹(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2› using pos_zmod_mult_2 [of ‹2 ^ n›k] by (simp add: ac_simps) moreover assume ‹take_bit LENGTH('a) k 🚫 LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))› with ‹LENGTH('a) = Suc n›have ‹take_bit LENGTH('a) k = take_bit n k› by (auto simp: take_bit_Suc_from_most) ultimately have ‹take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2› by (simp add: take_bit_eq_mod) with True show ‹take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) = take_bit LENGTH('a) k› by (auto simp: take_bit_Suc) qed ultimately show ?thesis by simp qed qed lemma even_mult_exp_div_word_iff: ‹even (a * 2 ^ m div 2 ^ n) ⟷¬ ( m ≤ n ∧ n 🚫('a) ∧ odd (a div 2 ^ (n - m)))› by transfer (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff, simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) instantiation word :: (len) semiring_bits begin lift_definition bit_word :: ‹'a word ==> nat ==> bool› is ‹λk n. n 🚫('a) ∧ bit k n› proof fix k l :: int and n :: nat assume *: ‹take_bit LENGTH('a) k = take_bit LENGTH('a) l› show ‹n 🚫('a) ∧ bit k n ⟷ n 🚫('a) ∧ bit l n› proof (cases ‹n 🚫('a)›) case True from * have ‹bit (take_bit LENGTH('a) k) n ⟷ bit (take_bit LENGTH('a) l) n› by simp then show ?thesis by (simp add: bit_take_bit_iff) next case False then show ?thesis by simp qed qed instance proof show ‹P a›if stable: ‹∧a. a div 2 = a ==> P a› and rec: ‹∧a b. P a ==> (of_bool b + 2 * a) div 2 = a ==> P (of_bool b + 2 * a)› for P and a :: ‹'a word› proof (induction a rule: word_bit_induct) case zero have ‹0 div 2 = (0::'a word)› by transfer simp with stable [of 0] show ?case by simp next case (even a) with rec [of a False] show ?case using bit_word_half_eq [of a False] by (simp add: ac_simps) next case (odd a) with rec [of a True] show ?case using bit_word_half_eq [of a True] by (simp add: ac_simps) qed show ‹bit a n ⟷ odd (a div 2 ^ n)›for a :: ‹'a word› and n by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit) show ‹a div 0 = 0› for a :: ‹'a word› by transfer simp show ‹a div 1 = a› for a :: ‹'a word› by transfer simp show ‹0 div a = 0› for a :: ‹'a word› by transfer simp show ‹a mod b div b = 0› for a b :: ‹'a word› by (simp add: word_eq_iff_unsigned [where ?'a = nat] unat_div_distrib unat_mod_distrib) show ‹a div 2 div 2 ^ n = a div 2 ^ Suc n› for a :: ‹'a word›and m n :: nat apply transfer using drop_bit_eq_div [symmetric, where ?'a = int,of _ 1] apply (auto simp: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps) apply (simp add: drop_bit_take_bit) done show ‹even (2 * a div 2 ^ Suc n) ⟷ even (a div 2 ^ n)›if ‹2 ^ Suc n ≠ (0::'a word)› for a :: ‹'a word›and n :: nat using that by transfer (simp add: even_drop_bit_iff_not_bit bit_simps flip: drop_bit_eq_div del: power.simps) qed end lemma bit_word_eqI: ‹a = b›if ‹∧n. n 🚫('a) ==> bit a n ⟷ bit b n› for a b :: ‹'a::len word› using that by transfer (auto simp: nat_less_le bit_eq_iff bit_take_bit_iff) lemma bit_imp_le_length: ‹n 🚫('a)›if ‹bit w n› for w :: ‹'a::len word› by (meson bit_word.rep_eq that) lemma not_bit_length [simp]: ‹¬ bit w LENGTH('a)›for w :: ‹'a::len word› using bit_imp_le_length by blast lemma finite_bit_word [simp]: ‹finite {n. bit w n}› for w :: ‹'a::len word› by (metis bit_imp_le_length bounded_nat_set_is_finite mem_Collect_eq) lemma bit_numeral_word_iff [simp]: ‹bit (numeral w :: 'a::len word) n ⟷ n 🚫('a) ∧ bit (numeral w :: int) n› by transfer simp lemma bit_neg_numeral_word_iff [simp]: ‹bit (- numeral w :: 'a::len word) n ⟷ n 🚫('a) ∧ bit (- numeral w :: int) n› by transfer simp instantiation word :: (len) ring_bit_operations begin lift_definition not_word :: ‹'a word ==> 'a word› is not by (simp add: take_bit_not_iff) lift_definition and_word :: ‹'a word ==> 'a word ==> 'a word› is ‹and› by simp lift_definition or_word :: ‹'a word ==> 'a word ==> 'a word› is or by simp lift_definition xor_word :: ‹'a word ==> 'a word ==> 'a word› is xor by simp lift_definition mask_word :: ‹nat ==> 'a word› is mask . lift_definition set_bit_word :: ‹nat ==> 'a word ==> 'a word› is set_bit by (simp add: set_bit_def) lift_definition unset_bit_word :: ‹nat ==> 'a word ==> 'a word› is unset_bit by (simp add: unset_bit_def) lift_definition flip_bit_word :: ‹nat ==> 'a word ==> 'a word› is flip_bit by (simp add: flip_bit_def) lift_definition push_bit_word :: ‹nat ==> 'a word ==> 'a word› is push_bit proof - show ‹take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)› if ‹take_bit LENGTH('a) k = take_bit LENGTH('a) l›for k l :: int and n :: nat by (metis le_add2 push_bit_take_bit take_bit_tightened that) qed lift_definition drop_bit_word :: ‹nat ==> 'a word ==> 'a word› is ‹λn. drop_bit n ∘ take_bit LENGTH('a)› by (simp add: take_bit_eq_mod) lift_definition take_bit_word :: ‹nat ==> 'a word ==> 'a word› is ‹λn. take_bit (min LENGTH('a) n)› by (simp add: ac_simps) (simp only: flip: take_bit_take_bit) context includes bit_operations_syntax begin instance proof fix v w :: ‹'a word›and n m :: nat show ‹NOT v = - v - 1› by transfer (simp add: not_eq_complement) show ‹v AND w = of_bool (odd v ∧ odd w) + 2 * (v div 2 AND w div 2)› apply transfer by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc) show ‹v OR w = of_bool (odd v ∨ odd w) + 2 * (v div 2 OR w div 2)› apply transfer by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc) show ‹v XOR w = of_bool (odd v ≠ odd w) + 2 * (v div 2 XOR w div 2)› apply transfer apply (rule bit_eqI) subgoal for k l n apply (cases n) apply (auto simp: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc) done done show ‹mask n = 2 ^ n - (1 :: 'a word)› by transfer (simp flip: mask_eq_exp_minus_1) show ‹set_bit n v = v OR push_bit n 1› by transfer (simp add: set_bit_eq_or) show ‹unset_bit n v = (v OR push_bit n 1) XOR push_bit n 1› by transfer (simp add: unset_bit_eq_or_xor) show ‹flip_bit n v = v XOR push_bit n 1› by transfer (simp add: flip_bit_eq_xor) show ‹push_bit n v = v * 2 ^ n› by transfer (simp add: push_bit_eq_mult) show ‹drop_bit n v = v div 2 ^ n› by transfer (simp add: drop_bit_take_bit flip: drop_bit_eq_div) show ‹take_bit n v = v mod 2 ^ n› by transfer (simp flip: take_bit_eq_mod) qed end end lemma [code]: ‹push_bit n w = w * 2 ^ n›for w :: ‹'a::len word› by (fact push_bit_eq_mult) lemma [code]: ‹Word.the_int (drop_bit n w) = drop_bit n (Word.the_int w)› by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv) lemma [code]: ‹Word.the_int (take_bit n w) = (if n 🚫('a::len) then take_bit n (Word.the_int w) else Word.the_int w)› for w :: ‹'a::len word› by transfer (simp add: not_le not_less ac_simps min_absorb2) lemma [code_abbrev]: ‹push_bit n 1 = (2 :: 'a::len word) ^ n› by (fact push_bit_of_1) context includes bit_operations_syntax begin lemma [code]: ‹NOT w = Word.of_int (NOT (Word.the_int w))› for w :: ‹'a::len word› by transfer (simp add: take_bit_not_take_bit) lemma [code]: ‹Word.the_int (v AND w) = Word.the_int v AND Word.the_int w› by transfer simp lemma [code]: ‹Word.the_int (v OR w) = Word.the_int v OR Word.the_int w› by transfer simp lemma [code]: ‹Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w› by transfer simp lemma [code]: ‹Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)› by transfer simp lemma [code]: ‹set_bit n w = w OR push_bit n 1›for w :: ‹'a::len word› by (fact set_bit_eq_or) lemma [code]: ‹unset_bit n w = w AND NOT (push_bit n 1)›for w :: ‹'a::len word› by (fact unset_bit_eq_and_not) lemma [code]: ‹flip_bit n w = w XOR push_bit n 1›for w :: ‹'a::len word› by (fact flip_bit_eq_xor) context includes lifting_syntax begin lemma set_bit_word_transfer [transfer_rule]: ‹((=) ===> pcr_word ===> pcr_word) set_bit set_bit› by (unfold set_bit_def) transfer_prover lemma unset_bit_word_transfer [transfer_rule]: ‹((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit› by (unfold unset_bit_def) transfer_prover lemma flip_bit_word_transfer [transfer_rule]: ‹((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit› by (unfold flip_bit_def) transfer_prover lemma signed_take_bit_word_transfer [transfer_rule]: ‹((=) ===> pcr_word ===> pcr_word) (λn k. signed_take_bit n (take_bit LENGTH('a::len) k)) (signed_take_bit :: nat ==> 'a word ==> 'a word)› proof - let ?K = ‹λn (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n 🚫('a) ∧ bit k n) * NOT (mask n)› let ?W = ‹λn (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)› have ‹((=) ===> pcr_word ===> pcr_word) ?K ?W› by transfer_prover also have ‹?K = (λn k. signed_take_bit n (take_bit LENGTH('a::len) k))› by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps) also have ‹?W = signed_take_bit› by (simp add: fun_eq_iff signed_take_bit_def) finally show ?thesis . qed end end subsection ‹Conversions including casts› subsubsection ‹Generic unsigned conversion› context semiring_bits begin lemma bit_unsigned_iff [bit_simps]: ‹bit (unsigned w) n ⟷ possible_bit TYPE('a) n ∧ bit w n› for w :: ‹'b::len word› by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff) end lemma possible_bit_word[simp]: ‹possible_bit TYPE(('a :: len) word) m ⟷ m 🚫('a)› by (simp add: possible_bit_def linorder_not_le) context semiring_bit_operations begin lemma unsigned_minus_1_eq_mask: ‹unsigned (- 1 :: 'b::len word) = mask LENGTH('b)› by (transfer fixing: mask) (simp add: nat_mask_eq of_nat_mask_eq) lemma unsigned_push_bit_eq: ‹unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))› for w :: ‹'b::len word› proof (rule bit_eqI) fix m assume ‹possible_bit TYPE('a) m› show ‹bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m› proof (cases ‹n ≤ m›) case True with ‹possible_bit TYPE('a) m›have ‹possible_bit TYPE('a) (m - n)› by (simp add: possible_bit_less_imp) with True show ?thesis by (simp add: bit_unsigned_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff bit_take_bit_iff not_le ac_simps) next case False then show ?thesis by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Bit_Operations.bit_push_bit_iff bit_take_bit_iff) qed qed lemma unsigned_take_bit_eq: ‹unsigned (take_bit n w) = take_bit n (unsigned w)› for w :: ‹'b::len word› by (rule bit_eqI) (simp add: bit_unsigned_iff bit_take_bit_iff Bit_Operations.bit_take_bit_iff) end context linordered_euclidean_semiring_bit_operations begin lemma unsigned_drop_bit_eq: ‹unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))› for w :: ‹'b::len word› by (rule bit_eqI) (auto simp: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq possible_bit_def dest: bit_imp_le_length) end lemma ucast_drop_bit_eq: ‹ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)› if ‹LENGTH('a) ≤ LENGTH('b)›for w :: ‹'a::len word› by (rule bit_word_eqI) (use that in ‹auto simp: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length›) context semiring_bit_operations begin context includes bit_operations_syntax begin lemma unsigned_and_eq: ‹unsigned (v AND w) = unsigned v AND unsigned w› for v w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps) lemma unsigned_or_eq: ‹unsigned (v OR w) = unsigned v OR unsigned w› for v w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps) lemma unsigned_xor_eq: ‹unsigned (v XOR w) = unsigned v XOR unsigned w› for v w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps) end end context ring_bit_operations begin context includes bit_operations_syntax begin lemma unsigned_not_eq: ‹unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))› for w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps) end end context linordered_euclidean_semiring begin lemma unsigned_greater_eq [simp]: ‹0 ≤ unsigned w›for w :: ‹'b::len word› by (transfer fixing: less_eq) simp lemma unsigned_less [simp]: ‹unsigned w 🚫 ^ LENGTH('b)›for w :: ‹'b::len word› by (transfer fixing: less) simp end context linordered_semidom begin lemma word_less_eq_iff_unsigned: "a ≤ b ⟷ unsigned a ≤ unsigned b" by (transfer fixing: less_eq) (simp add: nat_le_eq_zle) lemma word_less_iff_unsigned: "a 🚫⟷ unsigned a 🚫 b" by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative]) end subsubsection ‹Generic signed conversion› context ring_bit_operations begin lemma bit_signed_iff [bit_simps]: ‹bit (signed w) n ⟷ possible_bit TYPE('a) n ∧ bit w (min (LENGTH('b) - Suc 0) n)› for w :: ‹'b::len word› by (transfer fixing: bit) (auto simp: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def) lemma signed_push_bit_eq: ‹signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))› for w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj) auto lemma signed_take_bit_eq: ‹signed (take_bit n w) = (if n 🚫('b) then take_bit n (signed w) else signed w)› for w :: ‹'b::len word› by (transfer fixing: take_bit; cases ‹LENGTH('b)›) (auto simp: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq) context includes bit_operations_syntax begin lemma signed_not_eq: ‹signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))› for w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj) (auto simp: min_def) lemma signed_and_eq: ‹signed (v AND w) = signed v AND signed w› for v w :: ‹'b::len word› by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff) lemma signed_or_eq: ‹signed (v OR w) = signed v OR signed w› for v w :: ‹'b::len word› by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff) lemma signed_xor_eq: ‹signed (v XOR w) = signed v XOR signed w› for v w :: ‹'b::len word› by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff) end end subsubsection ‹More› lemma sint_greater_eq: ‹- (2 ^ (LENGTH('a) - Suc 0)) ≤ sint w›for w :: ‹'a::len word› proof (cases ‹bit w (LENGTH('a) - Suc 0)›) case True then show ?thesis by transfer (simp add: signed_take_bit_eq_if_negative minus_exp_eq_not_mask or_greater_eq ac_simps) next have *: ‹- (2 ^ (LENGTH('a) - Suc 0)) ≤ (0::int)› by simp case False then show ?thesis by transfer (auto simp: signed_take_bit_eq intro: order_trans *) qed
lemma sint_less: ‹sint w 🚫 ^ (LENGTH('a) - Suc 0)›for w :: ‹'a::len word› by (cases ‹bit w (LENGTH('a) - Suc 0)›; transfer)
(simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)
lemma uint_div_distrib: ‹uint (v div w) = uint v div uint w› by (metis int_ops(8) of_nat_unat unat_div_distrib)
lemma unat_drop_bit_eq: ‹unat (drop_bit n w) = drop_bit n (unat w)› by (rule bit_eqI) (simp add: bit_unsigned_iff bit_drop_bit_eq)
lemma uint_mod_distrib: ‹uint (v mod w) = uint v mod uint w› by (metis int_ops(9) of_nat_unat unat_mod_distrib)
context semiring_bit_operations begin
lemma unsigned_ucast_eq: ‹unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)› for w :: ‹'b::len word› by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff not_le)
end
context ring_bit_operations begin
lemma signed_ucast_eq: ‹signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)› for w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps min_less_iff_disj)
lemma signed_scast_eq: ‹signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)› for w :: ‹'b::len word› by (simp add: bit_eq_iff bit_simps min_less_iff_disj)
end
lemma uint_nonnegative: "0 ≤ uint w" by (fact unsigned_greater_eq)
lemma uint_bounded: "uint w < 2 ^ LENGTH('a)" for w :: "'a::len word" by (fact unsigned_less)
lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w" for w :: "'a::len word" by transfer (simp add: take_bit_eq_mod)
lemma word_uint_eqI: "uint a = uint b ==> a = b" by (fact unsigned_word_eqI)
lemma word_uint_eq_iff: "a = b ⟷ uint a = uint b" by (fact word_eq_iff_unsigned)
lemma uint_word_of_int_eq: ‹uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k› by transfer rule
lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)" by (simp add: uint_word_of_int_eq take_bit_eq_mod)
lemma word_of_int_uint: "word_of_int (uint w) = w" by transfer simp
lemma word_div_def [code]: "a div b = word_of_int (uint a div uint b)" by transfer rule
lemma word_mod_def [code]: "a mod b = word_of_int (uint a mod uint b)" by transfer rule
lemma split_word_all: "(∧x::'a::len word. PROP P x) ≡ (∧x. PROP P (word_of_int x))" proof fix x :: "'a word" assume"∧x. PROP P (word_of_int x)" thenhave"PROP P (word_of_int (uint x))" . thenshow"PROP P x" by (simp only: word_of_int_uint) qed
lemma sint_uint: ‹sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)› for w :: ‹'a::len word› by (cases ‹LENGTH('a)›; transfer) (simp_all add: signed_take_bit_take_bit)
lemma unat_eq_nat_uint: ‹unat w = nat (uint w)› by simp
lemma ucast_eq: ‹ucast w = word_of_int (uint w)› by transfer simp
lemma scast_eq: ‹scast w = word_of_int (sint w)› by transfer simp
lemma uint_0_eq: ‹uint 0 = 0› by (fact unsigned_0)
lemma uint_1_eq: ‹uint 1 = 1› by (fact unsigned_1)
lemma word_m1_wi: "- 1 = word_of_int (- 1)" by simp
lemma uint_0_iff: "uint x = 0 ⟷ x = 0" by (auto simp: unsigned_word_eqI)
lemma unat_0_iff: "unat x = 0 ⟷ x = 0" by (auto simp: unsigned_word_eqI)
lemma unat_0: "unat 0 = 0" by (fact unsigned_0)
lemma unat_gt_0: "0 < unat x ⟷ x ≠ 0" by (auto simp: unat_0_iff [symmetric])
lemma is_up_eq: ‹is_up f ⟷ source_size f ≤ target_size f› for f :: ‹'a::len word ==> 'b::len word› by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq)
lemma is_down_eq: ‹is_down f ⟷ target_size f ≤ source_size f› for f :: ‹'a::len word ==> 'b::len word› by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq)
lift_definition word_int_case :: ‹(int ==> 'b) ==> 'a::len word ==> 'b› is‹λf. f ∘ take_bit LENGTH('a)›by simp
lemma word_int_case_eq_uint [code]: ‹word_int_case f w = f (uint w)› by transfer simp
translations "case x of XCONST of_int y ==> b"⇌"CONST word_int_case (λy. b) x" "case x of (XCONST of_int :: 'a) y ==> b"⇀"CONST word_int_case (λy. b) x"
subsection‹Arithmetic operations›
lemma div_word_self: ‹w div w = 1›if‹w ≠ 0›for w :: ‹'a::len word› using that by transfer simp
lemma mod_word_self [simp]: ‹w mod w = 0›for w :: ‹'a::len word› by (simp add: word_mod_def)
lemma div_word_less: ‹w div v = 0›if‹w 🚫›for w v :: ‹'a::len word› using that by transfer simp
lemma mod_word_less: ‹w mod v = w›if‹w 🚫›for w v :: ‹'a::len word› using div_mult_mod_eq [of w v] using that by (simp add: div_word_less)
lemma div_word_one [simp]: ‹1 div w = of_bool (w = 1)›for w :: ‹'a::len word› proof transfer fix k :: int show‹take_bit LENGTH('a) (take_bit LENGTH('a) 1 div take_bit LENGTH('a) k) = take_bit LENGTH('a) (of_bool (take_bit LENGTH('a) k = take_bit LENGTH('a) 1))› using take_bit_nonnegative [of ‹LENGTH('a)› k] by (smt (verit, best) div_by_1 of_bool_eq take_bit_of_0 take_bit_of_1 zdiv_eq_0_iff) qed
lemma mod_word_one [simp]: ‹1 mod w = 1 - w * of_bool (w = 1)›for w :: ‹'a::len word› using div_mult_mod_eq [of 1 w] by auto
lemma div_word_by_minus_1_eq [simp]: ‹w div - 1 = of_bool (w = - 1)›for w :: ‹'a::len word› by (auto intro: div_word_less simp add: div_word_self word_order.not_eq_extremum)
lemma mod_word_by_minus_1_eq [simp]: ‹w mod - 1 = w * of_bool (w 🚫 1)›for w :: ‹'a::len word› using mod_word_less word_order.not_eq_extremum by fastforce
text‹Legacy theorems:›
lemma word_add_def [code]: "a + b = word_of_int (uint a + uint b)" by transfer (simp add: take_bit_add)
lemma word_sub_wi [code]: "a - b = word_of_int (uint a - uint b)" by transfer (simp add: take_bit_diff)
lemma word_mult_def [code]: "a * b = word_of_int (uint a * uint b)" by transfer (simp add: take_bit_eq_mod mod_simps)
lemma word_minus_def [code]: "- a = word_of_int (- uint a)" by transfer (simp add: take_bit_minus)
lemma word_0_wi: "0 = word_of_int 0" by transfer simp
lemma word_1_wi: "1 = word_of_int 1" by transfer simp
lift_definition word_succ :: "'a::len word ==> 'a word"is"λx. x + 1" by (auto simp: take_bit_eq_mod intro: mod_add_cong)
lift_definition word_pred :: "'a::len word ==> 'a word"is"λx. x - 1" by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
lemma word_succ_alt [code]: "word_succ a = word_of_int (uint a + 1)" by transfer (simp add: take_bit_eq_mod mod_simps)
lemma word_pred_alt [code]: "word_pred a = word_of_int (uint a - 1)" by transfer (simp add: take_bit_eq_mod mod_simps)
lemma wi_homs: shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)" and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and wi_hom_neg: "- word_of_int a = word_of_int (- a)" and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)" by (transfer, simp)+
lemma double_eq_zero_iff: ‹2 * a = 0 ⟷ a = 0 ∨ a = 2 ^ (LENGTH('a) - Suc 0)› for a :: ‹'a::len word› proof -
define n where‹n = LENGTH('a) - Suc 0› thenhave *: ‹LENGTH('a) = Suc n› by simp have‹a = 0›if‹2 * a = 0›and‹a ≠ 2 ^ (LENGTH('a) - Suc 0)› using that by transfer
(auto simp: take_bit_eq_0_iff take_bit_eq_mod *) moreoverhave‹2 ^ LENGTH('a) = (0 :: 'a word)› by transfer simp thenhave‹2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)› by (simp add: *) ultimatelyshow ?thesis by auto qed
subsection‹Ordering›
instance word :: (len) wellorder proof fix P :: "'a word ==> bool"and a assume *: "(∧b. (∧a. a < b ==> P a) ==> P b)" have"wf (measure unat)" .. moreoverhave"{(a, b :: ('a::len) word). a < b} ⊆ measure unat" by (auto simp add: word_less_iff_unsigned [where ?'a = nat]) ultimatelyhave"wf {(a, b :: ('a::len) word). a < b}" by (rule wf_subset) thenshow"P a"using * byinduction blast qed
lemma word_m1_ge [simp]: (* FIXME: delete *) "word_pred 0 ≥ y" by transfer (simp add: mask_eq_exp_minus_1)
lemma word_less_alt: "a < b ⟷ uint a < uint b" by (fact word_less_def)
lemma word_zero_le [simp]: "0 ≤ y"for y :: "'a::len word" by (fact word_coorder.extremum)
lemma word_n1_ge [simp]: "y ≤ - 1"for y :: "'a::len word" by (fact word_order.extremum)
lemma word_gt_0: "0 < y ⟷ 0 ≠ y" for y :: "'a::len word" by (simp add: less_le)
lemma word_gt_0_no [simp]: ‹(0 :: 'a::len word) 🚫 y ⟷ (0 :: 'a::len word) ≠ numeral y› by (fact word_gt_0)
lemma word_le_nat_alt: "a ≤ b ⟷ unat a ≤ unat b" by transfer (simp add: nat_le_eq_zle)
lemma word_less_nat_alt: "a < b ⟷ unat a < unat b" by transfer (auto simp: less_le [of 0])
lemmas unat_mono = word_less_nat_alt [THEN iffD1]
lemma wi_less: "(word_of_int n < (word_of_int m :: 'a::len word)) = (n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))" by (simp add: uint_word_of_int word_less_def)
lemma wi_le: "(word_of_int n ≤ (word_of_int m :: 'a::len word)) = (n mod 2 ^ LENGTH('a) ≤ m mod 2 ^ LENGTH('a))" by (simp add: uint_word_of_int word_le_def)
lift_definition word_sle :: ‹'a::len word ==> 'a word ==> bool› is‹λk l. signed_take_bit (LENGTH('a) - Suc 0) k ≤ signed_take_bit (LENGTH('a) - Suc 0) l› by (simp flip: signed_take_bit_decr_length_iff)
lift_definition word_sless :: ‹'a::len word ==> 'a word ==> bool› is‹λk l. signed_take_bit (LENGTH('a) - Suc 0) k 🚫 (LENGTH('a) - Suc 0) l› by (simp flip: signed_take_bit_decr_length_iff)
notation
word_sle (‹'(≤s')›) and
word_sle (‹(‹notation=‹infix ≤s›\›_/ ≤s _)› [51, 51] 50) and
word_sless (‹'(🚫)›) and
word_sless (‹(‹notation=‹infix 🚫›\›_/ <s _)› [51, 51] 50)
interpretation signed: linorder word_sle word_sless by (fact signed_linorder)
lemma word_sless_eq: ‹x 🚫y ⟷ x 🚫 y ∧ x ≠ y› by (fact signed.less_le)
lemma minus_1_sless_0 [simp]: ‹- 1 🚫0› by transfer simp
lemma not_0_sless_minus_1 [simp]: ‹¬ 0 🚫- 1› by transfer simp
lemma minus_1_sless_eq_0 [simp]: ‹- 1 ≤s 0› by transfer simp
lemma not_0_sless_eq_minus_1 [simp]: ‹¬ 0 ≤s - 1› by transfer simp
subsection‹Bit-wise operations›
context includes bit_operations_syntax begin
lemma take_bit_word_eq_self: ‹take_bit n w = w›if‹LENGTH('a) ≤ n›for w :: ‹'a::len word› using that by transfer simp
lemma take_bit_length_eq [simp]: ‹take_bit LENGTH('a) w = w›for w :: ‹'a::len word› by (simp add: nat_le_linear take_bit_word_eq_self)
lemma bit_word_of_int_iff: ‹bit (word_of_int k :: 'a::len word) n ⟷ n 🚫('a) ∧ bit k n› by (simp add: bit_simps)
lemma bit_uint_iff: ‹bit (uint w) n ⟷ n 🚫('a) ∧ bit w n› for w :: ‹'a::len word› by transfer (simp add: bit_take_bit_iff)
lemma bit_sint_iff: ‹bit (sint w) n ⟷ n ≥ LENGTH('a) ∧ bit w (LENGTH('a) - 1) ∨ bit w n› for w :: ‹'a::len word› by transfer (auto simp: bit_signed_take_bit_iff min_def le_less not_less)
lemma bit_word_ucast_iff: ‹bit (ucast w :: 'b::len word) n ⟷ n 🚫('a) ∧ n 🚫('b) ∧ bit w n› for w :: ‹'a::len word› by (auto simp add: bit_unsigned_iff bit_imp_le_length)
lemma bit_word_scast_iff: ‹bit (scast w :: 'b::len word) n ⟷ n 🚫('b) ∧ (bit w n ∨ LENGTH('a) ≤ n ∧ bit w (LENGTH('a) - Suc 0))› for w :: ‹'a::len word› by (auto simp add: bit_signed_iff bit_imp_le_length min_def le_less dest: bit_imp_possible_bit)
lemma bit_word_iff_drop_bit_and [code]: ‹bit a n ⟷ drop_bit n a AND 1 = 1›for a :: ‹'a::len word› by (simp add: bit_iff_odd_drop_bit odd_iff_mod_2_eq_one and_one_eq)
lemma
word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" by (transfer, simp add: take_bit_not_take_bit)+
definition even_word :: ‹'a::len word ==> bool› where [code_abbrev]: ‹even_word = even›
lemma even_word_iff [code]: ‹even_word a ⟷ a AND 1 = 0› by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)
lemma map_bit_range_eq_if_take_bit_eq: ‹map (bit k) [0..🚫 = map (bit l) [0..🚫› if‹take_bit n k = take_bit n l›for k l :: int using that proof (induction n arbitrary: k l) case 0 thenshow ?case by simp next case (Suc n) from Suc.prems have‹take_bit n (k div 2) = take_bit n (l div 2)› by (simp add: take_bit_Suc) thenhave‹map (bit (k div 2)) [0..🚫 = map (bit (l div 2)) [0..🚫› by (rule Suc.IH) moreoverhave‹bit (r div 2) = bit r ∘ Suc›for r :: int by (simp add: fun_eq_iff bit_Suc) moreoverfrom Suc.prems have‹even k ⟷ even l› by (metis Zero_neq_Suc even_take_bit_eq) ultimatelyshow ?case by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) (simp add: bit_0) qed
lemma
take_bit_word_Bit0_eq [simp]: ‹take_bit (numeral n) (numeral (num.Bit0 m) :: 'a::len word) = 2 * take_bit (pred_numeral n) (numeral m)› and take_bit_word_Bit1_eq [simp]: ‹take_bit (numeral n) (numeral (num.Bit1 m) :: 'a::len word) = 1 + 2 * take_bit (pred_numeral n) (numeral m)› and take_bit_word_minus_Bit0_eq [simp]: ‹take_bit (numeral n) (- numeral (num.Bit0 m) :: 'a::len word) = 2 * take_bit (pred_numeral n) (- numeral m)› and take_bit_word_minus_Bit1_eq [simp]: ‹take_bit (numeral n) (- numeral (num.Bit1 m) :: 'a::len word) = 1 + 2 * take_bit (pred_numeral n) (- numeral (Num.inc m))› proof -
define w :: ‹'a::len word› where‹w = numeral m› moreover define q :: nat where‹q = pred_numeral n› ultimatelyhave num: ‹numeral m = w› ‹numeral (num.Bit0 m) = 2 * w› ‹numeral (num.Bit1 m) = 1 + 2 * w› ‹numeral (Num.inc m) = 1 + w› ‹pred_numeral n = q› ‹numeral n = Suc q› by (simp_all only: w_def q_def numeral_Bit0 [of m] numeral_Bit1 [of m] ac_simps
numeral_inc numeral_eq_Suc flip: mult_2) have even: ‹take_bit (Suc q) (2 * w) = 2 * take_bit q w›for w :: ‹'a::len word› by (rule bit_word_eqI)
(auto simp: bit_take_bit_iff bit_double_iff) have odd: ‹take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w›for w :: ‹'a::len word› by (rule bit_eqI)
(auto simp: bit_take_bit_iff bit_double_iff even_bit_succ_iff) show ?P using even [of w] by (simp add: num) show ?Q using odd [of w] by (simp add: num) show ?R using even [of ‹- w›] by (simp add: num) show ?S using odd [of ‹- (1 + w)›] by (simp add: num) qed
subsection‹More shift operations›
lift_definition signed_drop_bit :: ‹nat ==> 'a word ==> 'a::len word› is‹λn. drop_bit n ∘ signed_take_bit (LENGTH('a) - Suc 0)› using signed_take_bit_decr_length_iff by (simp add: take_bit_drop_bit) force
lemma bit_signed_drop_bit_iff [bit_simps]: ‹bit (signed_drop_bit m w) n ⟷ bit w (if LENGTH('a) - m ≤ n ∧ n 🚫('a) then LENGTH('a) - 1 else m + n)› for w :: ‹'a::len word› by transfer (simp add: bit_drop_bit_eq bit_signed_take_bit_iff min_def le_less not_less, auto)
lemma [code]: ‹Word.the_int (signed_drop_bit n w) = take_bit LENGTH('a) (drop_bit n (Word.the_signed_int w))› for w :: ‹'a::len word› by transfer simp
lemma signed_drop_bit_of_0 [simp]: ‹signed_drop_bit n 0 = 0› by transfer simp
lemma signed_drop_bit_of_minus_1 [simp]: ‹signed_drop_bit n (- 1) = - 1› by transfer simp
lemma signed_drop_bit_signed_drop_bit [simp]: ‹signed_drop_bit m (signed_drop_bit n w) = signed_drop_bit (m + n) w› for w :: ‹'a::len word› proof (cases ‹LENGTH('a)›) case 0 thenshow ?thesis using len_not_eq_0 by blast next case (Suc n) thenshow ?thesis by (force simp: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI) qed
lemma signed_drop_bit_0 [simp]: ‹signed_drop_bit 0 w = w› by transfer (simp add: take_bit_signed_take_bit)
lemma sint_signed_drop_bit_eq: ‹sint (signed_drop_bit n w) = drop_bit n (sint w)› by (rule bit_eqI; cases n) (auto simp add: bit_simps not_less)
subsection‹Single-bit operations›
lemma set_bit_eq_idem_iff: ‹set_bit n w = w ⟷ bit w n ∨ n ≥ LENGTH('a)› for w :: ‹'a::len word› unfolding bit_eq_iff by (auto simp: bit_simps not_le)
lemma unset_bit_eq_idem_iff: ‹unset_bit n w = w ⟷ bit w n ⟶ n ≥ LENGTH('a)› for w :: ‹'a::len word› unfolding bit_eq_iff by (auto simp: bit_simps dest: bit_imp_le_length)
lemma flip_bit_eq_idem_iff: ‹flip_bit n w = w ⟷ n ≥ LENGTH('a)› for w :: ‹'a::len word› by (simp add: flip_bit_eq_if set_bit_eq_idem_iff unset_bit_eq_idem_iff)
subsection‹Rotation›
lift_definition word_rotr :: ‹nat ==> 'a::len word ==> 'a::len word› is‹λn k. concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (n mod LENGTH('a)) k)› using take_bit_tightened by fastforce
lift_definition word_rotl :: ‹nat ==> 'a::len word ==> 'a::len word› is‹λn k. concat_bit (n mod LENGTH('a)) (drop_bit (LENGTH('a) - n mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (LENGTH('a) - n mod LENGTH('a)) k)› using take_bit_tightened by fastforce
lift_definition word_roti :: ‹int ==> 'a::len word ==> 'a::len word› is‹λr k. concat_bit (LENGTH('a) - nat (r mod int LENGTH('a))) (drop_bit (nat (r mod int LENGTH('a))) (take_bit LENGTH('a) k)) (take_bit (nat (r mod int LENGTH('a))) k)› by (smt (verit, best) len_gt_0 nat_le_iff of_nat_0_less_iff pos_mod_bound
take_bit_tightened)
lemma word_rotl_eq_word_rotr [code]: ‹word_rotl n = (word_rotr (LENGTH('a) - n mod LENGTH('a)) :: 'a::len word ==> 'a word)› by (rule ext, cases ‹n mod LENGTH('a) = 0›; transfer) simp_all
lemma word_roti_eq_word_rotr_word_rotl [code]: ‹word_roti i w = (if i ≥ 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)› proof (cases ‹i ≥ 0›) case True moreover define n where‹n = nat i› ultimatelyhave‹i = int n› by simp moreoverhave‹word_roti (int n) = (word_rotr n :: _ ==> 'a word)› by (rule ext, transfer) (simp add: nat_mod_distrib) ultimatelyshow ?thesis by simp next case False moreover define n where‹n = nat (- i)› ultimatelyhave‹i = - int n›‹n > 0› by simp_all moreoverhave‹word_roti (- int n) = (word_rotl n :: _ ==> 'a word)› by (rule ext, transfer)
(simp add: zmod_zminus1_eq_if flip: of_nat_mod of_nat_diff) ultimatelyshow ?thesis by simp qed
lemma bit_word_rotr_iff [bit_simps]: ‹bit (word_rotr m w) n ⟷ n 🚫('a) ∧ bit w ((n + m) mod LENGTH('a))› for w :: ‹'a::len word› proof transfer fix k :: int and m n :: nat
define q where‹q = m mod LENGTH('a)› have‹q 🚫('a)› by (simp add: q_def) thenhave‹q ≤ LENGTH('a)› by simp have‹m mod LENGTH('a) = q› by (simp add: q_def) moreoverhave‹(n + m) mod LENGTH('a) = (n + q) mod LENGTH('a)› by (subst mod_add_right_eq [symmetric]) (simp add: ‹m mod LENGTH('a) = q›) moreoverhave‹n 🚫('a) ∧ bit (concat_bit (LENGTH('a) - q) (drop_bit q (take_bit LENGTH('a) k)) (take_bit q k)) n ⟷ n 🚫('a) ∧ bit k ((n + q) mod LENGTH('a))› using‹q 🚫('a)› by (cases ‹q + n ≥ LENGTH('a)›)
(auto simp: bit_concat_bit_iff bit_drop_bit_eq
bit_take_bit_iff le_mod_geq ac_simps) ultimatelyshow‹n 🚫('a) ∧ bit (concat_bit (LENGTH('a) - m mod LENGTH('a)) (drop_bit (m mod LENGTH('a)) (take_bit LENGTH('a) k)) (take_bit (m mod LENGTH('a)) k)) n ⟷ n 🚫('a) ∧ (n + m) mod LENGTH('a) 🚫('a) ∧ bit k ((n + m) mod LENGTH('a))› by simp qed
lemma bit_word_rotl_iff [bit_simps]: ‹bit (word_rotl m w) n ⟷ n 🚫('a) ∧ bit w ((n + (LENGTH('a) - m mod LENGTH('a))) mod LENGTH('a))› for w :: ‹'a::len word› by (simp add: word_rotl_eq_word_rotr bit_word_rotr_iff)
lemma bit_word_roti_iff [bit_simps]: ‹bit (word_roti k w) n ⟷ n 🚫('a) ∧ bit w (nat ((int n + k) mod int LENGTH('a)))› for w :: ‹'a::len word› proof transfer fix k l :: int and n :: nat
define m where‹m = nat (k mod int LENGTH('a))› have‹m 🚫('a)› by (simp add: nat_less_iff m_def) thenhave‹m ≤ LENGTH('a)› by simp have‹k mod int LENGTH('a) = int m› by (simp add: nat_less_iff m_def) moreoverhave‹(int n + k) mod int LENGTH('a) = int ((n + m) mod LENGTH('a))› by (subst mod_add_right_eq [symmetric]) (simp add: of_nat_mod ‹k mod int LENGTH('a) = int m›) moreoverhave‹n 🚫('a) ∧ bit (concat_bit (LENGTH('a) - m) (drop_bit m (take_bit LENGTH('a) l)) (take_bit m l)) n ⟷ n 🚫('a) ∧ bit l ((n + m) mod LENGTH('a))› using‹m 🚫('a)› by (cases ‹m + n ≥ LENGTH('a)›)
(auto simp: bit_concat_bit_iff bit_drop_bit_eq
bit_take_bit_iff nat_less_iff not_le not_less ac_simps
le_diff_conv le_mod_geq) ultimatelyshow‹n 🚫('a) ∧ bit (concat_bit (LENGTH('a) - nat (k mod int LENGTH('a))) (drop_bit (nat (k mod int LENGTH('a))) (take_bit LENGTH('a) l)) (take_bit (nat (k mod int LENGTH('a))) l)) n ⟷ n 🚫('a) ∧ nat ((int n + k) mod int LENGTH('a)) 🚫('a) ∧ bit l (nat ((int n + k) mod int LENGTH('a)))› by simp qed
lemma uint_word_rotr_eq: ‹uint (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (uint w)) (uint (take_bit (n mod LENGTH('a)) w))› for w :: ‹'a::len word› by transfer (simp add: take_bit_concat_bit_eq)
lemma [code]: ‹Word.the_int (word_rotr n w) = concat_bit (LENGTH('a) - n mod LENGTH('a)) (drop_bit (n mod LENGTH('a)) (Word.the_int w)) (Word.the_int (take_bit (n mod LENGTH('a)) w))› for w :: ‹'a::len word› using uint_word_rotr_eq [of n w] by simp
subsection‹Split and cat operations›
lift_definition word_cat :: ‹'a::len word ==> 'b::len word ==> 'c::len word› is‹λk l. concat_bit LENGTH('b) l (take_bit LENGTH('a) k)› by (simp add: bit_eq_iff bit_concat_bit_iff bit_take_bit_iff)
lemma word_cat_eq: ‹(word_cat v w :: 'c::len word) = push_bit LENGTH('b) (ucast v) + ucast w› for v :: ‹'a::len word›and w :: ‹'b::len word› by transfer (simp add: concat_bit_eq ac_simps)
lemma word_cat_eq' [code]: ‹word_cat a b = word_of_int (concat_bit LENGTH('b) (uint b) (uint a))› for a :: ‹'a::len word›and b :: ‹'b::len word› by transfer (simp add: concat_bit_take_bit_eq)
lemma bit_word_cat_iff [bit_simps]: ‹bit (word_cat v w :: 'c::len word) n ⟷ n 🚫('c) ∧ (if n 🚫('b) then bit w n else bit v (n - LENGTH('b)))› for v :: ‹'a::len word›and w :: ‹'b::len word› by transfer (simp add: bit_concat_bit_iff bit_take_bit_iff)
definition word_split :: ‹'a::len word ==> 'b::len word × 'c::len word› where‹word_split w = (ucast (drop_bit LENGTH('c) w) :: 'b::len word, ucast w :: 'c::len word)›
definition word_rcat :: ‹'a::len word list ==> 'b::len word› where‹word_rcat = word_of_int ∘ horner_sum uint (2 ^ LENGTH('a)) ∘ rev›
subsection‹More on conversions›
lemma int_word_sint: ‹sint (word_of_int x :: 'a::len word) = (x + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)› by transfer (simp flip: take_bit_eq_mod add: signed_take_bit_eq_take_bit_shift)
lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) bin" by (simp add: signed_of_int)
lemma uint_sint: "uint w = take_bit LENGTH('a) (sint w)" for w :: "'a::len word" by transfer (simp add: take_bit_signed_take_bit)
lemma bintr_uint: "LENGTH('a) ≤ n ==> take_bit n (uint w) = uint w" for w :: "'a::len word" by transfer (simp add: min_def)
lemma wi_bintr: "LENGTH('a::len) ≤ n ==> word_of_int (take_bit n w) = (word_of_int w :: 'a word)" by transfer simp
lemma word_numeral_alt: "numeral b = word_of_int (numeral b)" by simp
declare word_numeral_alt [symmetric, code_abbrev]
lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)" by simp
lemma uint_bintrunc [simp]: "uint (numeral bin :: 'a word) = take_bit LENGTH('a::len) (numeral bin)" by transfer rule
lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) = take_bit LENGTH('a::len) (- numeral bin)" by transfer rule
lemma sint_sbintrunc [simp]: "sint (numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (numeral bin)" by transfer simp
lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) = signed_take_bit (LENGTH('a::len) - 1) (- numeral bin)" by transfer simp
lemma unat_bintrunc [simp]: "unat (numeral bin :: 'a::len word) = take_bit LENGTH('a) (numeral bin)" by transfer simp
lemma unat_bintrunc_neg [simp]: "unat (- numeral bin :: 'a::len word) = nat (take_bit LENGTH('a) (- numeral bin))" by transfer simp
lemma size_0_eq: "size w = 0 ==> v = w" for v w :: "'a::len word" by transfer simp
lemma uint_ge_0 [iff]: "0 ≤ uint x" by (fact unsigned_greater_eq)
lemma uint_lt2p [iff]: "uint x < 2 ^ LENGTH('a)" for x :: "'a::len word" by (fact unsigned_less)
lemma sint_ge: "- (2 ^ (LENGTH('a) - 1)) ≤ sint x" for x :: "'a::len word" using sint_greater_eq [of x] by simp
lemma sint_lt: "sint x < 2 ^ (LENGTH('a) - 1)" for x :: "'a::len word" using sint_less [of x] by simp
lemma uint_m2p_neg: "uint x - 2 ^ LENGTH('a) < 0" for x :: "'a::len word" by (simp only: diff_less_0_iff_less uint_lt2p)
lemma uint_m2p_not_non_neg: "¬ 0 ≤ uint x - 2 ^ LENGTH('a)" for x :: "'a::len word" by (simp only: not_le uint_m2p_neg)
lemma lt2p_lem: "LENGTH('a) ≤ n ==> uint w < 2 ^ n" for w :: "'a::len word" using uint_bounded [of w] by (rule less_le_trans) simp
lemma uint_le_0_iff [simp]: "uint x ≤ 0 ⟷ uint x = 0" by (fact uint_ge_0 [THEN leD, THEN antisym_conv1])
lemma uint_nat: "uint w = int (unat w)" by transfer simp
lemma uint_numeral: "uint (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)" by (simp flip: take_bit_eq_mod add: of_nat_take_bit)
lemma uint_neg_numeral: "uint (- numeral b :: 'a::len word) = - numeral b mod 2 ^ LENGTH('a)" by (simp flip: take_bit_eq_mod add: of_nat_take_bit)
lemma unat_numeral: "unat (numeral b :: 'a::len word) = numeral b mod 2 ^ LENGTH('a)" by transfer (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq)
lemma sint_numeral: "sint (numeral b :: 'a::len word) = (numeral b + 2 ^ (LENGTH('a) - 1)) mod 2 ^ LENGTH('a) - 2 ^ (LENGTH('a) - 1)" by (metis int_word_sint word_numeral_alt)
lemma word_int_case_wi: "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ LENGTH('b::len))" by (simp add: uint_word_of_int word_int_case_eq_uint)
lemma word_int_split: "P (word_int_case f x) = (∀i. x = (word_of_int i :: 'b::len word) ∧ 0 ≤ i ∧ i < 2 ^ LENGTH('b) ⟶ P (f i))" by transfer (auto simp: take_bit_eq_mod)
lemma word_int_split_asm: "P (word_int_case f x) = (∄n. x = (word_of_int n :: 'b::len word) ∧ 0 ≤ n ∧ n < 2 ^ LENGTH('b::len) ∧¬ P (f n))" using word_int_split by auto
lemma uint_range_size: "0 ≤ uint w ∧ uint w < 2 ^ size w" by transfer simp
lemma sint_range_size: "- (2 ^ (size w - Suc 0)) ≤ sint w ∧ sint w < 2 ^ (size w - Suc 0)" by (simp add: word_size sint_greater_eq sint_less)
lemma sint_above_size: "2 ^ (size w - 1) ≤ x ==> sint w < x" for w :: "'a::len word" unfolding word_size by (rule less_le_trans [OF sint_lt])
lemma sint_below_size: "x ≤ - (2 ^ (size w - 1)) ==> x ≤ sint w" for w :: "'a::len word" unfolding word_size by (rule order_trans [OF _ sint_ge])
lemma word_unat_eq_iff: ‹v = w ⟷ unat v = unat w› for v w :: ‹'a::len word› by (fact word_eq_iff_unsigned)
subsection‹Testing bits›
lemma bin_nth_uint_imp: "bit (uint w) n ==> n < LENGTH('a)" for w :: "'a::len word" by (simp add: bit_uint_iff)
lemma bin_nth_sint: "LENGTH('a) ≤ n ==> bit (sint w) n = bit (sint w) (LENGTH('a) - 1)" for w :: "'a::len word" by (transfer fixing: n) (simp add: bit_signed_take_bit_iff le_diff_conv min_def)
lemma num_of_bintr': "take_bit (LENGTH('a::len)) (numeral a :: int) = (numeral b) ==> numeral a = (numeral b :: 'a word)" proof (transfer fixing: a b) assume‹take_bit LENGTH('a) (numeral a :: int) = numeral b› thenhave‹take_bit LENGTH('a) (take_bit LENGTH('a) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)› by simp thenshow‹take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)› by simp qed
lemma num_of_sbintr': "signed_take_bit (LENGTH('a::len) - 1) (numeral a :: int) = (numeral b) ==> numeral a = (numeral b :: 'a word)" proof (transfer fixing: a b) assume‹signed_take_bit (LENGTH('a) - 1) (numeral a :: int) = numeral b› thenhave‹take_bit LENGTH('a) (signed_take_bit (LENGTH('a) - 1) (numeral a :: int)) = take_bit LENGTH('a) (numeral b)› by simp thenshow‹take_bit LENGTH('a) (numeral a :: int) = take_bit LENGTH('a) (numeral b)› by (simp add: take_bit_signed_take_bit) qed
lemma num_abs_bintr: "(numeral x :: 'a word) = word_of_int (take_bit (LENGTH('a::len)) (numeral x))" by transfer simp
lemma num_abs_sbintr: "(numeral x :: 'a word) = word_of_int (signed_take_bit (LENGTH('a::len) - 1) (numeral x))" by transfer (simp add: take_bit_signed_take_bit)
text‹ ‹cast› - thusin‹cast w = w›, the type means cast to length of ‹w›! ›
lemma bit_ucast_iff: ‹bit (ucast a :: 'a::len word) n ⟷ n 🚫('a::len) ∧ bit a n› by transfer (simp add: bit_take_bit_iff)
lemma ucast_id [simp]: "ucast w = w" by transfer simp
lemma scast_id [simp]: "scast w = w" by transfer (simp add: take_bit_signed_take_bit)
lemma bit_last_iff: ‹bit w (LENGTH('a) - Suc 0) ⟷ sint w 🚫› (is‹?P ⟷ ?Q›) for w :: ‹'a::len word› by (simp add: bit_unsigned_iff sint_uint)
lemma drop_bit_eq_zero_iff_not_bit_last: ‹drop_bit (LENGTH('a) - Suc 0) w = 0 ⟷¬ bit w (LENGTH('a) - Suc 0)› for w :: "'a::len word" proof (cases ‹LENGTH('a)›) case (Suc n) thenshow ?thesis apply transfer apply (simp add: take_bit_drop_bit) by (simp add: bit_iff_odd_drop_bit drop_bit_take_bit odd_iff_mod_2_eq_one) qed auto
lemma unat_div: ‹unat (x div y) = unat x div unat y› by (fact unat_div_distrib)
lemma unat_mod: ‹unat (x mod y) = unat x mod unat y› by (fact unat_mod_distrib)
subsection‹Word Arithmetic›
lemmas less_eq_word_numeral_numeral [simp] =
word_le_def [of ‹numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_numeral_numeral [simp] =
word_less_def [of ‹numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_eq_word_minus_numeral_numeral [simp] =
word_le_def [of ‹- numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_minus_numeral_numeral [simp] =
word_less_def [of ‹- numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_eq_word_numeral_minus_numeral [simp] =
word_le_def [of ‹numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_numeral_minus_numeral [simp] =
word_less_def [of ‹numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_eq_word_minus_numeral_minus_numeral [simp] =
word_le_def [of ‹- numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_minus_numeral_minus_numeral [simp] =
word_less_def [of ‹- numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_numeral_minus_1 [simp] =
word_less_def [of ‹numeral a›‹- 1›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas less_word_minus_numeral_minus_1 [simp] =
word_less_def [of ‹- numeral a›‹- 1›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b
lemmas sless_eq_word_numeral_numeral [simp] =
word_sle_eq [of ‹numeral a›‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_word_numeral_numeral [simp] =
word_sless_alt [of ‹numeral a›‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_eq_word_minus_numeral_numeral [simp] =
word_sle_eq [of ‹- numeral a›‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_word_minus_numeral_numeral [simp] =
word_sless_alt [of ‹- numeral a›‹numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_eq_word_numeral_minus_numeral [simp] =
word_sle_eq [of ‹numeral a›‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_word_numeral_minus_numeral [simp] =
word_sless_alt [of ‹numeral a›‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_eq_word_minus_numeral_minus_numeral [simp] =
word_sle_eq [of ‹- numeral a›‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b lemmas sless_word_minus_numeral_minus_numeral [simp] =
word_sless_alt [of ‹- numeral a›‹- numeral b›, simplified sint_sbintrunc sint_sbintrunc_neg] for a b
lemmas div_word_numeral_numeral [simp] =
word_div_def [of ‹numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas div_word_minus_numeral_numeral [simp] =
word_div_def [of ‹- numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas div_word_numeral_minus_numeral [simp] =
word_div_def [of ‹numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas div_word_minus_numeral_minus_numeral [simp] =
word_div_def [of ‹- numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas div_word_minus_1_numeral [simp] =
word_div_def [of ‹- 1›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas div_word_minus_1_minus_numeral [simp] =
word_div_def [of ‹- 1›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b
lemmas mod_word_numeral_numeral [simp] =
word_mod_def [of ‹numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas mod_word_minus_numeral_numeral [simp] =
word_mod_def [of ‹- numeral a›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas mod_word_numeral_minus_numeral [simp] =
word_mod_def [of ‹numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas mod_word_minus_numeral_minus_numeral [simp] =
word_mod_def [of ‹- numeral a›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas mod_word_minus_1_numeral [simp] =
word_mod_def [of ‹- 1›‹numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b lemmas mod_word_minus_1_minus_numeral [simp] =
word_mod_def [of ‹- 1›‹- numeral b›, simplified uint_bintrunc uint_bintrunc_neg unsigned_minus_1_eq_mask mask_eq_exp_minus_1] for a b
lemma take_bit_word_beyond_length_eq: ‹take_bit n w = w›if‹LENGTH('a) ≤ n›for w :: ‹'a::len word› by (simp add: take_bit_word_eq_self that)
lemmas word_div_no [simp] = word_div_def [of "numeral a""numeral b"] for a b lemmas word_mod_no [simp] = word_mod_def [of "numeral a""numeral b"] for a b lemmas word_less_no [simp] = word_less_def [of "numeral a""numeral b"] for a b lemmas word_le_no [simp] = word_le_def [of "numeral a""numeral b"] for a b lemmas word_sless_no [simp] = word_sless_eq [of "numeral a""numeral b"] for a b lemmas word_sle_no [simp] = word_sle_eq [of "numeral a""numeral b"] for a b
lemma size_0_same': "size w = 0 ==> w = v" for v w :: "'a::len word" by (unfold word_size) simp
lemma bin_last_bintrunc: "odd (take_bit l n) ⟷ l > 0 ∧ odd n" by simp
lemma push_bit_word_beyond [simp]: ‹push_bit n w = 0›if‹LENGTH('a) ≤ n›for w :: ‹'a::len word› using that by (transfer fixing: n) (simp add: take_bit_push_bit)
lemma drop_bit_word_beyond [simp]: ‹drop_bit n w = 0›if‹LENGTH('a) ≤ n›for w :: ‹'a::len word› using that by (transfer fixing: n) (simp add: drop_bit_take_bit)
lemma signed_drop_bit_beyond: ‹signed_drop_bit n w = (if bit w (LENGTH('a) - Suc 0) then - 1 else 0)› if‹LENGTH('a) ≤ n›for w :: ‹'a::len word› by (rule bit_word_eqI) (simp add: bit_signed_drop_bit_iff that)
lemma take_bit_numeral_minus_numeral_word [simp]: ‹take_bit (numeral m) (- numeral n :: 'a::len word) = (case take_bit_num (numeral m) n of None ==> 0 | Some q ==> take_bit (numeral m) (2 ^ numeral m - numeral q))› proof (cases ‹LENGTH('a) ≤ numeral m›) case True thenhave *: ‹(take_bit (numeral m) :: 'a word ==> 'a word) = id› by (simp add: fun_eq_iff take_bit_word_eq_self) have **: ‹2 ^ numeral m = (0 :: 'a word)› using True by (simp flip: exp_eq_zero_iff) show ?thesis by (auto simp only: * ** split: option.split
dest!: take_bit_num_eq_None_imp [where ?'a = ‹'a word›] take_bit_num_eq_Some_imp [where?'a = ‹'a word›])
simp_all next case False thenshow ?thesis by (transfer fixing: m n) simp qed
lemma of_nat_inverse: ‹word_of_nat r = a ==> r 🚫 ^ LENGTH('a) ==> unat a = r› for a :: ‹'a::len word› by (metis id_apply of_nat_eq_id take_bit_nat_eq_self_iff unsigned_of_nat)
subsection‹Transferring goals from words to ints›
lemma word_ths: shows word_succ_p1: "word_succ a = a + 1" and word_pred_m1: "word_pred a = a - 1" and word_pred_succ: "word_pred (word_succ a) = a" and word_succ_pred: "word_succ (word_pred a) = a" and word_mult_succ: "word_succ a * b = b + a * b" by (transfer, simp add: algebra_simps)+
lemma uint_cong: "x = y ==> uint x = uint y" by simp
lemma uint_word_ariths: fixes a b :: "'a::len word" shows"uint (a + b) = (uint a + uint b) mod 2 ^ LENGTH('a::len)" and"uint (a - b) = (uint a - uint b) mod 2 ^ LENGTH('a)" and"uint (a * b) = uint a * uint b mod 2 ^ LENGTH('a)" and"uint (- a) = - uint a mod 2 ^ LENGTH('a)" and"uint (word_succ a) = (uint a + 1) mod 2 ^ LENGTH('a)" and"uint (word_pred a) = (uint a - 1) mod 2 ^ LENGTH('a)" and"uint (0 :: 'a word) = 0 mod 2 ^ LENGTH('a)" and"uint (1 :: 'a word) = 1 mod 2 ^ LENGTH('a)" by (simp_all only: word_arith_wis uint_word_of_int_eq flip: take_bit_eq_mod)
lemma uint_word_arith_bintrs: fixes a b :: "'a::len word" shows"uint (a + b) = take_bit (LENGTH('a)) (uint a + uint b)" and"uint (a - b) = take_bit (LENGTH('a)) (uint a - uint b)" and"uint (a * b) = take_bit (LENGTH('a)) (uint a * uint b)" and"uint (- a) = take_bit (LENGTH('a)) (- uint a)" and"uint (word_succ a) = take_bit (LENGTH('a)) (uint a + 1)" and"uint (word_pred a) = take_bit (LENGTH('a)) (uint a - 1)" and"uint (0 :: 'a word) = take_bit (LENGTH('a)) 0" and"uint (1 :: 'a word) = take_bit (LENGTH('a)) 1" by (simp_all add: uint_word_ariths take_bit_eq_mod)
context fixes a b :: "'a::len word" begin
lemma sint_word_add: "sint (a + b) = signed_take_bit (LENGTH('a) - 1) (sint a + sint b)" by transfer (simp add: signed_take_bit_add)
lemma sint_word_diff: "sint (a - b) = signed_take_bit (LENGTH('a) - 1) (sint a - sint b)" by transfer (simp add: signed_take_bit_diff)
lemma sint_word_mult: "sint (a * b) = signed_take_bit (LENGTH('a) - 1) (sint a * sint b)" by transfer (simp add: signed_take_bit_mult)
lemma sint_word_minus: "sint (- a) = signed_take_bit (LENGTH('a) - 1) (- sint a)" by transfer (simp add: signed_take_bit_minus)
lemma sint_word_succ: "sint (word_succ a) = signed_take_bit (LENGTH('a) - 1) (sint a + 1)" by (metis of_int_sint scast_id sint_sbintrunc' wi_hom_succ)
lemma sint_word_pred: "sint (word_pred a) = signed_take_bit (LENGTH('a) - 1) (sint a - 1)" by (metis of_int_sint scast_id sint_sbintrunc' wi_hom_pred)
lemma sint_word_01: "sint (0 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 0" "sint (1 :: 'a word) = signed_take_bit (LENGTH('a) - 1) 1" by (simp_all add: sint_uint)
🍋‹alternative approach to lifting arithmetic equalities› lemma word_of_int_Ex: "∃y. x = word_of_int y" by (rule_tac x="uint x"in exI) simp
subsection‹Order on fixed-length words›
lift_definition udvd :: ‹'a::len word ==> 'a::len word ==> bool› (infixl‹udvd› 50) is‹λk l. take_bit LENGTH('a) k dvd take_bit LENGTH('a) l›by simp
lemma udvd_iff_dvd: ‹x udvd y ⟷ unat x dvd unat y› by transfer (simp add: nat_dvd_iff)
lemma udvd_iff_dvd_int: ‹v udvd w ⟷ uint v dvd uint w› by transfer rule
lemma udvdI [intro]: ‹v udvd w›if‹unat w = unat v * unat u› proof - from that have‹unat v dvd unat w› .. thenshow ?thesis by (simp add: udvd_iff_dvd) qed
lemma udvdE [elim]: fixes v w :: ‹'a::len word› assumes‹v udvd w› obtains u :: ‹'a word›where‹unat w = unat v * unat u› proof (cases ‹v = 0›) case True moreoverfrom True ‹v udvd w›have‹w = 0› by transfer simp ultimatelyshow thesis using that by simp next case False thenhave‹unat v > 0› by (simp add: unat_gt_0) from‹v udvd w›have‹unat v dvd unat w› by (simp add: udvd_iff_dvd) thenobtain n where‹unat w = unat v * n› .. moreoverhave‹n 🚫 ^ LENGTH('a)› proof (rule ccontr) assume‹¬ n 🚫 ^ LENGTH('a)› thenhave‹n ≥ 2 ^ LENGTH('a)› by (simp add: not_le) thenhave‹unat v * n ≥ 2 ^ LENGTH('a)› using‹unat v > 0› mult_le_mono [of 1 ‹unat v›‹2 ^ LENGTH('a)› n] by simp with‹unat w = unat v * n› have‹unat w ≥ 2 ^ LENGTH('a)› by simp with unsigned_less [of w, where ?'a = nat] show False by linarith qed ultimatelyhave‹unat w = unat v * unat (word_of_nat n :: 'a word)› by (auto simp: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym) with that show thesis . qed
lemma udvd_imp_mod_eq_0: ‹w mod v = 0›if‹v udvd w› using that by transfer simp
lemma mod_eq_0_imp_udvd [intro?]: ‹v udvd w›if‹w mod v = 0› by (metis mod_0_imp_dvd that udvd_iff_dvd unat_0 unat_mod_distrib)
lemma udvd_imp_dvd: ‹v dvd w›if‹v udvd w›for v w :: ‹'a::len word› proof - from that obtain u :: ‹'a word›where‹unat w = unat v * unat u› .. thenhave‹w = v * u› by (metis of_nat_mult of_nat_unat word_mult_def word_of_int_uint) thenshow‹v dvd w› .. qed
lemma exp_dvd_iff_exp_udvd: ‹2 ^ n dvd w ⟷ 2 ^ n udvd w›for v w :: ‹'a::len word› proof assume‹2 ^ n udvd w›thenshow‹2 ^ n dvd w› by (rule udvd_imp_dvd) next assume‹2 ^ n dvd w› thenobtain u :: ‹'a word›where‹w = 2 ^ n * u› .. thenhave‹w = push_bit n u› by (simp add: push_bit_eq_mult) thenshow‹2 ^ n udvd w› by transfer (simp add: take_bit_push_bit dvd_eq_mod_eq_0 flip: take_bit_eq_mod) qed
lemma udvd_nat_alt: ‹a udvd b ⟷ (∃n. unat b = n * unat a)› by (auto simp: udvd_iff_dvd)
lemma udvd_unfold_int: ‹a udvd b ⟷ (∃n≥0. uint b = n * uint a)› unfolding udvd_iff_dvd_int by (metis dvd_div_mult_self dvd_triv_right uint_div_distrib uint_ge_0)
lemma unat_minus_one: ‹unat (w - 1) = unat w - 1›if‹w ≠ 0› proof - have"0 ≤ uint w"by (fact uint_nonnegative) moreoverfrom that have"0 ≠ uint w" by (simp add: uint_0_iff) ultimatelyhave"1 ≤ uint w" by arith from uint_lt2p [of w] have"uint w - 1 < 2 ^ LENGTH('a)" by arith with‹1 ≤ uint w›have"(uint w - 1) mod 2 ^ LENGTH('a) = uint w - 1" by (auto intro: mod_pos_pos_trivial) with‹1 ≤ uint w›have"nat ((uint w - 1) mod 2 ^ LENGTH('a)) = nat (uint w) - 1" by (auto simp del: nat_uint_eq) thenshow ?thesis by (metis uint_word_ariths(6) unat_eq_nat_uint word_pred_m1) qed
lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ LENGTH('a)" for x :: "'a::len word"and y :: "'b::len word" using uint_ge_0 [of y] uint_lt2p [of x] by arith
subsection‹Conditions for the addition (etc) of two words to overflow›
lemma uint_add_lem: "(uint x + uint y < 2 ^ LENGTH('a)) = (uint (x + y) = uint x + uint y)" for x y :: "'a::len word" by (metis add.right_neutral add_mono_thms_linordered_semiring(1) mod_pos_pos_trivial of_nat_0_le_iff uint_lt2p uint_nat uint_word_ariths(1))
lemma uint_mult_lem: "(uint x * uint y < 2 ^ LENGTH('a)) = (uint (x * y) = uint x * uint y)" for x y :: "'a::len word" by (metis mod_pos_pos_trivial uint_lt2p uint_mult_ge0 uint_word_ariths(3))
lemma uint_sub_lem: "uint x ≥ uint y ⟷ uint (x - y) = uint x - uint y" by (simp add: uint_word_arith_bintrs take_bit_int_eq_self_iff)
lemma uint_add_le: "uint (x + y) ≤ uint x + uint y" unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend)
lemma uint_sub_ge: "uint (x - y) ≥ uint x - uint y" by (smt (verit, ccfv_SIG) uint_nonnegative uint_sub_lem)
lemma int_mod_ge: ‹a ≤ a mod n›if‹a 🚫›‹0 🚫› for a n :: int using that order.trans [of a 0 ‹a mod n›] by (cases ‹a 🚫›) auto
lemma mod_add_if_z: "[x < z; y < z; 0 ≤ y; 0 ≤ x; 0 ≤ z]==> (x + y) mod z = (if x + y < z then x + y else x + y - z)" for x y z :: int by (smt (verit, best) minus_mod_self2 mod_pos_pos_trivial)
lemma uint_plus_if': "uint (a + b) = (if uint a + uint b < 2 ^ LENGTH('a) then uint a + uint b else uint a + uint b - 2 ^ LENGTH('a))" for a b :: "'a::len word" using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
lemma mod_sub_if_z: "[x < z; y < z; 0 ≤ y; 0 ≤ x; 0 ≤ z]==> (x - y) mod z = (if y ≤ x then x - y else x - y + z)" for x y z :: int using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp: not_le)
lemma uint_sub_if': "uint (a - b) = (if uint b ≤ uint a then uint a - uint b else uint a - uint b + 2 ^ LENGTH('a))" for a b :: "'a::len word" using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
lemma word_of_int_inverse: "word_of_int r = a ==> 0 ≤ r ==> r < 2 ^ LENGTH('a) ==> uint a = r" for a :: "'a::len word" by transfer (simp add: take_bit_int_eq_self)
lemma unat_split: "P (unat x) ⟷ (∀n. of_nat n = x ∧ n < 2^LENGTH('a) ⟶ P n)" for x :: "'a::len word" by (auto simp: unsigned_of_nat take_bit_nat_eq_self)
lemma unat_split_asm: "P (unat x) ⟷ (∄n. of_nat n = x ∧ n < 2^LENGTH('a) ∧¬ P n)" for x :: "'a::len word" using unat_split by auto
lemma un_ui_le: ‹unat a ≤ unat b ⟷ uint a ≤ uint b› by transfer (simp add: nat_le_iff)
lemma unat_plus_if': ‹unat (a + b) = (if unat a + unat b 🚫 ^ LENGTH('a) then unat a + unat b else unat a + unat b - 2 ^ LENGTH('a))› apply (auto simp: not_less le_iff_add) using of_nat_inverse apply force by (smt (verit, ccfv_SIG) numeral_Bit0 numerals(1) of_nat_0_le_iff of_nat_1 of_nat_add of_nat_eq_iff of_nat_power of_nat_unat uint_plus_if')
lemma unat_sub_if_size: "unat (x - y) = (if unat y ≤ unat x then unat x - unat y else unat x + 2 ^ size x - unat y)" proof -
{ assume xy: "¬ uint y ≤ uint x" have"nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)" by simp alsohave"… = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)" by (simp add: nat_diff_distrib') alsohave"… = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" by (simp add: nat_add_distrib nat_power_eq) finallyhave"nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
} thenshow ?thesis by (metis nat_diff_distrib' uint_range_size uint_sub_if' un_ui_le unat_eq_nat_uint
word_size) qed
lemma uint_split: "P (uint x) = (∀i. word_of_int i = x ∧ 0 ≤ i ∧ i < 2^LENGTH('a) ⟶ P i)" for x :: "'a::len word" by transfer (auto simp: take_bit_eq_mod)
lemma uint_split_asm: "P (uint x) = (∄i. word_of_int i = x ∧ 0 ≤ i ∧ i < 2^LENGTH('a) ∧¬ P i)" for x :: "'a::len word" by (auto simp: unsigned_of_int take_bit_int_eq_self)
subsection‹Some proof tool support›
🍋‹use this to stop, eg. ‹2 ^ LENGTH(32)› being simplified› lemma power_False_cong: "False ==> a ^ b = c ^ d" by auto
🍋‹‹unat_arith_tac›: tactic to reduce word arithmetic to‹nat›, try to solve via ‹arith›\<close>
ML ‹ val unat_arith_simpset = @{context} (* TODO: completely explicitly determined simpset *)
|> fold Simplifier.add_simp @{thms unat_arith_simps}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
|> simpset_of
fun unat_arith_tacs ctxt = let fun arith_tac' n t =
Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty; in
[ clarify_tac ctxt 1,
full_simp_tac (put_simpset unat_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms unat_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
REPEAT (eresolve_tac ctxt [conjE] n) THEN
REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
TRYALL arith_tac' ] end
fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt)) ›
method_setup unat_arith = ‹Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)› "solving word arithmetic via natural numbers and arith"
🍋‹‹uint_arith_tac›: reduce to arithmetic on int, try to solve by arith›
ML ‹ val uint_arith_simpset = @{context} (* TODO: completely explicitly determined simpset *)
|> fold Simplifier.add_simp @{thms uint_arith_simps}
|> fold Splitter.add_split @{thms if_split_asm}
|> fold Simplifier.add_cong @{thms power_False_cong}
|> simpset_of;
fun uint_arith_tacs ctxt = let fun arith_tac' n t =
Arith_Data.arith_tac ctxt n t
handle Cooper.COOPER _ => Seq.empty; in
[ clarify_tac ctxt 1,
full_simp_tac (put_simpset uint_arith_simpset ctxt) 1,
ALLGOALS (full_simp_tac
(put_simpset HOL_ss ctxt
|> fold Splitter.add_split @{thms uint_splits}
|> fold Simplifier.add_cong @{thms power_False_cong})),
rewrite_goals_tac ctxt @{thms word_size},
ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
REPEAT (eresolve_tac ctxt [conjE] n) THEN
REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n THEN assume_tac ctxt n THEN assume_tac ctxt n)),
TRYALL arith_tac' ] end
fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt)) ›
method_setup uint_arith = ‹Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)› "solving word arithmetic via integers and arith"
subsection‹More on overflows and monotonicity›
lemma no_plus_overflow_uint_size: "x ≤ x + y ⟷ uint x + uint y < 2 ^ size x" for x y :: "'a::len word" by (auto simp: word_size word_le_def uint_add_lem uint_sub_lem)
lemma word_less_sub1: "x ≠ 0 ==> 1 < x ⟷ 0 < x - 1" for x :: "'a::len word" by transfer (simp add: take_bit_decr_eq)
lemma word_le_sub1: "x ≠ 0 ==> 1 ≤ x ⟷ 0 ≤ x - 1" for x :: "'a::len word" by transfer (simp add: int_one_le_iff_zero_less less_le)
lemma sub_wrap_lt: "x < x - z ⟷ x < z" for x z :: "'a::len word" by (meson linorder_not_le word_sub_le_iff)
lemma sub_wrap: "x ≤ x - z ⟷ z = 0 ∨ x < z" for x z :: "'a::len word" by (simp add: le_less sub_wrap_lt ac_simps)
lemma plus_minus_not_NULL_ab: "x ≤ ab - c ==> c ≤ ab ==> c ≠ 0 ==> x + c ≠ 0" for x ab c :: "'a::len word" by uint_arith
lemma plus_minus_no_overflow_ab: "x ≤ ab - c ==> c ≤ ab ==> x ≤ x + c" for x ab c :: "'a::len word" by uint_arith
lemma le_minus': "a + c ≤ b ==> a ≤ a + c ==> c ≤ b - a" for a b c :: "'a::len word" by uint_arith
lemma le_plus': "a ≤ b ==> c ≤ b - a ==> a + c ≤ b" for a b c :: "'a::len word" by uint_arith
lemmas le_plus = le_plus' [rotated]
lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
lemma word_plus_mono_right: "y ≤ z ==> x ≤ x + z ==> x + y ≤ x + z" for x y z :: "'a::len word" by uint_arith
lemma word_less_minus_cancel: "y - x < z - x ==> x ≤ z ==> y < z" for x y z :: "'a::len word" by uint_arith
lemma word_less_minus_mono_left: "y < z ==> x ≤ y ==> y - x < z - x" for x y z :: "'a::len word" by uint_arith
lemma word_less_minus_mono: "a < c ==> d < b ==> a - b < a ==> c - d < c ==> a - b < c - d" for a b c d :: "'a::len word" by uint_arith
lemma word_le_minus_cancel: "y - x ≤ z - x ==> x ≤ z ==> y ≤ z" for x y z :: "'a::len word" by uint_arith
lemma word_le_minus_mono_left: "y ≤ z ==> x ≤ y ==> y - x ≤ z - x" for x y z :: "'a::len word" by uint_arith
lemma word_le_minus_mono: "a ≤ c ==> d ≤ b ==> a - b ≤ a ==> c - d ≤ c ==> a - b ≤ c - d" for a b c d :: "'a::len word" by uint_arith
lemma plus_le_left_cancel_wrap: "x + y' < x ==> x + y < x ==> x + y' < x + y ⟷ y' < y" for x y y' :: "'a::len word" by uint_arith
lemma plus_le_left_cancel_nowrap: "x ≤ x + y' ==> x ≤ x + y ==> x + y' < x + y ⟷ y' < y" for x y y' :: "'a::len word" by uint_arith
lemma word_plus_mono_right2: "a ≤ a + b ==> c ≤ b ==> a ≤ a + c" for a b c :: "'a::len word" by uint_arith
lemma word_less_add_right: "x < y - z ==> z ≤ y ==> x + z < y" for x y z :: "'a::len word" by uint_arith
lemma word_less_sub_right: "x < y + z ==> y ≤ x ==> x - y < z" for x y z :: "'a::len word" by uint_arith
lemma word_le_plus_either: "x ≤ y ∨ x ≤ z ==> y ≤ y + z ==> x ≤ y + z" for x y z :: "'a::len word" by uint_arith
lemma word_less_nowrapI: "x < z - k ==> k ≤ z ==> 0 < k ==> x < x + k" for x z k :: "'a::len word" by uint_arith
lemma inc_le: "i < m ==> i + 1 ≤ m" for i m :: "'a::len word" by uint_arith
lemma less_imp_less_eq_dec: ‹v ≤ w - 1›if‹v 🚫›for v w :: ‹'a::len word› using that proof transfer show‹take_bit LENGTH('a) k ≤ take_bit LENGTH('a) (l - 1)› if‹take_bit LENGTH('a) k 🚫 LENGTH('a) l› for k l :: int using that by (cases ‹take_bit LENGTH('a) l = 0›)
(auto simp add: take_bit_decr_eq) qed
lemma inc_less_eq_triv_imp: ‹w = - 1›if‹w + 1 ≤ w›for w :: ‹'a::len word› proof (rule ccontr) assume‹w ≠ - 1› with that show False by transfer (auto simp add: take_bit_eq_mask_iff dest: take_bit_decr_eq) qed
lemma less_eq_dec_triv_imp: ‹w = 0›if‹w ≤ w - 1›for w :: ‹'a::len word› proof (rule ccontr) assume‹w ≠ 0› with that show False by transfer (auto simp add: take_bit_eq_mask_iff dest: take_bit_decr_eq) qed
lemma inc_less_eq_iff: ‹v + 1 ≤ w ⟷ v = - 1 ∨ v 🚫›for v w :: ‹'a::len word› by (auto intro: inc_less_eq_triv_imp inc_le)
lemma less_eq_dec_iff: ‹v ≤ w - 1 ⟷ w = 0 ∨ v 🚫›for v w :: ‹'a::len word› by (auto intro: less_eq_dec_triv_imp less_imp_less_eq_dec)
lemma inc_i: "1 ≤ i ==> i < m ==> 1 ≤ i + 1 ∧ i + 1 ≤ m" for i m :: "'a::len word" by uint_arith
lemma dec_less_imp_less_eq: ‹v ≤ w›if‹v - 1 🚫›for v w :: ‹'a::len word› using that inc_le [of ‹v - 1› w] by simp
lemma less_inc_imp_less_eq: ‹v ≤ w›if‹v 🚫 + 1›for v w :: ‹'a::len word› using that less_imp_less_eq_dec [of v ‹w + 1›] by simp
lemma less_eq_dec_self_iff_eq: ‹w ≤ w - 1 ⟷ w = 0›for w :: ‹'a::len word› using less_eq_dec_iff [of w w] by simp
lemma inc_less_eq_self_iff_eq: ‹w + 1 ≤ w ⟷ w = - 1›for w :: ‹'a::len word› using inc_less_eq_triv_imp [of w] by auto
lemma udvd_incr_lem: "[up < uq; up = ua + n * uint K; uq = ua + n' * uint K] ==> up + uint K ≤ uq" by auto (metis int_distrib(1) linorder_not_less mult.left_neutral mult_right_mono uint_nonnegative zless_imp_add1_zle)
lemma udvd_incr': "p < q ==> uint p = ua + n * uint K ==> uint q = ua + n' * uint K ==> p + K ≤ q" unfolding word_less_alt word_le_def by (metis (full_types) order_trans udvd_incr_lem uint_add_le)
lemma udvd_decr': assumes"p < q""uint p = ua + n * uint K""uint q = ua + n' * uint K" shows"uint q = ua + n' * uint K ==> p ≤ q - K" proof - have"∧w v. uint (w::'a word) ≤ uint v + uint (w - v)" by (metis (no_types) add_diff_cancel_left' diff_add_cancel uint_add_le) moreoverhave"uint K + uint p ≤ uint q" using assms by (metis (no_types) add_diff_cancel_left' diff_add_cancel udvd_incr_lem word_less_def) ultimatelyshow ?thesis by (meson add_le_cancel_left order_trans word_less_eq_iff_unsigned) qed
lemma udvd_minus_le': "xy < k ==> z udvd xy ==> z udvd k ==> xy ≤ k - z" unfolding udvd_unfold_int by (meson udvd_decr0)
lemma udvd_incr2_K: "p < a + s ==> a ≤ a + s ==> K udvd s ==> K udvd p - a ==> a ≤ p ==> 0 < K ==> p ≤ p + K ∧ p + K ≤ a + s" unfolding udvd_unfold_int by (smt (verit, best) diff_add_cancel leD udvd_incr_lem uint_plus_if'
word_less_eq_iff_unsigned word_sub_le)
subsection‹Arithmetic type class instantiations›
lemmas word_le_0_iff [simp] =
word_zero_le [THEN leD, THEN antisym_conv1]
lemma word_of_int_nat: "0 ≤ x ==> word_of_int x = of_nat (nat x)" by simp
text‹ note that ‹iszero_def› i
which requires word length ‹≥ 1›, ie ‹'a::len word› › lemma iszero_word_no [simp]: "iszero (numeral bin :: 'a::len word) = iszero (take_bit LENGTH('a) (numeral bin :: int))" by (metis iszero_def uint_0_iff uint_bintrunc)
text‹Use ‹iszero› to simplify equalities between word numerals.›
lemma word_less_eq_imp_half_less_eq: ‹v div 2 ≤ w div 2›if‹v ≤ w›for v w :: ‹'a::len word› using that by (simp add: word_le_nat_alt unat_div div_le_mono)
lemma word_half_less_imp_less_eq: ‹v ≤ w›if‹v div 2 🚫 div 2›for v w :: ‹'a::len word› using that linorder_linear word_less_eq_imp_half_less_eq by fastforce
subsection‹Word and nat›
lemma word_nchotomy: "∀w :: 'a::len word. ∃n. w = of_nat n ∧ n < 2 ^ LENGTH('a)" by (metis of_nat_unat ucast_id unsigned_less)
lemma of_nat_eq: "of_nat n = w ⟷ (∃q. n = unat w + q * 2 ^ LENGTH('a))" for w :: "'a::len word" using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric] by (auto simp flip: take_bit_eq_mod simp add: unsigned_of_nat)
lemma of_nat_eq_size: "of_nat n = w ⟷ (∃q. n = unat w + q * 2 ^ size w)" unfolding word_size by (rule of_nat_eq)
lemma of_nat_0: "of_nat m = (0::'a::len word) ⟷ (∃q. m = q * 2 ^ LENGTH('a))" by (simp add: of_nat_eq)
lemma of_nat_2p [simp]: "of_nat (2 ^ LENGTH('a)) = (0::'a::len word)" by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
lemma of_nat_gt_0: "of_nat k ≠ 0 ==> 0 < k" by (cases k) auto
lemma of_nat_neq_0: "0 < k ==> k < 2 ^ LENGTH('a::len) ==> of_nat k ≠ (0 :: 'a word)" by (auto simp : of_nat_0)
lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)" by simp
lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)" by (simp add: wi_hom_mult)
lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)" by transfer (simp add: ac_simps)
lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0" by simp
lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)" by simp
lemma unat_add_lem: "unat x + unat y < 2 ^ LENGTH('a) ⟷ unat (x + y) = unat x + unat y" for x y :: "'a::len word" by (metis mod_less unat_word_ariths(1) unsigned_less)
lemma unat_mult_lem: "unat x * unat y < 2 ^ LENGTH('a) ⟷ unat (x * y) = unat x * unat y" for x y :: "'a::len word" by (metis mod_less unat_word_ariths(2) unsigned_less)
lemma le_no_overflow: "x ≤ b ==> a ≤ a + b ==> x ≤ a + b" for a b x :: "'a::len word" using word_le_plus_either by blast
lemma uint_div: ‹uint (x div y) = uint x div uint y› by (fact uint_div_distrib)
lemma uint_mod: ‹uint (x mod y) = uint x mod uint y› by (fact uint_mod_distrib)
lemma no_plus_overflow_unat_size: "x ≤ x + y ⟷ unat x + unat y < 2 ^ size x" for x y :: "'a::len word" unfolding word_size by unat_arith
lemmas unat_plus_simple =
trans [OF no_olen_add_nat unat_add_lem]
lemma word_div_mult: "[0 < y; unat x * unat y < 2 ^ LENGTH('a)]==> x * y div y = x" for x y :: "'a::len word" by (simp add: unat_eq_zero unat_mult_lem word_arith_nat_div)
lemma div_lt': "i ≤ k div x ==> unat i * unat x < 2 ^ LENGTH('a)" for i k x :: "'a::len word" by unat_arith (meson le_less_trans less_mult_imp_div_less not_le unsigned_less)
lemma div_lt_mult: "[i < k div x; 0 < x]==> i * x < k" for i k x :: "'a::len word" by (metis div_le_mono div_lt'' not_le unat_div word_div_mult word_less_iff_unsigned)
lemma div_le_mult: "[i ≤ k div x; 0 < x]==> i * x ≤ k" for i k x :: "'a::len word" by (metis div_lt' less_mult_imp_div_less not_less unat_arith_simps(2) unat_div unat_mult_lem)
lemma div_lt_uint': "i ≤ k div x ==> uint i * uint x < 2 ^ LENGTH('a)" for i k x :: "'a::len word" unfolding uint_nat by (metis div_lt' int_ops(7) of_nat_unat uint_mult_lem unat_mult_lem)
lemma word_le_exists': "x ≤ y ==>∃z. y = x + z ∧ uint x + uint z < 2 ^ LENGTH('a)" for x y z :: "'a::len word" by (metis add.commute diff_add_cancel no_olen_add)
lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
lemma le_unat_uoi: ‹y ≤ unat z ==> unat (word_of_nat y :: 'a word) = y› for z :: ‹'a::len word› by transfer (simp add: nat_take_bit_eq take_bit_nat_eq_self_iff le_less_trans)
lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n" for n b :: "'a::len word" by (fact div_mult_mod_eq)
lemma word_div_mult_le: "a div b * b ≤ a" for a b :: "'a::len word" by (metis div_le_mult mult_not_zero order.not_eq_order_implies_strict order_refl word_zero_le)
lemma word_mod_less_divisor: "0 < n ==> m mod n < n" for m n :: "'a::len word" by (simp add: unat_arith_simps)
lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)" by (induct n) (simp_all add: wi_hom_mult [symmetric])
lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)" by (simp add : word_of_int_power_hom [symmetric])
lemma unatSuc: "1 + n ≠ 0 ==> unat (1 + n) = Suc (unat n)" for n :: "'a::len word" by unat_arith
subsection‹Cardinality, finiteness of set of words›
lemma inj_on_word_of_int: ‹inj_on (word_of_int :: int ==> 'a word) {0..🚫^ LENGTH('a::len)}› unfolding inj_on_def by (metis atLeastLessThan_iff word_of_int_inverse)
lemma range_uint: ‹range (uint :: 'a word ==> int) = {0..🚫^ LENGTH('a::len)}› apply transfer apply (auto simp: image_iff) apply (metis take_bit_int_eq_self_iff) done
lemma UNIV_eq: ‹(UNIV :: 'a word set) = word_of_int ` {0..🚫^ LENGTH('a::len)}› by (auto simp: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
lemma card_word_size: "CARD('a word) = 2 ^ size x" for x :: "'a::len word" unfolding word_size by (rule card_word)
end
instance word :: (len) finite by standard (simp add: UNIV_eq)
subsection‹Bitwise Operations on Words›
context includes bit_operations_syntax begin
lemma word_wi_log_defs: "NOT (word_of_int a) = word_of_int (NOT a)" "word_of_int a AND word_of_int b = word_of_int (a AND b)" "word_of_int a OR word_of_int b = word_of_int (a OR b)" "word_of_int a XOR word_of_int b = word_of_int (a XOR b)" by (transfer, rule refl)+
lemma word_no_log_defs [simp]: "NOT (numeral a) = word_of_int (NOT (numeral a))" "NOT (- numeral a) = word_of_int (NOT (- numeral a))" "numeral a AND numeral b = word_of_int (numeral a AND numeral b)" "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)" "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)" "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)" "numeral a OR numeral b = word_of_int (numeral a OR numeral b)" "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)" "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)" "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)" "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)" "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)" "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)" "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)" by (transfer, rule refl)+
text‹Special cases for when one of the arguments equals 1.›
lemma word_bitwise_1_simps [simp]: "NOT (1::'a::len word) = -2" "1 AND numeral b = word_of_int (1 AND numeral b)" "1 AND - numeral b = word_of_int (1 AND - numeral b)" "numeral a AND 1 = word_of_int (numeral a AND 1)" "- numeral a AND 1 = word_of_int (- numeral a AND 1)" "1 OR numeral b = word_of_int (1 OR numeral b)" "1 OR - numeral b = word_of_int (1 OR - numeral b)" "numeral a OR 1 = word_of_int (numeral a OR 1)" "- numeral a OR 1 = word_of_int (- numeral a OR 1)" "1 XOR numeral b = word_of_int (1 XOR numeral b)" "1 XOR - numeral b = word_of_int (1 XOR - numeral b)" "numeral a XOR 1 = word_of_int (numeral a XOR 1)" "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)" apply (simp_all add: word_uint_eq_iff unsigned_not_eq unsigned_and_eq unsigned_or_eq
unsigned_xor_eq of_nat_take_bit ac_simps unsigned_of_int) apply (simp_all add: minus_numeral_eq_not_sub_one) apply (simp_all only: sub_one_eq_not_neg bit.xor_compl_right take_bit_xor bit.double_compl) apply simp_all done
text‹Special cases for when one of the arguments equals -1.›
lemma word_bitwise_m1_simps [simp]: "NOT (-1::'a::len word) = 0" "(-1::'a::len word) AND x = x" "x AND (-1::'a::len word) = x" "(-1::'a::len word) OR x = -1" "x OR (-1::'a::len word) = -1" " (-1::'a::len word) XOR x = NOT x" "x XOR (-1::'a::len word) = NOT x" by (transfer, simp)+
lemma word_of_int_not_numeral_eq [simp]: ‹(word_of_int (NOT (numeral bin)) :: 'a::len word) = - numeral bin - 1› by transfer (simp add: not_eq_complement)
lemma uint_and: ‹uint (x AND y) = uint x AND uint y› by transfer simp
lemma uint_or: ‹uint (x OR y) = uint x OR uint y› by transfer simp
lemma uint_xor: ‹uint (x XOR y) = uint x XOR uint y› by transfer simp
🍋‹get from commutativity, associativity etc of ‹int_and› etc to same for‹word_and etc›\<close> lemmas bwsimps =
wi_hom_add
word_wi_log_defs
lemma word_bw_assocs: "(x AND y) AND z = x AND y AND z" "(x OR y) OR z = x OR y OR z" "(x XOR y) XOR z = x XOR y XOR z" for x :: "'a::len word" by (fact ac_simps)+
lemma word_bw_comms: "x AND y = y AND x" "x OR y = y OR x" "x XOR y = y XOR x" for x :: "'a::len word" by (fact ac_simps)+
lemma word_bw_lcs: "y AND x AND z = x AND y AND z" "y OR x OR z = x OR y OR z" "y XOR x XOR z = x XOR y XOR z" for x :: "'a::len word" by (fact ac_simps)+
lemma word_log_esimps: "x AND 0 = 0" "x AND -1 = x" "x OR 0 = x" "x OR -1 = -1" "x XOR 0 = x" "x XOR -1 = NOT x" "0 AND x = 0" "-1 AND x = x" "0 OR x = x" "-1 OR x = -1" "0 XOR x = x" "-1 XOR x = NOT x" for x :: "'a::len word" by simp_all
lemma word_not_dist: "NOT (x OR y) = NOT x AND NOT y" "NOT (x AND y) = NOT x OR NOT y" for x :: "'a::len word" by simp_all
lemma word_bw_same: "x AND x = x" "x OR x = x" "x XOR x = 0" for x :: "'a::len word" by simp_all
lemma word_ao_absorbs [simp]: "x AND (y OR x) = x" "x OR y AND x = x" "x AND (x OR y) = x" "y AND x OR x = x" "(y OR x) AND x = x" "x OR x AND y = x" "(x OR y) AND x = x" "x AND y OR x = x" for x :: "'a::len word" by (auto intro: bit_eqI simp add: bit_and_iff bit_or_iff)
lemma word_not_not [simp]: "NOT (NOT x) = x" for x :: "'a::len word" by (fact bit.double_compl)
lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z" for x :: "'a::len word" by (fact bit.conj_disj_distrib2)
lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)" for x :: "'a::len word" by (fact bit.disj_conj_distrib2)
lemma word_add_not [simp]: "x + NOT x = -1" for x :: "'a::len word" by (simp add: not_eq_complement)
lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y" for x :: "'a::len word" by transfer (simp add: plus_and_or)
lemma leoa: "w = x OR y ==> y = w AND y" for x :: "'a::len word" by auto
lemma leao: "w' = x' AND y' ==> x' = x' OR w'" for x' :: "'a::len word" by auto
lemma word_ao_equiv: "w = w OR w' ⟷ w' = w AND w'" for w w' :: "'a::len word" by (auto intro: leoa leao)
lemma le_word_or2: "x ≤ x OR y" for x y :: "'a::len word" by (simp add: or_greater_eq uint_or word_le_def)
lemma bit_horner_sum_bit_word_iff [bit_simps]: ‹bit (horner_sum of_bool (2 :: 'a::len word) bs) n ⟷ n 🚫 LENGTH('a) (length bs) ∧ bs ! n› by transfer (simp add: bit_horner_sum_bit_iff)
definition word_reverse :: ‹'a::len word ==> 'a word› where‹word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..🚫'a)]))›
lemma bit_word_reverse_iff [bit_simps]: ‹bit (word_reverse w) n ⟷ n 🚫('a) ∧ bit w (LENGTH('a) - Suc n)› for w :: ‹'a::len word› by (cases ‹n 🚫('a)›)
(simp_all add: word_reverse_def bit_horner_sum_bit_word_iff rev_nth)
lemma align_lem_or: assumes"length xs = n + m""length ys = n + m" and"drop m xs = replicate n False""take m ys = replicate m False" shows"map2 (∨) xs ys = take m xs @ drop m ys" using assms proof (induction xs arbitrary: ys m) case (Cons a xs) thenshow ?case by (cases m) (auto simp: length_Suc_conv False_map2_or) qed auto
lemma align_lem_and: assumes"length xs = n + m""length ys = n + m" and"drop m xs = replicate n False""take m ys = replicate m False" shows"map2 (∧) xs ys = replicate (n + m) False" using assms proof (induction xs arbitrary: ys m) case (Cons a xs) thenshow ?case by (cases m) (auto simp: length_Suc_conv set_replicate_conv_if False_map2_and) qed auto
lemma mask_eq_decr_exp: ‹mask n = 2 ^ n - (1 :: 'a::len word)› by (fact mask_eq_exp_minus_1)
lemma mask_Suc_rec: ‹mask (Suc n) = 2 * mask n + (1 :: 'a::len word)› by (simp add: mask_eq_exp_minus_1)
context begin
qualified lemma bit_mask_iff [bit_simps]: ‹bit (mask m :: 'a::len word) n ⟷ n 🚫 LENGTH('a) m› by (simp add: bit_mask_iff not_le)
end
lemma mask_bin: "mask n = word_of_int (take_bit n (- 1))" by transfer simp
lemma and_mask_bintr: "w AND mask n = word_of_int (take_bit n (uint w))" by transfer (simp add: ac_simps take_bit_eq_mask)
lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (take_bit n i)" by (simp add: take_bit_eq_mask of_int_and_eq of_int_mask_eq)
lemma and_mask_wi': "word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)" by (auto simp: and_mask_wi min_def wi_bintr)
lemma and_mask_no: "numeral i AND mask n = word_of_int (take_bit n (numeral i))" unfolding word_numeral_alt by (rule and_mask_wi)
lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)" by (simp only: and_mask_bintr take_bit_eq_mod)
lemma uint_mask_eq: ‹uint (mask n :: 'a::len word) = mask (min LENGTH('a) n)› by transfer simp
lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n" by (metis take_bit_eq_mask take_bit_int_less_exp unsigned_take_bit_eq)
lemma mask_eq_iff: "w AND mask n = w ⟷ uint w < 2 ^ n" by (metis and_mask_bintr and_mask_lt_2p take_bit_int_eq_self take_bit_nonnegative
uint_sint word_of_int_uint)
lemma and_mask_dvd: "2 ^ n dvd uint w ⟷ w AND mask n = 0" by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 uint_0_iff)
lemma and_mask_dvd_nat: "2 ^ n dvd unat w ⟷ w AND mask n = 0" by (simp flip: take_bit_eq_mask take_bit_eq_mod unsigned_take_bit_eq add: dvd_eq_mod_eq_0 unat_0_iff uint_0_iff)
lemma word_2p_lem: "n < size w ==> w < 2 ^ n = (uint w < 2 ^ n)" for w :: "'a::len word" by transfer simp
lemma less_mask_eq: fixes x :: "'a::len word" assumes"x < 2 ^ n"shows"x AND mask n = x" by (metis (no_types) assms lt2p_lem mask_eq_iff not_less word_2p_lem word_size)
lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
lemma and_mask_less_size: "n < size x ==> x AND mask n < 2 ^ n" for x :: ‹'a::len word› unfolding word_size by (erule and_mask_less')
lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n ==> c > 0 ==> x mod c = x AND mask n" for c x :: "'a::len word" by (auto simp: word_mod_def uint_2p and_mask_mod_2p)
lemma mask_eqs: "(a AND mask n) + b AND mask n = a + b AND mask n" "a + (b AND mask n) AND mask n = a + b AND mask n" "(a AND mask n) - b AND mask n = a - b AND mask n" "a - (b AND mask n) AND mask n = a - b AND mask n" "a * (b AND mask n) AND mask n = a * b AND mask n" "(b AND mask n) * a AND mask n = b * a AND mask n" "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n" "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n" "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n" "- (a AND mask n) AND mask n = - a AND mask n" "word_succ (a AND mask n) AND mask n = word_succ a AND mask n" "word_pred (a AND mask n) AND mask n = word_pred a AND mask n" using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b] unfolding take_bit_eq_mask [symmetric] by (transfer; simp add: take_bit_eq_mod mod_simps)+
lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n" for x :: ‹'a::len word› using word_of_int_Ex [where x=x] unfolding take_bit_eq_mask [symmetric] by (transfer; simp add: take_bit_eq_mod mod_simps)+
lemma mask_full [simp]: "mask LENGTH('a) = (- 1 :: 'a::len word)" by transfer simp
subsubsection ‹Slices›
definition slice1 :: ‹nat ==> 'a::len word ==> 'b::len word› where‹slice1 n w = (if n 🚫('a) then ucast (drop_bit (LENGTH('a) - n) w) else push_bit (n - LENGTH('a)) (ucast w))›
lemma bit_slice1_iff [bit_simps]: ‹bit (slice1 m w :: 'b::len word) n ⟷ m - LENGTH('a) ≤ n ∧ n 🚫 LENGTH('b) m ∧ bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))› for w :: ‹'a::len word› by (auto simp: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps
dest: bit_imp_le_length)
definition slice :: ‹nat ==> 'a::len word ==> 'b::len word› where‹slice n = slice1 (LENGTH('a) - n)›
lemma bit_slice_iff [bit_simps]: ‹bit (slice m w :: 'b::len word) n ⟷ n 🚫 LENGTH('b) (LENGTH('a) - m) ∧ bit w (n + LENGTH('a) - (LENGTH('a) - m))› for w :: ‹'a::len word› by (simp add: slice_def word_size bit_slice1_iff)
lemma slice1_0 [simp] : "slice1 n 0 = 0" unfolding slice1_def by simp
lemma slice_0 [simp] : "slice n 0 = 0" unfolding slice_def by auto
lemma ucast_slice1: "ucast w = slice1 (size w) w" unfolding slice1_def by (simp add: size_word.rep_eq)
lemma ucast_slice: "ucast w = slice 0 w" by (simp add: slice_def slice1_def)
lemma slice_id: "slice 0 t = t" by (simp only: ucast_slice [symmetric] ucast_id)
lemma rev_slice1: ‹slice1 n (word_reverse w :: 'b::len word) = word_reverse (slice1 k w :: 'a::len word)› if‹n + k = LENGTH('a) + LENGTH('b)› proof (rule bit_word_eqI) fix m assume *: ‹m 🚫('a)› from that have **: ‹LENGTH('b) = n + k - LENGTH('a)› by simp show‹bit (slice1 n (word_reverse w :: 'b word) :: 'a word) m ⟷ bit (word_reverse (slice1 k w :: 'a word)) m› unfolding bit_slice1_iff bit_word_reverse_iff using * ** by (cases ‹n ≤ LENGTH('a)›; cases ‹k ≤ LENGTH('a)›) auto qed
lemma rev_slice: "n + k + LENGTH('a::len) = LENGTH('b::len) ==> slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)" unfolding slice_def word_size by (simp add: rev_slice1)
lemma bit_revcast_iff [bit_simps]: ‹bit (revcast w :: 'b::len word) n ⟷ LENGTH('b) - LENGTH('a) ≤ n ∧ n 🚫('b) ∧ bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))› for w :: ‹'a::len word› by (simp add: revcast_def bit_slice1_iff)
lemma revcast_slice1 [OF refl]: "rc = revcast w ==> slice1 (size rc) w = rc" by (simp add: revcast_def word_size)
lemma split_slices: assumes"word_split w = (u, v)" shows"u = slice (size v) w ∧ v = slice 0 w" unfolding word_size proof (intro conjI) have🍋: "∧n. [ucast (drop_bit LENGTH('b) w) = u; LENGTH('c) < LENGTH('b)]==>¬ bit u n" by (metis bit_take_bit_iff bit_word_of_int_iff diff_is_0_eq' drop_bit_take_bit less_imp_le less_nat_zero_code of_int_uint unsigned_drop_bit_eq) show"u = slice LENGTH('b) w" proof (rule bit_word_eqI) show"bit u n = bit ((slice LENGTH('b) w)::'a word) n"if"n < LENGTH('a)"for n using assms bit_imp_le_length unfolding word_split_def bit_slice_iff by (fastforce simp: 🍋 ac_simps word_size bit_ucast_iff bit_drop_bit_eq) qed show"v = slice 0 w" by (metis Pair_inject assms ucast_slice word_split_bin') qed
lemma slice_cat1 [OF refl]: "[wc = word_cat a b; size a + size b ≤ size wc]==> slice (size b) wc = a" by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
lemmas slice_cat2 = trans [OF slice_id word_cat_id]
lemma cat_slices: "[a = slice n c; b = slice 0 c; n = size b; size c ≤ size a + size b]==> word_cat a b = c" by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
lemma word_split_cat_alt: assumes"w = word_cat u v"and size: "size u + size v ≤ size w" shows"word_split w = (u,v)" proof - have"ucast ((drop_bit LENGTH('c) (word_cat u v))::'a word) = u""ucast ((word_cat u v)::'a word) = v" using assms by (auto simp: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI) thenshow ?thesis by (simp add: assms(1) word_split_bin') qed
lemma horner_sum_uint_exp_Cons_eq: ‹horner_sum uint (2 ^ LENGTH('a)) (w # ws) = concat_bit LENGTH('a) (uint w) (horner_sum uint (2 ^ LENGTH('a)) ws)› for ws :: ‹'a::len word list› by (simp add: bintr_uint concat_bit_eq push_bit_eq_mult)
lemma bit_horner_sum_uint_exp_iff: ‹bit (horner_sum uint (2 ^ LENGTH('a)) ws) n ⟷ n div LENGTH('a) 🚫 ws ∧ bit (ws ! (n div LENGTH('a))) (n mod LENGTH('a))› for ws :: ‹'a::len word list› proof (induction ws arbitrary: n) case Nil thenshow ?case by simp next case (Cons w ws) thenshow ?case by (cases ‹n ≥ LENGTH('a)›)
(simp_all only: horner_sum_uint_exp_Cons_eq, simp_all add: bit_concat_bit_iff le_div_geq le_mod_geq bit_uint_iff Cons) qed
subsection‹Rotation›
lemma word_rotr_word_rotr_eq: ‹word_rotr m (word_rotr n w) = word_rotr (m + n) w› by (rule bit_word_eqI) (simp add: bit_word_rotr_iff ac_simps mod_add_right_eq)
lemma word_rot_lem: "[l + k = d + k mod l; n < l]==> ((d + n) mod l) = n"for l::nat by (metis (no_types, lifting) add.commute add.right_neutral add_diff_cancel_left' mod_if mod_mult_div_eq mod_mult_self2 mod_self)
lemma word_rot_rl [simp]: ‹word_rotl k (word_rotr k v) = v› proof (rule bit_word_eqI) show"bit (word_rotl k (word_rotr k v)) n = bit v n"if"n < LENGTH('a)"for n using that by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split) qed
lemma word_rot_lr [simp]: ‹word_rotr k (word_rotl k v) = v› proof (rule bit_word_eqI) show"bit (word_rotr k (word_rotl k v)) n = bit v n"if"n < LENGTH('a)"for n using that by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split) qed
lemma word_rot_gal: ‹word_rotr n v = w ⟷ word_rotl n w = v› by auto
lemma word_rot_gal': ‹w = word_rotr n v ⟷ v = word_rotl n w› by auto
lemma word_reverse_word_rotl: ‹word_reverse (word_rotl n w) = word_rotr n (word_reverse w)› (is‹?lhs = ?rhs›) proof (rule bit_word_eqI) fix m assume‹m 🚫('a)› thenhave‹int (LENGTH('a) - Suc ((m + n) mod LENGTH('a))) = int ((LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a))› unfolding of_nat_diff of_nat_mod apply (simp add: Suc_le_eq add_less_le_mono of_nat_mod algebra_simps) apply (simp only: mod_diff_left_eq [symmetric, of ‹int LENGTH('a) * 2›] mod_mult_self1_is_0 diff_0 minus_mod_int_eq) apply (simp add: mod_simps) done thenhave‹LENGTH('a) - Suc ((m + n) mod LENGTH('a)) = (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a)› by simp with‹m 🚫('a)›show‹bit ?lhs m ⟷ bit ?rhs m› by (simp add: bit_simps) qed
lemma word_reverse_word_rotr: ‹word_reverse (word_rotr n w) = word_rotl n (word_reverse w)› by (rule word_eq_reverseI) (simp add: word_reverse_word_rotl)
lemma word_rotl_rev: ‹word_rotl n w = word_reverse (word_rotr n (word_reverse w))› by (simp add: word_reverse_word_rotr)
lemma word_rotr_rev: ‹word_rotr n w = word_reverse (word_rotl n (word_reverse w))› by (simp add: word_reverse_word_rotl)
lemma word_roti_0 [simp]: "word_roti 0 w = w" by transfer simp
lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)" by (rule bit_word_eqI)
(simp add: bit_word_roti_iff nat_less_iff mod_simps ac_simps)
lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w" by transfer simp
subsubsection ‹"Word rotation commutes with bit-wise operations›
🍋‹using locale to not pollute lemma namespace› locale word_rotate begin
context includes bit_operations_syntax begin
lemma word_rot_logs: "word_rotl n (NOT v) = NOT (word_rotl n v)" "word_rotr n (NOT v) = NOT (word_rotr n v)" "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y" "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y" "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y" "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y" "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y" "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y" by (rule bit_word_eqI, auto simp: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
end
end
lemmas word_rot_logs = word_rotate.word_rot_logs
lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 ∧ word_rotl i 0 = 0" by transfer simp_all
lemma word_roti_0' [simp] : "word_roti n 0 = 0" by transfer simp
declare word_roti_eq_word_rotr_word_rotl [simp]
subsection‹Maximum machine word›
context includes bit_operations_syntax begin
lemma word_int_cases: fixes x :: "'a::len word" obtains n where"x = word_of_int n"and"0 ≤ n"and"n < 2^LENGTH('a)" by (rule that [of ‹uint x›]) simp_all
lemma word_nat_cases [cases type: word]: fixes x :: "'a::len word" obtains n where"x = of_nat n"and"n < 2^LENGTH('a)" by (rule that [of ‹unat x›]) simp_all
lemma max_word_max [intro!]: ‹n ≤ - 1›for n :: ‹'a::len word› by (fact word_order.extremum)
lemma max_word_wrap: ‹x + 1 = 0 ==> x = - 1›for x :: ‹'a::len word› by (simp add: eq_neg_iff_add_eq_0)
lemma word_and_max: ‹x AND - 1 = x›for x :: ‹'a::len word› by (fact word_log_esimps)
lemma word_or_max: ‹x OR - 1 = - 1›for x :: ‹'a::len word› by (fact word_log_esimps)
lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z" for x y z :: "'a::len word" by (fact bit.conj_disj_distrib)
lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)" for x y z :: "'a::len word" by (fact bit.disj_conj_distrib)
lemma word_and_not [simp]: "x AND NOT x = 0" for x :: "'a::len word" by (fact bit.conj_cancel_right)
lemma word_or_not [simp]: ‹x OR NOT x = - 1›for x :: ‹'a::len word› by (fact bit.disj_cancel_right)
lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y" for x y :: "'a::len word" by (fact bit.xor_def)
lemma uint_lt_0 [simp]: "uint x < 0 = False" by (simp add: linorder_not_less)
lemma word_less_1 [simp]: "x < 1 ⟷ x = 0" for x :: "'a::len word" by (simp add: word_less_nat_alt unat_0_iff)
lemma uint_plus_if_size: "uint (x + y) = (if uint x + uint y < 2^size x then uint x + uint y else uint x + uint y - 2^size x)" by (simp add: take_bit_eq_mod word_size uint_word_of_int_eq uint_plus_if')
lemma unat_plus_if_size: "unat (x + y) = (if unat x + unat y < 2^size x then unat x + unat y else unat x + unat y - 2^size x)" for x y :: "'a::len word" by (simp add: size_word.rep_eq unat_arith_simps)
lemma word_neq_0_conv: "w ≠ 0 ⟷ 0 < w" for w :: "'a::len word" by (fact word_coorder.not_eq_extremum)
lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c" for c :: "'a::len word" by (fact unat_div)
lemma uint_sub_if_size: "uint (x - y) = (if uint y ≤ uint x then uint x - uint y else uint x - uint y + 2^size x)" by (simp add: size_word.rep_eq uint_sub_if')
lemma unat_sub: ‹unat (a - b) = unat a - unat b› if‹b ≤ a› by (meson that unat_sub_if_size word_le_nat_alt)
lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
lemma word_of_int_inj: ‹(word_of_int x :: 'a::len word) = word_of_int y ⟷ x = y› if‹0 ≤ x ∧ x 🚫 ^ LENGTH('a)›‹0 ≤ y ∧ y 🚫 ^ LENGTH('a)› using that by (transfer fixing: x y) (simp add: take_bit_int_eq_self)
lemma word_le_less_eq: "x ≤ y ⟷ x = y ∨ x < y" for x y :: "'z::len word" by (auto simp: order_class.le_less)
lemma mod_plus_cong: fixes b b' :: int assumes 1: "b = b'" and 2: "x mod b' = x' mod b'" and 3: "y mod b' = y' mod b'" and 4: "x' + y' = z'" shows"(x + y) mod b = z' mod b'" proof - from 1 2[symmetric] 3[symmetric] have"(x + y) mod b = (x' mod b' + y' mod b') mod b'" by (simp add: mod_add_eq) alsohave"… = (x' + y') mod b'" by (simp add: mod_add_eq) finallyshow ?thesis by (simp add: 4) qed
lemma mod_minus_cong: fixes b b' :: int assumes"b = b'" and"x mod b' = x' mod b'" and"y mod b' = y' mod b'" and"x' - y' = z'" shows"(x - y) mod b = z' mod b'" using assms [symmetric] by (auto intro: mod_diff_cong)
lemma word_induct_less [case_names zero less]: ‹P m›if zero: ‹P 0›and less: ‹∧n. n 🚫==> P n ==> P (1 + n)› for m :: ‹'a::len word› proof -
define q where‹q = unat m› with less have‹∧n. n 🚫 q ==> P n ==> P (1 + n)› by simp thenhave‹P (word_of_nat q :: 'a word)› proof (induction q) case 0 show ?case by (simp add: zero) next case (Suc q) show ?case proof (cases ‹1 + word_of_nat q = (0 :: 'a word)›) case True thenshow ?thesis by (simp add: zero) next case False thenhave *: ‹word_of_nat q 🚫word_of_nat (Suc q) :: 'a word)› by (simp add: unatSuc word_less_nat_alt) thenhave **: ‹n 🚫1 + word_of_nat q :: 'a word) ⟷ n ≤ (word_of_nat q :: 'a word)›for n by (metis (no_types, lifting) add.commute inc_le le_less_trans not_less of_nat_Suc) have‹P (word_of_nat q)› by (simp add: "**" Suc.IH Suc.prems) with * have‹P (1 + word_of_nat q)› by (rule Suc.prems) thenshow ?thesis by simp qed qed with‹q = unat m›show ?thesis by simp qed
lemma word_induct: "P 0 ==> (∧n. P n ==> P (1 + n)) ==> P m" for P :: "'a::len word ==> bool" by (rule word_induct_less)
lemma word_induct2 [case_names zero suc, induct type]: "P 0 ==> (∧n. 1 + n ≠ 0 ==> P n ==> P (1 + n)) ==> P n" for P :: "'b::len word ==> bool" by (induction rule: word_induct_less; force)
subsection‹Recursion combinator for words›
definition word_rec :: "'a ==> ('b::len word ==> 'a ==> 'a) ==> 'b word ==> 'a" where"word_rec forZero forSuc n = rec_nat forZero (forSuc ∘ of_nat) (unat n)"
lemma word_rec_0 [simp]: "word_rec z s 0 = z" by (simp add: word_rec_def)
lemma word_rec_Suc [simp]: "1 + n ≠ 0 ==> word_rec z s (1 + n) = s n (word_rec z s n)" for n :: "'a::len word" by (simp add: unatSuc word_rec_def)
lemma word_rec_Pred: "n ≠ 0 ==> word_rec z s n = s (n - 1) (word_rec z s (n - 1))" by (metis add.commute diff_add_cancel word_rec_Suc)
lemma word_rec_in: "f (word_rec z (λ_. f) n) = word_rec (f z) (λ_. f) n" by (induct n) simp_all
lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f ∘ (+) 1) n" by (induct n) simp_all
lemma word_rec_twice: "m ≤ n ==> word_rec z f n = word_rec (word_rec z f (n - m)) (f ∘ (+) (n - m)) m" proof (induction n arbitrary: z f) case zero thenshow ?case by (metis diff_0_right word_le_0_iff word_rec_0) next case (suc n z f) show ?case proof (cases "1 + (n - m) = 0") case True thenshow ?thesis by (simp add: add_diff_eq) next case False thenhave eq: "1 + n - m = 1 + (n - m)" by simp with False have"m ≤ n" using inc_le linorder_not_le suc.prems word_le_minus_mono_left by fastforce with False "suc.hyps"show ?thesis using suc.IH [of "f 0 z""f ∘ (+) 1"] by (simp add: word_rec_in2 eq add.assoc o_def) qed qed
lemma word_rec_id: "word_rec z (λ_. id) n = z" by (induct n) auto
lemma word_rec_id_eq: "(∧m. m < n ==> f m = id) ==> word_rec z f n = z" by (induction n) (auto simp: unatSuc unat_arith_simps(2))
lemma word_rec_max: assumes"∀m≥n. m ≠ - 1 ⟶ f m = id" shows"word_rec z f (- 1) = word_rec z f n" proof - have🍋: "∧m. [m < - 1 - n]==> (f ∘ (+) n) m = id" using assms by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge) have"word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f ∘ (+) (- 1 - (- 1 - n))) (- 1 - n)" by (meson word_n1_ge word_rec_twice) alsohave"… = word_rec z f n" by (metis (no_types, lifting) 🍋 diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq) finallyshow ?thesis . qed
lemma word_cat_eq_push_bit_or: ‹word_cat v w = (push_bit LENGTH('b) (ucast v) OR ucast w :: 'c::len word)› for v :: ‹'a::len word›and w :: ‹'b::len word› by transfer (simp add: concat_bit_def ac_simps)
end
context semiring_bit_operations begin
lemma of_nat_take_bit_numeral_eq [simp]: ‹of_nat (take_bit m (numeral n)) = take_bit m (numeral n)› by (simp add: of_nat_take_bit)
end
context ring_bit_operations begin
lemma signed_take_bit_of_int: ‹signed_take_bit n (of_int k) = of_int (signed_take_bit n k)› by (rule bit_eqI) (simp add: bit_simps)
lemma of_int_signed_take_bit: ‹of_int (signed_take_bit n k) = signed_take_bit n (of_int k)› by (simp add: signed_take_bit_of_int)
lemma of_int_take_bit_minus_numeral_eq [simp]: ‹of_int (take_bit m (numeral n)) = take_bit m (numeral n)› ‹of_int (take_bit m (- numeral n)) = take_bit m (- numeral n)› by (simp_all add: of_int_take_bit)
end
context includes bit_operations_syntax begin
lemma concat_bit_numeral_of_one_1 [simp]: ‹concat_bit (numeral m) 1 l = 1 OR push_bit (numeral m) l› by (rule bit_eqI) (auto simp add: bit_simps)
lemma concat_bit_of_one_2 [simp]: ‹concat_bit n k 1 = set_bit n (take_bit n k)› by (rule bit_eqI) (auto simp add: bit_simps)
lemma concat_bit_numeral_of_minus_one_1 [simp]: ‹concat_bit (numeral m) (- 1) l = push_bit (numeral m) l OR mask (numeral m)› by (rule bit_eqI) (auto simp add: bit_simps)
lemma concat_bit_numeral_of_minus_one_2 [simp]: ‹concat_bit (numeral m) k (- 1) = take_bit (numeral m) k OR NOT (mask (numeral m))› by (rule bit_eqI) (auto simp add: bit_simps)
lemma concat_bit_numeral [simp]: ‹concat_bit (numeral m) (numeral n) (numeral q) = take_bit (numeral m) (numeral n) OR push_bit (numeral m) (numeral q)› ‹concat_bit (numeral m) (- numeral n) (numeral q) = take_bit (numeral m) (- numeral n) OR push_bit (numeral m) (numeral q)› ‹concat_bit (numeral m) (numeral n) (- numeral q) = take_bit (numeral m) (numeral n) OR push_bit (numeral m) (- numeral q)› ‹concat_bit (numeral m) (- numeral n) (- numeral q) = take_bit (numeral m) (- numeral n) OR push_bit (numeral m) (- numeral q)› by (fact concat_bit_def)+
end
lemma word_cat_0_left [simp]: ‹word_cat 0 w = ucast w› by (simp add: word_cat_eq)
subsection‹Executable intervals›
instance word :: (len) ‹{interval_top, interval_bot}› by standard
(simp_all add: less_eq_dec_self_iff_eq inc_less_eq_self_iff_eq less_inc_imp_less_eq dec_less_imp_less_eq)
subsection‹Tool support›
ML_file ‹Tools/smt_word.ML›
end
Messung V0.5 in Prozent
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.202Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
