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