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