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