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