src/HOL/Word/Word.thy
author wenzelm
Tue Feb 26 20:09:25 2013 +0100 (2013-02-26)
changeset 51286 44a521ff87cf
parent 51143 0a2371e7ced3
child 51375 d9e62d9c98de
permissions -rw-r--r--
tuned;
     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 cr_word op =) (bintrunc (len_of TYPE('a)))
   251     (uint :: 'a::len0 word \<Rightarrow> int)"
   252   unfolding fun_rel_def 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 = cr_word) numeral numeral"
   603   "(fun_rel op = cr_word) neg_numeral neg_numeral"
   604   unfolding fun_rel_def 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_ss_of ss = 
  1451   ss 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_ss_of (simpset_of ctxt)) 1,
  1464       ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits}
  1465                                       |> fold Simplifier.add_cong @{thms power_False_cong})),
  1466       rewrite_goals_tac @{thms word_size}, 
  1467       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
  1468                          REPEAT (etac conjE n) THEN
  1469                          REPEAT (dtac @{thm word_of_int_inverse} n 
  1470                                  THEN atac n 
  1471                                  THEN atac n)),
  1472       TRYALL arith_tac' ]
  1473   end
  1474 
  1475 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
  1476 *}
  1477 
  1478 method_setup uint_arith = 
  1479   {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
  1480   "solving word arithmetic via integers and arith"
  1481 
  1482 
  1483 subsection "More on overflows and monotonicity"
  1484 
  1485 lemma no_plus_overflow_uint_size: 
  1486   "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
  1487   unfolding word_size by uint_arith
  1488 
  1489 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
  1490 
  1491 lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
  1492   by uint_arith
  1493 
  1494 lemma no_olen_add':
  1495   fixes x :: "'a::len0 word"
  1496   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
  1497   by (simp add: add_ac no_olen_add)
  1498 
  1499 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
  1500 
  1501 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem]
  1502 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1]
  1503 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem]
  1504 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
  1505 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
  1506 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
  1507 
  1508 lemma word_less_sub1: 
  1509   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
  1510   by uint_arith
  1511 
  1512 lemma word_le_sub1: 
  1513   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
  1514   by uint_arith
  1515 
  1516 lemma sub_wrap_lt: 
  1517   "((x :: 'a :: len0 word) < x - z) = (x < z)"
  1518   by uint_arith
  1519 
  1520 lemma sub_wrap: 
  1521   "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
  1522   by uint_arith
  1523 
  1524 lemma plus_minus_not_NULL_ab: 
  1525   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
  1526   by uint_arith
  1527 
  1528 lemma plus_minus_no_overflow_ab: 
  1529   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c" 
  1530   by uint_arith
  1531 
  1532 lemma le_minus': 
  1533   "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
  1534   by uint_arith
  1535 
  1536 lemma le_plus': 
  1537   "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
  1538   by uint_arith
  1539 
  1540 lemmas le_plus = le_plus' [rotated]
  1541 
  1542 lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
  1543 
  1544 lemma word_plus_mono_right: 
  1545   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
  1546   by uint_arith
  1547 
  1548 lemma word_less_minus_cancel: 
  1549   "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
  1550   by uint_arith
  1551 
  1552 lemma word_less_minus_mono_left: 
  1553   "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
  1554   by uint_arith
  1555 
  1556 lemma word_less_minus_mono:  
  1557   "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c 
  1558   \<Longrightarrow> a - b < c - (d::'a::len word)"
  1559   by uint_arith
  1560 
  1561 lemma word_le_minus_cancel: 
  1562   "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
  1563   by uint_arith
  1564 
  1565 lemma word_le_minus_mono_left: 
  1566   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
  1567   by uint_arith
  1568 
  1569 lemma word_le_minus_mono:  
  1570   "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c 
  1571   \<Longrightarrow> a - b <= c - (d::'a::len word)"
  1572   by uint_arith
  1573 
  1574 lemma plus_le_left_cancel_wrap: 
  1575   "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
  1576   by uint_arith
  1577 
  1578 lemma plus_le_left_cancel_nowrap: 
  1579   "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow> 
  1580     (x + y' < x + y) = (y' < y)" 
  1581   by uint_arith
  1582 
  1583 lemma word_plus_mono_right2: 
  1584   "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
  1585   by uint_arith
  1586 
  1587 lemma word_less_add_right: 
  1588   "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
  1589   by uint_arith
  1590 
  1591 lemma word_less_sub_right: 
  1592   "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
  1593   by uint_arith
  1594 
  1595 lemma word_le_plus_either: 
  1596   "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
  1597   by uint_arith
  1598 
  1599 lemma word_less_nowrapI: 
  1600   "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
  1601   by uint_arith
  1602 
  1603 lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
  1604   by uint_arith
  1605 
  1606 lemma inc_i: 
  1607   "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
  1608   by uint_arith
  1609 
  1610 lemma udvd_incr_lem:
  1611   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 
  1612     uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
  1613   apply clarsimp
  1614   apply (drule less_le_mult)
  1615   apply safe
  1616   done
  1617 
  1618 lemma udvd_incr': 
  1619   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
  1620     uint q = ua + n' * uint K \<Longrightarrow> p + K <= q" 
  1621   apply (unfold word_less_alt word_le_def)
  1622   apply (drule (2) udvd_incr_lem)
  1623   apply (erule uint_add_le [THEN order_trans])
  1624   done
  1625 
  1626 lemma udvd_decr': 
  1627   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
  1628     uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
  1629   apply (unfold word_less_alt word_le_def)
  1630   apply (drule (2) udvd_incr_lem)
  1631   apply (drule le_diff_eq [THEN iffD2])
  1632   apply (erule order_trans)
  1633   apply (rule uint_sub_ge)
  1634   done
  1635 
  1636 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
  1637 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
  1638 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
  1639 
  1640 lemma udvd_minus_le': 
  1641   "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
  1642   apply (unfold udvd_def)
  1643   apply clarify
  1644   apply (erule (2) udvd_decr0)
  1645   done
  1646 
  1647 lemma udvd_incr2_K: 
  1648   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
  1649     0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
  1650   using [[simproc del: linordered_ring_less_cancel_factor]]
  1651   apply (unfold udvd_def)
  1652   apply clarify
  1653   apply (simp add: uint_arith_simps split: split_if_asm)
  1654    prefer 2 
  1655    apply (insert uint_range' [of s])[1]
  1656    apply arith
  1657   apply (drule add_commute [THEN xtr1])
  1658   apply (simp add: diff_less_eq [symmetric])
  1659   apply (drule less_le_mult)
  1660    apply arith
  1661   apply simp
  1662   done
  1663 
  1664 (* links with rbl operations *)
  1665 lemma word_succ_rbl:
  1666   "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
  1667   apply (unfold word_succ_def)
  1668   apply clarify
  1669   apply (simp add: to_bl_of_bin)
  1670   apply (simp add: to_bl_def rbl_succ)
  1671   done
  1672 
  1673 lemma word_pred_rbl:
  1674   "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
  1675   apply (unfold word_pred_def)
  1676   apply clarify
  1677   apply (simp add: to_bl_of_bin)
  1678   apply (simp add: to_bl_def rbl_pred)
  1679   done
  1680 
  1681 lemma word_add_rbl:
  1682   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
  1683     to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
  1684   apply (unfold word_add_def)
  1685   apply clarify
  1686   apply (simp add: to_bl_of_bin)
  1687   apply (simp add: to_bl_def rbl_add)
  1688   done
  1689 
  1690 lemma word_mult_rbl:
  1691   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
  1692     to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
  1693   apply (unfold word_mult_def)
  1694   apply clarify
  1695   apply (simp add: to_bl_of_bin)
  1696   apply (simp add: to_bl_def rbl_mult)
  1697   done
  1698 
  1699 lemma rtb_rbl_ariths:
  1700   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
  1701   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
  1702   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
  1703   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
  1704   by (auto simp: rev_swap [symmetric] word_succ_rbl 
  1705                  word_pred_rbl word_mult_rbl word_add_rbl)
  1706 
  1707 
  1708 subsection "Arithmetic type class instantiations"
  1709 
  1710 lemmas word_le_0_iff [simp] =
  1711   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
  1712 
  1713 lemma word_of_int_nat: 
  1714   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
  1715   by (simp add: of_nat_nat word_of_int)
  1716 
  1717 (* note that iszero_def is only for class comm_semiring_1_cancel,
  1718    which requires word length >= 1, ie 'a :: len word *) 
  1719 lemma iszero_word_no [simp]:
  1720   "iszero (numeral bin :: 'a :: len word) = 
  1721     iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
  1722   using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
  1723   by (simp add: iszero_def [symmetric])
  1724     
  1725 text {* Use @{text iszero} to simplify equalities between word numerals. *}
  1726 
  1727 lemmas word_eq_numeral_iff_iszero [simp] =
  1728   eq_numeral_iff_iszero [where 'a="'a::len word"]
  1729 
  1730 
  1731 subsection "Word and nat"
  1732 
  1733 lemma td_ext_unat [OF refl]:
  1734   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  1735     td_ext (unat :: 'a word => nat) of_nat 
  1736     (unats n) (%i. i mod 2 ^ n)"
  1737   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
  1738   apply (auto intro!: imageI simp add : word_of_int_hom_syms)
  1739   apply (erule word_uint.Abs_inverse [THEN arg_cong])
  1740   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
  1741   done
  1742 
  1743 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
  1744 
  1745 interpretation word_unat:
  1746   td_ext "unat::'a::len word => nat" 
  1747          of_nat 
  1748          "unats (len_of TYPE('a::len))"
  1749          "%i. i mod 2 ^ len_of TYPE('a::len)"
  1750   by (rule td_ext_unat)
  1751 
  1752 lemmas td_unat = word_unat.td_thm
  1753 
  1754 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
  1755 
  1756 lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
  1757   apply (unfold unats_def)
  1758   apply clarsimp
  1759   apply (rule xtrans, rule unat_lt2p, assumption) 
  1760   done
  1761 
  1762 lemma word_nchotomy:
  1763   "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
  1764   apply (rule allI)
  1765   apply (rule word_unat.Abs_cases)
  1766   apply (unfold unats_def)
  1767   apply auto
  1768   done
  1769 
  1770 lemma of_nat_eq:
  1771   fixes w :: "'a::len word"
  1772   shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
  1773   apply (rule trans)
  1774    apply (rule word_unat.inverse_norm)
  1775   apply (rule iffI)
  1776    apply (rule mod_eqD)
  1777    apply simp
  1778   apply clarsimp
  1779   done
  1780 
  1781 lemma of_nat_eq_size: 
  1782   "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
  1783   unfolding word_size by (rule of_nat_eq)
  1784 
  1785 lemma of_nat_0:
  1786   "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
  1787   by (simp add: of_nat_eq)
  1788 
  1789 lemma of_nat_2p [simp]:
  1790   "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
  1791   by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
  1792 
  1793 lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
  1794   by (cases k) auto
  1795 
  1796 lemma of_nat_neq_0: 
  1797   "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
  1798   by (clarsimp simp add : of_nat_0)
  1799 
  1800 lemma Abs_fnat_hom_add:
  1801   "of_nat a + of_nat b = of_nat (a + b)"
  1802   by simp
  1803 
  1804 lemma Abs_fnat_hom_mult:
  1805   "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
  1806   by (simp add: word_of_nat wi_hom_mult zmult_int)
  1807 
  1808 lemma Abs_fnat_hom_Suc:
  1809   "word_succ (of_nat a) = of_nat (Suc a)"
  1810   by (simp add: word_of_nat wi_hom_succ add_ac)
  1811 
  1812 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
  1813   by simp
  1814 
  1815 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
  1816   by simp
  1817 
  1818 lemmas Abs_fnat_homs = 
  1819   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 
  1820   Abs_fnat_hom_0 Abs_fnat_hom_1
  1821 
  1822 lemma word_arith_nat_add:
  1823   "a + b = of_nat (unat a + unat b)" 
  1824   by simp
  1825 
  1826 lemma word_arith_nat_mult:
  1827   "a * b = of_nat (unat a * unat b)"
  1828   by (simp add: of_nat_mult)
  1829     
  1830 lemma word_arith_nat_Suc:
  1831   "word_succ a = of_nat (Suc (unat a))"
  1832   by (subst Abs_fnat_hom_Suc [symmetric]) simp
  1833 
  1834 lemma word_arith_nat_div:
  1835   "a div b = of_nat (unat a div unat b)"
  1836   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
  1837 
  1838 lemma word_arith_nat_mod:
  1839   "a mod b = of_nat (unat a mod unat b)"
  1840   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
  1841 
  1842 lemmas word_arith_nat_defs =
  1843   word_arith_nat_add word_arith_nat_mult
  1844   word_arith_nat_Suc Abs_fnat_hom_0
  1845   Abs_fnat_hom_1 word_arith_nat_div
  1846   word_arith_nat_mod 
  1847 
  1848 lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
  1849   by simp
  1850   
  1851 lemmas unat_word_ariths = word_arith_nat_defs
  1852   [THEN trans [OF unat_cong unat_of_nat]]
  1853 
  1854 lemmas word_sub_less_iff = word_sub_le_iff
  1855   [unfolded linorder_not_less [symmetric] Not_eq_iff]
  1856 
  1857 lemma unat_add_lem: 
  1858   "(unat x + unat y < 2 ^ len_of TYPE('a)) = 
  1859     (unat (x + y :: 'a :: len word) = unat x + unat y)"
  1860   unfolding unat_word_ariths
  1861   by (auto intro!: trans [OF _ nat_mod_lem])
  1862 
  1863 lemma unat_mult_lem: 
  1864   "(unat x * unat y < 2 ^ len_of TYPE('a)) = 
  1865     (unat (x * y :: 'a :: len word) = unat x * unat y)"
  1866   unfolding unat_word_ariths
  1867   by (auto intro!: trans [OF _ nat_mod_lem])
  1868 
  1869 lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
  1870 
  1871 lemma le_no_overflow: 
  1872   "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
  1873   apply (erule order_trans)
  1874   apply (erule olen_add_eqv [THEN iffD1])
  1875   done
  1876 
  1877 lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
  1878 
  1879 lemma unat_sub_if_size:
  1880   "unat (x - y) = (if unat y <= unat x 
  1881    then unat x - unat y 
  1882    else unat x + 2 ^ size x - unat y)"
  1883   apply (unfold word_size)
  1884   apply (simp add: un_ui_le)
  1885   apply (auto simp add: unat_def uint_sub_if')
  1886    apply (rule nat_diff_distrib)
  1887     prefer 3
  1888     apply (simp add: algebra_simps)
  1889     apply (rule nat_diff_distrib [THEN trans])
  1890       prefer 3
  1891       apply (subst nat_add_distrib)
  1892         prefer 3
  1893         apply (simp add: nat_power_eq)
  1894        apply auto
  1895   apply uint_arith
  1896   done
  1897 
  1898 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
  1899 
  1900 lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
  1901   apply (simp add : unat_word_ariths)
  1902   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1903   apply (rule div_le_dividend)
  1904   done
  1905 
  1906 lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
  1907   apply (clarsimp simp add : unat_word_ariths)
  1908   apply (cases "unat y")
  1909    prefer 2
  1910    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1911    apply (rule mod_le_divisor)
  1912    apply auto
  1913   done
  1914 
  1915 lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
  1916   unfolding uint_nat by (simp add : unat_div zdiv_int)
  1917 
  1918 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
  1919   unfolding uint_nat by (simp add : unat_mod zmod_int)
  1920 
  1921 
  1922 subsection {* Definition of unat\_arith tactic *}
  1923 
  1924 lemma unat_split:
  1925   fixes x::"'a::len word"
  1926   shows "P (unat x) = 
  1927          (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
  1928   by (auto simp: unat_of_nat)
  1929 
  1930 lemma unat_split_asm:
  1931   fixes x::"'a::len word"
  1932   shows "P (unat x) = 
  1933          (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
  1934   by (auto simp: unat_of_nat)
  1935 
  1936 lemmas of_nat_inverse = 
  1937   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
  1938 
  1939 lemmas unat_splits = unat_split unat_split_asm
  1940 
  1941 lemmas unat_arith_simps =
  1942   word_le_nat_alt word_less_nat_alt
  1943   word_unat.Rep_inject [symmetric]
  1944   unat_sub_if' unat_plus_if' unat_div unat_mod
  1945 
  1946 (* unat_arith_tac: tactic to reduce word arithmetic to nat, 
  1947    try to solve via arith *)
  1948 ML {*
  1949 fun unat_arith_ss_of ss = 
  1950   ss addsimps @{thms unat_arith_simps}
  1951      delsimps @{thms word_unat.Rep_inject}
  1952      |> fold Splitter.add_split @{thms split_if_asm}
  1953      |> fold Simplifier.add_cong @{thms power_False_cong}
  1954 
  1955 fun unat_arith_tacs ctxt =   
  1956   let
  1957     fun arith_tac' n t =
  1958       Arith_Data.verbose_arith_tac ctxt n t
  1959         handle Cooper.COOPER _ => Seq.empty;
  1960   in 
  1961     [ clarify_tac ctxt 1,
  1962       full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
  1963       ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits}
  1964                                       |> fold Simplifier.add_cong @{thms power_False_cong})),
  1965       rewrite_goals_tac @{thms word_size}, 
  1966       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
  1967                          REPEAT (etac conjE n) THEN
  1968                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
  1969       TRYALL arith_tac' ] 
  1970   end
  1971 
  1972 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
  1973 *}
  1974 
  1975 method_setup unat_arith = 
  1976   {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
  1977   "solving word arithmetic via natural numbers and arith"
  1978 
  1979 lemma no_plus_overflow_unat_size: 
  1980   "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
  1981   unfolding word_size by unat_arith
  1982 
  1983 lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
  1984 
  1985 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]
  1986 
  1987 lemma word_div_mult: 
  1988   "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> 
  1989     x * y div y = x"
  1990   apply unat_arith
  1991   apply clarsimp
  1992   apply (subst unat_mult_lem [THEN iffD1])
  1993   apply auto
  1994   done
  1995 
  1996 lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow> 
  1997     unat i * unat x < 2 ^ len_of TYPE('a)"
  1998   apply unat_arith
  1999   apply clarsimp
  2000   apply (drule mult_le_mono1)
  2001   apply (erule order_le_less_trans)
  2002   apply (rule xtr7 [OF unat_lt2p div_mult_le])
  2003   done
  2004 
  2005 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
  2006 
  2007 lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
  2008   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
  2009   apply (simp add: unat_arith_simps)
  2010   apply (drule (1) mult_less_mono1)
  2011   apply (erule order_less_le_trans)
  2012   apply (rule div_mult_le)
  2013   done
  2014 
  2015 lemma div_le_mult: 
  2016   "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
  2017   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
  2018   apply (simp add: unat_arith_simps)
  2019   apply (drule mult_le_mono1)
  2020   apply (erule order_trans)
  2021   apply (rule div_mult_le)
  2022   done
  2023 
  2024 lemma div_lt_uint': 
  2025   "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
  2026   apply (unfold uint_nat)
  2027   apply (drule div_lt')
  2028   apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
  2029                    nat_power_eq)
  2030   done
  2031 
  2032 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
  2033 
  2034 lemma word_le_exists': 
  2035   "(x :: 'a :: len0 word) <= y \<Longrightarrow> 
  2036     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
  2037   apply (rule exI)
  2038   apply (rule conjI)
  2039   apply (rule zadd_diff_inverse)
  2040   apply uint_arith
  2041   done
  2042 
  2043 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
  2044 
  2045 lemmas plus_minus_no_overflow =
  2046   order_less_imp_le [THEN plus_minus_no_overflow_ab]
  2047   
  2048 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
  2049   word_le_minus_cancel word_le_minus_mono_left
  2050 
  2051 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x
  2052 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
  2053 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
  2054 
  2055 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
  2056 
  2057 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
  2058 
  2059 lemma thd1:
  2060   "a div b * b \<le> (a::nat)"
  2061   using gt_or_eq_0 [of b]
  2062   apply (rule disjE)
  2063    apply (erule xtr4 [OF thd mult_commute])
  2064   apply clarsimp
  2065   done
  2066 
  2067 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1 
  2068 
  2069 lemma word_mod_div_equality:
  2070   "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
  2071   apply (unfold word_less_nat_alt word_arith_nat_defs)
  2072   apply (cut_tac y="unat b" in gt_or_eq_0)
  2073   apply (erule disjE)
  2074    apply (simp add: mod_div_equality uno_simps)
  2075   apply simp
  2076   done
  2077 
  2078 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
  2079   apply (unfold word_le_nat_alt word_arith_nat_defs)
  2080   apply (cut_tac y="unat b" in gt_or_eq_0)
  2081   apply (erule disjE)
  2082    apply (simp add: div_mult_le uno_simps)
  2083   apply simp
  2084   done
  2085 
  2086 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
  2087   apply (simp only: word_less_nat_alt word_arith_nat_defs)
  2088   apply (clarsimp simp add : uno_simps)
  2089   done
  2090 
  2091 lemma word_of_int_power_hom: 
  2092   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
  2093   by (induct n) (simp_all add: wi_hom_mult [symmetric])
  2094 
  2095 lemma word_arith_power_alt: 
  2096   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
  2097   by (simp add : word_of_int_power_hom [symmetric])
  2098 
  2099 lemma of_bl_length_less: 
  2100   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
  2101   apply (unfold of_bl_def word_less_alt word_numeral_alt)
  2102   apply safe
  2103   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
  2104                        del: word_of_int_numeral)
  2105   apply (simp add: mod_pos_pos_trivial)
  2106   apply (subst mod_pos_pos_trivial)
  2107     apply (rule bl_to_bin_ge0)
  2108    apply (rule order_less_trans)
  2109     apply (rule bl_to_bin_lt2p)
  2110    apply simp
  2111   apply (rule bl_to_bin_lt2p)
  2112   done
  2113 
  2114 
  2115 subsection "Cardinality, finiteness of set of words"
  2116 
  2117 instance word :: (len0) finite
  2118   by (default, simp add: type_definition.univ [OF type_definition_word])
  2119 
  2120 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
  2121   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
  2122 
  2123 lemma card_word_size: 
  2124   "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
  2125 unfolding word_size by (rule card_word)
  2126 
  2127 
  2128 subsection {* Bitwise Operations on Words *}
  2129 
  2130 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
  2131   
  2132 (* following definitions require both arithmetic and bit-wise word operations *)
  2133 
  2134 (* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
  2135 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
  2136   folded word_ubin.eq_norm, THEN eq_reflection]
  2137 
  2138 (* the binary operations only *)
  2139 (* BH: why is this needed? *)
  2140 lemmas word_log_binary_defs = 
  2141   word_and_def word_or_def word_xor_def
  2142 
  2143 lemma word_wi_log_defs:
  2144   "NOT word_of_int a = word_of_int (NOT a)"
  2145   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
  2146   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
  2147   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
  2148   by (transfer, rule refl)+
  2149 
  2150 lemma word_no_log_defs [simp]:
  2151   "NOT (numeral a) = word_of_int (NOT (numeral a))"
  2152   "NOT (neg_numeral a) = word_of_int (NOT (neg_numeral a))"
  2153   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
  2154   "numeral a AND neg_numeral b = word_of_int (numeral a AND neg_numeral b)"
  2155   "neg_numeral a AND numeral b = word_of_int (neg_numeral a AND numeral b)"
  2156   "neg_numeral a AND neg_numeral b = word_of_int (neg_numeral a AND neg_numeral b)"
  2157   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
  2158   "numeral a OR neg_numeral b = word_of_int (numeral a OR neg_numeral b)"
  2159   "neg_numeral a OR numeral b = word_of_int (neg_numeral a OR numeral b)"
  2160   "neg_numeral a OR neg_numeral b = word_of_int (neg_numeral a OR neg_numeral b)"
  2161   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
  2162   "numeral a XOR neg_numeral b = word_of_int (numeral a XOR neg_numeral b)"
  2163   "neg_numeral a XOR numeral b = word_of_int (neg_numeral a XOR numeral b)"
  2164   "neg_numeral a XOR neg_numeral b = word_of_int (neg_numeral a XOR neg_numeral b)"
  2165   by (transfer, rule refl)+
  2166 
  2167 text {* Special cases for when one of the arguments equals 1. *}
  2168 
  2169 lemma word_bitwise_1_simps [simp]:
  2170   "NOT (1::'a::len0 word) = -2"
  2171   "1 AND numeral b = word_of_int (1 AND numeral b)"
  2172   "1 AND neg_numeral b = word_of_int (1 AND neg_numeral b)"
  2173   "numeral a AND 1 = word_of_int (numeral a AND 1)"
  2174   "neg_numeral a AND 1 = word_of_int (neg_numeral a AND 1)"
  2175   "1 OR numeral b = word_of_int (1 OR numeral b)"
  2176   "1 OR neg_numeral b = word_of_int (1 OR neg_numeral b)"
  2177   "numeral a OR 1 = word_of_int (numeral a OR 1)"
  2178   "neg_numeral a OR 1 = word_of_int (neg_numeral a OR 1)"
  2179   "1 XOR numeral b = word_of_int (1 XOR numeral b)"
  2180   "1 XOR neg_numeral b = word_of_int (1 XOR neg_numeral b)"
  2181   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
  2182   "neg_numeral a XOR 1 = word_of_int (neg_numeral a XOR 1)"
  2183   by (transfer, simp)+
  2184 
  2185 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
  2186   by (transfer, simp add: bin_trunc_ao)
  2187 
  2188 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
  2189   by (transfer, simp add: bin_trunc_ao)
  2190 
  2191 lemma test_bit_wi [simp]:
  2192   "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
  2193   unfolding word_test_bit_def
  2194   by (simp add: word_ubin.eq_norm nth_bintr)
  2195 
  2196 lemma word_test_bit_transfer [transfer_rule]:
  2197   "(fun_rel cr_word (fun_rel op = op =))
  2198     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
  2199   unfolding fun_rel_def cr_word_def by simp
  2200 
  2201 lemma word_ops_nth_size:
  2202   "n < size (x::'a::len0 word) \<Longrightarrow> 
  2203     (x OR y) !! n = (x !! n | y !! n) & 
  2204     (x AND y) !! n = (x !! n & y !! n) & 
  2205     (x XOR y) !! n = (x !! n ~= y !! n) & 
  2206     (NOT x) !! n = (~ x !! n)"
  2207   unfolding word_size by transfer (simp add: bin_nth_ops)
  2208 
  2209 lemma word_ao_nth:
  2210   fixes x :: "'a::len0 word"
  2211   shows "(x OR y) !! n = (x !! n | y !! n) & 
  2212          (x AND y) !! n = (x !! n & y !! n)"
  2213   by transfer (auto simp add: bin_nth_ops)
  2214 
  2215 lemma test_bit_numeral [simp]:
  2216   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2217     n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
  2218   by transfer (rule refl)
  2219 
  2220 lemma test_bit_neg_numeral [simp]:
  2221   "(neg_numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2222     n < len_of TYPE('a) \<and> bin_nth (neg_numeral w) n"
  2223   by transfer (rule refl)
  2224 
  2225 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
  2226   by transfer auto
  2227   
  2228 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
  2229   by transfer simp
  2230 
  2231 lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  2232   by transfer simp
  2233 
  2234 (* get from commutativity, associativity etc of int_and etc
  2235   to same for word_and etc *)
  2236 
  2237 lemmas bwsimps = 
  2238   wi_hom_add
  2239   word_wi_log_defs
  2240 
  2241 lemma word_bw_assocs:
  2242   fixes x :: "'a::len0 word"
  2243   shows
  2244   "(x AND y) AND z = x AND y AND z"
  2245   "(x OR y) OR z = x OR y OR z"
  2246   "(x XOR y) XOR z = x XOR y XOR z"
  2247   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2248   
  2249 lemma word_bw_comms:
  2250   fixes x :: "'a::len0 word"
  2251   shows
  2252   "x AND y = y AND x"
  2253   "x OR y = y OR x"
  2254   "x XOR y = y XOR x"
  2255   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2256   
  2257 lemma word_bw_lcs:
  2258   fixes x :: "'a::len0 word"
  2259   shows
  2260   "y AND x AND z = x AND y AND z"
  2261   "y OR x OR z = x OR y OR z"
  2262   "y XOR x XOR z = x XOR y XOR z"
  2263   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2264 
  2265 lemma word_log_esimps [simp]:
  2266   fixes x :: "'a::len0 word"
  2267   shows
  2268   "x AND 0 = 0"
  2269   "x AND -1 = x"
  2270   "x OR 0 = x"
  2271   "x OR -1 = -1"
  2272   "x XOR 0 = x"
  2273   "x XOR -1 = NOT x"
  2274   "0 AND x = 0"
  2275   "-1 AND x = x"
  2276   "0 OR x = x"
  2277   "-1 OR x = -1"
  2278   "0 XOR x = x"
  2279   "-1 XOR x = NOT x"
  2280   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2281 
  2282 lemma word_not_dist:
  2283   fixes x :: "'a::len0 word"
  2284   shows
  2285   "NOT (x OR y) = NOT x AND NOT y"
  2286   "NOT (x AND y) = NOT x OR NOT y"
  2287   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2288 
  2289 lemma word_bw_same:
  2290   fixes x :: "'a::len0 word"
  2291   shows
  2292   "x AND x = x"
  2293   "x OR x = x"
  2294   "x XOR x = 0"
  2295   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2296 
  2297 lemma word_ao_absorbs [simp]:
  2298   fixes x :: "'a::len0 word"
  2299   shows
  2300   "x AND (y OR x) = x"
  2301   "x OR y AND x = x"
  2302   "x AND (x OR y) = x"
  2303   "y AND x OR x = x"
  2304   "(y OR x) AND x = x"
  2305   "x OR x AND y = x"
  2306   "(x OR y) AND x = x"
  2307   "x AND y OR x = x"
  2308   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2309 
  2310 lemma word_not_not [simp]:
  2311   "NOT NOT (x::'a::len0 word) = x"
  2312   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2313 
  2314 lemma word_ao_dist:
  2315   fixes x :: "'a::len0 word"
  2316   shows "(x OR y) AND z = x AND z OR y AND z"
  2317   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2318 
  2319 lemma word_oa_dist:
  2320   fixes x :: "'a::len0 word"
  2321   shows "x AND y OR z = (x OR z) AND (y OR z)"
  2322   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2323 
  2324 lemma word_add_not [simp]: 
  2325   fixes x :: "'a::len0 word"
  2326   shows "x + NOT x = -1"
  2327   by transfer (simp add: bin_add_not)
  2328 
  2329 lemma word_plus_and_or [simp]:
  2330   fixes x :: "'a::len0 word"
  2331   shows "(x AND y) + (x OR y) = x + y"
  2332   by transfer (simp add: plus_and_or)
  2333 
  2334 lemma leoa:   
  2335   fixes x :: "'a::len0 word"
  2336   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  2337 lemma leao: 
  2338   fixes x' :: "'a::len0 word"
  2339   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
  2340 
  2341 lemma word_ao_equiv:
  2342   fixes w w' :: "'a::len0 word"
  2343   shows "(w = w OR w') = (w' = w AND w')"
  2344   by (auto intro: leoa leao)
  2345 
  2346 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  2347   unfolding word_le_def uint_or
  2348   by (auto intro: le_int_or) 
  2349 
  2350 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
  2351 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
  2352 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
  2353 
  2354 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 
  2355   unfolding to_bl_def word_log_defs bl_not_bin
  2356   by (simp add: word_ubin.eq_norm)
  2357 
  2358 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
  2359   unfolding to_bl_def word_log_defs bl_xor_bin
  2360   by (simp add: word_ubin.eq_norm)
  2361 
  2362 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
  2363   unfolding to_bl_def word_log_defs bl_or_bin
  2364   by (simp add: word_ubin.eq_norm)
  2365 
  2366 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
  2367   unfolding to_bl_def word_log_defs bl_and_bin
  2368   by (simp add: word_ubin.eq_norm)
  2369 
  2370 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
  2371   by (auto simp: word_test_bit_def word_lsb_def)
  2372 
  2373 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
  2374   unfolding word_lsb_def uint_eq_0 uint_1 by simp
  2375 
  2376 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
  2377   apply (unfold word_lsb_def uint_bl bin_to_bl_def) 
  2378   apply (rule_tac bin="uint w" in bin_exhaust)
  2379   apply (cases "size w")
  2380    apply auto
  2381    apply (auto simp add: bin_to_bl_aux_alt)
  2382   done
  2383 
  2384 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
  2385   unfolding word_lsb_def bin_last_def by auto
  2386 
  2387 lemma word_msb_sint: "msb w = (sint w < 0)" 
  2388   unfolding word_msb_def sign_Min_lt_0 ..
  2389 
  2390 lemma msb_word_of_int:
  2391   "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  2392   unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)
  2393 
  2394 lemma word_msb_numeral [simp]:
  2395   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  2396   unfolding word_numeral_alt by (rule msb_word_of_int)
  2397 
  2398 lemma word_msb_neg_numeral [simp]:
  2399   "msb (neg_numeral w::'a::len word) = bin_nth (neg_numeral w) (len_of TYPE('a) - 1)"
  2400   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  2401 
  2402 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  2403   unfolding word_msb_def by simp
  2404 
  2405 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  2406   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  2407   by (simp add: Suc_le_eq)
  2408 
  2409 lemma word_msb_nth:
  2410   "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
  2411   unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
  2412 
  2413 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
  2414   apply (unfold word_msb_nth uint_bl)
  2415   apply (subst hd_conv_nth)
  2416   apply (rule length_greater_0_conv [THEN iffD1])
  2417    apply simp
  2418   apply (simp add : nth_bin_to_bl word_size)
  2419   done
  2420 
  2421 lemma word_set_nth [simp]:
  2422   "set_bit w n (test_bit w n) = (w::'a::len0 word)"
  2423   unfolding word_test_bit_def word_set_bit_def by auto
  2424 
  2425 lemma bin_nth_uint':
  2426   "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
  2427   apply (unfold word_size)
  2428   apply (safe elim!: bin_nth_uint_imp)
  2429    apply (frule bin_nth_uint_imp)
  2430    apply (fast dest!: bin_nth_bl)+
  2431   done
  2432 
  2433 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  2434 
  2435 lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
  2436   unfolding to_bl_def word_test_bit_def word_size
  2437   by (rule bin_nth_uint)
  2438 
  2439 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  2440   apply (unfold test_bit_bl)
  2441   apply clarsimp
  2442   apply (rule trans)
  2443    apply (rule nth_rev_alt)
  2444    apply (auto simp add: word_size)
  2445   done
  2446 
  2447 lemma test_bit_set: 
  2448   fixes w :: "'a::len0 word"
  2449   shows "(set_bit w n x) !! n = (n < size w & x)"
  2450   unfolding word_size word_test_bit_def word_set_bit_def
  2451   by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
  2452 
  2453 lemma test_bit_set_gen: 
  2454   fixes w :: "'a::len0 word"
  2455   shows "test_bit (set_bit w n x) m = 
  2456          (if m = n then n < size w & x else test_bit w m)"
  2457   apply (unfold word_size word_test_bit_def word_set_bit_def)
  2458   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  2459   apply (auto elim!: test_bit_size [unfolded word_size]
  2460               simp add: word_test_bit_def [symmetric])
  2461   done
  2462 
  2463 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  2464   unfolding of_bl_def bl_to_bin_rep_F by auto
  2465   
  2466 lemma msb_nth:
  2467   fixes w :: "'a::len word"
  2468   shows "msb w = w !! (len_of TYPE('a) - 1)"
  2469   unfolding word_msb_nth word_test_bit_def by simp
  2470 
  2471 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  2472 lemmas msb1 = msb0 [where i = 0]
  2473 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
  2474 
  2475 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
  2476 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  2477 
  2478 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  2479   "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 
  2480     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
  2481   apply (unfold word_size td_ext_def')
  2482   apply safe
  2483      apply (rule_tac [3] ext)
  2484      apply (rule_tac [4] ext)
  2485      apply (unfold word_size of_nth_def test_bit_bl)
  2486      apply safe
  2487        defer
  2488        apply (clarsimp simp: word_bl.Abs_inverse)+
  2489   apply (rule word_bl.Rep_inverse')
  2490   apply (rule sym [THEN trans])
  2491   apply (rule bl_of_nth_nth)
  2492   apply simp
  2493   apply (rule bl_of_nth_inj)
  2494   apply (clarsimp simp add : test_bit_bl word_size)
  2495   done
  2496 
  2497 interpretation test_bit:
  2498   td_ext "op !! :: 'a::len0 word => nat => bool"
  2499          set_bits
  2500          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  2501          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  2502   by (rule td_ext_nth)
  2503 
  2504 lemmas td_nth = test_bit.td_thm
  2505 
  2506 lemma word_set_set_same [simp]:
  2507   fixes w :: "'a::len0 word"
  2508   shows "set_bit (set_bit w n x) n y = set_bit w n y" 
  2509   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  2510     
  2511 lemma word_set_set_diff: 
  2512   fixes w :: "'a::len0 word"
  2513   assumes "m ~= n"
  2514   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
  2515   by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
  2516 
  2517 lemma nth_sint: 
  2518   fixes w :: "'a::len word"
  2519   defines "l \<equiv> len_of TYPE ('a)"
  2520   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  2521   unfolding sint_uint l_def
  2522   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
  2523 
  2524 lemma word_lsb_numeral [simp]:
  2525   "lsb (numeral bin :: 'a :: len word) = (bin_last (numeral bin) = 1)"
  2526   unfolding word_lsb_alt test_bit_numeral by simp
  2527 
  2528 lemma word_lsb_neg_numeral [simp]:
  2529   "lsb (neg_numeral bin :: 'a :: len word) = (bin_last (neg_numeral bin) = 1)"
  2530   unfolding word_lsb_alt test_bit_neg_numeral by simp
  2531 
  2532 lemma set_bit_word_of_int:
  2533   "set_bit (word_of_int x) n b = word_of_int (bin_sc n (if b then 1 else 0) x)"
  2534   unfolding word_set_bit_def
  2535   apply (rule word_eqI)
  2536   apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  2537   done
  2538 
  2539 lemma word_set_numeral [simp]:
  2540   "set_bit (numeral bin::'a::len0 word) n b = 
  2541     word_of_int (bin_sc n (if b then 1 else 0) (numeral bin))"
  2542   unfolding word_numeral_alt by (rule set_bit_word_of_int)
  2543 
  2544 lemma word_set_neg_numeral [simp]:
  2545   "set_bit (neg_numeral bin::'a::len0 word) n b = 
  2546     word_of_int (bin_sc n (if b then 1 else 0) (neg_numeral bin))"
  2547   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  2548 
  2549 lemma word_set_bit_0 [simp]:
  2550   "set_bit 0 n b = word_of_int (bin_sc n (if b then 1 else 0) 0)"
  2551   unfolding word_0_wi by (rule set_bit_word_of_int)
  2552 
  2553 lemma word_set_bit_1 [simp]:
  2554   "set_bit 1 n b = word_of_int (bin_sc n (if b then 1 else 0) 1)"
  2555   unfolding word_1_wi by (rule set_bit_word_of_int)
  2556 
  2557 lemma setBit_no [simp]:
  2558   "setBit (numeral bin) n = word_of_int (bin_sc n 1 (numeral bin))"
  2559   by (simp add: setBit_def)
  2560 
  2561 lemma clearBit_no [simp]:
  2562   "clearBit (numeral bin) n = word_of_int (bin_sc n 0 (numeral bin))"
  2563   by (simp add: clearBit_def)
  2564 
  2565 lemma to_bl_n1: 
  2566   "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
  2567   apply (rule word_bl.Abs_inverse')
  2568    apply simp
  2569   apply (rule word_eqI)
  2570   apply (clarsimp simp add: word_size)
  2571   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
  2572   done
  2573 
  2574 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  2575   unfolding word_msb_alt to_bl_n1 by simp
  2576 
  2577 lemma word_set_nth_iff: 
  2578   "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
  2579   apply (rule iffI)
  2580    apply (rule disjCI)
  2581    apply (drule word_eqD)
  2582    apply (erule sym [THEN trans])
  2583    apply (simp add: test_bit_set)
  2584   apply (erule disjE)
  2585    apply clarsimp
  2586   apply (rule word_eqI)
  2587   apply (clarsimp simp add : test_bit_set_gen)
  2588   apply (drule test_bit_size)
  2589   apply force
  2590   done
  2591 
  2592 lemma test_bit_2p:
  2593   "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  2594   unfolding word_test_bit_def
  2595   by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
  2596 
  2597 lemma nth_w2p:
  2598   "((2\<Colon>'a\<Colon>len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a\<Colon>len)"
  2599   unfolding test_bit_2p [symmetric] word_of_int [symmetric]
  2600   by (simp add:  of_int_power)
  2601 
  2602 lemma uint_2p: 
  2603   "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  2604   apply (unfold word_arith_power_alt)
  2605   apply (case_tac "len_of TYPE ('a)")
  2606    apply clarsimp
  2607   apply (case_tac "nat")
  2608    apply clarsimp
  2609    apply (case_tac "n")
  2610     apply clarsimp
  2611    apply clarsimp
  2612   apply (drule word_gt_0 [THEN iffD1])
  2613   apply (safe intro!: word_eqI bin_nth_lem)
  2614      apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric])
  2615   done
  2616 
  2617 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
  2618   apply (unfold word_arith_power_alt)
  2619   apply (case_tac "len_of TYPE ('a)")
  2620    apply clarsimp
  2621   apply (case_tac "nat")
  2622    apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
  2623    apply (rule box_equals) 
  2624      apply (rule_tac [2] bintr_ariths (1))+ 
  2625    apply simp
  2626   apply simp
  2627   done
  2628 
  2629 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
  2630   apply (rule xtr3) 
  2631   apply (rule_tac [2] y = "x" in le_word_or2)
  2632   apply (rule word_eqI)
  2633   apply (auto simp add: word_ao_nth nth_w2p word_size)
  2634   done
  2635 
  2636 lemma word_clr_le: 
  2637   fixes w :: "'a::len0 word"
  2638   shows "w >= set_bit w n False"
  2639   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2640   apply simp
  2641   apply (rule order_trans)
  2642    apply (rule bintr_bin_clr_le)
  2643   apply simp
  2644   done
  2645 
  2646 lemma word_set_ge: 
  2647   fixes w :: "'a::len word"
  2648   shows "w <= set_bit w n True"
  2649   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2650   apply simp
  2651   apply (rule order_trans [OF _ bintr_bin_set_ge])
  2652   apply simp
  2653   done
  2654 
  2655 
  2656 subsection {* Shifting, Rotating, and Splitting Words *}
  2657 
  2658 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT 0)"
  2659   unfolding shiftl1_def
  2660   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
  2661   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
  2662   apply (subst bintrunc_bintrunc_min)
  2663   apply simp
  2664   done
  2665 
  2666 lemma shiftl1_numeral [simp]:
  2667   "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  2668   unfolding word_numeral_alt shiftl1_wi by simp
  2669 
  2670 lemma shiftl1_neg_numeral [simp]:
  2671   "shiftl1 (neg_numeral w) = neg_numeral (Num.Bit0 w)"
  2672   unfolding word_neg_numeral_alt shiftl1_wi by simp
  2673 
  2674 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  2675   unfolding shiftl1_def by simp
  2676 
  2677 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT 0)"
  2678   by (simp only: shiftl1_def) (* FIXME: duplicate *)
  2679 
  2680 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT 0)"
  2681   unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
  2682 
  2683 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  2684   unfolding shiftr1_def by simp
  2685 
  2686 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  2687   unfolding sshiftr1_def by simp
  2688 
  2689 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
  2690   unfolding sshiftr1_def by simp
  2691 
  2692 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
  2693   unfolding shiftl_def by (induct n) auto
  2694 
  2695 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
  2696   unfolding shiftr_def by (induct n) auto
  2697 
  2698 lemma sshiftr_0 [simp] : "0 >>> n = 0"
  2699   unfolding sshiftr_def by (induct n) auto
  2700 
  2701 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
  2702   unfolding sshiftr_def by (induct n) auto
  2703 
  2704 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
  2705   apply (unfold shiftl1_def word_test_bit_def)
  2706   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  2707   apply (cases n)
  2708    apply auto
  2709   done
  2710 
  2711 lemma nth_shiftl' [rule_format]:
  2712   "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
  2713   apply (unfold shiftl_def)
  2714   apply (induct "m")
  2715    apply (force elim!: test_bit_size)
  2716   apply (clarsimp simp add : nth_shiftl1 word_size)
  2717   apply arith
  2718   done
  2719 
  2720 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
  2721 
  2722 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  2723   apply (unfold shiftr1_def word_test_bit_def)
  2724   apply (simp add: nth_bintr word_ubin.eq_norm)
  2725   apply safe
  2726   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
  2727   apply simp
  2728   done
  2729 
  2730 lemma nth_shiftr: 
  2731   "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
  2732   apply (unfold shiftr_def)
  2733   apply (induct "m")
  2734    apply (auto simp add : nth_shiftr1)
  2735   done
  2736    
  2737 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  2738   where f (ie bin_rest) takes normal arguments to normal results,
  2739   thus we get (2) from (1) *)
  2740 
  2741 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
  2742   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  2743   apply (subst bintr_uint [symmetric, OF order_refl])
  2744   apply (simp only : bintrunc_bintrunc_l)
  2745   apply simp 
  2746   done
  2747 
  2748 lemma nth_sshiftr1: 
  2749   "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  2750   apply (unfold sshiftr1_def word_test_bit_def)
  2751   apply (simp add: nth_bintr word_ubin.eq_norm
  2752                    bin_nth.Suc [symmetric] word_size 
  2753              del: bin_nth.simps)
  2754   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  2755   apply (auto simp add: bin_nth_sint)
  2756   done
  2757 
  2758 lemma nth_sshiftr [rule_format] : 
  2759   "ALL n. sshiftr w m !! n = (n < size w & 
  2760     (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
  2761   apply (unfold sshiftr_def)
  2762   apply (induct_tac "m")
  2763    apply (simp add: test_bit_bl)
  2764   apply (clarsimp simp add: nth_sshiftr1 word_size)
  2765   apply safe
  2766        apply arith
  2767       apply arith
  2768      apply (erule thin_rl)
  2769      apply (case_tac n)
  2770       apply safe
  2771       apply simp
  2772      apply simp
  2773     apply (erule thin_rl)
  2774     apply (case_tac n)
  2775      apply safe
  2776      apply simp
  2777     apply simp
  2778    apply arith+
  2779   done
  2780     
  2781 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
  2782   apply (unfold shiftr1_def bin_rest_def)
  2783   apply (rule word_uint.Abs_inverse)
  2784   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
  2785   apply (rule xtr7)
  2786    prefer 2
  2787    apply (rule zdiv_le_dividend)
  2788     apply auto
  2789   done
  2790 
  2791 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
  2792   apply (unfold sshiftr1_def bin_rest_def [symmetric])
  2793   apply (simp add: word_sbin.eq_norm)
  2794   apply (rule trans)
  2795    defer
  2796    apply (subst word_sbin.norm_Rep [symmetric])
  2797    apply (rule refl)
  2798   apply (subst word_sbin.norm_Rep [symmetric])
  2799   apply (unfold One_nat_def)
  2800   apply (rule sbintrunc_rest)
  2801   done
  2802 
  2803 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  2804   apply (unfold shiftr_def)
  2805   apply (induct "n")
  2806    apply simp
  2807   apply (simp add: shiftr1_div_2 mult_commute
  2808                    zdiv_zmult2_eq [symmetric])
  2809   done
  2810 
  2811 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  2812   apply (unfold sshiftr_def)
  2813   apply (induct "n")
  2814    apply simp
  2815   apply (simp add: sshiftr1_div_2 mult_commute
  2816                    zdiv_zmult2_eq [symmetric])
  2817   done
  2818 
  2819 subsubsection "shift functions in terms of lists of bools"
  2820 
  2821 lemmas bshiftr1_numeral [simp] = 
  2822   bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
  2823 
  2824 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
  2825   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
  2826 
  2827 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
  2828   by (simp add: of_bl_def bl_to_bin_append)
  2829 
  2830 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
  2831 proof -
  2832   have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
  2833   also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
  2834   finally show ?thesis .
  2835 qed
  2836 
  2837 lemma bl_shiftl1:
  2838   "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
  2839   apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
  2840   apply (fast intro!: Suc_leI)
  2841   done
  2842 
  2843 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  2844 lemma bl_shiftl1':
  2845   "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  2846   unfolding shiftl1_bl
  2847   by (simp add: word_rep_drop drop_Suc del: drop_append)
  2848 
  2849 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  2850   apply (unfold shiftr1_def uint_bl of_bl_def)
  2851   apply (simp add: butlast_rest_bin word_size)
  2852   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  2853   done
  2854 
  2855 lemma bl_shiftr1: 
  2856   "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
  2857   unfolding shiftr1_bl
  2858   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
  2859 
  2860 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  2861 lemma bl_shiftr1':
  2862   "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  2863   apply (rule word_bl.Abs_inverse')
  2864   apply (simp del: butlast.simps)
  2865   apply (simp add: shiftr1_bl of_bl_def)
  2866   done
  2867 
  2868 lemma shiftl1_rev: 
  2869   "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  2870   apply (unfold word_reverse_def)
  2871   apply (rule word_bl.Rep_inverse' [symmetric])
  2872   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  2873   apply (cases "to_bl w")
  2874    apply auto
  2875   done
  2876 
  2877 lemma shiftl_rev: 
  2878   "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  2879   apply (unfold shiftl_def shiftr_def)
  2880   apply (induct "n")
  2881    apply (auto simp add : shiftl1_rev)
  2882   done
  2883 
  2884 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  2885   by (simp add: shiftl_rev)
  2886 
  2887 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  2888   by (simp add: rev_shiftl)
  2889 
  2890 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  2891   by (simp add: shiftr_rev)
  2892 
  2893 lemma bl_sshiftr1:
  2894   "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
  2895   apply (unfold sshiftr1_def uint_bl word_size)
  2896   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  2897   apply (simp add: sint_uint)
  2898   apply (rule nth_equalityI)
  2899    apply clarsimp
  2900   apply clarsimp
  2901   apply (case_tac i)
  2902    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  2903                         nth_bin_to_bl bin_nth.Suc [symmetric] 
  2904                         nth_sbintr 
  2905                    del: bin_nth.Suc)
  2906    apply force
  2907   apply (rule impI)
  2908   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  2909   apply simp
  2910   done
  2911 
  2912 lemma drop_shiftr: 
  2913   "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
  2914   apply (unfold shiftr_def)
  2915   apply (induct n)
  2916    prefer 2
  2917    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  2918    apply (rule butlast_take [THEN trans])
  2919   apply (auto simp: word_size)
  2920   done
  2921 
  2922 lemma drop_sshiftr: 
  2923   "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
  2924   apply (unfold sshiftr_def)
  2925   apply (induct n)
  2926    prefer 2
  2927    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  2928    apply (rule butlast_take [THEN trans])
  2929   apply (auto simp: word_size)
  2930   done
  2931 
  2932 lemma take_shiftr:
  2933   "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  2934   apply (unfold shiftr_def)
  2935   apply (induct n)
  2936    prefer 2
  2937    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  2938    apply (rule take_butlast [THEN trans])
  2939   apply (auto simp: word_size)
  2940   done
  2941 
  2942 lemma take_sshiftr' [rule_format] :
  2943   "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
  2944     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
  2945   apply (unfold sshiftr_def)
  2946   apply (induct n)
  2947    prefer 2
  2948    apply (simp add: bl_sshiftr1)
  2949    apply (rule impI)
  2950    apply (rule take_butlast [THEN trans])
  2951   apply (auto simp: word_size)
  2952   done
  2953 
  2954 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  2955 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
  2956 
  2957 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
  2958   by (auto intro: append_take_drop_id [symmetric])
  2959 
  2960 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
  2961 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  2962 
  2963 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  2964   unfolding shiftl_def
  2965   by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
  2966 
  2967 lemma shiftl_bl:
  2968   "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
  2969 proof -
  2970   have "w << n = of_bl (to_bl w) << n" by simp
  2971   also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
  2972   finally show ?thesis .
  2973 qed
  2974 
  2975 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  2976 
  2977 lemma bl_shiftl:
  2978   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  2979   by (simp add: shiftl_bl word_rep_drop word_size)
  2980 
  2981 lemma shiftl_zero_size: 
  2982   fixes x :: "'a::len0 word"
  2983   shows "size x <= n \<Longrightarrow> x << n = 0"
  2984   apply (unfold word_size)
  2985   apply (rule word_eqI)
  2986   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  2987   done
  2988 
  2989 (* note - the following results use 'a :: len word < number_ring *)
  2990 
  2991 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
  2992   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  2993 
  2994 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
  2995   by (simp add: shiftl1_2t)
  2996 
  2997 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
  2998   unfolding shiftl_def 
  2999   by (induct n) (auto simp: shiftl1_2t)
  3000 
  3001 lemma shiftr1_bintr [simp]:
  3002   "(shiftr1 (numeral w) :: 'a :: len0 word) =
  3003     word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (numeral w)))"
  3004   unfolding shiftr1_def word_numeral_alt
  3005   by (simp add: word_ubin.eq_norm)
  3006 
  3007 lemma sshiftr1_sbintr [simp]:
  3008   "(sshiftr1 (numeral w) :: 'a :: len word) =
  3009     word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (numeral w)))"
  3010   unfolding sshiftr1_def word_numeral_alt
  3011   by (simp add: word_sbin.eq_norm)
  3012 
  3013 lemma shiftr_no [simp]:
  3014   (* FIXME: neg_numeral *)
  3015   "(numeral w::'a::len0 word) >> n = word_of_int
  3016     ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  3017   apply (rule word_eqI)
  3018   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  3019   done
  3020 
  3021 lemma sshiftr_no [simp]:
  3022   (* FIXME: neg_numeral *)
  3023   "(numeral w::'a::len word) >>> n = word_of_int
  3024     ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  3025   apply (rule word_eqI)
  3026   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
  3027    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
  3028   done
  3029 
  3030 lemma shiftr1_bl_of:
  3031   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3032     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  3033   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin 
  3034                      word_ubin.eq_norm trunc_bl2bin)
  3035 
  3036 lemma shiftr_bl_of:
  3037   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3038     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
  3039   apply (unfold shiftr_def)
  3040   apply (induct n)
  3041    apply clarsimp
  3042   apply clarsimp
  3043   apply (subst shiftr1_bl_of)
  3044    apply simp
  3045   apply (simp add: butlast_take)
  3046   done
  3047 
  3048 lemma shiftr_bl:
  3049   "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  3050   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  3051 
  3052 lemma msb_shift:
  3053   "msb (w::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
  3054   apply (unfold shiftr_bl word_msb_alt)
  3055   apply (simp add: word_size Suc_le_eq take_Suc)
  3056   apply (cases "hd (to_bl w)")
  3057    apply (auto simp: word_1_bl
  3058                      of_bl_rep_False [where n=1 and bs="[]", simplified])
  3059   done
  3060 
  3061 lemma align_lem_or [rule_format] :
  3062   "ALL x m. length x = n + m --> length y = n + m --> 
  3063     drop m x = replicate n False --> take m y = replicate m False --> 
  3064     map2 op | x y = take m x @ drop m y"
  3065   apply (induct_tac y)
  3066    apply force
  3067   apply clarsimp
  3068   apply (case_tac x, force)
  3069   apply (case_tac m, auto)
  3070   apply (drule sym)
  3071   apply auto
  3072   apply (induct_tac list, auto)
  3073   done
  3074 
  3075 lemma align_lem_and [rule_format] :
  3076   "ALL x m. length x = n + m --> length y = n + m --> 
  3077     drop m x = replicate n False --> take m y = replicate m False --> 
  3078     map2 op & x y = replicate (n + m) False"
  3079   apply (induct_tac y)
  3080    apply force
  3081   apply clarsimp
  3082   apply (case_tac x, force)
  3083   apply (case_tac m, auto)
  3084   apply (drule sym)
  3085   apply auto
  3086   apply (induct_tac list, auto)
  3087   done
  3088 
  3089 lemma aligned_bl_add_size [OF refl]:
  3090   "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  3091     take m (to_bl y) = replicate m False \<Longrightarrow> 
  3092     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  3093   apply (subgoal_tac "x AND y = 0")
  3094    prefer 2
  3095    apply (rule word_bl.Rep_eqD)
  3096    apply (simp add: bl_word_and)
  3097    apply (rule align_lem_and [THEN trans])
  3098        apply (simp_all add: word_size)[5]
  3099    apply simp
  3100   apply (subst word_plus_and_or [symmetric])
  3101   apply (simp add : bl_word_or)
  3102   apply (rule align_lem_or)
  3103      apply (simp_all add: word_size)
  3104   done
  3105 
  3106 subsubsection "Mask"
  3107 
  3108 lemma nth_mask [OF refl, simp]:
  3109   "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
  3110   apply (unfold mask_def test_bit_bl)
  3111   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  3112   apply (clarsimp simp add: word_size)
  3113   apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
  3114   apply (fold of_bl_def)
  3115   apply (simp add: word_1_bl)
  3116   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
  3117   apply auto
  3118   done
  3119 
  3120 lemma mask_bl: "mask n = of_bl (replicate n True)"
  3121   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
  3122 
  3123 lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
  3124   by (auto simp add: nth_bintr word_size intro: word_eqI)
  3125 
  3126 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
  3127   apply (rule word_eqI)
  3128   apply (simp add: nth_bintr word_size word_ops_nth_size)
  3129   apply (auto simp add: test_bit_bin)
  3130   done
  3131 
  3132 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  3133   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3134 
  3135 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  3136   unfolding word_numeral_alt by (rule and_mask_wi)
  3137 
  3138 lemma bl_and_mask':
  3139   "to_bl (w AND mask n :: 'a :: len word) = 
  3140     replicate (len_of TYPE('a) - n) False @ 
  3141     drop (len_of TYPE('a) - n) (to_bl w)"
  3142   apply (rule nth_equalityI)
  3143    apply simp
  3144   apply (clarsimp simp add: to_bl_nth word_size)
  3145   apply (simp add: word_size word_ops_nth_size)
  3146   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
  3147   done
  3148 
  3149 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
  3150   by (simp only: and_mask_bintr bintrunc_mod2p)
  3151 
  3152 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
  3153   apply (simp add: and_mask_bintr word_ubin.eq_norm)
  3154   apply (simp add: bintrunc_mod2p)
  3155   apply (rule xtr8)
  3156    prefer 2
  3157    apply (rule pos_mod_bound)
  3158   apply auto
  3159   done
  3160 
  3161 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  3162   by (simp add: int_mod_lem eq_sym_conv)
  3163 
  3164 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
  3165   apply (simp add: and_mask_bintr)
  3166   apply (simp add: word_ubin.inverse_norm)
  3167   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
  3168   apply (fast intro!: lt2p_lem)
  3169   done
  3170 
  3171 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
  3172   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  3173   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
  3174     del: word_of_int_0)
  3175   apply (subst word_uint.norm_Rep [symmetric])
  3176   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  3177   apply auto
  3178   done
  3179 
  3180 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
  3181   apply (unfold unat_def)
  3182   apply (rule trans [OF _ and_mask_dvd])
  3183   apply (unfold dvd_def) 
  3184   apply auto 
  3185   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  3186   apply (simp add : int_mult int_power)
  3187   apply (simp add : nat_mult_distrib nat_power_eq)
  3188   done
  3189 
  3190 lemma word_2p_lem: 
  3191   "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
  3192   apply (unfold word_size word_less_alt word_numeral_alt)
  3193   apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
  3194                             int_mod_eq'
  3195                   simp del: word_of_int_numeral)
  3196   done
  3197 
  3198 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
  3199   apply (unfold word_less_alt word_numeral_alt)
  3200   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
  3201                             word_uint.eq_norm
  3202                   simp del: word_of_int_numeral)
  3203   apply (drule xtr8 [rotated])
  3204   apply (rule int_mod_le)
  3205   apply (auto simp add : mod_pos_pos_trivial)
  3206   done
  3207 
  3208 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  3209 
  3210 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
  3211 
  3212 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  3213   unfolding word_size by (erule and_mask_less')
  3214 
  3215 lemma word_mod_2p_is_mask [OF refl]:
  3216   "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n" 
  3217   by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
  3218 
  3219 lemma mask_eqs:
  3220   "(a AND mask n) + b AND mask n = a + b AND mask n"
  3221   "a + (b AND mask n) AND mask n = a + b AND mask n"
  3222   "(a AND mask n) - b AND mask n = a - b AND mask n"
  3223   "a - (b AND mask n) AND mask n = a - b AND mask n"
  3224   "a * (b AND mask n) AND mask n = a * b AND mask n"
  3225   "(b AND mask n) * a AND mask n = b * a AND mask n"
  3226   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
  3227   "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
  3228   "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
  3229   "- (a AND mask n) AND mask n = - a AND mask n"
  3230   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  3231   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  3232   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  3233   by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
  3234 
  3235 lemma mask_power_eq:
  3236   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  3237   using word_of_int_Ex [where x=x]
  3238   by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
  3239 
  3240 
  3241 subsubsection "Revcast"
  3242 
  3243 lemmas revcast_def' = revcast_def [simplified]
  3244 lemmas revcast_def'' = revcast_def' [simplified word_size]
  3245 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  3246 
  3247 lemma to_bl_revcast: 
  3248   "to_bl (revcast w :: 'a :: len0 word) = 
  3249    takefill False (len_of TYPE ('a)) (to_bl w)"
  3250   apply (unfold revcast_def' word_size)
  3251   apply (rule word_bl.Abs_inverse)
  3252   apply simp
  3253   done
  3254 
  3255 lemma revcast_rev_ucast [OF refl refl refl]: 
  3256   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 
  3257     rc = word_reverse uc"
  3258   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  3259   apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
  3260   apply (simp add : word_bl.Abs_inverse word_size)
  3261   done
  3262 
  3263 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  3264   using revcast_rev_ucast [of "word_reverse w"] by simp
  3265 
  3266 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
  3267   by (fact revcast_rev_ucast [THEN word_rev_gal'])
  3268 
  3269 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
  3270   by (fact revcast_ucast [THEN word_rev_gal'])
  3271 
  3272 
  3273 -- "linking revcast and cast via shift"
  3274 
  3275 lemmas wsst_TYs = source_size target_size word_size
  3276 
  3277 lemma revcast_down_uu [OF refl]:
  3278   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3279     rc (w :: 'a :: len word) = ucast (w >> n)"
  3280   apply (simp add: revcast_def')
  3281   apply (rule word_bl.Rep_inverse')
  3282   apply (rule trans, rule ucast_down_drop)
  3283    prefer 2
  3284    apply (rule trans, rule drop_shiftr)
  3285    apply (auto simp: takefill_alt wsst_TYs)
  3286   done
  3287 
  3288 lemma revcast_down_us [OF refl]:
  3289   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3290     rc (w :: 'a :: len word) = ucast (w >>> n)"
  3291   apply (simp add: revcast_def')
  3292   apply (rule word_bl.Rep_inverse')
  3293   apply (rule trans, rule ucast_down_drop)
  3294    prefer 2
  3295    apply (rule trans, rule drop_sshiftr)
  3296    apply (auto simp: takefill_alt wsst_TYs)
  3297   done
  3298 
  3299 lemma revcast_down_su [OF refl]:
  3300   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3301     rc (w :: 'a :: len word) = scast (w >> n)"
  3302   apply (simp add: revcast_def')
  3303   apply (rule word_bl.Rep_inverse')
  3304   apply (rule trans, rule scast_down_drop)
  3305    prefer 2
  3306    apply (rule trans, rule drop_shiftr)
  3307    apply (auto simp: takefill_alt wsst_TYs)
  3308   done
  3309 
  3310 lemma revcast_down_ss [OF refl]:
  3311   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3312     rc (w :: 'a :: len word) = scast (w >>> n)"
  3313   apply (simp add: revcast_def')
  3314   apply (rule word_bl.Rep_inverse')
  3315   apply (rule trans, rule scast_down_drop)
  3316    prefer 2
  3317    apply (rule trans, rule drop_sshiftr)
  3318    apply (auto simp: takefill_alt wsst_TYs)
  3319   done
  3320 
  3321 (* FIXME: should this also be [OF refl] ? *)
  3322 lemma cast_down_rev: 
  3323   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
  3324     uc w = revcast ((w :: 'a :: len word) << n)"
  3325   apply (unfold shiftl_rev)
  3326   apply clarify
  3327   apply (simp add: revcast_rev_ucast)
  3328   apply (rule word_rev_gal')
  3329   apply (rule trans [OF _ revcast_rev_ucast])
  3330   apply (rule revcast_down_uu [symmetric])
  3331   apply (auto simp add: wsst_TYs)
  3332   done
  3333 
  3334 lemma revcast_up [OF refl]:
  3335   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 
  3336     rc w = (ucast w :: 'a :: len word) << n" 
  3337   apply (simp add: revcast_def')
  3338   apply (rule word_bl.Rep_inverse')
  3339   apply (simp add: takefill_alt)
  3340   apply (rule bl_shiftl [THEN trans])
  3341   apply (subst ucast_up_app)
  3342   apply (auto simp add: wsst_TYs)
  3343   done
  3344 
  3345 lemmas rc1 = revcast_up [THEN 
  3346   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3347 lemmas rc2 = revcast_down_uu [THEN 
  3348   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3349 
  3350 lemmas ucast_up =
  3351  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
  3352 lemmas ucast_down = 
  3353   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
  3354 
  3355 
  3356 subsubsection "Slices"
  3357 
  3358 lemma slice1_no_bin [simp]:
  3359   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3360   by (simp add: slice1_def) (* TODO: neg_numeral *)
  3361 
  3362 lemma slice_no_bin [simp]:
  3363   "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
  3364     (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3365   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
  3366 
  3367 lemma slice1_0 [simp] : "slice1 n 0 = 0"
  3368   unfolding slice1_def by simp
  3369 
  3370 lemma slice_0 [simp] : "slice n 0 = 0"
  3371   unfolding slice_def by auto
  3372 
  3373 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
  3374   unfolding slice_def' slice1_def
  3375   by (simp add : takefill_alt word_size)
  3376 
  3377 lemmas slice_take = slice_take' [unfolded word_size]
  3378 
  3379 -- "shiftr to a word of the same size is just slice, 
  3380     slice is just shiftr then ucast"
  3381 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
  3382 
  3383 lemma slice_shiftr: "slice n w = ucast (w >> n)"
  3384   apply (unfold slice_take shiftr_bl)
  3385   apply (rule ucast_of_bl_up [symmetric])
  3386   apply (simp add: word_size)
  3387   done
  3388 
  3389 lemma nth_slice: 
  3390   "(slice n w :: 'a :: len0 word) !! m = 
  3391    (w !! (m + n) & m < len_of TYPE ('a))"
  3392   unfolding slice_shiftr 
  3393   by (simp add : nth_ucast nth_shiftr)
  3394 
  3395 lemma slice1_down_alt': 
  3396   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 
  3397     to_bl sl = takefill False fs (drop k (to_bl w))"
  3398   unfolding slice1_def word_size of_bl_def uint_bl
  3399   by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  3400 
  3401 lemma slice1_up_alt': 
  3402   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 
  3403     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  3404   apply (unfold slice1_def word_size of_bl_def uint_bl)
  3405   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
  3406                         takefill_append [symmetric])
  3407   apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
  3408     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
  3409   apply arith
  3410   done
  3411     
  3412 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
  3413 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
  3414 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
  3415 lemmas slice1_up_alts = 
  3416   le_add_diff_inverse [symmetric, THEN su1] 
  3417   le_add_diff_inverse2 [symmetric, THEN su1]
  3418 
  3419 lemma ucast_slice1: "ucast w = slice1 (size w) w"
  3420   unfolding slice1_def ucast_bl
  3421   by (simp add : takefill_same' word_size)
  3422 
  3423 lemma ucast_slice: "ucast w = slice 0 w"
  3424   unfolding slice_def by (simp add : ucast_slice1)
  3425 
  3426 lemma slice_id: "slice 0 t = t"
  3427   by (simp only: ucast_slice [symmetric] ucast_id)
  3428 
  3429 lemma revcast_slice1 [OF refl]: 
  3430   "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  3431   unfolding slice1_def revcast_def' by (simp add : word_size)
  3432 
  3433 lemma slice1_tf_tf': 
  3434   "to_bl (slice1 n w :: 'a :: len0 word) = 
  3435    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
  3436   unfolding slice1_def by (rule word_rev_tf)
  3437 
  3438 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
  3439 
  3440 lemma rev_slice1:
  3441   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
  3442   slice1 n (word_reverse w :: 'b :: len0 word) = 
  3443   word_reverse (slice1 k w :: 'a :: len0 word)"
  3444   apply (unfold word_reverse_def slice1_tf_tf)
  3445   apply (rule word_bl.Rep_inverse')
  3446   apply (rule rev_swap [THEN iffD1])
  3447   apply (rule trans [symmetric])
  3448   apply (rule tf_rev)
  3449    apply (simp add: word_bl.Abs_inverse)
  3450   apply (simp add: word_bl.Abs_inverse)
  3451   done
  3452 
  3453 lemma rev_slice:
  3454   "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
  3455     slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
  3456   apply (unfold slice_def word_size)
  3457   apply (rule rev_slice1)
  3458   apply arith
  3459   done
  3460 
  3461 lemmas sym_notr = 
  3462   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
  3463 
  3464 -- {* problem posed by TPHOLs referee:
  3465       criterion for overflow of addition of signed integers *}
  3466 
  3467 lemma sofl_test:
  3468   "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
  3469      ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
  3470   apply (unfold word_size)
  3471   apply (cases "len_of TYPE('a)", simp) 
  3472   apply (subst msb_shift [THEN sym_notr])
  3473   apply (simp add: word_ops_msb)
  3474   apply (simp add: word_msb_sint)
  3475   apply safe
  3476        apply simp_all
  3477      apply (unfold sint_word_ariths)
  3478      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
  3479      apply safe
  3480         apply (insert sint_range' [where x=x])
  3481         apply (insert sint_range' [where x=y])
  3482         defer 
  3483         apply (simp (no_asm), arith)
  3484        apply (simp (no_asm), arith)
  3485       defer
  3486       defer
  3487       apply (simp (no_asm), arith)
  3488      apply (simp (no_asm), arith)
  3489     apply (rule notI [THEN notnotD],
  3490            drule leI not_leE,
  3491            drule sbintrunc_inc sbintrunc_dec,      
  3492            simp)+
  3493   done
  3494 
  3495 
  3496 subsection "Split and cat"
  3497 
  3498 lemmas word_split_bin' = word_split_def
  3499 lemmas word_cat_bin' = word_cat_def
  3500 
  3501 lemma word_rsplit_no:
  3502   "(word_rsplit (numeral bin :: 'b :: len0 word) :: 'a word list) = 
  3503     map word_of_int (bin_rsplit (len_of TYPE('a :: len)) 
  3504       (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
  3505   unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
  3506 
  3507 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
  3508   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  3509 
  3510 lemma test_bit_cat:
  3511   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc & 
  3512     (if n < size b then b !! n else a !! (n - size b)))"
  3513   apply (unfold word_cat_bin' test_bit_bin)
  3514   apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  3515   apply (erule bin_nth_uint_imp)
  3516   done
  3517 
  3518 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
  3519   apply (unfold of_bl_def to_bl_def word_cat_bin')
  3520   apply (simp add: bl_to_bin_app_cat)
  3521   done
  3522 
  3523 lemma of_bl_append:
  3524   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
  3525   apply (unfold of_bl_def)
  3526   apply (simp add: bl_to_bin_app_cat bin_cat_num)
  3527   apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
  3528   done
  3529 
  3530 lemma of_bl_False [simp]:
  3531   "of_bl (False#xs) = of_bl xs"
  3532   by (rule word_eqI)
  3533      (auto simp add: test_bit_of_bl nth_append)
  3534 
  3535 lemma of_bl_True [simp]:
  3536   "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
  3537   by (subst of_bl_append [where xs="[True]", simplified])
  3538      (simp add: word_1_bl)
  3539 
  3540 lemma of_bl_Cons:
  3541   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  3542   by (cases x) simp_all
  3543 
  3544 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow> 
  3545   a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
  3546   apply (frule word_ubin.norm_Rep [THEN ssubst])
  3547   apply (drule bin_split_trunc1)
  3548   apply (drule sym [THEN trans])
  3549   apply assumption
  3550   apply safe
  3551   done
  3552 
  3553 lemma word_split_bl': 
  3554   "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 
  3555     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
  3556   apply (unfold word_split_bin')
  3557   apply safe
  3558    defer
  3559    apply (clarsimp split: prod.splits)
  3560    apply (drule word_ubin.norm_Rep [THEN ssubst])
  3561    apply (drule split_bintrunc)
  3562    apply (simp add : of_bl_def bl2bin_drop word_size
  3563        word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
  3564   apply (clarsimp split: prod.splits)
  3565   apply (frule split_uint_lem [THEN conjunct1])
  3566   apply (unfold word_size)
  3567   apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
  3568    defer
  3569    apply simp
  3570   apply (simp add : of_bl_def to_bl_def)
  3571   apply (subst bin_split_take1 [symmetric])
  3572     prefer 2
  3573     apply assumption
  3574    apply simp
  3575   apply (erule thin_rl)
  3576   apply (erule arg_cong [THEN trans])
  3577   apply (simp add : word_ubin.norm_eq_iff [symmetric])
  3578   done
  3579 
  3580 lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
  3581     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
  3582     word_split c = (a, b)"
  3583   apply (rule iffI)
  3584    defer
  3585    apply (erule (1) word_split_bl')
  3586   apply (case_tac "word_split c")
  3587   apply (auto simp add : word_size)
  3588   apply (frule word_split_bl' [rotated])
  3589   apply (auto simp add : word_size)
  3590   done
  3591 
  3592 lemma word_split_bl_eq:
  3593    "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
  3594       (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
  3595        of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
  3596   apply (rule word_split_bl [THEN iffD1])
  3597   apply (unfold word_size)
  3598   apply (rule refl conjI)+
  3599   done
  3600 
  3601 -- "keep quantifiers for use in simplification"
  3602 lemma test_bit_split':
  3603   "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
  3604     a !! m = (m < size a & c !! (m + size b)))"
  3605   apply (unfold word_split_bin' test_bit_bin)
  3606   apply (clarify)
  3607   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
  3608   apply (drule bin_nth_split)
  3609   apply safe
  3610        apply (simp_all add: add_commute)
  3611    apply (erule bin_nth_uint_imp)+
  3612   done
  3613 
  3614 lemma test_bit_split:
  3615   "word_split c = (a, b) \<Longrightarrow>
  3616     (\<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))"
  3617   by (simp add: test_bit_split')
  3618 
  3619 lemma test_bit_split_eq: "word_split c = (a, b) <-> 
  3620   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
  3621     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
  3622   apply (rule_tac iffI)
  3623    apply (rule_tac conjI)
  3624     apply (erule test_bit_split [THEN conjunct1])
  3625    apply (erule test_bit_split [THEN conjunct2])
  3626   apply (case_tac "word_split c")
  3627   apply (frule test_bit_split)
  3628   apply (erule trans)
  3629   apply (fastforce intro ! : word_eqI simp add : word_size)
  3630   done
  3631 
  3632 -- {* this odd result is analogous to @{text "ucast_id"}, 
  3633       result to the length given by the result type *}
  3634 
  3635 lemma word_cat_id: "word_cat a b = b"
  3636   unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
  3637 
  3638 -- "limited hom result"
  3639 lemma word_cat_hom:
  3640   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  3641   \<Longrightarrow>
  3642   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
  3643   word_of_int (bin_cat w (size b) (uint b))"
  3644   apply (unfold word_cat_def word_size) 
  3645   apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
  3646       word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
  3647   done
  3648 
  3649 lemma word_cat_split_alt:
  3650   "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  3651   apply (rule word_eqI)
  3652   apply (drule test_bit_split)
  3653   apply (clarsimp simp add : test_bit_cat word_size)
  3654   apply safe
  3655   apply arith
  3656   done
  3657 
  3658 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
  3659 
  3660 
  3661 subsubsection "Split and slice"
  3662 
  3663 lemma split_slices: 
  3664   "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
  3665   apply (drule test_bit_split)
  3666   apply (rule conjI)
  3667    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  3668   done
  3669 
  3670 lemma slice_cat1 [OF refl]:
  3671   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  3672   apply safe
  3673   apply (rule word_eqI)
  3674   apply (simp add: nth_slice test_bit_cat word_size)
  3675   done
  3676 
  3677 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  3678 
  3679 lemma cat_slices:
  3680   "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  3681     size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  3682   apply safe
  3683   apply (rule word_eqI)
  3684   apply (simp add: nth_slice test_bit_cat word_size)
  3685   apply safe
  3686   apply arith
  3687   done
  3688 
  3689 lemma word_split_cat_alt:
  3690   "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
  3691   apply (case_tac "word_split ?w")
  3692   apply (rule trans, assumption)
  3693   apply (drule test_bit_split)
  3694   apply safe
  3695    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  3696   done
  3697 
  3698 lemmas word_cat_bl_no_bin [simp] =
  3699   word_cat_bl [where a="numeral a" and b="numeral b",
  3700     unfolded to_bl_numeral]
  3701   for a b (* FIXME: negative numerals, 0 and 1 *)
  3702 
  3703 lemmas word_split_bl_no_bin [simp] =
  3704   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
  3705 
  3706 text {* this odd result arises from the fact that the statement of the
  3707       result implies that the decoded words are of the same type, 
  3708       and therefore of the same length, as the original word *}
  3709 
  3710 lemma word_rsplit_same: "word_rsplit w = [w]"
  3711   unfolding word_rsplit_def by (simp add : bin_rsplit_all)
  3712 
  3713 lemma word_rsplit_empty_iff_size:
  3714   "(word_rsplit w = []) = (size w = 0)" 
  3715   unfolding word_rsplit_def bin_rsplit_def word_size
  3716   by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
  3717 
  3718 lemma test_bit_rsplit:
  3719   "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
  3720     k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  3721   apply (unfold word_rsplit_def word_test_bit_def)
  3722   apply (rule trans)
  3723    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  3724    apply (rule nth_map [symmetric])
  3725    apply simp
  3726   apply (rule bin_nth_rsplit)
  3727      apply simp_all
  3728   apply (simp add : word_size rev_map)
  3729   apply (rule trans)
  3730    defer
  3731    apply (rule map_ident [THEN fun_cong])
  3732   apply (rule refl [THEN map_cong])
  3733   apply (simp add : word_ubin.eq_norm)
  3734   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  3735   done
  3736 
  3737 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  3738   unfolding word_rcat_def to_bl_def' of_bl_def
  3739   by (clarsimp simp add : bin_rcat_bl)
  3740 
  3741 lemma size_rcat_lem':
  3742   "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  3743   unfolding word_size by (induct wl) auto
  3744 
  3745 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  3746 
  3747 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
  3748 
  3749 lemma nth_rcat_lem:
  3750   "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
  3751     rev (concat (map to_bl wl)) ! n =
  3752     rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
  3753   apply (induct "wl")
  3754    apply clarsimp
  3755   apply (clarsimp simp add : nth_append size_rcat_lem)
  3756   apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
  3757          td_gal_lt_len less_Suc_eq_le mod_div_equality')
  3758   apply clarsimp
  3759   done
  3760 
  3761 lemma test_bit_rcat:
  3762   "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
  3763     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
  3764   apply (unfold word_rcat_bl word_size)
  3765   apply (clarsimp simp add : 
  3766     test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  3767   apply safe
  3768    apply (auto simp add : 
  3769     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  3770   done
  3771 
  3772 lemma foldl_eq_foldr:
  3773   "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
  3774   by (induct xs arbitrary: x) (auto simp add : add_assoc)
  3775 
  3776 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  3777 
  3778 lemmas test_bit_rsplit_alt = 
  3779   trans [OF nth_rev_alt [THEN test_bit_cong] 
  3780   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  3781 
  3782 -- "lazy way of expressing that u and v, and su and sv, have same types"
  3783 lemma word_rsplit_len_indep [OF refl refl refl refl]:
  3784   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
  3785     word_rsplit v = sv \<Longrightarrow> length su = length sv"
  3786   apply (unfold word_rsplit_def)
  3787   apply (auto simp add : bin_rsplit_len_indep)
  3788   done
  3789 
  3790 lemma length_word_rsplit_size: 
  3791   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3792     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
  3793   apply (unfold word_rsplit_def word_size)
  3794   apply (clarsimp simp add : bin_rsplit_len_le)
  3795   done
  3796 
  3797 lemmas length_word_rsplit_lt_size = 
  3798   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  3799 
  3800 lemma length_word_rsplit_exp_size:
  3801   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3802     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  3803   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
  3804 
  3805 lemma length_word_rsplit_even_size: 
  3806   "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow> 
  3807     length (word_rsplit w :: 'a word list) = m"
  3808   by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
  3809 
  3810 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  3811 
  3812 (* alternative proof of word_rcat_rsplit *)
  3813 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
  3814 lemmas dtle = xtr4 [OF tdle mult_commute]
  3815 
  3816 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  3817   apply (rule word_eqI)
  3818   apply (clarsimp simp add : test_bit_rcat word_size)
  3819   apply (subst refl [THEN test_bit_rsplit])
  3820     apply (simp_all add: word_size 
  3821       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  3822    apply safe
  3823    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  3824   done
  3825 
  3826 lemma size_word_rsplit_rcat_size:
  3827   "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
  3828      size frcw = length ws * len_of TYPE('a)\<rbrakk>
  3829     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  3830   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
  3831   apply (fast intro: given_quot_alt)
  3832   done
  3833 
  3834 lemma msrevs:
  3835   fixes n::nat
  3836   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  3837   and   "(k * n + m) mod n = m mod n"
  3838   by (auto simp: add_commute)
  3839 
  3840 lemma word_rsplit_rcat_size [OF refl]:
  3841   "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
  3842     size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
  3843   apply (frule size_word_rsplit_rcat_size, assumption)
  3844   apply (clarsimp simp add : word_size)
  3845   apply (rule nth_equalityI, assumption)
  3846   apply clarsimp
  3847   apply (rule word_eqI [rule_format])
  3848   apply (rule trans)
  3849    apply (rule test_bit_rsplit_alt)
  3850      apply (clarsimp simp: word_size)+
  3851   apply (rule trans)
  3852   apply (rule test_bit_rcat [OF refl refl])
  3853   apply (simp add: word_size msrevs)
  3854   apply (subst nth_rev)
  3855    apply arith
  3856   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3857   apply safe
  3858   apply (simp add: diff_mult_distrib)
  3859   apply (rule mpl_lem)
  3860   apply (cases "size ws")
  3861    apply simp_all
  3862   done
  3863 
  3864 
  3865 subsection "Rotation"
  3866 
  3867 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  3868 
  3869 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  3870 
  3871 lemma rotate_eq_mod: 
  3872   "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  3873   apply (rule box_equals)
  3874     defer
  3875     apply (rule rotate_conv_mod [symmetric])+
  3876   apply simp
  3877   done
  3878 
  3879 lemmas rotate_eqs = 
  3880   trans [OF rotate0 [THEN fun_cong] id_apply]
  3881   rotate_rotate [symmetric] 
  3882   rotate_id
  3883   rotate_conv_mod 
  3884   rotate_eq_mod
  3885 
  3886 
  3887 subsubsection "Rotation of list to right"
  3888 
  3889 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  3890   unfolding rotater1_def by (cases l) auto
  3891 
  3892 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  3893   apply (unfold rotater1_def)
  3894   apply (cases "l")
  3895   apply (case_tac [2] "list")
  3896   apply auto
  3897   done
  3898 
  3899 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  3900   unfolding rotater1_def by (cases l) auto
  3901 
  3902 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  3903   apply (cases "xs")
  3904   apply (simp add : rotater1_def)
  3905   apply (simp add : rotate1_rl')
  3906   done
  3907   
  3908 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  3909   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
  3910 
  3911 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
  3912   using rotater_rev' [where xs = "rev ys"] by simp
  3913 
  3914 lemma rotater_drop_take: 
  3915   "rotater n xs = 
  3916    drop (length xs - n mod length xs) xs @
  3917    take (length xs - n mod length xs) xs"
  3918   by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
  3919 
  3920 lemma rotater_Suc [simp] : 
  3921   "rotater (Suc n) xs = rotater1 (rotater n xs)"
  3922   unfolding rotater_def by auto
  3923 
  3924 lemma rotate_inv_plus [rule_format] :
  3925   "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs & 
  3926     rotate k (rotater n xs) = rotate m xs & 
  3927     rotater n (rotate k xs) = rotate m xs & 
  3928     rotate n (rotater k xs) = rotater m xs"
  3929   unfolding rotater_def rotate_def
  3930   by (induct n) (auto intro: funpow_swap1 [THEN trans])
  3931   
  3932 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  3933 
  3934 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  3935 
  3936 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
  3937 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
  3938 
  3939 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
  3940   by auto
  3941 
  3942 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
  3943   by auto
  3944 
  3945 lemma length_rotater [simp]: 
  3946   "length (rotater n xs) = length xs"
  3947   by (simp add : rotater_rev)
  3948 
  3949 lemma restrict_to_left:
  3950   assumes "x = y"
  3951   shows "(x = z) = (y = z)"
  3952   using assms by simp
  3953 
  3954 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
  3955   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
  3956 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  3957 lemmas rotater_eqs = rrs1 [simplified length_rotater]
  3958 lemmas rotater_0 = rotater_eqs (1)
  3959 lemmas rotater_add = rotater_eqs (2)
  3960 
  3961 
  3962 subsubsection "map, map2, commuting with rotate(r)"
  3963 
  3964 lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
  3965   by (induct xs) auto
  3966 
  3967 lemma butlast_map:
  3968   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  3969   by (induct xs) auto
  3970 
  3971 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
  3972   unfolding rotater1_def
  3973   by (cases xs) (auto simp add: last_map butlast_map)
  3974 
  3975 lemma rotater_map:
  3976   "rotater n (map f xs) = map f (rotater n xs)" 
  3977   unfolding rotater_def
  3978   by (induct n) (auto simp add : rotater1_map)
  3979 
  3980 lemma but_last_zip [rule_format] :
  3981   "ALL ys. length xs = length ys --> xs ~= [] --> 
  3982     last (zip xs ys) = (last xs, last ys) & 
  3983     butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 
  3984   apply (induct "xs")
  3985   apply auto
  3986      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3987   done
  3988 
  3989 lemma but_last_map2 [rule_format] :
  3990   "ALL ys. length xs = length ys --> xs ~= [] --> 
  3991     last (map2 f xs ys) = f (last xs) (last ys) & 
  3992     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 
  3993   apply (induct "xs")
  3994   apply auto
  3995      apply (unfold map2_def)
  3996      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  3997   done
  3998 
  3999 lemma rotater1_zip:
  4000   "length xs = length ys \<Longrightarrow> 
  4001     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  4002   apply (unfold rotater1_def)
  4003   apply (cases "xs")
  4004    apply auto
  4005    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  4006   done
  4007 
  4008 lemma rotater1_map2:
  4009   "length xs = length ys \<Longrightarrow> 
  4010     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
  4011   unfolding map2_def by (simp add: rotater1_map rotater1_zip)
  4012 
  4013 lemmas lrth = 
  4014   box_equals [OF asm_rl length_rotater [symmetric] 
  4015                  length_rotater [symmetric], 
  4016               THEN rotater1_map2]
  4017 
  4018 lemma rotater_map2: 
  4019   "length xs = length ys \<Longrightarrow> 
  4020     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
  4021   by (induct n) (auto intro!: lrth)
  4022 
  4023 lemma rotate1_map2:
  4024   "length xs = length ys \<Longrightarrow> 
  4025     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  4026   apply (unfold map2_def)
  4027   apply (cases xs)
  4028    apply (cases ys, auto)+
  4029   done
  4030 
  4031 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
  4032   length_rotate [symmetric], THEN rotate1_map2]
  4033 
  4034 lemma rotate_map2: 
  4035   "length xs = length ys \<Longrightarrow> 
  4036     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
  4037   by (induct n) (auto intro!: lth)
  4038 
  4039 
  4040 -- "corresponding equalities for word rotation"
  4041 
  4042 lemma to_bl_rotl: 
  4043   "to_bl (word_rotl n w) = rotate n (to_bl w)"
  4044   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  4045 
  4046 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  4047 
  4048 lemmas word_rotl_eqs =
  4049   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  4050 
  4051 lemma to_bl_rotr: 
  4052   "to_bl (word_rotr n w) = rotater n (to_bl w)"
  4053   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  4054 
  4055 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  4056 
  4057 lemmas word_rotr_eqs =
  4058   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  4059 
  4060 declare word_rotr_eqs (1) [simp]
  4061 declare word_rotl_eqs (1) [simp]
  4062 
  4063 lemma
  4064   word_rot_rl [simp]:
  4065   "word_rotl k (word_rotr k v) = v" and
  4066   word_rot_lr [simp]:
  4067   "word_rotr k (word_rotl k v) = v"
  4068   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  4069 
  4070 lemma
  4071   word_rot_gal:
  4072   "(word_rotr n v = w) = (word_rotl n w = v)" and
  4073   word_rot_gal':
  4074   "(w = word_rotr n v) = (v = word_rotl n w)"
  4075   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] 
  4076            dest: sym)
  4077 
  4078 lemma word_rotr_rev:
  4079   "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  4080   by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
  4081                 to_bl_rotr to_bl_rotl rotater_rev)
  4082   
  4083 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  4084   by (unfold word_rot_defs) auto
  4085 
  4086 lemmas abl_cong = arg_cong [where f = "of_bl"]
  4087 
  4088 lemma word_roti_add: 
  4089   "word_roti (m + n) w = word_roti m (word_roti n w)"
  4090 proof -
  4091   have rotater_eq_lem: 
  4092     "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  4093     by auto
  4094 
  4095   have rotate_eq_lem: 
  4096     "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  4097     by auto
  4098 
  4099   note rpts [symmetric] = 
  4100     rotate_inv_plus [THEN conjunct1]
  4101     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  4102     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  4103     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  4104 
  4105   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  4106   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  4107 
  4108   show ?thesis
  4109   apply (unfold word_rot_defs)
  4110   apply (simp only: split: split_if)
  4111   apply (safe intro!: abl_cong)
  4112   apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
  4113                     to_bl_rotl
  4114                     to_bl_rotr [THEN word_bl.Rep_inverse']
  4115                     to_bl_rotr)
  4116   apply (rule rrp rrrp rpts,
  4117          simp add: nat_add_distrib [symmetric] 
  4118                    nat_diff_distrib [symmetric])+
  4119   done
  4120 qed
  4121     
  4122 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
  4123   apply (unfold word_rot_defs)
  4124   apply (cut_tac y="size w" in gt_or_eq_0)
  4125   apply (erule disjE)
  4126    apply simp_all
  4127   apply (safe intro!: abl_cong)
  4128    apply (rule rotater_eqs)
  4129    apply (simp add: word_size nat_mod_distrib)
  4130   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  4131   apply (rule rotater_eqs)
  4132   apply (simp add: word_size nat_mod_distrib)
  4133   apply (rule int_eq_0_conv [THEN iffD1])
  4134   apply (simp only: zmod_int of_nat_add)
  4135   apply (simp add: rdmods)
  4136   done
  4137 
  4138 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  4139 
  4140 
  4141 subsubsection "Word rotation commutes with bit-wise operations"
  4142 
  4143 (* using locale to not pollute lemma namespace *)
  4144 locale word_rotate 
  4145 begin
  4146 
  4147 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  4148 
  4149 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  4150 
  4151 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
  4152 
  4153 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  4154 
  4155 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
  4156 
  4157 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  4158 
  4159 lemma word_rot_logs:
  4160   "word_rotl n (NOT v) = NOT word_rotl n v"
  4161   "word_rotr n (NOT v) = NOT word_rotr n v"
  4162   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  4163   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  4164   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  4165   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  4166   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  4167   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"  
  4168   by (rule word_bl.Rep_eqD,
  4169       rule word_rot_defs' [THEN trans],
  4170       simp only: blwl_syms [symmetric],
  4171       rule th1s [THEN trans], 
  4172       rule refl)+
  4173 end
  4174 
  4175 lemmas word_rot_logs = word_rotate.word_rot_logs
  4176 
  4177 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  4178   simplified word_bl_Rep']
  4179 
  4180 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  4181   simplified word_bl_Rep']
  4182 
  4183 lemma bl_word_roti_dt': 
  4184   "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow> 
  4185     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4186   apply (unfold word_roti_def)
  4187   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4188   apply safe
  4189    apply (simp add: zmod_zminus1_eq_if)
  4190    apply safe
  4191     apply (simp add: nat_mult_distrib)
  4192    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 
  4193                                       [THEN conjunct2, THEN order_less_imp_le]]
  4194                     nat_mod_distrib)
  4195   apply (simp add: nat_mod_distrib)
  4196   done
  4197 
  4198 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  4199 
  4200 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]] 
  4201 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4202 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4203 
  4204 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
  4205   by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
  4206 
  4207 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  4208   unfolding word_roti_def by auto
  4209 
  4210 lemmas word_rotr_dt_no_bin' [simp] = 
  4211   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4212   (* FIXME: negative numerals, 0 and 1 *)
  4213 
  4214 lemmas word_rotl_dt_no_bin' [simp] = 
  4215   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4216   (* FIXME: negative numerals, 0 and 1 *)
  4217 
  4218 declare word_roti_def [simp]
  4219 
  4220 
  4221 subsection {* Maximum machine word *}
  4222 
  4223 lemma word_int_cases:
  4224   obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
  4225   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
  4226 
  4227 lemma word_nat_cases [cases type: word]:
  4228   obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
  4229   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
  4230 
  4231 lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
  4232   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
  4233 
  4234 lemma max_word_max [simp,intro!]: "n \<le> max_word"
  4235   by (cases n rule: word_int_cases)
  4236      (simp add: max_word_def word_le_def int_word_uint int_mod_eq')
  4237   
  4238 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
  4239   by (subst word_uint.Abs_norm [symmetric]) simp
  4240 
  4241 lemma word_pow_0:
  4242   "(2::'a::len word) ^ len_of TYPE('a) = 0"
  4243 proof -
  4244   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
  4245     by (rule word_of_int_2p_len)
  4246   thus ?thesis by (simp add: word_of_int_2p)
  4247 qed
  4248 
  4249 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
  4250   apply (simp add: max_word_eq)
  4251   apply uint_arith
  4252   apply auto
  4253   apply (simp add: word_pow_0)
  4254   done
  4255 
  4256 lemma max_word_minus: 
  4257   "max_word = (-1::'a::len word)"
  4258 proof -
  4259   have "-1 + 1 = (0::'a word)" by simp
  4260   thus ?thesis by (rule max_word_wrap [symmetric])
  4261 qed
  4262 
  4263 lemma max_word_bl [simp]:
  4264   "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
  4265   by (subst max_word_minus to_bl_n1)+ simp
  4266 
  4267 lemma max_test_bit [simp]:
  4268   "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
  4269   by (auto simp add: test_bit_bl word_size)
  4270 
  4271 lemma word_and_max [simp]:
  4272   "x AND max_word = x"
  4273   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4274 
  4275 lemma word_or_max [simp]:
  4276   "x OR max_word = max_word"
  4277   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4278 
  4279 lemma word_ao_dist2:
  4280   "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
  4281   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4282 
  4283 lemma word_oa_dist2:
  4284   "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
  4285   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4286 
  4287 lemma word_and_not [simp]:
  4288   "x AND NOT x = (0::'a::len0 word)"
  4289   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4290 
  4291 lemma word_or_not [simp]:
  4292   "x OR NOT x = max_word"
  4293   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4294 
  4295 lemma word_boolean:
  4296   "boolean (op AND) (op OR) bitNOT 0 max_word"
  4297   apply (rule boolean.intro)
  4298            apply (rule word_bw_assocs)
  4299           apply (rule word_bw_assocs)
  4300          apply (rule word_bw_comms)
  4301         apply (rule word_bw_comms)
  4302        apply (rule word_ao_dist2)
  4303       apply (rule word_oa_dist2)
  4304      apply (rule word_and_max)
  4305     apply (rule word_log_esimps)
  4306    apply (rule word_and_not)
  4307   apply (rule word_or_not)
  4308   done
  4309 
  4310 interpretation word_bool_alg:
  4311   boolean "op AND" "op OR" bitNOT 0 max_word
  4312   by (rule word_boolean)
  4313 
  4314 lemma word_xor_and_or:
  4315   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
  4316   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4317 
  4318 interpretation word_bool_alg:
  4319   boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
  4320   apply (rule boolean_xor.intro)
  4321    apply (rule word_boolean)
  4322   apply (rule boolean_xor_axioms.intro)
  4323   apply (rule word_xor_and_or)
  4324   done
  4325 
  4326 lemma shiftr_x_0 [iff]:
  4327   "(x::'a::len0 word) >> 0 = x"
  4328   by (simp add: shiftr_bl)
  4329 
  4330 lemma shiftl_x_0 [simp]: 
  4331   "(x :: 'a :: len word) << 0 = x"
  4332   by (simp add: shiftl_t2n)
  4333 
  4334 lemma shiftl_1 [simp]:
  4335   "(1::'a::len word) << n = 2^n"
  4336   by (simp add: shiftl_t2n)
  4337 
  4338 lemma uint_lt_0 [simp]:
  4339   "uint x < 0 = False"
  4340   by (simp add: linorder_not_less)
  4341 
  4342 lemma shiftr1_1 [simp]: 
  4343   "shiftr1 (1::'a::len word) = 0"
  4344   unfolding shiftr1_def by simp
  4345 
  4346 lemma shiftr_1[simp]: 
  4347   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  4348   by (induct n) (auto simp: shiftr_def)
  4349 
  4350 lemma word_less_1 [simp]: 
  4351   "((x::'a::len word) < 1) = (x = 0)"
  4352   by (simp add: word_less_nat_alt unat_0_iff)
  4353 
  4354 lemma to_bl_mask:
  4355   "to_bl (mask n :: 'a::len word) = 
  4356   replicate (len_of TYPE('a) - n) False @ 
  4357     replicate (min (len_of TYPE('a)) n) True"
  4358   by (simp add: mask_bl word_rep_drop min_def)
  4359 
  4360 lemma map_replicate_True:
  4361   "n = length xs \<Longrightarrow>
  4362     map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
  4363   by (induct xs arbitrary: n) auto
  4364 
  4365 lemma map_replicate_False:
  4366   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
  4367     (zip xs (replicate n False)) = replicate n False"
  4368   by (induct xs arbitrary: n) auto
  4369 
  4370 lemma bl_and_mask:
  4371   fixes w :: "'a::len word"
  4372   fixes n
  4373   defines "n' \<equiv> len_of TYPE('a) - n"
  4374   shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
  4375 proof - 
  4376   note [simp] = map_replicate_True map_replicate_False
  4377   have "to_bl (w AND mask n) = 
  4378         map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
  4379     by (simp add: bl_word_and)
  4380   also
  4381   have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
  4382   also
  4383   have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = 
  4384         replicate n' False @ drop n' (to_bl w)"
  4385     unfolding to_bl_mask n'_def map2_def
  4386     by (subst zip_append) auto
  4387   finally
  4388   show ?thesis .
  4389 qed
  4390 
  4391 lemma drop_rev_takefill:
  4392   "length xs \<le> n \<Longrightarrow>
  4393     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4394   by (simp add: takefill_alt rev_take)
  4395 
  4396 lemma map_nth_0 [simp]:
  4397   "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  4398   by (induct xs) auto
  4399 
  4400 lemma uint_plus_if_size:
  4401   "uint (x + y) = 
  4402   (if uint x + uint y < 2^size x then 
  4403       uint x + uint y 
  4404    else 
  4405       uint x + uint y - 2^size x)" 
  4406   by (simp add: word_arith_alts int_word_uint mod_add_if_z 
  4407                 word_size)
  4408 
  4409 lemma unat_plus_if_size:
  4410   "unat (x + (y::'a::len word)) = 
  4411   (if unat x + unat y < 2^size x then 
  4412       unat x + unat y 
  4413    else 
  4414       unat x + unat y - 2^size x)" 
  4415   apply (subst word_arith_nat_defs)
  4416   apply (subst unat_of_nat)
  4417   apply (simp add:  mod_nat_add word_size)
  4418   done
  4419 
  4420 lemma word_neq_0_conv:
  4421   fixes w :: "'a :: len word"
  4422   shows "(w \<noteq> 0) = (0 < w)"
  4423   unfolding word_gt_0 by simp
  4424 
  4425 lemma max_lt:
  4426   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
  4427   apply (subst word_arith_nat_defs)
  4428   apply (subst word_unat.eq_norm)
  4429   apply (subst mod_if)
  4430   apply clarsimp
  4431   apply (erule notE)
  4432   apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
  4433   apply (erule order_le_less_trans)
  4434   apply (insert unat_lt2p [of "max a b"])
  4435   apply simp
  4436   done
  4437 
  4438 lemma uint_sub_if_size:
  4439   "uint (x - y) = 
  4440   (if uint y \<le> uint x then 
  4441       uint x - uint y 
  4442    else 
  4443       uint x - uint y + 2^size x)"
  4444   by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
  4445                 word_size)
  4446 
  4447 lemma unat_sub:
  4448   "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4449   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4450 
  4451 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  4452 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  4453   
  4454 lemma word_of_int_minus: 
  4455   "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  4456 proof -
  4457   have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
  4458   show ?thesis
  4459     apply (subst x)
  4460     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  4461     apply simp
  4462     done
  4463 qed
  4464   
  4465 lemmas word_of_int_inj = 
  4466   word_uint.Abs_inject [unfolded uints_num, simplified]
  4467 
  4468 lemma word_le_less_eq:
  4469   "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
  4470   by (auto simp add: order_class.le_less)
  4471 
  4472 lemma mod_plus_cong:
  4473   assumes 1: "(b::int) = b'"
  4474       and 2: "x mod b' = x' mod b'"
  4475       and 3: "y mod b' = y' mod b'"
  4476       and 4: "x' + y' = z'"
  4477   shows "(x + y) mod b = z' mod b'"
  4478 proof -
  4479   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  4480     by (simp add: mod_add_eq[symmetric])
  4481   also have "\<dots> = (x' + y') mod b'"
  4482     by (simp add: mod_add_eq[symmetric])
  4483   finally show ?thesis by (simp add: 4)
  4484 qed
  4485 
  4486 lemma mod_minus_cong:
  4487   assumes 1: "(b::int) = b'"
  4488       and 2: "x mod b' = x' mod b'"
  4489       and 3: "y mod b' = y' mod b'"
  4490       and 4: "x' - y' = z'"
  4491   shows "(x - y) mod b = z' mod b'"
  4492   using assms
  4493   apply (subst mod_diff_left_eq)
  4494   apply (subst mod_diff_right_eq)
  4495   apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
  4496   done
  4497 
  4498 lemma word_induct_less: 
  4499   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4500   apply (cases m)
  4501   apply atomize
  4502   apply (erule rev_mp)+
  4503   apply (rule_tac x=m in spec)
  4504   apply (induct_tac n)
  4505    apply simp
  4506   apply clarsimp
  4507   apply (erule impE)
  4508    apply clarsimp
  4509    apply (erule_tac x=n in allE)
  4510    apply (erule impE)
  4511     apply (simp add: unat_arith_simps)
  4512     apply (clarsimp simp: unat_of_nat)
  4513    apply simp
  4514   apply (erule_tac x="of_nat na" in allE)
  4515   apply (erule impE)
  4516    apply (simp add: unat_arith_simps)
  4517    apply (clarsimp simp: unat_of_nat)
  4518   apply simp
  4519   done
  4520   
  4521 lemma word_induct: 
  4522   "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4523   by (erule word_induct_less, simp)
  4524 
  4525 lemma word_induct2 [induct type]: 
  4526   "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
  4527   apply (rule word_induct, simp)
  4528   apply (case_tac "1+n = 0", auto)
  4529   done
  4530 
  4531 subsection {* Recursion combinator for words *}
  4532 
  4533 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
  4534   "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
  4535 
  4536 lemma word_rec_0: "word_rec z s 0 = z"
  4537   by (simp add: word_rec_def)
  4538 
  4539 lemma word_rec_Suc: 
  4540   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
  4541   apply (simp add: word_rec_def unat_word_ariths)
  4542   apply (subst nat_mod_eq')
  4543    apply (cut_tac x=n in unat_lt2p)
  4544    apply (drule Suc_mono)
  4545    apply (simp add: less_Suc_eq_le)
  4546    apply (simp only: order_less_le, simp)
  4547    apply (erule contrapos_pn, simp)
  4548    apply (drule arg_cong[where f=of_nat])
  4549    apply simp
  4550    apply (subst (asm) word_unat.Rep_inverse[of n])
  4551    apply simp
  4552   apply simp
  4553   done
  4554 
  4555 lemma word_rec_Pred: 
  4556   "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
  4557   apply (rule subst[where t="n" and s="1 + (n - 1)"])
  4558    apply simp
  4559   apply (subst word_rec_Suc)
  4560    apply simp
  4561   apply simp
  4562   done
  4563 
  4564 lemma word_rec_in: 
  4565   "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  4566   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4567 
  4568 lemma word_rec_in2: 
  4569   "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  4570   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4571 
  4572 lemma word_rec_twice: 
  4573   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  4574 apply (erule rev_mp)
  4575 apply (rule_tac x=z in spec)
  4576 apply (rule_tac x=f in spec)
  4577 apply (induct n)
  4578  apply (simp add: word_rec_0)
  4579 apply clarsimp
  4580 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  4581  apply simp
  4582 apply (case_tac "1 + (n - m) = 0")
  4583  apply (simp add: word_rec_0)
  4584  apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
  4585  apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  4586   apply simp
  4587  apply (simp (no_asm_use))
  4588 apply (simp add: word_rec_Suc word_rec_in2)
  4589 apply (erule impE)
  4590  apply uint_arith
  4591 apply (drule_tac x="x \<circ> op + 1" in spec)
  4592 apply (drule_tac x="x 0 xa" in spec)
  4593 apply simp
  4594 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
  4595        in subst)
  4596  apply (clarsimp simp add: fun_eq_iff)
  4597  apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  4598   apply simp
  4599  apply (rule refl)
  4600 apply (rule refl)
  4601 done
  4602 
  4603 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  4604   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  4605 
  4606 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  4607 apply (erule rev_mp)
  4608 apply (induct n)
  4609  apply (auto simp add: word_rec_0 word_rec_Suc)
  4610  apply (drule spec, erule mp)
  4611  apply uint_arith
  4612 apply (drule_tac x=n in spec, erule impE)
  4613  apply uint_arith
  4614 apply simp
  4615 done
  4616 
  4617 lemma word_rec_max: 
  4618   "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
  4619 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  4620  apply simp
  4621 apply simp
  4622 apply (rule word_rec_id_eq)
  4623 apply clarsimp
  4624 apply (drule spec, rule mp, erule mp)
  4625  apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  4626   prefer 2 
  4627   apply assumption
  4628  apply simp
  4629 apply (erule contrapos_pn)
  4630 apply simp
  4631 apply (drule arg_cong[where f="\<lambda>x. x - n"])
  4632 apply simp
  4633 done
  4634 
  4635 lemma unatSuc: 
  4636   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  4637   by unat_arith
  4638 
  4639 lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
  4640   by (fact word_1_no [symmetric])
  4641 
  4642 declare bin_to_bl_def [simp]
  4643 
  4644 ML_file "~~/src/HOL/Word/Tools/word_lib.ML"
  4645 ML_file "~~/src/HOL/Word/Tools/smt_word.ML"
  4646 setup {* SMT_Word.setup *}
  4647 
  4648 hide_const (open) Word
  4649 
  4650 end
  4651