Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: session.ML Sprache: Isabelle

Untersuchung 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"
  "HOL-Library.Boolean_Algebra"
  "HOL-Library.Bit_Operations"
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 (cases \<open>LENGTH('a)\<close>)
    (simp_all 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 add: 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 add: take_bit_eq_mod intro: mod_diff_cong)

lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close>
  is uminus
  by (auto simp add: 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 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]:
  \<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
  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]:
  \<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
  by transfer simp

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 add: 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 [simp]:
  \<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 [simp]:
  \<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 [simp]:
  \<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 [simp]:
  \<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 [simp]:
  \<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 [simp]:
  \<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 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 = signed_take_bit (LENGTH('a) - Suc 0) (Word.the_int w)\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (simp add: signed_take_bit_take_bit)

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

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

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 = Ball UNIV\<close>

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

lemma [code]:
  \<open>Enum.enum_all P \<longleftrightarrow> Ball UNIV P\<close>
  \<open>Enum.enum_ex P \<longleftrightarrow> Bex UNIV P\<close> for P :: \<open>'a word \<Rightarrow> bool\<close>
  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 \<open>Bit-wise operations\<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

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]:
  \<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 add: word_greater_zero_iff l)
    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
  have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int
    by auto
  with False that show ?thesis
    by transfer (simp add: eq_iff)
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>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
        by (simp add: take_bit_eq_mod divmod_digit_0)
      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>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close>
        by (simp add: take_bit_eq_mod divmod_digit_0)
      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 add: 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>0 div a = 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
  have \<section>: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 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 \<open>a mod b div b = 0\<close>
    for a b :: \<open>'a word\<close>
    apply transfer
    apply (simp add: take_bit_eq_mod mod_eq_0_iff_dvd dvd_def)
    by (metis (no_types, hide_lams) "\

" 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 \<open>(1 + a) div 2 = a div 2\<close>
    if \<open>even a\<close>
    for a :: \<open>'a word\<close>
    using that by transfer
      (auto dest: le_Suc_ex simp add: mod_2_eq_odd take_bit_Suc elim!: evenE)
  show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close>
    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 \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close>
    if \<open>m \<le> n\<close> 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 \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
    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 \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
    for m n :: nat
    by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)
  show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close>
    for a :: \<open>'a word\<close> and m n :: nat
  proof transfer
    show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow>
      n < m
      \<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0
      \<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\<close>
    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:
  \<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 add: 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>
  using that by transfer simp

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

lemma finite_bit_word [simp]:
  \<open>finite {n. bit w n}\<close>
  for w :: \<open>'a::len word\<close>
proof -
  have \<open>{n. bit w n} \<subseteq> {0..LENGTH('a)}\<close>
    by (auto dest: bit_imp_le_length)
  moreover have \<open>finite {0..LENGTH('a)}\<close>
    by simp
  ultimately show ?thesis
    by (rule finite_subset)
qed

instantiation word :: (len) semiring_bit_shifts
begin

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
  proof -
    from that
    have \<open>take_bit (LENGTH('a) - n) (take_bit LENGTH('a) k)
      = take_bit (LENGTH('a) - n) (take_bit LENGTH('a) l)\<close>
      by simp
    moreover have \<open>min (LENGTH('a) - n) LENGTH('a) = LENGTH('a) - n\<close>
      by simp
    ultimately show ?thesis
      by (simp add: take_bit_push_bit)
  qed
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)

instance proof
  show \<open>push_bit n a = a * 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
    by transfer (simp add: push_bit_eq_mult)
  show \<open>drop_bit n a = a div 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
    by transfer (simp flip: drop_bit_eq_div add: drop_bit_take_bit)
  show \<open>take_bit n a = a mod 2 ^ n\<close> for n :: nat and a :: \<open>'a word\<close>
    by transfer (auto simp flip: take_bit_eq_mod)
qed

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)

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
  .

instance by (standard; transfer)
  (auto simp add: minus_eq_not_minus_1 mask_eq_exp_minus_1
    bit_not_iff bit_and_iff bit_or_iff bit_xor_iff)

end

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

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

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

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> 2 ^ n \<noteq> 0 \<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

context semiring_bit_shifts
begin

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>2 ^ m \<noteq> 0\<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>2 ^ m \<noteq> 0\<close> have \<open>2 ^ (m - n) \<noteq> 0\<close>
      by (metis (full_types) diff_add exp_add_not_zero_imp)
    with True show ?thesis
      by (simp add: bit_unsigned_iff bit_push_bit_iff Parity.bit_push_bit_iff bit_take_bit_iff not_le exp_eq_zero_iff ac_simps)
  next
    case False
    then show ?thesis
      by (simp add: not_le bit_unsigned_iff bit_push_bit_iff Parity.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 Parity.bit_take_bit_iff)

end

context unique_euclidean_semiring_with_bit_shifts
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 add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Parity.bit_drop_bit_eq dest: bit_imp_le_length)

end

context semiring_bit_operations
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 (rule bit_eqI) (simp add: bit_unsigned_iff bit_and_iff Bit_Operations.bit_and_iff)

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

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

end

context ring_bit_operations
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 (rule bit_eqI)
    (simp add: bit_unsigned_iff bit_take_bit_iff bit_not_iff Bit_Operations.bit_not_iff exp_eq_zero_iff not_le)

end

context unique_euclidean_semiring_numeral
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> 2 ^ n \<noteq> 0 \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
  for w :: \<open>'b::len word\<close>
  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:
  \<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>
proof (rule bit_eqI)
  fix m
  assume \<open>2 ^ m \<noteq> 0\<close>
  define q where \<open>q = LENGTH('b) - Suc 0\<close>
  then have *: \<open>LENGTH('b) = Suc q\<close>
    by simp
  show \<open>bit (signed (push_bit n w)) m \<longleftrightarrow>
    bit (signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))) m\<close>
  proof (cases \<open>q \<le> m\<close>)
    case True
    moreover define r where \<open>r = m - q\<close>
    ultimately have \<open>m = q + r\<close>
      by simp
    moreover from \<open>m = q + r\<close> \<open>2 ^ m \<noteq> 0\<close> have \<open>2 ^ q \<noteq> 0\<close> \<open>2 ^ r \<noteq> 0\<close>
      using exp_add_not_zero_imp_left [of q r] exp_add_not_zero_imp_right [of q r]
      by simp_all
    moreover from \<open>2 ^ q \<noteq> 0\<close> have \<open>2 ^ (q - n) \<noteq> 0\<close>
      by (rule exp_not_zero_imp_exp_diff_not_zero)
    ultimately show ?thesis
      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
      min_def * exp_eq_zero_iff le_diff_conv2)
  next
    case False
    then show ?thesis
      using exp_not_zero_imp_exp_diff_not_zero [of m n]
      by (auto simp add: bit_signed_iff bit_signed_take_bit_iff bit_push_bit_iff Parity.bit_push_bit_iff
      min_def not_le not_less * le_diff_conv2 less_diff_conv2 Parity.exp_eq_0_imp_not_bit exp_eq_0_imp_not_bit
      exp_eq_zero_iff)
  qed
qed

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 add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)

lemma signed_not_eq:
  \<open>signed (NOT w) = signed_take_bit LENGTH('b) (NOT (signed w))\<close>
  for w :: \<open>'b::len word\<close>
proof (rule bit_eqI)
  fix n
  assume \<open>2 ^ n \<noteq> 0\<close>
  define q where \<open>q = LENGTH('b) - Suc 0\<close>
  then have *: \<open>LENGTH('b) = Suc q\<close>
    by simp
  show \<open>bit (signed (NOT w)) n \<longleftrightarrow>
    bit (signed_take_bit LENGTH('b) (NOT (signed w))) n\
  proof (cases \<open>q < n\<close>)
    case True
    moreover define r where \<open>r = n - Suc q\<close>
    ultimately have \<open>n = r + Suc q\<close>
      by simp
    moreover from \<open>2 ^ n \<noteq> 0\<close> \<open>n = r + Suc q\<close>
      have \<open>2 ^ Suc q \<noteq> 0\<close>
      using exp_add_not_zero_imp_right by blast
    ultimately show ?thesis
      by (simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
        exp_eq_zero_iff)
  next
    case False
    then show ?thesis
      by (auto simp add: * bit_signed_iff bit_not_iff bit_signed_take_bit_iff Bit_Operations.bit_not_iff min_def
        exp_eq_zero_iff)
  qed
qed

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

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

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

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>
proof -
  have \<open>int (unat (v mod w)) = int (unat v mod unat w)\<close>
    by (simp add: unat_mod_distrib)
  then show ?thesis
    by (simp add: of_nat_mod)
qed

context semiring_bit_shifts
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 exp_eq_zero_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>
proof (rule bit_eqI)
  fix n
  assume \<open>2 ^ n \<noteq> 0\<close>
  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
    by (simp add: min_def)
      (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
  then show \<open>bit (signed (ucast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (unsigned w)) n\<close>
    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_unsigned_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
qed

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>
proof (rule bit_eqI)
  fix n
  assume \<open>2 ^ n \<noteq> 0\<close>
  then have \<open>2 ^ (min (LENGTH('c) - Suc 0) n) \<noteq> 0\<close>
    by (simp add: min_def)
      (metis (mono_tags) diff_diff_cancel exp_not_zero_imp_exp_diff_not_zero)
  then show \<open>bit (signed (scast w :: 'c::len word)) n \<longleftrightarrow> bit (signed_take_bit (LENGTH('c) - Suc 0) (signed w)) n\<close>
    by (simp add: bit_signed_iff bit_unsigned_iff Word.bit_signed_iff bit_signed_take_bit_iff exp_eq_zero_iff not_le)
qed

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 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 :: \<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>

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

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    ("'(\s')") and
  word_sle    ("(_/ \s _)" [51, 51] 50) and
  word_sless  ("'() and
  word_sless  ("(_/   [51, 51] 50)

notation (input)
  word_sle    ("(_/ <=s _)"  [51, 51] 50)

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

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

lemma signed_ordering: \<open>ordering word_sle word_sless\<close>
  apply (standard; transfer)
  using signed_take_bit_decr_length_iff by force+

lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
  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:
  \<open>x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y\<close>
  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: take_bit_minus_one_eq_mask 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 [THEN leD]

lemma word_gt_0: "0 < y \ 0 \ y"
  for y :: "'a::len word"
  by (simp add: less_le)

lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y

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

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 add: less_le [of 0])

lemmas unat_mono = word_less_nat_alt [THEN iffD1]

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_nat_alt)
  ultimately have "wf {(a, b :: ('a::len) word). a < b}"
    by (rule wf_subset)
  then show "P a" using *
    by induction blast
qed

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 transfer (simp add: take_bit_eq_mod)

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 transfer (simp add: take_bit_eq_mod)

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

lemma uint_take_bit_eq:
  \<open>uint (take_bit n w) = take_bit n (uint w)\<close>
  by transfer (simp add: ac_simps)

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 (rule take_bit_word_eq_self) simp

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 transfer rule

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 add: 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 transfer (simp add: bit_take_bit_iff ac_simps)

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 transfer (auto simp add: bit_signed_take_bit_iff le_less min_def)

lift_definition shiftl1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
  is \<open>(*) 2\<close>
  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)

lemma shiftl1_eq:
  \<open>shiftl1 w = word_of_int (2 * uint w)\<close>
  by transfer (simp add: take_bit_eq_mod mod_simps)

lemma shiftl1_eq_mult_2:
  \<open>shiftl1 = (*) 2\<close>
  by (rule ext, transfer) simp

lemma bit_shiftl1_iff [bit_simps]:
  \<open>bit (shiftl1 w) n \<longleftrightarrow> 0 < n \<and> n < LENGTH('a) \<and> bit w (n - 1)\<close>
    for w :: \<open>'a::len word\<close>
  by (simp add: shiftl1_eq_mult_2 bit_double_iff not_le) (simp add: ac_simps)

lift_definition shiftr1 :: \<open>'a::len word \<Rightarrow> 'a word\<close>
  \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
  is \<open>\<lambda>k. take_bit LENGTH('a) k div 2\<close>
  by simp

lemma shiftr1_eq_div_2:
  \<open>shiftr1 w = w div 2\<close>
  by transfer simp

lemma bit_shiftr1_iff [bit_simps]:
  \<open>bit (shiftr1 w) n \<longleftrightarrow> bit w (Suc n)\<close>
  by transfer (auto simp flip: bit_Suc simp add: bit_take_bit_iff)

lemma shiftr1_eq:
  \<open>shiftr1 w = word_of_int (uint w div 2)\<close>
  by transfer simp

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

lift_definition setBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>k n. set_bit n k\<close>
  by (simp add: take_bit_set_bit_eq)

lemma set_Bit_eq:
  \<open>setBit w n = set_bit n w\<close>
  by transfer simp

lemma bit_setBit_iff [bit_simps]:
  \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (auto simp add: bit_set_bit_iff)

lift_definition clearBit :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> 'a word\<close>
  is \<open>\<lambda>k n. unset_bit n k\<close>
  by (simp add: take_bit_unset_bit_eq)

lemma clear_Bit_eq:
  \<open>clearBit w n = unset_bit n w\<close>
  by transfer simp

lemma bit_clearBit_iff [bit_simps]:
  \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
  for w :: \<open>'a::len word\<close>
  by transfer (auto simp add: bit_unset_bit_iff)

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

--> maximum size reached

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

~~¤ Dauer der Verarbeitung: 0.67 Sekunden (vorverarbeitet) ¤~~

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: session.ML Sprache: Isabelle

Untersuchung Isabelle©

¤ Dauer der Verarbeitung: 0.67 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

Bot Zugriff

^© Kompilation durch diese Firma

Untersuchung Isabelle^©