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