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