src/HOL/Word/Word.thy
author paulson <lp15@cam.ac.uk>
Fri Nov 13 12:27:13 2015 +0000 (2015-11-13)
changeset 61649 268d88ec9087
parent 61424 c3658c18b7bc
child 61799 4cf66f21b764
permissions -rw-r--r--
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
     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 of_nat_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)
  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   by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
  2129 
  2130 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
  2131 
  2132 lemma word_le_exists': 
  2133   "(x :: 'a :: len0 word) <= y \<Longrightarrow> 
  2134     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
  2135   apply (rule exI)
  2136   apply (rule conjI)
  2137   apply (rule zadd_diff_inverse)
  2138   apply uint_arith
  2139   done
  2140 
  2141 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
  2142 
  2143 lemmas plus_minus_no_overflow =
  2144   order_less_imp_le [THEN plus_minus_no_overflow_ab]
  2145   
  2146 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
  2147   word_le_minus_cancel word_le_minus_mono_left
  2148 
  2149 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x
  2150 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
  2151 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
  2152 
  2153 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
  2154 
  2155 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
  2156 
  2157 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle 
  2158 
  2159 lemma word_mod_div_equality:
  2160   "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
  2161   apply (unfold word_less_nat_alt word_arith_nat_defs)
  2162   apply (cut_tac y="unat b" in gt_or_eq_0)
  2163   apply (erule disjE)
  2164    apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
  2165   apply simp
  2166   done
  2167 
  2168 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
  2169   apply (unfold word_le_nat_alt word_arith_nat_defs)
  2170   apply (cut_tac y="unat b" in gt_or_eq_0)
  2171   apply (erule disjE)
  2172    apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
  2173   apply simp
  2174   done
  2175 
  2176 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
  2177   apply (simp only: word_less_nat_alt word_arith_nat_defs)
  2178   apply (clarsimp simp add : uno_simps)
  2179   done
  2180 
  2181 lemma word_of_int_power_hom: 
  2182   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
  2183   by (induct n) (simp_all add: wi_hom_mult [symmetric])
  2184 
  2185 lemma word_arith_power_alt: 
  2186   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
  2187   by (simp add : word_of_int_power_hom [symmetric])
  2188 
  2189 lemma of_bl_length_less: 
  2190   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
  2191   apply (unfold of_bl_def word_less_alt word_numeral_alt)
  2192   apply safe
  2193   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
  2194                        del: word_of_int_numeral)
  2195   apply (simp add: mod_pos_pos_trivial)
  2196   apply (subst mod_pos_pos_trivial)
  2197     apply (rule bl_to_bin_ge0)
  2198    apply (rule order_less_trans)
  2199     apply (rule bl_to_bin_lt2p)
  2200    apply simp
  2201   apply (rule bl_to_bin_lt2p)
  2202   done
  2203 
  2204 
  2205 subsection {* Cardinality, finiteness of set of words *}
  2206 
  2207 instance word :: (len0) finite
  2208   by standard (simp add: type_definition.univ [OF type_definition_word])
  2209 
  2210 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
  2211   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
  2212 
  2213 lemma card_word_size: 
  2214   "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
  2215 unfolding word_size by (rule card_word)
  2216 
  2217 
  2218 subsection {* Bitwise Operations on Words *}
  2219 
  2220 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
  2221   
  2222 (* following definitions require both arithmetic and bit-wise word operations *)
  2223 
  2224 (* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
  2225 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
  2226   folded word_ubin.eq_norm, THEN eq_reflection]
  2227 
  2228 (* the binary operations only *)
  2229 (* BH: why is this needed? *)
  2230 lemmas word_log_binary_defs = 
  2231   word_and_def word_or_def word_xor_def
  2232 
  2233 lemma word_wi_log_defs:
  2234   "NOT word_of_int a = word_of_int (NOT a)"
  2235   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
  2236   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
  2237   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
  2238   by (transfer, rule refl)+
  2239 
  2240 lemma word_no_log_defs [simp]:
  2241   "NOT (numeral a) = word_of_int (NOT (numeral a))"
  2242   "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
  2243   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
  2244   "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
  2245   "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
  2246   "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
  2247   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
  2248   "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
  2249   "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
  2250   "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
  2251   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
  2252   "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
  2253   "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
  2254   "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
  2255   by (transfer, rule refl)+
  2256 
  2257 text {* Special cases for when one of the arguments equals 1. *}
  2258 
  2259 lemma word_bitwise_1_simps [simp]:
  2260   "NOT (1::'a::len0 word) = -2"
  2261   "1 AND numeral b = word_of_int (1 AND numeral b)"
  2262   "1 AND - numeral b = word_of_int (1 AND - numeral b)"
  2263   "numeral a AND 1 = word_of_int (numeral a AND 1)"
  2264   "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
  2265   "1 OR numeral b = word_of_int (1 OR numeral b)"
  2266   "1 OR - numeral b = word_of_int (1 OR - numeral b)"
  2267   "numeral a OR 1 = word_of_int (numeral a OR 1)"
  2268   "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
  2269   "1 XOR numeral b = word_of_int (1 XOR numeral b)"
  2270   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
  2271   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
  2272   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
  2273   by (transfer, simp)+
  2274 
  2275 text {* Special cases for when one of the arguments equals -1. *}
  2276 
  2277 lemma word_bitwise_m1_simps [simp]:
  2278   "NOT (-1::'a::len0 word) = 0"
  2279   "(-1::'a::len0 word) AND x = x"
  2280   "x AND (-1::'a::len0 word) = x"
  2281   "(-1::'a::len0 word) OR x = -1"
  2282   "x OR (-1::'a::len0 word) = -1"
  2283   " (-1::'a::len0 word) XOR x = NOT x"
  2284   "x XOR (-1::'a::len0 word) = NOT x"
  2285   by (transfer, simp)+
  2286 
  2287 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
  2288   by (transfer, simp add: bin_trunc_ao)
  2289 
  2290 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
  2291   by (transfer, simp add: bin_trunc_ao)
  2292 
  2293 lemma test_bit_wi [simp]:
  2294   "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
  2295   unfolding word_test_bit_def
  2296   by (simp add: word_ubin.eq_norm nth_bintr)
  2297 
  2298 lemma word_test_bit_transfer [transfer_rule]:
  2299   "(rel_fun pcr_word (rel_fun op = op =))
  2300     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
  2301   unfolding rel_fun_def word.pcr_cr_eq cr_word_def by simp
  2302 
  2303 lemma word_ops_nth_size:
  2304   "n < size (x::'a::len0 word) \<Longrightarrow> 
  2305     (x OR y) !! n = (x !! n | y !! n) & 
  2306     (x AND y) !! n = (x !! n & y !! n) & 
  2307     (x XOR y) !! n = (x !! n ~= y !! n) & 
  2308     (NOT x) !! n = (~ x !! n)"
  2309   unfolding word_size by transfer (simp add: bin_nth_ops)
  2310 
  2311 lemma word_ao_nth:
  2312   fixes x :: "'a::len0 word"
  2313   shows "(x OR y) !! n = (x !! n | y !! n) & 
  2314          (x AND y) !! n = (x !! n & y !! n)"
  2315   by transfer (auto simp add: bin_nth_ops)
  2316 
  2317 lemma test_bit_numeral [simp]:
  2318   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2319     n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
  2320   by transfer (rule refl)
  2321 
  2322 lemma test_bit_neg_numeral [simp]:
  2323   "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2324     n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
  2325   by transfer (rule refl)
  2326 
  2327 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
  2328   by transfer auto
  2329   
  2330 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
  2331   by transfer simp
  2332 
  2333 lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  2334   by transfer simp
  2335 
  2336 (* get from commutativity, associativity etc of int_and etc
  2337   to same for word_and etc *)
  2338 
  2339 lemmas bwsimps = 
  2340   wi_hom_add
  2341   word_wi_log_defs
  2342 
  2343 lemma word_bw_assocs:
  2344   fixes x :: "'a::len0 word"
  2345   shows
  2346   "(x AND y) AND z = x AND y AND z"
  2347   "(x OR y) OR z = x OR y OR z"
  2348   "(x XOR y) XOR z = x XOR y XOR z"
  2349   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2350   
  2351 lemma word_bw_comms:
  2352   fixes x :: "'a::len0 word"
  2353   shows
  2354   "x AND y = y AND x"
  2355   "x OR y = y OR x"
  2356   "x XOR y = y XOR x"
  2357   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2358   
  2359 lemma word_bw_lcs:
  2360   fixes x :: "'a::len0 word"
  2361   shows
  2362   "y AND x AND z = x AND y AND z"
  2363   "y OR x OR z = x OR y OR z"
  2364   "y XOR x XOR z = x XOR y XOR z"
  2365   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2366 
  2367 lemma word_log_esimps [simp]:
  2368   fixes x :: "'a::len0 word"
  2369   shows
  2370   "x AND 0 = 0"
  2371   "x AND -1 = x"
  2372   "x OR 0 = x"
  2373   "x OR -1 = -1"
  2374   "x XOR 0 = x"
  2375   "x XOR -1 = NOT x"
  2376   "0 AND x = 0"
  2377   "-1 AND x = x"
  2378   "0 OR x = x"
  2379   "-1 OR x = -1"
  2380   "0 XOR x = x"
  2381   "-1 XOR x = NOT x"
  2382   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2383 
  2384 lemma word_not_dist:
  2385   fixes x :: "'a::len0 word"
  2386   shows
  2387   "NOT (x OR y) = NOT x AND NOT y"
  2388   "NOT (x AND y) = NOT x OR NOT y"
  2389   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2390 
  2391 lemma word_bw_same:
  2392   fixes x :: "'a::len0 word"
  2393   shows
  2394   "x AND x = x"
  2395   "x OR x = x"
  2396   "x XOR x = 0"
  2397   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2398 
  2399 lemma word_ao_absorbs [simp]:
  2400   fixes x :: "'a::len0 word"
  2401   shows
  2402   "x AND (y OR x) = x"
  2403   "x OR y AND x = x"
  2404   "x AND (x OR y) = x"
  2405   "y AND x OR x = x"
  2406   "(y OR x) AND x = x"
  2407   "x OR x AND y = x"
  2408   "(x OR y) AND x = x"
  2409   "x AND y OR x = x"
  2410   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2411 
  2412 lemma word_not_not [simp]:
  2413   "NOT NOT (x::'a::len0 word) = x"
  2414   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2415 
  2416 lemma word_ao_dist:
  2417   fixes x :: "'a::len0 word"
  2418   shows "(x OR y) AND z = x AND z OR y AND z"
  2419   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2420 
  2421 lemma word_oa_dist:
  2422   fixes x :: "'a::len0 word"
  2423   shows "x AND y OR z = (x OR z) AND (y OR z)"
  2424   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2425 
  2426 lemma word_add_not [simp]: 
  2427   fixes x :: "'a::len0 word"
  2428   shows "x + NOT x = -1"
  2429   by transfer (simp add: bin_add_not)
  2430 
  2431 lemma word_plus_and_or [simp]:
  2432   fixes x :: "'a::len0 word"
  2433   shows "(x AND y) + (x OR y) = x + y"
  2434   by transfer (simp add: plus_and_or)
  2435 
  2436 lemma leoa:   
  2437   fixes x :: "'a::len0 word"
  2438   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  2439 lemma leao: 
  2440   fixes x' :: "'a::len0 word"
  2441   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
  2442 
  2443 lemma word_ao_equiv:
  2444   fixes w w' :: "'a::len0 word"
  2445   shows "(w = w OR w') = (w' = w AND w')"
  2446   by (auto intro: leoa leao)
  2447 
  2448 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  2449   unfolding word_le_def uint_or
  2450   by (auto intro: le_int_or) 
  2451 
  2452 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
  2453 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
  2454 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
  2455 
  2456 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 
  2457   unfolding to_bl_def word_log_defs bl_not_bin
  2458   by (simp add: word_ubin.eq_norm)
  2459 
  2460 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
  2461   unfolding to_bl_def word_log_defs bl_xor_bin
  2462   by (simp add: word_ubin.eq_norm)
  2463 
  2464 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
  2465   unfolding to_bl_def word_log_defs bl_or_bin
  2466   by (simp add: word_ubin.eq_norm)
  2467 
  2468 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
  2469   unfolding to_bl_def word_log_defs bl_and_bin
  2470   by (simp add: word_ubin.eq_norm)
  2471 
  2472 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
  2473   by (auto simp: word_test_bit_def word_lsb_def)
  2474 
  2475 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
  2476   unfolding word_lsb_def uint_eq_0 uint_1 by simp
  2477 
  2478 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
  2479   apply (unfold word_lsb_def uint_bl bin_to_bl_def) 
  2480   apply (rule_tac bin="uint w" in bin_exhaust)
  2481   apply (cases "size w")
  2482    apply auto
  2483    apply (auto simp add: bin_to_bl_aux_alt)
  2484   done
  2485 
  2486 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
  2487   unfolding word_lsb_def bin_last_def by auto
  2488 
  2489 lemma word_msb_sint: "msb w = (sint w < 0)" 
  2490   unfolding word_msb_def sign_Min_lt_0 ..
  2491 
  2492 lemma msb_word_of_int:
  2493   "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  2494   unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)
  2495 
  2496 lemma word_msb_numeral [simp]:
  2497   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  2498   unfolding word_numeral_alt by (rule msb_word_of_int)
  2499 
  2500 lemma word_msb_neg_numeral [simp]:
  2501   "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
  2502   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  2503 
  2504 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  2505   unfolding word_msb_def by simp
  2506 
  2507 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  2508   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  2509   by (simp add: Suc_le_eq)
  2510 
  2511 lemma word_msb_nth:
  2512   "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
  2513   unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
  2514 
  2515 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
  2516   apply (unfold word_msb_nth uint_bl)
  2517   apply (subst hd_conv_nth)
  2518   apply (rule length_greater_0_conv [THEN iffD1])
  2519    apply simp
  2520   apply (simp add : nth_bin_to_bl word_size)
  2521   done
  2522 
  2523 lemma word_set_nth [simp]:
  2524   "set_bit w n (test_bit w n) = (w::'a::len0 word)"
  2525   unfolding word_test_bit_def word_set_bit_def by auto
  2526 
  2527 lemma bin_nth_uint':
  2528   "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
  2529   apply (unfold word_size)
  2530   apply (safe elim!: bin_nth_uint_imp)
  2531    apply (frule bin_nth_uint_imp)
  2532    apply (fast dest!: bin_nth_bl)+
  2533   done
  2534 
  2535 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  2536 
  2537 lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
  2538   unfolding to_bl_def word_test_bit_def word_size
  2539   by (rule bin_nth_uint)
  2540 
  2541 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  2542   apply (unfold test_bit_bl)
  2543   apply clarsimp
  2544   apply (rule trans)
  2545    apply (rule nth_rev_alt)
  2546    apply (auto simp add: word_size)
  2547   done
  2548 
  2549 lemma test_bit_set: 
  2550   fixes w :: "'a::len0 word"
  2551   shows "(set_bit w n x) !! n = (n < size w & x)"
  2552   unfolding word_size word_test_bit_def word_set_bit_def
  2553   by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
  2554 
  2555 lemma test_bit_set_gen: 
  2556   fixes w :: "'a::len0 word"
  2557   shows "test_bit (set_bit w n x) m = 
  2558          (if m = n then n < size w & x else test_bit w m)"
  2559   apply (unfold word_size word_test_bit_def word_set_bit_def)
  2560   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  2561   apply (auto elim!: test_bit_size [unfolded word_size]
  2562               simp add: word_test_bit_def [symmetric])
  2563   done
  2564 
  2565 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  2566   unfolding of_bl_def bl_to_bin_rep_F by auto
  2567   
  2568 lemma msb_nth:
  2569   fixes w :: "'a::len word"
  2570   shows "msb w = w !! (len_of TYPE('a) - 1)"
  2571   unfolding word_msb_nth word_test_bit_def by simp
  2572 
  2573 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  2574 lemmas msb1 = msb0 [where i = 0]
  2575 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
  2576 
  2577 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
  2578 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  2579 
  2580 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  2581   "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 
  2582     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
  2583   apply (unfold word_size td_ext_def')
  2584   apply safe
  2585      apply (rule_tac [3] ext)
  2586      apply (rule_tac [4] ext)
  2587      apply (unfold word_size of_nth_def test_bit_bl)
  2588      apply safe
  2589        defer
  2590        apply (clarsimp simp: word_bl.Abs_inverse)+
  2591   apply (rule word_bl.Rep_inverse')
  2592   apply (rule sym [THEN trans])
  2593   apply (rule bl_of_nth_nth)
  2594   apply simp
  2595   apply (rule bl_of_nth_inj)
  2596   apply (clarsimp simp add : test_bit_bl word_size)
  2597   done
  2598 
  2599 interpretation test_bit:
  2600   td_ext "op !! :: 'a::len0 word => nat => bool"
  2601          set_bits
  2602          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  2603          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  2604   by (rule td_ext_nth)
  2605 
  2606 lemmas td_nth = test_bit.td_thm
  2607 
  2608 lemma word_set_set_same [simp]:
  2609   fixes w :: "'a::len0 word"
  2610   shows "set_bit (set_bit w n x) n y = set_bit w n y" 
  2611   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  2612     
  2613 lemma word_set_set_diff: 
  2614   fixes w :: "'a::len0 word"
  2615   assumes "m ~= n"
  2616   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
  2617   by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
  2618 
  2619 lemma nth_sint: 
  2620   fixes w :: "'a::len word"
  2621   defines "l \<equiv> len_of TYPE ('a)"
  2622   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  2623   unfolding sint_uint l_def
  2624   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
  2625 
  2626 lemma word_lsb_numeral [simp]:
  2627   "lsb (numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (numeral bin)"
  2628   unfolding word_lsb_alt test_bit_numeral by simp
  2629 
  2630 lemma word_lsb_neg_numeral [simp]:
  2631   "lsb (- numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (- numeral bin)"
  2632   unfolding word_lsb_alt test_bit_neg_numeral by simp
  2633 
  2634 lemma set_bit_word_of_int:
  2635   "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  2636   unfolding word_set_bit_def
  2637   apply (rule word_eqI)
  2638   apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  2639   done
  2640 
  2641 lemma word_set_numeral [simp]:
  2642   "set_bit (numeral bin::'a::len0 word) n b = 
  2643     word_of_int (bin_sc n b (numeral bin))"
  2644   unfolding word_numeral_alt by (rule set_bit_word_of_int)
  2645 
  2646 lemma word_set_neg_numeral [simp]:
  2647   "set_bit (- numeral bin::'a::len0 word) n b = 
  2648     word_of_int (bin_sc n b (- numeral bin))"
  2649   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  2650 
  2651 lemma word_set_bit_0 [simp]:
  2652   "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  2653   unfolding word_0_wi by (rule set_bit_word_of_int)
  2654 
  2655 lemma word_set_bit_1 [simp]:
  2656   "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  2657   unfolding word_1_wi by (rule set_bit_word_of_int)
  2658 
  2659 lemma setBit_no [simp]:
  2660   "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  2661   by (simp add: setBit_def)
  2662 
  2663 lemma clearBit_no [simp]:
  2664   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
  2665   by (simp add: clearBit_def)
  2666 
  2667 lemma to_bl_n1: 
  2668   "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
  2669   apply (rule word_bl.Abs_inverse')
  2670    apply simp
  2671   apply (rule word_eqI)
  2672   apply (clarsimp simp add: word_size)
  2673   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
  2674   done
  2675 
  2676 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  2677   unfolding word_msb_alt to_bl_n1 by simp
  2678 
  2679 lemma word_set_nth_iff: 
  2680   "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
  2681   apply (rule iffI)
  2682    apply (rule disjCI)
  2683    apply (drule word_eqD)
  2684    apply (erule sym [THEN trans])
  2685    apply (simp add: test_bit_set)
  2686   apply (erule disjE)
  2687    apply clarsimp
  2688   apply (rule word_eqI)
  2689   apply (clarsimp simp add : test_bit_set_gen)
  2690   apply (drule test_bit_size)
  2691   apply force
  2692   done
  2693 
  2694 lemma test_bit_2p:
  2695   "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  2696   unfolding word_test_bit_def
  2697   by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
  2698 
  2699 lemma nth_w2p:
  2700   "((2::'a::len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a::len)"
  2701   unfolding test_bit_2p [symmetric] word_of_int [symmetric]
  2702   by (simp add:  of_int_power)
  2703 
  2704 lemma uint_2p: 
  2705   "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  2706   apply (unfold word_arith_power_alt)
  2707   apply (case_tac "len_of TYPE ('a)")
  2708    apply clarsimp
  2709   apply (case_tac "nat")
  2710    apply clarsimp
  2711    apply (case_tac "n")
  2712     apply clarsimp
  2713    apply clarsimp
  2714   apply (drule word_gt_0 [THEN iffD1])
  2715   apply (safe intro!: word_eqI)
  2716   apply (auto simp add: nth_2p_bin)
  2717   apply (erule notE)
  2718   apply (simp (no_asm_use) add: uint_word_of_int word_size)
  2719   apply (subst mod_pos_pos_trivial)
  2720   apply simp
  2721   apply (rule power_strict_increasing)
  2722   apply simp_all
  2723   done
  2724 
  2725 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
  2726   apply (unfold word_arith_power_alt)
  2727   apply (case_tac "len_of TYPE ('a)")
  2728    apply clarsimp
  2729   apply (case_tac "nat")
  2730    apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
  2731    apply (rule box_equals) 
  2732      apply (rule_tac [2] bintr_ariths (1))+ 
  2733    apply simp
  2734   apply simp
  2735   done
  2736 
  2737 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
  2738   apply (rule xtr3) 
  2739   apply (rule_tac [2] y = "x" in le_word_or2)
  2740   apply (rule word_eqI)
  2741   apply (auto simp add: word_ao_nth nth_w2p word_size)
  2742   done
  2743 
  2744 lemma word_clr_le: 
  2745   fixes w :: "'a::len0 word"
  2746   shows "w >= set_bit w n False"
  2747   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2748   apply (rule order_trans)
  2749    apply (rule bintr_bin_clr_le)
  2750   apply simp
  2751   done
  2752 
  2753 lemma word_set_ge: 
  2754   fixes w :: "'a::len word"
  2755   shows "w <= set_bit w n True"
  2756   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2757   apply (rule order_trans [OF _ bintr_bin_set_ge])
  2758   apply simp
  2759   done
  2760 
  2761 
  2762 subsection {* Shifting, Rotating, and Splitting Words *}
  2763 
  2764 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
  2765   unfolding shiftl1_def
  2766   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
  2767   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
  2768   apply (subst bintrunc_bintrunc_min)
  2769   apply simp
  2770   done
  2771 
  2772 lemma shiftl1_numeral [simp]:
  2773   "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  2774   unfolding word_numeral_alt shiftl1_wi by simp
  2775 
  2776 lemma shiftl1_neg_numeral [simp]:
  2777   "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  2778   unfolding word_neg_numeral_alt shiftl1_wi by simp
  2779 
  2780 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  2781   unfolding shiftl1_def by simp
  2782 
  2783 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
  2784   by (simp only: shiftl1_def) (* FIXME: duplicate *)
  2785 
  2786 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
  2787   unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
  2788 
  2789 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  2790   unfolding shiftr1_def by simp
  2791 
  2792 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  2793   unfolding sshiftr1_def by simp
  2794 
  2795 lemma sshiftr1_n1 [simp] : "sshiftr1 (- 1) = - 1"
  2796   unfolding sshiftr1_def by simp
  2797 
  2798 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
  2799   unfolding shiftl_def by (induct n) auto
  2800 
  2801 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
  2802   unfolding shiftr_def by (induct n) auto
  2803 
  2804 lemma sshiftr_0 [simp] : "0 >>> n = 0"
  2805   unfolding sshiftr_def by (induct n) auto
  2806 
  2807 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
  2808   unfolding sshiftr_def by (induct n) auto
  2809 
  2810 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
  2811   apply (unfold shiftl1_def word_test_bit_def)
  2812   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  2813   apply (cases n)
  2814    apply auto
  2815   done
  2816 
  2817 lemma nth_shiftl' [rule_format]:
  2818   "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
  2819   apply (unfold shiftl_def)
  2820   apply (induct "m")
  2821    apply (force elim!: test_bit_size)
  2822   apply (clarsimp simp add : nth_shiftl1 word_size)
  2823   apply arith
  2824   done
  2825 
  2826 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
  2827 
  2828 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  2829   apply (unfold shiftr1_def word_test_bit_def)
  2830   apply (simp add: nth_bintr word_ubin.eq_norm)
  2831   apply safe
  2832   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
  2833   apply simp
  2834   done
  2835 
  2836 lemma nth_shiftr: 
  2837   "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
  2838   apply (unfold shiftr_def)
  2839   apply (induct "m")
  2840    apply (auto simp add : nth_shiftr1)
  2841   done
  2842    
  2843 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  2844   where f (ie bin_rest) takes normal arguments to normal results,
  2845   thus we get (2) from (1) *)
  2846 
  2847 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
  2848   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  2849   apply (subst bintr_uint [symmetric, OF order_refl])
  2850   apply (simp only : bintrunc_bintrunc_l)
  2851   apply simp 
  2852   done
  2853 
  2854 lemma nth_sshiftr1: 
  2855   "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  2856   apply (unfold sshiftr1_def word_test_bit_def)
  2857   apply (simp add: nth_bintr word_ubin.eq_norm
  2858                    bin_nth.Suc [symmetric] word_size 
  2859              del: bin_nth.simps)
  2860   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  2861   apply (auto simp add: bin_nth_sint)
  2862   done
  2863 
  2864 lemma nth_sshiftr [rule_format] : 
  2865   "ALL n. sshiftr w m !! n = (n < size w & 
  2866     (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
  2867   apply (unfold sshiftr_def)
  2868   apply (induct_tac "m")
  2869    apply (simp add: test_bit_bl)
  2870   apply (clarsimp simp add: nth_sshiftr1 word_size)
  2871   apply safe
  2872        apply arith
  2873       apply arith
  2874      apply (erule thin_rl)
  2875      apply (case_tac n)
  2876       apply safe
  2877       apply simp
  2878      apply simp
  2879     apply (erule thin_rl)
  2880     apply (case_tac n)
  2881      apply safe
  2882      apply simp
  2883     apply simp
  2884    apply arith+
  2885   done
  2886     
  2887 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
  2888   apply (unfold shiftr1_def bin_rest_def)
  2889   apply (rule word_uint.Abs_inverse)
  2890   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
  2891   apply (rule xtr7)
  2892    prefer 2
  2893    apply (rule zdiv_le_dividend)
  2894     apply auto
  2895   done
  2896 
  2897 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
  2898   apply (unfold sshiftr1_def bin_rest_def [symmetric])
  2899   apply (simp add: word_sbin.eq_norm)
  2900   apply (rule trans)
  2901    defer
  2902    apply (subst word_sbin.norm_Rep [symmetric])
  2903    apply (rule refl)
  2904   apply (subst word_sbin.norm_Rep [symmetric])
  2905   apply (unfold One_nat_def)
  2906   apply (rule sbintrunc_rest)
  2907   done
  2908 
  2909 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  2910   apply (unfold shiftr_def)
  2911   apply (induct "n")
  2912    apply simp
  2913   apply (simp add: shiftr1_div_2 mult.commute
  2914                    zdiv_zmult2_eq [symmetric])
  2915   done
  2916 
  2917 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  2918   apply (unfold sshiftr_def)
  2919   apply (induct "n")
  2920    apply simp
  2921   apply (simp add: sshiftr1_div_2 mult.commute
  2922                    zdiv_zmult2_eq [symmetric])
  2923   done
  2924 
  2925 
  2926 subsubsection {* shift functions in terms of lists of bools *}
  2927 
  2928 lemmas bshiftr1_numeral [simp] = 
  2929   bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
  2930 
  2931 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
  2932   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
  2933 
  2934 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
  2935   by (simp add: of_bl_def bl_to_bin_append)
  2936 
  2937 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
  2938 proof -
  2939   have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
  2940   also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
  2941   finally show ?thesis .
  2942 qed
  2943 
  2944 lemma bl_shiftl1:
  2945   "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
  2946   apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
  2947   apply (fast intro!: Suc_leI)
  2948   done
  2949 
  2950 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  2951 lemma bl_shiftl1':
  2952   "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  2953   unfolding shiftl1_bl
  2954   by (simp add: word_rep_drop drop_Suc del: drop_append)
  2955 
  2956 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  2957   apply (unfold shiftr1_def uint_bl of_bl_def)
  2958   apply (simp add: butlast_rest_bin word_size)
  2959   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  2960   done
  2961 
  2962 lemma bl_shiftr1: 
  2963   "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
  2964   unfolding shiftr1_bl
  2965   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
  2966 
  2967 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  2968 lemma bl_shiftr1':
  2969   "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  2970   apply (rule word_bl.Abs_inverse')
  2971   apply (simp del: butlast.simps)
  2972   apply (simp add: shiftr1_bl of_bl_def)
  2973   done
  2974 
  2975 lemma shiftl1_rev: 
  2976   "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  2977   apply (unfold word_reverse_def)
  2978   apply (rule word_bl.Rep_inverse' [symmetric])
  2979   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  2980   apply (cases "to_bl w")
  2981    apply auto
  2982   done
  2983 
  2984 lemma shiftl_rev: 
  2985   "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  2986   apply (unfold shiftl_def shiftr_def)
  2987   apply (induct "n")
  2988    apply (auto simp add : shiftl1_rev)
  2989   done
  2990 
  2991 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  2992   by (simp add: shiftl_rev)
  2993 
  2994 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  2995   by (simp add: rev_shiftl)
  2996 
  2997 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  2998   by (simp add: shiftr_rev)
  2999 
  3000 lemma bl_sshiftr1:
  3001   "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
  3002   apply (unfold sshiftr1_def uint_bl word_size)
  3003   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  3004   apply (simp add: sint_uint)
  3005   apply (rule nth_equalityI)
  3006    apply clarsimp
  3007   apply clarsimp
  3008   apply (case_tac i)
  3009    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  3010                         nth_bin_to_bl bin_nth.Suc [symmetric] 
  3011                         nth_sbintr 
  3012                    del: bin_nth.Suc)
  3013    apply force
  3014   apply (rule impI)
  3015   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  3016   apply simp
  3017   done
  3018 
  3019 lemma drop_shiftr: 
  3020   "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
  3021   apply (unfold shiftr_def)
  3022   apply (induct n)
  3023    prefer 2
  3024    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  3025    apply (rule butlast_take [THEN trans])
  3026   apply (auto simp: word_size)
  3027   done
  3028 
  3029 lemma drop_sshiftr: 
  3030   "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
  3031   apply (unfold sshiftr_def)
  3032   apply (induct n)
  3033    prefer 2
  3034    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  3035    apply (rule butlast_take [THEN trans])
  3036   apply (auto simp: word_size)
  3037   done
  3038 
  3039 lemma take_shiftr:
  3040   "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  3041   apply (unfold shiftr_def)
  3042   apply (induct n)
  3043    prefer 2
  3044    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  3045    apply (rule take_butlast [THEN trans])
  3046   apply (auto simp: word_size)
  3047   done
  3048 
  3049 lemma take_sshiftr' [rule_format] :
  3050   "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
  3051     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
  3052   apply (unfold sshiftr_def)
  3053   apply (induct n)
  3054    prefer 2
  3055    apply (simp add: bl_sshiftr1)
  3056    apply (rule impI)
  3057    apply (rule take_butlast [THEN trans])
  3058   apply (auto simp: word_size)
  3059   done
  3060 
  3061 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  3062 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
  3063 
  3064 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
  3065   by (auto intro: append_take_drop_id [symmetric])
  3066 
  3067 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
  3068 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  3069 
  3070 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  3071   unfolding shiftl_def
  3072   by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
  3073 
  3074 lemma shiftl_bl:
  3075   "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
  3076 proof -
  3077   have "w << n = of_bl (to_bl w) << n" by simp
  3078   also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
  3079   finally show ?thesis .
  3080 qed
  3081 
  3082 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  3083 
  3084 lemma bl_shiftl:
  3085   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  3086   by (simp add: shiftl_bl word_rep_drop word_size)
  3087 
  3088 lemma shiftl_zero_size: 
  3089   fixes x :: "'a::len0 word"
  3090   shows "size x <= n \<Longrightarrow> x << n = 0"
  3091   apply (unfold word_size)
  3092   apply (rule word_eqI)
  3093   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  3094   done
  3095 
  3096 (* note - the following results use 'a :: len word < number_ring *)
  3097 
  3098 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
  3099   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  3100 
  3101 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
  3102   by (simp add: shiftl1_2t)
  3103 
  3104 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
  3105   unfolding shiftl_def 
  3106   by (induct n) (auto simp: shiftl1_2t)
  3107 
  3108 lemma shiftr1_bintr [simp]:
  3109   "(shiftr1 (numeral w) :: 'a :: len0 word) =
  3110     word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (numeral w)))"
  3111   unfolding shiftr1_def word_numeral_alt
  3112   by (simp add: word_ubin.eq_norm)
  3113 
  3114 lemma sshiftr1_sbintr [simp]:
  3115   "(sshiftr1 (numeral w) :: 'a :: len word) =
  3116     word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (numeral w)))"
  3117   unfolding sshiftr1_def word_numeral_alt
  3118   by (simp add: word_sbin.eq_norm)
  3119 
  3120 lemma shiftr_no [simp]:
  3121   (* FIXME: neg_numeral *)
  3122   "(numeral w::'a::len0 word) >> n = word_of_int
  3123     ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  3124   apply (rule word_eqI)
  3125   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  3126   done
  3127 
  3128 lemma sshiftr_no [simp]:
  3129   (* FIXME: neg_numeral *)
  3130   "(numeral w::'a::len word) >>> n = word_of_int
  3131     ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  3132   apply (rule word_eqI)
  3133   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
  3134    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
  3135   done
  3136 
  3137 lemma shiftr1_bl_of:
  3138   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3139     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  3140   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin 
  3141                      word_ubin.eq_norm trunc_bl2bin)
  3142 
  3143 lemma shiftr_bl_of:
  3144   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3145     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
  3146   apply (unfold shiftr_def)
  3147   apply (induct n)
  3148    apply clarsimp
  3149   apply clarsimp
  3150   apply (subst shiftr1_bl_of)
  3151    apply simp
  3152   apply (simp add: butlast_take)
  3153   done
  3154 
  3155 lemma shiftr_bl:
  3156   "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  3157   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  3158 
  3159 lemma msb_shift:
  3160   "msb (w::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
  3161   apply (unfold shiftr_bl word_msb_alt)
  3162   apply (simp add: word_size Suc_le_eq take_Suc)
  3163   apply (cases "hd (to_bl w)")
  3164    apply (auto simp: word_1_bl
  3165                      of_bl_rep_False [where n=1 and bs="[]", simplified])
  3166   done
  3167 
  3168 lemma zip_replicate:
  3169   "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys" 
  3170   apply (induct ys arbitrary: n, simp_all)
  3171   apply (case_tac n, simp_all)
  3172   done
  3173 
  3174 lemma align_lem_or [rule_format] :
  3175   "ALL x m. length x = n + m --> length y = n + m --> 
  3176     drop m x = replicate n False --> take m y = replicate m False --> 
  3177     map2 op | x y = take m x @ drop m y"
  3178   apply (induct_tac y)
  3179    apply force
  3180   apply clarsimp
  3181   apply (case_tac x, force)
  3182   apply (case_tac m, auto)
  3183   apply (drule_tac t="length xs" for xs in sym)
  3184   apply (clarsimp simp: map2_def zip_replicate o_def)
  3185   done
  3186 
  3187 lemma align_lem_and [rule_format] :
  3188   "ALL x m. length x = n + m --> length y = n + m --> 
  3189     drop m x = replicate n False --> take m y = replicate m False --> 
  3190     map2 op & x y = replicate (n + m) False"
  3191   apply (induct_tac y)
  3192    apply force
  3193   apply clarsimp
  3194   apply (case_tac x, force)
  3195   apply (case_tac m, auto)
  3196   apply (drule_tac t="length xs" for xs in sym)
  3197   apply (clarsimp simp: map2_def zip_replicate o_def map_replicate_const)
  3198   done
  3199 
  3200 lemma aligned_bl_add_size [OF refl]:
  3201   "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  3202     take m (to_bl y) = replicate m False \<Longrightarrow> 
  3203     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  3204   apply (subgoal_tac "x AND y = 0")
  3205    prefer 2
  3206    apply (rule word_bl.Rep_eqD)
  3207    apply (simp add: bl_word_and)
  3208    apply (rule align_lem_and [THEN trans])
  3209        apply (simp_all add: word_size)[5]
  3210    apply simp
  3211   apply (subst word_plus_and_or [symmetric])
  3212   apply (simp add : bl_word_or)
  3213   apply (rule align_lem_or)
  3214      apply (simp_all add: word_size)
  3215   done
  3216 
  3217 
  3218 subsubsection {* Mask *}
  3219 
  3220 lemma nth_mask [OF refl, simp]:
  3221   "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
  3222   apply (unfold mask_def test_bit_bl)
  3223   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  3224   apply (clarsimp simp add: word_size)
  3225   apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
  3226   apply (fold of_bl_def)
  3227   apply (simp add: word_1_bl)
  3228   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
  3229   apply auto
  3230   done
  3231 
  3232 lemma mask_bl: "mask n = of_bl (replicate n True)"
  3233   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
  3234 
  3235 lemma mask_bin: "mask n = word_of_int (bintrunc n (- 1))"
  3236   by (auto simp add: nth_bintr word_size intro: word_eqI)
  3237 
  3238 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
  3239   apply (rule word_eqI)
  3240   apply (simp add: nth_bintr word_size word_ops_nth_size)
  3241   apply (auto simp add: test_bit_bin)
  3242   done
  3243 
  3244 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  3245   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3246 
  3247 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  3248   unfolding word_numeral_alt by (rule and_mask_wi)
  3249 
  3250 lemma bl_and_mask':
  3251   "to_bl (w AND mask n :: 'a :: len word) = 
  3252     replicate (len_of TYPE('a) - n) False @ 
  3253     drop (len_of TYPE('a) - n) (to_bl w)"
  3254   apply (rule nth_equalityI)
  3255    apply simp
  3256   apply (clarsimp simp add: to_bl_nth word_size)
  3257   apply (simp add: word_size word_ops_nth_size)
  3258   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
  3259   done
  3260 
  3261 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
  3262   by (simp only: and_mask_bintr bintrunc_mod2p)
  3263 
  3264 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
  3265   apply (simp add: and_mask_bintr word_ubin.eq_norm)
  3266   apply (simp add: bintrunc_mod2p)
  3267   apply (rule xtr8)
  3268    prefer 2
  3269    apply (rule pos_mod_bound)
  3270   apply auto
  3271   done
  3272 
  3273 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  3274   by (simp add: int_mod_lem eq_sym_conv)
  3275 
  3276 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
  3277   apply (simp add: and_mask_bintr)
  3278   apply (simp add: word_ubin.inverse_norm)
  3279   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
  3280   apply (fast intro!: lt2p_lem)
  3281   done
  3282 
  3283 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
  3284   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  3285   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
  3286     del: word_of_int_0)
  3287   apply (subst word_uint.norm_Rep [symmetric])
  3288   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  3289   apply auto
  3290   done
  3291 
  3292 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
  3293   apply (unfold unat_def)
  3294   apply (rule trans [OF _ and_mask_dvd])
  3295   apply (unfold dvd_def) 
  3296   apply auto 
  3297   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  3298   apply (simp add : int_mult of_nat_power)
  3299   apply (simp add : nat_mult_distrib nat_power_eq)
  3300   done
  3301 
  3302 lemma word_2p_lem: 
  3303   "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
  3304   apply (unfold word_size word_less_alt word_numeral_alt)
  3305   apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
  3306                             mod_pos_pos_trivial
  3307                   simp del: word_of_int_numeral)
  3308   done
  3309 
  3310 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
  3311   apply (unfold word_less_alt word_numeral_alt)
  3312   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
  3313                             word_uint.eq_norm
  3314                   simp del: word_of_int_numeral)
  3315   apply (drule xtr8 [rotated])
  3316   apply (rule int_mod_le)
  3317   apply (auto simp add : mod_pos_pos_trivial)
  3318   done
  3319 
  3320 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  3321 
  3322 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
  3323 
  3324 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  3325   unfolding word_size by (erule and_mask_less')
  3326 
  3327 lemma word_mod_2p_is_mask [OF refl]:
  3328   "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n" 
  3329   by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
  3330 
  3331 lemma mask_eqs:
  3332   "(a AND mask n) + b AND mask n = a + b AND mask n"
  3333   "a + (b AND mask n) AND mask n = a + b AND mask n"
  3334   "(a AND mask n) - b AND mask n = a - b AND mask n"
  3335   "a - (b AND mask n) AND mask n = a - b AND mask n"
  3336   "a * (b AND mask n) AND mask n = a * b AND mask n"
  3337   "(b AND mask n) * a AND mask n = b * a AND mask n"
  3338   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
  3339   "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
  3340   "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
  3341   "- (a AND mask n) AND mask n = - a AND mask n"
  3342   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  3343   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  3344   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  3345   by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
  3346 
  3347 lemma mask_power_eq:
  3348   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  3349   using word_of_int_Ex [where x=x]
  3350   by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
  3351 
  3352 
  3353 subsubsection {* Revcast *}
  3354 
  3355 lemmas revcast_def' = revcast_def [simplified]
  3356 lemmas revcast_def'' = revcast_def' [simplified word_size]
  3357 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  3358 
  3359 lemma to_bl_revcast: 
  3360   "to_bl (revcast w :: 'a :: len0 word) = 
  3361    takefill False (len_of TYPE ('a)) (to_bl w)"
  3362   apply (unfold revcast_def' word_size)
  3363   apply (rule word_bl.Abs_inverse)
  3364   apply simp
  3365   done
  3366 
  3367 lemma revcast_rev_ucast [OF refl refl refl]: 
  3368   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 
  3369     rc = word_reverse uc"
  3370   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  3371   apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
  3372   apply (simp add : word_bl.Abs_inverse word_size)
  3373   done
  3374 
  3375 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  3376   using revcast_rev_ucast [of "word_reverse w"] by simp
  3377 
  3378 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
  3379   by (fact revcast_rev_ucast [THEN word_rev_gal'])
  3380 
  3381 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
  3382   by (fact revcast_ucast [THEN word_rev_gal'])
  3383 
  3384 
  3385 -- "linking revcast and cast via shift"
  3386 
  3387 lemmas wsst_TYs = source_size target_size word_size
  3388 
  3389 lemma revcast_down_uu [OF refl]:
  3390   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3391     rc (w :: 'a :: len word) = ucast (w >> n)"
  3392   apply (simp add: revcast_def')
  3393   apply (rule word_bl.Rep_inverse')
  3394   apply (rule trans, rule ucast_down_drop)
  3395    prefer 2
  3396    apply (rule trans, rule drop_shiftr)
  3397    apply (auto simp: takefill_alt wsst_TYs)
  3398   done
  3399 
  3400 lemma revcast_down_us [OF refl]:
  3401   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3402     rc (w :: 'a :: len word) = ucast (w >>> n)"
  3403   apply (simp add: revcast_def')
  3404   apply (rule word_bl.Rep_inverse')
  3405   apply (rule trans, rule ucast_down_drop)
  3406    prefer 2
  3407    apply (rule trans, rule drop_sshiftr)
  3408    apply (auto simp: takefill_alt wsst_TYs)
  3409   done
  3410 
  3411 lemma revcast_down_su [OF refl]:
  3412   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3413     rc (w :: 'a :: len word) = scast (w >> n)"
  3414   apply (simp add: revcast_def')
  3415   apply (rule word_bl.Rep_inverse')
  3416   apply (rule trans, rule scast_down_drop)
  3417    prefer 2
  3418    apply (rule trans, rule drop_shiftr)
  3419    apply (auto simp: takefill_alt wsst_TYs)
  3420   done
  3421 
  3422 lemma revcast_down_ss [OF refl]:
  3423   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3424     rc (w :: 'a :: len word) = scast (w >>> n)"
  3425   apply (simp add: revcast_def')
  3426   apply (rule word_bl.Rep_inverse')
  3427   apply (rule trans, rule scast_down_drop)
  3428    prefer 2
  3429    apply (rule trans, rule drop_sshiftr)
  3430    apply (auto simp: takefill_alt wsst_TYs)
  3431   done
  3432 
  3433 (* FIXME: should this also be [OF refl] ? *)
  3434 lemma cast_down_rev: 
  3435   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
  3436     uc w = revcast ((w :: 'a :: len word) << n)"
  3437   apply (unfold shiftl_rev)
  3438   apply clarify
  3439   apply (simp add: revcast_rev_ucast)
  3440   apply (rule word_rev_gal')
  3441   apply (rule trans [OF _ revcast_rev_ucast])
  3442   apply (rule revcast_down_uu [symmetric])
  3443   apply (auto simp add: wsst_TYs)
  3444   done
  3445 
  3446 lemma revcast_up [OF refl]:
  3447   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 
  3448     rc w = (ucast w :: 'a :: len word) << n" 
  3449   apply (simp add: revcast_def')
  3450   apply (rule word_bl.Rep_inverse')
  3451   apply (simp add: takefill_alt)
  3452   apply (rule bl_shiftl [THEN trans])
  3453   apply (subst ucast_up_app)
  3454   apply (auto simp add: wsst_TYs)
  3455   done
  3456 
  3457 lemmas rc1 = revcast_up [THEN 
  3458   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3459 lemmas rc2 = revcast_down_uu [THEN 
  3460   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3461 
  3462 lemmas ucast_up =
  3463  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
  3464 lemmas ucast_down = 
  3465   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
  3466 
  3467 
  3468 subsubsection {* Slices *}
  3469 
  3470 lemma slice1_no_bin [simp]:
  3471   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3472   by (simp add: slice1_def) (* TODO: neg_numeral *)
  3473 
  3474 lemma slice_no_bin [simp]:
  3475   "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
  3476     (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3477   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
  3478 
  3479 lemma slice1_0 [simp] : "slice1 n 0 = 0"
  3480   unfolding slice1_def by simp
  3481 
  3482 lemma slice_0 [simp] : "slice n 0 = 0"
  3483   unfolding slice_def by auto
  3484 
  3485 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
  3486   unfolding slice_def' slice1_def
  3487   by (simp add : takefill_alt word_size)
  3488 
  3489 lemmas slice_take = slice_take' [unfolded word_size]
  3490 
  3491 -- "shiftr to a word of the same size is just slice, 
  3492     slice is just shiftr then ucast"
  3493 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
  3494 
  3495 lemma slice_shiftr: "slice n w = ucast (w >> n)"
  3496   apply (unfold slice_take shiftr_bl)
  3497   apply (rule ucast_of_bl_up [symmetric])
  3498   apply (simp add: word_size)
  3499   done
  3500 
  3501 lemma nth_slice: 
  3502   "(slice n w :: 'a :: len0 word) !! m = 
  3503    (w !! (m + n) & m < len_of TYPE ('a))"
  3504   unfolding slice_shiftr 
  3505   by (simp add : nth_ucast nth_shiftr)
  3506 
  3507 lemma slice1_down_alt': 
  3508   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 
  3509     to_bl sl = takefill False fs (drop k (to_bl w))"
  3510   unfolding slice1_def word_size of_bl_def uint_bl
  3511   by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  3512 
  3513 lemma slice1_up_alt': 
  3514   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 
  3515     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  3516   apply (unfold slice1_def word_size of_bl_def uint_bl)
  3517   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
  3518                         takefill_append [symmetric])
  3519   apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
  3520     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
  3521   apply arith
  3522   done
  3523     
  3524 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
  3525 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
  3526 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
  3527 lemmas slice1_up_alts = 
  3528   le_add_diff_inverse [symmetric, THEN su1] 
  3529   le_add_diff_inverse2 [symmetric, THEN su1]
  3530 
  3531 lemma ucast_slice1: "ucast w = slice1 (size w) w"
  3532   unfolding slice1_def ucast_bl
  3533   by (simp add : takefill_same' word_size)
  3534 
  3535 lemma ucast_slice: "ucast w = slice 0 w"
  3536   unfolding slice_def by (simp add : ucast_slice1)
  3537 
  3538 lemma slice_id: "slice 0 t = t"
  3539   by (simp only: ucast_slice [symmetric] ucast_id)
  3540 
  3541 lemma revcast_slice1 [OF refl]: 
  3542   "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  3543   unfolding slice1_def revcast_def' by (simp add : word_size)
  3544 
  3545 lemma slice1_tf_tf': 
  3546   "to_bl (slice1 n w :: 'a :: len0 word) = 
  3547    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
  3548   unfolding slice1_def by (rule word_rev_tf)
  3549 
  3550 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
  3551 
  3552 lemma rev_slice1:
  3553   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
  3554   slice1 n (word_reverse w :: 'b :: len0 word) = 
  3555   word_reverse (slice1 k w :: 'a :: len0 word)"
  3556   apply (unfold word_reverse_def slice1_tf_tf)
  3557   apply (rule word_bl.Rep_inverse')
  3558   apply (rule rev_swap [THEN iffD1])
  3559   apply (rule trans [symmetric])
  3560   apply (rule tf_rev)
  3561    apply (simp add: word_bl.Abs_inverse)
  3562   apply (simp add: word_bl.Abs_inverse)
  3563   done
  3564 
  3565 lemma rev_slice:
  3566   "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
  3567     slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
  3568   apply (unfold slice_def word_size)
  3569   apply (rule rev_slice1)
  3570   apply arith
  3571   done
  3572 
  3573 lemmas sym_notr = 
  3574   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
  3575 
  3576 -- {* problem posed by TPHOLs referee:
  3577       criterion for overflow of addition of signed integers *}
  3578 
  3579 lemma sofl_test:
  3580   "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
  3581      ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
  3582   apply (unfold word_size)
  3583   apply (cases "len_of TYPE('a)", simp) 
  3584   apply (subst msb_shift [THEN sym_notr])
  3585   apply (simp add: word_ops_msb)
  3586   apply (simp add: word_msb_sint)
  3587   apply safe
  3588        apply simp_all
  3589      apply (unfold sint_word_ariths)
  3590      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
  3591      apply safe
  3592         apply (insert sint_range' [where x=x])
  3593         apply (insert sint_range' [where x=y])
  3594         defer 
  3595         apply (simp (no_asm), arith)
  3596        apply (simp (no_asm), arith)
  3597       defer
  3598       defer
  3599       apply (simp (no_asm), arith)
  3600      apply (simp (no_asm), arith)
  3601     apply (rule notI [THEN notnotD],
  3602            drule leI not_leE,
  3603            drule sbintrunc_inc sbintrunc_dec,      
  3604            simp)+
  3605   done
  3606 
  3607 
  3608 subsection {* Split and cat *}
  3609 
  3610 lemmas word_split_bin' = word_split_def
  3611 lemmas word_cat_bin' = word_cat_def
  3612 
  3613 lemma word_rsplit_no:
  3614   "(word_rsplit (numeral bin :: 'b :: len0 word) :: 'a word list) = 
  3615     map word_of_int (bin_rsplit (len_of TYPE('a :: len)) 
  3616       (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
  3617   unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
  3618 
  3619 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
  3620   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  3621 
  3622 lemma test_bit_cat:
  3623   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc & 
  3624     (if n < size b then b !! n else a !! (n - size b)))"
  3625   apply (unfold word_cat_bin' test_bit_bin)
  3626   apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  3627   apply (erule bin_nth_uint_imp)
  3628   done
  3629 
  3630 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
  3631   apply (unfold of_bl_def to_bl_def word_cat_bin')
  3632   apply (simp add: bl_to_bin_app_cat)
  3633   done
  3634 
  3635 lemma of_bl_append:
  3636   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
  3637   apply (unfold of_bl_def)
  3638   apply (simp add: bl_to_bin_app_cat bin_cat_num)
  3639   apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
  3640   done
  3641 
  3642 lemma of_bl_False [simp]:
  3643   "of_bl (False#xs) = of_bl xs"
  3644   by (rule word_eqI)
  3645      (auto simp add: test_bit_of_bl nth_append)
  3646 
  3647 lemma of_bl_True [simp]:
  3648   "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
  3649   by (subst of_bl_append [where xs="[True]", simplified])
  3650      (simp add: word_1_bl)
  3651 
  3652 lemma of_bl_Cons:
  3653   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  3654   by (cases x) simp_all
  3655 
  3656 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow> 
  3657   a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
  3658   apply (frule word_ubin.norm_Rep [THEN ssubst])
  3659   apply (drule bin_split_trunc1)
  3660   apply (drule sym [THEN trans])
  3661   apply assumption
  3662   apply safe
  3663   done
  3664 
  3665 lemma word_split_bl': 
  3666   "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 
  3667     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
  3668   apply (unfold word_split_bin')
  3669   apply safe
  3670    defer
  3671    apply (clarsimp split: prod.splits)
  3672    apply hypsubst_thin
  3673    apply (drule word_ubin.norm_Rep [THEN ssubst])
  3674    apply (drule split_bintrunc)
  3675    apply (simp add : of_bl_def bl2bin_drop word_size
  3676        word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
  3677   apply (clarsimp split: prod.splits)
  3678   apply (frule split_uint_lem [THEN conjunct1])
  3679   apply (unfold word_size)
  3680   apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
  3681    defer
  3682    apply simp
  3683   apply (simp add : of_bl_def to_bl_def)
  3684   apply (subst bin_split_take1 [symmetric])
  3685     prefer 2
  3686     apply assumption
  3687    apply simp
  3688   apply (erule thin_rl)
  3689   apply (erule arg_cong [THEN trans])
  3690   apply (simp add : word_ubin.norm_eq_iff [symmetric])
  3691   done
  3692 
  3693 lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
  3694     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
  3695     word_split c = (a, b)"
  3696   apply (rule iffI)
  3697    defer
  3698    apply (erule (1) word_split_bl')
  3699   apply (case_tac "word_split c")
  3700   apply (auto simp add : word_size)
  3701   apply (frule word_split_bl' [rotated])
  3702   apply (auto simp add : word_size)
  3703   done
  3704 
  3705 lemma word_split_bl_eq:
  3706    "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
  3707       (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
  3708        of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
  3709   apply (rule word_split_bl [THEN iffD1])
  3710   apply (unfold word_size)
  3711   apply (rule refl conjI)+
  3712   done
  3713 
  3714 -- "keep quantifiers for use in simplification"
  3715 lemma test_bit_split':
  3716   "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
  3717     a !! m = (m < size a & c !! (m + size b)))"
  3718   apply (unfold word_split_bin' test_bit_bin)
  3719   apply (clarify)
  3720   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
  3721   apply (drule bin_nth_split)
  3722   apply safe
  3723        apply (simp_all add: add.commute)
  3724    apply (erule bin_nth_uint_imp)+
  3725   done
  3726 
  3727 lemma test_bit_split:
  3728   "word_split c = (a, b) \<Longrightarrow>
  3729     (\<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))"
  3730   by (simp add: test_bit_split')
  3731 
  3732 lemma test_bit_split_eq: "word_split c = (a, b) <-> 
  3733   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
  3734     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
  3735   apply (rule_tac iffI)
  3736    apply (rule_tac conjI)
  3737     apply (erule test_bit_split [THEN conjunct1])
  3738    apply (erule test_bit_split [THEN conjunct2])
  3739   apply (case_tac "word_split c")
  3740   apply (frule test_bit_split)
  3741   apply (erule trans)
  3742   apply (fastforce intro ! : word_eqI simp add : word_size)
  3743   done
  3744 
  3745 -- {* this odd result is analogous to @{text "ucast_id"}, 
  3746       result to the length given by the result type *}
  3747 
  3748 lemma word_cat_id: "word_cat a b = b"
  3749   unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
  3750 
  3751 -- "limited hom result"
  3752 lemma word_cat_hom:
  3753   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  3754   \<Longrightarrow>
  3755   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
  3756   word_of_int (bin_cat w (size b) (uint b))"
  3757   apply (unfold word_cat_def word_size) 
  3758   apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
  3759       word_ubin.eq_norm bintr_cat min.absorb1)
  3760   done
  3761 
  3762 lemma word_cat_split_alt:
  3763   "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  3764   apply (rule word_eqI)
  3765   apply (drule test_bit_split)
  3766   apply (clarsimp simp add : test_bit_cat word_size)
  3767   apply safe
  3768   apply arith
  3769   done
  3770 
  3771 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
  3772 
  3773 
  3774 subsubsection {* Split and slice *}
  3775 
  3776 lemma split_slices: 
  3777   "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
  3778   apply (drule test_bit_split)
  3779   apply (rule conjI)
  3780    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  3781   done
  3782 
  3783 lemma slice_cat1 [OF refl]:
  3784   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  3785   apply safe
  3786   apply (rule word_eqI)
  3787   apply (simp add: nth_slice test_bit_cat word_size)
  3788   done
  3789 
  3790 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  3791 
  3792 lemma cat_slices:
  3793   "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  3794     size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  3795   apply safe
  3796   apply (rule word_eqI)
  3797   apply (simp add: nth_slice test_bit_cat word_size)
  3798   apply safe
  3799   apply arith
  3800   done
  3801 
  3802 lemma word_split_cat_alt:
  3803   "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
  3804   apply (case_tac "word_split w")
  3805   apply (rule trans, assumption)
  3806   apply (drule test_bit_split)
  3807   apply safe
  3808    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  3809   done
  3810 
  3811 lemmas word_cat_bl_no_bin [simp] =
  3812   word_cat_bl [where a="numeral a" and b="numeral b",
  3813     unfolded to_bl_numeral]
  3814   for a b (* FIXME: negative numerals, 0 and 1 *)
  3815 
  3816 lemmas word_split_bl_no_bin [simp] =
  3817   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
  3818 
  3819 text {* this odd result arises from the fact that the statement of the
  3820       result implies that the decoded words are of the same type, 
  3821       and therefore of the same length, as the original word *}
  3822 
  3823 lemma word_rsplit_same: "word_rsplit w = [w]"
  3824   unfolding word_rsplit_def by (simp add : bin_rsplit_all)
  3825 
  3826 lemma word_rsplit_empty_iff_size:
  3827   "(word_rsplit w = []) = (size w = 0)" 
  3828   unfolding word_rsplit_def bin_rsplit_def word_size
  3829   by (simp add: bin_rsplit_aux_simp_alt Let_def split: prod.split)
  3830 
  3831 lemma test_bit_rsplit:
  3832   "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
  3833     k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  3834   apply (unfold word_rsplit_def word_test_bit_def)
  3835   apply (rule trans)
  3836    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  3837    apply (rule nth_map [symmetric])
  3838    apply simp
  3839   apply (rule bin_nth_rsplit)
  3840      apply simp_all
  3841   apply (simp add : word_size rev_map)
  3842   apply (rule trans)
  3843    defer
  3844    apply (rule map_ident [THEN fun_cong])
  3845   apply (rule refl [THEN map_cong])
  3846   apply (simp add : word_ubin.eq_norm)
  3847   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  3848   done
  3849 
  3850 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  3851   unfolding word_rcat_def to_bl_def' of_bl_def
  3852   by (clarsimp simp add : bin_rcat_bl)
  3853 
  3854 lemma size_rcat_lem':
  3855   "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  3856   unfolding word_size by (induct wl) auto
  3857 
  3858 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  3859 
  3860 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
  3861 
  3862 lemma nth_rcat_lem:
  3863   "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
  3864     rev (concat (map to_bl wl)) ! n =
  3865     rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
  3866   apply (induct "wl")
  3867    apply clarsimp
  3868   apply (clarsimp simp add : nth_append size_rcat_lem)
  3869   apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
  3870          td_gal_lt_len less_Suc_eq_le mod_div_equality')
  3871   apply clarsimp
  3872   done
  3873 
  3874 lemma test_bit_rcat:
  3875   "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
  3876     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
  3877   apply (unfold word_rcat_bl word_size)
  3878   apply (clarsimp simp add : 
  3879     test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  3880   apply safe
  3881    apply (auto simp add : 
  3882     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  3883   done
  3884 
  3885 lemma foldl_eq_foldr:
  3886   "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
  3887   by (induct xs arbitrary: x) (auto simp add : add.assoc)
  3888 
  3889 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  3890 
  3891 lemmas test_bit_rsplit_alt = 
  3892   trans [OF nth_rev_alt [THEN test_bit_cong] 
  3893   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  3894 
  3895 -- "lazy way of expressing that u and v, and su and sv, have same types"
  3896 lemma word_rsplit_len_indep [OF refl refl refl refl]:
  3897   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
  3898     word_rsplit v = sv \<Longrightarrow> length su = length sv"
  3899   apply (unfold word_rsplit_def)
  3900   apply (auto simp add : bin_rsplit_len_indep)
  3901   done
  3902 
  3903 lemma length_word_rsplit_size: 
  3904   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3905     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
  3906   apply (unfold word_rsplit_def word_size)
  3907   apply (clarsimp simp add : bin_rsplit_len_le)
  3908   done
  3909 
  3910 lemmas length_word_rsplit_lt_size = 
  3911   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  3912 
  3913 lemma length_word_rsplit_exp_size:
  3914   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3915     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  3916   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
  3917 
  3918 lemma length_word_rsplit_even_size: 
  3919   "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow> 
  3920     length (word_rsplit w :: 'a word list) = m"
  3921   by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
  3922 
  3923 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  3924 
  3925 (* alternative proof of word_rcat_rsplit *)
  3926 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
  3927 lemmas dtle = xtr4 [OF tdle mult.commute]
  3928 
  3929 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  3930   apply (rule word_eqI)
  3931   apply (clarsimp simp add : test_bit_rcat word_size)
  3932   apply (subst refl [THEN test_bit_rsplit])
  3933     apply (simp_all add: word_size 
  3934       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  3935    apply safe
  3936    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  3937   done
  3938 
  3939 lemma size_word_rsplit_rcat_size:
  3940   "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
  3941      size frcw = length ws * len_of TYPE('a)\<rbrakk>
  3942     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  3943   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
  3944   apply (fast intro: given_quot_alt)
  3945   done
  3946 
  3947 lemma msrevs:
  3948   fixes n::nat
  3949   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  3950   and   "(k * n + m) mod n = m mod n"
  3951   by (auto simp: add.commute)
  3952 
  3953 lemma word_rsplit_rcat_size [OF refl]:
  3954   "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
  3955     size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
  3956   apply (frule size_word_rsplit_rcat_size, assumption)
  3957   apply (clarsimp simp add : word_size)
  3958   apply (rule nth_equalityI, assumption)
  3959   apply clarsimp
  3960   apply (rule word_eqI [rule_format])
  3961   apply (rule trans)
  3962    apply (rule test_bit_rsplit_alt)
  3963      apply (clarsimp simp: word_size)+
  3964   apply (rule trans)
  3965   apply (rule test_bit_rcat [OF refl refl])
  3966   apply (simp add: word_size)
  3967   apply (subst nth_rev)
  3968    apply arith
  3969   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3970   apply safe
  3971   apply (simp add: diff_mult_distrib)
  3972   apply (rule mpl_lem)
  3973   apply (cases "size ws")
  3974    apply simp_all
  3975   done
  3976 
  3977 
  3978 subsection {* Rotation *}
  3979 
  3980 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  3981 
  3982 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  3983 
  3984 lemma rotate_eq_mod: 
  3985   "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  3986   apply (rule box_equals)
  3987     defer
  3988     apply (rule rotate_conv_mod [symmetric])+
  3989   apply simp
  3990   done
  3991 
  3992 lemmas rotate_eqs = 
  3993   trans [OF rotate0 [THEN fun_cong] id_apply]
  3994   rotate_rotate [symmetric] 
  3995   rotate_id
  3996   rotate_conv_mod 
  3997   rotate_eq_mod
  3998 
  3999 
  4000 subsubsection {* Rotation of list to right *}
  4001 
  4002 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  4003   unfolding rotater1_def by (cases l) auto
  4004 
  4005 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  4006   apply (unfold rotater1_def)
  4007   apply (cases "l")
  4008   apply (case_tac [2] "list")
  4009   apply auto
  4010   done
  4011 
  4012 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  4013   unfolding rotater1_def by (cases l) auto
  4014 
  4015 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  4016   apply (cases "xs")
  4017   apply (simp add : rotater1_def)
  4018   apply (simp add : rotate1_rl')
  4019   done
  4020   
  4021 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  4022   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
  4023 
  4024 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
  4025   using rotater_rev' [where xs = "rev ys"] by simp
  4026 
  4027 lemma rotater_drop_take: 
  4028   "rotater n xs = 
  4029    drop (length xs - n mod length xs) xs @
  4030    take (length xs - n mod length xs) xs"
  4031   by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
  4032 
  4033 lemma rotater_Suc [simp] : 
  4034   "rotater (Suc n) xs = rotater1 (rotater n xs)"
  4035   unfolding rotater_def by auto
  4036 
  4037 lemma rotate_inv_plus [rule_format] :
  4038   "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs & 
  4039     rotate k (rotater n xs) = rotate m xs & 
  4040     rotater n (rotate k xs) = rotate m xs & 
  4041     rotate n (rotater k xs) = rotater m xs"
  4042   unfolding rotater_def rotate_def
  4043   by (induct n) (auto intro: funpow_swap1 [THEN trans])
  4044   
  4045 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  4046 
  4047 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  4048 
  4049 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
  4050 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
  4051 
  4052 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
  4053   by auto
  4054 
  4055 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
  4056   by auto
  4057 
  4058 lemma length_rotater [simp]: 
  4059   "length (rotater n xs) = length xs"
  4060   by (simp add : rotater_rev)
  4061 
  4062 lemma restrict_to_left:
  4063   assumes "x = y"
  4064   shows "(x = z) = (y = z)"
  4065   using assms by simp
  4066 
  4067 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
  4068   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
  4069 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  4070 lemmas rotater_eqs = rrs1 [simplified length_rotater]
  4071 lemmas rotater_0 = rotater_eqs (1)
  4072 lemmas rotater_add = rotater_eqs (2)
  4073 
  4074 
  4075 subsubsection {* map, map2, commuting with rotate(r) *}
  4076 
  4077 lemma butlast_map:
  4078   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  4079   by (induct xs) auto
  4080 
  4081 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
  4082   unfolding rotater1_def
  4083   by (cases xs) (auto simp add: last_map butlast_map)
  4084 
  4085 lemma rotater_map:
  4086   "rotater n (map f xs) = map f (rotater n xs)" 
  4087   unfolding rotater_def
  4088   by (induct n) (auto simp add : rotater1_map)
  4089 
  4090 lemma but_last_zip [rule_format] :
  4091   "ALL ys. length xs = length ys --> xs ~= [] --> 
  4092     last (zip xs ys) = (last xs, last ys) & 
  4093     butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 
  4094   apply (induct "xs")
  4095   apply auto
  4096      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  4097   done
  4098 
  4099 lemma but_last_map2 [rule_format] :
  4100   "ALL ys. length xs = length ys --> xs ~= [] --> 
  4101     last (map2 f xs ys) = f (last xs) (last ys) & 
  4102     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 
  4103   apply (induct "xs")
  4104   apply auto
  4105      apply (unfold map2_def)
  4106      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  4107   done
  4108 
  4109 lemma rotater1_zip:
  4110   "length xs = length ys \<Longrightarrow> 
  4111     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  4112   apply (unfold rotater1_def)
  4113   apply (cases "xs")
  4114    apply auto
  4115    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  4116   done
  4117 
  4118 lemma rotater1_map2:
  4119   "length xs = length ys \<Longrightarrow> 
  4120     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
  4121   unfolding map2_def by (simp add: rotater1_map rotater1_zip)
  4122 
  4123 lemmas lrth = 
  4124   box_equals [OF asm_rl length_rotater [symmetric] 
  4125                  length_rotater [symmetric], 
  4126               THEN rotater1_map2]
  4127 
  4128 lemma rotater_map2: 
  4129   "length xs = length ys \<Longrightarrow> 
  4130     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
  4131   by (induct n) (auto intro!: lrth)
  4132 
  4133 lemma rotate1_map2:
  4134   "length xs = length ys \<Longrightarrow> 
  4135     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  4136   apply (unfold map2_def)
  4137   apply (cases xs)
  4138    apply (cases ys, auto)+
  4139   done
  4140 
  4141 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
  4142   length_rotate [symmetric], THEN rotate1_map2]
  4143 
  4144 lemma rotate_map2: 
  4145   "length xs = length ys \<Longrightarrow> 
  4146     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
  4147   by (induct n) (auto intro!: lth)
  4148 
  4149 
  4150 -- "corresponding equalities for word rotation"
  4151 
  4152 lemma to_bl_rotl: 
  4153   "to_bl (word_rotl n w) = rotate n (to_bl w)"
  4154   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  4155 
  4156 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  4157 
  4158 lemmas word_rotl_eqs =
  4159   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  4160 
  4161 lemma to_bl_rotr: 
  4162   "to_bl (word_rotr n w) = rotater n (to_bl w)"
  4163   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  4164 
  4165 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  4166 
  4167 lemmas word_rotr_eqs =
  4168   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  4169 
  4170 declare word_rotr_eqs (1) [simp]
  4171 declare word_rotl_eqs (1) [simp]
  4172 
  4173 lemma
  4174   word_rot_rl [simp]:
  4175   "word_rotl k (word_rotr k v) = v" and
  4176   word_rot_lr [simp]:
  4177   "word_rotr k (word_rotl k v) = v"
  4178   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  4179 
  4180 lemma
  4181   word_rot_gal:
  4182   "(word_rotr n v = w) = (word_rotl n w = v)" and
  4183   word_rot_gal':
  4184   "(w = word_rotr n v) = (v = word_rotl n w)"
  4185   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] 
  4186            dest: sym)
  4187 
  4188 lemma word_rotr_rev:
  4189   "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  4190   by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
  4191                 to_bl_rotr to_bl_rotl rotater_rev)
  4192   
  4193 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  4194   by (unfold word_rot_defs) auto
  4195 
  4196 lemmas abl_cong = arg_cong [where f = "of_bl"]
  4197 
  4198 lemma word_roti_add: 
  4199   "word_roti (m + n) w = word_roti m (word_roti n w)"
  4200 proof -
  4201   have rotater_eq_lem: 
  4202     "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  4203     by auto
  4204 
  4205   have rotate_eq_lem: 
  4206     "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  4207     by auto
  4208 
  4209   note rpts [symmetric] = 
  4210     rotate_inv_plus [THEN conjunct1]
  4211     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  4212     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  4213     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  4214 
  4215   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  4216   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  4217 
  4218   show ?thesis
  4219   apply (unfold word_rot_defs)
  4220   apply (simp only: split: split_if)
  4221   apply (safe intro!: abl_cong)
  4222   apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
  4223                     to_bl_rotl
  4224                     to_bl_rotr [THEN word_bl.Rep_inverse']
  4225                     to_bl_rotr)
  4226   apply (rule rrp rrrp rpts,
  4227          simp add: nat_add_distrib [symmetric] 
  4228                    nat_diff_distrib [symmetric])+
  4229   done
  4230 qed
  4231     
  4232 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
  4233   apply (unfold word_rot_defs)
  4234   apply (cut_tac y="size w" in gt_or_eq_0)
  4235   apply (erule disjE)
  4236    apply simp_all
  4237   apply (safe intro!: abl_cong)
  4238    apply (rule rotater_eqs)
  4239    apply (simp add: word_size nat_mod_distrib)
  4240   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  4241   apply (rule rotater_eqs)
  4242   apply (simp add: word_size nat_mod_distrib)
  4243   apply (rule int_eq_0_conv [THEN iffD1])
  4244   apply (simp only: zmod_int of_nat_add)
  4245   apply (simp add: rdmods)
  4246   done
  4247 
  4248 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  4249 
  4250 
  4251 subsubsection {* "Word rotation commutes with bit-wise operations *}
  4252 
  4253 (* using locale to not pollute lemma namespace *)
  4254 locale word_rotate 
  4255 begin
  4256 
  4257 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  4258 
  4259 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  4260 
  4261 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
  4262 
  4263 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  4264 
  4265 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
  4266 
  4267 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  4268 
  4269 lemma word_rot_logs:
  4270   "word_rotl n (NOT v) = NOT word_rotl n v"
  4271   "word_rotr n (NOT v) = NOT word_rotr n v"
  4272   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  4273   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  4274   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  4275   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  4276   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  4277   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"  
  4278   by (rule word_bl.Rep_eqD,
  4279       rule word_rot_defs' [THEN trans],
  4280       simp only: blwl_syms [symmetric],
  4281       rule th1s [THEN trans], 
  4282       rule refl)+
  4283 end
  4284 
  4285 lemmas word_rot_logs = word_rotate.word_rot_logs
  4286 
  4287 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  4288   simplified word_bl_Rep']
  4289 
  4290 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  4291   simplified word_bl_Rep']
  4292 
  4293 lemma bl_word_roti_dt': 
  4294   "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow> 
  4295     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4296   apply (unfold word_roti_def)
  4297   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4298   apply safe
  4299    apply (simp add: zmod_zminus1_eq_if)
  4300    apply safe
  4301     apply (simp add: nat_mult_distrib)
  4302    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 
  4303                                       [THEN conjunct2, THEN order_less_imp_le]]
  4304                     nat_mod_distrib)
  4305   apply (simp add: nat_mod_distrib)
  4306   done
  4307 
  4308 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  4309 
  4310 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]] 
  4311 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4312 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4313 
  4314 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
  4315   by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
  4316 
  4317 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  4318   unfolding word_roti_def by auto
  4319 
  4320 lemmas word_rotr_dt_no_bin' [simp] = 
  4321   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4322   (* FIXME: negative numerals, 0 and 1 *)
  4323 
  4324 lemmas word_rotl_dt_no_bin' [simp] = 
  4325   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4326   (* FIXME: negative numerals, 0 and 1 *)
  4327 
  4328 declare word_roti_def [simp]
  4329 
  4330 
  4331 subsection {* Maximum machine word *}
  4332 
  4333 lemma word_int_cases:
  4334   obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
  4335   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
  4336 
  4337 lemma word_nat_cases [cases type: word]:
  4338   obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
  4339   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
  4340 
  4341 lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
  4342   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
  4343 
  4344 lemma max_word_max [simp,intro!]: "n \<le> max_word"
  4345   by (cases n rule: word_int_cases)
  4346     (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
  4347   
  4348 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
  4349   by (subst word_uint.Abs_norm [symmetric]) simp
  4350 
  4351 lemma word_pow_0:
  4352   "(2::'a::len word) ^ len_of TYPE('a) = 0"
  4353 proof -
  4354   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
  4355     by (rule word_of_int_2p_len)
  4356   thus ?thesis by (simp add: word_of_int_2p)
  4357 qed
  4358 
  4359 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
  4360   apply (simp add: max_word_eq)
  4361   apply uint_arith
  4362   apply auto
  4363   apply (simp add: word_pow_0)
  4364   done
  4365 
  4366 lemma max_word_minus: 
  4367   "max_word = (-1::'a::len word)"
  4368 proof -
  4369   have "-1 + 1 = (0::'a word)" by simp
  4370   thus ?thesis by (rule max_word_wrap [symmetric])
  4371 qed
  4372 
  4373 lemma max_word_bl [simp]:
  4374   "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
  4375   by (subst max_word_minus to_bl_n1)+ simp
  4376 
  4377 lemma max_test_bit [simp]:
  4378   "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
  4379   by (auto simp add: test_bit_bl word_size)
  4380 
  4381 lemma word_and_max [simp]:
  4382   "x AND max_word = x"
  4383   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4384 
  4385 lemma word_or_max [simp]:
  4386   "x OR max_word = max_word"
  4387   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4388 
  4389 lemma word_ao_dist2:
  4390   "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
  4391   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4392 
  4393 lemma word_oa_dist2:
  4394   "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
  4395   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4396 
  4397 lemma word_and_not [simp]:
  4398   "x AND NOT x = (0::'a::len0 word)"
  4399   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4400 
  4401 lemma word_or_not [simp]:
  4402   "x OR NOT x = max_word"
  4403   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4404 
  4405 lemma word_boolean:
  4406   "boolean (op AND) (op OR) bitNOT 0 max_word"
  4407   apply (rule boolean.intro)
  4408            apply (rule word_bw_assocs)
  4409           apply (rule word_bw_assocs)
  4410          apply (rule word_bw_comms)
  4411         apply (rule word_bw_comms)
  4412        apply (rule word_ao_dist2)
  4413       apply (rule word_oa_dist2)
  4414      apply (rule word_and_max)
  4415     apply (rule word_log_esimps)
  4416    apply (rule word_and_not)
  4417   apply (rule word_or_not)
  4418   done
  4419 
  4420 interpretation word_bool_alg:
  4421   boolean "op AND" "op OR" bitNOT 0 max_word
  4422   by (rule word_boolean)
  4423 
  4424 lemma word_xor_and_or:
  4425   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
  4426   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4427 
  4428 interpretation word_bool_alg:
  4429   boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
  4430   apply (rule boolean_xor.intro)
  4431    apply (rule word_boolean)
  4432   apply (rule boolean_xor_axioms.intro)
  4433   apply (rule word_xor_and_or)
  4434   done
  4435 
  4436 lemma shiftr_x_0 [iff]:
  4437   "(x::'a::len0 word) >> 0 = x"
  4438   by (simp add: shiftr_bl)
  4439 
  4440 lemma shiftl_x_0 [simp]: 
  4441   "(x :: 'a :: len word) << 0 = x"
  4442   by (simp add: shiftl_t2n)
  4443 
  4444 lemma shiftl_1 [simp]:
  4445   "(1::'a::len word) << n = 2^n"
  4446   by (simp add: shiftl_t2n)
  4447 
  4448 lemma uint_lt_0 [simp]:
  4449   "uint x < 0 = False"
  4450   by (simp add: linorder_not_less)
  4451 
  4452 lemma shiftr1_1 [simp]: 
  4453   "shiftr1 (1::'a::len word) = 0"
  4454   unfolding shiftr1_def by simp
  4455 
  4456 lemma shiftr_1[simp]: 
  4457   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  4458   by (induct n) (auto simp: shiftr_def)
  4459 
  4460 lemma word_less_1 [simp]: 
  4461   "((x::'a::len word) < 1) = (x = 0)"
  4462   by (simp add: word_less_nat_alt unat_0_iff)
  4463 
  4464 lemma to_bl_mask:
  4465   "to_bl (mask n :: 'a::len word) = 
  4466   replicate (len_of TYPE('a) - n) False @ 
  4467     replicate (min (len_of TYPE('a)) n) True"
  4468   by (simp add: mask_bl word_rep_drop min_def)
  4469 
  4470 lemma map_replicate_True:
  4471   "n = length xs \<Longrightarrow>
  4472     map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
  4473   by (induct xs arbitrary: n) auto
  4474 
  4475 lemma map_replicate_False:
  4476   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
  4477     (zip xs (replicate n False)) = replicate n False"
  4478   by (induct xs arbitrary: n) auto
  4479 
  4480 lemma bl_and_mask:
  4481   fixes w :: "'a::len word"
  4482   fixes n
  4483   defines "n' \<equiv> len_of TYPE('a) - n"
  4484   shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
  4485 proof - 
  4486   note [simp] = map_replicate_True map_replicate_False
  4487   have "to_bl (w AND mask n) = 
  4488         map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
  4489     by (simp add: bl_word_and)
  4490   also
  4491   have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
  4492   also
  4493   have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = 
  4494         replicate n' False @ drop n' (to_bl w)"
  4495     unfolding to_bl_mask n'_def map2_def
  4496     by (subst zip_append) auto
  4497   finally
  4498   show ?thesis .
  4499 qed
  4500 
  4501 lemma drop_rev_takefill:
  4502   "length xs \<le> n \<Longrightarrow>
  4503     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4504   by (simp add: takefill_alt rev_take)
  4505 
  4506 lemma map_nth_0 [simp]:
  4507   "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  4508   by (induct xs) auto
  4509 
  4510 lemma uint_plus_if_size:
  4511   "uint (x + y) = 
  4512   (if uint x + uint y < 2^size x then 
  4513       uint x + uint y 
  4514    else 
  4515       uint x + uint y - 2^size x)" 
  4516   by (simp add: word_arith_wis int_word_uint mod_add_if_z 
  4517                 word_size)
  4518 
  4519 lemma unat_plus_if_size:
  4520   "unat (x + (y::'a::len word)) = 
  4521   (if unat x + unat y < 2^size x then 
  4522       unat x + unat y 
  4523    else 
  4524       unat x + unat y - 2^size x)" 
  4525   apply (subst word_arith_nat_defs)
  4526   apply (subst unat_of_nat)
  4527   apply (simp add:  mod_nat_add word_size)
  4528   done
  4529 
  4530 lemma word_neq_0_conv:
  4531   fixes w :: "'a :: len word"
  4532   shows "(w \<noteq> 0) = (0 < w)"
  4533   unfolding word_gt_0 by simp
  4534 
  4535 lemma max_lt:
  4536   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
  4537   by (fact unat_div)
  4538 
  4539 lemma uint_sub_if_size:
  4540   "uint (x - y) = 
  4541   (if uint y \<le> uint x then 
  4542       uint x - uint y 
  4543    else 
  4544       uint x - uint y + 2^size x)"
  4545   by (simp add: word_arith_wis int_word_uint mod_sub_if_z 
  4546                 word_size)
  4547 
  4548 lemma unat_sub:
  4549   "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4550   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4551 
  4552 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  4553 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  4554   
  4555 lemma word_of_int_minus: 
  4556   "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  4557 proof -
  4558   have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
  4559   show ?thesis
  4560     apply (subst x)
  4561     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  4562     apply simp
  4563     done
  4564 qed
  4565   
  4566 lemmas word_of_int_inj = 
  4567   word_uint.Abs_inject [unfolded uints_num, simplified]
  4568 
  4569 lemma word_le_less_eq:
  4570   "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
  4571   by (auto simp add: order_class.le_less)
  4572 
  4573 lemma mod_plus_cong:
  4574   assumes 1: "(b::int) = b'"
  4575       and 2: "x mod b' = x' mod b'"
  4576       and 3: "y mod b' = y' mod b'"
  4577       and 4: "x' + y' = z'"
  4578   shows "(x + y) mod b = z' mod b'"
  4579 proof -
  4580   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  4581     by (simp add: mod_add_eq[symmetric])
  4582   also have "\<dots> = (x' + y') mod b'"
  4583     by (simp add: mod_add_eq[symmetric])
  4584   finally show ?thesis by (simp add: 4)
  4585 qed
  4586 
  4587 lemma mod_minus_cong:
  4588   assumes 1: "(b::int) = b'"
  4589       and 2: "x mod b' = x' mod b'"
  4590       and 3: "y mod b' = y' mod b'"
  4591       and 4: "x' - y' = z'"
  4592   shows "(x - y) mod b = z' mod b'"
  4593   using assms
  4594   apply (subst mod_diff_left_eq)
  4595   apply (subst mod_diff_right_eq)
  4596   apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
  4597   done
  4598 
  4599 lemma word_induct_less: 
  4600   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4601   apply (cases m)
  4602   apply atomize
  4603   apply (erule rev_mp)+
  4604   apply (rule_tac x=m in spec)
  4605   apply (induct_tac n)
  4606    apply simp
  4607   apply clarsimp
  4608   apply (erule impE)
  4609    apply clarsimp
  4610    apply (erule_tac x=n in allE)
  4611    apply (erule impE)
  4612     apply (simp add: unat_arith_simps)
  4613     apply (clarsimp simp: unat_of_nat)
  4614    apply simp
  4615   apply (erule_tac x="of_nat na" in allE)
  4616   apply (erule impE)
  4617    apply (simp add: unat_arith_simps)
  4618    apply (clarsimp simp: unat_of_nat)
  4619   apply simp
  4620   done
  4621   
  4622 lemma word_induct: 
  4623   "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4624   by (erule word_induct_less, simp)
  4625 
  4626 lemma word_induct2 [induct type]: 
  4627   "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
  4628   apply (rule word_induct, simp)
  4629   apply (case_tac "1+n = 0", auto)
  4630   done
  4631 
  4632 
  4633 subsection {* Recursion combinator for words *}
  4634 
  4635 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  4636 where
  4637   "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  4638 
  4639 lemma word_rec_0: "word_rec z s 0 = z"
  4640   by (simp add: word_rec_def)
  4641 
  4642 lemma word_rec_Suc: 
  4643   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
  4644   apply (simp add: word_rec_def unat_word_ariths)
  4645   apply (subst nat_mod_eq')
  4646    apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
  4647   apply simp
  4648   done
  4649 
  4650 lemma word_rec_Pred: 
  4651   "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
  4652   apply (rule subst[where t="n" and s="1 + (n - 1)"])
  4653    apply simp
  4654   apply (subst word_rec_Suc)
  4655    apply simp
  4656   apply simp
  4657   done
  4658 
  4659 lemma word_rec_in: 
  4660   "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  4661   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4662 
  4663 lemma word_rec_in2: 
  4664   "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  4665   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4666 
  4667 lemma word_rec_twice: 
  4668   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  4669 apply (erule rev_mp)
  4670 apply (rule_tac x=z in spec)
  4671 apply (rule_tac x=f in spec)
  4672 apply (induct n)
  4673  apply (simp add: word_rec_0)
  4674 apply clarsimp
  4675 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  4676  apply simp
  4677 apply (case_tac "1 + (n - m) = 0")
  4678  apply (simp add: word_rec_0)
  4679  apply (rule_tac f = "word_rec a b" for a b in arg_cong)
  4680  apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  4681   apply simp
  4682  apply (simp (no_asm_use))
  4683 apply (simp add: word_rec_Suc word_rec_in2)
  4684 apply (erule impE)
  4685  apply uint_arith
  4686 apply (drule_tac x="x \<circ> op + 1" in spec)
  4687 apply (drule_tac x="x 0 xa" in spec)
  4688 apply simp
  4689 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
  4690        in subst)
  4691  apply (clarsimp simp add: fun_eq_iff)
  4692  apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  4693   apply simp
  4694  apply (rule refl)
  4695 apply (rule refl)
  4696 done
  4697 
  4698 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  4699   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  4700 
  4701 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  4702 apply (erule rev_mp)
  4703 apply (induct n)
  4704  apply (auto simp add: word_rec_0 word_rec_Suc)
  4705  apply (drule spec, erule mp)
  4706  apply uint_arith
  4707 apply (drule_tac x=n in spec, erule impE)
  4708  apply uint_arith
  4709 apply simp
  4710 done
  4711 
  4712 lemma word_rec_max: 
  4713   "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f (- 1) = word_rec z f n"
  4714 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  4715  apply simp
  4716 apply simp
  4717 apply (rule word_rec_id_eq)
  4718 apply clarsimp
  4719 apply (drule spec, rule mp, erule mp)
  4720  apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  4721   prefer 2 
  4722   apply assumption
  4723  apply simp
  4724 apply (erule contrapos_pn)
  4725 apply simp
  4726 apply (drule arg_cong[where f="\<lambda>x. x - n"])
  4727 apply simp
  4728 done
  4729 
  4730 lemma unatSuc: 
  4731   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  4732   by unat_arith
  4733 
  4734 declare bin_to_bl_def [simp]
  4735 
  4736 ML_file "Tools/word_lib.ML"
  4737 ML_file "Tools/smt_word.ML"
  4738 
  4739 hide_const (open) Word
  4740 
  4741 end