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