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