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