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