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