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