(*  Title:      HOL/Word/Word.thy

     Author:     Jeremy Dawson and Gerwin Klein, NICTA

 *)

 section {* A type of finite bit strings *}

 theory Word

 imports

   Type_Length

   "~~/src/HOL/Library/Boolean_Algebra"

   Bits_Bit

   Bool_List_Representation

   Misc_Typedef

   Word_Miscellaneous

 begin

 text {* See @{file "Examples/WordExamples.thy"} for examples. *}

 subsection {* Type definition *}

 typedef 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"

   morphisms uint Abs_word by auto

 lemma uint_nonnegative:

   "0 \<le> uint w"

   using word.uint [of w] by simp

 lemma uint_bounded:

   fixes w :: "'a::len0 word"

   shows "uint w < 2 ^ len_of TYPE('a)"

   using word.uint [of w] by simp

 lemma uint_idem:

   fixes w :: "'a::len0 word"

   shows "uint w mod 2 ^ len_of TYPE('a) = uint w"

   using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)

 lemma word_uint_eq_iff:

   "a = b \<longleftrightarrow> uint a = uint b"

   by (simp add: uint_inject)

 lemma word_uint_eqI:

   "uint a = uint b \<Longrightarrow> a = b"

   by (simp add: word_uint_eq_iff)

 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"

 where

   -- {* representation of words using unsigned or signed bins,

     only difference in these is the type class *}

   "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"

 lemma uint_word_of_int:

   "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"

   by (auto simp add: word_of_int_def intro: Abs_word_inverse)

 lemma word_of_int_uint:

   "word_of_int (uint w) = w"

   by (simp add: word_of_int_def uint_idem uint_inverse)

 lemma split_word_all:

   "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"

 proof

   fix x :: "'a word"

   assume "\<And>x. PROP P (word_of_int x)"

   then have "PROP P (word_of_int (uint x))" .

   then show "PROP P x" by (simp add: word_of_int_uint)

 qed

 subsection {* Type conversions and casting *}

 definition sint :: "'a::len word \<Rightarrow> int"

 where

   -- {* treats the most-significant-bit as a sign bit *}

   sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"

 definition unat :: "'a::len0 word \<Rightarrow> nat"

 where

   "unat w = nat (uint w)"

 definition uints :: "nat \<Rightarrow> int set"

 where

   -- "the sets of integers representing the words"

   "uints n = range (bintrunc n)"

 definition sints :: "nat \<Rightarrow> int set"

 where

   "sints n = range (sbintrunc (n - 1))"

 lemma uints_num:

   "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"

   by (simp add: uints_def range_bintrunc)

 lemma sints_num:

   "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"

   by (simp add: sints_def range_sbintrunc)

 definition unats :: "nat \<Rightarrow> nat set"

 where

   "unats n = {i. i < 2 ^ n}"

 definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"

 where

   "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"

 definition scast :: "'a::len word \<Rightarrow> 'b::len word"

 where

   -- "cast a word to a different length"

   "scast w = word_of_int (sint w)"

 definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word"

 where

   "ucast w = word_of_int (uint w)"

 instantiation word :: (len0) size

 begin

 definition

   word_size: "size (w :: 'a word) = len_of TYPE('a)"

 instance ..

 end

 lemma word_size_gt_0 [iff]:

   "0 < size (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]:

   shows "size (w::'a::len word) \<noteq> 0"

   and "len_of TYPE('a::len) \<noteq> 0"

   by auto

 definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"

 where

   -- "whether a cast (or other) function is to a longer or shorter length"

   [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"

 definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"

 where

   [code del]: "target_size c = size (c undefined)"

 definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"

 where

   "is_up c \<longleftrightarrow> source_size c \<le> target_size c"

 definition is_down :: "('a :: len0 word \<Rightarrow> 'b :: len0 word) \<Rightarrow> bool"

 where

   "is_down c \<longleftrightarrow> target_size c \<le> source_size c"

 definition of_bl :: "bool list \<Rightarrow> 'a::len0 word"

 where

   "of_bl bl = word_of_int (bl_to_bin bl)"

 definition to_bl :: "'a::len0 word \<Rightarrow> bool list"

 where

   "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"

 definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word"

 where

   "word_reverse w = of_bl (rev (to_bl w))"

 definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b" 

 where

   "word_int_case f w = f (uint w)"

 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 {* Correspondence relation for theorem transfer *}

 definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"

 where

   "cr_word = (\<lambda>x y. word_of_int x = y)"

 lemma Quotient_word:

   "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)

     word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"

   unfolding Quotient_alt_def cr_word_def

   by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)

 lemma reflp_word:

   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"

   by (simp add: reflp_def)

 setup_lifting Quotient_word reflp_word

 text {* TODO: The next lemma could be generated automatically. *}

 lemma uint_transfer [transfer_rule]:

   "(rel_fun pcr_word op =) (bintrunc (len_of TYPE('a)))

     (uint :: 'a::len0 word \<Rightarrow> int)"

   unfolding rel_fun_def word.pcr_cr_eq cr_word_def

   by (simp add: no_bintr_alt1 uint_word_of_int)

 subsection {* Basic code generation setup *}

 definition Word :: "int \<Rightarrow> 'a::len0 word"

 where

   [code_post]: "Word = word_of_int"

 lemma [code abstype]:

   "Word (uint w) = w"

   by (simp add: Word_def word_of_int_uint)

 declare uint_word_of_int [code abstract]

 instantiation word :: (len0) equal

 begin

 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"

 where

   "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"

 instance proof

 qed (simp add: equal equal_word_def word_uint_eq_iff)

 end

 notation fcomp (infixl "\<circ>>" 60)

 notation scomp (infixl "\<circ>\<rightarrow>" 60)

 instantiation word :: ("{len0, typerep}") random

 begin

 definition

   "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (

      let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word

      in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"

 instance ..

 end

 no_notation fcomp (infixl "\<circ>>" 60)

 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)

 subsection {* Type-definition locale instantiations *}

 lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)

 lemmas uint_lt = uint_bounded (* FIXME duplicate *)

 lemmas uint_mod_same = uint_idem (* FIXME duplicate *)

 lemma td_ext_uint: 

   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0))) 

     (\<lambda>w::int. w mod 2 ^ len_of TYPE('a))"

   apply (unfold td_ext_def')

   apply (simp add: uints_num word_of_int_def bintrunc_mod2p)

   apply (simp add: uint_mod_same uint_0 uint_lt

                    word.uint_inverse word.Abs_word_inverse int_mod_lem)

   done

 interpretation word_uint:

   td_ext "uint::'a::len0 word \<Rightarrow> int" 

          word_of_int 

          "uints (len_of TYPE('a::len0))"

          "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"

   by (fact td_ext_uint)

 lemmas td_uint = word_uint.td_thm

 lemmas int_word_uint = word_uint.eq_norm

 lemma td_ext_ubin:

   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))

     (bintrunc (len_of TYPE('a)))"

   by (unfold no_bintr_alt1) (fact td_ext_uint)

 interpretation word_ubin:

   td_ext "uint::'a::len0 word \<Rightarrow> int" 

          word_of_int 

          "uints (len_of TYPE('a::len0))"

          "bintrunc (len_of TYPE('a::len0))"

   by (fact td_ext_ubin)

 subsection {* Arithmetic operations *}

 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"

   by (metis bintr_ariths(6))

 lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"

   by (metis bintr_ariths(7))

 instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}"

 begin

 lift_definition zero_word :: "'a word" is "0" .

 lift_definition one_word :: "'a word" is "1" .

 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op +"

   by (metis bintr_ariths(2))

 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op -"

   by (metis bintr_ariths(3))

 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus

   by (metis bintr_ariths(5))

 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "op *"

   by (metis bintr_ariths(4))

 definition

   word_div_def: "a div b = word_of_int (uint a div uint b)"

 definition

   word_mod_def: "a mod b = word_of_int (uint a mod uint b)"

 instance

   by default (transfer, simp add: algebra_simps)+

 end

 text {* Legacy theorems: *}

 lemma word_arith_wis [code]: shows

   word_add_def: "a + b = word_of_int (uint a + uint b)" and

   word_sub_wi: "a - b = word_of_int (uint a - uint b)" and

   word_mult_def: "a * b = word_of_int (uint a * uint b)" and

   word_minus_def: "- a = word_of_int (- uint a)" and

   word_succ_alt: "word_succ a = word_of_int (uint a + 1)" and

   word_pred_alt: "word_pred a = word_of_int (uint a - 1)" and

   word_0_wi: "0 = word_of_int 0" and

   word_1_wi: "1 = word_of_int 1"

   unfolding plus_word_def minus_word_def times_word_def uminus_word_def

   unfolding word_succ_def word_pred_def zero_word_def one_word_def

   by simp_all

 lemmas arths = 

   bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]

 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]

 instance word :: (len) comm_ring_1

 proof

   have "0 < len_of TYPE('a)" by (rule len_gt_0)

   then show "(0::'a word) \<noteq> 1"

     by - (transfer, auto simp add: gr0_conv_Suc)

 qed

 lemma word_of_nat: "of_nat n = word_of_int (int n)"

   by (induct n) (auto simp add : word_of_int_hom_syms)

 lemma word_of_int: "of_int = word_of_int"

   apply (rule ext)

   apply (case_tac x rule: int_diff_cases)

   apply (simp add: word_of_nat wi_hom_sub)

   done

 definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50)

 where

   "a udvd b = (EX n>=0. uint b = n * uint a)"

 subsection {* Ordering *}

 instantiation word :: (len0) linorder

 begin

 definition

   word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"

 definition

   word_less_def: "a < b \<longleftrightarrow> uint a < uint b"

 instance

   by default (auto simp: word_less_def word_le_def)

 end

 definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50)

 where

   "a <=s b = (sint a <= sint b)"

 definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50)

 where

   "(x <s y) = (x <=s y & x ~= y)"

 subsection {* Bit-wise operations *}

 instantiation word :: (len0) bits

 begin

 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT

   by (metis bin_trunc_not)

 lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitAND

   by (metis bin_trunc_and)

 lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitOR

   by (metis bin_trunc_or)

 lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR

   by (metis bin_trunc_xor)

 definition

   word_test_bit_def: "test_bit a = bin_nth (uint a)"

 definition

   word_set_bit_def: "set_bit a n x =

    word_of_int (bin_sc n x (uint a))"

 definition

   word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"

 definition

   word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"

 definition shiftl1 :: "'a word \<Rightarrow> 'a word"

 where

   "shiftl1 w = word_of_int (uint w BIT False)"

 definition shiftr1 :: "'a word \<Rightarrow> 'a word"

 where

   -- "shift right as unsigned or as signed, ie logical or arithmetic"

   "shiftr1 w = word_of_int (bin_rest (uint w))"

 definition

   shiftl_def: "w << n = (shiftl1 ^^ n) w"

 definition

   shiftr_def: "w >> n = (shiftr1 ^^ n) w"

 instance ..

 end

 lemma [code]: shows

   word_not_def: "NOT (a::'a::len0 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)"

   unfolding bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def

   by simp_all

 instantiation word :: (len) bitss

 begin

 definition

   word_msb_def: 

   "msb a \<longleftrightarrow> bin_sign (sint a) = -1"

 instance ..

 end

 definition setBit :: "'a :: len0 word => nat => 'a word"

 where 

   "setBit w n = set_bit w n True"

 definition clearBit :: "'a :: len0 word => nat => 'a word"

 where

   "clearBit w n = set_bit w n False"

 subsection {* Shift operations *}

 definition sshiftr1 :: "'a :: len word => 'a word"

 where 

   "sshiftr1 w = word_of_int (bin_rest (sint w))"

 definition bshiftr1 :: "bool => 'a :: len word => 'a word"

 where

   "bshiftr1 b w = of_bl (b # butlast (to_bl w))"

 definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55)

 where

   "w >>> n = (sshiftr1 ^^ n) w"

 definition mask :: "nat => 'a::len word"

 where

   "mask n = (1 << n) - 1"

 definition revcast :: "'a :: len0 word => 'b :: len0 word"

 where

   "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"

 definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word"

 where

   "slice1 n w = of_bl (takefill False n (to_bl w))"

 definition slice :: "nat => 'a :: len0 word => 'b :: len0 word"

 where

   "slice n w = slice1 (size w - n) w"

 subsection {* Rotation *}

 definition rotater1 :: "'a list => 'a list"

 where

   "rotater1 ys = 

     (case ys of [] => [] | x # xs => last ys # butlast ys)"

 definition rotater :: "nat => 'a list => 'a list"

 where

   "rotater n = rotater1 ^^ n"

 definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word"

 where

   "word_rotr n w = of_bl (rotater n (to_bl w))"

 definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word"

 where

   "word_rotl n w = of_bl (rotate n (to_bl w))"

 definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word"

 where

   "word_roti i w = (if i >= 0 then word_rotr (nat i) w

                     else word_rotl (nat (- i)) w)"

 subsection {* Split and cat operations *}

 definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word"

 where

   "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"

 definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)"

 where

   "word_split a = 

    (case bin_split (len_of TYPE ('c)) (uint a) of 

      (u, v) => (word_of_int u, word_of_int v))"

 definition word_rcat :: "'a :: len0 word list => 'b :: len0 word"

 where

   "word_rcat ws = 

   word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"

 definition word_rsplit :: "'a :: len0 word => 'b :: len word list"

 where

   "word_rsplit w = 

   map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"

 definition max_word :: "'a::len word" -- "Largest representable machine integer."

 where

   "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"

 lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)

 subsection {* Theorems about typedefs *}

 lemma sint_sbintrunc': 

   "sint (word_of_int bin :: 'a word) = 

     (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"

   unfolding sint_uint 

   by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt)

 lemma uint_sint: 

   "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))"

   unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)

 lemma bintr_uint:

   fixes w :: "'a::len0 word"

   shows "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"

   apply (subst word_ubin.norm_Rep [symmetric]) 

   apply (simp only: bintrunc_bintrunc_min word_size)

   apply (simp add: min.absorb2)

   done

 lemma wi_bintr:

   "len_of TYPE('a::len0) \<le> n \<Longrightarrow>

     word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"

   by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min.absorb1)

 lemma td_ext_sbin: 

   "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len))) 

     (sbintrunc (len_of TYPE('a) - 1))"

   apply (unfold td_ext_def' sint_uint)

   apply (simp add : word_ubin.eq_norm)

   apply (cases "len_of TYPE('a)")

    apply (auto simp add : sints_def)

   apply (rule sym [THEN trans])

   apply (rule word_ubin.Abs_norm)

   apply (simp only: bintrunc_sbintrunc)

   apply (drule sym)

   apply simp

   done

 lemma td_ext_sint:

   "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))

      (\<lambda>w. (w + 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -

          2 ^ (len_of TYPE('a) - 1))"

   using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)

 (* We do sint before sbin, before sint is the user version

    and interpretations do not produce thm duplicates. I.e. 

    we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,

    because the latter is the same thm as the former *)

 interpretation word_sint:

   td_ext "sint ::'a::len word => int" 

           word_of_int 

           "sints (len_of TYPE('a::len))"

           "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -

                2 ^ (len_of TYPE('a::len) - 1)"

   by (rule td_ext_sint)

 interpretation word_sbin:

   td_ext "sint ::'a::len word => int" 

           word_of_int 

           "sints (len_of TYPE('a::len))"

           "sbintrunc (len_of TYPE('a::len) - 1)"

   by (rule td_ext_sbin)

 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]

 lemmas td_sint = word_sint.td

 lemma to_bl_def': 

   "(to_bl :: 'a :: len0 word => bool list) =

     bin_to_bl (len_of TYPE('a)) o uint"

   by (auto simp: to_bl_def)

 lemmas word_reverse_no_def [simp] = word_reverse_def [of "numeral w"] for w

 lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"

   by (fact uints_def [unfolded no_bintr_alt1])

 lemma word_numeral_alt:

   "numeral b = word_of_int (numeral b)"

   by (induct b, simp_all only: numeral.simps word_of_int_homs)

 declare word_numeral_alt [symmetric, code_abbrev]

 lemma word_neg_numeral_alt:

   "- numeral b = word_of_int (- numeral b)"

   by (simp only: word_numeral_alt wi_hom_neg)

 declare word_neg_numeral_alt [symmetric, code_abbrev]

 lemma word_numeral_transfer [transfer_rule]:

   "(rel_fun op = pcr_word) numeral numeral"

   "(rel_fun op = pcr_word) (- numeral) (- numeral)"

   apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)

   using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by blast+

 lemma uint_bintrunc [simp]:

   "uint (numeral bin :: 'a word) = 

     bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"

   unfolding word_numeral_alt by (rule word_ubin.eq_norm)

 lemma uint_bintrunc_neg [simp]: "uint (- numeral bin :: 'a word) = 

     bintrunc (len_of TYPE ('a :: len0)) (- numeral bin)"

   by (simp only: word_neg_numeral_alt word_ubin.eq_norm)

 lemma sint_sbintrunc [simp]:

   "sint (numeral bin :: 'a word) = 

     sbintrunc (len_of TYPE ('a :: len) - 1) (numeral bin)"

   by (simp only: word_numeral_alt word_sbin.eq_norm)

 lemma sint_sbintrunc_neg [simp]: "sint (- numeral bin :: 'a word) = 

     sbintrunc (len_of TYPE ('a :: len) - 1) (- numeral bin)"

   by (simp only: word_neg_numeral_alt word_sbin.eq_norm)

 lemma unat_bintrunc [simp]:

   "unat (numeral bin :: 'a :: len0 word) =

     nat (bintrunc (len_of TYPE('a)) (numeral bin))"

   by (simp only: unat_def uint_bintrunc)

 lemma unat_bintrunc_neg [simp]:

   "unat (- numeral bin :: 'a :: len0 word) =

     nat (bintrunc (len_of TYPE('a)) (- numeral bin))"

   by (simp only: unat_def uint_bintrunc_neg)

 lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"

   apply (unfold word_size)

   apply (rule word_uint.Rep_eqD)

   apply (rule box_equals)

     defer

     apply (rule word_ubin.norm_Rep)+

   apply simp

   done

 lemma uint_ge_0 [iff]: "0 \<le> uint (x::'a::len0 word)"

   using word_uint.Rep [of x] by (simp add: uints_num)

 lemma uint_lt2p [iff]: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"

   using word_uint.Rep [of x] by (simp add: uints_num)

 lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint (x::'a::len word)"

   using word_sint.Rep [of x] by (simp add: sints_num)

 lemma sint_lt: "sint (x::'a::len word) < 2 ^ (len_of TYPE('a) - 1)"

   using word_sint.Rep [of x] by (simp add: sints_num)

 lemma sign_uint_Pls [simp]: 

   "bin_sign (uint x) = 0"

   by (simp add: sign_Pls_ge_0)

 lemma uint_m2p_neg: "uint (x::'a::len0 word) - 2 ^ len_of TYPE('a) < 0"

   by (simp only: diff_less_0_iff_less uint_lt2p)

 lemma uint_m2p_not_non_neg:

   "\<not> 0 \<le> uint (x::'a::len0 word) - 2 ^ len_of TYPE('a)"

   by (simp only: not_le uint_m2p_neg)

 lemma lt2p_lem:

   "len_of TYPE('a) \<le> n \<Longrightarrow> uint (w :: 'a::len0 word) < 2 ^ n"

   by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)

 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"

   by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])

 lemma uint_nat: "uint w = int (unat w)"

   unfolding unat_def by auto

 lemma uint_numeral:

   "uint (numeral b :: 'a :: len0 word) = numeral b mod 2 ^ len_of TYPE('a)"

   unfolding word_numeral_alt

   by (simp only: int_word_uint)

 lemma uint_neg_numeral:

   "uint (- numeral b :: 'a :: len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"

   unfolding word_neg_numeral_alt

   by (simp only: int_word_uint)

 lemma unat_numeral: 

   "unat (numeral b::'a::len0 word) = numeral b mod 2 ^ len_of TYPE ('a)"

   apply (unfold unat_def)

   apply (clarsimp simp only: uint_numeral)

   apply (rule nat_mod_distrib [THEN trans])

     apply (rule zero_le_numeral)

    apply (simp_all add: nat_power_eq)

   done

 lemma sint_numeral: "sint (numeral b :: 'a :: len word) = (numeral b + 

     2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -

     2 ^ (len_of TYPE('a) - 1)"

   unfolding word_numeral_alt by (rule int_word_sint)

 lemma word_of_int_0 [simp, code_post]:

   "word_of_int 0 = 0"

   unfolding word_0_wi ..

 lemma word_of_int_1 [simp, code_post]:

   "word_of_int 1 = 1"

   unfolding word_1_wi ..

 lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"

   by (simp add: wi_hom_syms)

 lemma word_of_int_numeral [simp] : 

   "(word_of_int (numeral bin) :: 'a :: len0 word) = (numeral bin)"

   unfolding word_numeral_alt ..

 lemma word_of_int_neg_numeral [simp]:

   "(word_of_int (- numeral bin) :: 'a :: len0 word) = (- numeral bin)"

   unfolding word_numeral_alt wi_hom_syms ..

 lemma word_int_case_wi: 

   "word_int_case f (word_of_int i :: 'b word) = 

     f (i mod 2 ^ len_of TYPE('b::len0))"

   unfolding word_int_case_def by (simp add: word_uint.eq_norm)

 lemma word_int_split: 

   "P (word_int_case f x) = 

     (ALL i. x = (word_of_int i :: 'b :: len0 word) & 

       0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"

   unfolding word_int_case_def

   by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)

 lemma word_int_split_asm: 

   "P (word_int_case f x) = 

     (~ (EX n. x = (word_of_int n :: 'b::len0 word) &

       0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"

   unfolding word_int_case_def

   by (auto simp: word_uint.eq_norm mod_pos_pos_trivial)

 lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]

 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]

 lemma uint_range_size: "0 <= uint w & uint w < 2 ^ size w"

   unfolding word_size by (rule uint_range')

 lemma sint_range_size:

   "- (2 ^ (size w - Suc 0)) <= sint w & sint w < 2 ^ (size w - Suc 0)"

   unfolding word_size by (rule sint_range')

 lemma sint_above_size: "2 ^ (size (w::'a::len word) - 1) \<le> x \<Longrightarrow> sint w < x"

   unfolding word_size by (rule less_le_trans [OF sint_lt])

 lemma sint_below_size:

   "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"

   unfolding word_size by (rule order_trans [OF _ sint_ge])

 subsection {* Testing bits *}

 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"

   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)

 lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"

   apply (unfold word_test_bit_def)

   apply (subst word_ubin.norm_Rep [symmetric])

   apply (simp only: nth_bintr word_size)

   apply fast

   done

 lemma word_eq_iff:

   fixes x y :: "'a::len0 word"

   shows "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"

   unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]

   by (metis test_bit_size [unfolded word_size])

 lemma word_eqI [rule_format]:

   fixes u :: "'a::len0 word"

   shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"

   by (simp add: word_size word_eq_iff)

 lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"

   by simp

 lemma test_bit_bin': "w !! n = (n < size w & bin_nth (uint w) n)"

   unfolding word_test_bit_def word_size

   by (simp add: nth_bintr [symmetric])

 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]

 lemma bin_nth_uint_imp:

   "bin_nth (uint (w::'a::len0 word)) n \<Longrightarrow> n < len_of TYPE('a)"

   apply (rule nth_bintr [THEN iffD1, THEN conjunct1])

   apply (subst word_ubin.norm_Rep)

   apply assumption

   done

 lemma bin_nth_sint:

   fixes w :: "'a::len word"

   shows "len_of TYPE('a) \<le> n \<Longrightarrow>

     bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"

   apply (subst word_sbin.norm_Rep [symmetric])

   apply (auto simp add: nth_sbintr)

   done

 (* type definitions theorem for in terms of equivalent bool list *)

 lemma td_bl: 

   "type_definition (to_bl :: 'a::len0 word => bool list) 

                    of_bl  

                    {bl. length bl = len_of TYPE('a)}"

   apply (unfold type_definition_def of_bl_def to_bl_def)

   apply (simp add: word_ubin.eq_norm)

   apply safe

   apply (drule sym)

   apply simp

   done

 interpretation word_bl:

   type_definition "to_bl :: 'a::len0 word => bool list"

                   of_bl  

                   "{bl. length bl = len_of TYPE('a::len0)}"

   by (fact td_bl)

 lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]

 lemma word_size_bl: "size w = size (to_bl w)"

   unfolding word_size by auto

 lemma to_bl_use_of_bl:

   "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"

   by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])

 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"

   unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)

 lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"

   unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)

 lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"

   by (metis word_rev_rev)

 lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"

   by simp

 lemma length_bl_gt_0 [iff]: "0 < length (to_bl (x::'a::len word))"

   unfolding word_bl_Rep' by (rule len_gt_0)

 lemma bl_not_Nil [iff]: "to_bl (x::'a::len word) \<noteq> []"

   by (fact length_bl_gt_0 [unfolded length_greater_0_conv])

 lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"

   by (fact length_bl_gt_0 [THEN gr_implies_not0])

 lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"

   apply (unfold to_bl_def sint_uint)

   apply (rule trans [OF _ bl_sbin_sign])

   apply simp

   done

 lemma of_bl_drop': 

   "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow> 

     of_bl (drop lend bl) = (of_bl bl :: 'a word)"

   apply (unfold of_bl_def)

   apply (clarsimp simp add : trunc_bl2bin [symmetric])

   done

 lemma test_bit_of_bl:  

   "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"

   apply (unfold of_bl_def word_test_bit_def)

   apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)

   done

 lemma no_of_bl: 

   "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) (numeral bin))"

   unfolding of_bl_def by simp

 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"

   unfolding word_size to_bl_def by auto

 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"

   unfolding uint_bl by (simp add : word_size)

 lemma to_bl_of_bin: 

   "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"

   unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)

 lemma to_bl_numeral [simp]:

   "to_bl (numeral bin::'a::len0 word) =

     bin_to_bl (len_of TYPE('a)) (numeral bin)"

   unfolding word_numeral_alt by (rule to_bl_of_bin)

 lemma to_bl_neg_numeral [simp]:

   "to_bl (- numeral bin::'a::len0 word) =

     bin_to_bl (len_of TYPE('a)) (- numeral bin)"

   unfolding word_neg_numeral_alt by (rule to_bl_of_bin)

 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"

   unfolding uint_bl by (simp add : word_size)

 lemma uint_bl_bin:

   fixes x :: "'a::len0 word"

   shows "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"

   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])

 (* naturals *)

 lemma uints_unats: "uints n = int ` unats n"

   apply (unfold unats_def uints_num)

   apply safe

   apply (rule_tac image_eqI)

   apply (erule_tac nat_0_le [symmetric])

   apply auto

   apply (erule_tac nat_less_iff [THEN iffD2])

   apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])

   apply (auto simp add : nat_power_eq int_power)

   done

 lemma unats_uints: "unats n = nat ` uints n"

   by (auto simp add : uints_unats image_iff)

 lemmas bintr_num = word_ubin.norm_eq_iff

   [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b

 lemmas sbintr_num = word_sbin.norm_eq_iff

   [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b

 lemma num_of_bintr':

   "bintrunc (len_of TYPE('a :: len0)) (numeral a) = (numeral b) \<Longrightarrow> 

     numeral a = (numeral b :: 'a word)"

   unfolding bintr_num by (erule subst, simp)

 lemma num_of_sbintr':

   "sbintrunc (len_of TYPE('a :: len) - 1) (numeral a) = (numeral b) \<Longrightarrow> 

     numeral a = (numeral b :: 'a word)"

   unfolding sbintr_num by (erule subst, simp)

 lemma num_abs_bintr:

   "(numeral x :: 'a word) =

     word_of_int (bintrunc (len_of TYPE('a::len0)) (numeral x))"

   by (simp only: word_ubin.Abs_norm word_numeral_alt)

 lemma num_abs_sbintr:

   "(numeral x :: 'a word) =

     word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))"

   by (simp only: word_sbin.Abs_norm word_numeral_alt)

 (** cast - note, no arg for new length, as it's determined by type of result,

   thus in "cast w = w, the type means cast to length of w! **)

 lemma ucast_id: "ucast w = w"

   unfolding ucast_def by auto

 lemma scast_id: "scast w = w"

   unfolding scast_def by auto

 lemma ucast_bl: "ucast w = of_bl (to_bl w)"

   unfolding ucast_def of_bl_def uint_bl

   by (auto simp add : word_size)

 lemma nth_ucast: 

   "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))"

   apply (unfold ucast_def test_bit_bin)

   apply (simp add: word_ubin.eq_norm nth_bintr word_size) 

   apply (fast elim!: bin_nth_uint_imp)

   done

 (* for literal u(s)cast *)

 lemma ucast_bintr [simp]:

   "ucast (numeral w ::'a::len0 word) = 

    word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"

   unfolding ucast_def by simp

 (* TODO: neg_numeral *)

 lemma scast_sbintr [simp]:

   "scast (numeral w ::'a::len word) = 

    word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (numeral w))"

   unfolding scast_def by simp

 lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"

   unfolding source_size_def word_size Let_def ..

 lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"

   unfolding target_size_def word_size Let_def ..

 lemma is_down:

   fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"

   shows "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"

   unfolding is_down_def source_size target_size ..

 lemma is_up:

   fixes c :: "'a::len0 word \<Rightarrow> 'b::len0 word"

   shows "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"

   unfolding is_up_def source_size target_size ..

 lemmas is_up_down = trans [OF is_up is_down [symmetric]]

 lemma down_cast_same [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"

   apply (unfold is_down)

   apply safe

   apply (rule ext)

   apply (unfold ucast_def scast_def uint_sint)

   apply (rule word_ubin.norm_eq_iff [THEN iffD1])

   apply simp

   done

 lemma word_rev_tf:

   "to_bl (of_bl bl::'a::len0 word) =

     rev (takefill False (len_of TYPE('a)) (rev bl))"

   unfolding of_bl_def uint_bl

   by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)

 lemma word_rep_drop:

   "to_bl (of_bl bl::'a::len0 word) =

     replicate (len_of TYPE('a) - length bl) False @

     drop (length bl - len_of TYPE('a)) bl"

   by (simp add: word_rev_tf takefill_alt rev_take)

 lemma to_bl_ucast: 

   "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) = 

    replicate (len_of TYPE('a) - len_of TYPE('b)) False @

    drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"

   apply (unfold ucast_bl)

   apply (rule trans)

    apply (rule word_rep_drop)

   apply simp

   done

 lemma ucast_up_app [OF refl]:

   "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow> 

     to_bl (uc w) = replicate n False @ (to_bl w)"

   by (auto simp add : source_size target_size to_bl_ucast)

 lemma ucast_down_drop [OF refl]:

   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 

     to_bl (uc w) = drop n (to_bl w)"

   by (auto simp add : source_size target_size to_bl_ucast)

 lemma scast_down_drop [OF refl]:

   "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow> 

     to_bl (sc w) = drop n (to_bl w)"

   apply (subgoal_tac "sc = ucast")

    apply safe

    apply simp

    apply (erule ucast_down_drop)

   apply (rule down_cast_same [symmetric])

   apply (simp add : source_size target_size is_down)

   done

 lemma sint_up_scast [OF refl]:

   "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"

   apply (unfold is_up)

   apply safe

   apply (simp add: scast_def word_sbin.eq_norm)

   apply (rule box_equals)

     prefer 3

     apply (rule word_sbin.norm_Rep)

    apply (rule sbintrunc_sbintrunc_l)

    defer

    apply (subst word_sbin.norm_Rep)

    apply (rule refl)

   apply simp

   done

 lemma uint_up_ucast [OF refl]:

   "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"

   apply (unfold is_up)

   apply safe

   apply (rule bin_eqI)

   apply (fold word_test_bit_def)

   apply (auto simp add: nth_ucast)

   apply (auto simp add: test_bit_bin)

   done

 lemma ucast_up_ucast [OF refl]:

   "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"

   apply (simp (no_asm) add: ucast_def)

   apply (clarsimp simp add: uint_up_ucast)

   done

 lemma scast_up_scast [OF refl]:

   "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"

   apply (simp (no_asm) add: scast_def)

   apply (clarsimp simp add: sint_up_scast)

   done

 lemma ucast_of_bl_up [OF refl]:

   "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"

   by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)

 lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]

 lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id]

 lemmas isduu = is_up_down [where c = "ucast", THEN iffD2]

 lemmas isdus = is_up_down [where c = "scast", THEN iffD2]

 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id]

 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]

 lemma up_ucast_surj:

   "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 

    surj (ucast :: 'a word => 'b word)"

   by (rule surjI, erule ucast_up_ucast_id)

 lemma up_scast_surj:

   "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 

    surj (scast :: 'a word => 'b word)"

   by (rule surjI, erule scast_up_scast_id)

 lemma down_scast_inj:

   "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow> 

    inj_on (ucast :: 'a word => 'b word) A"

   by (rule inj_on_inverseI, erule scast_down_scast_id)

 lemma down_ucast_inj:

   "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow> 

    inj_on (ucast :: 'a word => 'b word) A"

   by (rule inj_on_inverseI, erule ucast_down_ucast_id)

 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"

   by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)

 lemma ucast_down_wi [OF refl]:

   "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x"

   apply (unfold is_down)

   apply (clarsimp simp add: ucast_def word_ubin.eq_norm)

   apply (rule word_ubin.norm_eq_iff [THEN iffD1])

   apply (erule bintrunc_bintrunc_ge)

   done

 lemma ucast_down_no [OF refl]:

   "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin"

   unfolding word_numeral_alt by clarify (rule ucast_down_wi)

 lemma ucast_down_bl [OF refl]:

   "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"

   unfolding of_bl_def by clarify (erule ucast_down_wi)

 lemmas slice_def' = slice_def [unfolded word_size]

 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]

 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def

 subsection {* Word Arithmetic *}

 lemma word_less_alt: "(a < b) = (uint a < uint b)"

   by (fact word_less_def)

 lemma signed_linorder: "class.linorder word_sle word_sless"

   by default (unfold word_sle_def word_sless_def, auto)

 interpretation signed: linorder "word_sle" "word_sless"

   by (rule signed_linorder)

 lemma udvdI: 

   "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"

   by (auto simp: udvd_def)

 lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b

 lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b

 lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b

 lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b

 lemmas word_sless_no [simp] = word_sless_def [of "numeral a" "numeral b"] for a b

 lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b

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

   using word_neg_numeral_alt [of Num.One] by simp

 lemma word_0_bl [simp]: "of_bl [] = 0"

   unfolding of_bl_def by simp

 lemma word_1_bl: "of_bl [True] = 1" 

   unfolding of_bl_def by (simp add: bl_to_bin_def)

 lemma uint_eq_0 [simp]: "uint 0 = 0"

   unfolding word_0_wi word_ubin.eq_norm by simp

 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"

   by (simp add: of_bl_def bl_to_bin_rep_False)

 lemma to_bl_0 [simp]:

   "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"

   unfolding uint_bl

   by (simp add: word_size bin_to_bl_zero)

 lemma uint_0_iff:

   "uint x = 0 \<longleftrightarrow> x = 0"

   by (simp add: word_uint_eq_iff)

 lemma unat_0_iff:

   "unat x = 0 \<longleftrightarrow> x = 0"

   unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)

 lemma unat_0 [simp]:

   "unat 0 = 0"

   unfolding unat_def by auto

 lemma size_0_same':

   "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"

   apply (unfold word_size)

   apply (rule box_equals)

     defer

     apply (rule word_uint.Rep_inverse)+

   apply (rule word_ubin.norm_eq_iff [THEN iffD1])

   apply simp

   done

 lemmas size_0_same = size_0_same' [unfolded word_size]

 lemmas unat_eq_0 = unat_0_iff

 lemmas unat_eq_zero = unat_0_iff

 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"

 by (auto simp: unat_0_iff [symmetric])

 lemma ucast_0 [simp]: "ucast 0 = 0"

   unfolding ucast_def by simp

 lemma sint_0 [simp]: "sint 0 = 0"

   unfolding sint_uint by simp

 lemma scast_0 [simp]: "scast 0 = 0"

   unfolding scast_def by simp

 lemma sint_n1 [simp] : "sint (- 1) = - 1"

   unfolding word_m1_wi word_sbin.eq_norm by simp

 lemma scast_n1 [simp]: "scast (- 1) = - 1"

   unfolding scast_def by simp

 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"

   by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))

 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"

   unfolding unat_def by simp

 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"

   unfolding ucast_def by simp

 (* now, to get the weaker results analogous to word_div/mod_def *)

 subsection {* Transferring goals from words to ints *}

 lemma word_ths:  

   shows

   word_succ_p1:   "word_succ a = a + 1" and

   word_pred_m1:   "word_pred a = a - 1" and

   word_pred_succ: "word_pred (word_succ a) = a" and

   word_succ_pred: "word_succ (word_pred a) = a" and

   word_mult_succ: "word_succ a * b = b + a * b"

   by (transfer, simp add: algebra_simps)+

 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"

   by simp

 lemma uint_word_ariths:

   fixes a b :: "'a::len0 word"

   shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"

     and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"

     and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"

     and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"

     and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"

     and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"

     and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"

     and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"

   by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])

 lemma uint_word_arith_bintrs:

   fixes a b :: "'a::len0 word"

   shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"

     and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"

     and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"

     and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"

     and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"

     and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"

     and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"

     and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"

   by (simp_all add: uint_word_ariths bintrunc_mod2p)

 lemma sint_word_ariths:

   fixes a b :: "'a::len word"

   shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"

     and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"

     and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"

     and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"

     and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"

     and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"

     and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"

     and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"

   by (simp_all add: uint_word_arith_bintrs

     [THEN uint_sint [symmetric, THEN trans],

     unfolded uint_sint bintr_arith1s bintr_ariths 

       len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep])

 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]

 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]

 lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"

   unfolding word_pred_m1 by simp

 lemma succ_pred_no [simp]:

   "word_succ (numeral w) = numeral w + 1"

   "word_pred (numeral w) = numeral w - 1"

   "word_succ (- numeral w) = - numeral w + 1"

   "word_pred (- numeral w) = - numeral w - 1"

   unfolding word_succ_p1 word_pred_m1 by simp_all

 lemma word_sp_01 [simp] : 

   "word_succ (- 1) = 0 & word_succ 0 = 1 & word_pred 0 = - 1 & word_pred 1 = 0"

   unfolding word_succ_p1 word_pred_m1 by simp_all

 (* alternative approach to lifting arithmetic equalities *)

 lemma word_of_int_Ex:

   "\<exists>y. x = word_of_int y"

   by (rule_tac x="uint x" in exI) simp

 subsection {* Order on fixed-length words *}

 lemma word_zero_le [simp] :

   "0 <= (y :: 'a :: len0 word)"

   unfolding word_le_def by auto

 lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)

   unfolding word_le_def

   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto

 lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"

   unfolding word_le_def

   by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto

 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 \<longleftrightarrow> 0 \<noteq> (y :: 'a :: len0 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 <s b) = (sint a < sint b)"

   unfolding word_sle_def word_sless_def

   by (auto simp add: less_le)

 lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"

   unfolding unat_def word_le_def

   by (rule nat_le_eq_zle [symmetric]) simp

 lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"

   unfolding unat_def word_less_alt

   by (rule nat_less_eq_zless [symmetric]) simp

 lemma wi_less: 

   "(word_of_int n < (word_of_int m :: 'a :: len0 word)) = 

     (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"

   unfolding word_less_alt by (simp add: word_uint.eq_norm)

 lemma wi_le: 

   "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = 

     (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"

   unfolding word_le_def by (simp add: word_uint.eq_norm)

 lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"

   apply (unfold udvd_def)

   apply safe

    apply (simp add: unat_def nat_mult_distrib)

   apply (simp add: uint_nat int_mult)

   apply (rule exI)

   apply safe

    prefer 2

    apply (erule notE)

    apply (rule refl)

   apply force

   done

 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"

   unfolding dvd_def udvd_nat_alt by force

 lemmas unat_mono = word_less_nat_alt [THEN iffD1]

 lemma unat_minus_one:

   assumes "w \<noteq> 0"

   shows "unat (w - 1) = unat w - 1"

 proof -

   have "0 \<le> uint w" by (fact uint_nonnegative)

   moreover from assms have "0 \<noteq> uint w" by (simp add: uint_0_iff)

   ultimately have "1 \<le> uint w" by arith

   from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)" by arith

   with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"

     by (auto intro: mod_pos_pos_trivial)

   with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"

     by auto

   then show ?thesis

     by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq [symmetric])

 qed

 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"

   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])

 lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]

 lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]

 lemma uint_sub_lt2p [simp]: 

   "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) < 

     2 ^ len_of TYPE('a)"

   using uint_ge_0 [of y] uint_lt2p [of x] by arith

 subsection {* Conditions for the addition (etc) of two words to overflow *}

 lemma uint_add_lem: 

   "(uint x + uint y < 2 ^ len_of TYPE('a)) = 

     (uint (x + y :: 'a :: len0 word) = uint x + uint y)"

   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])

 lemma uint_mult_lem: 

   "(uint x * uint y < 2 ^ len_of TYPE('a)) = 

     (uint (x * y :: 'a :: len0 word) = uint x * uint y)"

   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])

 lemma uint_sub_lem: 

   "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"

   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])

 lemma uint_add_le: "uint (x + y) <= uint x + uint y"

   unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)

 lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"

   unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)

 lemma mod_add_if_z:

   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 

    (x + y) mod z = (if x + y < z then x + y else x + y - z)"

   by (auto intro: int_mod_eq)

 lemma uint_plus_if':

   "uint ((a::'a word) + b) =

   (if uint a + uint b < 2 ^ len_of TYPE('a::len0) then uint a + uint b

    else uint a + uint b - 2 ^ len_of TYPE('a))"

   using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)

 lemma mod_sub_if_z:

   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 

    (x - y) mod z = (if y <= x then x - y else x - y + z)"

   by (auto intro: int_mod_eq)

 lemma uint_sub_if':

   "uint ((a::'a word) - b) =

   (if uint b \<le> uint a then uint a - uint b

    else uint a - uint b + 2 ^ len_of TYPE('a::len0))"

   using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)

 subsection {* Definition of @{text uint_arith} *}

 lemma word_of_int_inverse:

   "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> 

    uint (a::'a::len0 word) = r"

   apply (erule word_uint.Abs_inverse' [rotated])

   apply (simp add: uints_num)

   done

 lemma uint_split:

   fixes x::"'a::len0 word"

   shows "P (uint x) = 

          (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"

   apply (fold word_int_case_def)

   apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial

               split: word_int_split)

   done

 lemma uint_split_asm:

   fixes x::"'a::len0 word"

   shows "P (uint x) = 

          (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"

   by (auto dest!: word_of_int_inverse 

            simp: int_word_uint mod_pos_pos_trivial

            split: uint_split)

 lemmas uint_splits = uint_split uint_split_asm

 lemmas uint_arith_simps = 

   word_le_def word_less_alt

   word_uint.Rep_inject [symmetric] 

   uint_sub_if' uint_plus_if'

 (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)

 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" 

   by auto

 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)

 ML {*

 fun uint_arith_simpset ctxt = 

   ctxt addsimps @{thms uint_arith_simps}

      delsimps @{thms word_uint.Rep_inject}

      |> fold Splitter.add_split @{thms split_if_asm}

      |> fold Simplifier.add_cong @{thms power_False_cong}

 fun uint_arith_tacs ctxt = 

   let

     fun arith_tac' n t =

       Arith_Data.verbose_arith_tac ctxt n t

         handle Cooper.COOPER _ => Seq.empty;

   in 

     [ clarify_tac ctxt 1,

       full_simp_tac (uint_arith_simpset ctxt) 1,

       ALLGOALS (full_simp_tac

         (put_simpset HOL_ss ctxt

           |> fold Splitter.add_split @{thms uint_splits}

           |> fold Simplifier.add_cong @{thms power_False_cong})),

       rewrite_goals_tac ctxt @{thms word_size}, 

       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      

                          REPEAT (etac conjE n) THEN

                          REPEAT (dtac @{thm word_of_int_inverse} n 

                                  THEN assume_tac ctxt n 

                                  THEN assume_tac ctxt n)),

       TRYALL arith_tac' ]

   end

 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))

 *}

 method_setup uint_arith = 

   {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}

   "solving word arithmetic via integers and arith"

 subsection {* More on overflows and monotonicity *}

 lemma no_plus_overflow_uint_size: 

   "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"

   unfolding word_size by uint_arith

 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]

 lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"

   by uint_arith

 lemma no_olen_add':

   fixes x :: "'a::len0 word"

   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"

   by (simp add: ac_simps no_olen_add)

 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]

 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem]

 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1]

 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem]

 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]

 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]

 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]

 lemma word_less_sub1: 

   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"

   by uint_arith

 lemma word_le_sub1: 

   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"

   by uint_arith

 lemma sub_wrap_lt: 

   "((x :: 'a :: len0 word) < x - z) = (x < z)"

   by uint_arith

 lemma sub_wrap: 

   "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"

   by uint_arith

 lemma plus_minus_not_NULL_ab: 

   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"

   by uint_arith

 lemma plus_minus_no_overflow_ab: 

   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c" 

   by uint_arith

 lemma le_minus': 

   "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"

   by uint_arith

 lemma le_plus': 

   "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"

   by uint_arith

 lemmas le_plus = le_plus' [rotated]

 lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)

 lemma word_plus_mono_right: 

   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"

   by uint_arith

 lemma word_less_minus_cancel: 

   "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"

   by uint_arith

 lemma word_less_minus_mono_left: 

   "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"

   by uint_arith

 lemma word_less_minus_mono:  

   "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c 

   \<Longrightarrow> a - b < c - (d::'a::len word)"

   by uint_arith

 lemma word_le_minus_cancel: 

   "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"

   by uint_arith

 lemma word_le_minus_mono_left: 

   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"

   by uint_arith

 lemma word_le_minus_mono:  

   "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c 

   \<Longrightarrow> a - b <= c - (d::'a::len word)"

   by uint_arith

 lemma plus_le_left_cancel_wrap: 

   "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"

   by uint_arith

 lemma plus_le_left_cancel_nowrap: 

   "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow> 

     (x + y' < x + y) = (y' < y)" 

   by uint_arith

 lemma word_plus_mono_right2: 

   "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"

   by uint_arith

 lemma word_less_add_right: 

   "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"

   by uint_arith

 lemma word_less_sub_right: 

   "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"

   by uint_arith

 lemma word_le_plus_either: 

   "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"

   by uint_arith

 lemma word_less_nowrapI: 

   "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"

   by uint_arith

 lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"

   by uint_arith

 lemma inc_i: 

   "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"

   by uint_arith

 lemma udvd_incr_lem:

   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 

     uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"

   apply clarsimp

   apply (drule less_le_mult)

   apply safe

   done

 lemma udvd_incr': 

   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 

     uint q = ua + n' * uint K \<Longrightarrow> p + K <= q" 

   apply (unfold word_less_alt word_le_def)

   apply (drule (2) udvd_incr_lem)

   apply (erule uint_add_le [THEN order_trans])

   done

 lemma udvd_decr': 

   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 

     uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"

   apply (unfold word_less_alt word_le_def)

   apply (drule (2) udvd_incr_lem)

   apply (drule le_diff_eq [THEN iffD2])

   apply (erule order_trans)

   apply (rule uint_sub_ge)

   done

 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]

 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]

 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]

 lemma udvd_minus_le': 

   "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"

   apply (unfold udvd_def)

   apply clarify

   apply (erule (2) udvd_decr0)

   done

 lemma udvd_incr2_K: 

   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 

     0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"

   using [[simproc del: linordered_ring_less_cancel_factor]]

   apply (unfold udvd_def)

   apply clarify

   apply (simp add: uint_arith_simps split: split_if_asm)

    prefer 2 

    apply (insert uint_range' [of s])[1]

    apply arith

   apply (drule add.commute [THEN xtr1])

   apply (simp add: diff_less_eq [symmetric])

   apply (drule less_le_mult)

    apply arith

   apply simp

   done

 (* links with rbl operations *)

 lemma word_succ_rbl:

   "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"

   apply (unfold word_succ_def)

   apply clarify

   apply (simp add: to_bl_of_bin)

   apply (simp add: to_bl_def rbl_succ)

   done

 lemma word_pred_rbl:

   "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"

   apply (unfold word_pred_def)

   apply clarify

   apply (simp add: to_bl_of_bin)

   apply (simp add: to_bl_def rbl_pred)

   done

 lemma word_add_rbl:

   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 

     to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"

   apply (unfold word_add_def)

   apply clarify

   apply (simp add: to_bl_of_bin)

   apply (simp add: to_bl_def rbl_add)

   done

 lemma word_mult_rbl:

   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 

     to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"

   apply (unfold word_mult_def)

   apply clarify

   apply (simp add: to_bl_of_bin)

   apply (simp add: to_bl_def rbl_mult)

   done

 lemma rtb_rbl_ariths:

   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"

   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"

   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"

   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"

   by (auto simp: rev_swap [symmetric] word_succ_rbl 

                  word_pred_rbl word_mult_rbl word_add_rbl)

 subsection {* Arithmetic type class instantiations *}

 lemmas word_le_0_iff [simp] =

   word_zero_le [THEN leD, THEN linorder_antisym_conv1]

 lemma word_of_int_nat: 

   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"

   by (simp add: of_nat_nat word_of_int)

 (* note that iszero_def is only for class comm_semiring_1_cancel,

    which requires word length >= 1, ie 'a :: len word *) 

 lemma iszero_word_no [simp]:

   "iszero (numeral bin :: 'a :: len word) = 

     iszero (bintrunc (len_of TYPE('a)) (numeral bin))"

   using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]

   by (simp add: iszero_def [symmetric])

 text {* Use @{text iszero} to simplify equalities between word numerals. *}

 lemmas word_eq_numeral_iff_iszero [simp] =

   eq_numeral_iff_iszero [where 'a="'a::len word"]

 subsection {* Word and nat *}

 lemma td_ext_unat [OF refl]:

   "n = len_of TYPE ('a :: len) \<Longrightarrow> 

     td_ext (unat :: 'a word => nat) of_nat 

     (unats n) (%i. i mod 2 ^ n)"

   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)

   apply (auto intro!: imageI simp add : word_of_int_hom_syms)

   apply (erule word_uint.Abs_inverse [THEN arg_cong])

   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)

   done

 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]

 interpretation word_unat:

   td_ext "unat::'a::len word => nat" 

          of_nat 

          "unats (len_of TYPE('a::len))"

          "%i. i mod 2 ^ len_of TYPE('a::len)"

   by (rule td_ext_unat)

 lemmas td_unat = word_unat.td_thm

 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]

 lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"

   apply (unfold unats_def)

   apply clarsimp

   apply (rule xtrans, rule unat_lt2p, assumption) 

   done

 lemma word_nchotomy:

   "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"

   apply (rule allI)

   apply (rule word_unat.Abs_cases)

   apply (unfold unats_def)

   apply auto

   done

 lemma of_nat_eq:

   fixes w :: "'a::len word"

   shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"

   apply (rule trans)

    apply (rule word_unat.inverse_norm)

   apply (rule iffI)

    apply (rule mod_eqD)

    apply simp

   apply clarsimp

   done

 lemma of_nat_eq_size: 

   "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"

   unfolding word_size by (rule of_nat_eq)

 lemma of_nat_0:

   "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"

   by (simp add: of_nat_eq)

 lemma of_nat_2p [simp]:

   "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"

   by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])

 lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"

   by (cases k) auto

 lemma of_nat_neq_0: 

   "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"

   by (clarsimp simp add : of_nat_0)

 lemma Abs_fnat_hom_add:

   "of_nat a + of_nat b = of_nat (a + b)"

   by simp

 lemma Abs_fnat_hom_mult:

   "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"

   by (simp add: word_of_nat wi_hom_mult zmult_int)

 lemma Abs_fnat_hom_Suc:

   "word_succ (of_nat a) = of_nat (Suc a)"

   by (simp add: word_of_nat wi_hom_succ ac_simps)

 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"

   by simp

 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"

   by simp

 lemmas Abs_fnat_homs = 

   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 

   Abs_fnat_hom_0 Abs_fnat_hom_1

 lemma word_arith_nat_add:

   "a + b = of_nat (unat a + unat b)" 

   by simp

 lemma word_arith_nat_mult:

   "a * b = of_nat (unat a * unat b)"

   by (simp add: of_nat_mult)

 lemma word_arith_nat_Suc:

   "word_succ a = of_nat (Suc (unat a))"

   by (subst Abs_fnat_hom_Suc [symmetric]) simp

 lemma word_arith_nat_div:

   "a div b = of_nat (unat a div unat b)"

   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)

 lemma word_arith_nat_mod:

   "a mod b = of_nat (unat a mod unat b)"

   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)

 lemmas word_arith_nat_defs =

   word_arith_nat_add word_arith_nat_mult

   word_arith_nat_Suc Abs_fnat_hom_0

   Abs_fnat_hom_1 word_arith_nat_div

   word_arith_nat_mod 

 lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"

   by simp

 lemmas unat_word_ariths = word_arith_nat_defs

   [THEN trans [OF unat_cong unat_of_nat]]

 lemmas word_sub_less_iff = word_sub_le_iff

   [unfolded linorder_not_less [symmetric] Not_eq_iff]

 lemma unat_add_lem: 

   "(unat x + unat y < 2 ^ len_of TYPE('a)) = 

     (unat (x + y :: 'a :: len word) = unat x + unat y)"

   unfolding unat_word_ariths

   by (auto intro!: trans [OF _ nat_mod_lem])

 lemma unat_mult_lem: 

   "(unat x * unat y < 2 ^ len_of TYPE('a)) = 

     (unat (x * y :: 'a :: len word) = unat x * unat y)"

   unfolding unat_word_ariths

   by (auto intro!: trans [OF _ nat_mod_lem])

 lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]

 lemma le_no_overflow: 

   "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"

   apply (erule order_trans)

   apply (erule olen_add_eqv [THEN iffD1])

   done

 lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]

 lemma unat_sub_if_size:

   "unat (x - y) = (if unat y <= unat x 

    then unat x - unat y 

    else unat x + 2 ^ size x - unat y)"

   apply (unfold word_size)

   apply (simp add: un_ui_le)

   apply (auto simp add: unat_def uint_sub_if')

    apply (rule nat_diff_distrib)

     prefer 3

     apply (simp add: algebra_simps)

     apply (rule nat_diff_distrib [THEN trans])

       prefer 3

       apply (subst nat_add_distrib)

         prefer 3

         apply (simp add: nat_power_eq)

        apply auto

   apply uint_arith

   done

 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]

 lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"

   apply (simp add : unat_word_ariths)

   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])

   apply (rule div_le_dividend)

   done

 lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"

   apply (clarsimp simp add : unat_word_ariths)

   apply (cases "unat y")

    prefer 2

    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])

    apply (rule mod_le_divisor)

    apply auto

   done

 lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"

   unfolding uint_nat by (simp add : unat_div zdiv_int)

 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"

   unfolding uint_nat by (simp add : unat_mod zmod_int)

 subsection {* Definition of @{text unat_arith} tactic *}

 lemma unat_split:

   fixes x::"'a::len word"

   shows "P (unat x) = 

          (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"

   by (auto simp: unat_of_nat)

 lemma unat_split_asm:

   fixes x::"'a::len word"

   shows "P (unat x) = 

          (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"

   by (auto simp: unat_of_nat)

 lemmas of_nat_inverse = 

   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]

 lemmas unat_splits = unat_split unat_split_asm

 lemmas unat_arith_simps =

   word_le_nat_alt word_less_nat_alt

   word_unat.Rep_inject [symmetric]

   unat_sub_if' unat_plus_if' unat_div unat_mod

 (* unat_arith_tac: tactic to reduce word arithmetic to nat, 

    try to solve via arith *)

 ML {*

 fun unat_arith_simpset ctxt = 

   ctxt addsimps @{thms unat_arith_simps}

      delsimps @{thms word_unat.Rep_inject}

      |> fold Splitter.add_split @{thms split_if_asm}

      |> fold Simplifier.add_cong @{thms power_False_cong}

 fun unat_arith_tacs ctxt =   

   let

     fun arith_tac' n t =

       Arith_Data.verbose_arith_tac ctxt n t

         handle Cooper.COOPER _ => Seq.empty;

   in 

     [ clarify_tac ctxt 1,

       full_simp_tac (unat_arith_simpset ctxt) 1,

       ALLGOALS (full_simp_tac

         (put_simpset HOL_ss ctxt

           |> fold Splitter.add_split @{thms unat_splits}

           |> fold Simplifier.add_cong @{thms power_False_cong})),

       rewrite_goals_tac ctxt @{thms word_size}, 

       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      

                          REPEAT (etac conjE n) THEN

                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),

       TRYALL arith_tac' ] 

   end

 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))

 *}

 method_setup unat_arith = 

   {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}

   "solving word arithmetic via natural numbers and arith"

 lemma no_plus_overflow_unat_size: 

   "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 

   unfolding word_size by unat_arith

 lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]

 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]

 lemma word_div_mult: 

   "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> 

     x * y div y = x"

   apply unat_arith

   apply clarsimp

   apply (subst unat_mult_lem [THEN iffD1])

   apply auto

   done

 lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow> 

     unat i * unat x < 2 ^ len_of TYPE('a)"

   apply unat_arith

   apply clarsimp

   apply (drule mult_le_mono1)

   apply (erule order_le_less_trans)

   apply (rule xtr7 [OF unat_lt2p div_mult_le])

   done

 lemmas div_lt'' = order_less_imp_le [THEN div_lt']

 lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"

   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])

   apply (simp add: unat_arith_simps)

   apply (drule (1) mult_less_mono1)

   apply (erule order_less_le_trans)

   apply (rule div_mult_le)

   done

 lemma div_le_mult: 

   "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"

   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])

   apply (simp add: unat_arith_simps)

   apply (drule mult_le_mono1)

   apply (erule order_trans)

   apply (rule div_mult_le)

   done

 lemma div_lt_uint': 

   "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"

   apply (unfold uint_nat)

   apply (drule div_lt')

   apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 

                    nat_power_eq)

   done

 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']

 lemma word_le_exists': 

   "(x :: 'a :: len0 word) <= y \<Longrightarrow> 

     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"

   apply (rule exI)

   apply (rule conjI)

   apply (rule zadd_diff_inverse)

   apply uint_arith

   done

 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]

 lemmas plus_minus_no_overflow =

   order_less_imp_le [THEN plus_minus_no_overflow_ab]

 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left

   word_le_minus_cancel word_le_minus_mono_left

 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x

 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x

 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x

 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]

 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]

 lemma thd1:

   "a div b * b \<le> (a::nat)"

   using gt_or_eq_0 [of b]

   apply (rule disjE)

    apply (erule xtr4 [OF thd mult.commute])

   apply clarsimp

   done

 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1 

 lemma word_mod_div_equality:

   "(n div b) * b + (n mod b) = (n :: 'a :: len word)"

   apply (unfold word_less_nat_alt word_arith_nat_defs)

   apply (cut_tac y="unat b" in gt_or_eq_0)

   apply (erule disjE)

    apply (simp add: mod_div_equality uno_simps)

   apply simp

   done

 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"

   apply (unfold word_le_nat_alt word_arith_nat_defs)

   apply (cut_tac y="unat b" in gt_or_eq_0)

   apply (erule disjE)

    apply (simp add: div_mult_le uno_simps)

   apply simp

   done

 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"

   apply (simp only: word_less_nat_alt word_arith_nat_defs)

   apply (clarsimp simp add : uno_simps)

   done

 lemma word_of_int_power_hom: 

   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"

   by (induct n) (simp_all add: wi_hom_mult [symmetric])

 lemma word_arith_power_alt: 

   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"

   by (simp add : word_of_int_power_hom [symmetric])

 lemma of_bl_length_less: 

   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"

   apply (unfold of_bl_def word_less_alt word_numeral_alt)

   apply safe

   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 

                        del: word_of_int_numeral)

   apply (simp add: mod_pos_pos_trivial)

   apply (subst mod_pos_pos_trivial)

     apply (rule bl_to_bin_ge0)

    apply (rule order_less_trans)

     apply (rule bl_to_bin_lt2p)

    apply simp

   apply (rule bl_to_bin_lt2p)

   done

 subsection {* Cardinality, finiteness of set of words *}

 instance word :: (len0) finite

   by (default, simp add: type_definition.univ [OF type_definition_word])

 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"

   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)

 lemma card_word_size: 

   "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"

 unfolding word_size by (rule card_word)

 subsection {* Bitwise Operations on Words *}

 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or

 (* following definitions require both arithmetic and bit-wise word operations *)

 (* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)

 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],

   folded word_ubin.eq_norm, THEN eq_reflection]

 (* the binary operations only *)

 (* BH: why is this needed? *)

 lemmas word_log_binary_defs = 

   word_and_def word_or_def word_xor_def

 lemma word_wi_log_defs:

   "NOT word_of_int a = word_of_int (NOT a)"

   "word_of_int a AND word_of_int b = word_of_int (a AND b)"

   "word_of_int a OR word_of_int b = word_of_int (a OR b)"

   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"

   by (transfer, rule refl)+

 lemma word_no_log_defs [simp]:

   "NOT (numeral a) = word_of_int (NOT (numeral a))"

   "NOT (- numeral a) = word_of_int (NOT (- numeral a))"

   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"

   "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"

   "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"

   "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"

   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"

   "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"

   "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"

   "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"

   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"

   "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"

   "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"

   "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"

   by (transfer, rule refl)+

 text {* Special cases for when one of the arguments equals 1. *}

 lemma word_bitwise_1_simps [simp]:

   "NOT (1::'a::len0 word) = -2"

   "1 AND numeral b = word_of_int (1 AND numeral b)"

   "1 AND - numeral b = word_of_int (1 AND - numeral b)"

   "numeral a AND 1 = word_of_int (numeral a AND 1)"

   "- numeral a AND 1 = word_of_int (- numeral a AND 1)"

   "1 OR numeral b = word_of_int (1 OR numeral b)"

   "1 OR - numeral b = word_of_int (1 OR - numeral b)"

   "numeral a OR 1 = word_of_int (numeral a OR 1)"

   "- numeral a OR 1 = word_of_int (- numeral a OR 1)"

   "1 XOR numeral b = word_of_int (1 XOR numeral b)"

   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"

   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"

   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"

   by (transfer, simp)+

 text {* Special cases for when one of the arguments equals -1. *}

 lemma word_bitwise_m1_simps [simp]:

   "NOT (-1::'a::len0 word) = 0"

   "(-1::'a::len0 word) AND x = x"

   "x AND (-1::'a::len0 word) = x"

   "(-1::'a::len0 word) OR x = -1"

   "x OR (-1::'a::len0 word) = -1"

   " (-1::'a::len0 word) XOR x = NOT x"

   "x XOR (-1::'a::len0 word) = NOT x"

   by (transfer, simp)+

 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"

   by (transfer, simp add: bin_trunc_ao)

 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"

   by (transfer, simp add: bin_trunc_ao)

 lemma test_bit_wi [simp]:

   "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"

   unfolding word_test_bit_def

   by (simp add: word_ubin.eq_norm nth_bintr)

 lemma word_test_bit_transfer [transfer_rule]:

   "(rel_fun pcr_word (rel_fun op = op =))

     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"

   unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp

 lemma word_ops_nth_size:

   "n < size (x::'a::len0 word) \<Longrightarrow> 

     (x OR y) !! n = (x !! n | y !! n) & 

     (x AND y) !! n = (x !! n & y !! n) & 

     (x XOR y) !! n = (x !! n ~= y !! n) & 

     (NOT x) !! n = (~ x !! n)"

   unfolding word_size by transfer (simp add: bin_nth_ops)

 lemma word_ao_nth:

   fixes x :: "'a::len0 word"

   shows "(x OR y) !! n = (x !! n | y !! n) & 

          (x AND y) !! n = (x !! n & y !! n)"

   by transfer (auto simp add: bin_nth_ops)

 lemma test_bit_numeral [simp]:

   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>

     n < len_of TYPE('a) \<and> bin_nth (numeral w) n"

   by transfer (rule refl)

 lemma test_bit_neg_numeral [simp]:

   "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>

     n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"

   by transfer (rule refl)

 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"

   by transfer auto

 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"

   by transfer simp

 lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"

   by transfer simp

 (* get from commutativity, associativity etc of int_and etc

   to same for word_and etc *)

 lemmas bwsimps = 

   wi_hom_add

   word_wi_log_defs

 lemma word_bw_assocs:

   fixes x :: "'a::len0 word"

   shows

   "(x AND y) AND z = x AND y AND z"

   "(x OR y) OR z = x OR y OR z"

   "(x XOR y) XOR z = x XOR y XOR z"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_bw_comms:

   fixes x :: "'a::len0 word"

   shows

   "x AND y = y AND x"

   "x OR y = y OR x"

   "x XOR y = y XOR x"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_bw_lcs:

   fixes x :: "'a::len0 word"

   shows

   "y AND x AND z = x AND y AND z"

   "y OR x OR z = x OR y OR z"

   "y XOR x XOR z = x XOR y XOR z"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_log_esimps [simp]:

   fixes x :: "'a::len0 word"

   shows

   "x AND 0 = 0"

   "x AND -1 = x"

   "x OR 0 = x"

   "x OR -1 = -1"

   "x XOR 0 = x"

   "x XOR -1 = NOT x"

   "0 AND x = 0"

   "-1 AND x = x"

   "0 OR x = x"

   "-1 OR x = -1"

   "0 XOR x = x"

   "-1 XOR x = NOT x"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_not_dist:

   fixes x :: "'a::len0 word"

   shows

   "NOT (x OR y) = NOT x AND NOT y"

   "NOT (x AND y) = NOT x OR NOT y"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_bw_same:

   fixes x :: "'a::len0 word"

   shows

   "x AND x = x"

   "x OR x = x"

   "x XOR x = 0"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_ao_absorbs [simp]:

   fixes x :: "'a::len0 word"

   shows

   "x AND (y OR x) = x"

   "x OR y AND x = x"

   "x AND (x OR y) = x"

   "y AND x OR x = x"

   "(y OR x) AND x = x"

   "x OR x AND y = x"

   "(x OR y) AND x = x"

   "x AND y OR x = x"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_not_not [simp]:

   "NOT NOT (x::'a::len0 word) = x"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_ao_dist:

   fixes x :: "'a::len0 word"

   shows "(x OR y) AND z = x AND z OR y AND z"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_oa_dist:

   fixes x :: "'a::len0 word"

   shows "x AND y OR z = (x OR z) AND (y OR z)"

   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])

 lemma word_add_not [simp]: 

   fixes x :: "'a::len0 word"

   shows "x + NOT x = -1"

   by transfer (simp add: bin_add_not)

 lemma word_plus_and_or [simp]:

   fixes x :: "'a::len0 word"

   shows "(x AND y) + (x OR y) = x + y"

   by transfer (simp add: plus_and_or)

 lemma leoa:   

   fixes x :: "'a::len0 word"

   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto

 lemma leao: 

   fixes x' :: "'a::len0 word"

   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 

 lemma word_ao_equiv:

   fixes w w' :: "'a::len0 word"

   shows "(w = w OR w') = (w' = w AND w')"

   by (auto intro: leoa leao)

 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"

   unfolding word_le_def uint_or

   by (auto intro: le_int_or) 

 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]

 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]

 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]

 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 

   unfolding to_bl_def word_log_defs bl_not_bin

   by (simp add: word_ubin.eq_norm)

 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 

   unfolding to_bl_def word_log_defs bl_xor_bin

   by (simp add: word_ubin.eq_norm)

 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 

   unfolding to_bl_def word_log_defs bl_or_bin

   by (simp add: word_ubin.eq_norm)

 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 

   unfolding to_bl_def word_log_defs bl_and_bin

   by (simp add: word_ubin.eq_norm)

 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"

   by (auto simp: word_test_bit_def word_lsb_def)

 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"

   unfolding word_lsb_def uint_eq_0 uint_1 by simp

 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"

   apply (unfold word_lsb_def uint_bl bin_to_bl_def) 

   apply (rule_tac bin="uint w" in bin_exhaust)

   apply (cases "size w")

    apply auto

    apply (auto simp add: bin_to_bl_aux_alt)

   done

 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"

   unfolding word_lsb_def bin_last_def by auto

 lemma word_msb_sint: "msb w = (sint w < 0)" 

   unfolding word_msb_def sign_Min_lt_0 ..

 lemma msb_word_of_int:

   "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"

   unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)

 lemma word_msb_numeral [simp]:

   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"

   unfolding word_numeral_alt by (rule msb_word_of_int)

 lemma word_msb_neg_numeral [simp]:

   "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"

   unfolding word_neg_numeral_alt by (rule msb_word_of_int)

 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"

   unfolding word_msb_def by simp

 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"

   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]

   by (simp add: Suc_le_eq)

 lemma word_msb_nth:

   "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"

   unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)

 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"

   apply (unfold word_msb_nth uint_bl)

   apply (subst hd_conv_nth)

   apply (rule length_greater_0_conv [THEN iffD1])

    apply simp

   apply (simp add : nth_bin_to_bl word_size)

   done

 lemma word_set_nth [simp]:

   "set_bit w n (test_bit w n) = (w::'a::len0 word)"

   unfolding word_test_bit_def word_set_bit_def by auto

 lemma bin_nth_uint':

   "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"

   apply (unfold word_size)

   apply (safe elim!: bin_nth_uint_imp)

    apply (frule bin_nth_uint_imp)

    apply (fast dest!: bin_nth_bl)+

   done

 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]

 lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"

   unfolding to_bl_def word_test_bit_def word_size

   by (rule bin_nth_uint)

 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"

   apply (unfold test_bit_bl)

   apply clarsimp

   apply (rule trans)

    apply (rule nth_rev_alt)

    apply (auto simp add: word_size)

   done

 lemma test_bit_set: 

   fixes w :: "'a::len0 word"

   shows "(set_bit w n x) !! n = (n < size w & x)"

   unfolding word_size word_test_bit_def word_set_bit_def

   by (clarsimp simp add : word_ubin.eq_norm nth_bintr)

 lemma test_bit_set_gen: 

   fixes w :: "'a::len0 word"

   shows "test_bit (set_bit w n x) m = 

          (if m = n then n < size w & x else test_bit w m)"

   apply (unfold word_size word_test_bit_def word_set_bit_def)

   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)

   apply (auto elim!: test_bit_size [unfolded word_size]

               simp add: word_test_bit_def [symmetric])

   done

 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"

   unfolding of_bl_def bl_to_bin_rep_F by auto

 lemma msb_nth:

   fixes w :: "'a::len word"

   shows "msb w = w !! (len_of TYPE('a) - 1)"

   unfolding word_msb_nth word_test_bit_def by simp

 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]

 lemmas msb1 = msb0 [where i = 0]

 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]

 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]

 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]

 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:

   "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 

     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"

   apply (unfold word_size td_ext_def')

   apply safe

      apply (rule_tac [3] ext)

      apply (rule_tac [4] ext)

      apply (unfold word_size of_nth_def test_bit_bl)

      apply safe

        defer

        apply (clarsimp simp: word_bl.Abs_inverse)+

   apply (rule word_bl.Rep_inverse')

   apply (rule sym [THEN trans])

   apply (rule bl_of_nth_nth)

   apply simp

   apply (rule bl_of_nth_inj)

   apply (clarsimp simp add : test_bit_bl word_size)

   done

 interpretation test_bit:

   td_ext "op !! :: 'a::len0 word => nat => bool"

          set_bits

          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"

          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"

   by (rule td_ext_nth)

 lemmas td_nth = test_bit.td_thm

 lemma word_set_set_same [simp]:

   fixes w :: "'a::len0 word"

   shows "set_bit (set_bit w n x) n y = set_bit w n y" 

   by (rule word_eqI) (simp add : test_bit_set_gen word_size)

 lemma word_set_set_diff: 

   fixes w :: "'a::len0 word"

   assumes "m ~= n"

   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 

   by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)

 lemma nth_sint: 

   fixes w :: "'a::len word"

   defines "l \<equiv> len_of TYPE ('a)"

   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"

   unfolding sint_uint l_def

   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])

 lemma word_lsb_numeral [simp]:

   "lsb (numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (numeral bin)"

   unfolding word_lsb_alt test_bit_numeral by simp

 lemma word_lsb_neg_numeral [simp]:

   "lsb (- numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (- numeral bin)"

   unfolding word_lsb_alt test_bit_neg_numeral by simp

 lemma set_bit_word_of_int:

   "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"

   unfolding word_set_bit_def

   apply (rule word_eqI)

   apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)

   done

 lemma word_set_numeral [simp]:

   "set_bit (numeral bin::'a::len0 word) n b =