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