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