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