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