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