Quelle Word.thy Sprache: Isabelle

(*  Title:      HOL/Library/Word.thy
    Author:     Jeremy Dawson and Gerwin Klein, NICTA, et. al.
*)

section \<open>A type of finite bit strings\<close>

theory Word
imports
  "HOL-Library.Type_Length"
begin

subsection \<open>Preliminaries\<close>

lemma signed_take_bit_decr_length_iff:
  \<open>signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l
    \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
  by (simp add: signed_take_bit_eq_iff_take_bit_eq)

subsection \<open>Fundamentals\<close>

subsubsection \<open>Type definition\<close>

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 \<comment> \<open>only for foundational purpose\<close>
hide_const (open) Word \<comment> \<open>only for code generation\<close>

subsubsection \<open>Basic arithmetic\<close>

instantiation word :: (len) comm_ring_1
begin

lift_definition zero_word :: \<open>'a word\<close>
  is 0 .

lift_definition one_word :: \<open>'a word\<close>
  is 1 .

lift_definition plus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>(+)\<close>
  by (auto simp: take_bit_eq_mod intro: mod_add_cong)

lift_definition minus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>(-)\<close>
  by (auto simp: take_bit_eq_mod intro: mod_diff_cong)

lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close>
  is uminus
  by (auto simp: take_bit_eq_mod intro: mod_minus_cong)

lift_definition times_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>(*)\<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]:
  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
  by transfer_prover

lemma [transfer_rule]:
  \<open>((=) ===> pcr_word) of_bool of_bool\<close>
  by transfer_prover

lemma [transfer_rule]:
  \<open>((=) ===> pcr_word) numeral numeral\<close>
  by transfer_prover

lemma [transfer_rule]:
  \<open>((=) ===> pcr_word) int of_nat\<close>
  by transfer_prover

lemma [transfer_rule]:
  \<open>((=) ===> pcr_word) (\<lambda>k. k) of_int\<close>
proof -
  have \<open>((=) ===> pcr_word) of_int of_int\<close>
    by transfer_prover
  then show ?thesis by (simp add: id_def)
qed

lemma [transfer_rule]:
  \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close>
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]:
  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
  by transfer auto

lemma word_exp_length_eq_0 [simp]:
  \<open>(2 :: 'a::len word) ^ LENGTH('a) = 0\<close>
  by simp

subsubsection \<open>Basic tool setup\<close>

ML_file \<open>Tools/word_lib.ML\<close>

subsubsection \<open>Basic code generation setup\<close>

context
begin

qualified lift_definition the_int :: \<open>'a::len word \<Rightarrow> int\<close>
  is \<open>take_bit LENGTH('a)\<close> .

end

lemma [code abstype]:
  \<open>Word.Word (Word.the_int w) = w\<close>
  by transfer simp

lemma Word_eq_word_of_int [code_post, simp]:
  \<open>Word.Word = of_int\<close>
  by (rule; transfer) simp

quickcheck_generator word
  constructors:
    \<open>0 :: 'a::len word\<close>,
    \<open>numeral :: num \<Rightarrow> 'a::len word\<close>

instantiation word :: (len) equal
begin

lift_definition equal_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
  is \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
  by simp

instance
  by (standard; transfer) rule

end

lemma [code]:
  \<open>HOL.equal v w \<longleftrightarrow> HOL.equal (Word.the_int v) (Word.the_int w)\<close>
  by transfer (simp add: equal)

lemma [code]:
  \<open>Word.the_int 0 = 0\<close>
  by transfer simp

lemma [code]:
  \<open>Word.the_int 1 = 1\<close>
  by transfer simp

lemma [code]:
  \<open>Word.the_int (v + w) = take_bit LENGTH('a) (Word.the_int v + Word.the_int w)\<close>
  for v w :: \<open>'a::len word\<close>
  by transfer (simp add: take_bit_add)

lemma [code]:
  \<open>Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (auto simp: take_bit_eq_mod zmod_zminus1_eq_if)

lemma [code]:
  \<open>Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\<close>
  for v w :: \<open>'a::len word\<close>
  by transfer (simp add: take_bit_diff)

lemma [code]:
  \<open>Word.the_int (v * w) = take_bit LENGTH('a) (Word.the_int v * Word.the_int w)\<close>
  for v w :: \<open>'a::len word\<close>
  by transfer (simp add: take_bit_mult)

subsubsection \<open>Basic conversions\<close>

abbreviation word_of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
  where \<open>word_of_nat \<equiv> of_nat\<close>

abbreviation word_of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
  where \<open>word_of_int \<equiv> of_int\<close>

lemma word_of_nat_eq_iff:
  \<open>word_of_nat m = (word_of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
  by transfer (simp add: take_bit_of_nat)

lemma word_of_int_eq_iff:
  \<open>word_of_int k = (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
  by transfer rule

lemma word_of_nat_eq_0_iff:
  \<open>word_of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close>
  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:
  \<open>word_of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close>
  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 :: \<open>'b::len word \<Rightarrow> 'a\<close>
  is \<open>of_nat \<circ> nat \<circ> take_bit LENGTH('b)\<close>
  by simp

lemma unsigned_0 [simp]:
  \<open>unsigned 0 = 0\<close>
  by transfer simp

lemma unsigned_1 [simp]:
  \<open>unsigned 1 = 1\<close>
  by transfer simp

lemma unsigned_numeral [simp]:
  \<open>unsigned (numeral n :: 'b::len word) = of_nat (take_bit LENGTH('b) (numeral n))\<close>
  by transfer (simp add: nat_take_bit_eq)

lemma unsigned_neg_numeral [simp]:
  \<open>unsigned (- numeral n :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) (- numeral n)))\<close>
  by transfer simp

end

context semiring_1
begin

lemma unsigned_of_nat:
  \<open>unsigned (word_of_nat n :: 'b::len word) = of_nat (take_bit LENGTH('b) n)\<close>
  by transfer (simp add: nat_eq_iff take_bit_of_nat)

lemma unsigned_of_int:
  \<open>unsigned (word_of_int k :: 'b::len word) = of_nat (nat (take_bit LENGTH('b) k))\<close>
  by transfer simp

end

context semiring_char_0
begin

lemma unsigned_word_eqI:
  \<open>v = w\<close> if \<open>unsigned v = unsigned w\<close>
  using that by transfer (simp add: eq_nat_nat_iff)

lemma word_eq_iff_unsigned:
  \<open>v = w \<longleftrightarrow> unsigned v = unsigned w\<close>
  by (auto intro: unsigned_word_eqI)

lemma inj_unsigned [simp]:
  \<open>inj unsigned\<close>
  by (rule injI) (simp add: unsigned_word_eqI)

lemma unsigned_eq_0_iff:
  \<open>unsigned w = 0 \<longleftrightarrow> w = 0\<close>
  using word_eq_iff_unsigned [of w 0] by simp

end

context ring_1
begin

lift_definition signed :: \<open>'b::len word \<Rightarrow> 'a\<close>
  is \<open>of_int \<circ> signed_take_bit (LENGTH('b) - Suc 0)\<close>
  by (simp flip: signed_take_bit_decr_length_iff)

lemma signed_0 [simp]:
  \<open>signed 0 = 0\<close>
  by transfer simp

lemma signed_1 [simp]:
  \<open>signed (1 :: 'b::len word) = (if LENGTH('b) = 1 then - 1 else 1)\<close>
  by (transfer fixing: uminus; cases \<open>LENGTH('b)\<close>) (auto dest: gr0_implies_Suc)

lemma signed_minus_1 [simp]:
  \<open>signed (- 1 :: 'b::len word) = - 1\<close>
  by (transfer fixing: uminus) simp

lemma signed_numeral [simp]:
  \<open>signed (numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (numeral n))\<close>
  by transfer simp

lemma signed_neg_numeral [simp]:
  \<open>signed (- numeral n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - 1) (- numeral n))\<close>
  by transfer simp

lemma signed_of_nat:
  \<open>signed (word_of_nat n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) (int n))\<close>
  by transfer simp

lemma signed_of_int:
  \<open>signed (word_of_int n :: 'b::len word) = of_int (signed_take_bit (LENGTH('b) - Suc 0) n)\<close>
  by transfer simp

end

context ring_char_0
begin

lemma signed_word_eqI:
  \<open>v = w\<close> if \<open>signed v = signed w\<close>
  using that by transfer (simp flip: signed_take_bit_decr_length_iff)

lemma word_eq_iff_signed:
  \<open>v = w \<longleftrightarrow> signed v = signed w\<close>
  by (auto intro: signed_word_eqI)

lemma inj_signed [simp]:
  \<open>inj signed\<close>
  by (rule injI) (simp add: signed_word_eqI)

lemma signed_eq_0_iff:
  \<open>signed w = 0 \<longleftrightarrow> w = 0\<close>
  using word_eq_iff_signed [of w 0] by simp

end

abbreviation unat :: \<open>'a::len word \<Rightarrow> nat\<close>
  where \<open>unat \<equiv> unsigned\<close>

abbreviation uint :: \<open>'a::len word \<Rightarrow> int\<close>
  where \<open>uint \<equiv> unsigned\<close>

abbreviation sint :: \<open>'a::len word \<Rightarrow> int\<close>
  where \<open>sint \<equiv> signed\<close>

abbreviation ucast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  where \<open>ucast \<equiv> unsigned\<close>

abbreviation scast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  where \<open>scast \<equiv> signed\<close>

context
  includes lifting_syntax
begin

lemma [transfer_rule]:
  \<open>(pcr_word ===> (=)) (nat \<circ> take_bit LENGTH('a)) (unat :: 'a::len word \<Rightarrow> nat)\<close>
  using unsigned.transfer [where ?'a = nat] by simp

lemma [transfer_rule]:
  \<open>(pcr_word ===> (=)) (take_bit LENGTH('a)) (uint :: 'a::len word \<Rightarrow> int)\<close>
  using unsigned.transfer [where ?'a = int] by (simp add: comp_def)

lemma [transfer_rule]:
  \<open>(pcr_word ===> (=)) (signed_take_bit (LENGTH('a) - Suc 0)) (sint :: 'a::len word \<Rightarrow> int)\<close>
  using signed.transfer [where ?'a = int] by simp

lemma [transfer_rule]:
  \<open>(pcr_word ===> pcr_word) (take_bit LENGTH('a)) (ucast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
proof (rule rel_funI)
  fix k :: int and w :: \<open>'a word\<close>
  assume \<open>pcr_word k w\<close>
  then have \<open>w = word_of_int k\<close>
    by (simp add: pcr_word_def cr_word_def relcompp_apply)
  moreover have \<open>pcr_word (take_bit LENGTH('a) k) (ucast (word_of_int k :: 'a word))\<close>
    by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
  ultimately show \<open>pcr_word (take_bit LENGTH('a) k) (ucast w)\<close>
    by simp
qed

lemma [transfer_rule]:
  \<open>(pcr_word ===> pcr_word) (signed_take_bit (LENGTH('a) - Suc 0)) (scast :: 'a::len word \<Rightarrow> 'b::len word)\<close>
proof (rule rel_funI)
  fix k :: int and w :: \<open>'a word\<close>
  assume \<open>pcr_word k w\<close>
  then have \<open>w = word_of_int k\<close>
    by (simp add: pcr_word_def cr_word_def relcompp_apply)
  moreover have \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast (word_of_int k :: 'a word))\<close>
    by transfer (simp add: pcr_word_def cr_word_def relcompp_apply)
  ultimately show \<open>pcr_word (signed_take_bit (LENGTH('a) - Suc 0) k) (scast w)\<close>
    by simp
qed

end

lemma of_nat_unat [simp]:
  \<open>of_nat (unat w) = unsigned w\<close>
  by transfer simp

lemma of_int_uint [simp]:
  \<open>of_int (uint w) = unsigned w\<close>
  by transfer simp

lemma of_int_sint [simp]:
  \<open>of_int (sint a) = signed a\<close>
  by transfer (simp_all add: take_bit_signed_take_bit)

lemma nat_uint_eq [simp]:
  \<open>nat (uint w) = unat w\<close>
  by transfer simp

lemma nat_of_natural_unsigned_eq [simp]:
  \<open>nat_of_natural (unsigned w) = unat w\<close>
  by transfer simp

lemma int_of_integer_unsigned_eq [simp]:
  \<open>int_of_integer (unsigned w) = uint w\<close>
  by transfer simp

lemma int_of_integer_signed_eq [simp]:
  \<open>int_of_integer (signed w) = sint w\<close>
  by transfer simp

lemma sgn_uint_eq [simp]:
  \<open>sgn (uint w) = of_bool (w \<noteq> 0)\<close>
  by transfer (simp add: less_le)

text \<open>Aliasses only for code generation\<close>

context
begin

qualified lift_definition of_int :: \<open>int \<Rightarrow> 'a::len word\<close>
  is \<open>take_bit LENGTH('a)\<close> .

qualified lift_definition of_nat :: \<open>nat \<Rightarrow> 'a::len word\<close>
  is \<open>int \<circ> take_bit LENGTH('a)\<close> .

qualified lift_definition the_nat :: \<open>'a::len word \<Rightarrow> nat\<close>
  is \<open>nat \<circ> take_bit LENGTH('a)\<close> by simp

qualified lift_definition the_signed_int :: \<open>'a::len word \<Rightarrow> int\<close>
  is \<open>signed_take_bit (LENGTH('a) - Suc 0)\<close> by (simp add: signed_take_bit_decr_length_iff)

qualified lift_definition cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  is \<open>take_bit LENGTH('a)\<close> by simp

qualified lift_definition signed_cast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  is \<open>signed_take_bit (LENGTH('a) - Suc 0)\<close> by (metis signed_take_bit_decr_length_iff)

end

lemma [code_abbrev, simp]:
  \<open>Word.the_int = uint\<close>
  by transfer rule

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

lemma [code_abbrev, simp]:
  \<open>Word.of_int = word_of_int\<close>
  by (rule; transfer) simp

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

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

lemma [code]:
  \<open>Word.the_nat w = nat (Word.the_int w)\<close>
  by transfer simp

lemma [code_abbrev, simp]:
  \<open>Word.the_nat = unat\<close>
  by (rule; transfer) simp

lemma [code]:
  \<open>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)\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (simp add: bit_simps signed_take_bit_eq_take_bit_add)

lemma [code_abbrev, simp]:
  \<open>Word.the_signed_int = sint\<close>
  by (rule; transfer) simp

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

lemma [code_abbrev, simp]:
  \<open>Word.cast = ucast\<close>
  by (rule; transfer) simp

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

lemma [code_abbrev, simp]:
  \<open>Word.signed_cast = scast\<close>
  by (rule; transfer) simp

lemma [code]:
  \<open>unsigned w = of_nat (nat (Word.the_int w))\<close>
  by transfer simp

lemma [code]:
  \<open>signed w = of_int (Word.the_signed_int w)\<close>
  by transfer simp

subsection \<open>Elementary case distinctions\<close>

lemma word_length_one [case_names zero minus_one length_beyond]:
  fixes w :: \<open>'a::len word\<close>
  obtains (zero) \<open>LENGTH('a) = Suc 0\<close> \<open>w = 0\<close>
  | (minus_one) \<open>LENGTH('a) = Suc 0\<close> \<open>w = - 1\<close>
  | (length_beyond) \<open>2 \<le> LENGTH('a)\<close>
proof (cases \<open>2 \<le> LENGTH('a)\<close>)
  case True
  with length_beyond show ?thesis .
next
  case False
  then have \<open>LENGTH('a) = Suc 0\<close>
    by simp
  then have \<open>w = 0 \<or> w = - 1\<close>
    by transfer auto
  with \<open>LENGTH('a) = Suc 0\<close> zero minus_one show ?thesis
    by blast
qed

subsubsection \<open>Basic ordering\<close>

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 \<open>(\<le>)\<close> \<open>(<)\<close> \<open>- 1 :: 'a::len word\<close>
  by (standard; transfer) (simp add: take_bit_eq_mod zmod_minus1)

interpretation word_coorder: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0 :: 'a::len word\<close>
  by (standard; transfer) simp

lemma word_of_nat_less_eq_iff:
  \<open>word_of_nat m \<le> (word_of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
  by transfer (simp add: take_bit_of_nat)

lemma word_of_int_less_eq_iff:
  \<open>word_of_int k \<le> (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
  by transfer rule

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

lemma word_of_int_less_iff:
  \<open>word_of_int k < (word_of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
  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:
  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close>
  by transfer (simp add: less_le)

lemma of_nat_word_less_eq_iff:
  \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close>
  by transfer (simp add: take_bit_of_nat)

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

lemma of_int_word_less_eq_iff:
  \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close>
  by transfer rule

lemma of_int_word_less_iff:
  \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close>
  by transfer rule

instantiation word :: (len) order_bot
begin

lift_definition bot_word :: \<open>'a word\<close>
  is 0 .

instance
  by (standard; transfer) simp

end

lemma bot_word_eq:
  \<open>bot = (0 :: 'a::len word)\<close>
  by transfer rule

instantiation word :: (len) order_top
begin

lift_definition top_word :: \<open>'a word\<close>
  is \<open>- 1\<close> .

instance
  by (standard; transfer) (simp add: take_bit_int_less_eq_mask)

end

lemma top_word_eq:
  \<open>top = (- 1 :: 'a::len word)\<close>
  by transfer rule

subsection \<open>Enumeration\<close>

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

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

instantiation word :: (len) enum
begin

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

definition enum_all_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
  where \<open>enum_all_word = All\<close>

definition enum_ex_word :: \<open>('a word \<Rightarrow> bool) \<Rightarrow> bool\<close>
  where \<open>enum_ex_word = Ex\<close>

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]:
  \<open>Enum.enum_all P \<longleftrightarrow> list_all P Enum.enum\<close>
  \<open>Enum.enum_ex P \<longleftrightarrow> list_ex P Enum.enum\<close> for P :: \<open>'a::len word \<Rightarrow> bool\<close>
  by (simp_all add: enum_all_word_def enum_ex_word_def enum_UNIV list_all_iff list_ex_iff)

subsection \<open>Bit-wise operations\<close>

text \<open>
  The following specification of word division just lifts the pre-existing
  division on integers named ``F-Division'' in \<^cite>\<open>"leijen01"\<close>.
\<close>

instantiation word :: (len) semiring_modulo
begin

lift_definition divide_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b\<close>
  by simp

lift_definition modulo_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b\<close>
  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:
  \<open>unat (v div w) = unat v div unat w\<close>
proof transfer
  fix k l
  have \<open>nat (take_bit LENGTH('a) k) div nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
    by (rule div_le_dividend)
  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
    by (simp add: nat_less_iff)
  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k div take_bit LENGTH('a) l) =
    (nat \<circ> take_bit LENGTH('a)) k div (nat \<circ> take_bit LENGTH('a)) l\<close>
    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:
  \<open>unat (v mod w) = unat v mod unat w\<close>
proof transfer
  fix k l
  have \<open>nat (take_bit LENGTH('a) k) mod nat (take_bit LENGTH('a) l) \<le> nat (take_bit LENGTH('a) k)\<close>
    by (rule mod_less_eq_dividend)
  also have \<open>nat (take_bit LENGTH('a) k) < 2 ^ LENGTH('a)\<close>
    by (simp add: nat_less_iff)
  finally show \<open>(nat \<circ> take_bit LENGTH('a)) (take_bit LENGTH('a) k mod take_bit LENGTH('a) l) =
    (nat \<circ> take_bit LENGTH('a)) k mod (nat \<circ> take_bit LENGTH('a)) l\<close>
    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]:
  \<open>P a\<close> if word_zero: \<open>P 0\<close>
    and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> P (2 * a)\<close>
    and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - Suc 0) \<Longrightarrow> P (1 + 2 * a)\<close>
  for P and a :: \<open>'a::len word\<close>
proof -
  define m :: nat where \<open>m = LENGTH('a) - Suc 0\<close>
  then have l: \<open>LENGTH('a) = Suc m\<close>
    by simp
  define n :: nat where \<open>n = unat a\<close>
  then have \<open>n < 2 ^ LENGTH('a)\<close>
    by transfer (simp add: take_bit_eq_mod)
  then have \<open>n < 2 * 2 ^ m\<close>
    by (simp add: l)
  then have \<open>P (of_nat n)\<close>
  proof (induction n rule: nat_bit_induct)
    case zero
    show ?case
      by simp (rule word_zero)
  next
    case (even n)
    then have \<open>n < 2 ^ m\<close>
      by simp
    with even.IH have \<open>P (of_nat n)\<close>
      by simp
    moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
      by (auto simp: word_greater_zero_iff l word_of_nat_eq_0_iff)
    moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<close>
      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
      by (simp add: l take_bit_eq_mod)
    ultimately have \<open>P (2 * of_nat n)\<close>
      by (rule word_even)
    then show ?case
      by simp
  next
    case (odd n)
    then have \<open>Suc n \<le> 2 ^ m\<close>
      by simp
    with odd.IH have \<open>P (of_nat n)\<close>
      by simp
    moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<close>
      using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
      by (simp add: l take_bit_eq_mod)
    ultimately have \<open>P (1 + 2 * of_nat n)\<close>
      by (rule word_odd)
    then show ?case
      by simp
  qed
  moreover have \<open>of_nat (nat (uint a)) = a\<close>
    by transfer simp
  ultimately show ?thesis
    by (simp add: n_def)
qed

lemma bit_word_half_eq:
  \<open>(of_bool b + a * 2) div 2 = a\<close>
    if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close>
    for a :: \<open>'a::len word\<close>
proof (cases \<open>2 \<le> LENGTH('a::len)\<close>)
  case False
  with that show ?thesis
    by transfer simp
next
  case True
  obtain n where length: \<open>LENGTH('a) = Suc n\<close>
    by (cases \<open>LENGTH('a)\<close>) simp_all
  show ?thesis proof (cases b)
    case False
    moreover have \<open>a * 2 div 2 = a\<close>
    using that proof transfer
      fix k :: int
      from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close>
        by simp
      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
      with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
        by (auto simp: take_bit_Suc_from_most)
      ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
        by (simp add: take_bit_eq_mod)
      with True show \<open>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 \<open>(1 + a * 2) div 2 = a\<close>
    using that proof transfer
      fix k :: int
      from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close>
        using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
      moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
      with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
        by (auto simp: take_bit_Suc_from_most)
      ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
        by (simp add: take_bit_eq_mod)
      with True show \<open>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:
  \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> (
    m \<le> n \<and>
    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 :: \<open>'a word \<Rightarrow> nat \<Rightarrow> bool\<close>
  is \<open>\<lambda>k n. n < LENGTH('a) \<and> bit k n\<close>
proof
  fix k l :: int and n :: nat
  assume *: \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
  show \<open>n < LENGTH('a) \<and> bit k n \<longleftrightarrow> n < LENGTH('a) \<and> bit l n\<close>
  proof (cases \<open>n < LENGTH('a)\<close>)
    case True
    from * have \<open>bit (take_bit LENGTH('a) k) n \<longleftrightarrow> bit (take_bit LENGTH('a) l) n\<close>
      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 \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close>
    and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close>
  for P and a :: \<open>'a word\<close>
  proof (induction a rule: word_bit_induct)
    case zero
    have \<open>0 div 2 = (0::'a word)\<close>
      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 \<open>bit a n \<longleftrightarrow> odd (a div 2 ^ n)\<close> for a :: \<open>'a word\<close> and n
    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit bit_iff_odd_drop_bit)
  show \<open>a div 0 = 0\<close>
    for a :: \<open>'a word\<close>
    by transfer simp
  show \<open>a div 1 = a\<close>
    for a :: \<open>'a word\<close>
    by transfer simp
  show \<open>0 div a = 0\<close>
    for a :: \<open>'a word\<close>
    by transfer simp
  show \<open>a mod b div b = 0\<close>
    for a b :: \<open>'a word\<close>
    by (simp add: word_eq_iff_unsigned [where ?'a = nat] unat_div_distrib unat_mod_distrib)
  show \<open>a div 2 div 2 ^ n = a div 2 ^ Suc n\<close>
    for a :: \<open>'a word\<close> 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 \<open>even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> if \<open>2 ^ Suc n \<noteq> (0::'a word)\<close>
    for a :: \<open>'a word\<close> 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:
  \<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
  for a b :: \<open>'a::len word\<close>
  using that by transfer (auto simp: nat_less_le bit_eq_iff bit_take_bit_iff)

lemma bit_imp_le_length: \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close> for w :: \<open>'a::len word\<close>
  by (meson bit_word.rep_eq that)

lemma not_bit_length [simp]:
  \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
  using bit_imp_le_length by blast

lemma finite_bit_word [simp]:
  \<open>finite {n. bit w n}\<close>
  for w :: \<open>'a::len word\<close>
  by (metis bit_imp_le_length bounded_nat_set_is_finite mem_Collect_eq)

lemma bit_numeral_word_iff [simp]:
  \<open>bit (numeral w :: 'a::len word) n
    \<longleftrightarrow> n < LENGTH('a) \<and> bit (numeral w :: int) n\<close>
  by transfer simp

lemma bit_neg_numeral_word_iff [simp]:
  \<open>bit (- numeral w :: 'a::len word) n
    \<longleftrightarrow> n < LENGTH('a) \<and> bit (- numeral w :: int) n\<close>
  by transfer simp

instantiation word :: (len) ring_bit_operations
begin

lift_definition not_word :: \<open>'a word \<Rightarrow> 'a word\<close>
  is not
  by (simp add: take_bit_not_iff)

lift_definition and_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>and\<close>
  by simp

lift_definition or_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is or
  by simp

lift_definition xor_word ::  \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is xor
  by simp

lift_definition mask_word :: \<open>nat \<Rightarrow> 'a word\<close>
  is mask
  .

lift_definition set_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is set_bit
  by (simp add: set_bit_def)

lift_definition unset_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is unset_bit
  by (simp add: unset_bit_def)

lift_definition flip_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is flip_bit
  by (simp add: flip_bit_def)

lift_definition push_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is push_bit
proof -
  show \<open>take_bit LENGTH('a) (push_bit n k) = take_bit LENGTH('a) (push_bit n l)\<close>
    if \<open>take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> 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 :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>n. drop_bit n \<circ> take_bit LENGTH('a)\<close>
  by (simp add: take_bit_eq_mod)

lift_definition take_bit_word :: \<open>nat \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>n. take_bit (min LENGTH('a) n)\<close>
  by (simp add: ac_simps) (simp only: flip: take_bit_take_bit)

context
  includes bit_operations_syntax
begin

instance proof
  fix v w :: \<open>'a word\<close> and n m :: nat
  show \<open>NOT v = - v - 1\<close>
    by transfer (simp add: not_eq_complement)
  show \<open>v AND w = of_bool (odd v \<and> odd w) + 2 * (v div 2 AND w div 2)\<close>
    apply transfer
    by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
  show \<open>v OR w = of_bool (odd v \<or> odd w) + 2 * (v div 2 OR w div 2)\<close>
    apply transfer
    by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
  show \<open>v XOR w = of_bool (odd v \<noteq> odd w) + 2 * (v div 2 XOR w div 2)\<close>
    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 \<open>mask n = 2 ^ n - (1 :: 'a word)\<close>
    by transfer (simp flip: mask_eq_exp_minus_1)
  show \<open>set_bit n v = v OR push_bit n 1\<close>
    by transfer (simp add: set_bit_eq_or)
  show \<open>unset_bit n v = (v OR push_bit n 1) XOR push_bit n 1\<close>
    by transfer (simp add: unset_bit_eq_or_xor)
  show \<open>flip_bit n v = v XOR push_bit n 1\<close>
    by transfer (simp add: flip_bit_eq_xor)
  show \<open>push_bit n v = v * 2 ^ n\<close>
    by transfer (simp add: push_bit_eq_mult)
  show \<open>drop_bit n v = v div 2 ^ n\<close>
    by transfer (simp add: drop_bit_take_bit flip: drop_bit_eq_div)
  show \<open>take_bit n v = v mod 2 ^ n\<close>
    by transfer (simp flip: take_bit_eq_mod)
qed

end

end

lemma [code]:
  \<open>push_bit n w = w * 2 ^ n\<close> for w :: \<open>'a::len word\<close>
  by (fact push_bit_eq_mult)

lemma [code]:
  \<open>Word.the_int (drop_bit n w) = drop_bit n (Word.the_int w)\<close>
  by transfer (simp add: drop_bit_take_bit min_def le_less less_diff_conv)

lemma [code]:
  \<open>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)\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (simp add: not_le not_less ac_simps min_absorb2)

lemma [code_abbrev]:
  \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
  by (fact push_bit_of_1)

context
  includes bit_operations_syntax
begin

lemma [code]:
  \<open>NOT w = Word.of_int (NOT (Word.the_int w))\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (simp add: take_bit_not_take_bit)

lemma [code]:
  \<open>Word.the_int (v AND w) = Word.the_int v AND Word.the_int w\<close>
  by transfer simp

lemma [code]:
  \<open>Word.the_int (v OR w) = Word.the_int v OR Word.the_int w\<close>
  by transfer simp

lemma [code]:
  \<open>Word.the_int (v XOR w) = Word.the_int v XOR Word.the_int w\<close>
  by transfer simp

lemma [code]:
  \<open>Word.the_int (mask n :: 'a::len word) = mask (min LENGTH('a) n)\<close>
  by transfer simp

lemma [code]:
  \<open>set_bit n w = w OR push_bit n 1\<close> for w :: \<open>'a::len word\<close>
  by (fact set_bit_eq_or)

lemma [code]:
  \<open>unset_bit n w = w AND NOT (push_bit n 1)\<close> for w :: \<open>'a::len word\<close>
  by (fact unset_bit_eq_and_not)

lemma [code]:
  \<open>flip_bit n w = w XOR push_bit n 1\<close> for w :: \<open>'a::len word\<close>
  by (fact flip_bit_eq_xor)

context
  includes lifting_syntax
begin

lemma set_bit_word_transfer [transfer_rule]:
  \<open>((=) ===> pcr_word ===> pcr_word) set_bit set_bit\<close>
  by (unfold set_bit_def) transfer_prover

lemma unset_bit_word_transfer [transfer_rule]:
  \<open>((=) ===> pcr_word ===> pcr_word) unset_bit unset_bit\<close>
  by (unfold unset_bit_def) transfer_prover

lemma flip_bit_word_transfer [transfer_rule]:
  \<open>((=) ===> pcr_word ===> pcr_word) flip_bit flip_bit\<close>
  by (unfold flip_bit_def) transfer_prover

lemma signed_take_bit_word_transfer [transfer_rule]:
  \<open>((=) ===> pcr_word ===> pcr_word)
    (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))
    (signed_take_bit :: nat \<Rightarrow> 'a word \<Rightarrow> 'a word)\<close>
proof -
  let ?K = \<open>\<lambda>n (k :: int). take_bit (min LENGTH('a) n) k OR of_bool (n < LENGTH('a) \<and> bit k n) * NOT (mask n)\<close>
  let ?W = \<open>\<lambda>n (w :: 'a word). take_bit n w OR of_bool (bit w n) * NOT (mask n)\<close>
  have \<open>((=) ===> pcr_word ===> pcr_word) ?K ?W\<close>
    by transfer_prover
  also have \<open>?K = (\<lambda>n k. signed_take_bit n (take_bit LENGTH('a::len) k))\<close>
    by (simp add: fun_eq_iff signed_take_bit_def bit_take_bit_iff ac_simps)
  also have \<open>?W = signed_take_bit\<close>
    by (simp add: fun_eq_iff signed_take_bit_def)
  finally show ?thesis .
qed

end

end

subsection \<open>Conversions including casts\<close>

subsubsection \<open>Generic unsigned conversion\<close>

context semiring_bits
begin

lemma bit_unsigned_iff [bit_simps]:
  \<open>bit (unsigned w) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit w n\<close>
  for w :: \<open>'b::len word\<close>
  by (transfer fixing: bit) (simp add: bit_of_nat_iff bit_nat_iff bit_take_bit_iff)

end

lemma possible_bit_word[simp]:
  \<open>possible_bit TYPE(('a :: len) word) m \<longleftrightarrow> m < LENGTH('a)\<close>
  by (simp add: possible_bit_def linorder_not_le)

context semiring_bit_operations
begin

lemma unsigned_minus_1_eq_mask:
  \<open>unsigned (- 1 :: 'b::len word) = mask LENGTH('b)\<close>
  by (transfer fixing: mask) (simp add: nat_mask_eq of_nat_mask_eq)

lemma unsigned_push_bit_eq:
  \<open>unsigned (push_bit n w) = take_bit LENGTH('b) (push_bit n (unsigned w))\<close>
  for w :: \<open>'b::len word\<close>
proof (rule bit_eqI)
  fix m
  assume \<open>possible_bit TYPE('a) m\<close>
  show \<open>bit (unsigned (push_bit n w)) m = bit (take_bit LENGTH('b) (push_bit n (unsigned w))) m\<close>
  proof (cases \<open>n \<le> m\<close>)
    case True
    with \<open>possible_bit TYPE('a) m\<close> have \<open>possible_bit TYPE('a) (m - n)\<close>
      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:
  \<open>unsigned (take_bit n w) = take_bit n (unsigned w)\<close>
  for w :: \<open>'b::len word\<close>
  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:
  \<open>unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\<close>
  for w :: \<open>'b::len word\<close>
  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:
  \<open>ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)\<close>
  if \<open>LENGTH('a) \<le> LENGTH('b)\<close> for w :: \<open>'a::len word\<close>
  by (rule bit_word_eqI) (use that in \<open>auto simp: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)

context semiring_bit_operations
begin

context
  includes bit_operations_syntax
begin

lemma unsigned_and_eq:
  \<open>unsigned (v AND w) = unsigned v AND unsigned w\<close>
  for v w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps)

lemma unsigned_or_eq:
  \<open>unsigned (v OR w) = unsigned v OR unsigned w\<close>
  for v w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps)

lemma unsigned_xor_eq:
  \<open>unsigned (v XOR w) = unsigned v XOR unsigned w\<close>
  for v w :: \<open>'b::len word\<close>
  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:
  \<open>unsigned (NOT w) = take_bit LENGTH('b) (NOT (unsigned w))\<close>
  for w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps)

end

end

context linordered_euclidean_semiring
begin

lemma unsigned_greater_eq [simp]:
  \<open>0 \<le> unsigned w\<close> for w :: \<open>'b::len word\<close>
  by (transfer fixing: less_eq) simp

lemma unsigned_less [simp]:
  \<open>unsigned w < 2 ^ LENGTH('b)\<close> for w :: \<open>'b::len word\<close>
  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 \<open>Generic signed conversion\<close>

context ring_bit_operations
begin

lemma bit_signed_iff [bit_simps]:
  \<open>bit (signed w) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
  for w :: \<open>'b::len word\<close>
  by (transfer fixing: bit)
    (auto simp: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)

lemma signed_push_bit_eq:
  \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
  for w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj) auto

lemma signed_take_bit_eq:
  \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
  for w :: \<open>'b::len word\<close>
  by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
    (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:
  \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
  for w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps possible_bit_less_imp min_less_iff_disj)
    (auto simp: min_def)

lemma signed_and_eq:
  \<open>signed (v AND w) = signed v AND signed w\<close>
  for v w :: \<open>'b::len word\<close>
  by (rule bit_eqI) (simp add: bit_signed_iff bit_and_iff Bit_Operations.bit_and_iff)

lemma signed_or_eq:
  \<open>signed (v OR w) = signed v OR signed w\<close>
  for v w :: \<open>'b::len word\<close>
  by (rule bit_eqI) (simp add: bit_signed_iff bit_or_iff Bit_Operations.bit_or_iff)

lemma signed_xor_eq:
  \<open>signed (v XOR w) = signed v XOR signed w\<close>
  for v w :: \<open>'b::len word\<close>
  by (rule bit_eqI) (simp add: bit_signed_iff bit_xor_iff Bit_Operations.bit_xor_iff)

end

end

subsubsection \<open>More\<close>

lemma sint_greater_eq:
  \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint w\<close> for w :: \<open>'a::len word\<close>
proof (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>)
  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 *: \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> (0::int)\<close>
    by simp
  case False
  then show ?thesis
    by transfer (auto simp: signed_take_bit_eq intro: order_trans *)
qed

lemma sint_less:
  \<open>sint w < 2 ^ (LENGTH('a) - Suc 0)\<close> for w :: \<open>'a::len word\<close>
  by (cases \<open>bit w (LENGTH('a) - Suc 0)\<close>; 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:
  \<open>uint (v div w) = uint v div uint w\<close>
  by (metis int_ops(8) of_nat_unat unat_div_distrib)

lemma unat_drop_bit_eq:
  \<open>unat (drop_bit n w) = drop_bit n (unat w)\<close>
  by (rule bit_eqI) (simp add: bit_unsigned_iff bit_drop_bit_eq)

lemma uint_mod_distrib:
  \<open>uint (v mod w) = uint v mod uint w\<close>
  by (metis int_ops(9) of_nat_unat unat_mod_distrib)

context semiring_bit_operations
begin

lemma unsigned_ucast_eq:
  \<open>unsigned (ucast w :: 'c::len word) = take_bit LENGTH('c) (unsigned w)\<close>
  for w :: \<open>'b::len word\<close>
  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:
  \<open>signed (ucast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)\<close>
  for w :: \<open>'b::len word\<close>
  by (simp add: bit_eq_iff bit_simps min_less_iff_disj)

lemma signed_scast_eq:
  \<open>signed (scast w :: 'c::len word) = signed_take_bit (LENGTH('c) - Suc 0) (signed w)\<close>
  for w :: \<open>'b::len word\<close>
  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:
  \<open>uint (word_of_int k :: 'a::len word) = take_bit LENGTH('a) k\<close>
  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:
  \<open>sint w = signed_take_bit (LENGTH('a) - Suc 0) (uint w)\<close>
  for w :: \<open>'a::len word\<close>
  by (cases \<open>LENGTH('a)\<close>; transfer) (simp_all add: signed_take_bit_take_bit)

lemma unat_eq_nat_uint:
  \<open>unat w = nat (uint w)\<close>
  by simp

lemma ucast_eq:
  \<open>ucast w = word_of_int (uint w)\<close>
  by transfer simp

lemma scast_eq:
  \<open>scast w = word_of_int (sint w)\<close>
  by transfer simp

lemma uint_0_eq:
  \<open>uint 0 = 0\<close>
  by (fact unsigned_0)

lemma uint_1_eq:
  \<open>uint 1 = 1\<close>
  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 :: \<open>'a word \<Rightarrow> nat\<close>
  is \<open>\<lambda>_. LENGTH('a)\<close> ..

instance ..

end

lemma word_size [code]:
  \<open>size w = LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
  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]:
  \<open>size w \<noteq> 0\<close> for  w :: \<open>'a::len word\<close>
  by auto

lift_definition source_size :: \<open>('a::len word \<Rightarrow> 'b) \<Rightarrow> nat\<close>
  is \<open>\<lambda>_. LENGTH('a)\<close> .

lift_definition target_size :: \<open>('a \<Rightarrow> 'b::len word) \<Rightarrow> nat\<close>
  is \<open>\<lambda>_. LENGTH('b)\<close> ..

lift_definition is_up :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
  is \<open>\<lambda>_. LENGTH('a) \<le> LENGTH('b)\<close> ..

lift_definition is_down :: \<open>('a::len word \<Rightarrow> 'b::len word) \<Rightarrow> bool\<close>
  is \<open>\<lambda>_. LENGTH('a) \<ge> LENGTH('b)\<close> ..

lemma is_up_eq:
  \<open>is_up f \<longleftrightarrow> source_size f \<le> target_size f\<close>
  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  by (simp add: source_size.rep_eq target_size.rep_eq is_up.rep_eq)

lemma is_down_eq:
  \<open>is_down f \<longleftrightarrow> target_size f \<le> source_size f\<close>
  for f :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
  by (simp add: source_size.rep_eq target_size.rep_eq is_down.rep_eq)

lift_definition word_int_case :: \<open>(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b\<close>
  is \<open>\<lambda>f. f \<circ> take_bit LENGTH('a)\<close> by simp

lemma word_int_case_eq_uint [code]:
  \<open>word_int_case f w = f (uint w)\<close>
  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 \<open>Arithmetic operations\<close>

lemma div_word_self:
  \<open>w div w = 1\<close> if \<open>w \<noteq> 0\<close> for w :: \<open>'a::len word\<close>
  using that by transfer simp

lemma mod_word_self [simp]:
  \<open>w mod w = 0\<close> for w :: \<open>'a::len word\<close>
  by (simp add: word_mod_def)

lemma div_word_less:
  \<open>w div v = 0\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
  using that by transfer simp

lemma mod_word_less:
  \<open>w mod v = w\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
  using div_mult_mod_eq [of w v] using that by (simp add: div_word_less)

lemma div_word_one [simp]:
  \<open>1 div w = of_bool (w = 1)\<close> for w :: \<open>'a::len word\<close>
proof transfer
  fix k :: int
  show \<open>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 \<open>LENGTH('a)\<close> 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]:
  \<open>1 mod w = 1 - w * of_bool (w = 1)\<close> for w :: \<open>'a::len word\<close>
  using div_mult_mod_eq [of 1 w] by auto

lemma div_word_by_minus_1_eq [simp]:
  \<open>w div - 1 = of_bool (w = - 1)\<close> for w :: \<open>'a::len word\<close>
  by (auto intro: div_word_less simp add: div_word_self word_order.not_eq_extremum)

lemma mod_word_by_minus_1_eq [simp]:
  \<open>w mod - 1 = w * of_bool (w < - 1)\<close> for w :: \<open>'a::len word\<close>
  using mod_word_less word_order.not_eq_extremum by fastforce

text \<open>Legacy theorems:\<close>

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:
  \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close>
  for a :: \<open>'a::len word\<close>
proof -
  define n where \<open>n = LENGTH('a) - Suc 0\<close>
  then have *: \<open>LENGTH('a) = Suc n\<close>
    by simp
  have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
    using that by transfer
      (auto simp: take_bit_eq_0_iff take_bit_eq_mod *)
  moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
    by transfer simp
  then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
    by (simp add: *)
  ultimately show ?thesis
    by auto
qed

subsection \<open>Ordering\<close>

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]:
  \<open>(0 :: 'a::len word) < numeral y \<longleftrightarrow> (0 :: 'a::len word) \<noteq> numeral y\<close>
  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 :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k \<le> signed_take_bit (LENGTH('a) - Suc 0) l\<close>
  by (simp flip: signed_take_bit_decr_length_iff)

lift_definition word_sless :: \<open>'a::len word \<Rightarrow> 'a word \<Rightarrow> bool\<close>
  is \<open>\<lambda>k l. signed_take_bit (LENGTH('a) - Suc 0) k < signed_take_bit (LENGTH('a) - Suc 0) l\<close>
  by (simp flip: signed_take_bit_decr_length_iff)

notation
  word_sle    (\<open>'(\<le>s')\<close>) and
  word_sle    (\<open>(\<open>notation=\<open>infix \<le>s\<close>\<close>_/ \<le>s _)\<close>  [51, 51] 50) and
  word_sless  (\<open>'(<s')\<close>) and
  word_sless  (\<open>(\<open>notation=\<open>infix <s\<close>\<close>_/ <s _)\<close>  [51, 51] 50)

notation (input)
  word_sle    (\<open>(\<open>notation=\<open>infix <=s\<close>\<close>_/ <=s _)\<close>  [51, 51] 50)

lemma word_sle_eq [code]:
  \<open>a <=s b \<longleftrightarrow> sint a \<le> sint b\<close>
  by transfer simp

lemma word_sless_alt [code]:
  "a ~~sint a < sint b"~~
  by transfer simp

lemma signed_ordering: \<open>ordering word_sle word_sless\<close>
  by (standard; transfer) (auto simp flip: signed_take_bit_decr_length_iff)

lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
  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:
  \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
  by (fact signed.less_le)

lemma minus_1_sless_0 [simp]:
  \<open>- 1 <s 0\<close>
  by transfer simp

lemma not_0_sless_minus_1 [simp]:
  \<open>\<not> 0 <s - 1\<close>
  by transfer simp

lemma minus_1_sless_eq_0 [simp]:
  \<open>- 1 \<le>s 0\<close>
  by transfer simp

lemma not_0_sless_eq_minus_1 [simp]:
  \<open>\<not> 0 \<le>s - 1\<close>
  by transfer simp

subsection \<open>Bit-wise operations\<close>

context
  includes bit_operations_syntax
begin

lemma take_bit_word_eq_self:
  \<open>take_bit n w = w\<close> if \<open>LENGTH('a) \<le> n\<close> for w :: \<open>'a::len word\<close>
  using that by transfer simp

lemma take_bit_length_eq [simp]:
  \<open>take_bit LENGTH('a) w = w\<close> for w :: \<open>'a::len word\<close>
  by (simp add: nat_le_linear take_bit_word_eq_self)

lemma bit_word_of_int_iff:
  \<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
  by (simp add: bit_simps)

lemma bit_uint_iff:
  \<open>bit (uint w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w n\<close>
    for w :: \<open>'a::len word\<close>
  by transfer (simp add: bit_take_bit_iff)

lemma bit_sint_iff:
  \<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a) - 1) \<or> bit w n\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (auto simp: bit_signed_take_bit_iff min_def le_less not_less)

lemma bit_word_ucast_iff:
  \<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close>
  for w :: \<open>'a::len word\<close>
  by (auto simp add: bit_unsigned_iff bit_imp_le_length)

lemma bit_word_scast_iff:
  \<open>bit (scast w :: 'b::len word) n \<longleftrightarrow>
    n < LENGTH('b) \ (bit w n \ LENGTH('a) \ n \ bit w (LENGTH('a) - Suc 0))\
  for w :: \<open>'a::len word\<close>
  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]:
  \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
  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 :: \<open>'a::len word \<Rightarrow> bool\<close>
  where [code_abbrev]: \<open>even_word = even\<close>

lemma even_word_iff [code]:
  \<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
  by (simp add: and_one_eq even_iff_mod_2_eq_zero even_word_def)

lemma map_bit_range_eq_if_take_bit_eq:
  \<open>map (bit k) [0..<n] = map (bit l) [0..<n]\<close>
  if \<open>take_bit n k = take_bit n l\<close> 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 \<open>take_bit n (k div 2) = take_bit n (l div 2)\<close>
    by (simp add: take_bit_Suc)
  then have \<open>map (bit (k div 2)) [0..<n] = map (bit (l div 2)) [0..<n]\<close>
    by (rule Suc.IH)
  moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int
    by (simp add: fun_eq_iff bit_Suc)
  moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close>
    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]: \<open>take_bit (numeral n) (numeral (num.Bit0 m) :: 'a::len word)
    = 2 * take_bit (pred_numeral n) (numeral m)\<close> (is ?P)
  and take_bit_word_Bit1_eq [simp]: \<open>take_bit (numeral n) (numeral (num.Bit1 m) :: 'a::len word)
    = 1 + 2 * take_bit (pred_numeral n) (numeral m)\<close> (is ?Q)
  and take_bit_word_minus_Bit0_eq [simp]: \<open>take_bit (numeral n) (- numeral (num.Bit0 m) :: 'a::len word)
    = 2 * take_bit (pred_numeral n) (- numeral m)\<close> (is ?R)
  and take_bit_word_minus_Bit1_eq [simp]: \<open>take_bit (numeral n) (- numeral (num.Bit1 m) :: 'a::len word)
    = 1 + 2 * take_bit (pred_numeral n) (- numeral (Num.inc m))\<close> (is ?S)
proof -
  define w :: \<open>'a::len word\<close>
    where \<open>w = numeral m\<close>
  moreover define q :: nat
    where \<open>q = pred_numeral n\<close>
  ultimately have num:
    \<open>numeral m = w\<close>
    \<open>numeral (num.Bit0 m) = 2 * w\<close>
    \<open>numeral (num.Bit1 m) = 1 + 2 * w\<close>
    \<open>numeral (Num.inc m) = 1 + w\<close>
--> --------------------

--> maximum size reached

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

quality95%

¤ Dauer der Verarbeitung: 0.39 Sekunden (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.