src/HOL/Word/Word.thy
author haftmann
Sat May 12 22:20:46 2018 +0200 (21 months ago ago)
changeset 68157 057d5b4ce47e
parent 67443 3abf6a722518
child 69046 5840724b1d71
permissions -rw-r--r--
removed some non-essential rules
     1 (*  Title:      HOL/Word/Word.thy
     2     Author:     Jeremy Dawson and Gerwin Klein, NICTA
     3 *)
     4 
     5 section \<open>A type of finite bit strings\<close>
     6 
     7 theory Word
     8 imports
     9   "HOL-Library.Type_Length"
    10   "HOL-Library.Boolean_Algebra"
    11   Bits_Bit
    12   Bool_List_Representation
    13   Misc_Typedef
    14   Word_Miscellaneous
    15 begin
    16 
    17 text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close>
    18 
    19 subsection \<open>Type definition\<close>
    20 
    21 typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}"
    22   morphisms uint Abs_word by auto
    23 
    24 lemma uint_nonnegative: "0 \<le> uint w"
    25   using word.uint [of w] by simp
    26 
    27 lemma uint_bounded: "uint w < 2 ^ len_of TYPE('a)"
    28   for w :: "'a::len0 word"
    29   using word.uint [of w] by simp
    30 
    31 lemma uint_idem: "uint w mod 2 ^ len_of TYPE('a) = uint w"
    32   for w :: "'a::len0 word"
    33   using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
    34 
    35 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
    36   by (simp add: uint_inject)
    37 
    38 lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
    39   by (simp add: word_uint_eq_iff)
    40 
    41 definition word_of_int :: "int \<Rightarrow> 'a::len0 word"
    42   \<comment> \<open>representation of words using unsigned or signed bins,
    43     only difference in these is the type class\<close>
    44   where "word_of_int k = Abs_word (k mod 2 ^ len_of TYPE('a))"
    45 
    46 lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ len_of TYPE('a)"
    47   by (auto simp add: word_of_int_def intro: Abs_word_inverse)
    48 
    49 lemma word_of_int_uint: "word_of_int (uint w) = w"
    50   by (simp add: word_of_int_def uint_idem uint_inverse)
    51 
    52 lemma split_word_all: "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
    53 proof
    54   fix x :: "'a word"
    55   assume "\<And>x. PROP P (word_of_int x)"
    56   then have "PROP P (word_of_int (uint x))" .
    57   then show "PROP P x" by (simp add: word_of_int_uint)
    58 qed
    59 
    60 
    61 subsection \<open>Type conversions and casting\<close>
    62 
    63 definition sint :: "'a::len word \<Rightarrow> int"
    64   \<comment> \<open>treats the most-significant-bit as a sign bit\<close>
    65   where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
    66 
    67 definition unat :: "'a::len0 word \<Rightarrow> nat"
    68   where "unat w = nat (uint w)"
    69 
    70 definition uints :: "nat \<Rightarrow> int set"
    71   \<comment> \<open>the sets of integers representing the words\<close>
    72   where "uints n = range (bintrunc n)"
    73 
    74 definition sints :: "nat \<Rightarrow> int set"
    75   where "sints n = range (sbintrunc (n - 1))"
    76 
    77 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
    78   by (simp add: uints_def range_bintrunc)
    79 
    80 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
    81   by (simp add: sints_def range_sbintrunc)
    82 
    83 definition unats :: "nat \<Rightarrow> nat set"
    84   where "unats n = {i. i < 2 ^ n}"
    85 
    86 definition norm_sint :: "nat \<Rightarrow> int \<Rightarrow> int"
    87   where "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
    88 
    89 definition scast :: "'a::len word \<Rightarrow> 'b::len word"
    90   \<comment> \<open>cast a word to a different length\<close>
    91   where "scast w = word_of_int (sint w)"
    92 
    93 definition ucast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
    94   where "ucast w = word_of_int (uint w)"
    95 
    96 instantiation word :: (len0) size
    97 begin
    98 
    99 definition word_size: "size (w :: 'a word) = len_of TYPE('a)"
   100 
   101 instance ..
   102 
   103 end
   104 
   105 lemma word_size_gt_0 [iff]: "0 < size w"
   106   for w :: "'a::len word"
   107   by (simp add: word_size)
   108 
   109 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
   110 
   111 lemma lens_not_0 [iff]:
   112   fixes w :: "'a::len word"
   113   shows "size w \<noteq> 0"
   114   and "len_of TYPE('a) \<noteq> 0"
   115   by auto
   116 
   117 definition source_size :: "('a::len0 word \<Rightarrow> 'b) \<Rightarrow> nat"
   118   \<comment> \<open>whether a cast (or other) function is to a longer or shorter length\<close>
   119   where [code del]: "source_size c = (let arb = undefined; x = c arb in size arb)"
   120 
   121 definition target_size :: "('a \<Rightarrow> 'b::len0 word) \<Rightarrow> nat"
   122   where [code del]: "target_size c = size (c undefined)"
   123 
   124 definition is_up :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
   125   where "is_up c \<longleftrightarrow> source_size c \<le> target_size c"
   126 
   127 definition is_down :: "('a::len0 word \<Rightarrow> 'b::len0 word) \<Rightarrow> bool"
   128   where "is_down c \<longleftrightarrow> target_size c \<le> source_size c"
   129 
   130 definition of_bl :: "bool list \<Rightarrow> 'a::len0 word"
   131   where "of_bl bl = word_of_int (bl_to_bin bl)"
   132 
   133 definition to_bl :: "'a::len0 word \<Rightarrow> bool list"
   134   where "to_bl w = bin_to_bl (len_of TYPE('a)) (uint w)"
   135 
   136 definition word_reverse :: "'a::len0 word \<Rightarrow> 'a word"
   137   where "word_reverse w = of_bl (rev (to_bl w))"
   138 
   139 definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len0 word \<Rightarrow> 'b"
   140   where "word_int_case f w = f (uint w)"
   141 
   142 translations
   143   "case x of XCONST of_int y \<Rightarrow> b" \<rightleftharpoons> "CONST word_int_case (\<lambda>y. b) x"
   144   "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x"
   145 
   146 
   147 subsection \<open>Correspondence relation for theorem transfer\<close>
   148 
   149 definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   150   where "cr_word = (\<lambda>x y. word_of_int x = y)"
   151 
   152 lemma Quotient_word:
   153   "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
   154     word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
   155   unfolding Quotient_alt_def cr_word_def
   156   by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)
   157 
   158 lemma reflp_word:
   159   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   160   by (simp add: reflp_def)
   161 
   162 setup_lifting Quotient_word reflp_word
   163 
   164 text \<open>TODO: The next lemma could be generated automatically.\<close>
   165 
   166 lemma uint_transfer [transfer_rule]:
   167   "(rel_fun pcr_word (=)) (bintrunc (len_of TYPE('a))) (uint :: 'a::len0 word \<Rightarrow> int)"
   168   unfolding rel_fun_def word.pcr_cr_eq cr_word_def
   169   by (simp add: no_bintr_alt1 uint_word_of_int)
   170 
   171 
   172 subsection \<open>Basic code generation setup\<close>
   173 
   174 definition Word :: "int \<Rightarrow> 'a::len0 word"
   175   where [code_post]: "Word = word_of_int"
   176 
   177 lemma [code abstype]: "Word (uint w) = w"
   178   by (simp add: Word_def word_of_int_uint)
   179 
   180 declare uint_word_of_int [code abstract]
   181 
   182 instantiation word :: (len0) equal
   183 begin
   184 
   185 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   186   where "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
   187 
   188 instance
   189   by standard (simp add: equal equal_word_def word_uint_eq_iff)
   190 
   191 end
   192 
   193 notation fcomp (infixl "\<circ>>" 60)
   194 notation scomp (infixl "\<circ>\<rightarrow>" 60)
   195 
   196 instantiation word :: ("{len0, typerep}") random
   197 begin
   198 
   199 definition
   200   "random_word i = Random.range i \<circ>\<rightarrow> (\<lambda>k. Pair (
   201      let j = word_of_int (int_of_integer (integer_of_natural k)) :: 'a word
   202      in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
   203 
   204 instance ..
   205 
   206 end
   207 
   208 no_notation fcomp (infixl "\<circ>>" 60)
   209 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
   210 
   211 
   212 subsection \<open>Type-definition locale instantiations\<close>
   213 
   214 lemmas uint_0 = uint_nonnegative (* FIXME duplicate *)
   215 lemmas uint_lt = uint_bounded (* FIXME duplicate *)
   216 lemmas uint_mod_same = uint_idem (* FIXME duplicate *)
   217 
   218 lemma td_ext_uint:
   219   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
   220     (\<lambda>w::int. w mod 2 ^ len_of TYPE('a))"
   221   apply (unfold td_ext_def')
   222   apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
   223   apply (simp add: uint_mod_same uint_0 uint_lt
   224                    word.uint_inverse word.Abs_word_inverse int_mod_lem)
   225   done
   226 
   227 interpretation word_uint:
   228   td_ext
   229     "uint::'a::len0 word \<Rightarrow> int"
   230     word_of_int
   231     "uints (len_of TYPE('a::len0))"
   232     "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
   233   by (fact td_ext_uint)
   234 
   235 lemmas td_uint = word_uint.td_thm
   236 lemmas int_word_uint = word_uint.eq_norm
   237 
   238 lemma td_ext_ubin:
   239   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (len_of TYPE('a::len0)))
   240     (bintrunc (len_of TYPE('a)))"
   241   by (unfold no_bintr_alt1) (fact td_ext_uint)
   242 
   243 interpretation word_ubin:
   244   td_ext
   245     "uint::'a::len0 word \<Rightarrow> int"
   246     word_of_int
   247     "uints (len_of TYPE('a::len0))"
   248     "bintrunc (len_of TYPE('a::len0))"
   249   by (fact td_ext_ubin)
   250 
   251 
   252 subsection \<open>Arithmetic operations\<close>
   253 
   254 lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
   255   by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
   256 
   257 lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
   258   by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
   259 
   260 instantiation word :: (len0) "{neg_numeral, modulo, comm_monoid_mult, comm_ring}"
   261 begin
   262 
   263 lift_definition zero_word :: "'a word" is "0" .
   264 
   265 lift_definition one_word :: "'a word" is "1" .
   266 
   267 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(+)"
   268   by (auto simp add: bintrunc_mod2p intro: mod_add_cong)
   269 
   270 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(-)"
   271   by (auto simp add: bintrunc_mod2p intro: mod_diff_cong)
   272 
   273 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word" is uminus
   274   by (auto simp add: bintrunc_mod2p intro: mod_minus_cong)
   275 
   276 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "( * )"
   277   by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
   278 
   279 definition word_div_def: "a div b = word_of_int (uint a div uint b)"
   280 
   281 definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
   282 
   283 instance
   284   by standard (transfer, simp add: algebra_simps)+
   285 
   286 end
   287 
   288 text \<open>Legacy theorems:\<close>
   289 
   290 lemma word_arith_wis [code]:
   291   shows word_add_def: "a + b = word_of_int (uint a + uint b)"
   292     and word_sub_wi: "a - b = word_of_int (uint a - uint b)"
   293     and word_mult_def: "a * b = word_of_int (uint a * uint b)"
   294     and word_minus_def: "- a = word_of_int (- uint a)"
   295     and word_succ_alt: "word_succ a = word_of_int (uint a + 1)"
   296     and word_pred_alt: "word_pred a = word_of_int (uint a - 1)"
   297     and word_0_wi: "0 = word_of_int 0"
   298     and word_1_wi: "1 = word_of_int 1"
   299   unfolding plus_word_def minus_word_def times_word_def uminus_word_def
   300   unfolding word_succ_def word_pred_def zero_word_def one_word_def
   301   by simp_all
   302 
   303 lemma wi_homs:
   304   shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
   305     and wi_hom_sub: "word_of_int a - word_of_int b = word_of_int (a - b)"
   306     and wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)"
   307     and wi_hom_neg: "- word_of_int a = word_of_int (- a)"
   308     and wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)"
   309     and wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
   310   by (transfer, simp)+
   311 
   312 lemmas wi_hom_syms = wi_homs [symmetric]
   313 
   314 lemmas word_of_int_homs = wi_homs word_0_wi word_1_wi
   315 
   316 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
   317 
   318 instance word :: (len) comm_ring_1
   319 proof
   320   have *: "0 < len_of TYPE('a)" by (rule len_gt_0)
   321   show "(0::'a word) \<noteq> 1"
   322     by transfer (use * in \<open>auto simp add: gr0_conv_Suc\<close>)
   323 qed
   324 
   325 lemma word_of_nat: "of_nat n = word_of_int (int n)"
   326   by (induct n) (auto simp add : word_of_int_hom_syms)
   327 
   328 lemma word_of_int: "of_int = word_of_int"
   329   apply (rule ext)
   330   apply (case_tac x rule: int_diff_cases)
   331   apply (simp add: word_of_nat wi_hom_sub)
   332   done
   333 
   334 definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
   335   where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
   336 
   337 
   338 subsection \<open>Ordering\<close>
   339 
   340 instantiation word :: (len0) linorder
   341 begin
   342 
   343 definition word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
   344 
   345 definition word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
   346 
   347 instance
   348   by standard (auto simp: word_less_def word_le_def)
   349 
   350 end
   351 
   352 definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"  ("(_/ <=s _)" [50, 51] 50)
   353   where "a <=s b \<longleftrightarrow> sint a \<le> sint b"
   354 
   355 definition word_sless :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"  ("(_/ <s _)" [50, 51] 50)
   356   where "x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y"
   357 
   358 
   359 subsection \<open>Bit-wise operations\<close>
   360 
   361 instantiation word :: (len0) bits
   362 begin
   363 
   364 lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word" is bitNOT
   365   by (metis bin_trunc_not)
   366 
   367 lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitAND
   368   by (metis bin_trunc_and)
   369 
   370 lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitOR
   371   by (metis bin_trunc_or)
   372 
   373 lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is bitXOR
   374   by (metis bin_trunc_xor)
   375 
   376 definition word_test_bit_def: "test_bit a = bin_nth (uint a)"
   377 
   378 definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
   379 
   380 definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
   381 
   382 definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
   383 
   384 definition shiftl1 :: "'a word \<Rightarrow> 'a word"
   385   where "shiftl1 w = word_of_int (uint w BIT False)"
   386 
   387 definition shiftr1 :: "'a word \<Rightarrow> 'a word"
   388   \<comment> \<open>shift right as unsigned or as signed, ie logical or arithmetic\<close>
   389   where "shiftr1 w = word_of_int (bin_rest (uint w))"
   390 
   391 definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
   392 
   393 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"
   394 
   395 instance ..
   396 
   397 end
   398 
   399 lemma [code]:
   400   shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
   401     and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
   402     and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)"
   403     and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   404   by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
   405 
   406 instantiation word :: (len) bitss
   407 begin
   408 
   409 definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
   410 
   411 instance ..
   412 
   413 end
   414 
   415 definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
   416   where "setBit w n = set_bit w n True"
   417 
   418 definition clearBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
   419   where "clearBit w n = set_bit w n False"
   420 
   421 
   422 subsection \<open>Shift operations\<close>
   423 
   424 definition sshiftr1 :: "'a::len word \<Rightarrow> 'a word"
   425   where "sshiftr1 w = word_of_int (bin_rest (sint w))"
   426 
   427 definition bshiftr1 :: "bool \<Rightarrow> 'a::len word \<Rightarrow> 'a word"
   428   where "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
   429 
   430 definition sshiftr :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"  (infixl ">>>" 55)
   431   where "w >>> n = (sshiftr1 ^^ n) w"
   432 
   433 definition mask :: "nat \<Rightarrow> 'a::len word"
   434   where "mask n = (1 << n) - 1"
   435 
   436 definition revcast :: "'a::len0 word \<Rightarrow> 'b::len0 word"
   437   where "revcast w =  of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
   438 
   439 definition slice1 :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
   440   where "slice1 n w = of_bl (takefill False n (to_bl w))"
   441 
   442 definition slice :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'b::len0 word"
   443   where "slice n w = slice1 (size w - n) w"
   444 
   445 
   446 subsection \<open>Rotation\<close>
   447 
   448 definition rotater1 :: "'a list \<Rightarrow> 'a list"
   449   where "rotater1 ys =
   450     (case ys of [] \<Rightarrow> [] | x # xs \<Rightarrow> last ys # butlast ys)"
   451 
   452 definition rotater :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
   453   where "rotater n = rotater1 ^^ n"
   454 
   455 definition word_rotr :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
   456   where "word_rotr n w = of_bl (rotater n (to_bl w))"
   457 
   458 definition word_rotl :: "nat \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
   459   where "word_rotl n w = of_bl (rotate n (to_bl w))"
   460 
   461 definition word_roti :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> 'a::len0 word"
   462   where "word_roti i w =
   463     (if i \<ge> 0 then word_rotr (nat i) w else word_rotl (nat (- i)) w)"
   464 
   465 
   466 subsection \<open>Split and cat operations\<close>
   467 
   468 definition word_cat :: "'a::len0 word \<Rightarrow> 'b::len0 word \<Rightarrow> 'c::len0 word"
   469   where "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE('b)) (uint b))"
   470 
   471 definition word_split :: "'a::len0 word \<Rightarrow> 'b::len0 word \<times> 'c::len0 word"
   472   where "word_split a =
   473     (case bin_split (len_of TYPE('c)) (uint a) of
   474       (u, v) \<Rightarrow> (word_of_int u, word_of_int v))"
   475 
   476 definition word_rcat :: "'a::len0 word list \<Rightarrow> 'b::len0 word"
   477   where "word_rcat ws = word_of_int (bin_rcat (len_of TYPE('a)) (map uint ws))"
   478 
   479 definition word_rsplit :: "'a::len0 word \<Rightarrow> 'b::len word list"
   480   where "word_rsplit w = map word_of_int (bin_rsplit (len_of TYPE('b)) (len_of TYPE('a), uint w))"
   481 
   482 definition max_word :: "'a::len word"
   483   \<comment> \<open>Largest representable machine integer.\<close>
   484   where "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
   485 
   486 lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
   487 
   488 
   489 subsection \<open>Theorems about typedefs\<close>
   490 
   491 lemma sint_sbintrunc': "sint (word_of_int bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) bin"
   492   by (auto simp: sint_uint word_ubin.eq_norm sbintrunc_bintrunc_lt)
   493 
   494 lemma uint_sint: "uint w = bintrunc (len_of TYPE('a)) (sint w)"
   495   for w :: "'a::len word"
   496   by (auto simp: sint_uint bintrunc_sbintrunc_le)
   497 
   498 lemma bintr_uint: "len_of TYPE('a) \<le> n \<Longrightarrow> bintrunc n (uint w) = uint w"
   499   for w :: "'a::len0 word"
   500   apply (subst word_ubin.norm_Rep [symmetric])
   501   apply (simp only: bintrunc_bintrunc_min word_size)
   502   apply (simp add: min.absorb2)
   503   done
   504 
   505 lemma wi_bintr:
   506   "len_of TYPE('a::len0) \<le> n \<Longrightarrow>
   507     word_of_int (bintrunc n w) = (word_of_int w :: 'a word)"
   508   by (auto simp: word_ubin.norm_eq_iff [symmetric] min.absorb1)
   509 
   510 lemma td_ext_sbin:
   511   "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))
   512     (sbintrunc (len_of TYPE('a) - 1))"
   513   apply (unfold td_ext_def' sint_uint)
   514   apply (simp add : word_ubin.eq_norm)
   515   apply (cases "len_of TYPE('a)")
   516    apply (auto simp add : sints_def)
   517   apply (rule sym [THEN trans])
   518    apply (rule word_ubin.Abs_norm)
   519   apply (simp only: bintrunc_sbintrunc)
   520   apply (drule sym)
   521   apply simp
   522   done
   523 
   524 lemma td_ext_sint:
   525   "td_ext (sint :: 'a word \<Rightarrow> int) word_of_int (sints (len_of TYPE('a::len)))
   526      (\<lambda>w. (w + 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
   527          2 ^ (len_of TYPE('a) - 1))"
   528   using td_ext_sbin [where ?'a = 'a] by (simp add: no_sbintr_alt2)
   529 
   530 text \<open>
   531   We do \<open>sint\<close> before \<open>sbin\<close>, before \<open>sint\<close> is the user version
   532   and interpretations do not produce thm duplicates. I.e.
   533   we get the name \<open>word_sint.Rep_eqD\<close>, but not \<open>word_sbin.Req_eqD\<close>,
   534   because the latter is the same thm as the former.
   535 \<close>
   536 interpretation word_sint:
   537   td_ext
   538     "sint ::'a::len word \<Rightarrow> int"
   539     word_of_int
   540     "sints (len_of TYPE('a::len))"
   541     "\<lambda>w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
   542       2 ^ (len_of TYPE('a::len) - 1)"
   543   by (rule td_ext_sint)
   544 
   545 interpretation word_sbin:
   546   td_ext
   547     "sint ::'a::len word \<Rightarrow> int"
   548     word_of_int
   549     "sints (len_of TYPE('a::len))"
   550     "sbintrunc (len_of TYPE('a::len) - 1)"
   551   by (rule td_ext_sbin)
   552 
   553 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
   554 
   555 lemmas td_sint = word_sint.td
   556 
   557 lemma to_bl_def': "(to_bl :: 'a::len0 word \<Rightarrow> bool list) = bin_to_bl (len_of TYPE('a)) \<circ> uint"
   558   by (auto simp: to_bl_def)
   559 
   560 lemmas word_reverse_no_def [simp] =
   561   word_reverse_def [of "numeral w"] for w
   562 
   563 lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
   564   by (fact uints_def [unfolded no_bintr_alt1])
   565 
   566 lemma word_numeral_alt: "numeral b = word_of_int (numeral b)"
   567   by (induct b, simp_all only: numeral.simps word_of_int_homs)
   568 
   569 declare word_numeral_alt [symmetric, code_abbrev]
   570 
   571 lemma word_neg_numeral_alt: "- numeral b = word_of_int (- numeral b)"
   572   by (simp only: word_numeral_alt wi_hom_neg)
   573 
   574 declare word_neg_numeral_alt [symmetric, code_abbrev]
   575 
   576 lemma word_numeral_transfer [transfer_rule]:
   577   "(rel_fun (=) pcr_word) numeral numeral"
   578   "(rel_fun (=) pcr_word) (- numeral) (- numeral)"
   579   apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
   580   using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by auto
   581 
   582 lemma uint_bintrunc [simp]:
   583   "uint (numeral bin :: 'a word) =
   584     bintrunc (len_of TYPE('a::len0)) (numeral bin)"
   585   unfolding word_numeral_alt by (rule word_ubin.eq_norm)
   586 
   587 lemma uint_bintrunc_neg [simp]:
   588   "uint (- numeral bin :: 'a word) = bintrunc (len_of TYPE('a::len0)) (- numeral bin)"
   589   by (simp only: word_neg_numeral_alt word_ubin.eq_norm)
   590 
   591 lemma sint_sbintrunc [simp]:
   592   "sint (numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (numeral bin)"
   593   by (simp only: word_numeral_alt word_sbin.eq_norm)
   594 
   595 lemma sint_sbintrunc_neg [simp]:
   596   "sint (- numeral bin :: 'a word) = sbintrunc (len_of TYPE('a::len) - 1) (- numeral bin)"
   597   by (simp only: word_neg_numeral_alt word_sbin.eq_norm)
   598 
   599 lemma unat_bintrunc [simp]:
   600   "unat (numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (numeral bin))"
   601   by (simp only: unat_def uint_bintrunc)
   602 
   603 lemma unat_bintrunc_neg [simp]:
   604   "unat (- numeral bin :: 'a::len0 word) = nat (bintrunc (len_of TYPE('a)) (- numeral bin))"
   605   by (simp only: unat_def uint_bintrunc_neg)
   606 
   607 lemma size_0_eq: "size w = 0 \<Longrightarrow> v = w"
   608   for v w :: "'a::len0 word"
   609   apply (unfold word_size)
   610   apply (rule word_uint.Rep_eqD)
   611   apply (rule box_equals)
   612     defer
   613     apply (rule word_ubin.norm_Rep)+
   614   apply simp
   615   done
   616 
   617 lemma uint_ge_0 [iff]: "0 \<le> uint x"
   618   for x :: "'a::len0 word"
   619   using word_uint.Rep [of x] by (simp add: uints_num)
   620 
   621 lemma uint_lt2p [iff]: "uint x < 2 ^ len_of TYPE('a)"
   622   for x :: "'a::len0 word"
   623   using word_uint.Rep [of x] by (simp add: uints_num)
   624 
   625 lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint x"
   626   for x :: "'a::len word"
   627   using word_sint.Rep [of x] by (simp add: sints_num)
   628 
   629 lemma sint_lt: "sint x < 2 ^ (len_of TYPE('a) - 1)"
   630   for x :: "'a::len word"
   631   using word_sint.Rep [of x] by (simp add: sints_num)
   632 
   633 lemma sign_uint_Pls [simp]: "bin_sign (uint x) = 0"
   634   by (simp add: sign_Pls_ge_0)
   635 
   636 lemma uint_m2p_neg: "uint x - 2 ^ len_of TYPE('a) < 0"
   637   for x :: "'a::len0 word"
   638   by (simp only: diff_less_0_iff_less uint_lt2p)
   639 
   640 lemma uint_m2p_not_non_neg: "\<not> 0 \<le> uint x - 2 ^ len_of TYPE('a)"
   641   for x :: "'a::len0 word"
   642   by (simp only: not_le uint_m2p_neg)
   643 
   644 lemma lt2p_lem: "len_of TYPE('a) \<le> n \<Longrightarrow> uint w < 2 ^ n"
   645   for w :: "'a::len0 word"
   646   by (metis bintr_uint bintrunc_mod2p int_mod_lem zless2p)
   647 
   648 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
   649   by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
   650 
   651 lemma uint_nat: "uint w = int (unat w)"
   652   by (auto simp: unat_def)
   653 
   654 lemma uint_numeral: "uint (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
   655   by (simp only: word_numeral_alt int_word_uint)
   656 
   657 lemma uint_neg_numeral: "uint (- numeral b :: 'a::len0 word) = - numeral b mod 2 ^ len_of TYPE('a)"
   658   by (simp only: word_neg_numeral_alt int_word_uint)
   659 
   660 lemma unat_numeral: "unat (numeral b :: 'a::len0 word) = numeral b mod 2 ^ len_of TYPE('a)"
   661   apply (unfold unat_def)
   662   apply (clarsimp simp only: uint_numeral)
   663   apply (rule nat_mod_distrib [THEN trans])
   664     apply (rule zero_le_numeral)
   665    apply (simp_all add: nat_power_eq)
   666   done
   667 
   668 lemma sint_numeral:
   669   "sint (numeral b :: 'a::len word) =
   670     (numeral b +
   671       2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
   672       2 ^ (len_of TYPE('a) - 1)"
   673   unfolding word_numeral_alt by (rule int_word_sint)
   674 
   675 lemma word_of_int_0 [simp, code_post]: "word_of_int 0 = 0"
   676   unfolding word_0_wi ..
   677 
   678 lemma word_of_int_1 [simp, code_post]: "word_of_int 1 = 1"
   679   unfolding word_1_wi ..
   680 
   681 lemma word_of_int_neg_1 [simp]: "word_of_int (- 1) = - 1"
   682   by (simp add: wi_hom_syms)
   683 
   684 lemma word_of_int_numeral [simp] : "(word_of_int (numeral bin) :: 'a::len0 word) = numeral bin"
   685   by (simp only: word_numeral_alt)
   686 
   687 lemma word_of_int_neg_numeral [simp]:
   688   "(word_of_int (- numeral bin) :: 'a::len0 word) = - numeral bin"
   689   by (simp only: word_numeral_alt wi_hom_syms)
   690 
   691 lemma word_int_case_wi:
   692   "word_int_case f (word_of_int i :: 'b word) = f (i mod 2 ^ len_of TYPE('b::len0))"
   693   by (simp add: word_int_case_def word_uint.eq_norm)
   694 
   695 lemma word_int_split:
   696   "P (word_int_case f x) =
   697     (\<forall>i. x = (word_of_int i :: 'b::len0 word) \<and> 0 \<le> i \<and> i < 2 ^ len_of TYPE('b) \<longrightarrow> P (f i))"
   698   by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
   699 
   700 lemma word_int_split_asm:
   701   "P (word_int_case f x) =
   702     (\<nexists>n. x = (word_of_int n :: 'b::len0 word) \<and> 0 \<le> n \<and> n < 2 ^ len_of TYPE('b::len0) \<and> \<not> P (f n))"
   703   by (auto simp: word_int_case_def word_uint.eq_norm mod_pos_pos_trivial)
   704 
   705 lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
   706 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
   707 
   708 lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
   709   unfolding word_size by (rule uint_range')
   710 
   711 lemma sint_range_size: "- (2 ^ (size w - Suc 0)) \<le> sint w \<and> sint w < 2 ^ (size w - Suc 0)"
   712   unfolding word_size by (rule sint_range')
   713 
   714 lemma sint_above_size: "2 ^ (size w - 1) \<le> x \<Longrightarrow> sint w < x"
   715   for w :: "'a::len word"
   716   unfolding word_size by (rule less_le_trans [OF sint_lt])
   717 
   718 lemma sint_below_size: "x \<le> - (2 ^ (size w - 1)) \<Longrightarrow> x \<le> sint w"
   719   for w :: "'a::len word"
   720   unfolding word_size by (rule order_trans [OF _ sint_ge])
   721 
   722 
   723 subsection \<open>Testing bits\<close>
   724 
   725 lemma test_bit_eq_iff: "test_bit u = test_bit v \<longleftrightarrow> u = v"
   726   for u v :: "'a::len0 word"
   727   unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
   728 
   729 lemma test_bit_size [rule_format] : "w !! n \<longrightarrow> n < size w"
   730   for w :: "'a::len0 word"
   731   apply (unfold word_test_bit_def)
   732   apply (subst word_ubin.norm_Rep [symmetric])
   733   apply (simp only: nth_bintr word_size)
   734   apply fast
   735   done
   736 
   737 lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<len_of TYPE('a). x !! n = y !! n)"
   738   for x y :: "'a::len0 word"
   739   unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
   740   by (metis test_bit_size [unfolded word_size])
   741 
   742 lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
   743   for u :: "'a::len0 word"
   744   by (simp add: word_size word_eq_iff)
   745 
   746 lemma word_eqD: "u = v \<Longrightarrow> u !! x = v !! x"
   747   for u v :: "'a::len0 word"
   748   by simp
   749 
   750 lemma test_bit_bin': "w !! n \<longleftrightarrow> n < size w \<and> bin_nth (uint w) n"
   751   by (simp add: word_test_bit_def word_size nth_bintr [symmetric])
   752 
   753 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
   754 
   755 lemma bin_nth_uint_imp: "bin_nth (uint w) n \<Longrightarrow> n < len_of TYPE('a)"
   756   for w :: "'a::len0 word"
   757   apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
   758   apply (subst word_ubin.norm_Rep)
   759   apply assumption
   760   done
   761 
   762 lemma bin_nth_sint:
   763   "len_of TYPE('a) \<le> n \<Longrightarrow>
   764     bin_nth (sint w) n = bin_nth (sint w) (len_of TYPE('a) - 1)"
   765   for w :: "'a::len word"
   766   apply (subst word_sbin.norm_Rep [symmetric])
   767   apply (auto simp add: nth_sbintr)
   768   done
   769 
   770 \<comment> \<open>type definitions theorem for in terms of equivalent bool list\<close>
   771 lemma td_bl:
   772   "type_definition
   773     (to_bl :: 'a::len0 word \<Rightarrow> bool list)
   774     of_bl
   775     {bl. length bl = len_of TYPE('a)}"
   776   apply (unfold type_definition_def of_bl_def to_bl_def)
   777   apply (simp add: word_ubin.eq_norm)
   778   apply safe
   779   apply (drule sym)
   780   apply simp
   781   done
   782 
   783 interpretation word_bl:
   784   type_definition
   785     "to_bl :: 'a::len0 word \<Rightarrow> bool list"
   786     of_bl
   787     "{bl. length bl = len_of TYPE('a::len0)}"
   788   by (fact td_bl)
   789 
   790 lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
   791 
   792 lemma word_size_bl: "size w = size (to_bl w)"
   793   by (auto simp: word_size)
   794 
   795 lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
   796   by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
   797 
   798 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
   799   by (simp add: word_reverse_def word_bl.Abs_inverse)
   800 
   801 lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
   802   by (simp add: word_reverse_def word_bl.Abs_inverse)
   803 
   804 lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
   805   by (metis word_rev_rev)
   806 
   807 lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
   808   by simp
   809 
   810 lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
   811   for x :: "'a::len word"
   812   unfolding word_bl_Rep' by (rule len_gt_0)
   813 
   814 lemma bl_not_Nil [iff]: "to_bl x \<noteq> []"
   815   for x :: "'a::len word"
   816   by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
   817 
   818 lemma length_bl_neq_0 [iff]: "length (to_bl x) \<noteq> 0"
   819   for x :: "'a::len word"
   820   by (fact length_bl_gt_0 [THEN gr_implies_not0])
   821 
   822 lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = -1)"
   823   apply (unfold to_bl_def sint_uint)
   824   apply (rule trans [OF _ bl_sbin_sign])
   825   apply simp
   826   done
   827 
   828 lemma of_bl_drop':
   829   "lend = length bl - len_of TYPE('a::len0) \<Longrightarrow>
   830     of_bl (drop lend bl) = (of_bl bl :: 'a word)"
   831   by (auto simp: of_bl_def trunc_bl2bin [symmetric])
   832 
   833 lemma test_bit_of_bl:
   834   "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
   835   by (auto simp add: of_bl_def word_test_bit_def word_size
   836       word_ubin.eq_norm nth_bintr bin_nth_of_bl)
   837 
   838 lemma no_of_bl: "(numeral bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE('a)) (numeral bin))"
   839   by (simp add: of_bl_def)
   840 
   841 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
   842   by (auto simp: word_size to_bl_def)
   843 
   844 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
   845   by (simp add: uint_bl word_size)
   846 
   847 lemma to_bl_of_bin: "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
   848   by (auto simp: uint_bl word_ubin.eq_norm word_size)
   849 
   850 lemma to_bl_numeral [simp]:
   851   "to_bl (numeral bin::'a::len0 word) =
   852     bin_to_bl (len_of TYPE('a)) (numeral bin)"
   853   unfolding word_numeral_alt by (rule to_bl_of_bin)
   854 
   855 lemma to_bl_neg_numeral [simp]:
   856   "to_bl (- numeral bin::'a::len0 word) =
   857     bin_to_bl (len_of TYPE('a)) (- numeral bin)"
   858   unfolding word_neg_numeral_alt by (rule to_bl_of_bin)
   859 
   860 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
   861   by (simp add: uint_bl word_size)
   862 
   863 lemma uint_bl_bin: "bl_to_bin (bin_to_bl (len_of TYPE('a)) (uint x)) = uint x"
   864   for x :: "'a::len0 word"
   865   by (rule trans [OF bin_bl_bin word_ubin.norm_Rep])
   866 
   867 \<comment> \<open>naturals\<close>
   868 lemma uints_unats: "uints n = int ` unats n"
   869   apply (unfold unats_def uints_num)
   870   apply safe
   871     apply (rule_tac image_eqI)
   872      apply (erule_tac nat_0_le [symmetric])
   873   by auto
   874 
   875 lemma unats_uints: "unats n = nat ` uints n"
   876   by (auto simp: uints_unats image_iff)
   877 
   878 lemmas bintr_num =
   879   word_ubin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
   880 lemmas sbintr_num =
   881   word_sbin.norm_eq_iff [of "numeral a" "numeral b", symmetric, folded word_numeral_alt] for a b
   882 
   883 lemma num_of_bintr':
   884   "bintrunc (len_of TYPE('a::len0)) (numeral a) = (numeral b) \<Longrightarrow>
   885     numeral a = (numeral b :: 'a word)"
   886   unfolding bintr_num by (erule subst, simp)
   887 
   888 lemma num_of_sbintr':
   889   "sbintrunc (len_of TYPE('a::len) - 1) (numeral a) = (numeral b) \<Longrightarrow>
   890     numeral a = (numeral b :: 'a word)"
   891   unfolding sbintr_num by (erule subst, simp)
   892 
   893 lemma num_abs_bintr:
   894   "(numeral x :: 'a word) =
   895     word_of_int (bintrunc (len_of TYPE('a::len0)) (numeral x))"
   896   by (simp only: word_ubin.Abs_norm word_numeral_alt)
   897 
   898 lemma num_abs_sbintr:
   899   "(numeral x :: 'a word) =
   900     word_of_int (sbintrunc (len_of TYPE('a::len) - 1) (numeral x))"
   901   by (simp only: word_sbin.Abs_norm word_numeral_alt)
   902 
   903 text \<open>
   904   \<open>cast\<close> -- note, no arg for new length, as it's determined by type of result,
   905   thus in \<open>cast w = w\<close>, the type means cast to length of \<open>w\<close>!
   906 \<close>
   907 
   908 lemma ucast_id: "ucast w = w"
   909   by (auto simp: ucast_def)
   910 
   911 lemma scast_id: "scast w = w"
   912   by (auto simp: scast_def)
   913 
   914 lemma ucast_bl: "ucast w = of_bl (to_bl w)"
   915   by (auto simp: ucast_def of_bl_def uint_bl word_size)
   916 
   917 lemma nth_ucast: "(ucast w::'a::len0 word) !! n = (w !! n \<and> n < len_of TYPE('a))"
   918   by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
   919     (fast elim!: bin_nth_uint_imp)
   920 
   921 \<comment> \<open>literal u(s)cast\<close>
   922 lemma ucast_bintr [simp]:
   923   "ucast (numeral w :: 'a::len0 word) =
   924     word_of_int (bintrunc (len_of TYPE('a)) (numeral w))"
   925   by (simp add: ucast_def)
   926 
   927 (* TODO: neg_numeral *)
   928 
   929 lemma scast_sbintr [simp]:
   930   "scast (numeral w ::'a::len word) =
   931     word_of_int (sbintrunc (len_of TYPE('a) - Suc 0) (numeral w))"
   932   by (simp add: scast_def)
   933 
   934 lemma source_size: "source_size (c::'a::len0 word \<Rightarrow> _) = len_of TYPE('a)"
   935   unfolding source_size_def word_size Let_def ..
   936 
   937 lemma target_size: "target_size (c::_ \<Rightarrow> 'b::len0 word) = len_of TYPE('b)"
   938   unfolding target_size_def word_size Let_def ..
   939 
   940 lemma is_down: "is_down c \<longleftrightarrow> len_of TYPE('b) \<le> len_of TYPE('a)"
   941   for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
   942   by (simp only: is_down_def source_size target_size)
   943 
   944 lemma is_up: "is_up c \<longleftrightarrow> len_of TYPE('a) \<le> len_of TYPE('b)"
   945   for c :: "'a::len0 word \<Rightarrow> 'b::len0 word"
   946   by (simp only: is_up_def source_size target_size)
   947 
   948 lemmas is_up_down = trans [OF is_up is_down [symmetric]]
   949 
   950 lemma down_cast_same [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"
   951   apply (unfold is_down)
   952   apply safe
   953   apply (rule ext)
   954   apply (unfold ucast_def scast_def uint_sint)
   955   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
   956   apply simp
   957   done
   958 
   959 lemma word_rev_tf:
   960   "to_bl (of_bl bl::'a::len0 word) =
   961     rev (takefill False (len_of TYPE('a)) (rev bl))"
   962   by (auto simp: of_bl_def uint_bl bl_bin_bl_rtf word_ubin.eq_norm word_size)
   963 
   964 lemma word_rep_drop:
   965   "to_bl (of_bl bl::'a::len0 word) =
   966     replicate (len_of TYPE('a) - length bl) False @
   967     drop (length bl - len_of TYPE('a)) bl"
   968   by (simp add: word_rev_tf takefill_alt rev_take)
   969 
   970 lemma to_bl_ucast:
   971   "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
   972     replicate (len_of TYPE('a) - len_of TYPE('b)) False @
   973     drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
   974   apply (unfold ucast_bl)
   975   apply (rule trans)
   976    apply (rule word_rep_drop)
   977   apply simp
   978   done
   979 
   980 lemma ucast_up_app [OF refl]:
   981   "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow>
   982     to_bl (uc w) = replicate n False @ (to_bl w)"
   983   by (auto simp add : source_size target_size to_bl_ucast)
   984 
   985 lemma ucast_down_drop [OF refl]:
   986   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
   987     to_bl (uc w) = drop n (to_bl w)"
   988   by (auto simp add : source_size target_size to_bl_ucast)
   989 
   990 lemma scast_down_drop [OF refl]:
   991   "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
   992     to_bl (sc w) = drop n (to_bl w)"
   993   apply (subgoal_tac "sc = ucast")
   994    apply safe
   995    apply simp
   996    apply (erule ucast_down_drop)
   997   apply (rule down_cast_same [symmetric])
   998   apply (simp add : source_size target_size is_down)
   999   done
  1000 
  1001 lemma sint_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
  1002   apply (unfold is_up)
  1003   apply safe
  1004   apply (simp add: scast_def word_sbin.eq_norm)
  1005   apply (rule box_equals)
  1006     prefer 3
  1007     apply (rule word_sbin.norm_Rep)
  1008    apply (rule sbintrunc_sbintrunc_l)
  1009    defer
  1010    apply (subst word_sbin.norm_Rep)
  1011    apply (rule refl)
  1012   apply simp
  1013   done
  1014 
  1015 lemma uint_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
  1016   apply (unfold is_up)
  1017   apply safe
  1018   apply (rule bin_eqI)
  1019   apply (fold word_test_bit_def)
  1020   apply (auto simp add: nth_ucast)
  1021   apply (auto simp add: test_bit_bin)
  1022   done
  1023 
  1024 lemma ucast_up_ucast [OF refl]: "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
  1025   apply (simp (no_asm) add: ucast_def)
  1026   apply (clarsimp simp add: uint_up_ucast)
  1027   done
  1028 
  1029 lemma scast_up_scast [OF refl]: "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
  1030   apply (simp (no_asm) add: scast_def)
  1031   apply (clarsimp simp add: sint_up_scast)
  1032   done
  1033 
  1034 lemma ucast_of_bl_up [OF refl]: "w = of_bl bl \<Longrightarrow> size bl \<le> size w \<Longrightarrow> ucast w = of_bl bl"
  1035   by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
  1036 
  1037 lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]
  1038 lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id]
  1039 
  1040 lemmas isduu = is_up_down [where c = "ucast", THEN iffD2]
  1041 lemmas isdus = is_up_down [where c = "scast", THEN iffD2]
  1042 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id]
  1043 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
  1044 
  1045 lemma up_ucast_surj:
  1046   "is_up (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow>
  1047     surj (ucast :: 'a word \<Rightarrow> 'b word)"
  1048   by (rule surjI) (erule ucast_up_ucast_id)
  1049 
  1050 lemma up_scast_surj:
  1051   "is_up (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow>
  1052     surj (scast :: 'a word \<Rightarrow> 'b word)"
  1053   by (rule surjI) (erule scast_up_scast_id)
  1054 
  1055 lemma down_scast_inj:
  1056   "is_down (scast :: 'b::len word \<Rightarrow> 'a::len word) \<Longrightarrow>
  1057     inj_on (ucast :: 'a word \<Rightarrow> 'b word) A"
  1058   by (rule inj_on_inverseI, erule scast_down_scast_id)
  1059 
  1060 lemma down_ucast_inj:
  1061   "is_down (ucast :: 'b::len0 word \<Rightarrow> 'a::len0 word) \<Longrightarrow>
  1062     inj_on (ucast :: 'a word \<Rightarrow> 'b word) A"
  1063   by (rule inj_on_inverseI) (erule ucast_down_ucast_id)
  1064 
  1065 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
  1066   by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
  1067 
  1068 lemma ucast_down_wi [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (word_of_int x) = word_of_int x"
  1069   apply (unfold is_down)
  1070   apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
  1071   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
  1072   apply (erule bintrunc_bintrunc_ge)
  1073   done
  1074 
  1075 lemma ucast_down_no [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (numeral bin) = numeral bin"
  1076   unfolding word_numeral_alt by clarify (rule ucast_down_wi)
  1077 
  1078 lemma ucast_down_bl [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
  1079   unfolding of_bl_def by clarify (erule ucast_down_wi)
  1080 
  1081 lemmas slice_def' = slice_def [unfolded word_size]
  1082 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
  1083 
  1084 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
  1085 
  1086 
  1087 subsection \<open>Word Arithmetic\<close>
  1088 
  1089 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b"
  1090   by (fact word_less_def)
  1091 
  1092 lemma signed_linorder: "class.linorder word_sle word_sless"
  1093   by standard (auto simp: word_sle_def word_sless_def)
  1094 
  1095 interpretation signed: linorder "word_sle" "word_sless"
  1096   by (rule signed_linorder)
  1097 
  1098 lemma udvdI: "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
  1099   by (auto simp: udvd_def)
  1100 
  1101 lemmas word_div_no [simp] = word_div_def [of "numeral a" "numeral b"] for a b
  1102 lemmas word_mod_no [simp] = word_mod_def [of "numeral a" "numeral b"] for a b
  1103 lemmas word_less_no [simp] = word_less_def [of "numeral a" "numeral b"] for a b
  1104 lemmas word_le_no [simp] = word_le_def [of "numeral a" "numeral b"] for a b
  1105 lemmas word_sless_no [simp] = word_sless_def [of "numeral a" "numeral b"] for a b
  1106 lemmas word_sle_no [simp] = word_sle_def [of "numeral a" "numeral b"] for a b
  1107 
  1108 lemma word_m1_wi: "- 1 = word_of_int (- 1)"
  1109   by (simp add: word_neg_numeral_alt [of Num.One])
  1110 
  1111 lemma word_0_bl [simp]: "of_bl [] = 0"
  1112   by (simp add: of_bl_def)
  1113 
  1114 lemma word_1_bl: "of_bl [True] = 1"
  1115   by (simp add: of_bl_def bl_to_bin_def)
  1116 
  1117 lemma uint_eq_0 [simp]: "uint 0 = 0"
  1118   unfolding word_0_wi word_ubin.eq_norm by simp
  1119 
  1120 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
  1121   by (simp add: of_bl_def bl_to_bin_rep_False)
  1122 
  1123 lemma to_bl_0 [simp]: "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
  1124   by (simp add: uint_bl word_size bin_to_bl_zero)
  1125 
  1126 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
  1127   by (simp add: word_uint_eq_iff)
  1128 
  1129 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
  1130   by (auto simp: unat_def nat_eq_iff uint_0_iff)
  1131 
  1132 lemma unat_0 [simp]: "unat 0 = 0"
  1133   by (auto simp: unat_def)
  1134 
  1135 lemma size_0_same': "size w = 0 \<Longrightarrow> w = v"
  1136   for v w :: "'a::len0 word"
  1137   apply (unfold word_size)
  1138   apply (rule box_equals)
  1139     defer
  1140     apply (rule word_uint.Rep_inverse)+
  1141   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
  1142   apply simp
  1143   done
  1144 
  1145 lemmas size_0_same = size_0_same' [unfolded word_size]
  1146 
  1147 lemmas unat_eq_0 = unat_0_iff
  1148 lemmas unat_eq_zero = unat_0_iff
  1149 
  1150 lemma unat_gt_0: "0 < unat x \<longleftrightarrow> x \<noteq> 0"
  1151   by (auto simp: unat_0_iff [symmetric])
  1152 
  1153 lemma ucast_0 [simp]: "ucast 0 = 0"
  1154   by (simp add: ucast_def)
  1155 
  1156 lemma sint_0 [simp]: "sint 0 = 0"
  1157   by (simp add: sint_uint)
  1158 
  1159 lemma scast_0 [simp]: "scast 0 = 0"
  1160   by (simp add: scast_def)
  1161 
  1162 lemma sint_n1 [simp] : "sint (- 1) = - 1"
  1163   by (simp only: word_m1_wi word_sbin.eq_norm) simp
  1164 
  1165 lemma scast_n1 [simp]: "scast (- 1) = - 1"
  1166   by (simp add: scast_def)
  1167 
  1168 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
  1169   by (simp only: word_1_wi word_ubin.eq_norm) (simp add: bintrunc_minus_simps(4))
  1170 
  1171 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
  1172   by (simp add: unat_def)
  1173 
  1174 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
  1175   by (simp add: ucast_def)
  1176 
  1177 \<comment> \<open>now, to get the weaker results analogous to \<open>word_div\<close>/\<open>mod_def\<close>\<close>
  1178 
  1179 
  1180 subsection \<open>Transferring goals from words to ints\<close>
  1181 
  1182 lemma word_ths:
  1183   shows word_succ_p1: "word_succ a = a + 1"
  1184     and word_pred_m1: "word_pred a = a - 1"
  1185     and word_pred_succ: "word_pred (word_succ a) = a"
  1186     and word_succ_pred: "word_succ (word_pred a) = a"
  1187     and word_mult_succ: "word_succ a * b = b + a * b"
  1188   by (transfer, simp add: algebra_simps)+
  1189 
  1190 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
  1191   by simp
  1192 
  1193 lemma uint_word_ariths:
  1194   fixes a b :: "'a::len0 word"
  1195   shows "uint (a + b) = (uint a + uint b) mod 2 ^ len_of TYPE('a::len0)"
  1196     and "uint (a - b) = (uint a - uint b) mod 2 ^ len_of TYPE('a)"
  1197     and "uint (a * b) = uint a * uint b mod 2 ^ len_of TYPE('a)"
  1198     and "uint (- a) = - uint a mod 2 ^ len_of TYPE('a)"
  1199     and "uint (word_succ a) = (uint a + 1) mod 2 ^ len_of TYPE('a)"
  1200     and "uint (word_pred a) = (uint a - 1) mod 2 ^ len_of TYPE('a)"
  1201     and "uint (0 :: 'a word) = 0 mod 2 ^ len_of TYPE('a)"
  1202     and "uint (1 :: 'a word) = 1 mod 2 ^ len_of TYPE('a)"
  1203   by (simp_all add: word_arith_wis [THEN trans [OF uint_cong int_word_uint]])
  1204 
  1205 lemma uint_word_arith_bintrs:
  1206   fixes a b :: "'a::len0 word"
  1207   shows "uint (a + b) = bintrunc (len_of TYPE('a)) (uint a + uint b)"
  1208     and "uint (a - b) = bintrunc (len_of TYPE('a)) (uint a - uint b)"
  1209     and "uint (a * b) = bintrunc (len_of TYPE('a)) (uint a * uint b)"
  1210     and "uint (- a) = bintrunc (len_of TYPE('a)) (- uint a)"
  1211     and "uint (word_succ a) = bintrunc (len_of TYPE('a)) (uint a + 1)"
  1212     and "uint (word_pred a) = bintrunc (len_of TYPE('a)) (uint a - 1)"
  1213     and "uint (0 :: 'a word) = bintrunc (len_of TYPE('a)) 0"
  1214     and "uint (1 :: 'a word) = bintrunc (len_of TYPE('a)) 1"
  1215   by (simp_all add: uint_word_ariths bintrunc_mod2p)
  1216 
  1217 lemma sint_word_ariths:
  1218   fixes a b :: "'a::len word"
  1219   shows "sint (a + b) = sbintrunc (len_of TYPE('a) - 1) (sint a + sint b)"
  1220     and "sint (a - b) = sbintrunc (len_of TYPE('a) - 1) (sint a - sint b)"
  1221     and "sint (a * b) = sbintrunc (len_of TYPE('a) - 1) (sint a * sint b)"
  1222     and "sint (- a) = sbintrunc (len_of TYPE('a) - 1) (- sint a)"
  1223     and "sint (word_succ a) = sbintrunc (len_of TYPE('a) - 1) (sint a + 1)"
  1224     and "sint (word_pred a) = sbintrunc (len_of TYPE('a) - 1) (sint a - 1)"
  1225     and "sint (0 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 0"
  1226     and "sint (1 :: 'a word) = sbintrunc (len_of TYPE('a) - 1) 1"
  1227          apply (simp_all only: word_sbin.inverse_norm [symmetric])
  1228          apply (simp_all add: wi_hom_syms)
  1229    apply transfer apply simp
  1230   apply transfer apply simp
  1231   done
  1232 
  1233 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
  1234 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
  1235 
  1236 lemma word_pred_0_n1: "word_pred 0 = word_of_int (- 1)"
  1237   unfolding word_pred_m1 by simp
  1238 
  1239 lemma succ_pred_no [simp]:
  1240     "word_succ (numeral w) = numeral w + 1"
  1241     "word_pred (numeral w) = numeral w - 1"
  1242     "word_succ (- numeral w) = - numeral w + 1"
  1243     "word_pred (- numeral w) = - numeral w - 1"
  1244   by (simp_all add: word_succ_p1 word_pred_m1)
  1245 
  1246 lemma word_sp_01 [simp]:
  1247   "word_succ (- 1) = 0 \<and> word_succ 0 = 1 \<and> word_pred 0 = - 1 \<and> word_pred 1 = 0"
  1248   by (simp_all add: word_succ_p1 word_pred_m1)
  1249 
  1250 \<comment> \<open>alternative approach to lifting arithmetic equalities\<close>
  1251 lemma word_of_int_Ex: "\<exists>y. x = word_of_int y"
  1252   by (rule_tac x="uint x" in exI) simp
  1253 
  1254 
  1255 subsection \<open>Order on fixed-length words\<close>
  1256 
  1257 lemma word_zero_le [simp]: "0 \<le> y"
  1258   for y :: "'a::len0 word"
  1259   unfolding word_le_def by auto
  1260 
  1261 lemma word_m1_ge [simp] : "word_pred 0 \<ge> y" (* FIXME: delete *)
  1262   by (simp only: word_le_def word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
  1263 
  1264 lemma word_n1_ge [simp]: "y \<le> -1"
  1265   for y :: "'a::len0 word"
  1266   by (simp only: word_le_def word_m1_wi word_uint.eq_norm m1mod2k) auto
  1267 
  1268 lemmas word_not_simps [simp] =
  1269   word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
  1270 
  1271 lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> y"
  1272   for y :: "'a::len0 word"
  1273   by (simp add: less_le)
  1274 
  1275 lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
  1276 
  1277 lemma word_sless_alt: "a <s b \<longleftrightarrow> sint a < sint b"
  1278   by (auto simp add: word_sle_def word_sless_def less_le)
  1279 
  1280 lemma word_le_nat_alt: "a \<le> b \<longleftrightarrow> unat a \<le> unat b"
  1281   unfolding unat_def word_le_def
  1282   by (rule nat_le_eq_zle [symmetric]) simp
  1283 
  1284 lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
  1285   unfolding unat_def word_less_alt
  1286   by (rule nat_less_eq_zless [symmetric]) simp
  1287 
  1288 lemma wi_less:
  1289   "(word_of_int n < (word_of_int m :: 'a::len0 word)) =
  1290     (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
  1291   unfolding word_less_alt by (simp add: word_uint.eq_norm)
  1292 
  1293 lemma wi_le:
  1294   "(word_of_int n \<le> (word_of_int m :: 'a::len0 word)) =
  1295     (n mod 2 ^ len_of TYPE('a) \<le> m mod 2 ^ len_of TYPE('a))"
  1296   unfolding word_le_def by (simp add: word_uint.eq_norm)
  1297 
  1298 lemma udvd_nat_alt: "a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. unat b = n * unat a)"
  1299   apply (unfold udvd_def)
  1300   apply safe
  1301    apply (simp add: unat_def nat_mult_distrib)
  1302   apply (simp add: uint_nat)
  1303   apply (rule exI)
  1304   apply safe
  1305    prefer 2
  1306    apply (erule notE)
  1307    apply (rule refl)
  1308   apply force
  1309   done
  1310 
  1311 lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
  1312   unfolding dvd_def udvd_nat_alt by force
  1313 
  1314 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
  1315 
  1316 lemma unat_minus_one:
  1317   assumes "w \<noteq> 0"
  1318   shows "unat (w - 1) = unat w - 1"
  1319 proof -
  1320   have "0 \<le> uint w" by (fact uint_nonnegative)
  1321   moreover from assms have "0 \<noteq> uint w"
  1322     by (simp add: uint_0_iff)
  1323   ultimately have "1 \<le> uint w"
  1324     by arith
  1325   from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)"
  1326     by arith
  1327   with \<open>1 \<le> uint w\<close> have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
  1328     by (auto intro: mod_pos_pos_trivial)
  1329   with \<open>1 \<le> uint w\<close> have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
  1330     by auto
  1331   then show ?thesis
  1332     by (simp only: unat_def int_word_uint word_arith_wis mod_diff_right_eq)
  1333 qed
  1334 
  1335 lemma measure_unat: "p \<noteq> 0 \<Longrightarrow> unat (p - 1) < unat p"
  1336   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
  1337 
  1338 lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
  1339 lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
  1340 
  1341 lemma uint_sub_lt2p [simp]: "uint x - uint y < 2 ^ len_of TYPE('a)"
  1342   for x :: "'a::len0 word" and y :: "'b::len0 word"
  1343   using uint_ge_0 [of y] uint_lt2p [of x] by arith
  1344 
  1345 
  1346 subsection \<open>Conditions for the addition (etc) of two words to overflow\<close>
  1347 
  1348 lemma uint_add_lem:
  1349   "(uint x + uint y < 2 ^ len_of TYPE('a)) =
  1350     (uint (x + y) = uint x + uint y)"
  1351   for x y :: "'a::len0 word"
  1352   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
  1353 
  1354 lemma uint_mult_lem:
  1355   "(uint x * uint y < 2 ^ len_of TYPE('a)) =
  1356     (uint (x * y) = uint x * uint y)"
  1357   for x y :: "'a::len0 word"
  1358   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
  1359 
  1360 lemma uint_sub_lem: "uint x \<ge> uint y \<longleftrightarrow> uint (x - y) = uint x - uint y"
  1361   by (auto simp: uint_word_ariths intro!: trans [OF _ int_mod_lem])
  1362 
  1363 lemma uint_add_le: "uint (x + y) \<le> uint x + uint y"
  1364   unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
  1365 
  1366 lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
  1367   unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
  1368 
  1369 lemma mod_add_if_z:
  1370   "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
  1371     (x + y) mod z = (if x + y < z then x + y else x + y - z)"
  1372   for x y z :: int
  1373   by (auto intro: int_mod_eq)
  1374 
  1375 lemma uint_plus_if':
  1376   "uint (a + b) =
  1377     (if uint a + uint b < 2 ^ len_of TYPE('a) then uint a + uint b
  1378      else uint a + uint b - 2 ^ len_of TYPE('a))"
  1379   for a b :: "'a::len0 word"
  1380   using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
  1381 
  1382 lemma mod_sub_if_z:
  1383   "x < z \<Longrightarrow> y < z \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x \<Longrightarrow> 0 \<le> z \<Longrightarrow>
  1384     (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
  1385   for x y z :: int
  1386   by (auto intro: int_mod_eq)
  1387 
  1388 lemma uint_sub_if':
  1389   "uint (a - b) =
  1390     (if uint b \<le> uint a then uint a - uint b
  1391      else uint a - uint b + 2 ^ len_of TYPE('a))"
  1392   for a b :: "'a::len0 word"
  1393   using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
  1394 
  1395 
  1396 subsection \<open>Definition of \<open>uint_arith\<close>\<close>
  1397 
  1398 lemma word_of_int_inverse:
  1399   "word_of_int r = a \<Longrightarrow> 0 \<le> r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> uint a = r"
  1400   for a :: "'a::len0 word"
  1401   apply (erule word_uint.Abs_inverse' [rotated])
  1402   apply (simp add: uints_num)
  1403   done
  1404 
  1405 lemma uint_split:
  1406   "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('a) \<longrightarrow> P i)"
  1407   for x :: "'a::len0 word"
  1408   apply (fold word_int_case_def)
  1409   apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
  1410       split: word_int_split)
  1411   done
  1412 
  1413 lemma uint_split_asm:
  1414   "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^len_of TYPE('a) \<and> \<not> P i)"
  1415   for x :: "'a::len0 word"
  1416   by (auto dest!: word_of_int_inverse
  1417       simp: int_word_uint mod_pos_pos_trivial
  1418       split: uint_split)
  1419 
  1420 lemmas uint_splits = uint_split uint_split_asm
  1421 
  1422 lemmas uint_arith_simps =
  1423   word_le_def word_less_alt
  1424   word_uint.Rep_inject [symmetric]
  1425   uint_sub_if' uint_plus_if'
  1426 
  1427 \<comment> \<open>use this to stop, eg. \<open>2 ^ len_of TYPE(32)\<close> being simplified\<close>
  1428 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
  1429   by auto
  1430 
  1431 \<comment> \<open>\<open>uint_arith_tac\<close>: reduce to arithmetic on int, try to solve by arith\<close>
  1432 ML \<open>
  1433 fun uint_arith_simpset ctxt =
  1434   ctxt addsimps @{thms uint_arith_simps}
  1435      delsimps @{thms word_uint.Rep_inject}
  1436      |> fold Splitter.add_split @{thms if_split_asm}
  1437      |> fold Simplifier.add_cong @{thms power_False_cong}
  1438 
  1439 fun uint_arith_tacs ctxt =
  1440   let
  1441     fun arith_tac' n t =
  1442       Arith_Data.arith_tac ctxt n t
  1443         handle Cooper.COOPER _ => Seq.empty;
  1444   in
  1445     [ clarify_tac ctxt 1,
  1446       full_simp_tac (uint_arith_simpset ctxt) 1,
  1447       ALLGOALS (full_simp_tac
  1448         (put_simpset HOL_ss ctxt
  1449           |> fold Splitter.add_split @{thms uint_splits}
  1450           |> fold Simplifier.add_cong @{thms power_False_cong})),
  1451       rewrite_goals_tac ctxt @{thms word_size},
  1452       ALLGOALS  (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
  1453                          REPEAT (eresolve_tac ctxt [conjE] n) THEN
  1454                          REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n
  1455                                  THEN assume_tac ctxt n
  1456                                  THEN assume_tac ctxt n)),
  1457       TRYALL arith_tac' ]
  1458   end
  1459 
  1460 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
  1461 \<close>
  1462 
  1463 method_setup uint_arith =
  1464   \<open>Scan.succeed (SIMPLE_METHOD' o uint_arith_tac)\<close>
  1465   "solving word arithmetic via integers and arith"
  1466 
  1467 
  1468 subsection \<open>More on overflows and monotonicity\<close>
  1469 
  1470 lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
  1471   for x y :: "'a::len0 word"
  1472   unfolding word_size by uint_arith
  1473 
  1474 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
  1475 
  1476 lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
  1477   for x y :: "'a::len0 word"
  1478   by uint_arith
  1479 
  1480 lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ len_of TYPE('a)"
  1481   for x y :: "'a::len0 word"
  1482   by (simp add: ac_simps no_olen_add)
  1483 
  1484 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
  1485 
  1486 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem]
  1487 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1]
  1488 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem]
  1489 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
  1490 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
  1491 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
  1492 
  1493 lemma word_less_sub1: "x \<noteq> 0 \<Longrightarrow> 1 < x \<longleftrightarrow> 0 < x - 1"
  1494   for x :: "'a::len word"
  1495   by uint_arith
  1496 
  1497 lemma word_le_sub1: "x \<noteq> 0 \<Longrightarrow> 1 \<le> x \<longleftrightarrow> 0 \<le> x - 1"
  1498   for x :: "'a::len word"
  1499   by uint_arith
  1500 
  1501 lemma sub_wrap_lt: "x < x - z \<longleftrightarrow> x < z"
  1502   for x z :: "'a::len0 word"
  1503   by uint_arith
  1504 
  1505 lemma sub_wrap: "x \<le> x - z \<longleftrightarrow> z = 0 \<or> x < z"
  1506   for x z :: "'a::len0 word"
  1507   by uint_arith
  1508 
  1509 lemma plus_minus_not_NULL_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> x + c \<noteq> 0"
  1510   for x ab c :: "'a::len0 word"
  1511   by uint_arith
  1512 
  1513 lemma plus_minus_no_overflow_ab: "x \<le> ab - c \<Longrightarrow> c \<le> ab \<Longrightarrow> x \<le> x + c"
  1514   for x ab c :: "'a::len0 word"
  1515   by uint_arith
  1516 
  1517 lemma le_minus': "a + c \<le> b \<Longrightarrow> a \<le> a + c \<Longrightarrow> c \<le> b - a"
  1518   for a b c :: "'a::len0 word"
  1519   by uint_arith
  1520 
  1521 lemma le_plus': "a \<le> b \<Longrightarrow> c \<le> b - a \<Longrightarrow> a + c \<le> b"
  1522   for a b c :: "'a::len0 word"
  1523   by uint_arith
  1524 
  1525 lemmas le_plus = le_plus' [rotated]
  1526 
  1527 lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
  1528 
  1529 lemma word_plus_mono_right: "y \<le> z \<Longrightarrow> x \<le> x + z \<Longrightarrow> x + y \<le> x + z"
  1530   for x y z :: "'a::len0 word"
  1531   by uint_arith
  1532 
  1533 lemma word_less_minus_cancel: "y - x < z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y < z"
  1534   for x y z :: "'a::len0 word"
  1535   by uint_arith
  1536 
  1537 lemma word_less_minus_mono_left: "y < z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x < z - x"
  1538   for x y z :: "'a::len0 word"
  1539   by uint_arith
  1540 
  1541 lemma word_less_minus_mono: "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c \<Longrightarrow> a - b < c - d"
  1542   for a b c d :: "'a::len word"
  1543   by uint_arith
  1544 
  1545 lemma word_le_minus_cancel: "y - x \<le> z - x \<Longrightarrow> x \<le> z \<Longrightarrow> y \<le> z"
  1546   for x y z :: "'a::len0 word"
  1547   by uint_arith
  1548 
  1549 lemma word_le_minus_mono_left: "y \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> y - x \<le> z - x"
  1550   for x y z :: "'a::len0 word"
  1551   by uint_arith
  1552 
  1553 lemma word_le_minus_mono:
  1554   "a \<le> c \<Longrightarrow> d \<le> b \<Longrightarrow> a - b \<le> a \<Longrightarrow> c - d \<le> c \<Longrightarrow> a - b \<le> c - d"
  1555   for a b c d :: "'a::len word"
  1556   by uint_arith
  1557 
  1558 lemma plus_le_left_cancel_wrap: "x + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
  1559   for x y y' :: "'a::len0 word"
  1560   by uint_arith
  1561 
  1562 lemma plus_le_left_cancel_nowrap: "x \<le> x + y' \<Longrightarrow> x \<le> x + y \<Longrightarrow> x + y' < x + y \<longleftrightarrow> y' < y"
  1563   for x y y' :: "'a::len0 word"
  1564   by uint_arith
  1565 
  1566 lemma word_plus_mono_right2: "a \<le> a + b \<Longrightarrow> c \<le> b \<Longrightarrow> a \<le> a + c"
  1567   for a b c :: "'a::len0 word"
  1568   by uint_arith
  1569 
  1570 lemma word_less_add_right: "x < y - z \<Longrightarrow> z \<le> y \<Longrightarrow> x + z < y"
  1571   for x y z :: "'a::len0 word"
  1572   by uint_arith
  1573 
  1574 lemma word_less_sub_right: "x < y + z \<Longrightarrow> y \<le> x \<Longrightarrow> x - y < z"
  1575   for x y z :: "'a::len0 word"
  1576   by uint_arith
  1577 
  1578 lemma word_le_plus_either: "x \<le> y \<or> x \<le> z \<Longrightarrow> y \<le> y + z \<Longrightarrow> x \<le> y + z"
  1579   for x y z :: "'a::len0 word"
  1580   by uint_arith
  1581 
  1582 lemma word_less_nowrapI: "x < z - k \<Longrightarrow> k \<le> z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
  1583   for x z k :: "'a::len0 word"
  1584   by uint_arith
  1585 
  1586 lemma inc_le: "i < m \<Longrightarrow> i + 1 \<le> m"
  1587   for i m :: "'a::len word"
  1588   by uint_arith
  1589 
  1590 lemma inc_i: "1 \<le> i \<Longrightarrow> i < m \<Longrightarrow> 1 \<le> i + 1 \<and> i + 1 \<le> m"
  1591   for i m :: "'a::len word"
  1592   by uint_arith
  1593 
  1594 lemma udvd_incr_lem:
  1595   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
  1596     uq = ua + n' * uint K \<Longrightarrow> up + uint K \<le> uq"
  1597   apply clarsimp
  1598   apply (drule less_le_mult)
  1599    apply safe
  1600   done
  1601 
  1602 lemma udvd_incr':
  1603   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
  1604     uint q = ua + n' * uint K \<Longrightarrow> p + K \<le> q"
  1605   apply (unfold word_less_alt word_le_def)
  1606   apply (drule (2) udvd_incr_lem)
  1607   apply (erule uint_add_le [THEN order_trans])
  1608   done
  1609 
  1610 lemma udvd_decr':
  1611   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
  1612     uint q = ua + n' * uint K \<Longrightarrow> p \<le> q - K"
  1613   apply (unfold word_less_alt word_le_def)
  1614   apply (drule (2) udvd_incr_lem)
  1615   apply (drule le_diff_eq [THEN iffD2])
  1616   apply (erule order_trans)
  1617   apply (rule uint_sub_ge)
  1618   done
  1619 
  1620 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
  1621 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
  1622 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
  1623 
  1624 lemma udvd_minus_le': "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy \<le> k - z"
  1625   apply (unfold udvd_def)
  1626   apply clarify
  1627   apply (erule (2) udvd_decr0)
  1628   done
  1629 
  1630 lemma udvd_incr2_K:
  1631   "p < a + s \<Longrightarrow> a \<le> a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a \<le> p \<Longrightarrow>
  1632     0 < K \<Longrightarrow> p \<le> p + K \<and> p + K \<le> a + s"
  1633   supply [[simproc del: linordered_ring_less_cancel_factor]]
  1634   apply (unfold udvd_def)
  1635   apply clarify
  1636   apply (simp add: uint_arith_simps split: if_split_asm)
  1637    prefer 2
  1638    apply (insert uint_range' [of s])[1]
  1639    apply arith
  1640   apply (drule add.commute [THEN xtr1])
  1641   apply (simp add: diff_less_eq [symmetric])
  1642   apply (drule less_le_mult)
  1643    apply arith
  1644   apply simp
  1645   done
  1646 
  1647 \<comment> \<open>links with \<open>rbl\<close> operations\<close>
  1648 lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
  1649   apply (unfold word_succ_def)
  1650   apply clarify
  1651   apply (simp add: to_bl_of_bin)
  1652   apply (simp add: to_bl_def rbl_succ)
  1653   done
  1654 
  1655 lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
  1656   apply (unfold word_pred_def)
  1657   apply clarify
  1658   apply (simp add: to_bl_of_bin)
  1659   apply (simp add: to_bl_def rbl_pred)
  1660   done
  1661 
  1662 lemma word_add_rbl:
  1663   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
  1664     to_bl (v + w) = rev (rbl_add (rev vbl) (rev wbl))"
  1665   apply (unfold word_add_def)
  1666   apply clarify
  1667   apply (simp add: to_bl_of_bin)
  1668   apply (simp add: to_bl_def rbl_add)
  1669   done
  1670 
  1671 lemma word_mult_rbl:
  1672   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
  1673     to_bl (v * w) = rev (rbl_mult (rev vbl) (rev wbl))"
  1674   apply (unfold word_mult_def)
  1675   apply clarify
  1676   apply (simp add: to_bl_of_bin)
  1677   apply (simp add: to_bl_def rbl_mult)
  1678   done
  1679 
  1680 lemma rtb_rbl_ariths:
  1681   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
  1682   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
  1683   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
  1684   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
  1685   by (auto simp: rev_swap [symmetric] word_succ_rbl word_pred_rbl word_mult_rbl word_add_rbl)
  1686 
  1687 
  1688 subsection \<open>Arithmetic type class instantiations\<close>
  1689 
  1690 lemmas word_le_0_iff [simp] =
  1691   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
  1692 
  1693 lemma word_of_int_nat: "0 \<le> x \<Longrightarrow> word_of_int x = of_nat (nat x)"
  1694   by (simp add: word_of_int)
  1695 
  1696 text \<open>
  1697   note that \<open>iszero_def\<close> is only for class \<open>comm_semiring_1_cancel\<close>,
  1698   which requires word length \<open>\<ge> 1\<close>, ie \<open>'a::len word\<close>
  1699 \<close>
  1700 lemma iszero_word_no [simp]:
  1701   "iszero (numeral bin :: 'a::len word) =
  1702     iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
  1703   using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
  1704   by (simp add: iszero_def [symmetric])
  1705 
  1706 text \<open>Use \<open>iszero\<close> to simplify equalities between word numerals.\<close>
  1707 
  1708 lemmas word_eq_numeral_iff_iszero [simp] =
  1709   eq_numeral_iff_iszero [where 'a="'a::len word"]
  1710 
  1711 
  1712 subsection \<open>Word and nat\<close>
  1713 
  1714 lemma td_ext_unat [OF refl]:
  1715   "n = len_of TYPE('a::len) \<Longrightarrow>
  1716     td_ext (unat :: 'a word \<Rightarrow> nat) of_nat (unats n) (\<lambda>i. i mod 2 ^ n)"
  1717   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
  1718   apply (auto intro!: imageI simp add : word_of_int_hom_syms)
  1719    apply (erule word_uint.Abs_inverse [THEN arg_cong])
  1720   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
  1721   done
  1722 
  1723 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
  1724 
  1725 interpretation word_unat:
  1726   td_ext
  1727     "unat::'a::len word \<Rightarrow> nat"
  1728     of_nat
  1729     "unats (len_of TYPE('a::len))"
  1730     "\<lambda>i. i mod 2 ^ len_of TYPE('a::len)"
  1731   by (rule td_ext_unat)
  1732 
  1733 lemmas td_unat = word_unat.td_thm
  1734 
  1735 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
  1736 
  1737 lemma unat_le: "y \<le> unat z \<Longrightarrow> y \<in> unats (len_of TYPE('a))"
  1738   for z :: "'a::len word"
  1739   apply (unfold unats_def)
  1740   apply clarsimp
  1741   apply (rule xtrans, rule unat_lt2p, assumption)
  1742   done
  1743 
  1744 lemma word_nchotomy: "\<forall>w :: 'a::len word. \<exists>n. w = of_nat n \<and> n < 2 ^ len_of TYPE('a)"
  1745   apply (rule allI)
  1746   apply (rule word_unat.Abs_cases)
  1747   apply (unfold unats_def)
  1748   apply auto
  1749   done
  1750 
  1751 lemma of_nat_eq: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
  1752   for w :: "'a::len word"
  1753   using mod_div_mult_eq [of n "2 ^ LENGTH('a)", symmetric]
  1754   by (auto simp add: word_unat.inverse_norm)
  1755 
  1756 lemma of_nat_eq_size: "of_nat n = w \<longleftrightarrow> (\<exists>q. n = unat w + q * 2 ^ size w)"
  1757   unfolding word_size by (rule of_nat_eq)
  1758 
  1759 lemma of_nat_0: "of_nat m = (0::'a::len word) \<longleftrightarrow> (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
  1760   by (simp add: of_nat_eq)
  1761 
  1762 lemma of_nat_2p [simp]: "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
  1763   by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
  1764 
  1765 lemma of_nat_gt_0: "of_nat k \<noteq> 0 \<Longrightarrow> 0 < k"
  1766   by (cases k) auto
  1767 
  1768 lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
  1769   by (auto simp add : of_nat_0)
  1770 
  1771 lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)"
  1772   by simp
  1773 
  1774 lemma Abs_fnat_hom_mult: "of_nat a * of_nat b = (of_nat (a * b) :: 'a::len word)"
  1775   by (simp add: word_of_nat wi_hom_mult)
  1776 
  1777 lemma Abs_fnat_hom_Suc: "word_succ (of_nat a) = of_nat (Suc a)"
  1778   by (simp add: word_of_nat wi_hom_succ ac_simps)
  1779 
  1780 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
  1781   by simp
  1782 
  1783 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
  1784   by simp
  1785 
  1786 lemmas Abs_fnat_homs =
  1787   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
  1788   Abs_fnat_hom_0 Abs_fnat_hom_1
  1789 
  1790 lemma word_arith_nat_add: "a + b = of_nat (unat a + unat b)"
  1791   by simp
  1792 
  1793 lemma word_arith_nat_mult: "a * b = of_nat (unat a * unat b)"
  1794   by simp
  1795 
  1796 lemma word_arith_nat_Suc: "word_succ a = of_nat (Suc (unat a))"
  1797   by (subst Abs_fnat_hom_Suc [symmetric]) simp
  1798 
  1799 lemma word_arith_nat_div: "a div b = of_nat (unat a div unat b)"
  1800   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
  1801 
  1802 lemma word_arith_nat_mod: "a mod b = of_nat (unat a mod unat b)"
  1803   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
  1804 
  1805 lemmas word_arith_nat_defs =
  1806   word_arith_nat_add word_arith_nat_mult
  1807   word_arith_nat_Suc Abs_fnat_hom_0
  1808   Abs_fnat_hom_1 word_arith_nat_div
  1809   word_arith_nat_mod
  1810 
  1811 lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
  1812   by simp
  1813 
  1814 lemmas unat_word_ariths = word_arith_nat_defs
  1815   [THEN trans [OF unat_cong unat_of_nat]]
  1816 
  1817 lemmas word_sub_less_iff = word_sub_le_iff
  1818   [unfolded linorder_not_less [symmetric] Not_eq_iff]
  1819 
  1820 lemma unat_add_lem:
  1821   "unat x + unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x + y) = unat x + unat y"
  1822   for x y :: "'a::len word"
  1823   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
  1824 
  1825 lemma unat_mult_lem:
  1826   "unat x * unat y < 2 ^ len_of TYPE('a) \<longleftrightarrow> unat (x * y) = unat x * unat y"
  1827   for x y :: "'a::len word"
  1828   by (auto simp: unat_word_ariths intro!: trans [OF _ nat_mod_lem])
  1829 
  1830 lemmas unat_plus_if' =
  1831   trans [OF unat_word_ariths(1) mod_nat_add, simplified]
  1832 
  1833 lemma le_no_overflow: "x \<le> b \<Longrightarrow> a \<le> a + b \<Longrightarrow> x \<le> a + b"
  1834   for a b x :: "'a::len0 word"
  1835   apply (erule order_trans)
  1836   apply (erule olen_add_eqv [THEN iffD1])
  1837   done
  1838 
  1839 lemmas un_ui_le =
  1840   trans [OF word_le_nat_alt [symmetric] word_le_def]
  1841 
  1842 lemma unat_sub_if_size:
  1843   "unat (x - y) =
  1844     (if unat y \<le> unat x
  1845      then unat x - unat y
  1846      else unat x + 2 ^ size x - unat y)"
  1847   apply (unfold word_size)
  1848   apply (simp add: un_ui_le)
  1849   apply (auto simp add: unat_def uint_sub_if')
  1850    apply (rule nat_diff_distrib)
  1851     prefer 3
  1852     apply (simp add: algebra_simps)
  1853     apply (rule nat_diff_distrib [THEN trans])
  1854       prefer 3
  1855       apply (subst nat_add_distrib)
  1856         prefer 3
  1857         apply (simp add: nat_power_eq)
  1858        apply auto
  1859   apply uint_arith
  1860   done
  1861 
  1862 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
  1863 
  1864 lemma unat_div: "unat (x div y) = unat x div unat y"
  1865   for x y :: " 'a::len word"
  1866   apply (simp add : unat_word_ariths)
  1867   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1868   apply (rule div_le_dividend)
  1869   done
  1870 
  1871 lemma unat_mod: "unat (x mod y) = unat x mod unat y"
  1872   for x y :: "'a::len word"
  1873   apply (clarsimp simp add : unat_word_ariths)
  1874   apply (cases "unat y")
  1875    prefer 2
  1876    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1877    apply (rule mod_le_divisor)
  1878    apply auto
  1879   done
  1880 
  1881 lemma uint_div: "uint (x div y) = uint x div uint y"
  1882   for x y :: "'a::len word"
  1883   by (simp add: uint_nat unat_div zdiv_int)
  1884 
  1885 lemma uint_mod: "uint (x mod y) = uint x mod uint y"
  1886   for x y :: "'a::len word"
  1887   by (simp add: uint_nat unat_mod zmod_int)
  1888 
  1889 
  1890 subsection \<open>Definition of \<open>unat_arith\<close> tactic\<close>
  1891 
  1892 lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<longrightarrow> P n)"
  1893   for x :: "'a::len word"
  1894   by (auto simp: unat_of_nat)
  1895 
  1896 lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^len_of TYPE('a) \<and> \<not> P n)"
  1897   for x :: "'a::len word"
  1898   by (auto simp: unat_of_nat)
  1899 
  1900 lemmas of_nat_inverse =
  1901   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
  1902 
  1903 lemmas unat_splits = unat_split unat_split_asm
  1904 
  1905 lemmas unat_arith_simps =
  1906   word_le_nat_alt word_less_nat_alt
  1907   word_unat.Rep_inject [symmetric]
  1908   unat_sub_if' unat_plus_if' unat_div unat_mod
  1909 
  1910 \<comment> \<open>\<open>unat_arith_tac\<close>: tactic to reduce word arithmetic to \<open>nat\<close>, try to solve via \<open>arith\<close>\<close>
  1911 ML \<open>
  1912 fun unat_arith_simpset ctxt =
  1913   ctxt addsimps @{thms unat_arith_simps}
  1914      delsimps @{thms word_unat.Rep_inject}
  1915      |> fold Splitter.add_split @{thms if_split_asm}
  1916      |> fold Simplifier.add_cong @{thms power_False_cong}
  1917 
  1918 fun unat_arith_tacs ctxt =
  1919   let
  1920     fun arith_tac' n t =
  1921       Arith_Data.arith_tac ctxt n t
  1922         handle Cooper.COOPER _ => Seq.empty;
  1923   in
  1924     [ clarify_tac ctxt 1,
  1925       full_simp_tac (unat_arith_simpset ctxt) 1,
  1926       ALLGOALS (full_simp_tac
  1927         (put_simpset HOL_ss ctxt
  1928           |> fold Splitter.add_split @{thms unat_splits}
  1929           |> fold Simplifier.add_cong @{thms power_False_cong})),
  1930       rewrite_goals_tac ctxt @{thms word_size},
  1931       ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN
  1932                          REPEAT (eresolve_tac ctxt [conjE] n) THEN
  1933                          REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)),
  1934       TRYALL arith_tac' ]
  1935   end
  1936 
  1937 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
  1938 \<close>
  1939 
  1940 method_setup unat_arith =
  1941   \<open>Scan.succeed (SIMPLE_METHOD' o unat_arith_tac)\<close>
  1942   "solving word arithmetic via natural numbers and arith"
  1943 
  1944 lemma no_plus_overflow_unat_size: "x \<le> x + y \<longleftrightarrow> unat x + unat y < 2 ^ size x"
  1945   for x y :: "'a::len word"
  1946   unfolding word_size by unat_arith
  1947 
  1948 lemmas no_olen_add_nat =
  1949   no_plus_overflow_unat_size [unfolded word_size]
  1950 
  1951 lemmas unat_plus_simple =
  1952   trans [OF no_olen_add_nat unat_add_lem]
  1953 
  1954 lemma word_div_mult: "0 < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> x * y div y = x"
  1955   for x y :: "'a::len word"
  1956   apply unat_arith
  1957   apply clarsimp
  1958   apply (subst unat_mult_lem [THEN iffD1])
  1959    apply auto
  1960   done
  1961 
  1962 lemma div_lt': "i \<le> k div x \<Longrightarrow> unat i * unat x < 2 ^ len_of TYPE('a)"
  1963   for i k x :: "'a::len word"
  1964   apply unat_arith
  1965   apply clarsimp
  1966   apply (drule mult_le_mono1)
  1967   apply (erule order_le_less_trans)
  1968   apply (rule xtr7 [OF unat_lt2p div_mult_le])
  1969   done
  1970 
  1971 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
  1972 
  1973 lemma div_lt_mult: "i < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
  1974   for i k x :: "'a::len word"
  1975   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
  1976   apply (simp add: unat_arith_simps)
  1977   apply (drule (1) mult_less_mono1)
  1978   apply (erule order_less_le_trans)
  1979   apply (rule div_mult_le)
  1980   done
  1981 
  1982 lemma div_le_mult: "i \<le> k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x \<le> k"
  1983   for i k x :: "'a::len word"
  1984   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
  1985   apply (simp add: unat_arith_simps)
  1986   apply (drule mult_le_mono1)
  1987   apply (erule order_trans)
  1988   apply (rule div_mult_le)
  1989   done
  1990 
  1991 lemma div_lt_uint': "i \<le> k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
  1992   for i k x :: "'a::len word"
  1993   apply (unfold uint_nat)
  1994   apply (drule div_lt')
  1995   apply (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
  1996   done
  1997 
  1998 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
  1999 
  2000 lemma word_le_exists': "x \<le> y \<Longrightarrow> \<exists>z. y = x + z \<and> uint x + uint z < 2 ^ len_of TYPE('a)"
  2001   for x y z :: "'a::len0 word"
  2002   apply (rule exI)
  2003   apply (rule conjI)
  2004    apply (rule zadd_diff_inverse)
  2005   apply uint_arith
  2006   done
  2007 
  2008 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
  2009 
  2010 lemmas plus_minus_no_overflow =
  2011   order_less_imp_le [THEN plus_minus_no_overflow_ab]
  2012 
  2013 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
  2014   word_le_minus_cancel word_le_minus_mono_left
  2015 
  2016 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x
  2017 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
  2018 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
  2019 
  2020 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
  2021 
  2022 lemmas thd = times_div_less_eq_dividend
  2023 
  2024 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
  2025 
  2026 lemma word_mod_div_equality: "(n div b) * b + (n mod b) = n"
  2027   for n b :: "'a::len word"
  2028   apply (unfold word_less_nat_alt word_arith_nat_defs)
  2029   apply (cut_tac y="unat b" in gt_or_eq_0)
  2030   apply (erule disjE)
  2031    apply (simp only: div_mult_mod_eq uno_simps Word.word_unat.Rep_inverse)
  2032   apply simp
  2033   done
  2034 
  2035 lemma word_div_mult_le: "a div b * b \<le> a"
  2036   for a b :: "'a::len word"
  2037   apply (unfold word_le_nat_alt word_arith_nat_defs)
  2038   apply (cut_tac y="unat b" in gt_or_eq_0)
  2039   apply (erule disjE)
  2040    apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
  2041   apply simp
  2042   done
  2043 
  2044 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < n"
  2045   for m n :: "'a::len word"
  2046   apply (simp only: word_less_nat_alt word_arith_nat_defs)
  2047   apply (auto simp: uno_simps)
  2048   done
  2049 
  2050 lemma word_of_int_power_hom: "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a::len word)"
  2051   by (induct n) (simp_all add: wi_hom_mult [symmetric])
  2052 
  2053 lemma word_arith_power_alt: "a ^ n = (word_of_int (uint a ^ n) :: 'a::len word)"
  2054   by (simp add : word_of_int_power_hom [symmetric])
  2055 
  2056 lemma of_bl_length_less:
  2057   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a::len word) < 2 ^ k"
  2058   apply (unfold of_bl_def word_less_alt word_numeral_alt)
  2059   apply safe
  2060   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
  2061       del: word_of_int_numeral)
  2062   apply (simp add: mod_pos_pos_trivial)
  2063   apply (subst mod_pos_pos_trivial)
  2064     apply (rule bl_to_bin_ge0)
  2065    apply (rule order_less_trans)
  2066     apply (rule bl_to_bin_lt2p)
  2067    apply simp
  2068   apply (rule bl_to_bin_lt2p)
  2069   done
  2070 
  2071 
  2072 subsection \<open>Cardinality, finiteness of set of words\<close>
  2073 
  2074 instance word :: (len0) finite
  2075   by standard (simp add: type_definition.univ [OF type_definition_word])
  2076 
  2077 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
  2078   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
  2079 
  2080 lemma card_word_size: "card (UNIV :: 'a word set) = (2 ^ size x)"
  2081   for x :: "'a::len0 word"
  2082   unfolding word_size by (rule card_word)
  2083 
  2084 
  2085 subsection \<open>Bitwise Operations on Words\<close>
  2086 
  2087 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
  2088 
  2089 \<comment> \<open>following definitions require both arithmetic and bit-wise word operations\<close>
  2090 
  2091 \<comment> \<open>to get \<open>word_no_log_defs\<close> from \<open>word_log_defs\<close>, using \<open>bin_log_bintrs\<close>\<close>
  2092 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
  2093   folded word_ubin.eq_norm, THEN eq_reflection]
  2094 
  2095 \<comment> \<open>the binary operations only\<close>  (* BH: why is this needed? *)
  2096 lemmas word_log_binary_defs =
  2097   word_and_def word_or_def word_xor_def
  2098 
  2099 lemma word_wi_log_defs:
  2100   "NOT word_of_int a = word_of_int (NOT a)"
  2101   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
  2102   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
  2103   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
  2104   by (transfer, rule refl)+
  2105 
  2106 lemma word_no_log_defs [simp]:
  2107   "NOT (numeral a) = word_of_int (NOT (numeral a))"
  2108   "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
  2109   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
  2110   "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
  2111   "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
  2112   "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
  2113   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
  2114   "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
  2115   "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
  2116   "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
  2117   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
  2118   "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
  2119   "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
  2120   "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
  2121   by (transfer, rule refl)+
  2122 
  2123 text \<open>Special cases for when one of the arguments equals 1.\<close>
  2124 
  2125 lemma word_bitwise_1_simps [simp]:
  2126   "NOT (1::'a::len0 word) = -2"
  2127   "1 AND numeral b = word_of_int (1 AND numeral b)"
  2128   "1 AND - numeral b = word_of_int (1 AND - numeral b)"
  2129   "numeral a AND 1 = word_of_int (numeral a AND 1)"
  2130   "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
  2131   "1 OR numeral b = word_of_int (1 OR numeral b)"
  2132   "1 OR - numeral b = word_of_int (1 OR - numeral b)"
  2133   "numeral a OR 1 = word_of_int (numeral a OR 1)"
  2134   "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
  2135   "1 XOR numeral b = word_of_int (1 XOR numeral b)"
  2136   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
  2137   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
  2138   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
  2139   by (transfer, simp)+
  2140 
  2141 text \<open>Special cases for when one of the arguments equals -1.\<close>
  2142 
  2143 lemma word_bitwise_m1_simps [simp]:
  2144   "NOT (-1::'a::len0 word) = 0"
  2145   "(-1::'a::len0 word) AND x = x"
  2146   "x AND (-1::'a::len0 word) = x"
  2147   "(-1::'a::len0 word) OR x = -1"
  2148   "x OR (-1::'a::len0 word) = -1"
  2149   " (-1::'a::len0 word) XOR x = NOT x"
  2150   "x XOR (-1::'a::len0 word) = NOT x"
  2151   by (transfer, simp)+
  2152 
  2153 lemma uint_or: "uint (x OR y) = uint x OR uint y"
  2154   by (transfer, simp add: bin_trunc_ao)
  2155 
  2156 lemma uint_and: "uint (x AND y) = uint x AND uint y"
  2157   by (transfer, simp add: bin_trunc_ao)
  2158 
  2159 lemma test_bit_wi [simp]:
  2160   "(word_of_int x :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
  2161   by (simp add: word_test_bit_def word_ubin.eq_norm nth_bintr)
  2162 
  2163 lemma word_test_bit_transfer [transfer_rule]:
  2164   "(rel_fun pcr_word (rel_fun (=) (=)))
  2165     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
  2166   unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
  2167 
  2168 lemma word_ops_nth_size:
  2169   "n < size x \<Longrightarrow>
  2170     (x OR y) !! n = (x !! n | y !! n) \<and>
  2171     (x AND y) !! n = (x !! n \<and> y !! n) \<and>
  2172     (x XOR y) !! n = (x !! n \<noteq> y !! n) \<and>
  2173     (NOT x) !! n = (\<not> x !! n)"
  2174   for x :: "'a::len0 word"
  2175   unfolding word_size by transfer (simp add: bin_nth_ops)
  2176 
  2177 lemma word_ao_nth:
  2178   "(x OR y) !! n = (x !! n | y !! n) \<and>
  2179     (x AND y) !! n = (x !! n \<and> y !! n)"
  2180   for x :: "'a::len0 word"
  2181   by transfer (auto simp add: bin_nth_ops)
  2182 
  2183 lemma test_bit_numeral [simp]:
  2184   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2185     n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
  2186   by transfer (rule refl)
  2187 
  2188 lemma test_bit_neg_numeral [simp]:
  2189   "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2190     n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
  2191   by transfer (rule refl)
  2192 
  2193 lemma test_bit_1 [simp]: "(1 :: 'a::len word) !! n \<longleftrightarrow> n = 0"
  2194   by transfer auto
  2195 
  2196 lemma nth_0 [simp]: "\<not> (0 :: 'a::len0 word) !! n"
  2197   by transfer simp
  2198 
  2199 lemma nth_minus1 [simp]: "(-1 :: 'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  2200   by transfer simp
  2201 
  2202 \<comment> \<open>get from commutativity, associativity etc of \<open>int_and\<close> etc to same for \<open>word_and etc\<close>\<close>
  2203 lemmas bwsimps =
  2204   wi_hom_add
  2205   word_wi_log_defs
  2206 
  2207 lemma word_bw_assocs:
  2208   "(x AND y) AND z = x AND y AND z"
  2209   "(x OR y) OR z = x OR y OR z"
  2210   "(x XOR y) XOR z = x XOR y XOR z"
  2211   for x :: "'a::len0 word"
  2212   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2213 
  2214 lemma word_bw_comms:
  2215   "x AND y = y AND x"
  2216   "x OR y = y OR x"
  2217   "x XOR y = y XOR x"
  2218   for x :: "'a::len0 word"
  2219   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2220 
  2221 lemma word_bw_lcs:
  2222   "y AND x AND z = x AND y AND z"
  2223   "y OR x OR z = x OR y OR z"
  2224   "y XOR x XOR z = x XOR y XOR z"
  2225   for x :: "'a::len0 word"
  2226   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2227 
  2228 lemma word_log_esimps [simp]:
  2229   "x AND 0 = 0"
  2230   "x AND -1 = x"
  2231   "x OR 0 = x"
  2232   "x OR -1 = -1"
  2233   "x XOR 0 = x"
  2234   "x XOR -1 = NOT x"
  2235   "0 AND x = 0"
  2236   "-1 AND x = x"
  2237   "0 OR x = x"
  2238   "-1 OR x = -1"
  2239   "0 XOR x = x"
  2240   "-1 XOR x = NOT x"
  2241   for x :: "'a::len0 word"
  2242   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2243 
  2244 lemma word_not_dist:
  2245   "NOT (x OR y) = NOT x AND NOT y"
  2246   "NOT (x AND y) = NOT x OR NOT y"
  2247   for x :: "'a::len0 word"
  2248   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2249 
  2250 lemma word_bw_same:
  2251   "x AND x = x"
  2252   "x OR x = x"
  2253   "x XOR x = 0"
  2254   for x :: "'a::len0 word"
  2255   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2256 
  2257 lemma word_ao_absorbs [simp]:
  2258   "x AND (y OR x) = x"
  2259   "x OR y AND x = x"
  2260   "x AND (x OR y) = x"
  2261   "y AND x OR x = x"
  2262   "(y OR x) AND x = x"
  2263   "x OR x AND y = x"
  2264   "(x OR y) AND x = x"
  2265   "x AND y OR x = x"
  2266   for x :: "'a::len0 word"
  2267   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2268 
  2269 lemma word_not_not [simp]: "NOT NOT x = x"
  2270   for x :: "'a::len0 word"
  2271   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2272 
  2273 lemma word_ao_dist: "(x OR y) AND z = x AND z OR y AND z"
  2274   for x :: "'a::len0 word"
  2275   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2276 
  2277 lemma word_oa_dist: "x AND y OR z = (x OR z) AND (y OR z)"
  2278   for x :: "'a::len0 word"
  2279   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2280 
  2281 lemma word_add_not [simp]: "x + NOT x = -1"
  2282   for x :: "'a::len0 word"
  2283   by transfer (simp add: bin_add_not)
  2284 
  2285 lemma word_plus_and_or [simp]: "(x AND y) + (x OR y) = x + y"
  2286   for x :: "'a::len0 word"
  2287   by transfer (simp add: plus_and_or)
  2288 
  2289 lemma leoa: "w = x OR y \<Longrightarrow> y = w AND y"
  2290   for x :: "'a::len0 word"
  2291   by auto
  2292 
  2293 lemma leao: "w' = x' AND y' \<Longrightarrow> x' = x' OR w'"
  2294   for x' :: "'a::len0 word"
  2295   by auto
  2296 
  2297 lemma word_ao_equiv: "w = w OR w' \<longleftrightarrow> w' = w AND w'"
  2298   for w w' :: "'a::len0 word"
  2299   by (auto intro: leoa leao)
  2300 
  2301 lemma le_word_or2: "x \<le> x OR y"
  2302   for x y :: "'a::len0 word"
  2303   by (auto simp: word_le_def uint_or intro: le_int_or)
  2304 
  2305 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
  2306 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
  2307 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
  2308 
  2309 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
  2310   unfolding to_bl_def word_log_defs bl_not_bin
  2311   by (simp add: word_ubin.eq_norm)
  2312 
  2313 lemma bl_word_xor: "to_bl (v XOR w) = map2 (\<noteq>) (to_bl v) (to_bl w)"
  2314   unfolding to_bl_def word_log_defs bl_xor_bin
  2315   by (simp add: word_ubin.eq_norm)
  2316 
  2317 lemma bl_word_or: "to_bl (v OR w) = map2 (\<or>) (to_bl v) (to_bl w)"
  2318   unfolding to_bl_def word_log_defs bl_or_bin
  2319   by (simp add: word_ubin.eq_norm)
  2320 
  2321 lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)"
  2322   unfolding to_bl_def word_log_defs bl_and_bin
  2323   by (simp add: word_ubin.eq_norm)
  2324 
  2325 lemma word_lsb_alt: "lsb w = test_bit w 0"
  2326   for w :: "'a::len0 word"
  2327   by (auto simp: word_test_bit_def word_lsb_def)
  2328 
  2329 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
  2330   unfolding word_lsb_def uint_eq_0 uint_1 by simp
  2331 
  2332 lemma word_lsb_last: "lsb w = last (to_bl w)"
  2333   for w :: "'a::len word"
  2334   apply (unfold word_lsb_def uint_bl bin_to_bl_def)
  2335   apply (rule_tac bin="uint w" in bin_exhaust)
  2336   apply (cases "size w")
  2337    apply auto
  2338    apply (auto simp add: bin_to_bl_aux_alt)
  2339   done
  2340 
  2341 lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
  2342   by (auto simp: word_lsb_def bin_last_def)
  2343 
  2344 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
  2345   by (simp only: word_msb_def sign_Min_lt_0)
  2346 
  2347 lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  2348   by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
  2349 
  2350 lemma word_msb_numeral [simp]:
  2351   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  2352   unfolding word_numeral_alt by (rule msb_word_of_int)
  2353 
  2354 lemma word_msb_neg_numeral [simp]:
  2355   "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
  2356   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  2357 
  2358 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  2359   by (simp add: word_msb_def)
  2360 
  2361 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  2362   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  2363   by (simp add: Suc_le_eq)
  2364 
  2365 lemma word_msb_nth: "msb w = bin_nth (uint w) (len_of TYPE('a) - 1)"
  2366   for w :: "'a::len word"
  2367   by (simp add: word_msb_def sint_uint bin_sign_lem)
  2368 
  2369 lemma word_msb_alt: "msb w = hd (to_bl w)"
  2370   for w :: "'a::len word"
  2371   apply (unfold word_msb_nth uint_bl)
  2372   apply (subst hd_conv_nth)
  2373    apply (rule length_greater_0_conv [THEN iffD1])
  2374    apply simp
  2375   apply (simp add : nth_bin_to_bl word_size)
  2376   done
  2377 
  2378 lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
  2379   for w :: "'a::len0 word"
  2380   by (auto simp: word_test_bit_def word_set_bit_def)
  2381 
  2382 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
  2383   apply (unfold word_size)
  2384   apply (safe elim!: bin_nth_uint_imp)
  2385    apply (frule bin_nth_uint_imp)
  2386    apply (fast dest!: bin_nth_bl)+
  2387   done
  2388 
  2389 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  2390 
  2391 lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
  2392   unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
  2393 
  2394 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  2395   apply (unfold test_bit_bl)
  2396   apply clarsimp
  2397   apply (rule trans)
  2398    apply (rule nth_rev_alt)
  2399    apply (auto simp add: word_size)
  2400   done
  2401 
  2402 lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
  2403   for w :: "'a::len0 word"
  2404   by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
  2405 
  2406 lemma test_bit_set_gen:
  2407   "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
  2408   for w :: "'a::len0 word"
  2409   apply (unfold word_size word_test_bit_def word_set_bit_def)
  2410   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  2411   apply (auto elim!: test_bit_size [unfolded word_size]
  2412       simp add: word_test_bit_def [symmetric])
  2413   done
  2414 
  2415 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  2416   by (auto simp: of_bl_def bl_to_bin_rep_F)
  2417 
  2418 lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
  2419   for w :: "'a::len word"
  2420   by (simp add: word_msb_nth word_test_bit_def)
  2421 
  2422 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  2423 lemmas msb1 = msb0 [where i = 0]
  2424 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
  2425 
  2426 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
  2427 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  2428 
  2429 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  2430   "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
  2431     td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
  2432   for w :: "'a::len0 word"
  2433   apply (unfold word_size td_ext_def')
  2434   apply safe
  2435      apply (rule_tac [3] ext)
  2436      apply (rule_tac [4] ext)
  2437      apply (unfold word_size of_nth_def test_bit_bl)
  2438      apply safe
  2439        defer
  2440        apply (clarsimp simp: word_bl.Abs_inverse)+
  2441   apply (rule word_bl.Rep_inverse')
  2442   apply (rule sym [THEN trans])
  2443    apply (rule bl_of_nth_nth)
  2444   apply simp
  2445   apply (rule bl_of_nth_inj)
  2446   apply (clarsimp simp add : test_bit_bl word_size)
  2447   done
  2448 
  2449 interpretation test_bit:
  2450   td_ext
  2451     "(!!) :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
  2452     set_bits
  2453     "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  2454     "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  2455   by (rule td_ext_nth)
  2456 
  2457 lemmas td_nth = test_bit.td_thm
  2458 
  2459 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
  2460   for w :: "'a::len0 word"
  2461   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  2462 
  2463 lemma word_set_set_diff:
  2464   fixes w :: "'a::len0 word"
  2465   assumes "m \<noteq> n"
  2466   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
  2467   by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
  2468 
  2469 lemma nth_sint:
  2470   fixes w :: "'a::len word"
  2471   defines "l \<equiv> len_of TYPE('a)"
  2472   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  2473   unfolding sint_uint l_def
  2474   by (auto simp: nth_sbintr word_test_bit_def [symmetric])
  2475 
  2476 lemma word_lsb_numeral [simp]:
  2477   "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
  2478   unfolding word_lsb_alt test_bit_numeral by simp
  2479 
  2480 lemma word_lsb_neg_numeral [simp]:
  2481   "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
  2482   by (simp add: word_lsb_alt)
  2483 
  2484 lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  2485   unfolding word_set_bit_def
  2486   by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  2487 
  2488 lemma word_set_numeral [simp]:
  2489   "set_bit (numeral bin::'a::len0 word) n b =
  2490     word_of_int (bin_sc n b (numeral bin))"
  2491   unfolding word_numeral_alt by (rule set_bit_word_of_int)
  2492 
  2493 lemma word_set_neg_numeral [simp]:
  2494   "set_bit (- numeral bin::'a::len0 word) n b =
  2495     word_of_int (bin_sc n b (- numeral bin))"
  2496   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  2497 
  2498 lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  2499   unfolding word_0_wi by (rule set_bit_word_of_int)
  2500 
  2501 lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  2502   unfolding word_1_wi by (rule set_bit_word_of_int)
  2503 
  2504 lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  2505   by (simp add: setBit_def)
  2506 
  2507 lemma clearBit_no [simp]:
  2508   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
  2509   by (simp add: clearBit_def)
  2510 
  2511 lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
  2512   apply (rule word_bl.Abs_inverse')
  2513    apply simp
  2514   apply (rule word_eqI)
  2515   apply (clarsimp simp add: word_size)
  2516   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
  2517   done
  2518 
  2519 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  2520   unfolding word_msb_alt to_bl_n1 by simp
  2521 
  2522 lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
  2523   for w :: "'a::len0 word"
  2524   apply (rule iffI)
  2525    apply (rule disjCI)
  2526    apply (drule word_eqD)
  2527    apply (erule sym [THEN trans])
  2528    apply (simp add: test_bit_set)
  2529   apply (erule disjE)
  2530    apply clarsimp
  2531   apply (rule word_eqI)
  2532   apply (clarsimp simp add : test_bit_set_gen)
  2533   apply (drule test_bit_size)
  2534   apply force
  2535   done
  2536 
  2537 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  2538   by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
  2539 
  2540 lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
  2541   by (simp add: test_bit_2p [symmetric] word_of_int [symmetric])
  2542 
  2543 lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  2544   apply (unfold word_arith_power_alt)
  2545   apply (case_tac "len_of TYPE('a)")
  2546    apply clarsimp
  2547   apply (case_tac "nat")
  2548    apply clarsimp
  2549    apply (case_tac "n")
  2550     apply clarsimp
  2551    apply clarsimp
  2552   apply (drule word_gt_0 [THEN iffD1])
  2553   apply (safe intro!: word_eqI)
  2554    apply (auto simp add: nth_2p_bin)
  2555   apply (erule notE)
  2556   apply (simp (no_asm_use) add: uint_word_of_int word_size)
  2557   apply (subst mod_pos_pos_trivial)
  2558     apply simp
  2559    apply (rule power_strict_increasing)
  2560     apply simp_all
  2561   done
  2562 
  2563 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
  2564   by (induct n) (simp_all add: wi_hom_syms)
  2565 
  2566 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
  2567   for x :: "'a::len word"
  2568   apply (rule xtr3)
  2569    apply (rule_tac [2] y = "x" in le_word_or2)
  2570   apply (rule word_eqI)
  2571   apply (auto simp add: word_ao_nth nth_w2p word_size)
  2572   done
  2573 
  2574 lemma word_clr_le: "w \<ge> set_bit w n False"
  2575   for w :: "'a::len0 word"
  2576   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2577   apply (rule order_trans)
  2578    apply (rule bintr_bin_clr_le)
  2579   apply simp
  2580   done
  2581 
  2582 lemma word_set_ge: "w \<le> set_bit w n True"
  2583   for w :: "'a::len word"
  2584   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2585   apply (rule order_trans [OF _ bintr_bin_set_ge])
  2586   apply simp
  2587   done
  2588 
  2589 
  2590 subsection \<open>Shifting, Rotating, and Splitting Words\<close>
  2591 
  2592 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
  2593   unfolding shiftl1_def
  2594   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
  2595   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
  2596   apply (subst bintrunc_bintrunc_min)
  2597   apply simp
  2598   done
  2599 
  2600 lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  2601   unfolding word_numeral_alt shiftl1_wi by simp
  2602 
  2603 lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  2604   unfolding word_neg_numeral_alt shiftl1_wi by simp
  2605 
  2606 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  2607   by (simp add: shiftl1_def)
  2608 
  2609 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
  2610   by (simp only: shiftl1_def) (* FIXME: duplicate *)
  2611 
  2612 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
  2613   by (simp add: shiftl1_def Bit_B0 wi_hom_syms)
  2614 
  2615 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  2616   by (simp add: shiftr1_def)
  2617 
  2618 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  2619   by (simp add: sshiftr1_def)
  2620 
  2621 lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1"
  2622   by (simp add: sshiftr1_def)
  2623 
  2624 lemma shiftl_0 [simp]: "(0::'a::len0 word) << n = 0"
  2625   by (induct n) (auto simp: shiftl_def)
  2626 
  2627 lemma shiftr_0 [simp]: "(0::'a::len0 word) >> n = 0"
  2628   by (induct n) (auto simp: shiftr_def)
  2629 
  2630 lemma sshiftr_0 [simp]: "0 >>> n = 0"
  2631   by (induct n) (auto simp: sshiftr_def)
  2632 
  2633 lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
  2634   by (induct n) (auto simp: sshiftr_def)
  2635 
  2636 lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
  2637   apply (unfold shiftl1_def word_test_bit_def)
  2638   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  2639   apply (cases n)
  2640    apply auto
  2641   done
  2642 
  2643 lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
  2644   for w :: "'a::len0 word"
  2645   apply (unfold shiftl_def)
  2646   apply (induct m arbitrary: n)
  2647    apply (force elim!: test_bit_size)
  2648   apply (clarsimp simp add : nth_shiftl1 word_size)
  2649   apply arith
  2650   done
  2651 
  2652 lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
  2653 
  2654 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  2655   apply (unfold shiftr1_def word_test_bit_def)
  2656   apply (simp add: nth_bintr word_ubin.eq_norm)
  2657   apply safe
  2658   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
  2659   apply simp
  2660   done
  2661 
  2662 lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
  2663   for w :: "'a::len0 word"
  2664   apply (unfold shiftr_def)
  2665   apply (induct "m" arbitrary: n)
  2666    apply (auto simp add: nth_shiftr1)
  2667   done
  2668 
  2669 text \<open>
  2670   see paper page 10, (1), (2), \<open>shiftr1_def\<close> is of the form of (1),
  2671   where \<open>f\<close> (ie \<open>bin_rest\<close>) takes normal arguments to normal results,
  2672   thus we get (2) from (1)
  2673 \<close>
  2674 
  2675 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
  2676   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  2677   apply (subst bintr_uint [symmetric, OF order_refl])
  2678   apply (simp only : bintrunc_bintrunc_l)
  2679   apply simp
  2680   done
  2681 
  2682 lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  2683   apply (unfold sshiftr1_def word_test_bit_def)
  2684   apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size
  2685       del: bin_nth.simps)
  2686   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  2687   apply (auto simp add: bin_nth_sint)
  2688   done
  2689 
  2690 lemma nth_sshiftr [rule_format] :
  2691   "\<forall>n. sshiftr w m !! n =
  2692     (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
  2693   apply (unfold sshiftr_def)
  2694   apply (induct_tac m)
  2695    apply (simp add: test_bit_bl)
  2696   apply (clarsimp simp add: nth_sshiftr1 word_size)
  2697   apply safe
  2698        apply arith
  2699       apply arith
  2700      apply (erule thin_rl)
  2701      apply (case_tac n)
  2702       apply safe
  2703       apply simp
  2704      apply simp
  2705     apply (erule thin_rl)
  2706     apply (case_tac n)
  2707      apply safe
  2708      apply simp
  2709     apply simp
  2710    apply arith+
  2711   done
  2712 
  2713 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
  2714   apply (unfold shiftr1_def bin_rest_def)
  2715   apply (rule word_uint.Abs_inverse)
  2716   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
  2717   apply (rule xtr7)
  2718    prefer 2
  2719    apply (rule zdiv_le_dividend)
  2720     apply auto
  2721   done
  2722 
  2723 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
  2724   apply (unfold sshiftr1_def bin_rest_def [symmetric])
  2725   apply (simp add: word_sbin.eq_norm)
  2726   apply (rule trans)
  2727    defer
  2728    apply (subst word_sbin.norm_Rep [symmetric])
  2729    apply (rule refl)
  2730   apply (subst word_sbin.norm_Rep [symmetric])
  2731   apply (unfold One_nat_def)
  2732   apply (rule sbintrunc_rest)
  2733   done
  2734 
  2735 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  2736   apply (unfold shiftr_def)
  2737   apply (induct n)
  2738    apply simp
  2739   apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  2740   done
  2741 
  2742 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  2743   apply (unfold sshiftr_def)
  2744   apply (induct n)
  2745    apply simp
  2746   apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  2747   done
  2748 
  2749 
  2750 subsubsection \<open>shift functions in terms of lists of bools\<close>
  2751 
  2752 lemmas bshiftr1_numeral [simp] =
  2753   bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
  2754 
  2755 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
  2756   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
  2757 
  2758 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
  2759   by (simp add: of_bl_def bl_to_bin_append)
  2760 
  2761 lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
  2762   for w :: "'a::len0 word"
  2763 proof -
  2764   have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
  2765     by simp
  2766   also have "\<dots> = of_bl (to_bl w @ [False])"
  2767     by (rule shiftl1_of_bl)
  2768   finally show ?thesis .
  2769 qed
  2770 
  2771 lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
  2772   for w :: "'a::len word"
  2773   by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
  2774 
  2775 \<comment> \<open>Generalized version of \<open>bl_shiftl1\<close>. Maybe this one should replace it?\<close>
  2776 lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  2777   by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
  2778 
  2779 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  2780   apply (unfold shiftr1_def uint_bl of_bl_def)
  2781   apply (simp add: butlast_rest_bin word_size)
  2782   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  2783   done
  2784 
  2785 lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
  2786   for w :: "'a::len word"
  2787   by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
  2788 
  2789 \<comment> \<open>Generalized version of \<open>bl_shiftr1\<close>. Maybe this one should replace it?\<close>
  2790 lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  2791   apply (rule word_bl.Abs_inverse')
  2792    apply (simp del: butlast.simps)
  2793   apply (simp add: shiftr1_bl of_bl_def)
  2794   done
  2795 
  2796 lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  2797   apply (unfold word_reverse_def)
  2798   apply (rule word_bl.Rep_inverse' [symmetric])
  2799   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  2800   apply (cases "to_bl w")
  2801    apply auto
  2802   done
  2803 
  2804 lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  2805   by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
  2806 
  2807 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  2808   by (simp add: shiftl_rev)
  2809 
  2810 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  2811   by (simp add: rev_shiftl)
  2812 
  2813 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  2814   by (simp add: shiftr_rev)
  2815 
  2816 lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
  2817   for w :: "'a::len word"
  2818   apply (unfold sshiftr1_def uint_bl word_size)
  2819   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  2820   apply (simp add: sint_uint)
  2821   apply (rule nth_equalityI)
  2822    apply clarsimp
  2823   apply clarsimp
  2824   apply (case_tac i)
  2825    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  2826       nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr
  2827       del: bin_nth.Suc)
  2828    apply force
  2829   apply (rule impI)
  2830   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  2831   apply simp
  2832   done
  2833 
  2834 lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
  2835   for w :: "'a::len word"
  2836   apply (unfold shiftr_def)
  2837   apply (induct n)
  2838    prefer 2
  2839    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  2840    apply (rule butlast_take [THEN trans])
  2841     apply (auto simp: word_size)
  2842   done
  2843 
  2844 lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
  2845   for w :: "'a::len word"
  2846   apply (unfold sshiftr_def)
  2847   apply (induct n)
  2848    prefer 2
  2849    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  2850    apply (rule butlast_take [THEN trans])
  2851     apply (auto simp: word_size)
  2852   done
  2853 
  2854 lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  2855   apply (unfold shiftr_def)
  2856   apply (induct n)
  2857    prefer 2
  2858    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  2859    apply (rule take_butlast [THEN trans])
  2860     apply (auto simp: word_size)
  2861   done
  2862 
  2863 lemma take_sshiftr' [rule_format] :
  2864   "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
  2865     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
  2866   for w :: "'a::len word"
  2867   apply (unfold sshiftr_def)
  2868   apply (induct n)
  2869    prefer 2
  2870    apply (simp add: bl_sshiftr1)
  2871    apply (rule impI)
  2872    apply (rule take_butlast [THEN trans])
  2873     apply (auto simp: word_size)
  2874   done
  2875 
  2876 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  2877 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
  2878 
  2879 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
  2880   by (auto intro: append_take_drop_id [symmetric])
  2881 
  2882 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
  2883 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  2884 
  2885 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  2886   by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
  2887 
  2888 lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
  2889   for w :: "'a::len0 word"
  2890 proof -
  2891   have "w << n = of_bl (to_bl w) << n"
  2892     by simp
  2893   also have "\<dots> = of_bl (to_bl w @ replicate n False)"
  2894     by (rule shiftl_of_bl)
  2895   finally show ?thesis .
  2896 qed
  2897 
  2898 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  2899 
  2900 lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  2901   by (simp add: shiftl_bl word_rep_drop word_size)
  2902 
  2903 lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
  2904   for x :: "'a::len0 word"
  2905   apply (unfold word_size)
  2906   apply (rule word_eqI)
  2907   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  2908   done
  2909 
  2910 \<comment> \<open>note -- the following results use \<open>'a::len word < number_ring\<close>\<close>
  2911 
  2912 lemma shiftl1_2t: "shiftl1 w = 2 * w"
  2913   for w :: "'a::len word"
  2914   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  2915 
  2916 lemma shiftl1_p: "shiftl1 w = w + w"
  2917   for w :: "'a::len word"
  2918   by (simp add: shiftl1_2t)
  2919 
  2920 lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
  2921   for w :: "'a::len word"
  2922   by (induct n) (auto simp: shiftl_def shiftl1_2t)
  2923 
  2924 lemma shiftr1_bintr [simp]:
  2925   "(shiftr1 (numeral w) :: 'a::len0 word) =
  2926     word_of_int (bin_rest (bintrunc (len_of TYPE('a)) (numeral w)))"
  2927   unfolding shiftr1_def word_numeral_alt by (simp add: word_ubin.eq_norm)
  2928 
  2929 lemma sshiftr1_sbintr [simp]:
  2930   "(sshiftr1 (numeral w) :: 'a::len word) =
  2931     word_of_int (bin_rest (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  2932   unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
  2933 
  2934 lemma shiftr_no [simp]:
  2935   (* FIXME: neg_numeral *)
  2936   "(numeral w::'a::len0 word) >> n = word_of_int
  2937     ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  2938   by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  2939 
  2940 lemma sshiftr_no [simp]:
  2941   (* FIXME: neg_numeral *)
  2942   "(numeral w::'a::len word) >>> n = word_of_int
  2943     ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  2944   apply (rule word_eqI)
  2945   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
  2946    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
  2947   done
  2948 
  2949 lemma shiftr1_bl_of:
  2950   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  2951     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  2952   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin)
  2953 
  2954 lemma shiftr_bl_of:
  2955   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  2956     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
  2957   apply (unfold shiftr_def)
  2958   apply (induct n)
  2959    apply clarsimp
  2960   apply clarsimp
  2961   apply (subst shiftr1_bl_of)
  2962    apply simp
  2963   apply (simp add: butlast_take)
  2964   done
  2965 
  2966 lemma shiftr_bl: "x >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  2967   for x :: "'a::len0 word"
  2968   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  2969 
  2970 lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
  2971   for w :: "'a::len word"
  2972   apply (unfold shiftr_bl word_msb_alt)
  2973   apply (simp add: word_size Suc_le_eq take_Suc)
  2974   apply (cases "hd (to_bl w)")
  2975    apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
  2976   done
  2977 
  2978 lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
  2979   apply (induct ys arbitrary: n)
  2980    apply simp_all
  2981   apply (case_tac n)
  2982    apply simp_all
  2983   done
  2984 
  2985 lemma align_lem_or [rule_format] :
  2986   "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  2987     drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  2988     map2 (|) x y = take m x @ drop m y"
  2989   apply (induct y)
  2990    apply force
  2991   apply clarsimp
  2992   apply (case_tac x)
  2993    apply force
  2994   apply (case_tac m)
  2995    apply auto
  2996   apply (drule_tac t="length xs" for xs in sym)
  2997   apply (auto simp: map2_def zip_replicate o_def)
  2998   done
  2999 
  3000 lemma align_lem_and [rule_format] :
  3001   "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  3002     drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  3003     map2 (\<and>) x y = replicate (n + m) False"
  3004   apply (induct y)
  3005    apply force
  3006   apply clarsimp
  3007   apply (case_tac x)
  3008    apply force
  3009   apply (case_tac m)
  3010   apply auto
  3011   apply (drule_tac t="length xs" for xs in sym)
  3012   apply (auto simp: map2_def zip_replicate o_def map_replicate_const)
  3013   done
  3014 
  3015 lemma aligned_bl_add_size [OF refl]:
  3016   "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  3017     take m (to_bl y) = replicate m False \<Longrightarrow>
  3018     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  3019   apply (subgoal_tac "x AND y = 0")
  3020    prefer 2
  3021    apply (rule word_bl.Rep_eqD)
  3022    apply (simp add: bl_word_and)
  3023    apply (rule align_lem_and [THEN trans])
  3024        apply (simp_all add: word_size)[5]
  3025    apply simp
  3026   apply (subst word_plus_and_or [symmetric])
  3027   apply (simp add : bl_word_or)
  3028   apply (rule align_lem_or)
  3029      apply (simp_all add: word_size)
  3030   done
  3031 
  3032 
  3033 subsubsection \<open>Mask\<close>
  3034 
  3035 lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m"
  3036   apply (unfold mask_def test_bit_bl)
  3037   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  3038   apply (clarsimp simp add: word_size)
  3039   apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
  3040   apply (fold of_bl_def)
  3041   apply (simp add: word_1_bl)
  3042   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
  3043   apply auto
  3044   done
  3045 
  3046 lemma mask_bl: "mask n = of_bl (replicate n True)"
  3047   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
  3048 
  3049 lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
  3050   by (auto simp add: nth_bintr word_size intro: word_eqI)
  3051 
  3052 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
  3053   apply (rule word_eqI)
  3054   apply (simp add: nth_bintr word_size word_ops_nth_size)
  3055   apply (auto simp add: test_bit_bin)
  3056   done
  3057 
  3058 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  3059   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3060 
  3061 lemma and_mask_wi':
  3062   "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
  3063   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3064 
  3065 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  3066   unfolding word_numeral_alt by (rule and_mask_wi)
  3067 
  3068 lemma bl_and_mask':
  3069   "to_bl (w AND mask n :: 'a::len word) =
  3070     replicate (len_of TYPE('a) - n) False @
  3071     drop (len_of TYPE('a) - n) (to_bl w)"
  3072   apply (rule nth_equalityI)
  3073    apply simp
  3074   apply (clarsimp simp add: to_bl_nth word_size)
  3075   apply (simp add: word_size word_ops_nth_size)
  3076   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
  3077   done
  3078 
  3079 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
  3080   by (simp only: and_mask_bintr bintrunc_mod2p)
  3081 
  3082 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
  3083   apply (simp add: and_mask_bintr word_ubin.eq_norm)
  3084   apply (simp add: bintrunc_mod2p)
  3085   apply (rule xtr8)
  3086    prefer 2
  3087    apply (rule pos_mod_bound)
  3088    apply auto
  3089   done
  3090 
  3091 lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  3092   for b n :: int
  3093   by (simp add: int_mod_lem eq_sym_conv)
  3094 
  3095 lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
  3096   apply (simp add: and_mask_bintr)
  3097   apply (simp add: word_ubin.inverse_norm)
  3098   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
  3099   apply (fast intro!: lt2p_lem)
  3100   done
  3101 
  3102 lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
  3103   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  3104   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0)
  3105   apply (subst word_uint.norm_Rep [symmetric])
  3106   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  3107   apply auto
  3108   done
  3109 
  3110 lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0"
  3111   apply (unfold unat_def)
  3112   apply (rule trans [OF _ and_mask_dvd])
  3113   apply (unfold dvd_def)
  3114   apply auto
  3115    apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  3116    apply simp
  3117   apply (simp add: nat_mult_distrib nat_power_eq)
  3118   done
  3119 
  3120 lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
  3121   for w :: "'a::len word"
  3122   apply (unfold word_size word_less_alt word_numeral_alt)
  3123   apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial
  3124       simp del: word_of_int_numeral)
  3125   done
  3126 
  3127 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
  3128   for x :: "'a::len word"
  3129   apply (unfold word_less_alt word_numeral_alt)
  3130   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
  3131       simp del: word_of_int_numeral)
  3132   apply (drule xtr8 [rotated])
  3133    apply (rule int_mod_le)
  3134    apply (auto simp add : mod_pos_pos_trivial)
  3135   done
  3136 
  3137 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  3138 
  3139 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
  3140 
  3141 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  3142   unfolding word_size by (erule and_mask_less')
  3143 
  3144 lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
  3145   for c x :: "'a::len word"
  3146   by (auto simp: word_mod_def uint_2p and_mask_mod_2p)
  3147 
  3148 lemma mask_eqs:
  3149   "(a AND mask n) + b AND mask n = a + b AND mask n"
  3150   "a + (b AND mask n) AND mask n = a + b AND mask n"
  3151   "(a AND mask n) - b AND mask n = a - b AND mask n"
  3152   "a - (b AND mask n) AND mask n = a - b AND mask n"
  3153   "a * (b AND mask n) AND mask n = a * b AND mask n"
  3154   "(b AND mask n) * a AND mask n = b * a AND mask n"
  3155   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
  3156   "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
  3157   "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
  3158   "- (a AND mask n) AND mask n = - a AND mask n"
  3159   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  3160   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  3161   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  3162   by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
  3163 
  3164 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  3165   using word_of_int_Ex [where x=x]
  3166   by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
  3167 
  3168 
  3169 subsubsection \<open>Revcast\<close>
  3170 
  3171 lemmas revcast_def' = revcast_def [simplified]
  3172 lemmas revcast_def'' = revcast_def' [simplified word_size]
  3173 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  3174 
  3175 lemma to_bl_revcast:
  3176   "to_bl (revcast w :: 'a::len0 word) = takefill False (len_of TYPE('a)) (to_bl w)"
  3177   apply (unfold revcast_def' word_size)
  3178   apply (rule word_bl.Abs_inverse)
  3179   apply simp
  3180   done
  3181 
  3182 lemma revcast_rev_ucast [OF refl refl refl]:
  3183   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
  3184     rc = word_reverse uc"
  3185   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  3186   apply (auto simp: to_bl_of_bin takefill_bintrunc)
  3187   apply (simp add: word_bl.Abs_inverse word_size)
  3188   done
  3189 
  3190 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  3191   using revcast_rev_ucast [of "word_reverse w"] by simp
  3192 
  3193 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
  3194   by (fact revcast_rev_ucast [THEN word_rev_gal'])
  3195 
  3196 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
  3197   by (fact revcast_ucast [THEN word_rev_gal'])
  3198 
  3199 
  3200 text "linking revcast and cast via shift"
  3201 
  3202 lemmas wsst_TYs = source_size target_size word_size
  3203 
  3204 lemma revcast_down_uu [OF refl]:
  3205   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
  3206   for w :: "'a::len word"
  3207   apply (simp add: revcast_def')
  3208   apply (rule word_bl.Rep_inverse')
  3209   apply (rule trans, rule ucast_down_drop)
  3210    prefer 2
  3211    apply (rule trans, rule drop_shiftr)
  3212    apply (auto simp: takefill_alt wsst_TYs)
  3213   done
  3214 
  3215 lemma revcast_down_us [OF refl]:
  3216   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
  3217   for w :: "'a::len word"
  3218   apply (simp add: revcast_def')
  3219   apply (rule word_bl.Rep_inverse')
  3220   apply (rule trans, rule ucast_down_drop)
  3221    prefer 2
  3222    apply (rule trans, rule drop_sshiftr)
  3223    apply (auto simp: takefill_alt wsst_TYs)
  3224   done
  3225 
  3226 lemma revcast_down_su [OF refl]:
  3227   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
  3228   for w :: "'a::len word"
  3229   apply (simp add: revcast_def')
  3230   apply (rule word_bl.Rep_inverse')
  3231   apply (rule trans, rule scast_down_drop)
  3232    prefer 2
  3233    apply (rule trans, rule drop_shiftr)
  3234    apply (auto simp: takefill_alt wsst_TYs)
  3235   done
  3236 
  3237 lemma revcast_down_ss [OF refl]:
  3238   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
  3239   for w :: "'a::len word"
  3240   apply (simp add: revcast_def')
  3241   apply (rule word_bl.Rep_inverse')
  3242   apply (rule trans, rule scast_down_drop)
  3243    prefer 2
  3244    apply (rule trans, rule drop_sshiftr)
  3245    apply (auto simp: takefill_alt wsst_TYs)
  3246   done
  3247 
  3248 (* FIXME: should this also be [OF refl] ? *)
  3249 lemma cast_down_rev:
  3250   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
  3251   for w :: "'a::len word"
  3252   apply (unfold shiftl_rev)
  3253   apply clarify
  3254   apply (simp add: revcast_rev_ucast)
  3255   apply (rule word_rev_gal')
  3256   apply (rule trans [OF _ revcast_rev_ucast])
  3257   apply (rule revcast_down_uu [symmetric])
  3258   apply (auto simp add: wsst_TYs)
  3259   done
  3260 
  3261 lemma revcast_up [OF refl]:
  3262   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
  3263     rc w = (ucast w :: 'a::len word) << n"
  3264   apply (simp add: revcast_def')
  3265   apply (rule word_bl.Rep_inverse')
  3266   apply (simp add: takefill_alt)
  3267   apply (rule bl_shiftl [THEN trans])
  3268   apply (subst ucast_up_app)
  3269    apply (auto simp add: wsst_TYs)
  3270   done
  3271 
  3272 lemmas rc1 = revcast_up [THEN
  3273   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3274 lemmas rc2 = revcast_down_uu [THEN
  3275   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3276 
  3277 lemmas ucast_up =
  3278  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
  3279 lemmas ucast_down =
  3280   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
  3281 
  3282 
  3283 subsubsection \<open>Slices\<close>
  3284 
  3285 lemma slice1_no_bin [simp]:
  3286   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
  3287   by (simp add: slice1_def) (* TODO: neg_numeral *)
  3288 
  3289 lemma slice_no_bin [simp]:
  3290   "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b::len0) - n)
  3291     (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
  3292   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
  3293 
  3294 lemma slice1_0 [simp] : "slice1 n 0 = 0"
  3295   unfolding slice1_def by simp
  3296 
  3297 lemma slice_0 [simp] : "slice n 0 = 0"
  3298   unfolding slice_def by auto
  3299 
  3300 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
  3301   unfolding slice_def' slice1_def
  3302   by (simp add : takefill_alt word_size)
  3303 
  3304 lemmas slice_take = slice_take' [unfolded word_size]
  3305 
  3306 \<comment> \<open>shiftr to a word of the same size is just slice,
  3307     slice is just shiftr then ucast\<close>
  3308 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
  3309 
  3310 lemma slice_shiftr: "slice n w = ucast (w >> n)"
  3311   apply (unfold slice_take shiftr_bl)
  3312   apply (rule ucast_of_bl_up [symmetric])
  3313   apply (simp add: word_size)
  3314   done
  3315 
  3316 lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
  3317   by (simp add: slice_shiftr nth_ucast nth_shiftr)
  3318 
  3319 lemma slice1_down_alt':
  3320   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
  3321     to_bl sl = takefill False fs (drop k (to_bl w))"
  3322   by (auto simp: slice1_def word_size of_bl_def uint_bl
  3323       word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  3324 
  3325 lemma slice1_up_alt':
  3326   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
  3327     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  3328   apply (unfold slice1_def word_size of_bl_def uint_bl)
  3329   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
  3330   apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
  3331     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
  3332   apply arith
  3333   done
  3334 
  3335 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
  3336 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
  3337 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
  3338 lemmas slice1_up_alts =
  3339   le_add_diff_inverse [symmetric, THEN su1]
  3340   le_add_diff_inverse2 [symmetric, THEN su1]
  3341 
  3342 lemma ucast_slice1: "ucast w = slice1 (size w) w"
  3343   by (simp add: slice1_def ucast_bl takefill_same' word_size)
  3344 
  3345 lemma ucast_slice: "ucast w = slice 0 w"
  3346   by (simp add: slice_def ucast_slice1)
  3347 
  3348 lemma slice_id: "slice 0 t = t"
  3349   by (simp only: ucast_slice [symmetric] ucast_id)
  3350 
  3351 lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  3352   by (simp add: slice1_def revcast_def' word_size)
  3353 
  3354 lemma slice1_tf_tf':
  3355   "to_bl (slice1 n w :: 'a::len0 word) =
  3356     rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
  3357   unfolding slice1_def by (rule word_rev_tf)
  3358 
  3359 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
  3360 
  3361 lemma rev_slice1:
  3362   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
  3363     slice1 n (word_reverse w :: 'b::len0 word) =
  3364     word_reverse (slice1 k w :: 'a::len0 word)"
  3365   apply (unfold word_reverse_def slice1_tf_tf)
  3366   apply (rule word_bl.Rep_inverse')
  3367   apply (rule rev_swap [THEN iffD1])
  3368   apply (rule trans [symmetric])
  3369    apply (rule tf_rev)
  3370    apply (simp add: word_bl.Abs_inverse)
  3371   apply (simp add: word_bl.Abs_inverse)
  3372   done
  3373 
  3374 lemma rev_slice:
  3375   "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
  3376     slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
  3377   apply (unfold slice_def word_size)
  3378   apply (rule rev_slice1)
  3379   apply arith
  3380   done
  3381 
  3382 lemmas sym_notr =
  3383   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
  3384 
  3385 \<comment> \<open>problem posed by TPHOLs referee:
  3386       criterion for overflow of addition of signed integers\<close>
  3387 
  3388 lemma sofl_test:
  3389   "(sint x + sint y = sint (x + y)) =
  3390      ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
  3391   for x y :: "'a::len word"
  3392   apply (unfold word_size)
  3393   apply (cases "len_of TYPE('a)", simp)
  3394   apply (subst msb_shift [THEN sym_notr])
  3395   apply (simp add: word_ops_msb)
  3396   apply (simp add: word_msb_sint)
  3397   apply safe
  3398        apply simp_all
  3399      apply (unfold sint_word_ariths)
  3400      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
  3401      apply safe
  3402          apply (insert sint_range' [where x=x])
  3403          apply (insert sint_range' [where x=y])
  3404          defer
  3405          apply (simp (no_asm), arith)
  3406         apply (simp (no_asm), arith)
  3407        defer
  3408        defer
  3409        apply (simp (no_asm), arith)
  3410       apply (simp (no_asm), arith)
  3411      apply (rule notI [THEN notnotD],
  3412       drule leI not_le_imp_less,
  3413       drule sbintrunc_inc sbintrunc_dec,
  3414       simp)+
  3415   done
  3416 
  3417 
  3418 subsection \<open>Split and cat\<close>
  3419 
  3420 lemmas word_split_bin' = word_split_def
  3421 lemmas word_cat_bin' = word_cat_def
  3422 
  3423 lemma word_rsplit_no:
  3424   "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
  3425     map word_of_int (bin_rsplit (len_of TYPE('a::len))
  3426       (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
  3427   by (simp add: word_rsplit_def word_ubin.eq_norm)
  3428 
  3429 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
  3430   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  3431 
  3432 lemma test_bit_cat:
  3433   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
  3434     (if n < size b then b !! n else a !! (n - size b)))"
  3435   apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  3436   apply (erule bin_nth_uint_imp)
  3437   done
  3438 
  3439 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
  3440   by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
  3441 
  3442 lemma of_bl_append:
  3443   "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
  3444   apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
  3445   apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
  3446   done
  3447 
  3448 lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
  3449   by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
  3450 
  3451 lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
  3452   by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
  3453 
  3454 lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  3455   by (cases x) simp_all
  3456 
  3457 lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
  3458     a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
  3459   for w :: "'a::len0 word"
  3460   apply (frule word_ubin.norm_Rep [THEN ssubst])
  3461   apply (drule bin_split_trunc1)
  3462   apply (drule sym [THEN trans])
  3463    apply assumption
  3464   apply safe
  3465   done
  3466 
  3467 lemma word_split_bl':
  3468   "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
  3469     (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
  3470   apply (unfold word_split_bin')
  3471   apply safe
  3472    defer
  3473    apply (clarsimp split: prod.splits)
  3474    apply hypsubst_thin
  3475    apply (drule word_ubin.norm_Rep [THEN ssubst])
  3476    apply (drule split_bintrunc)
  3477    apply (simp add: of_bl_def bl2bin_drop word_size
  3478       word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
  3479   apply (clarsimp split: prod.splits)
  3480   apply (frule split_uint_lem [THEN conjunct1])
  3481   apply (unfold word_size)
  3482   apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
  3483    defer
  3484    apply simp
  3485   apply (simp add : of_bl_def to_bl_def)
  3486   apply (subst bin_split_take1 [symmetric])
  3487     prefer 2
  3488     apply assumption
  3489    apply simp
  3490   apply (erule thin_rl)
  3491   apply (erule arg_cong [THEN trans])
  3492   apply (simp add : word_ubin.norm_eq_iff [symmetric])
  3493   done
  3494 
  3495 lemma word_split_bl: "std = size c - size b \<Longrightarrow>
  3496     (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
  3497     word_split c = (a, b)"
  3498   apply (rule iffI)
  3499    defer
  3500    apply (erule (1) word_split_bl')
  3501   apply (case_tac "word_split c")
  3502   apply (auto simp add: word_size)
  3503   apply (frule word_split_bl' [rotated])
  3504    apply (auto simp add: word_size)
  3505   done
  3506 
  3507 lemma word_split_bl_eq:
  3508   "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
  3509     (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
  3510      of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
  3511   for c :: "'a::len word"
  3512   apply (rule word_split_bl [THEN iffD1])
  3513    apply (unfold word_size)
  3514    apply (rule refl conjI)+
  3515   done
  3516 
  3517 \<comment> \<open>keep quantifiers for use in simplification\<close>
  3518 lemma test_bit_split':
  3519   "word_split c = (a, b) \<longrightarrow>
  3520     (\<forall>n m.
  3521       b !! n = (n < size b \<and> c !! n) \<and>
  3522       a !! m = (m < size a \<and> c !! (m + size b)))"
  3523   apply (unfold word_split_bin' test_bit_bin)
  3524   apply (clarify)
  3525   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
  3526   apply (drule bin_nth_split)
  3527   apply safe
  3528        apply (simp_all add: add.commute)
  3529    apply (erule bin_nth_uint_imp)+
  3530   done
  3531 
  3532 lemma test_bit_split:
  3533   "word_split c = (a, b) \<Longrightarrow>
  3534     (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
  3535     (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
  3536   by (simp add: test_bit_split')
  3537 
  3538 lemma test_bit_split_eq:
  3539   "word_split c = (a, b) \<longleftrightarrow>
  3540     ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
  3541      (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
  3542   apply (rule_tac iffI)
  3543    apply (rule_tac conjI)
  3544     apply (erule test_bit_split [THEN conjunct1])
  3545    apply (erule test_bit_split [THEN conjunct2])
  3546   apply (case_tac "word_split c")
  3547   apply (frule test_bit_split)
  3548   apply (erule trans)
  3549   apply (fastforce intro!: word_eqI simp add: word_size)
  3550   done
  3551 
  3552 \<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
  3553       result to the length given by the result type\<close>
  3554 
  3555 lemma word_cat_id: "word_cat a b = b"
  3556   by (simp add: word_cat_bin' word_ubin.inverse_norm)
  3557 
  3558 \<comment> \<open>limited hom result\<close>
  3559 lemma word_cat_hom:
  3560   "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
  3561     (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
  3562     word_of_int (bin_cat w (size b) (uint b))"
  3563   by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
  3564       word_ubin.eq_norm bintr_cat min.absorb1)
  3565 
  3566 lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  3567   apply (rule word_eqI)
  3568   apply (drule test_bit_split)
  3569   apply (clarsimp simp add : test_bit_cat word_size)
  3570   apply safe
  3571   apply arith
  3572   done
  3573 
  3574 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
  3575 
  3576 
  3577 subsubsection \<open>Split and slice\<close>
  3578 
  3579 lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
  3580   apply (drule test_bit_split)
  3581   apply (rule conjI)
  3582    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  3583   done
  3584 
  3585 lemma slice_cat1 [OF refl]:
  3586   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  3587   apply safe
  3588   apply (rule word_eqI)
  3589   apply (simp add: nth_slice test_bit_cat word_size)
  3590   done
  3591 
  3592 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  3593 
  3594 lemma cat_slices:
  3595   "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  3596     size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  3597   apply safe
  3598   apply (rule word_eqI)
  3599   apply (simp add: nth_slice test_bit_cat word_size)
  3600   apply safe
  3601   apply arith
  3602   done
  3603 
  3604 lemma word_split_cat_alt:
  3605   "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
  3606   apply (case_tac "word_split w")
  3607   apply (rule trans, assumption)
  3608   apply (drule test_bit_split)
  3609   apply safe
  3610    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  3611   done
  3612 
  3613 lemmas word_cat_bl_no_bin [simp] =
  3614   word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
  3615   for a b (* FIXME: negative numerals, 0 and 1 *)
  3616 
  3617 lemmas word_split_bl_no_bin [simp] =
  3618   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
  3619 
  3620 text \<open>
  3621   This odd result arises from the fact that the statement of the
  3622   result implies that the decoded words are of the same type,
  3623   and therefore of the same length, as the original word.\<close>
  3624 
  3625 lemma word_rsplit_same: "word_rsplit w = [w]"
  3626   by (simp add: word_rsplit_def bin_rsplit_all)
  3627 
  3628 lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
  3629   by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
  3630       split: prod.split)
  3631 
  3632 lemma test_bit_rsplit:
  3633   "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
  3634     k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
  3635   for sw :: "'a::len word list"
  3636   apply (unfold word_rsplit_def word_test_bit_def)
  3637   apply (rule trans)
  3638    apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
  3639    apply (rule nth_map [symmetric])
  3640    apply simp
  3641   apply (rule bin_nth_rsplit)
  3642      apply simp_all
  3643   apply (simp add : word_size rev_map)
  3644   apply (rule trans)
  3645    defer
  3646    apply (rule map_ident [THEN fun_cong])
  3647   apply (rule refl [THEN map_cong])
  3648   apply (simp add : word_ubin.eq_norm)
  3649   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  3650   done
  3651 
  3652 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  3653   by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
  3654 
  3655 lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  3656   by (induct wl) (auto simp: word_size)
  3657 
  3658 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  3659 
  3660 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
  3661 
  3662 lemma nth_rcat_lem:
  3663   "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
  3664     rev (concat (map to_bl wl)) ! n =
  3665     rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
  3666   apply (induct wl)
  3667    apply clarsimp
  3668   apply (clarsimp simp add : nth_append size_rcat_lem)
  3669   apply (simp (no_asm_use) only:  mult_Suc [symmetric]
  3670          td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
  3671   apply clarsimp
  3672   done
  3673 
  3674 lemma test_bit_rcat:
  3675   "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
  3676     (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
  3677   for wl :: "'a::len word list"
  3678   apply (unfold word_rcat_bl word_size)
  3679   apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  3680   apply safe
  3681    apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  3682   done
  3683 
  3684 lemma foldl_eq_foldr: "foldl (+) x xs = foldr (+) (x # xs) 0"
  3685   for x :: "'a::comm_monoid_add"
  3686   by (induct xs arbitrary: x) (auto simp: add.assoc)
  3687 
  3688 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  3689 
  3690 lemmas test_bit_rsplit_alt =
  3691   trans [OF nth_rev_alt [THEN test_bit_cong]
  3692   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  3693 
  3694 \<comment> \<open>lazy way of expressing that u and v, and su and sv, have same types\<close>
  3695 lemma word_rsplit_len_indep [OF refl refl refl refl]:
  3696   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
  3697     word_rsplit v = sv \<Longrightarrow> length su = length sv"
  3698   by (auto simp: word_rsplit_def bin_rsplit_len_indep)
  3699 
  3700 lemma length_word_rsplit_size:
  3701   "n = len_of TYPE('a::len) \<Longrightarrow>
  3702     length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
  3703   by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
  3704 
  3705 lemmas length_word_rsplit_lt_size =
  3706   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  3707 
  3708 lemma length_word_rsplit_exp_size:
  3709   "n = len_of TYPE('a::len) \<Longrightarrow>
  3710     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  3711   by (auto simp: word_rsplit_def word_size bin_rsplit_len)
  3712 
  3713 lemma length_word_rsplit_even_size:
  3714   "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
  3715     length (word_rsplit w :: 'a word list) = m"
  3716   by (auto simp: length_word_rsplit_exp_size given_quot_alt)
  3717 
  3718 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  3719 
  3720 \<comment> \<open>alternative proof of \<open>word_rcat_rsplit\<close>\<close>
  3721 lemmas tdle = times_div_less_eq_dividend
  3722 lemmas dtle = xtr4 [OF tdle mult.commute]
  3723 
  3724 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  3725   apply (rule word_eqI)
  3726   apply (clarsimp simp: test_bit_rcat word_size)
  3727   apply (subst refl [THEN test_bit_rsplit])
  3728     apply (simp_all add: word_size
  3729       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  3730    apply safe
  3731    apply (erule xtr7, rule dtle)+
  3732   done
  3733 
  3734 lemma size_word_rsplit_rcat_size:
  3735   "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
  3736     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  3737   for ws :: "'a::len word list" and frcw :: "'b::len0 word"
  3738   apply (clarsimp simp: word_size length_word_rsplit_exp_size')
  3739   apply (fast intro: given_quot_alt)
  3740   done
  3741 
  3742 lemma msrevs:
  3743   "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  3744   "(k * n + m) mod n = m mod n"
  3745   for n :: nat
  3746   by (auto simp: add.commute)
  3747 
  3748 lemma word_rsplit_rcat_size [OF refl]:
  3749   "word_rcat ws = frcw \<Longrightarrow>
  3750     size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
  3751   for ws :: "'a::len word list"
  3752   apply (frule size_word_rsplit_rcat_size, assumption)
  3753   apply (clarsimp simp add : word_size)
  3754   apply (rule nth_equalityI, assumption)
  3755   apply clarsimp
  3756   apply (rule word_eqI [rule_format])
  3757   apply (rule trans)
  3758    apply (rule test_bit_rsplit_alt)
  3759      apply (clarsimp simp: word_size)+
  3760   apply (rule trans)
  3761    apply (rule test_bit_rcat [OF refl refl])
  3762   apply (simp add: word_size)
  3763   apply (subst nth_rev)
  3764    apply arith
  3765   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3766   apply safe
  3767   apply (simp add: diff_mult_distrib)
  3768   apply (rule mpl_lem)
  3769    apply (cases "size ws")
  3770     apply simp_all
  3771   done
  3772 
  3773 
  3774 subsection \<open>Rotation\<close>
  3775 
  3776 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  3777 
  3778 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  3779 
  3780 lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  3781   apply (rule box_equals)
  3782     defer
  3783     apply (rule rotate_conv_mod [symmetric])+
  3784   apply simp
  3785   done
  3786 
  3787 lemmas rotate_eqs =
  3788   trans [OF rotate0 [THEN fun_cong] id_apply]
  3789   rotate_rotate [symmetric]
  3790   rotate_id
  3791   rotate_conv_mod
  3792   rotate_eq_mod
  3793 
  3794 
  3795 subsubsection \<open>Rotation of list to right\<close>
  3796 
  3797 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  3798   by (cases l) (auto simp: rotater1_def)
  3799 
  3800 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  3801   apply (unfold rotater1_def)
  3802   apply (cases "l")
  3803    apply (case_tac [2] "list")
  3804     apply auto
  3805   done
  3806 
  3807 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  3808   by (cases l) (auto simp: rotater1_def)
  3809 
  3810 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  3811   by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
  3812 
  3813 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  3814   by (induct n) (auto simp: rotater_def intro: rotater1_rev')
  3815 
  3816 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
  3817   using rotater_rev' [where xs = "rev ys"] by simp
  3818 
  3819 lemma rotater_drop_take:
  3820   "rotater n xs =
  3821     drop (length xs - n mod length xs) xs @
  3822     take (length xs - n mod length xs) xs"
  3823   by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
  3824 
  3825 lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
  3826   unfolding rotater_def by auto
  3827 
  3828 lemma rotate_inv_plus [rule_format] :
  3829   "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
  3830     rotate k (rotater n xs) = rotate m xs \<and>
  3831     rotater n (rotate k xs) = rotate m xs \<and>
  3832     rotate n (rotater k xs) = rotater m xs"
  3833   by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
  3834 
  3835 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  3836 
  3837 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  3838 
  3839 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
  3840 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
  3841 
  3842 lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
  3843   by auto
  3844 
  3845 lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
  3846   by auto
  3847 
  3848 lemma length_rotater [simp]: "length (rotater n xs) = length xs"
  3849   by (simp add : rotater_rev)
  3850 
  3851 lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
  3852   by simp
  3853 
  3854 lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
  3855   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
  3856 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  3857 lemmas rotater_eqs = rrs1 [simplified length_rotater]
  3858 lemmas rotater_0 = rotater_eqs (1)
  3859 lemmas rotater_add = rotater_eqs (2)
  3860 
  3861 
  3862 subsubsection \<open>map, map2, commuting with rotate(r)\<close>
  3863 
  3864 lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  3865   by (induct xs) auto
  3866 
  3867 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
  3868   by (cases xs) (auto simp: rotater1_def last_map butlast_map)
  3869 
  3870 lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
  3871   by (induct n) (auto simp: rotater_def rotater1_map)
  3872 
  3873 lemma but_last_zip [rule_format] :
  3874   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
  3875     last (zip xs ys) = (last xs, last ys) \<and>
  3876     butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
  3877   apply (induct xs)
  3878    apply auto
  3879      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3880   done
  3881 
  3882 lemma but_last_map2 [rule_format] :
  3883   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
  3884     last (map2 f xs ys) = f (last xs) (last ys) \<and>
  3885     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
  3886   apply (induct xs)
  3887    apply auto
  3888      apply (unfold map2_def)
  3889      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3890   done
  3891 
  3892 lemma rotater1_zip:
  3893   "length xs = length ys \<Longrightarrow>
  3894     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
  3895   apply (unfold rotater1_def)
  3896   apply (cases xs)
  3897    apply auto
  3898    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  3899   done
  3900 
  3901 lemma rotater1_map2:
  3902   "length xs = length ys \<Longrightarrow>
  3903     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
  3904   by (simp add: map2_def rotater1_map rotater1_zip)
  3905 
  3906 lemmas lrth =
  3907   box_equals [OF asm_rl length_rotater [symmetric]
  3908                  length_rotater [symmetric],
  3909               THEN rotater1_map2]
  3910 
  3911 lemma rotater_map2:
  3912   "length xs = length ys \<Longrightarrow>
  3913     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
  3914   by (induct n) (auto intro!: lrth)
  3915 
  3916 lemma rotate1_map2:
  3917   "length xs = length ys \<Longrightarrow>
  3918     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
  3919   by (cases xs; cases ys) (auto simp: map2_def)
  3920 
  3921 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
  3922   length_rotate [symmetric], THEN rotate1_map2]
  3923 
  3924 lemma rotate_map2:
  3925   "length xs = length ys \<Longrightarrow>
  3926     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
  3927   by (induct n) (auto intro!: lth)
  3928 
  3929 
  3930 \<comment> \<open>corresponding equalities for word rotation\<close>
  3931 
  3932 lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
  3933   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  3934 
  3935 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  3936 
  3937 lemmas word_rotl_eqs =
  3938   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  3939 
  3940 lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
  3941   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  3942 
  3943 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  3944 
  3945 lemmas word_rotr_eqs =
  3946   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  3947 
  3948 declare word_rotr_eqs (1) [simp]
  3949 declare word_rotl_eqs (1) [simp]
  3950 
  3951 lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
  3952   and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
  3953   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  3954 
  3955 lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
  3956   and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
  3957   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
  3958 
  3959 lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  3960   by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
  3961 
  3962 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  3963   by (auto simp: word_rot_defs)
  3964 
  3965 lemmas abl_cong = arg_cong [where f = "of_bl"]
  3966 
  3967 lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
  3968 proof -
  3969   have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  3970     by auto
  3971 
  3972   have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  3973     by auto
  3974 
  3975   note rpts [symmetric] =
  3976     rotate_inv_plus [THEN conjunct1]
  3977     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  3978     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  3979     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  3980 
  3981   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  3982   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  3983 
  3984   show ?thesis
  3985     apply (unfold word_rot_defs)
  3986     apply (simp only: split: if_split)
  3987     apply (safe intro!: abl_cong)
  3988            apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
  3989                   to_bl_rotl
  3990                   to_bl_rotr [THEN word_bl.Rep_inverse']
  3991                   to_bl_rotr)
  3992          apply (rule rrp rrrp rpts,
  3993                 simp add: nat_add_distrib [symmetric]
  3994                 nat_diff_distrib [symmetric])+
  3995     done
  3996 qed
  3997 
  3998 lemma word_roti_conv_mod':
  3999   "word_roti n w = word_roti (n mod int (size w)) w"
  4000 proof (cases "size w = 0")
  4001   case True
  4002   then show ?thesis
  4003     by simp
  4004 next
  4005   case False
  4006   then have [simp]: "l mod int (size w) \<ge> 0" for l
  4007     by simp
  4008   then have *: "word_roti (n mod int (size w)) w = word_rotr (nat (n mod int (size w))) w"
  4009     by (simp add: word_roti_def)
  4010   show ?thesis
  4011   proof (cases "n \<ge> 0")
  4012     case True
  4013     then show ?thesis
  4014       apply (auto simp add: not_le *)
  4015       apply (auto simp add: word_rot_defs)
  4016       apply (safe intro!: abl_cong)
  4017       apply (rule rotater_eqs)
  4018       apply (simp add: word_size nat_mod_distrib)
  4019       done
  4020   next
  4021     case False
  4022     moreover define k where "k = - n"
  4023     ultimately have n: "n = - k"
  4024       by simp_all
  4025     from False show ?thesis
  4026       apply (auto simp add: not_le *)
  4027       apply (auto simp add: word_rot_defs)
  4028       apply (simp add: n)
  4029       apply (safe intro!: abl_cong)
  4030       apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  4031       apply (rule rotater_eqs)
  4032       apply (simp add: word_size [symmetric, of w])
  4033       apply (rule of_nat_eq_0_iff [THEN iffD1])
  4034       apply (auto simp add: nat_add_distrib [symmetric] mod_eq_0_iff_dvd)
  4035       using dvd_nat_abs_iff [of "size w" "- k mod int (size w) + k"]
  4036       apply (simp add: algebra_simps)
  4037       apply (simp add: word_size)
  4038       apply (metis (no_types, hide_lams) add.right_inverse dvd_0_right dvd_mod_imp_dvd dvd_refl minus_dvd_iff minus_equation_iff mod_0 mod_add_eq mod_minus_eq)
  4039       done
  4040   qed
  4041 qed
  4042 
  4043 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  4044 
  4045 
  4046 subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
  4047 
  4048 \<comment> \<open>using locale to not pollute lemma namespace\<close>
  4049 locale word_rotate
  4050 begin
  4051 
  4052 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  4053 
  4054 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  4055 
  4056 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
  4057 
  4058 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  4059 
  4060 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
  4061 
  4062 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  4063 
  4064 lemma word_rot_logs:
  4065   "word_rotl n (NOT v) = NOT word_rotl n v"
  4066   "word_rotr n (NOT v) = NOT word_rotr n v"
  4067   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  4068   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  4069   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  4070   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  4071   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  4072   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
  4073   by (rule word_bl.Rep_eqD,
  4074       rule word_rot_defs' [THEN trans],
  4075       simp only: blwl_syms [symmetric],
  4076       rule th1s [THEN trans],
  4077       rule refl)+
  4078 end
  4079 
  4080 lemmas word_rot_logs = word_rotate.word_rot_logs
  4081 
  4082 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  4083   simplified word_bl_Rep']
  4084 
  4085 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  4086   simplified word_bl_Rep']
  4087 
  4088 lemma bl_word_roti_dt':
  4089   "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
  4090     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4091   apply (unfold word_roti_def)
  4092   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4093   apply safe
  4094    apply (simp add: zmod_zminus1_eq_if)
  4095    apply safe
  4096     apply (simp add: nat_mult_distrib)
  4097    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
  4098                                       [THEN conjunct2, THEN order_less_imp_le]]
  4099                     nat_mod_distrib)
  4100   apply (simp add: nat_mod_distrib)
  4101   done
  4102 
  4103 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  4104 
  4105 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4106 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4107 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4108 
  4109 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
  4110   by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
  4111 
  4112 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  4113   by (auto simp: word_roti_def)
  4114 
  4115 lemmas word_rotr_dt_no_bin' [simp] =
  4116   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4117   (* FIXME: negative numerals, 0 and 1 *)
  4118 
  4119 lemmas word_rotl_dt_no_bin' [simp] =
  4120   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4121   (* FIXME: negative numerals, 0 and 1 *)
  4122 
  4123 declare word_roti_def [simp]
  4124 
  4125 
  4126 subsection \<open>Maximum machine word\<close>
  4127 
  4128 lemma word_int_cases:
  4129   fixes x :: "'a::len0 word"
  4130   obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
  4131   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
  4132 
  4133 lemma word_nat_cases [cases type: word]:
  4134   fixes x :: "'a::len word"
  4135   obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
  4136   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
  4137 
  4138 lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
  4139   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
  4140 
  4141 lemma max_word_max [simp,intro!]: "n \<le> max_word"
  4142   by (cases n rule: word_int_cases)
  4143     (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
  4144 
  4145 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
  4146   by (subst word_uint.Abs_norm [symmetric]) simp
  4147 
  4148 lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
  4149 proof -
  4150   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
  4151     by (rule word_of_int_2p_len)
  4152   then show ?thesis by (simp add: word_of_int_2p)
  4153 qed
  4154 
  4155 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
  4156   apply (simp add: max_word_eq)
  4157   apply uint_arith
  4158   apply (auto simp: word_pow_0)
  4159   done
  4160 
  4161 lemma max_word_minus: "max_word = (-1::'a::len word)"
  4162 proof -
  4163   have "-1 + 1 = (0::'a word)"
  4164     by simp
  4165   then show ?thesis
  4166     by (rule max_word_wrap [symmetric])
  4167 qed
  4168 
  4169 lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
  4170   by (subst max_word_minus to_bl_n1)+ simp
  4171 
  4172 lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  4173   by (auto simp: test_bit_bl word_size)
  4174 
  4175 lemma word_and_max [simp]: "x AND max_word = x"
  4176   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4177 
  4178 lemma word_or_max [simp]: "x OR max_word = max_word"
  4179   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4180 
  4181 lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
  4182   for x y z :: "'a::len0 word"
  4183   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4184 
  4185 lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)"
  4186   for x y z :: "'a::len0 word"
  4187   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4188 
  4189 lemma word_and_not [simp]: "x AND NOT x = 0"
  4190   for x :: "'a::len0 word"
  4191   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4192 
  4193 lemma word_or_not [simp]: "x OR NOT x = max_word"
  4194   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4195 
  4196 lemma word_boolean: "boolean (AND) (OR) bitNOT 0 max_word"
  4197   apply (rule boolean.intro)
  4198            apply (rule word_bw_assocs)
  4199           apply (rule word_bw_assocs)
  4200          apply (rule word_bw_comms)
  4201         apply (rule word_bw_comms)
  4202        apply (rule word_ao_dist2)
  4203       apply (rule word_oa_dist2)
  4204      apply (rule word_and_max)
  4205     apply (rule word_log_esimps)
  4206    apply (rule word_and_not)
  4207   apply (rule word_or_not)
  4208   done
  4209 
  4210 interpretation word_bool_alg: boolean "(AND)" "(OR)" bitNOT 0 max_word
  4211   by (rule word_boolean)
  4212 
  4213 lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
  4214   for x y :: "'a::len0 word"
  4215   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4216 
  4217 interpretation word_bool_alg: boolean_xor "(AND)" "(OR)" bitNOT 0 max_word "(XOR)"
  4218   apply (rule boolean_xor.intro)
  4219    apply (rule word_boolean)
  4220   apply (rule boolean_xor_axioms.intro)
  4221   apply (rule word_xor_and_or)
  4222   done
  4223 
  4224 lemma shiftr_x_0 [iff]: "x >> 0 = x"
  4225   for x :: "'a::len0 word"
  4226   by (simp add: shiftr_bl)
  4227 
  4228 lemma shiftl_x_0 [simp]: "x << 0 = x"
  4229   for x :: "'a::len word"
  4230   by (simp add: shiftl_t2n)
  4231 
  4232 lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
  4233   by (simp add: shiftl_t2n)
  4234 
  4235 lemma uint_lt_0 [simp]: "uint x < 0 = False"
  4236   by (simp add: linorder_not_less)
  4237 
  4238 lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0"
  4239   unfolding shiftr1_def by simp
  4240 
  4241 lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  4242   by (induct n) (auto simp: shiftr_def)
  4243 
  4244 lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0"
  4245   for x :: "'a::len word"
  4246   by (simp add: word_less_nat_alt unat_0_iff)
  4247 
  4248 lemma to_bl_mask:
  4249   "to_bl (mask n :: 'a::len word) =
  4250   replicate (len_of TYPE('a) - n) False @
  4251     replicate (min (len_of TYPE('a)) n) True"
  4252   by (simp add: mask_bl word_rep_drop min_def)
  4253 
  4254 lemma map_replicate_True:
  4255   "n = length xs \<Longrightarrow>
  4256     map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
  4257   by (induct xs arbitrary: n) auto
  4258 
  4259 lemma map_replicate_False:
  4260   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
  4261     (zip xs (replicate n False)) = replicate n False"
  4262   by (induct xs arbitrary: n) auto
  4263 
  4264 lemma bl_and_mask:
  4265   fixes w :: "'a::len word"
  4266     and n :: nat
  4267   defines "n' \<equiv> len_of TYPE('a) - n"
  4268   shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
  4269 proof -
  4270   note [simp] = map_replicate_True map_replicate_False
  4271   have "to_bl (w AND mask n) = map2 (\<and>) (to_bl w) (to_bl (mask n::'a::len word))"
  4272     by (simp add: bl_word_and)
  4273   also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
  4274     by simp
  4275   also have "map2 (\<and>) \<dots> (to_bl (mask n::'a::len word)) =
  4276       replicate n' False @ drop n' (to_bl w)"
  4277     unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
  4278   finally show ?thesis .
  4279 qed
  4280 
  4281 lemma drop_rev_takefill:
  4282   "length xs \<le> n \<Longrightarrow>
  4283     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4284   by (simp add: takefill_alt rev_take)
  4285 
  4286 lemma map_nth_0 [simp]: "map ((!!) (0::'a::len0 word)) xs = replicate (length xs) False"
  4287   by (induct xs) auto
  4288 
  4289 lemma uint_plus_if_size:
  4290   "uint (x + y) =
  4291     (if uint x + uint y < 2^size x
  4292      then uint x + uint y
  4293      else uint x + uint y - 2^size x)"
  4294   by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
  4295 
  4296 lemma unat_plus_if_size:
  4297   "unat (x + y) =
  4298     (if unat x + unat y < 2^size x
  4299      then unat x + unat y
  4300      else unat x + unat y - 2^size x)"
  4301   for x y :: "'a::len word"
  4302   apply (subst word_arith_nat_defs)
  4303   apply (subst unat_of_nat)
  4304   apply (simp add:  mod_nat_add word_size)
  4305   done
  4306 
  4307 lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
  4308   for w :: "'a::len word"
  4309   by (simp add: word_gt_0)
  4310 
  4311 lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
  4312   for c :: "'a::len word"
  4313   by (fact unat_div)
  4314 
  4315 lemma uint_sub_if_size:
  4316   "uint (x - y) =
  4317     (if uint y \<le> uint x
  4318      then uint x - uint y
  4319      else uint x - uint y + 2^size x)"
  4320   by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
  4321 
  4322 lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4323   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4324 
  4325 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  4326 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  4327 
  4328 lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  4329 proof -
  4330   have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
  4331     by simp
  4332   show ?thesis
  4333     apply (subst *)
  4334     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  4335     apply simp
  4336     done
  4337 qed
  4338 
  4339 lemmas word_of_int_inj =
  4340   word_uint.Abs_inject [unfolded uints_num, simplified]
  4341 
  4342 lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
  4343   for x y :: "'z::len word"
  4344   by (auto simp add: order_class.le_less)
  4345 
  4346 lemma mod_plus_cong:
  4347   fixes b b' :: int
  4348   assumes 1: "b = b'"
  4349     and 2: "x mod b' = x' mod b'"
  4350     and 3: "y mod b' = y' mod b'"
  4351     and 4: "x' + y' = z'"
  4352   shows "(x + y) mod b = z' mod b'"
  4353 proof -
  4354   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  4355     by (simp add: mod_add_eq)
  4356   also have "\<dots> = (x' + y') mod b'"
  4357     by (simp add: mod_add_eq)
  4358   finally show ?thesis
  4359     by (simp add: 4)
  4360 qed
  4361 
  4362 lemma mod_minus_cong:
  4363   fixes b b' :: int
  4364   assumes "b = b'"
  4365     and "x mod b' = x' mod b'"
  4366     and "y mod b' = y' mod b'"
  4367     and "x' - y' = z'"
  4368   shows "(x - y) mod b = z' mod b'"
  4369   using assms [symmetric] by (auto intro: mod_diff_cong)
  4370 
  4371 lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
  4372   for P :: "'a::len word \<Rightarrow> bool"
  4373   apply (cases m)
  4374   apply atomize
  4375   apply (erule rev_mp)+
  4376   apply (rule_tac x=m in spec)
  4377   apply (induct_tac n)
  4378    apply simp
  4379   apply clarsimp
  4380   apply (erule impE)
  4381    apply clarsimp
  4382    apply (erule_tac x=n in allE)
  4383    apply (erule impE)
  4384     apply (simp add: unat_arith_simps)
  4385     apply (clarsimp simp: unat_of_nat)
  4386    apply simp
  4387   apply (erule_tac x="of_nat na" in allE)
  4388   apply (erule impE)
  4389    apply (simp add: unat_arith_simps)
  4390    apply (clarsimp simp: unat_of_nat)
  4391   apply simp
  4392   done
  4393 
  4394 lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
  4395   for P :: "'a::len word \<Rightarrow> bool"
  4396   by (erule word_induct_less) simp
  4397 
  4398 lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
  4399   for P :: "'b::len word \<Rightarrow> bool"
  4400   apply (rule word_induct)
  4401    apply simp
  4402   apply (case_tac "1 + n = 0")
  4403    apply auto
  4404   done
  4405 
  4406 
  4407 subsection \<open>Recursion combinator for words\<close>
  4408 
  4409 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  4410   where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  4411 
  4412 lemma word_rec_0: "word_rec z s 0 = z"
  4413   by (simp add: word_rec_def)
  4414 
  4415 lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
  4416   for n :: "'a::len word"
  4417   apply (simp add: word_rec_def unat_word_ariths)
  4418   apply (subst nat_mod_eq')
  4419    apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
  4420   apply simp
  4421   done
  4422 
  4423 lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
  4424   apply (rule subst[where t="n" and s="1 + (n - 1)"])
  4425    apply simp
  4426   apply (subst word_rec_Suc)
  4427    apply simp
  4428   apply simp
  4429   done
  4430 
  4431 lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  4432   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4433 
  4434 lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> (+) 1) n"
  4435   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4436 
  4437 lemma word_rec_twice:
  4438   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> (+) (n - m)) m"
  4439   apply (erule rev_mp)
  4440   apply (rule_tac x=z in spec)
  4441   apply (rule_tac x=f in spec)
  4442   apply (induct n)
  4443    apply (simp add: word_rec_0)
  4444   apply clarsimp
  4445   apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  4446    apply simp
  4447   apply (case_tac "1 + (n - m) = 0")
  4448    apply (simp add: word_rec_0)
  4449    apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  4450    apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  4451     apply simp
  4452    apply (simp (no_asm_use))
  4453   apply (simp add: word_rec_Suc word_rec_in2)
  4454   apply (erule impE)
  4455    apply uint_arith
  4456   apply (drule_tac x="x \<circ> (+) 1" in spec)
  4457   apply (drule_tac x="x 0 xa" in spec)
  4458   apply simp
  4459   apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
  4460    apply (clarsimp simp add: fun_eq_iff)
  4461    apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  4462     apply simp
  4463    apply (rule refl)
  4464   apply (rule refl)
  4465   done
  4466 
  4467 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  4468   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  4469 
  4470 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  4471   apply (erule rev_mp)
  4472   apply (induct n)
  4473    apply (auto simp add: word_rec_0 word_rec_Suc)
  4474    apply (drule spec, erule mp)
  4475    apply uint_arith
  4476   apply (drule_tac x=n in spec, erule impE)
  4477    apply uint_arith
  4478   apply simp
  4479   done
  4480 
  4481 lemma word_rec_max:
  4482   "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
  4483   apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  4484    apply simp
  4485   apply simp
  4486   apply (rule word_rec_id_eq)
  4487   apply clarsimp
  4488   apply (drule spec, rule mp, erule mp)
  4489    apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  4490     prefer 2
  4491     apply assumption
  4492    apply simp
  4493   apply (erule contrapos_pn)
  4494   apply simp
  4495   apply (drule arg_cong[where f="\<lambda>x. x - n"])
  4496   apply simp
  4497   done
  4498 
  4499 lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  4500   for n :: "'a::len word"
  4501   by unat_arith
  4502 
  4503 declare bin_to_bl_def [simp]
  4504 
  4505 ML_file "Tools/word_lib.ML"
  4506 ML_file "Tools/smt_word.ML"
  4507 
  4508 hide_const (open) Word
  4509 
  4510 end