Theory 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))
    (simp_all 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 add: take_bit_eq_mod intro: mod_add_cong)

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)
  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 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
  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 sgn_uint_eq [simp]:
  sgn (uint w) = of_bool (w  0)
  by transfer (simp add: less_le)

text Aliasses only for code generation

context
begin

qualified lift_definition of_int :: int  'a::len word
  is take_bit LENGTH('a) .

qualified lift_definition of_nat :: nat  'a::len word
  is int  take_bit LENGTH('a) .

qualified lift_definition the_nat :: 'a::len word  nat
  is nat  take_bit LENGTH('a) by simp

qualified lift_definition the_signed_int :: 'a::len word  int
  is signed_take_bit (LENGTH('a) - Suc 0) by (simp add: signed_take_bit_decr_length_iff)

qualified lift_definition cast :: 'a::len word  'b::len word
  is take_bit LENGTH('a) by simp

qualified lift_definition signed_cast :: 'a::len word  'b::len word
  is signed_take_bit (LENGTH('a) - Suc 0) by (metis signed_take_bit_decr_length_iff)

end

lemma [code_abbrev, simp]:
  Word.the_int = uint
  by transfer rule

lemma [code]:
  Word.the_int (Word.of_int k :: 'a::len word) = take_bit LENGTH('a) k
  by transfer simp

lemma [code_abbrev, simp]:
  Word.of_int = word_of_int
  by (rule; transfer) simp

lemma [code]:
  Word.the_int (Word.of_nat n :: 'a::len word) = take_bit LENGTH('a) (int n)
  by transfer (simp add: take_bit_of_nat)

lemma [code_abbrev, simp]:
  Word.of_nat = word_of_nat
  by (rule; transfer) (simp add: take_bit_of_nat)

lemma [code]:
  Word.the_nat w = nat (Word.the_int w)
  by transfer simp

lemma [code_abbrev, simp]:
  Word.the_nat = unat
  by (rule; transfer) simp

lemma [code]:
  Word.the_signed_int w = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)
  for w :: 'a::len word
  by transfer (simp add: signed_take_bit_take_bit)

lemma [code_abbrev, simp]:
  Word.the_signed_int = sint
  by (rule; transfer) simp

lemma [code]:
  Word.the_int (Word.cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_int w)
  for w :: 'a::len word
  by transfer simp

lemma [code_abbrev, simp]:
  Word.cast = ucast
  by (rule; transfer) simp

lemma [code]:
  Word.the_int (Word.signed_cast w :: 'b::len word) = take_bit LENGTH('b) (Word.the_signed_int w)
  for w :: 'a::len word
  by transfer simp

lemma [code_abbrev, simp]:
  Word.signed_cast = scast
  by (rule; transfer) simp

lemma [code]:
  unsigned w = of_nat (nat (Word.the_int w))
  by transfer simp

lemma [code]:
  signed w = of_int (Word.the_signed_int w)
  by transfer simp


subsubsection Basic ordering

instantiation word :: (len) linorder
begin

lift_definition less_eq_word :: "'a word  'a word  bool"
  is "λa b. take_bit LENGTH('a) a  take_bit LENGTH('a) b"
  by simp

lift_definition less_word :: "'a word  'a word  bool"
  is "λa b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
  by simp

instance
  by (standard; transfer) auto

end

interpretation word_order: ordering_top (≤) (<) - 1 :: 'a::len word
  by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1)

interpretation word_coorder: ordering_top (≥) (>) 0 :: 'a::len word
  by (standard; transfer) simp

lemma word_of_nat_less_eq_iff:
  word_of_nat m  (word_of_nat n :: 'a::len word)  take_bit LENGTH('a) m  take_bit LENGTH('a) n
  by transfer (simp add: take_bit_of_nat)

lemma word_of_int_less_eq_iff:
  word_of_int k  (word_of_int l :: 'a::len word)  take_bit LENGTH('a) k  take_bit LENGTH('a) l
  by transfer rule

lemma word_of_nat_less_iff:
  word_of_nat m < (word_of_nat n :: 'a::len word)  take_bit LENGTH('a) m < take_bit LENGTH('a) n
  by transfer (simp add: take_bit_of_nat)

lemma word_of_int_less_iff:
  word_of_int k < (word_of_int l :: 'a::len word)  take_bit LENGTH('a) k < take_bit LENGTH('a) l
  by transfer rule

lemma word_le_def [code]:
  "a  b  uint a  uint b"
  by transfer rule

lemma word_less_def [code]:
  "a < b  uint a < uint b"
  by transfer rule

lemma word_greater_zero_iff:
  a > 0  a  0 for a :: 'a::len word
  by transfer (simp add: less_le)

lemma of_nat_word_less_eq_iff:
  of_nat m  (of_nat n :: 'a::len word)  take_bit LENGTH('a) m  take_bit LENGTH('a) n
  by transfer (simp add: take_bit_of_nat)

lemma of_nat_word_less_iff:
  of_nat m < (of_nat n :: 'a::len word)  take_bit LENGTH('a) m < take_bit LENGTH('a) n
  by transfer (simp add: take_bit_of_nat)

lemma of_int_word_less_eq_iff:
  of_int k  (of_int l :: 'a::len word)  take_bit LENGTH('a) k  take_bit LENGTH('a) l
  by transfer rule

lemma of_int_word_less_iff:
  of_int k < (of_int l :: 'a::len word)  take_bit LENGTH('a) k < take_bit LENGTH('a) l
  by transfer rule



subsection Enumeration

lemma inj_on_word_of_nat:
  inj_on (word_of_nat :: nat  'a::len word) {0..<2 ^ LENGTH('a)}
  by (rule inj_onI; transfer) (simp_all add: take_bit_int_eq_self)

lemma UNIV_word_eq_word_of_nat:
  (UNIV :: 'a::len word set) = word_of_nat ` {0..<2 ^ LENGTH('a)} (is _ = ?A)
proof
  show word_of_nat ` {0..<2 ^ LENGTH('a)}  UNIV
    by simp
  show UNIV  ?A
  proof
    fix w :: 'a word
    show w  (word_of_nat ` {0..<2 ^ LENGTH('a)} :: 'a word set)
      by (rule image_eqI [of _ _ unat w]; transfer) simp_all
  qed
qed

instantiation word :: (len) enum
begin

definition enum_word :: 'a word list
  where enum_word = map word_of_nat [0..<2 ^ LENGTH('a)]

definition enum_all_word :: ('a word  bool)  bool
  where enum_all_word = Ball UNIV

definition enum_ex_word :: ('a word  bool)  bool
  where enum_ex_word = Bex UNIV

lemma [code]:
  Enum.enum_all P  Ball UNIV P
  Enum.enum_ex P  Bex UNIV P for P :: 'a word  bool
  by (simp_all add: enum_all_word_def enum_ex_word_def)

instance
  by standard (simp_all add: UNIV_word_eq_word_of_nat inj_on_word_of_nat enum_word_def enum_all_word_def enum_ex_word_def distinct_map)

end


subsection Bit-wise operations

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

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)
    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 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]
      by (simp add: l take_bit_eq_mod)
    ultimately have P (2 * of_nat n)
      by (rule word_even)
    then show ?case
      by simp
  next
    case (odd n)
    then have Suc n  2 ^ m
      by simp
    with odd.IH have P (of_nat n)
      by simp
    moreover from Suc n  2 ^ m have (of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)
      using of_nat_word_less_iff [where ?'a = 'a, of n 2 ^ m]
      by (simp add: l take_bit_eq_mod)
    ultimately have P (1 + 2 * of_nat n)
      by (rule word_odd)
    then show ?case
      by simp
  qed
  moreover have of_nat (nat (uint a)) = a
    by transfer simp
  ultimately show ?thesis
    by (simp add: n_def)
qed

lemma bit_word_half_eq:
  (of_bool b + a * 2) div 2 = a
    if a < 2 ^ (LENGTH('a) - Suc 0)
    for a :: 'a::len word
proof (cases 2  LENGTH('a::len))
  case False
  have of_bool (odd k) < (1 :: int)  even k for k :: int
    by auto
  with False that show ?thesis
    by transfer (simp add: eq_iff)
next
  case True
  obtain n where length: LENGTH('a) = Suc n
    by (cases LENGTH('a)) simp_all
  show ?thesis proof (cases b)
    case False
    moreover have a * 2 div 2 = a
    using that proof transfer
      fix k :: int
      from length have k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2
        by simp
      moreover assume take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))
      with LENGTH('a) = Suc n
      have k mod 2 ^ LENGTH('a) = k mod 2 ^ n
        by (simp add: take_bit_eq_mod divmod_digit_0)
      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 k mod 2 ^ LENGTH('a) = k mod 2 ^ n
        by (simp add: take_bit_eq_mod divmod_digit_0)
      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 add: 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 0 div a = 0
    for a :: 'a word
    by transfer simp
  show a div 1 = a
    for a :: 'a word
    by transfer simp
  have §: "i n. (i::int) mod 2 ^ n = 0  0 < i mod 2 ^ n"
    by (metis le_less take_bit_eq_mod take_bit_nonnegative)
  have less_power: "n i p. (i::int) mod numeral p ^ n < numeral p ^ n"
    by simp
  show a mod b div b = 0
    for a b :: 'a word
    apply transfer
    apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def)
    by (metis (no_types, opaque_lifting) "§" Euclidean_Division.pos_mod_bound Euclidean_Division.pos_mod_sign le_less_trans mult_eq_0_iff take_bit_eq_mod take_bit_nonnegative zdiv_eq_0_iff zmod_le_nonneg_dividend)
  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)
    apply (simp add: drop_bit_take_bit)
    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
      (simp flip: drop_bit_eq_div mask_eq_exp_minus_1 add: bit_simps even_drop_bit_iff_not_bit not_less)
  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
  by (simp add: take_bit_not_iff)

lift_definition and_word :: 'a word  'a word  'a word
  is and
  by simp

lift_definition or_word :: 'a word  'a word  'a word
  is or
  by simp

lift_definition xor_word ::  'a word  'a word  'a word
  is xor
  by simp

lift_definition mask_word :: nat  'a word
  is mask
  .

lift_definition set_bit_word :: nat  'a word  'a word
  is set_bit
  by (simp add: set_bit_def)

lift_definition unset_bit_word :: nat  'a word  'a word
  is unset_bit
  by (simp add: unset_bit_def)

lift_definition flip_bit_word :: nat  'a word  'a word
  is flip_bit
  by (simp add: flip_bit_def)

lift_definition push_bit_word :: nat  'a word  'a word
  is push_bit
proof -
  show take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)
    if take_bit LENGTH('a) k = take_bit LENGTH('a) l for k l :: int and n :: nat
  proof -
    from that
    have take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)
      by simp
    moreover have min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n
      by simp
    ultimately show ?thesis
      by (simp add: take_bit_push_bit)
  qed
qed

lift_definition drop_bit_word :: nat  'a word  'a word
  is λn. drop_bit n  take_bit LENGTH('a)
  by (simp add: take_bit_eq_mod)

lift_definition take_bit_word :: nat  'a word  'a word
  is λn. take_bit (min LENGTH('a) n)
  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)

instance apply (standard; transfer)
  apply (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
    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
  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 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
  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 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
    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 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)
    (simp_all add: signed_take_bit_eq signed_take_bit_def not_eq_complement mask_eq_exp_minus_1 OR_upper)

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

lemma uint_div_distrib:
  uint (v div w) = uint v div uint w
proof -
  have int (unat (v div w)) = int (unat v div unat w)
    by (simp add: unat_div_distrib)
  then show ?thesis
    by (simp add: of_nat_div)
qed

lemma unat_drop_bit_eq:
  unat (drop_bit n w) = drop_bit n (unat w)
  by (rule bit_eqI) (simp add: bit_unsigned_iff bit_drop_bit_eq)

lemma uint_mod_distrib:
  uint (v mod w) = uint v mod uint w
proof -
  have int (unat (v mod w)) = int (unat v mod unat w)
    by (simp add: unat_mod_distrib)
  then show ?thesis
    by (simp add: of_nat_mod)
qed

context semiring_bit_operations
begin

lemma unsigned_ucast_eq:
  unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)
  for w :: 'b::len word
  by (rule bit_eqI) (simp add: bit_unsigned_iff Word.bit_unsigned_iff bit_take_bit_iff not_le)

end

context ring_bit_operations
begin

lemma signed_ucast_eq:
  signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)
  for w :: 'b::len word
  by (simp add: bit_eq_iff bit_simps min_less_iff_disj)

lemma signed_scast_eq:
  signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)
  for w :: 'b::len word
  by (simp add: bit_eq_iff bit_simps min_less_iff_disj)

end

lemma uint_nonnegative: "0  uint w"
  by (fact unsigned_greater_eq)

lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
  for w :: "'a::len word"
  by (fact unsigned_less)

lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
  for w :: "'a::len word"
  by transfer (simp add: take_bit_eq_mod)

lemma word_uint_eqI: "uint a = uint b  a = b"
  by (fact unsigned_word_eqI)

lemma word_uint_eq_iff: "a = b  uint a = uint b"
  by (fact word_eq_iff_unsigned)

lemma uint_word_of_int_eq:
  uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k
  by transfer rule

lemma uint_word_of_int: "uint (word_of_int k :: 'a::len word) = k mod 2 ^ LENGTH('a)"
  by (simp add: uint_word_of_int_eq take_bit_eq_mod)
  
lemma word_of_int_uint: "word_of_int (uint w) = w"
  by transfer simp

lemma word_div_def [code]:
  "a div b = word_of_int (uint a div uint b)"
  by transfer rule

lemma word_mod_def [code]:
  "a mod b = word_of_int (uint a mod uint b)"
  by transfer rule

lemma split_word_all: "(x::'a::len word. PROP P x)  (x. PROP P (word_of_int x))"
proof
  fix x :: "'a word"
  assume "x. PROP P (word_of_int x)"
  then have "PROP P (word_of_int (uint x))" .
  then show "PROP P x"
    by (simp only: word_of_int_uint)
qed

lemma sint_uint:
  sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)
  for w :: 'a::len word
  by (cases LENGTH('a); transfer) (simp_all add: signed_take_bit_take_bit)

lemma unat_eq_nat_uint:
  unat w = nat (uint w)
  by simp

lemma ucast_eq:
  ucast w = word_of_int (uint w)
  by transfer simp

lemma scast_eq:
  scast w = word_of_int (sint w)
  by transfer simp

lemma uint_0_eq:
  uint 0 = 0
  by (fact unsigned_0)

lemma uint_1_eq:
  uint 1 = 1
  by (fact unsigned_1)

lemma word_m1_wi: "- 1 = word_of_int (- 1)"
  by simp

lemma uint_0_iff: "uint x = 0  x = 0"
  by (auto simp add: unsigned_word_eqI)

lemma unat_0_iff: "unat x = 0  x = 0"
  by (auto simp add: 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
  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 simp

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
  apply (cases w = - 1)
   apply (auto simp add: word_order.not_eq_extremum)
  using div_mult_mod_eq [of w - 1] by simp

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 add: take_bit_eq_mod intro: mod_add_cong)

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_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 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)
    by (simp add: *)
  ultimately show ?thesis
    by auto
qed


subsection Ordering

lift_definition word_sle :: 'a::len word  'a word  bool
  is λk l. signed_take_bit (LENGTH('a) - Suc 0) k  signed_take_bit (LENGTH('a) - Suc 0) l
  by (simp flip: signed_take_bit_decr_length_iff)

lift_definition word_sless :: 'a::len word  'a word  bool
  is λk l. signed_take_bit (LENGTH('a) - Suc 0) k < signed_take_bit (LENGTH('a) - Suc 0) l
  by (simp flip: signed_take_bit_decr_length_iff)

notation
  word_sle    ("'(≤s')") and
  word_sle    ("(_/ ≤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)

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 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_m1_ge [simp] : "word_pred 0  y" (* FIXME: delete *)
  by transfer (simp add: mask_eq_exp_minus_1)

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 [