Theory HOL-Library.Word
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
hide_const (open) Word
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
proof
assume ?P
then show ?Q
by auto
next
assume ?Q
then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
then have "even (take_bit LENGTH('a) k)"
by simp
then show ?P
by simp
qed
show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
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 = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)›
for w :: ‹'a::len word›
by transfer (simp add: signed_take_bit_take_bit)
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
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 < take_bit 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 < take_bit 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 < take_bit 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 < b ⟷ uint a < uint 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 < take_bit 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 < take_bit LENGTH('a) l›
by transfer rule
subsection ‹Enumeration›
lemma inj_on_word_of_nat:
‹inj_on (word_of_nat :: nat ⇒ 'a::len word) {0..<2 ^ 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..<2 ^ LENGTH('a)}› (is ‹_ = ?A›)
proof
show ‹word_of_nat ` {0..<2 ^ LENGTH('a)} ⊆ UNIV›
by simp
show ‹UNIV ⊆ ?A›
proof
fix w :: ‹'a word›
show ‹w ∈ (word_of_nat ` {0..<2 ^ 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..<2 ^ 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 \<^cite>‹"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) < 2 ^ 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) < 2 ^ 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 ⟹ a < 2 ^ (LENGTH('a) - Suc 0) ⟹ P (2 * a)›
and word_odd: ‹⋀a. P a ⟹ a < 2 ^ (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 < 2 ^ LENGTH('a)›
by transfer (simp add: take_bit_eq_mod)
then have ‹n < 2 * 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 < 2 ^ m›
by simp
with even.IH have ‹P (of_nat n)›
by simp
moreover from ‹n < 2 ^ 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 < 2 ^ m› have ‹(of_nat n :: 'a word) < 2 ^ (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) < 2 ^ (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 < 2 ^ (LENGTH('a) - Suc 0)›
for a :: ‹'a::len word›
proof (cases ‹2 ≤ LENGTH('a::len)›)
case False
have ‹of_bool (odd k) < (1 :: int) ⟷ even k› for k :: int
by auto
with False that show ?thesis
by transfer (simp add: eq_iff)
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 < take_bit 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 < take_bit 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 < LENGTH('a) ∧ odd (a div 2 ^ (n - m)))› for a :: ‹'a::len word›
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 < LENGTH('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 < LENGTH('a) ∧ bit k n ⟷ n < LENGTH('a) ∧ bit l n›
proof (cases ‹n < LENGTH('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 < LENGTH('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 < LENGTH('a)› if ‹bit w n›
for w :: ‹'a::len word›
using that by transfer simp
lemma not_bit_length [simp]:
‹¬ bit w LENGTH('a)› for w :: ‹'a::len word›
by transfer simp
lemma finite_bit_word [simp]:
‹finite {n. bit w n}›
for w :: ‹'a::len word›
proof -
have ‹{n. bit w n} ⊆ {0..LENGTH('a)}›
by (auto dest: bit_imp_le_length)
moreover have ‹finite {0..LENGTH('a)}›
by simp
ultimately show ?thesis
by (rule finite_subset)
qed
lemma bit_numeral_word_iff [simp]:
‹bit (numeral w :: 'a::len word) n
⟷ n < LENGTH('a) ∧ bit (numeral w :: int) n›
by transfer simp
lemma bit_neg_numeral_word_iff [simp]:
‹bit (- numeral w :: 'a::len word) n
⟷ n < LENGTH('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
proof -
from that
have ‹take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
= take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)›
by simp
moreover have ‹min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n›
by simp
ultimately show ?thesis
by (simp add: take_bit_push_bit)
qed
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 < LENGTH('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 < LENGTH('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 < LENGTH('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 < 2 ^ 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 < b ⟷ unsigned a < unsigned 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›
apply (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
apply (cases n, simp_all add: min_def)
done
lemma signed_take_bit_eq:
‹signed (take_bit n w) = (if n < LENGTH('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 < 2 ^ (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›
proof -
have ‹int (unat (v div w)) = int (unat v div unat w)›
by (simp add: unat_div_distrib)
then show ?thesis
by (simp add: of_nat_div)
qed
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›
proof -
have ‹int (unat (v mod w)) = int (unat v mod unat w)›
by (simp add: unat_mod_distrib)
then show ?thesis
by (simp add: of_nat_mod)
qed
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)"
then have "PROP P (word_of_int (uint x))" .
then show "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 ucast_0: "ucast 0 = 0"
by (fact unsigned_0)
lemma sint_0: "sint 0 = 0"
by (fact signed_0)
lemma scast_0: "scast 0 = 0"
by (fact signed_0)
lemma sint_n1: "sint (- 1) = - 1"
by (fact signed_minus_1)
lemma scast_n1: "scast (- 1) = - 1"
by (fact signed_minus_1)
lemma uint_1: "uint (1::'a::len word) = 1"
by (fact uint_1_eq)
lemma unat_1: "unat (1::'a::len word) = 1"
by (fact unsigned_1)
lemma ucast_1: "ucast (1::'a::len word) = 1"
by (fact unsigned_1)
instantiation word :: (len) size
begin
lift_definition size_word :: ‹'a word ⇒ nat›
is ‹λ_. LENGTH('a)› ..
instance ..
end
lemma word_size [code]:
‹size w = LENGTH('a)› for w :: ‹'a::len word›
by (fact size_word.rep_eq)
lemma word_size_gt_0 [iff]: "0 < size w"
for w :: "'a::len word"
by (simp add: word_size)
lemmas lens_gt_0 = word_size_gt_0 len_gt_0
lemma lens_not_0 [iff]:
‹size w ≠ 0› for w :: ‹'a::len word›
by auto
lift_definition source_size :: ‹('a::len word ⇒ 'b) ⇒ nat›
is ‹λ_. LENGTH('a)› .
lift_definition target_size :: ‹('a ⇒ 'b::len word) ⇒ nat›
is ‹λ_. LENGTH('b)› ..
lift_definition is_up :: ‹('a::len word ⇒ 'b::len word) ⇒ bool›
is ‹λ_. LENGTH('a) ≤ LENGTH('b)› ..
lift_definition is_down :: ‹('a::len word ⇒ 'b::len word) ⇒ bool›
is ‹λ_. LENGTH('a) ≥ LENGTH('b)› ..
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 < v› for w v :: ‹'a::len word›
using that by transfer simp
lemma mod_word_less:
‹w mod v = w› if ‹w < v› 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))›
proof (cases ‹take_bit LENGTH('a) k > 1›)
case False
with take_bit_nonnegative [of ‹LENGTH('a)› k]
have ‹take_bit LENGTH('a) k = 0 ∨ take_bit LENGTH('a) k = 1›
by linarith
then show ?thesis
by auto
next
case True
then show ?thesis
by simp
qed
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›
proof (cases ‹w = - 1›)
case True
then show ?thesis
by simp
next
case False
moreover have ‹w < - 1›
using False by (simp add: word_order.not_eq_extremum)
ultimately show ?thesis
by (simp add: mod_word_less)
qed
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)
lemmas word_arith_wis =
word_add_def word_sub_wi word_mult_def
word_minus_def word_succ_alt word_pred_alt
word_0_wi word_1_wi
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)+
lemmas wi_hom_syms = wi_homs [symmetric]
lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
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›
then have *: ‹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 *)
moreover have ‹2 ^ LENGTH('a) = (0 :: 'a word)›
by transfer simp
then have ‹2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)›
by (simp add: *)
ultimately show ?thesis
by auto
qed
subsection ‹Ordering›
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 < signed_take_bit (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 (‹'(<s')›) and
word_sless (‹(‹notation=‹infix <s››_/ <s _)› [51, 51] 50)
notation (input)
word_sle (‹(‹notation=‹infix <=s››_/ <=s _)› [51, 51] 50)
lemma word_sle_eq [code]:
‹a <=s b ⟷ sint a ≤ sint b›
by transfer simp
lemma [code]:
‹a <s b ⟷ sint a < sint b›
by transfer simp
lemma signed_ordering: ‹ordering word_sle word_sless›
apply (standard; transfer)
using signed_take_bit_decr_length_iff by force+
lemma signed_linorder: ‹class.linorder word_sle word_sless›
by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff)