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