Quelle  Word.thy   Sprache: Isabelle

(*  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 ‹(*)\<close>
  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 < 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

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..<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 🍋‹"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
  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 < 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›
  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 < 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
    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 < 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\
  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 < 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›
  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)"
  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))\
    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)

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›

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)" ..
  moreover have "{(a, b :: ('a::len) word). a < b} \ measure unat"
    by (auto simp add: word_less_iff_unsigned [where ?'a = nat])
  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
    by (rule wf_subset)
  then show "P a" using *
    by induction 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)

lemmas word_not_simps [simp] =
  word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]

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) < numeral 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 < 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  (‹'()›) 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 word_sless_alt [code]:
  "a sint a < sint b"
  by transfer simp

lemma signed_ordering: ‹ordering word_sle word_sless›
  by (standard; transfer) (auto simp flip: signed_take_bit_decr_length_iff)

lemma signed_linorder: ‹class.linorder word_sle word_sless›
  by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff)

interpretation signed: linorder word_sle word_sless
  by (fact signed_linorder)

lemma word_sless_eq:
  ‹x <s y ⟷ x <=s y ∧ x ≠ y›
  by (fact signed.less_le)

lemma minus_1_sless_0 [simp]:
  ‹- 1 <s 0›
  by transfer simp

lemma not_0_sless_minus_1 [simp]:
  ‹¬ 0 <s - 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 < LENGTH('a) ∧ bit k n›
  by (simp add: bit_simps)

lemma bit_uint_iff:
  ‹bit (uint w) n ⟷ n < LENGTH('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 < LENGTH('a) ∧ n < LENGTH('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 < LENGTH('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..<n] = map (bit l) [0..<n]›
  if ‹take_bit n k = take_bit n l› for k l :: int
  using that 
proof (induction n arbitrary: k l)
  case 0
  then show ?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)
  then have ‹map (bit (k div 2)) [0..<n] = map (bit (l div 2)) [0..<n]›
    by (rule Suc.IH)
  moreover have ‹bit (r div 2) = bit r ∘ Suc› for r :: int
    by (simp add: fun_eq_iff bit_Suc)
  moreover from Suc.prems have ‹even k ⟷ even l›
    by (metis Zero_neq_Suc even_take_bit_eq)
  ultimately show ?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)› (is ?P)
  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)› (is ?Q)
  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)› (is ?R)
  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))› (is ?S)
proof -
  define w :: ‹'a::len word\
    where ‹w = numeral m›
  moreover define q :: nat
    where ‹q = pred_numeral n›
  ultimately have num:
    ‹numeral m = w›
    ‹numeral (num.Bit0 m) = 2 * w›
    ‹numeral (num.Bit1 m) = 1 + 2 * w›
    ‹numeral (Num.inc m) = 1 + w›
--> --------------------

--> maximum size reached

--> --------------------