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