src/HOL/Word/Word.thy
author wenzelm
Mon Apr 03 23:12:16 2017 +0200 (2017-04-03)
changeset 65363 5eb619751b14
parent 65336 8e5274fc0093
child 66453 cc19f7ca2ed6
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> unat (x * y) = unat x * unat y"
  1831   for x y :: "'a::len word"
  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 = test_bit w 0"
  2334   for w :: "'a::len0 word"
  2335   by (auto simp: word_test_bit_def word_lsb_def)
  2336 
  2337 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len0 word)"
  2338   unfolding word_lsb_def uint_eq_0 uint_1 by simp
  2339 
  2340 lemma word_lsb_last: "lsb w = last (to_bl w)"
  2341   for w :: "'a::len word"
  2342   apply (unfold word_lsb_def uint_bl bin_to_bl_def)
  2343   apply (rule_tac bin="uint w" in bin_exhaust)
  2344   apply (cases "size w")
  2345    apply auto
  2346    apply (auto simp add: bin_to_bl_aux_alt)
  2347   done
  2348 
  2349 lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
  2350   by (auto simp: word_lsb_def bin_last_def)
  2351 
  2352 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
  2353   by (simp only: word_msb_def sign_Min_lt_0)
  2354 
  2355 lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  2356   by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
  2357 
  2358 lemma word_msb_numeral [simp]:
  2359   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  2360   unfolding word_numeral_alt by (rule msb_word_of_int)
  2361 
  2362 lemma word_msb_neg_numeral [simp]:
  2363   "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
  2364   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  2365 
  2366 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  2367   by (simp add: word_msb_def)
  2368 
  2369 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  2370   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  2371   by (simp add: Suc_le_eq)
  2372 
  2373 lemma word_msb_nth: "msb w = bin_nth (uint w) (len_of TYPE('a) - 1)"
  2374   for w :: "'a::len word"
  2375   by (simp add: word_msb_def sint_uint bin_sign_lem)
  2376 
  2377 lemma word_msb_alt: "msb w = hd (to_bl w)"
  2378   for w :: "'a::len word"
  2379   apply (unfold word_msb_nth uint_bl)
  2380   apply (subst hd_conv_nth)
  2381    apply (rule length_greater_0_conv [THEN iffD1])
  2382    apply simp
  2383   apply (simp add : nth_bin_to_bl word_size)
  2384   done
  2385 
  2386 lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
  2387   for w :: "'a::len0 word"
  2388   by (auto simp: word_test_bit_def word_set_bit_def)
  2389 
  2390 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
  2391   apply (unfold word_size)
  2392   apply (safe elim!: bin_nth_uint_imp)
  2393    apply (frule bin_nth_uint_imp)
  2394    apply (fast dest!: bin_nth_bl)+
  2395   done
  2396 
  2397 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  2398 
  2399 lemma test_bit_bl: "w !! n \<longleftrightarrow> rev (to_bl w) ! n \<and> n < size w"
  2400   unfolding to_bl_def word_test_bit_def word_size by (rule bin_nth_uint)
  2401 
  2402 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  2403   apply (unfold test_bit_bl)
  2404   apply clarsimp
  2405   apply (rule trans)
  2406    apply (rule nth_rev_alt)
  2407    apply (auto simp add: word_size)
  2408   done
  2409 
  2410 lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
  2411   for w :: "'a::len0 word"
  2412   by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
  2413 
  2414 lemma test_bit_set_gen:
  2415   "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
  2416   for w :: "'a::len0 word"
  2417   apply (unfold word_size word_test_bit_def word_set_bit_def)
  2418   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  2419   apply (auto elim!: test_bit_size [unfolded word_size]
  2420       simp add: word_test_bit_def [symmetric])
  2421   done
  2422 
  2423 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  2424   by (auto simp: of_bl_def bl_to_bin_rep_F)
  2425 
  2426 lemma msb_nth: "msb w = w !! (len_of TYPE('a) - 1)"
  2427   for w :: "'a::len word"
  2428   by (simp add: word_msb_nth word_test_bit_def)
  2429 
  2430 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  2431 lemmas msb1 = msb0 [where i = 0]
  2432 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
  2433 
  2434 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
  2435 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  2436 
  2437 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  2438   "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
  2439     td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
  2440   for w :: "'a::len0 word"
  2441   apply (unfold word_size td_ext_def')
  2442   apply safe
  2443      apply (rule_tac [3] ext)
  2444      apply (rule_tac [4] ext)
  2445      apply (unfold word_size of_nth_def test_bit_bl)
  2446      apply safe
  2447        defer
  2448        apply (clarsimp simp: word_bl.Abs_inverse)+
  2449   apply (rule word_bl.Rep_inverse')
  2450   apply (rule sym [THEN trans])
  2451    apply (rule bl_of_nth_nth)
  2452   apply simp
  2453   apply (rule bl_of_nth_inj)
  2454   apply (clarsimp simp add : test_bit_bl word_size)
  2455   done
  2456 
  2457 interpretation test_bit:
  2458   td_ext
  2459     "op !! :: 'a::len0 word \<Rightarrow> nat \<Rightarrow> bool"
  2460     set_bits
  2461     "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  2462     "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  2463   by (rule td_ext_nth)
  2464 
  2465 lemmas td_nth = test_bit.td_thm
  2466 
  2467 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
  2468   for w :: "'a::len0 word"
  2469   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  2470 
  2471 lemma word_set_set_diff:
  2472   fixes w :: "'a::len0 word"
  2473   assumes "m \<noteq> n"
  2474   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
  2475   by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
  2476 
  2477 lemma nth_sint:
  2478   fixes w :: "'a::len word"
  2479   defines "l \<equiv> len_of TYPE('a)"
  2480   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  2481   unfolding sint_uint l_def
  2482   by (auto simp: nth_sbintr word_test_bit_def [symmetric])
  2483 
  2484 lemma word_lsb_numeral [simp]:
  2485   "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
  2486   unfolding word_lsb_alt test_bit_numeral by simp
  2487 
  2488 lemma word_lsb_neg_numeral [simp]:
  2489   "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
  2490   by (simp add: word_lsb_alt)
  2491 
  2492 lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  2493   unfolding word_set_bit_def
  2494   by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  2495 
  2496 lemma word_set_numeral [simp]:
  2497   "set_bit (numeral bin::'a::len0 word) n b =
  2498     word_of_int (bin_sc n b (numeral bin))"
  2499   unfolding word_numeral_alt by (rule set_bit_word_of_int)
  2500 
  2501 lemma word_set_neg_numeral [simp]:
  2502   "set_bit (- numeral bin::'a::len0 word) n b =
  2503     word_of_int (bin_sc n b (- numeral bin))"
  2504   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  2505 
  2506 lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  2507   unfolding word_0_wi by (rule set_bit_word_of_int)
  2508 
  2509 lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  2510   unfolding word_1_wi by (rule set_bit_word_of_int)
  2511 
  2512 lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  2513   by (simp add: setBit_def)
  2514 
  2515 lemma clearBit_no [simp]:
  2516   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
  2517   by (simp add: clearBit_def)
  2518 
  2519 lemma to_bl_n1: "to_bl (-1::'a::len0 word) = replicate (len_of TYPE('a)) True"
  2520   apply (rule word_bl.Abs_inverse')
  2521    apply simp
  2522   apply (rule word_eqI)
  2523   apply (clarsimp simp add: word_size)
  2524   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
  2525   done
  2526 
  2527 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  2528   unfolding word_msb_alt to_bl_n1 by simp
  2529 
  2530 lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
  2531   for w :: "'a::len0 word"
  2532   apply (rule iffI)
  2533    apply (rule disjCI)
  2534    apply (drule word_eqD)
  2535    apply (erule sym [THEN trans])
  2536    apply (simp add: test_bit_set)
  2537   apply (erule disjE)
  2538    apply clarsimp
  2539   apply (rule word_eqI)
  2540   apply (clarsimp simp add : test_bit_set_gen)
  2541   apply (drule test_bit_size)
  2542   apply force
  2543   done
  2544 
  2545 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  2546   by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
  2547 
  2548 lemma nth_w2p: "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
  2549   by (simp add: test_bit_2p [symmetric] word_of_int [symmetric])
  2550 
  2551 lemma uint_2p: "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  2552   apply (unfold word_arith_power_alt)
  2553   apply (case_tac "len_of TYPE('a)")
  2554    apply clarsimp
  2555   apply (case_tac "nat")
  2556    apply clarsimp
  2557    apply (case_tac "n")
  2558     apply clarsimp
  2559    apply clarsimp
  2560   apply (drule word_gt_0 [THEN iffD1])
  2561   apply (safe intro!: word_eqI)
  2562    apply (auto simp add: nth_2p_bin)
  2563   apply (erule notE)
  2564   apply (simp (no_asm_use) add: uint_word_of_int word_size)
  2565   apply (subst mod_pos_pos_trivial)
  2566     apply simp
  2567    apply (rule power_strict_increasing)
  2568     apply simp_all
  2569   done
  2570 
  2571 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a::len word) = 2 ^ n"
  2572   by (induct n) (simp_all add: wi_hom_syms)
  2573 
  2574 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m \<le> x"
  2575   for x :: "'a::len word"
  2576   apply (rule xtr3)
  2577    apply (rule_tac [2] y = "x" in le_word_or2)
  2578   apply (rule word_eqI)
  2579   apply (auto simp add: word_ao_nth nth_w2p word_size)
  2580   done
  2581 
  2582 lemma word_clr_le: "w \<ge> set_bit w n False"
  2583   for w :: "'a::len0 word"
  2584   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2585   apply (rule order_trans)
  2586    apply (rule bintr_bin_clr_le)
  2587   apply simp
  2588   done
  2589 
  2590 lemma word_set_ge: "w \<le> set_bit w n True"
  2591   for w :: "'a::len word"
  2592   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2593   apply (rule order_trans [OF _ bintr_bin_set_ge])
  2594   apply simp
  2595   done
  2596 
  2597 
  2598 subsection \<open>Shifting, Rotating, and Splitting Words\<close>
  2599 
  2600 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
  2601   unfolding shiftl1_def
  2602   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
  2603   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
  2604   apply (subst bintrunc_bintrunc_min)
  2605   apply simp
  2606   done
  2607 
  2608 lemma shiftl1_numeral [simp]: "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  2609   unfolding word_numeral_alt shiftl1_wi by simp
  2610 
  2611 lemma shiftl1_neg_numeral [simp]: "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  2612   unfolding word_neg_numeral_alt shiftl1_wi by simp
  2613 
  2614 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  2615   by (simp add: shiftl1_def)
  2616 
  2617 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
  2618   by (simp only: shiftl1_def) (* FIXME: duplicate *)
  2619 
  2620 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
  2621   by (simp add: shiftl1_def Bit_B0 wi_hom_syms)
  2622 
  2623 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  2624   by (simp add: shiftr1_def)
  2625 
  2626 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  2627   by (simp add: sshiftr1_def)
  2628 
  2629 lemma sshiftr1_n1 [simp]: "sshiftr1 (- 1) = - 1"
  2630   by (simp add: sshiftr1_def)
  2631 
  2632 lemma shiftl_0 [simp]: "(0::'a::len0 word) << n = 0"
  2633   by (induct n) (auto simp: shiftl_def)
  2634 
  2635 lemma shiftr_0 [simp]: "(0::'a::len0 word) >> n = 0"
  2636   by (induct n) (auto simp: shiftr_def)
  2637 
  2638 lemma sshiftr_0 [simp]: "0 >>> n = 0"
  2639   by (induct n) (auto simp: sshiftr_def)
  2640 
  2641 lemma sshiftr_n1 [simp]: "-1 >>> n = -1"
  2642   by (induct n) (auto simp: sshiftr_def)
  2643 
  2644 lemma nth_shiftl1: "shiftl1 w !! n \<longleftrightarrow> n < size w \<and> n > 0 \<and> w !! (n - 1)"
  2645   apply (unfold shiftl1_def word_test_bit_def)
  2646   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  2647   apply (cases n)
  2648    apply auto
  2649   done
  2650 
  2651 lemma nth_shiftl': "(w << m) !! n \<longleftrightarrow> n < size w \<and> n >= m \<and> w !! (n - m)"
  2652   for w :: "'a::len0 word"
  2653   apply (unfold shiftl_def)
  2654   apply (induct m arbitrary: n)
  2655    apply (force elim!: test_bit_size)
  2656   apply (clarsimp simp add : nth_shiftl1 word_size)
  2657   apply arith
  2658   done
  2659 
  2660 lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
  2661 
  2662 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  2663   apply (unfold shiftr1_def word_test_bit_def)
  2664   apply (simp add: nth_bintr word_ubin.eq_norm)
  2665   apply safe
  2666   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
  2667   apply simp
  2668   done
  2669 
  2670 lemma nth_shiftr: "(w >> m) !! n = w !! (n + m)"
  2671   for w :: "'a::len0 word"
  2672   apply (unfold shiftr_def)
  2673   apply (induct "m" arbitrary: n)
  2674    apply (auto simp add: nth_shiftr1)
  2675   done
  2676 
  2677 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  2678   where f (ie bin_rest) takes normal arguments to normal results,
  2679   thus we get (2) from (1) *)
  2680 
  2681 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
  2682   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  2683   apply (subst bintr_uint [symmetric, OF order_refl])
  2684   apply (simp only : bintrunc_bintrunc_l)
  2685   apply simp
  2686   done
  2687 
  2688 lemma nth_sshiftr1: "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  2689   apply (unfold sshiftr1_def word_test_bit_def)
  2690   apply (simp add: nth_bintr word_ubin.eq_norm bin_nth.Suc [symmetric] word_size
  2691       del: bin_nth.simps)
  2692   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  2693   apply (auto simp add: bin_nth_sint)
  2694   done
  2695 
  2696 lemma nth_sshiftr [rule_format] :
  2697   "\<forall>n. sshiftr w m !! n =
  2698     (n < size w \<and> (if n + m \<ge> size w then w !! (size w - 1) else w !! (n + m)))"
  2699   apply (unfold sshiftr_def)
  2700   apply (induct_tac m)
  2701    apply (simp add: test_bit_bl)
  2702   apply (clarsimp simp add: nth_sshiftr1 word_size)
  2703   apply safe
  2704        apply arith
  2705       apply arith
  2706      apply (erule thin_rl)
  2707      apply (case_tac n)
  2708       apply safe
  2709       apply simp
  2710      apply simp
  2711     apply (erule thin_rl)
  2712     apply (case_tac n)
  2713      apply safe
  2714      apply simp
  2715     apply simp
  2716    apply arith+
  2717   done
  2718 
  2719 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
  2720   apply (unfold shiftr1_def bin_rest_def)
  2721   apply (rule word_uint.Abs_inverse)
  2722   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
  2723   apply (rule xtr7)
  2724    prefer 2
  2725    apply (rule zdiv_le_dividend)
  2726     apply auto
  2727   done
  2728 
  2729 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
  2730   apply (unfold sshiftr1_def bin_rest_def [symmetric])
  2731   apply (simp add: word_sbin.eq_norm)
  2732   apply (rule trans)
  2733    defer
  2734    apply (subst word_sbin.norm_Rep [symmetric])
  2735    apply (rule refl)
  2736   apply (subst word_sbin.norm_Rep [symmetric])
  2737   apply (unfold One_nat_def)
  2738   apply (rule sbintrunc_rest)
  2739   done
  2740 
  2741 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  2742   apply (unfold shiftr_def)
  2743   apply (induct n)
  2744    apply simp
  2745   apply (simp add: shiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  2746   done
  2747 
  2748 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  2749   apply (unfold sshiftr_def)
  2750   apply (induct n)
  2751    apply simp
  2752   apply (simp add: sshiftr1_div_2 mult.commute zdiv_zmult2_eq [symmetric])
  2753   done
  2754 
  2755 
  2756 subsubsection \<open>shift functions in terms of lists of bools\<close>
  2757 
  2758 lemmas bshiftr1_numeral [simp] =
  2759   bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
  2760 
  2761 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
  2762   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
  2763 
  2764 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
  2765   by (simp add: of_bl_def bl_to_bin_append)
  2766 
  2767 lemma shiftl1_bl: "shiftl1 w = of_bl (to_bl w @ [False])"
  2768   for w :: "'a::len0 word"
  2769 proof -
  2770   have "shiftl1 w = shiftl1 (of_bl (to_bl w))"
  2771     by simp
  2772   also have "\<dots> = of_bl (to_bl w @ [False])"
  2773     by (rule shiftl1_of_bl)
  2774   finally show ?thesis .
  2775 qed
  2776 
  2777 lemma bl_shiftl1: "to_bl (shiftl1 w) = tl (to_bl w) @ [False]"
  2778   for w :: "'a::len word"
  2779   by (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons') (fast intro!: Suc_leI)
  2780 
  2781 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  2782 lemma bl_shiftl1': "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  2783   by (simp add: shiftl1_bl word_rep_drop drop_Suc del: drop_append)
  2784 
  2785 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  2786   apply (unfold shiftr1_def uint_bl of_bl_def)
  2787   apply (simp add: butlast_rest_bin word_size)
  2788   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  2789   done
  2790 
  2791 lemma bl_shiftr1: "to_bl (shiftr1 w) = False # butlast (to_bl w)"
  2792   for w :: "'a::len word"
  2793   by (simp add: shiftr1_bl word_rep_drop len_gt_0 [THEN Suc_leI])
  2794 
  2795 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  2796 lemma bl_shiftr1': "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  2797   apply (rule word_bl.Abs_inverse')
  2798    apply (simp del: butlast.simps)
  2799   apply (simp add: shiftr1_bl of_bl_def)
  2800   done
  2801 
  2802 lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  2803   apply (unfold word_reverse_def)
  2804   apply (rule word_bl.Rep_inverse' [symmetric])
  2805   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  2806   apply (cases "to_bl w")
  2807    apply auto
  2808   done
  2809 
  2810 lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  2811   by (induct n) (auto simp add: shiftl_def shiftr_def shiftl1_rev)
  2812 
  2813 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  2814   by (simp add: shiftl_rev)
  2815 
  2816 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  2817   by (simp add: rev_shiftl)
  2818 
  2819 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  2820   by (simp add: shiftr_rev)
  2821 
  2822 lemma bl_sshiftr1: "to_bl (sshiftr1 w) = hd (to_bl w) # butlast (to_bl w)"
  2823   for w :: "'a::len word"
  2824   apply (unfold sshiftr1_def uint_bl word_size)
  2825   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  2826   apply (simp add: sint_uint)
  2827   apply (rule nth_equalityI)
  2828    apply clarsimp
  2829   apply clarsimp
  2830   apply (case_tac i)
  2831    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  2832       nth_bin_to_bl bin_nth.Suc [symmetric] nth_sbintr
  2833       del: bin_nth.Suc)
  2834    apply force
  2835   apply (rule impI)
  2836   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  2837   apply simp
  2838   done
  2839 
  2840 lemma drop_shiftr: "drop n (to_bl (w >> n)) = take (size w - n) (to_bl w)"
  2841   for w :: "'a::len word"
  2842   apply (unfold shiftr_def)
  2843   apply (induct n)
  2844    prefer 2
  2845    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  2846    apply (rule butlast_take [THEN trans])
  2847     apply (auto simp: word_size)
  2848   done
  2849 
  2850 lemma drop_sshiftr: "drop n (to_bl (w >>> n)) = take (size w - n) (to_bl w)"
  2851   for w :: "'a::len word"
  2852   apply (unfold sshiftr_def)
  2853   apply (induct n)
  2854    prefer 2
  2855    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  2856    apply (rule butlast_take [THEN trans])
  2857     apply (auto simp: word_size)
  2858   done
  2859 
  2860 lemma take_shiftr: "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  2861   apply (unfold shiftr_def)
  2862   apply (induct n)
  2863    prefer 2
  2864    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  2865    apply (rule take_butlast [THEN trans])
  2866     apply (auto simp: word_size)
  2867   done
  2868 
  2869 lemma take_sshiftr' [rule_format] :
  2870   "n \<le> size w \<longrightarrow> hd (to_bl (w >>> n)) = hd (to_bl w) \<and>
  2871     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
  2872   for w :: "'a::len word"
  2873   apply (unfold sshiftr_def)
  2874   apply (induct n)
  2875    prefer 2
  2876    apply (simp add: bl_sshiftr1)
  2877    apply (rule impI)
  2878    apply (rule take_butlast [THEN trans])
  2879     apply (auto simp: word_size)
  2880   done
  2881 
  2882 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  2883 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
  2884 
  2885 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
  2886   by (auto intro: append_take_drop_id [symmetric])
  2887 
  2888 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
  2889 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  2890 
  2891 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  2892   by (induct n) (auto simp: shiftl_def shiftl1_of_bl replicate_app_Cons_same)
  2893 
  2894 lemma shiftl_bl: "w << n = of_bl (to_bl w @ replicate n False)"
  2895   for w :: "'a::len0 word"
  2896 proof -
  2897   have "w << n = of_bl (to_bl w) << n"
  2898     by simp
  2899   also have "\<dots> = of_bl (to_bl w @ replicate n False)"
  2900     by (rule shiftl_of_bl)
  2901   finally show ?thesis .
  2902 qed
  2903 
  2904 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  2905 
  2906 lemma bl_shiftl: "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  2907   by (simp add: shiftl_bl word_rep_drop word_size)
  2908 
  2909 lemma shiftl_zero_size: "size x \<le> n \<Longrightarrow> x << n = 0"
  2910   for x :: "'a::len0 word"
  2911   apply (unfold word_size)
  2912   apply (rule word_eqI)
  2913   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  2914   done
  2915 
  2916 (* note - the following results use 'a::len word < number_ring *)
  2917 
  2918 lemma shiftl1_2t: "shiftl1 w = 2 * w"
  2919   for w :: "'a::len word"
  2920   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  2921 
  2922 lemma shiftl1_p: "shiftl1 w = w + w"
  2923   for w :: "'a::len word"
  2924   by (simp add: shiftl1_2t)
  2925 
  2926 lemma shiftl_t2n: "shiftl w n = 2 ^ n * w"
  2927   for w :: "'a::len word"
  2928   by (induct n) (auto simp: shiftl_def shiftl1_2t)
  2929 
  2930 lemma shiftr1_bintr [simp]:
  2931   "(shiftr1 (numeral w) :: 'a::len0 word) =
  2932     word_of_int (bin_rest (bintrunc (len_of TYPE('a)) (numeral w)))"
  2933   unfolding shiftr1_def word_numeral_alt by (simp add: word_ubin.eq_norm)
  2934 
  2935 lemma sshiftr1_sbintr [simp]:
  2936   "(sshiftr1 (numeral w) :: 'a::len word) =
  2937     word_of_int (bin_rest (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  2938   unfolding sshiftr1_def word_numeral_alt by (simp add: word_sbin.eq_norm)
  2939 
  2940 lemma shiftr_no [simp]:
  2941   (* FIXME: neg_numeral *)
  2942   "(numeral w::'a::len0 word) >> n = word_of_int
  2943     ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  2944   by (rule word_eqI) (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  2945 
  2946 lemma sshiftr_no [simp]:
  2947   (* FIXME: neg_numeral *)
  2948   "(numeral w::'a::len word) >>> n = word_of_int
  2949     ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  2950   apply (rule word_eqI)
  2951   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
  2952    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
  2953   done
  2954 
  2955 lemma shiftr1_bl_of:
  2956   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  2957     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  2958   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin word_ubin.eq_norm trunc_bl2bin)
  2959 
  2960 lemma shiftr_bl_of:
  2961   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  2962     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
  2963   apply (unfold shiftr_def)
  2964   apply (induct n)
  2965    apply clarsimp
  2966   apply clarsimp
  2967   apply (subst shiftr1_bl_of)
  2968    apply simp
  2969   apply (simp add: butlast_take)
  2970   done
  2971 
  2972 lemma shiftr_bl: "x >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  2973   for x :: "'a::len0 word"
  2974   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  2975 
  2976 lemma msb_shift: "msb w \<longleftrightarrow> w >> (len_of TYPE('a) - 1) \<noteq> 0"
  2977   for w :: "'a::len word"
  2978   apply (unfold shiftr_bl word_msb_alt)
  2979   apply (simp add: word_size Suc_le_eq take_Suc)
  2980   apply (cases "hd (to_bl w)")
  2981    apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
  2982   done
  2983 
  2984 lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
  2985   apply (induct ys arbitrary: n)
  2986    apply simp_all
  2987   apply (case_tac n)
  2988    apply simp_all
  2989   done
  2990 
  2991 lemma align_lem_or [rule_format] :
  2992   "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  2993     drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  2994     map2 op | x y = take m x @ drop m y"
  2995   apply (induct y)
  2996    apply force
  2997   apply clarsimp
  2998   apply (case_tac x)
  2999    apply force
  3000   apply (case_tac m)
  3001    apply auto
  3002   apply (drule_tac t="length xs" for xs in sym)
  3003   apply (auto simp: map2_def zip_replicate o_def)
  3004   done
  3005 
  3006 lemma align_lem_and [rule_format] :
  3007   "\<forall>x m. length x = n + m \<longrightarrow> length y = n + m \<longrightarrow>
  3008     drop m x = replicate n False \<longrightarrow> take m y = replicate m False \<longrightarrow>
  3009     map2 op \<and> x y = replicate (n + m) False"
  3010   apply (induct y)
  3011    apply force
  3012   apply clarsimp
  3013   apply (case_tac x)
  3014    apply force
  3015   apply (case_tac m)
  3016   apply auto
  3017   apply (drule_tac t="length xs" for xs in sym)
  3018   apply (auto simp: map2_def zip_replicate o_def map_replicate_const)
  3019   done
  3020 
  3021 lemma aligned_bl_add_size [OF refl]:
  3022   "size x - n = m \<Longrightarrow> n \<le> size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  3023     take m (to_bl y) = replicate m False \<Longrightarrow>
  3024     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  3025   apply (subgoal_tac "x AND y = 0")
  3026    prefer 2
  3027    apply (rule word_bl.Rep_eqD)
  3028    apply (simp add: bl_word_and)
  3029    apply (rule align_lem_and [THEN trans])
  3030        apply (simp_all add: word_size)[5]
  3031    apply simp
  3032   apply (subst word_plus_and_or [symmetric])
  3033   apply (simp add : bl_word_or)
  3034   apply (rule align_lem_or)
  3035      apply (simp_all add: word_size)
  3036   done
  3037 
  3038 
  3039 subsubsection \<open>Mask\<close>
  3040 
  3041 lemma nth_mask [OF refl, simp]: "m = mask n \<Longrightarrow> test_bit m i \<longleftrightarrow> i < n \<and> i < size m"
  3042   apply (unfold mask_def test_bit_bl)
  3043   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  3044   apply (clarsimp simp add: word_size)
  3045   apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
  3046   apply (fold of_bl_def)
  3047   apply (simp add: word_1_bl)
  3048   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
  3049   apply auto
  3050   done
  3051 
  3052 lemma mask_bl: "mask n = of_bl (replicate n True)"
  3053   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
  3054 
  3055 lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
  3056   by (auto simp add: nth_bintr word_size intro: word_eqI)
  3057 
  3058 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
  3059   apply (rule word_eqI)
  3060   apply (simp add: nth_bintr word_size word_ops_nth_size)
  3061   apply (auto simp add: test_bit_bin)
  3062   done
  3063 
  3064 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  3065   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3066 
  3067 lemma and_mask_wi':
  3068   "word_of_int i AND mask n = (word_of_int (bintrunc (min LENGTH('a) n) i) :: 'a::len word)"
  3069   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3070 
  3071 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  3072   unfolding word_numeral_alt by (rule and_mask_wi)
  3073 
  3074 lemma bl_and_mask':
  3075   "to_bl (w AND mask n :: 'a::len word) =
  3076     replicate (len_of TYPE('a) - n) False @
  3077     drop (len_of TYPE('a) - n) (to_bl w)"
  3078   apply (rule nth_equalityI)
  3079    apply simp
  3080   apply (clarsimp simp add: to_bl_nth word_size)
  3081   apply (simp add: word_size word_ops_nth_size)
  3082   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
  3083   done
  3084 
  3085 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
  3086   by (simp only: and_mask_bintr bintrunc_mod2p)
  3087 
  3088 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
  3089   apply (simp add: and_mask_bintr word_ubin.eq_norm)
  3090   apply (simp add: bintrunc_mod2p)
  3091   apply (rule xtr8)
  3092    prefer 2
  3093    apply (rule pos_mod_bound)
  3094    apply auto
  3095   done
  3096 
  3097 lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  3098   for b n :: int
  3099   by (simp add: int_mod_lem eq_sym_conv)
  3100 
  3101 lemma mask_eq_iff: "w AND mask n = w \<longleftrightarrow> uint w < 2 ^ n"
  3102   apply (simp add: and_mask_bintr)
  3103   apply (simp add: word_ubin.inverse_norm)
  3104   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
  3105   apply (fast intro!: lt2p_lem)
  3106   done
  3107 
  3108 lemma and_mask_dvd: "2 ^ n dvd uint w \<longleftrightarrow> w AND mask n = 0"
  3109   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  3110   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs del: word_of_int_0)
  3111   apply (subst word_uint.norm_Rep [symmetric])
  3112   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  3113   apply auto
  3114   done
  3115 
  3116 lemma and_mask_dvd_nat: "2 ^ n dvd unat w \<longleftrightarrow> w AND mask n = 0"
  3117   apply (unfold unat_def)
  3118   apply (rule trans [OF _ and_mask_dvd])
  3119   apply (unfold dvd_def)
  3120   apply auto
  3121    apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  3122    apply simp
  3123   apply (simp add: nat_mult_distrib nat_power_eq)
  3124   done
  3125 
  3126 lemma word_2p_lem: "n < size w \<Longrightarrow> w < 2 ^ n = (uint w < 2 ^ n)"
  3127   for w :: "'a::len word"
  3128   apply (unfold word_size word_less_alt word_numeral_alt)
  3129   apply (auto simp add: word_of_int_power_hom word_uint.eq_norm mod_pos_pos_trivial
  3130       simp del: word_of_int_numeral)
  3131   done
  3132 
  3133 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = x"
  3134   for x :: "'a::len word"
  3135   apply (unfold word_less_alt word_numeral_alt)
  3136   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom word_uint.eq_norm
  3137       simp del: word_of_int_numeral)
  3138   apply (drule xtr8 [rotated])
  3139    apply (rule int_mod_le)
  3140    apply (auto simp add : mod_pos_pos_trivial)
  3141   done
  3142 
  3143 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  3144 
  3145 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
  3146 
  3147 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  3148   unfolding word_size by (erule and_mask_less')
  3149 
  3150 lemma word_mod_2p_is_mask [OF refl]: "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = x AND mask n"
  3151   for c x :: "'a::len word"
  3152   by (auto simp: word_mod_def uint_2p and_mask_mod_2p)
  3153 
  3154 lemma mask_eqs:
  3155   "(a AND mask n) + b AND mask n = a + b AND mask n"
  3156   "a + (b AND mask n) AND mask n = a + b AND mask n"
  3157   "(a AND mask n) - b AND mask n = a - b AND mask n"
  3158   "a - (b AND mask n) AND mask n = a - b AND mask n"
  3159   "a * (b AND mask n) AND mask n = a * b AND mask n"
  3160   "(b AND mask n) * a AND mask n = b * a AND mask n"
  3161   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
  3162   "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
  3163   "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
  3164   "- (a AND mask n) AND mask n = - a AND mask n"
  3165   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  3166   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  3167   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  3168   by (auto simp: and_mask_wi' word_of_int_homs word.abs_eq_iff bintrunc_mod2p mod_simps)
  3169 
  3170 lemma mask_power_eq: "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  3171   using word_of_int_Ex [where x=x]
  3172   by (auto simp: and_mask_wi' word_of_int_power_hom word.abs_eq_iff bintrunc_mod2p mod_simps)
  3173 
  3174 
  3175 subsubsection \<open>Revcast\<close>
  3176 
  3177 lemmas revcast_def' = revcast_def [simplified]
  3178 lemmas revcast_def'' = revcast_def' [simplified word_size]
  3179 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  3180 
  3181 lemma to_bl_revcast:
  3182   "to_bl (revcast w :: 'a::len0 word) = takefill False (len_of TYPE('a)) (to_bl w)"
  3183   apply (unfold revcast_def' word_size)
  3184   apply (rule word_bl.Abs_inverse)
  3185   apply simp
  3186   done
  3187 
  3188 lemma revcast_rev_ucast [OF refl refl refl]:
  3189   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
  3190     rc = word_reverse uc"
  3191   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  3192   apply (auto simp: to_bl_of_bin takefill_bintrunc)
  3193   apply (simp add: word_bl.Abs_inverse word_size)
  3194   done
  3195 
  3196 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  3197   using revcast_rev_ucast [of "word_reverse w"] by simp
  3198 
  3199 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
  3200   by (fact revcast_rev_ucast [THEN word_rev_gal'])
  3201 
  3202 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
  3203   by (fact revcast_ucast [THEN word_rev_gal'])
  3204 
  3205 
  3206 text "linking revcast and cast via shift"
  3207 
  3208 lemmas wsst_TYs = source_size target_size word_size
  3209 
  3210 lemma revcast_down_uu [OF refl]:
  3211   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
  3212   for w :: "'a::len word"
  3213   apply (simp add: revcast_def')
  3214   apply (rule word_bl.Rep_inverse')
  3215   apply (rule trans, rule ucast_down_drop)
  3216    prefer 2
  3217    apply (rule trans, rule drop_shiftr)
  3218    apply (auto simp: takefill_alt wsst_TYs)
  3219   done
  3220 
  3221 lemma revcast_down_us [OF refl]:
  3222   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
  3223   for w :: "'a::len word"
  3224   apply (simp add: revcast_def')
  3225   apply (rule word_bl.Rep_inverse')
  3226   apply (rule trans, rule ucast_down_drop)
  3227    prefer 2
  3228    apply (rule trans, rule drop_sshiftr)
  3229    apply (auto simp: takefill_alt wsst_TYs)
  3230   done
  3231 
  3232 lemma revcast_down_su [OF refl]:
  3233   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
  3234   for w :: "'a::len word"
  3235   apply (simp add: revcast_def')
  3236   apply (rule word_bl.Rep_inverse')
  3237   apply (rule trans, rule scast_down_drop)
  3238    prefer 2
  3239    apply (rule trans, rule drop_shiftr)
  3240    apply (auto simp: takefill_alt wsst_TYs)
  3241   done
  3242 
  3243 lemma revcast_down_ss [OF refl]:
  3244   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
  3245   for w :: "'a::len word"
  3246   apply (simp add: revcast_def')
  3247   apply (rule word_bl.Rep_inverse')
  3248   apply (rule trans, rule scast_down_drop)
  3249    prefer 2
  3250    apply (rule trans, rule drop_sshiftr)
  3251    apply (auto simp: takefill_alt wsst_TYs)
  3252   done
  3253 
  3254 (* FIXME: should this also be [OF refl] ? *)
  3255 lemma cast_down_rev:
  3256   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> uc w = revcast (w << n)"
  3257   for w :: "'a::len word"
  3258   apply (unfold shiftl_rev)
  3259   apply clarify
  3260   apply (simp add: revcast_rev_ucast)
  3261   apply (rule word_rev_gal')
  3262   apply (rule trans [OF _ revcast_rev_ucast])
  3263   apply (rule revcast_down_uu [symmetric])
  3264   apply (auto simp add: wsst_TYs)
  3265   done
  3266 
  3267 lemma revcast_up [OF refl]:
  3268   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
  3269     rc w = (ucast w :: 'a::len word) << n"
  3270   apply (simp add: revcast_def')
  3271   apply (rule word_bl.Rep_inverse')
  3272   apply (simp add: takefill_alt)
  3273   apply (rule bl_shiftl [THEN trans])
  3274   apply (subst ucast_up_app)
  3275    apply (auto simp add: wsst_TYs)
  3276   done
  3277 
  3278 lemmas rc1 = revcast_up [THEN
  3279   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3280 lemmas rc2 = revcast_down_uu [THEN
  3281   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3282 
  3283 lemmas ucast_up =
  3284  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
  3285 lemmas ucast_down =
  3286   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
  3287 
  3288 
  3289 subsubsection \<open>Slices\<close>
  3290 
  3291 lemma slice1_no_bin [simp]:
  3292   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
  3293   by (simp add: slice1_def) (* TODO: neg_numeral *)
  3294 
  3295 lemma slice_no_bin [simp]:
  3296   "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b::len0) - n)
  3297     (bin_to_bl (len_of TYPE('b::len0)) (numeral w)))"
  3298   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
  3299 
  3300 lemma slice1_0 [simp] : "slice1 n 0 = 0"
  3301   unfolding slice1_def by simp
  3302 
  3303 lemma slice_0 [simp] : "slice n 0 = 0"
  3304   unfolding slice_def by auto
  3305 
  3306 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
  3307   unfolding slice_def' slice1_def
  3308   by (simp add : takefill_alt word_size)
  3309 
  3310 lemmas slice_take = slice_take' [unfolded word_size]
  3311 
  3312 \<comment> "shiftr to a word of the same size is just slice,
  3313     slice is just shiftr then ucast"
  3314 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
  3315 
  3316 lemma slice_shiftr: "slice n w = ucast (w >> n)"
  3317   apply (unfold slice_take shiftr_bl)
  3318   apply (rule ucast_of_bl_up [symmetric])
  3319   apply (simp add: word_size)
  3320   done
  3321 
  3322 lemma nth_slice: "(slice n w :: 'a::len0 word) !! m = (w !! (m + n) \<and> m < len_of TYPE('a))"
  3323   by (simp add: slice_shiftr nth_ucast nth_shiftr)
  3324 
  3325 lemma slice1_down_alt':
  3326   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
  3327     to_bl sl = takefill False fs (drop k (to_bl w))"
  3328   by (auto simp: slice1_def word_size of_bl_def uint_bl
  3329       word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  3330 
  3331 lemma slice1_up_alt':
  3332   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
  3333     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  3334   apply (unfold slice1_def word_size of_bl_def uint_bl)
  3335   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
  3336   apply (rule_tac f = "\<lambda>k. takefill False (len_of TYPE('a))
  3337     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
  3338   apply arith
  3339   done
  3340 
  3341 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
  3342 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
  3343 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
  3344 lemmas slice1_up_alts =
  3345   le_add_diff_inverse [symmetric, THEN su1]
  3346   le_add_diff_inverse2 [symmetric, THEN su1]
  3347 
  3348 lemma ucast_slice1: "ucast w = slice1 (size w) w"
  3349   by (simp add: slice1_def ucast_bl takefill_same' word_size)
  3350 
  3351 lemma ucast_slice: "ucast w = slice 0 w"
  3352   by (simp add: slice_def ucast_slice1)
  3353 
  3354 lemma slice_id: "slice 0 t = t"
  3355   by (simp only: ucast_slice [symmetric] ucast_id)
  3356 
  3357 lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  3358   by (simp add: slice1_def revcast_def' word_size)
  3359 
  3360 lemma slice1_tf_tf':
  3361   "to_bl (slice1 n w :: 'a::len0 word) =
  3362     rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
  3363   unfolding slice1_def by (rule word_rev_tf)
  3364 
  3365 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
  3366 
  3367 lemma rev_slice1:
  3368   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
  3369     slice1 n (word_reverse w :: 'b::len0 word) =
  3370     word_reverse (slice1 k w :: 'a::len0 word)"
  3371   apply (unfold word_reverse_def slice1_tf_tf)
  3372   apply (rule word_bl.Rep_inverse')
  3373   apply (rule rev_swap [THEN iffD1])
  3374   apply (rule trans [symmetric])
  3375    apply (rule tf_rev)
  3376    apply (simp add: word_bl.Abs_inverse)
  3377   apply (simp add: word_bl.Abs_inverse)
  3378   done
  3379 
  3380 lemma rev_slice:
  3381   "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
  3382     slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
  3383   apply (unfold slice_def word_size)
  3384   apply (rule rev_slice1)
  3385   apply arith
  3386   done
  3387 
  3388 lemmas sym_notr =
  3389   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
  3390 
  3391 \<comment> \<open>problem posed by TPHOLs referee:
  3392       criterion for overflow of addition of signed integers\<close>
  3393 
  3394 lemma sofl_test:
  3395   "(sint x + sint y = sint (x + y)) =
  3396      ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
  3397   for x y :: "'a::len word"
  3398   apply (unfold word_size)
  3399   apply (cases "len_of TYPE('a)", simp)
  3400   apply (subst msb_shift [THEN sym_notr])
  3401   apply (simp add: word_ops_msb)
  3402   apply (simp add: word_msb_sint)
  3403   apply safe
  3404        apply simp_all
  3405      apply (unfold sint_word_ariths)
  3406      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
  3407      apply safe
  3408          apply (insert sint_range' [where x=x])
  3409          apply (insert sint_range' [where x=y])
  3410          defer
  3411          apply (simp (no_asm), arith)
  3412         apply (simp (no_asm), arith)
  3413        defer
  3414        defer
  3415        apply (simp (no_asm), arith)
  3416       apply (simp (no_asm), arith)
  3417      apply (rule notI [THEN notnotD],
  3418       drule leI not_le_imp_less,
  3419       drule sbintrunc_inc sbintrunc_dec,
  3420       simp)+
  3421   done
  3422 
  3423 
  3424 subsection \<open>Split and cat\<close>
  3425 
  3426 lemmas word_split_bin' = word_split_def
  3427 lemmas word_cat_bin' = word_cat_def
  3428 
  3429 lemma word_rsplit_no:
  3430   "(word_rsplit (numeral bin :: 'b::len0 word) :: 'a word list) =
  3431     map word_of_int (bin_rsplit (len_of TYPE('a::len))
  3432       (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
  3433   by (simp add: word_rsplit_def word_ubin.eq_norm)
  3434 
  3435 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
  3436   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  3437 
  3438 lemma test_bit_cat:
  3439   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc \<and>
  3440     (if n < size b then b !! n else a !! (n - size b)))"
  3441   apply (auto simp: word_cat_bin' test_bit_bin word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  3442   apply (erule bin_nth_uint_imp)
  3443   done
  3444 
  3445 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
  3446   by (simp add: of_bl_def to_bl_def word_cat_bin' bl_to_bin_app_cat)
  3447 
  3448 lemma of_bl_append:
  3449   "(of_bl (xs @ ys) :: 'a::len word) = of_bl xs * 2^(length ys) + of_bl ys"
  3450   apply (simp add: of_bl_def bl_to_bin_app_cat bin_cat_num)
  3451   apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
  3452   done
  3453 
  3454 lemma of_bl_False [simp]: "of_bl (False#xs) = of_bl xs"
  3455   by (rule word_eqI) (auto simp: test_bit_of_bl nth_append)
  3456 
  3457 lemma of_bl_True [simp]: "(of_bl (True # xs) :: 'a::len word) = 2^length xs + of_bl xs"
  3458   by (subst of_bl_append [where xs="[True]", simplified]) (simp add: word_1_bl)
  3459 
  3460 lemma of_bl_Cons: "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  3461   by (cases x) simp_all
  3462 
  3463 lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
  3464     a = bintrunc (len_of TYPE('a) - n) a \<and> b = bintrunc (len_of TYPE('a)) b"
  3465   for w :: "'a::len0 word"
  3466   apply (frule word_ubin.norm_Rep [THEN ssubst])
  3467   apply (drule bin_split_trunc1)
  3468   apply (drule sym [THEN trans])
  3469    apply assumption
  3470   apply safe
  3471   done
  3472 
  3473 lemma word_split_bl':
  3474   "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
  3475     (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c)))"
  3476   apply (unfold word_split_bin')
  3477   apply safe
  3478    defer
  3479    apply (clarsimp split: prod.splits)
  3480    apply hypsubst_thin
  3481    apply (drule word_ubin.norm_Rep [THEN ssubst])
  3482    apply (drule split_bintrunc)
  3483    apply (simp add: of_bl_def bl2bin_drop word_size
  3484       word_ubin.norm_eq_iff [symmetric] min_def del: word_ubin.norm_Rep)
  3485   apply (clarsimp split: prod.splits)
  3486   apply (frule split_uint_lem [THEN conjunct1])
  3487   apply (unfold word_size)
  3488   apply (cases "len_of TYPE('a) \<ge> len_of TYPE('b)")
  3489    defer
  3490    apply simp
  3491   apply (simp add : of_bl_def to_bl_def)
  3492   apply (subst bin_split_take1 [symmetric])
  3493     prefer 2
  3494     apply assumption
  3495    apply simp
  3496   apply (erule thin_rl)
  3497   apply (erule arg_cong [THEN trans])
  3498   apply (simp add : word_ubin.norm_eq_iff [symmetric])
  3499   done
  3500 
  3501 lemma word_split_bl: "std = size c - size b \<Longrightarrow>
  3502     (a = of_bl (take std (to_bl c)) \<and> b = of_bl (drop std (to_bl c))) \<longleftrightarrow>
  3503     word_split c = (a, b)"
  3504   apply (rule iffI)
  3505    defer
  3506    apply (erule (1) word_split_bl')
  3507   apply (case_tac "word_split c")
  3508   apply (auto simp add: word_size)
  3509   apply (frule word_split_bl' [rotated])
  3510    apply (auto simp add: word_size)
  3511   done
  3512 
  3513 lemma word_split_bl_eq:
  3514   "(word_split c :: ('c::len0 word \<times> 'd::len0 word)) =
  3515     (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
  3516      of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
  3517   for c :: "'a::len word"
  3518   apply (rule word_split_bl [THEN iffD1])
  3519    apply (unfold word_size)
  3520    apply (rule refl conjI)+
  3521   done
  3522 
  3523 \<comment> "keep quantifiers for use in simplification"
  3524 lemma test_bit_split':
  3525   "word_split c = (a, b) \<longrightarrow>
  3526     (\<forall>n m.
  3527       b !! n = (n < size b \<and> c !! n) \<and>
  3528       a !! m = (m < size a \<and> c !! (m + size b)))"
  3529   apply (unfold word_split_bin' test_bit_bin)
  3530   apply (clarify)
  3531   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
  3532   apply (drule bin_nth_split)
  3533   apply safe
  3534        apply (simp_all add: add.commute)
  3535    apply (erule bin_nth_uint_imp)+
  3536   done
  3537 
  3538 lemma test_bit_split:
  3539   "word_split c = (a, b) \<Longrightarrow>
  3540     (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and>
  3541     (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
  3542   by (simp add: test_bit_split')
  3543 
  3544 lemma test_bit_split_eq:
  3545   "word_split c = (a, b) \<longleftrightarrow>
  3546     ((\<forall>n::nat. b !! n = (n < size b \<and> c !! n)) \<and>
  3547      (\<forall>m::nat. a !! m = (m < size a \<and> c !! (m + size b))))"
  3548   apply (rule_tac iffI)
  3549    apply (rule_tac conjI)
  3550     apply (erule test_bit_split [THEN conjunct1])
  3551    apply (erule test_bit_split [THEN conjunct2])
  3552   apply (case_tac "word_split c")
  3553   apply (frule test_bit_split)
  3554   apply (erule trans)
  3555   apply (fastforce intro!: word_eqI simp add: word_size)
  3556   done
  3557 
  3558 \<comment> \<open>this odd result is analogous to \<open>ucast_id\<close>,
  3559       result to the length given by the result type\<close>
  3560 
  3561 lemma word_cat_id: "word_cat a b = b"
  3562   by (simp add: word_cat_bin' word_ubin.inverse_norm)
  3563 
  3564 \<comment> "limited hom result"
  3565 lemma word_cat_hom:
  3566   "len_of TYPE('a::len0) \<le> len_of TYPE('b::len0) + len_of TYPE('c::len0) \<Longrightarrow>
  3567     (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
  3568     word_of_int (bin_cat w (size b) (uint b))"
  3569   by (auto simp: word_cat_def word_size word_ubin.norm_eq_iff [symmetric]
  3570       word_ubin.eq_norm bintr_cat min.absorb1)
  3571 
  3572 lemma word_cat_split_alt: "size w \<le> size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  3573   apply (rule word_eqI)
  3574   apply (drule test_bit_split)
  3575   apply (clarsimp simp add : test_bit_cat word_size)
  3576   apply safe
  3577   apply arith
  3578   done
  3579 
  3580 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
  3581 
  3582 
  3583 subsubsection \<open>Split and slice\<close>
  3584 
  3585 lemma split_slices: "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w \<and> v = slice 0 w"
  3586   apply (drule test_bit_split)
  3587   apply (rule conjI)
  3588    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  3589   done
  3590 
  3591 lemma slice_cat1 [OF refl]:
  3592   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  3593   apply safe
  3594   apply (rule word_eqI)
  3595   apply (simp add: nth_slice test_bit_cat word_size)
  3596   done
  3597 
  3598 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  3599 
  3600 lemma cat_slices:
  3601   "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  3602     size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  3603   apply safe
  3604   apply (rule word_eqI)
  3605   apply (simp add: nth_slice test_bit_cat word_size)
  3606   apply safe
  3607   apply arith
  3608   done
  3609 
  3610 lemma word_split_cat_alt:
  3611   "w = word_cat u v \<Longrightarrow> size u + size v \<le> size w \<Longrightarrow> word_split w = (u, v)"
  3612   apply (case_tac "word_split w")
  3613   apply (rule trans, assumption)
  3614   apply (drule test_bit_split)
  3615   apply safe
  3616    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  3617   done
  3618 
  3619 lemmas word_cat_bl_no_bin [simp] =
  3620   word_cat_bl [where a="numeral a" and b="numeral b", unfolded to_bl_numeral]
  3621   for a b (* FIXME: negative numerals, 0 and 1 *)
  3622 
  3623 lemmas word_split_bl_no_bin [simp] =
  3624   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
  3625 
  3626 text \<open>
  3627   This odd result arises from the fact that the statement of the
  3628   result implies that the decoded words are of the same type,
  3629   and therefore of the same length, as the original word.\<close>
  3630 
  3631 lemma word_rsplit_same: "word_rsplit w = [w]"
  3632   by (simp add: word_rsplit_def bin_rsplit_all)
  3633 
  3634 lemma word_rsplit_empty_iff_size: "word_rsplit w = [] \<longleftrightarrow> size w = 0"
  3635   by (simp add: word_rsplit_def bin_rsplit_def word_size bin_rsplit_aux_simp_alt Let_def
  3636       split: prod.split)
  3637 
  3638 lemma test_bit_rsplit:
  3639   "sw = word_rsplit w \<Longrightarrow> m < size (hd sw) \<Longrightarrow>
  3640     k < length sw \<Longrightarrow> (rev sw ! k) !! m = w !! (k * size (hd sw) + m)"
  3641   for sw :: "'a::len word list"
  3642   apply (unfold word_rsplit_def word_test_bit_def)
  3643   apply (rule trans)
  3644    apply (rule_tac f = "\<lambda>x. bin_nth x m" in arg_cong)
  3645    apply (rule nth_map [symmetric])
  3646    apply simp
  3647   apply (rule bin_nth_rsplit)
  3648      apply simp_all
  3649   apply (simp add : word_size rev_map)
  3650   apply (rule trans)
  3651    defer
  3652    apply (rule map_ident [THEN fun_cong])
  3653   apply (rule refl [THEN map_cong])
  3654   apply (simp add : word_ubin.eq_norm)
  3655   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  3656   done
  3657 
  3658 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  3659   by (auto simp: word_rcat_def to_bl_def' of_bl_def bin_rcat_bl)
  3660 
  3661 lemma size_rcat_lem': "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  3662   by (induct wl) (auto simp: word_size)
  3663 
  3664 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  3665 
  3666 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
  3667 
  3668 lemma nth_rcat_lem:
  3669   "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
  3670     rev (concat (map to_bl wl)) ! n =
  3671     rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
  3672   apply (induct wl)
  3673    apply clarsimp
  3674   apply (clarsimp simp add : nth_append size_rcat_lem)
  3675   apply (simp (no_asm_use) only:  mult_Suc [symmetric]
  3676          td_gal_lt_len less_Suc_eq_le minus_div_mult_eq_mod [symmetric])
  3677   apply clarsimp
  3678   done
  3679 
  3680 lemma test_bit_rcat:
  3681   "sw = size (hd wl) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
  3682     (n < size rc \<and> n div sw < size wl \<and> (rev wl) ! (n div sw) !! (n mod sw))"
  3683   for wl :: "'a::len word list"
  3684   apply (unfold word_rcat_bl word_size)
  3685   apply (clarsimp simp add: test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  3686   apply safe
  3687    apply (auto simp: test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  3688   done
  3689 
  3690 lemma foldl_eq_foldr: "foldl op + x xs = foldr op + (x # xs) 0"
  3691   for x :: "'a::comm_monoid_add"
  3692   by (induct xs arbitrary: x) (auto simp: add.assoc)
  3693 
  3694 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  3695 
  3696 lemmas test_bit_rsplit_alt =
  3697   trans [OF nth_rev_alt [THEN test_bit_cong]
  3698   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  3699 
  3700 \<comment> "lazy way of expressing that u and v, and su and sv, have same types"
  3701 lemma word_rsplit_len_indep [OF refl refl refl refl]:
  3702   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
  3703     word_rsplit v = sv \<Longrightarrow> length su = length sv"
  3704   by (auto simp: word_rsplit_def bin_rsplit_len_indep)
  3705 
  3706 lemma length_word_rsplit_size:
  3707   "n = len_of TYPE('a::len) \<Longrightarrow>
  3708     length (word_rsplit w :: 'a word list) \<le> m \<longleftrightarrow> size w \<le> m * n"
  3709   by (auto simp: word_rsplit_def word_size bin_rsplit_len_le)
  3710 
  3711 lemmas length_word_rsplit_lt_size =
  3712   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  3713 
  3714 lemma length_word_rsplit_exp_size:
  3715   "n = len_of TYPE('a::len) \<Longrightarrow>
  3716     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  3717   by (auto simp: word_rsplit_def word_size bin_rsplit_len)
  3718 
  3719 lemma length_word_rsplit_even_size:
  3720   "n = len_of TYPE('a::len) \<Longrightarrow> size w = m * n \<Longrightarrow>
  3721     length (word_rsplit w :: 'a word list) = m"
  3722   by (auto simp: length_word_rsplit_exp_size given_quot_alt)
  3723 
  3724 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  3725 
  3726 (* alternative proof of word_rcat_rsplit *)
  3727 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
  3728 lemmas dtle = xtr4 [OF tdle mult.commute]
  3729 
  3730 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  3731   apply (rule word_eqI)
  3732   apply (clarsimp simp: test_bit_rcat word_size)
  3733   apply (subst refl [THEN test_bit_rsplit])
  3734     apply (simp_all add: word_size
  3735       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  3736    apply safe
  3737    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  3738   done
  3739 
  3740 lemma size_word_rsplit_rcat_size:
  3741   "word_rcat ws = frcw \<Longrightarrow> size frcw = length ws * len_of TYPE('a)
  3742     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  3743   for ws :: "'a::len word list" and frcw :: "'b::len0 word"
  3744   apply (clarsimp simp: word_size length_word_rsplit_exp_size')
  3745   apply (fast intro: given_quot_alt)
  3746   done
  3747 
  3748 lemma msrevs:
  3749   "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  3750   "(k * n + m) mod n = m mod n"
  3751   for n :: nat
  3752   by (auto simp: add.commute)
  3753 
  3754 lemma word_rsplit_rcat_size [OF refl]:
  3755   "word_rcat ws = frcw \<Longrightarrow>
  3756     size frcw = length ws * len_of TYPE('a) \<Longrightarrow> word_rsplit frcw = ws"
  3757   for ws :: "'a::len word list"
  3758   apply (frule size_word_rsplit_rcat_size, assumption)
  3759   apply (clarsimp simp add : word_size)
  3760   apply (rule nth_equalityI, assumption)
  3761   apply clarsimp
  3762   apply (rule word_eqI [rule_format])
  3763   apply (rule trans)
  3764    apply (rule test_bit_rsplit_alt)
  3765      apply (clarsimp simp: word_size)+
  3766   apply (rule trans)
  3767    apply (rule test_bit_rcat [OF refl refl])
  3768   apply (simp add: word_size)
  3769   apply (subst nth_rev)
  3770    apply arith
  3771   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3772   apply safe
  3773   apply (simp add: diff_mult_distrib)
  3774   apply (rule mpl_lem)
  3775    apply (cases "size ws")
  3776     apply simp_all
  3777   done
  3778 
  3779 
  3780 subsection \<open>Rotation\<close>
  3781 
  3782 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  3783 
  3784 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  3785 
  3786 lemma rotate_eq_mod: "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  3787   apply (rule box_equals)
  3788     defer
  3789     apply (rule rotate_conv_mod [symmetric])+
  3790   apply simp
  3791   done
  3792 
  3793 lemmas rotate_eqs =
  3794   trans [OF rotate0 [THEN fun_cong] id_apply]
  3795   rotate_rotate [symmetric]
  3796   rotate_id
  3797   rotate_conv_mod
  3798   rotate_eq_mod
  3799 
  3800 
  3801 subsubsection \<open>Rotation of list to right\<close>
  3802 
  3803 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  3804   by (cases l) (auto simp: rotater1_def)
  3805 
  3806 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  3807   apply (unfold rotater1_def)
  3808   apply (cases "l")
  3809    apply (case_tac [2] "list")
  3810     apply auto
  3811   done
  3812 
  3813 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  3814   by (cases l) (auto simp: rotater1_def)
  3815 
  3816 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  3817   by (cases "xs") (simp add: rotater1_def, simp add: rotate1_rl')
  3818 
  3819 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  3820   by (induct n) (auto simp: rotater_def intro: rotater1_rev')
  3821 
  3822 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
  3823   using rotater_rev' [where xs = "rev ys"] by simp
  3824 
  3825 lemma rotater_drop_take:
  3826   "rotater n xs =
  3827     drop (length xs - n mod length xs) xs @
  3828     take (length xs - n mod length xs) xs"
  3829   by (auto simp: rotater_rev rotate_drop_take rev_take rev_drop)
  3830 
  3831 lemma rotater_Suc [simp]: "rotater (Suc n) xs = rotater1 (rotater n xs)"
  3832   unfolding rotater_def by auto
  3833 
  3834 lemma rotate_inv_plus [rule_format] :
  3835   "\<forall>k. k = m + n \<longrightarrow> rotater k (rotate n xs) = rotater m xs \<and>
  3836     rotate k (rotater n xs) = rotate m xs \<and>
  3837     rotater n (rotate k xs) = rotate m xs \<and>
  3838     rotate n (rotater k xs) = rotater m xs"
  3839   by (induct n) (auto simp: rotater_def rotate_def intro: funpow_swap1 [THEN trans])
  3840 
  3841 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  3842 
  3843 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  3844 
  3845 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
  3846 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
  3847 
  3848 lemma rotate_gal: "rotater n xs = ys \<longleftrightarrow> rotate n ys = xs"
  3849   by auto
  3850 
  3851 lemma rotate_gal': "ys = rotater n xs \<longleftrightarrow> xs = rotate n ys"
  3852   by auto
  3853 
  3854 lemma length_rotater [simp]: "length (rotater n xs) = length xs"
  3855   by (simp add : rotater_rev)
  3856 
  3857 lemma restrict_to_left: "x = y \<Longrightarrow> x = z \<longleftrightarrow> y = z"
  3858   by simp
  3859 
  3860 lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
  3861   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
  3862 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  3863 lemmas rotater_eqs = rrs1 [simplified length_rotater]
  3864 lemmas rotater_0 = rotater_eqs (1)
  3865 lemmas rotater_add = rotater_eqs (2)
  3866 
  3867 
  3868 subsubsection \<open>map, map2, commuting with rotate(r)\<close>
  3869 
  3870 lemma butlast_map: "xs \<noteq> [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  3871   by (induct xs) auto
  3872 
  3873 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
  3874   by (cases xs) (auto simp: rotater1_def last_map butlast_map)
  3875 
  3876 lemma rotater_map: "rotater n (map f xs) = map f (rotater n xs)"
  3877   by (induct n) (auto simp: rotater_def rotater1_map)
  3878 
  3879 lemma but_last_zip [rule_format] :
  3880   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
  3881     last (zip xs ys) = (last xs, last ys) \<and>
  3882     butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
  3883   apply (induct xs)
  3884    apply auto
  3885      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3886   done
  3887 
  3888 lemma but_last_map2 [rule_format] :
  3889   "\<forall>ys. length xs = length ys \<longrightarrow> xs \<noteq> [] \<longrightarrow>
  3890     last (map2 f xs ys) = f (last xs) (last ys) \<and>
  3891     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
  3892   apply (induct xs)
  3893    apply auto
  3894      apply (unfold map2_def)
  3895      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3896   done
  3897 
  3898 lemma rotater1_zip:
  3899   "length xs = length ys \<Longrightarrow>
  3900     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
  3901   apply (unfold rotater1_def)
  3902   apply (cases xs)
  3903    apply auto
  3904    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  3905   done
  3906 
  3907 lemma rotater1_map2:
  3908   "length xs = length ys \<Longrightarrow>
  3909     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
  3910   by (simp add: map2_def rotater1_map rotater1_zip)
  3911 
  3912 lemmas lrth =
  3913   box_equals [OF asm_rl length_rotater [symmetric]
  3914                  length_rotater [symmetric],
  3915               THEN rotater1_map2]
  3916 
  3917 lemma rotater_map2:
  3918   "length xs = length ys \<Longrightarrow>
  3919     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
  3920   by (induct n) (auto intro!: lrth)
  3921 
  3922 lemma rotate1_map2:
  3923   "length xs = length ys \<Longrightarrow>
  3924     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
  3925   by (cases xs; cases ys) (auto simp: map2_def)
  3926 
  3927 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
  3928   length_rotate [symmetric], THEN rotate1_map2]
  3929 
  3930 lemma rotate_map2:
  3931   "length xs = length ys \<Longrightarrow>
  3932     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
  3933   by (induct n) (auto intro!: lth)
  3934 
  3935 
  3936 \<comment> "corresponding equalities for word rotation"
  3937 
  3938 lemma to_bl_rotl: "to_bl (word_rotl n w) = rotate n (to_bl w)"
  3939   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  3940 
  3941 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  3942 
  3943 lemmas word_rotl_eqs =
  3944   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  3945 
  3946 lemma to_bl_rotr: "to_bl (word_rotr n w) = rotater n (to_bl w)"
  3947   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  3948 
  3949 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  3950 
  3951 lemmas word_rotr_eqs =
  3952   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  3953 
  3954 declare word_rotr_eqs (1) [simp]
  3955 declare word_rotl_eqs (1) [simp]
  3956 
  3957 lemma word_rot_rl [simp]: "word_rotl k (word_rotr k v) = v"
  3958   and word_rot_lr [simp]: "word_rotr k (word_rotl k v) = v"
  3959   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  3960 
  3961 lemma word_rot_gal: "word_rotr n v = w \<longleftrightarrow> word_rotl n w = v"
  3962   and word_rot_gal': "w = word_rotr n v \<longleftrightarrow> v = word_rotl n w"
  3963   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] dest: sym)
  3964 
  3965 lemma word_rotr_rev: "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  3966   by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev to_bl_rotr to_bl_rotl rotater_rev)
  3967 
  3968 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  3969   by (auto simp: word_rot_defs)
  3970 
  3971 lemmas abl_cong = arg_cong [where f = "of_bl"]
  3972 
  3973 lemma word_roti_add: "word_roti (m + n) w = word_roti m (word_roti n w)"
  3974 proof -
  3975   have rotater_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  3976     by auto
  3977 
  3978   have rotate_eq_lem: "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  3979     by auto
  3980 
  3981   note rpts [symmetric] =
  3982     rotate_inv_plus [THEN conjunct1]
  3983     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  3984     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  3985     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  3986 
  3987   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  3988   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  3989 
  3990   show ?thesis
  3991     apply (unfold word_rot_defs)
  3992     apply (simp only: split: if_split)
  3993     apply (safe intro!: abl_cong)
  3994            apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
  3995                   to_bl_rotl
  3996                   to_bl_rotr [THEN word_bl.Rep_inverse']
  3997                   to_bl_rotr)
  3998          apply (rule rrp rrrp rpts,
  3999                 simp add: nat_add_distrib [symmetric]
  4000                 nat_diff_distrib [symmetric])+
  4001     done
  4002 qed
  4003 
  4004 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
  4005   apply (unfold word_rot_defs)
  4006   apply (cut_tac y="size w" in gt_or_eq_0)
  4007   apply (erule disjE)
  4008    apply simp_all
  4009   apply (safe intro!: abl_cong)
  4010    apply (rule rotater_eqs)
  4011    apply (simp add: word_size nat_mod_distrib)
  4012   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  4013   apply (rule rotater_eqs)
  4014   apply (simp add: word_size nat_mod_distrib)
  4015   apply (rule of_nat_eq_0_iff [THEN iffD1])
  4016   apply (auto simp add: not_le mod_eq_0_iff_dvd zdvd_int nat_add_distrib [symmetric])
  4017   using mod_mod_trivial mod_eq_dvd_iff
  4018   apply blast
  4019   done
  4020 
  4021 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  4022 
  4023 
  4024 subsubsection \<open>"Word rotation commutes with bit-wise operations\<close>
  4025 
  4026 (* using locale to not pollute lemma namespace *)
  4027 locale word_rotate
  4028 begin
  4029 
  4030 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  4031 
  4032 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  4033 
  4034 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
  4035 
  4036 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  4037 
  4038 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
  4039 
  4040 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  4041 
  4042 lemma word_rot_logs:
  4043   "word_rotl n (NOT v) = NOT word_rotl n v"
  4044   "word_rotr n (NOT v) = NOT word_rotr n v"
  4045   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  4046   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  4047   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  4048   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  4049   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  4050   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
  4051   by (rule word_bl.Rep_eqD,
  4052       rule word_rot_defs' [THEN trans],
  4053       simp only: blwl_syms [symmetric],
  4054       rule th1s [THEN trans],
  4055       rule refl)+
  4056 end
  4057 
  4058 lemmas word_rot_logs = word_rotate.word_rot_logs
  4059 
  4060 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  4061   simplified word_bl_Rep']
  4062 
  4063 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  4064   simplified word_bl_Rep']
  4065 
  4066 lemma bl_word_roti_dt':
  4067   "n = nat ((- i) mod int (size (w :: 'a::len word))) \<Longrightarrow>
  4068     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4069   apply (unfold word_roti_def)
  4070   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4071   apply safe
  4072    apply (simp add: zmod_zminus1_eq_if)
  4073    apply safe
  4074     apply (simp add: nat_mult_distrib)
  4075    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
  4076                                       [THEN conjunct2, THEN order_less_imp_le]]
  4077                     nat_mod_distrib)
  4078   apply (simp add: nat_mod_distrib)
  4079   done
  4080 
  4081 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  4082 
  4083 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4084 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4085 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4086 
  4087 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 \<and> word_rotl i 0 = 0"
  4088   by (simp add: word_rotr_dt word_rotl_dt replicate_add [symmetric])
  4089 
  4090 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  4091   by (auto simp: word_roti_def)
  4092 
  4093 lemmas word_rotr_dt_no_bin' [simp] =
  4094   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4095   (* FIXME: negative numerals, 0 and 1 *)
  4096 
  4097 lemmas word_rotl_dt_no_bin' [simp] =
  4098   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4099   (* FIXME: negative numerals, 0 and 1 *)
  4100 
  4101 declare word_roti_def [simp]
  4102 
  4103 
  4104 subsection \<open>Maximum machine word\<close>
  4105 
  4106 lemma word_int_cases:
  4107   fixes x :: "'a::len0 word"
  4108   obtains n where "x = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
  4109   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
  4110 
  4111 lemma word_nat_cases [cases type: word]:
  4112   fixes x :: "'a::len word"
  4113   obtains n where "x = of_nat n" and "n < 2^len_of TYPE('a)"
  4114   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
  4115 
  4116 lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
  4117   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
  4118 
  4119 lemma max_word_max [simp,intro!]: "n \<le> max_word"
  4120   by (cases n rule: word_int_cases)
  4121     (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
  4122 
  4123 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
  4124   by (subst word_uint.Abs_norm [symmetric]) simp
  4125 
  4126 lemma word_pow_0: "(2::'a::len word) ^ len_of TYPE('a) = 0"
  4127 proof -
  4128   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
  4129     by (rule word_of_int_2p_len)
  4130   then show ?thesis by (simp add: word_of_int_2p)
  4131 qed
  4132 
  4133 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
  4134   apply (simp add: max_word_eq)
  4135   apply uint_arith
  4136   apply (auto simp: word_pow_0)
  4137   done
  4138 
  4139 lemma max_word_minus: "max_word = (-1::'a::len word)"
  4140 proof -
  4141   have "-1 + 1 = (0::'a word)"
  4142     by simp
  4143   then show ?thesis
  4144     by (rule max_word_wrap [symmetric])
  4145 qed
  4146 
  4147 lemma max_word_bl [simp]: "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
  4148   by (subst max_word_minus to_bl_n1)+ simp
  4149 
  4150 lemma max_test_bit [simp]: "(max_word::'a::len word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  4151   by (auto simp: test_bit_bl word_size)
  4152 
  4153 lemma word_and_max [simp]: "x AND max_word = x"
  4154   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4155 
  4156 lemma word_or_max [simp]: "x OR max_word = max_word"
  4157   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4158 
  4159 lemma word_ao_dist2: "x AND (y OR z) = x AND y OR x AND z"
  4160   for x y z :: "'a::len0 word"
  4161   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4162 
  4163 lemma word_oa_dist2: "x OR y AND z = (x OR y) AND (x OR z)"
  4164   for x y z :: "'a::len0 word"
  4165   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4166 
  4167 lemma word_and_not [simp]: "x AND NOT x = 0"
  4168   for x :: "'a::len0 word"
  4169   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4170 
  4171 lemma word_or_not [simp]: "x OR NOT x = max_word"
  4172   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4173 
  4174 lemma word_boolean: "boolean (op AND) (op OR) bitNOT 0 max_word"
  4175   apply (rule boolean.intro)
  4176            apply (rule word_bw_assocs)
  4177           apply (rule word_bw_assocs)
  4178          apply (rule word_bw_comms)
  4179         apply (rule word_bw_comms)
  4180        apply (rule word_ao_dist2)
  4181       apply (rule word_oa_dist2)
  4182      apply (rule word_and_max)
  4183     apply (rule word_log_esimps)
  4184    apply (rule word_and_not)
  4185   apply (rule word_or_not)
  4186   done
  4187 
  4188 interpretation word_bool_alg: boolean "op AND" "op OR" bitNOT 0 max_word
  4189   by (rule word_boolean)
  4190 
  4191 lemma word_xor_and_or: "x XOR y = x AND NOT y OR NOT x AND y"
  4192   for x y :: "'a::len0 word"
  4193   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4194 
  4195 interpretation word_bool_alg: boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
  4196   apply (rule boolean_xor.intro)
  4197    apply (rule word_boolean)
  4198   apply (rule boolean_xor_axioms.intro)
  4199   apply (rule word_xor_and_or)
  4200   done
  4201 
  4202 lemma shiftr_x_0 [iff]: "x >> 0 = x"
  4203   for x :: "'a::len0 word"
  4204   by (simp add: shiftr_bl)
  4205 
  4206 lemma shiftl_x_0 [simp]: "x << 0 = x"
  4207   for x :: "'a::len word"
  4208   by (simp add: shiftl_t2n)
  4209 
  4210 lemma shiftl_1 [simp]: "(1::'a::len word) << n = 2^n"
  4211   by (simp add: shiftl_t2n)
  4212 
  4213 lemma uint_lt_0 [simp]: "uint x < 0 = False"
  4214   by (simp add: linorder_not_less)
  4215 
  4216 lemma shiftr1_1 [simp]: "shiftr1 (1::'a::len word) = 0"
  4217   unfolding shiftr1_def by simp
  4218 
  4219 lemma shiftr_1[simp]: "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  4220   by (induct n) (auto simp: shiftr_def)
  4221 
  4222 lemma word_less_1 [simp]: "x < 1 \<longleftrightarrow> x = 0"
  4223   for x :: "'a::len word"
  4224   by (simp add: word_less_nat_alt unat_0_iff)
  4225 
  4226 lemma to_bl_mask:
  4227   "to_bl (mask n :: 'a::len word) =
  4228   replicate (len_of TYPE('a) - n) False @
  4229     replicate (min (len_of TYPE('a)) n) True"
  4230   by (simp add: mask_bl word_rep_drop min_def)
  4231 
  4232 lemma map_replicate_True:
  4233   "n = length xs \<Longrightarrow>
  4234     map (\<lambda>(x,y). x \<and> y) (zip xs (replicate n True)) = xs"
  4235   by (induct xs arbitrary: n) auto
  4236 
  4237 lemma map_replicate_False:
  4238   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x \<and> y)
  4239     (zip xs (replicate n False)) = replicate n False"
  4240   by (induct xs arbitrary: n) auto
  4241 
  4242 lemma bl_and_mask:
  4243   fixes w :: "'a::len word"
  4244     and n :: nat
  4245   defines "n' \<equiv> len_of TYPE('a) - n"
  4246   shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
  4247 proof -
  4248   note [simp] = map_replicate_True map_replicate_False
  4249   have "to_bl (w AND mask n) = map2 op \<and> (to_bl w) (to_bl (mask n::'a::len word))"
  4250     by (simp add: bl_word_and)
  4251   also have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)"
  4252     by simp
  4253   also have "map2 op \<and> \<dots> (to_bl (mask n::'a::len word)) =
  4254       replicate n' False @ drop n' (to_bl w)"
  4255     unfolding to_bl_mask n'_def map2_def by (subst zip_append) auto
  4256   finally show ?thesis .
  4257 qed
  4258 
  4259 lemma drop_rev_takefill:
  4260   "length xs \<le> n \<Longrightarrow>
  4261     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4262   by (simp add: takefill_alt rev_take)
  4263 
  4264 lemma map_nth_0 [simp]: "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  4265   by (induct xs) auto
  4266 
  4267 lemma uint_plus_if_size:
  4268   "uint (x + y) =
  4269     (if uint x + uint y < 2^size x
  4270      then uint x + uint y
  4271      else uint x + uint y - 2^size x)"
  4272   by (simp add: word_arith_wis int_word_uint mod_add_if_z word_size)
  4273 
  4274 lemma unat_plus_if_size:
  4275   "unat (x + y) =
  4276     (if unat x + unat y < 2^size x
  4277      then unat x + unat y
  4278      else unat x + unat y - 2^size x)"
  4279   for x y :: "'a::len word"
  4280   apply (subst word_arith_nat_defs)
  4281   apply (subst unat_of_nat)
  4282   apply (simp add:  mod_nat_add word_size)
  4283   done
  4284 
  4285 lemma word_neq_0_conv: "w \<noteq> 0 \<longleftrightarrow> 0 < w"
  4286   for w :: "'a::len word"
  4287   by (simp add: word_gt_0)
  4288 
  4289 lemma max_lt: "unat (max a b div c) = unat (max a b) div unat c"
  4290   for c :: "'a::len word"
  4291   by (fact unat_div)
  4292 
  4293 lemma uint_sub_if_size:
  4294   "uint (x - y) =
  4295     (if uint y \<le> uint x
  4296      then uint x - uint y
  4297      else uint x - uint y + 2^size x)"
  4298   by (simp add: word_arith_wis int_word_uint mod_sub_if_z word_size)
  4299 
  4300 lemma unat_sub: "b \<le> a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4301   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4302 
  4303 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  4304 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  4305 
  4306 lemma word_of_int_minus: "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  4307 proof -
  4308   have *: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)"
  4309     by simp
  4310   show ?thesis
  4311     apply (subst *)
  4312     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  4313     apply simp
  4314     done
  4315 qed
  4316 
  4317 lemmas word_of_int_inj =
  4318   word_uint.Abs_inject [unfolded uints_num, simplified]
  4319 
  4320 lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
  4321   for x y :: "'z::len word"
  4322   by (auto simp add: order_class.le_less)
  4323 
  4324 lemma mod_plus_cong:
  4325   fixes b b' :: int
  4326   assumes 1: "b = b'"
  4327     and 2: "x mod b' = x' mod b'"
  4328     and 3: "y mod b' = y' mod b'"
  4329     and 4: "x' + y' = z'"
  4330   shows "(x + y) mod b = z' mod b'"
  4331 proof -
  4332   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  4333     by (simp add: mod_add_eq)
  4334   also have "\<dots> = (x' + y') mod b'"
  4335     by (simp add: mod_add_eq)
  4336   finally show ?thesis
  4337     by (simp add: 4)
  4338 qed
  4339 
  4340 lemma mod_minus_cong:
  4341   fixes b b' :: int
  4342   assumes "b = b'"
  4343     and "x mod b' = x' mod b'"
  4344     and "y mod b' = y' mod b'"
  4345     and "x' - y' = z'"
  4346   shows "(x - y) mod b = z' mod b'"
  4347   using assms [symmetric] by (auto intro: mod_diff_cong)
  4348 
  4349 lemma word_induct_less: "P 0 \<Longrightarrow> (\<And>n. n < m \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
  4350   for P :: "'a::len word \<Rightarrow> bool"
  4351   apply (cases m)
  4352   apply atomize
  4353   apply (erule rev_mp)+
  4354   apply (rule_tac x=m in spec)
  4355   apply (induct_tac n)
  4356    apply simp
  4357   apply clarsimp
  4358   apply (erule impE)
  4359    apply clarsimp
  4360    apply (erule_tac x=n in allE)
  4361    apply (erule impE)
  4362     apply (simp add: unat_arith_simps)
  4363     apply (clarsimp simp: unat_of_nat)
  4364    apply simp
  4365   apply (erule_tac x="of_nat na" in allE)
  4366   apply (erule impE)
  4367    apply (simp add: unat_arith_simps)
  4368    apply (clarsimp simp: unat_of_nat)
  4369   apply simp
  4370   done
  4371 
  4372 lemma word_induct: "P 0 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P m"
  4373   for P :: "'a::len word \<Rightarrow> bool"
  4374   by (erule word_induct_less) simp
  4375 
  4376 lemma word_induct2 [induct type]: "P 0 \<Longrightarrow> (\<And>n. 1 + n \<noteq> 0 \<Longrightarrow> P n \<Longrightarrow> P (1 + n)) \<Longrightarrow> P n"
  4377   for P :: "'b::len word \<Rightarrow> bool"
  4378   apply (rule word_induct)
  4379    apply simp
  4380   apply (case_tac "1 + n = 0")
  4381    apply auto
  4382   done
  4383 
  4384 
  4385 subsection \<open>Recursion combinator for words\<close>
  4386 
  4387 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  4388   where "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  4389 
  4390 lemma word_rec_0: "word_rec z s 0 = z"
  4391   by (simp add: word_rec_def)
  4392 
  4393 lemma word_rec_Suc: "1 + n \<noteq> 0 \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
  4394   for n :: "'a::len word"
  4395   apply (simp add: word_rec_def unat_word_ariths)
  4396   apply (subst nat_mod_eq')
  4397    apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
  4398   apply simp
  4399   done
  4400 
  4401 lemma word_rec_Pred: "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
  4402   apply (rule subst[where t="n" and s="1 + (n - 1)"])
  4403    apply simp
  4404   apply (subst word_rec_Suc)
  4405    apply simp
  4406   apply simp
  4407   done
  4408 
  4409 lemma word_rec_in: "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  4410   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4411 
  4412 lemma word_rec_in2: "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  4413   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4414 
  4415 lemma word_rec_twice:
  4416   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  4417   apply (erule rev_mp)
  4418   apply (rule_tac x=z in spec)
  4419   apply (rule_tac x=f in spec)
  4420   apply (induct n)
  4421    apply (simp add: word_rec_0)
  4422   apply clarsimp
  4423   apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  4424    apply simp
  4425   apply (case_tac "1 + (n - m) = 0")
  4426    apply (simp add: word_rec_0)
  4427    apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  4428    apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  4429     apply simp
  4430    apply (simp (no_asm_use))
  4431   apply (simp add: word_rec_Suc word_rec_in2)
  4432   apply (erule impE)
  4433    apply uint_arith
  4434   apply (drule_tac x="x \<circ> op + 1" in spec)
  4435   apply (drule_tac x="x 0 xa" in spec)
  4436   apply simp
  4437   apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)" in subst)
  4438    apply (clarsimp simp add: fun_eq_iff)
  4439    apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  4440     apply simp
  4441    apply (rule refl)
  4442   apply (rule refl)
  4443   done
  4444 
  4445 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  4446   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  4447 
  4448 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  4449   apply (erule rev_mp)
  4450   apply (induct n)
  4451    apply (auto simp add: word_rec_0 word_rec_Suc)
  4452    apply (drule spec, erule mp)
  4453    apply uint_arith
  4454   apply (drule_tac x=n in spec, erule impE)
  4455    apply uint_arith
  4456   apply simp
  4457   done
  4458 
  4459 lemma word_rec_max:
  4460   "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
  4461   apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  4462    apply simp
  4463   apply simp
  4464   apply (rule word_rec_id_eq)
  4465   apply clarsimp
  4466   apply (drule spec, rule mp, erule mp)
  4467    apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  4468     prefer 2
  4469     apply assumption
  4470    apply simp
  4471   apply (erule contrapos_pn)
  4472   apply simp
  4473   apply (drule arg_cong[where f="\<lambda>x. x - n"])
  4474   apply simp
  4475   done
  4476 
  4477 lemma unatSuc: "1 + n \<noteq> 0 \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  4478   for n :: "'a::len word"
  4479   by unat_arith
  4480 
  4481 declare bin_to_bl_def [simp]
  4482 
  4483 ML_file "Tools/word_lib.ML"
  4484 ML_file "Tools/smt_word.ML"
  4485 
  4486 hide_const (open) Word
  4487 
  4488 end