# Theory HOL-Library.Word

```(*  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 (cases ‹LENGTH('a)›)

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 ‹(+)›

lift_definition minus_word :: ‹'a word ⇒ 'a word ⇒ 'a word›
is ‹(-)›
by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)

lift_definition uminus_word :: ‹'a word ⇒ 'a word›
is uminus
by (auto simp add: take_bit_eq_mod intro: mod_minus_cong)

lift_definition times_word :: ‹'a word ⇒ 'a word ⇒ 'a word›
is ‹(*)›
by (auto simp add: 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)›

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›

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 add: 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›

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›

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›

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))›

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›

lemma nat_uint_eq [simp]:
‹nat (uint w) = unat w›
by transfer simp

lemma sgn_uint_eq [simp]:
‹sgn (uint w) = of_bool (w ≠ 0)›

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)›

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›

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›

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›

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›

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›

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›

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
have "k mod r = ((k mod r) div (l mod r) * (l mod r)
+ (k mod r) mod (l mod r)) mod r"
also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+ (k mod r) mod (l mod r)) mod r"
also have "... = (((k mod r) div (l mod r) * l) mod r
+ (k mod r) mod (l mod r)) mod r"
finally have "k mod r = ((k mod r) div (l mod r) * l
+ (k mod r) mod (l mod r)) mod r"
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

instance word :: (len) semiring_parity
proof
show "¬ 2 dvd (1::'a word)"
by transfer simp
show even_iff_mod_2_eq_0: "2 dvd a ⟷ a mod 2 = 0"
for a :: "'a word"
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
show "¬ 2 dvd a ⟷ a mod 2 = 1"
for a :: "'a word"
by transfer (simp_all add: mod_2_eq_odd take_bit_Suc)
qed

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)›
then have ‹n < 2 * 2 ^ m›
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 add: 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›]
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›]
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
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
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›
ultimately have ‹take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2›
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›
ultimately have ‹take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2›
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›
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,

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
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 ‹0 div a = 0›
for a :: ‹'a word›
by transfer simp
show ‹a div 1 = a›
for a :: ‹'a word›
by transfer simp
show ‹a mod b div b = 0›
for a b :: ‹'a word›
apply transfer
apply (smt (verit, best) Euclidean_Rings.pos_mod_bound Euclidean_Rings.pos_mod_sign div_int_pos_iff
nonneg1_imp_zdiv_pos_iff zero_less_power zmod_le_nonneg_dividend)
done
show ‹(1 + a) div 2 = a div 2›
if ‹even a›
for a :: ‹'a word›
using that by transfer
(auto dest: le_Suc_ex simp add: take_bit_Suc elim!: evenE)
show ‹(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m ≠ 0 ∧ n ≤ m) * 2 ^ (m - n)›
for m n :: nat
by transfer (simp, simp add: exp_div_exp_eq)
show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)"
for a :: "'a word" and m n :: nat
apply transfer
apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div)
done
show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n"
for a :: "'a word" and m n :: nat
by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps)
show ‹a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m›
if ‹m ≤ n› for a :: "'a word" and m n :: nat
using that apply transfer
apply (auto simp flip: take_bit_eq_mod)
apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin)
done
show ‹a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n›
for a :: "'a word" and m n :: nat
by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin)
show ‹even ((2 ^ m - 1) div (2::'a word) ^ n) ⟷ 2 ^ n = (0::'a word) ∨ m ≤ n›
for m n :: nat
by transfer
show ‹even (a * 2 ^ m div 2 ^ n) ⟷ n < m ∨ (2::'a word) ^ n = 0 ∨ m ≤ n ∧ even (a div 2 ^ (n - m))›
for a :: ‹'a word› and m n :: nat
proof transfer
show ‹even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) ⟷
n < m
∨ take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0
∨ (m ≤ n ∧ even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))›
for m n :: nat and k l :: int
by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult
simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m])
qed
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 add: 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

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›
.

lift_definition set_bit_word :: ‹nat ⇒ 'a word ⇒ 'a word›
is set_bit

lift_definition unset_bit_word :: ‹nat ⇒ 'a word ⇒ 'a word›
is unset_bit

lift_definition flip_bit_word :: ‹nat ⇒ 'a word ⇒ 'a word›
is flip_bit

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
qed
qed

lift_definition drop_bit_word :: ‹nat ⇒ 'a word ⇒ 'a word›
is ‹λn. drop_bit n ∘ take_bit LENGTH('a)›

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)

instance apply (standard; transfer)
bit_simps set_bit_def flip_bit_def take_bit_drop_bit
simp flip: drop_bit_eq_div take_bit_eq_mod)
apply (simp_all add: drop_bit_take_bit flip: push_bit_eq_mult)
done

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›

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]:
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›
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)›

context semiring_bit_operations
begin

‹unsigned (- 1 :: 'b::len word) = mask LENGTH('b)›

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)›
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 unique_euclidean_semiring_with_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 add: 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 add: 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›

lemma unsigned_or_eq:
‹unsigned (v OR w) = unsigned v OR unsigned w›
for v w :: ‹'b::len word›

lemma unsigned_xor_eq:
‹unsigned (v XOR w) = unsigned v XOR unsigned w›
for v w :: ‹'b::len word›

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›

end

end

context unique_euclidean_semiring_numeral
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 add: 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 add: 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
next
have *: ‹- (2 ^ (LENGTH('a) - Suc 0)) ≤ (0::int)›
by simp
case False
then show ?thesis
by transfer (auto simp add: 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)

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)›
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)›
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

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)›
then show ?thesis
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)›
then show ?thesis
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"

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)"

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"

lemma unat_0_iff: "unat x = 0 ⟷ x = 0"

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"

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›
apply (cases ‹w = 0›)
apply auto
using div_mult_mod_eq [of w w] by (simp add: div_word_self)

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
qed

text ‹Legacy theorems:›

"a + b = word_of_int (uint a + uint b)"

lemma word_sub_wi [code]:
"a - b = word_of_int (uint a - uint b)"

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)"

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"

lift_definition word_pred :: "'a::len word ⇒ 'a word" is "λx. x - 1"
by (auto simp add: 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_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 add: 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)›
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    ("(_/ ≤s _)"  [51, 51] 50) and
word_sless  ("'(<s')") and
word_sless  ("(_/ <s _)"  [51, 51] 50)

notation (input)
word_sle    ("(_/ <=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 add: signed_take_bit_decr_length_iff)

```