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