src/HOL/Word/Word.thy
author haftmann
Sat Mar 01 09:34:08 2014 +0100 (2014-03-01)
changeset 55817 0bc0217387a5
parent 55816 e8dd03241e86
child 55818 d8b2f50705d0
permissions -rw-r--r--
earlier setup of transfer, without dependency on psychodelic interpretations
     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   "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
   197     (uint :: 'a::len0 word \<Rightarrow> int)"
   198   unfolding fun_rel_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   "(fun_rel op = pcr_word) numeral numeral"
   655   "(fun_rel op = pcr_word) (- numeral) (- numeral)"
   656   apply (simp_all add: fun_rel_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   unfolding word_less_def word_le_def by (simp add: less_le)
  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: "(uint x = 0) = (x = 0)"
  1240   by (auto intro!: word_uint.Rep_eqD)
  1241 
  1242 lemma unat_0_iff: "(unat x = 0) = (x = 0)"
  1243   unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
  1244 
  1245 lemma unat_0 [simp]: "unat 0 = 0"
  1246   unfolding unat_def by auto
  1247 
  1248 lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
  1249   apply (unfold word_size)
  1250   apply (rule box_equals)
  1251     defer
  1252     apply (rule word_uint.Rep_inverse)+
  1253   apply (rule word_ubin.norm_eq_iff [THEN iffD1])
  1254   apply simp
  1255   done
  1256 
  1257 lemmas size_0_same = size_0_same' [unfolded word_size]
  1258 
  1259 lemmas unat_eq_0 = unat_0_iff
  1260 lemmas unat_eq_zero = unat_0_iff
  1261 
  1262 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
  1263 by (auto simp: unat_0_iff [symmetric])
  1264 
  1265 lemma ucast_0 [simp]: "ucast 0 = 0"
  1266   unfolding ucast_def by simp
  1267 
  1268 lemma sint_0 [simp]: "sint 0 = 0"
  1269   unfolding sint_uint by simp
  1270 
  1271 lemma scast_0 [simp]: "scast 0 = 0"
  1272   unfolding scast_def by simp
  1273 
  1274 lemma sint_n1 [simp] : "sint -1 = -1"
  1275   unfolding word_m1_wi word_sbin.eq_norm by simp
  1276 
  1277 lemma scast_n1 [simp]: "scast (- 1) = - 1"
  1278   unfolding scast_def by simp
  1279 
  1280 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
  1281   unfolding word_1_wi
  1282   by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
  1283 
  1284 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
  1285   unfolding unat_def by simp
  1286 
  1287 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
  1288   unfolding ucast_def by simp
  1289 
  1290 (* now, to get the weaker results analogous to word_div/mod_def *)
  1291 
  1292 lemmas word_arith_alts = 
  1293   word_sub_wi
  1294   word_arith_wis (* FIXME: duplicate *)
  1295 
  1296 
  1297 subsection {* Transferring goals from words to ints *}
  1298 
  1299 lemma word_ths:  
  1300   shows
  1301   word_succ_p1:   "word_succ a = a + 1" and
  1302   word_pred_m1:   "word_pred a = a - 1" and
  1303   word_pred_succ: "word_pred (word_succ a) = a" and
  1304   word_succ_pred: "word_succ (word_pred a) = a" and
  1305   word_mult_succ: "word_succ a * b = b + a * b"
  1306   by (transfer, simp add: algebra_simps)+
  1307 
  1308 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
  1309   by simp
  1310 
  1311 lemmas uint_word_ariths = 
  1312   word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
  1313 
  1314 lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
  1315 
  1316 (* similar expressions for sint (arith operations) *)
  1317 lemmas sint_word_ariths = uint_word_arith_bintrs
  1318   [THEN uint_sint [symmetric, THEN trans],
  1319   unfolded uint_sint bintr_arith1s bintr_ariths 
  1320     len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
  1321 
  1322 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
  1323 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
  1324 
  1325 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
  1326   unfolding word_pred_m1 by simp
  1327 
  1328 lemma succ_pred_no [simp]:
  1329   "word_succ (numeral w) = numeral w + 1"
  1330   "word_pred (numeral w) = numeral w - 1"
  1331   "word_succ (- numeral w) = - numeral w + 1"
  1332   "word_pred (- numeral w) = - numeral w - 1"
  1333   unfolding word_succ_p1 word_pred_m1 by simp_all
  1334 
  1335 lemma word_sp_01 [simp] : 
  1336   "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
  1337   unfolding word_succ_p1 word_pred_m1 by simp_all
  1338 
  1339 (* alternative approach to lifting arithmetic equalities *)
  1340 lemma word_of_int_Ex:
  1341   "\<exists>y. x = word_of_int y"
  1342   by (rule_tac x="uint x" in exI) simp
  1343 
  1344 
  1345 subsection {* Order on fixed-length words *}
  1346 
  1347 lemma word_zero_le [simp] :
  1348   "0 <= (y :: 'a :: len0 word)"
  1349   unfolding word_le_def by auto
  1350   
  1351 lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
  1352   unfolding word_le_def
  1353   by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
  1354 
  1355 lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
  1356   unfolding word_le_def
  1357   by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
  1358 
  1359 lemmas word_not_simps [simp] = 
  1360   word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
  1361 
  1362 lemma word_gt_0: "0 < y \<longleftrightarrow> 0 \<noteq> (y :: 'a :: len0 word)"
  1363   by (simp add: less_le)
  1364 
  1365 lemmas word_gt_0_no [simp] = word_gt_0 [of "numeral y"] for y
  1366 
  1367 lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
  1368   unfolding word_sle_def word_sless_def
  1369   by (auto simp add: less_le)
  1370 
  1371 lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
  1372   unfolding unat_def word_le_def
  1373   by (rule nat_le_eq_zle [symmetric]) simp
  1374 
  1375 lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
  1376   unfolding unat_def word_less_alt
  1377   by (rule nat_less_eq_zless [symmetric]) simp
  1378   
  1379 lemma wi_less: 
  1380   "(word_of_int n < (word_of_int m :: 'a :: len0 word)) = 
  1381     (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
  1382   unfolding word_less_alt by (simp add: word_uint.eq_norm)
  1383 
  1384 lemma wi_le: 
  1385   "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) = 
  1386     (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
  1387   unfolding word_le_def by (simp add: word_uint.eq_norm)
  1388 
  1389 lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
  1390   apply (unfold udvd_def)
  1391   apply safe
  1392    apply (simp add: unat_def nat_mult_distrib)
  1393   apply (simp add: uint_nat int_mult)
  1394   apply (rule exI)
  1395   apply safe
  1396    prefer 2
  1397    apply (erule notE)
  1398    apply (rule refl)
  1399   apply force
  1400   done
  1401 
  1402 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
  1403   unfolding dvd_def udvd_nat_alt by force
  1404 
  1405 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
  1406 
  1407 lemma unat_minus_one:
  1408   assumes "w \<noteq> 0"
  1409   shows "unat (w - 1) = unat w - 1"
  1410 proof -
  1411   have "0 \<le> uint w" by (fact uint_nonnegative)
  1412   moreover from assms have "0 \<noteq> uint w" by (simp add: uint_0_iff)
  1413   ultimately have "1 \<le> uint w" by arith
  1414   from uint_lt2p [of w] have "uint w - 1 < 2 ^ len_of TYPE('a)" by arith
  1415   with `1 \<le> uint w` have "(uint w - 1) mod 2 ^ len_of TYPE('a) = uint w - 1"
  1416     by (auto intro: mod_pos_pos_trivial)
  1417   with `1 \<le> uint w` have "nat ((uint w - 1) mod 2 ^ len_of TYPE('a)) = nat (uint w) - 1"
  1418     by auto
  1419   then show ?thesis
  1420     by (simp only: unat_def int_word_uint word_arith_alts mod_diff_right_eq [symmetric])
  1421 qed
  1422 
  1423 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
  1424   by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
  1425   
  1426 lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
  1427 lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
  1428 
  1429 lemma uint_sub_lt2p [simp]: 
  1430   "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) < 
  1431     2 ^ len_of TYPE('a)"
  1432   using uint_ge_0 [of y] uint_lt2p [of x] by arith
  1433 
  1434 
  1435 subsection {* Conditions for the addition (etc) of two words to overflow *}
  1436 
  1437 lemma uint_add_lem: 
  1438   "(uint x + uint y < 2 ^ len_of TYPE('a)) = 
  1439     (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
  1440   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
  1441 
  1442 lemma uint_mult_lem: 
  1443   "(uint x * uint y < 2 ^ len_of TYPE('a)) = 
  1444     (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
  1445   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
  1446 
  1447 lemma uint_sub_lem: 
  1448   "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
  1449   by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
  1450 
  1451 lemma uint_add_le: "uint (x + y) <= uint x + uint y"
  1452   unfolding uint_word_ariths by (metis uint_add_ge0 zmod_le_nonneg_dividend)
  1453 
  1454 lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
  1455   unfolding uint_word_ariths by (metis int_mod_ge uint_sub_lt2p zless2p)
  1456 
  1457 lemma mod_add_if_z:
  1458   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
  1459    (x + y) mod z = (if x + y < z then x + y else x + y - z)"
  1460   by (auto intro: int_mod_eq)
  1461 
  1462 lemma uint_plus_if':
  1463   "uint ((a::'a word) + b) =
  1464   (if uint a + uint b < 2 ^ len_of TYPE('a::len0) then uint a + uint b
  1465    else uint a + uint b - 2 ^ len_of TYPE('a))"
  1466   using mod_add_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
  1467 
  1468 lemma mod_sub_if_z:
  1469   "(x :: int) < z ==> y < z ==> 0 <= y ==> 0 <= x ==> 0 <= z ==> 
  1470    (x - y) mod z = (if y <= x then x - y else x - y + z)"
  1471   by (auto intro: int_mod_eq)
  1472 
  1473 lemma uint_sub_if':
  1474   "uint ((a::'a word) - b) =
  1475   (if uint b \<le> uint a then uint a - uint b
  1476    else uint a - uint b + 2 ^ len_of TYPE('a::len0))"
  1477   using mod_sub_if_z [of "uint a" _ "uint b"] by (simp add: uint_word_ariths)
  1478 
  1479 
  1480 subsection {* Definition of @{text uint_arith} *}
  1481 
  1482 lemma word_of_int_inverse:
  1483   "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow> 
  1484    uint (a::'a::len0 word) = r"
  1485   apply (erule word_uint.Abs_inverse' [rotated])
  1486   apply (simp add: uints_num)
  1487   done
  1488 
  1489 lemma uint_split:
  1490   fixes x::"'a::len0 word"
  1491   shows "P (uint x) = 
  1492          (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
  1493   apply (fold word_int_case_def)
  1494   apply (auto dest!: word_of_int_inverse simp: int_word_uint mod_pos_pos_trivial
  1495               split: word_int_split)
  1496   done
  1497 
  1498 lemma uint_split_asm:
  1499   fixes x::"'a::len0 word"
  1500   shows "P (uint x) = 
  1501          (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
  1502   by (auto dest!: word_of_int_inverse 
  1503            simp: int_word_uint mod_pos_pos_trivial
  1504            split: uint_split)
  1505 
  1506 lemmas uint_splits = uint_split uint_split_asm
  1507 
  1508 lemmas uint_arith_simps = 
  1509   word_le_def word_less_alt
  1510   word_uint.Rep_inject [symmetric] 
  1511   uint_sub_if' uint_plus_if'
  1512 
  1513 (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
  1514 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d" 
  1515   by auto
  1516 
  1517 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
  1518 ML {*
  1519 fun uint_arith_simpset ctxt = 
  1520   ctxt addsimps @{thms uint_arith_simps}
  1521      delsimps @{thms word_uint.Rep_inject}
  1522      |> fold Splitter.add_split @{thms split_if_asm}
  1523      |> fold Simplifier.add_cong @{thms power_False_cong}
  1524 
  1525 fun uint_arith_tacs ctxt = 
  1526   let
  1527     fun arith_tac' n t =
  1528       Arith_Data.verbose_arith_tac ctxt n t
  1529         handle Cooper.COOPER _ => Seq.empty;
  1530   in 
  1531     [ clarify_tac ctxt 1,
  1532       full_simp_tac (uint_arith_simpset ctxt) 1,
  1533       ALLGOALS (full_simp_tac
  1534         (put_simpset HOL_ss ctxt
  1535           |> fold Splitter.add_split @{thms uint_splits}
  1536           |> fold Simplifier.add_cong @{thms power_False_cong})),
  1537       rewrite_goals_tac ctxt @{thms word_size}, 
  1538       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
  1539                          REPEAT (etac conjE n) THEN
  1540                          REPEAT (dtac @{thm word_of_int_inverse} n 
  1541                                  THEN atac n 
  1542                                  THEN atac n)),
  1543       TRYALL arith_tac' ]
  1544   end
  1545 
  1546 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
  1547 *}
  1548 
  1549 method_setup uint_arith = 
  1550   {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
  1551   "solving word arithmetic via integers and arith"
  1552 
  1553 
  1554 subsection {* More on overflows and monotonicity *}
  1555 
  1556 lemma no_plus_overflow_uint_size: 
  1557   "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
  1558   unfolding word_size by uint_arith
  1559 
  1560 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
  1561 
  1562 lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
  1563   by uint_arith
  1564 
  1565 lemma no_olen_add':
  1566   fixes x :: "'a::len0 word"
  1567   shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
  1568   by (simp add: add_ac no_olen_add)
  1569 
  1570 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
  1571 
  1572 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem]
  1573 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1]
  1574 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem]
  1575 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
  1576 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
  1577 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
  1578 
  1579 lemma word_less_sub1: 
  1580   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
  1581   by uint_arith
  1582 
  1583 lemma word_le_sub1: 
  1584   "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
  1585   by uint_arith
  1586 
  1587 lemma sub_wrap_lt: 
  1588   "((x :: 'a :: len0 word) < x - z) = (x < z)"
  1589   by uint_arith
  1590 
  1591 lemma sub_wrap: 
  1592   "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
  1593   by uint_arith
  1594 
  1595 lemma plus_minus_not_NULL_ab: 
  1596   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
  1597   by uint_arith
  1598 
  1599 lemma plus_minus_no_overflow_ab: 
  1600   "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c" 
  1601   by uint_arith
  1602 
  1603 lemma le_minus': 
  1604   "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
  1605   by uint_arith
  1606 
  1607 lemma le_plus': 
  1608   "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
  1609   by uint_arith
  1610 
  1611 lemmas le_plus = le_plus' [rotated]
  1612 
  1613 lemmas le_minus = leD [THEN thin_rl, THEN le_minus'] (* FIXME *)
  1614 
  1615 lemma word_plus_mono_right: 
  1616   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
  1617   by uint_arith
  1618 
  1619 lemma word_less_minus_cancel: 
  1620   "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
  1621   by uint_arith
  1622 
  1623 lemma word_less_minus_mono_left: 
  1624   "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
  1625   by uint_arith
  1626 
  1627 lemma word_less_minus_mono:  
  1628   "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c 
  1629   \<Longrightarrow> a - b < c - (d::'a::len word)"
  1630   by uint_arith
  1631 
  1632 lemma word_le_minus_cancel: 
  1633   "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
  1634   by uint_arith
  1635 
  1636 lemma word_le_minus_mono_left: 
  1637   "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
  1638   by uint_arith
  1639 
  1640 lemma word_le_minus_mono:  
  1641   "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c 
  1642   \<Longrightarrow> a - b <= c - (d::'a::len word)"
  1643   by uint_arith
  1644 
  1645 lemma plus_le_left_cancel_wrap: 
  1646   "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
  1647   by uint_arith
  1648 
  1649 lemma plus_le_left_cancel_nowrap: 
  1650   "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow> 
  1651     (x + y' < x + y) = (y' < y)" 
  1652   by uint_arith
  1653 
  1654 lemma word_plus_mono_right2: 
  1655   "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
  1656   by uint_arith
  1657 
  1658 lemma word_less_add_right: 
  1659   "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
  1660   by uint_arith
  1661 
  1662 lemma word_less_sub_right: 
  1663   "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
  1664   by uint_arith
  1665 
  1666 lemma word_le_plus_either: 
  1667   "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
  1668   by uint_arith
  1669 
  1670 lemma word_less_nowrapI: 
  1671   "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
  1672   by uint_arith
  1673 
  1674 lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
  1675   by uint_arith
  1676 
  1677 lemma inc_i: 
  1678   "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
  1679   by uint_arith
  1680 
  1681 lemma udvd_incr_lem:
  1682   "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow> 
  1683     uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
  1684   apply clarsimp
  1685   
  1686   apply (drule less_le_mult)
  1687   apply safe
  1688   done
  1689 
  1690 lemma udvd_incr': 
  1691   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
  1692     uint q = ua + n' * uint K \<Longrightarrow> p + K <= q" 
  1693   apply (unfold word_less_alt word_le_def)
  1694   apply (drule (2) udvd_incr_lem)
  1695   apply (erule uint_add_le [THEN order_trans])
  1696   done
  1697 
  1698 lemma udvd_decr': 
  1699   "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow> 
  1700     uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
  1701   apply (unfold word_less_alt word_le_def)
  1702   apply (drule (2) udvd_incr_lem)
  1703   apply (drule le_diff_eq [THEN iffD2])
  1704   apply (erule order_trans)
  1705   apply (rule uint_sub_ge)
  1706   done
  1707 
  1708 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
  1709 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
  1710 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
  1711 
  1712 lemma udvd_minus_le': 
  1713   "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
  1714   apply (unfold udvd_def)
  1715   apply clarify
  1716   apply (erule (2) udvd_decr0)
  1717   done
  1718 
  1719 lemma udvd_incr2_K: 
  1720   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
  1721     0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
  1722   using [[simproc del: linordered_ring_less_cancel_factor]]
  1723   apply (unfold udvd_def)
  1724   apply clarify
  1725   apply (simp add: uint_arith_simps split: split_if_asm)
  1726    prefer 2 
  1727    apply (insert uint_range' [of s])[1]
  1728    apply arith
  1729   apply (drule add_commute [THEN xtr1])
  1730   apply (simp add: diff_less_eq [symmetric])
  1731   apply (drule less_le_mult)
  1732    apply arith
  1733   apply simp
  1734   done
  1735 
  1736 (* links with rbl operations *)
  1737 lemma word_succ_rbl:
  1738   "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
  1739   apply (unfold word_succ_def)
  1740   apply clarify
  1741   apply (simp add: to_bl_of_bin)
  1742   apply (simp add: to_bl_def rbl_succ)
  1743   done
  1744 
  1745 lemma word_pred_rbl:
  1746   "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
  1747   apply (unfold word_pred_def)
  1748   apply clarify
  1749   apply (simp add: to_bl_of_bin)
  1750   apply (simp add: to_bl_def rbl_pred)
  1751   done
  1752 
  1753 lemma word_add_rbl:
  1754   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
  1755     to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
  1756   apply (unfold word_add_def)
  1757   apply clarify
  1758   apply (simp add: to_bl_of_bin)
  1759   apply (simp add: to_bl_def rbl_add)
  1760   done
  1761 
  1762 lemma word_mult_rbl:
  1763   "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow> 
  1764     to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
  1765   apply (unfold word_mult_def)
  1766   apply clarify
  1767   apply (simp add: to_bl_of_bin)
  1768   apply (simp add: to_bl_def rbl_mult)
  1769   done
  1770 
  1771 lemma rtb_rbl_ariths:
  1772   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
  1773   "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
  1774   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
  1775   "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
  1776   by (auto simp: rev_swap [symmetric] word_succ_rbl 
  1777                  word_pred_rbl word_mult_rbl word_add_rbl)
  1778 
  1779 
  1780 subsection {* Arithmetic type class instantiations *}
  1781 
  1782 lemmas word_le_0_iff [simp] =
  1783   word_zero_le [THEN leD, THEN linorder_antisym_conv1]
  1784 
  1785 lemma word_of_int_nat: 
  1786   "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
  1787   by (simp add: of_nat_nat word_of_int)
  1788 
  1789 (* note that iszero_def is only for class comm_semiring_1_cancel,
  1790    which requires word length >= 1, ie 'a :: len word *) 
  1791 lemma iszero_word_no [simp]:
  1792   "iszero (numeral bin :: 'a :: len word) = 
  1793     iszero (bintrunc (len_of TYPE('a)) (numeral bin))"
  1794   using word_ubin.norm_eq_iff [where 'a='a, of "numeral bin" 0]
  1795   by (simp add: iszero_def [symmetric])
  1796     
  1797 text {* Use @{text iszero} to simplify equalities between word numerals. *}
  1798 
  1799 lemmas word_eq_numeral_iff_iszero [simp] =
  1800   eq_numeral_iff_iszero [where 'a="'a::len word"]
  1801 
  1802 
  1803 subsection {* Word and nat *}
  1804 
  1805 lemma td_ext_unat [OF refl]:
  1806   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  1807     td_ext (unat :: 'a word => nat) of_nat 
  1808     (unats n) (%i. i mod 2 ^ n)"
  1809   apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
  1810   apply (auto intro!: imageI simp add : word_of_int_hom_syms)
  1811   apply (erule word_uint.Abs_inverse [THEN arg_cong])
  1812   apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
  1813   done
  1814 
  1815 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
  1816 
  1817 interpretation word_unat:
  1818   td_ext "unat::'a::len word => nat" 
  1819          of_nat 
  1820          "unats (len_of TYPE('a::len))"
  1821          "%i. i mod 2 ^ len_of TYPE('a::len)"
  1822   by (rule td_ext_unat)
  1823 
  1824 lemmas td_unat = word_unat.td_thm
  1825 
  1826 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
  1827 
  1828 lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
  1829   apply (unfold unats_def)
  1830   apply clarsimp
  1831   apply (rule xtrans, rule unat_lt2p, assumption) 
  1832   done
  1833 
  1834 lemma word_nchotomy:
  1835   "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
  1836   apply (rule allI)
  1837   apply (rule word_unat.Abs_cases)
  1838   apply (unfold unats_def)
  1839   apply auto
  1840   done
  1841 
  1842 lemma of_nat_eq:
  1843   fixes w :: "'a::len word"
  1844   shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
  1845   apply (rule trans)
  1846    apply (rule word_unat.inverse_norm)
  1847   apply (rule iffI)
  1848    apply (rule mod_eqD)
  1849    apply simp
  1850   apply clarsimp
  1851   done
  1852 
  1853 lemma of_nat_eq_size: 
  1854   "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
  1855   unfolding word_size by (rule of_nat_eq)
  1856 
  1857 lemma of_nat_0:
  1858   "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
  1859   by (simp add: of_nat_eq)
  1860 
  1861 lemma of_nat_2p [simp]:
  1862   "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
  1863   by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
  1864 
  1865 lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
  1866   by (cases k) auto
  1867 
  1868 lemma of_nat_neq_0: 
  1869   "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
  1870   by (clarsimp simp add : of_nat_0)
  1871 
  1872 lemma Abs_fnat_hom_add:
  1873   "of_nat a + of_nat b = of_nat (a + b)"
  1874   by simp
  1875 
  1876 lemma Abs_fnat_hom_mult:
  1877   "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
  1878   by (simp add: word_of_nat wi_hom_mult zmult_int)
  1879 
  1880 lemma Abs_fnat_hom_Suc:
  1881   "word_succ (of_nat a) = of_nat (Suc a)"
  1882   by (simp add: word_of_nat wi_hom_succ add_ac)
  1883 
  1884 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
  1885   by simp
  1886 
  1887 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
  1888   by simp
  1889 
  1890 lemmas Abs_fnat_homs = 
  1891   Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc 
  1892   Abs_fnat_hom_0 Abs_fnat_hom_1
  1893 
  1894 lemma word_arith_nat_add:
  1895   "a + b = of_nat (unat a + unat b)" 
  1896   by simp
  1897 
  1898 lemma word_arith_nat_mult:
  1899   "a * b = of_nat (unat a * unat b)"
  1900   by (simp add: of_nat_mult)
  1901     
  1902 lemma word_arith_nat_Suc:
  1903   "word_succ a = of_nat (Suc (unat a))"
  1904   by (subst Abs_fnat_hom_Suc [symmetric]) simp
  1905 
  1906 lemma word_arith_nat_div:
  1907   "a div b = of_nat (unat a div unat b)"
  1908   by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
  1909 
  1910 lemma word_arith_nat_mod:
  1911   "a mod b = of_nat (unat a mod unat b)"
  1912   by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
  1913 
  1914 lemmas word_arith_nat_defs =
  1915   word_arith_nat_add word_arith_nat_mult
  1916   word_arith_nat_Suc Abs_fnat_hom_0
  1917   Abs_fnat_hom_1 word_arith_nat_div
  1918   word_arith_nat_mod 
  1919 
  1920 lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
  1921   by simp
  1922   
  1923 lemmas unat_word_ariths = word_arith_nat_defs
  1924   [THEN trans [OF unat_cong unat_of_nat]]
  1925 
  1926 lemmas word_sub_less_iff = word_sub_le_iff
  1927   [unfolded linorder_not_less [symmetric] Not_eq_iff]
  1928 
  1929 lemma unat_add_lem: 
  1930   "(unat x + unat y < 2 ^ len_of TYPE('a)) = 
  1931     (unat (x + y :: 'a :: len word) = unat x + unat y)"
  1932   unfolding unat_word_ariths
  1933   by (auto intro!: trans [OF _ nat_mod_lem])
  1934 
  1935 lemma unat_mult_lem: 
  1936   "(unat x * unat y < 2 ^ len_of TYPE('a)) = 
  1937     (unat (x * y :: 'a :: len word) = unat x * unat y)"
  1938   unfolding unat_word_ariths
  1939   by (auto intro!: trans [OF _ nat_mod_lem])
  1940 
  1941 lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
  1942 
  1943 lemma le_no_overflow: 
  1944   "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
  1945   apply (erule order_trans)
  1946   apply (erule olen_add_eqv [THEN iffD1])
  1947   done
  1948 
  1949 lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
  1950 
  1951 lemma unat_sub_if_size:
  1952   "unat (x - y) = (if unat y <= unat x 
  1953    then unat x - unat y 
  1954    else unat x + 2 ^ size x - unat y)"
  1955   apply (unfold word_size)
  1956   apply (simp add: un_ui_le)
  1957   apply (auto simp add: unat_def uint_sub_if')
  1958    apply (rule nat_diff_distrib)
  1959     prefer 3
  1960     apply (simp add: algebra_simps)
  1961     apply (rule nat_diff_distrib [THEN trans])
  1962       prefer 3
  1963       apply (subst nat_add_distrib)
  1964         prefer 3
  1965         apply (simp add: nat_power_eq)
  1966        apply auto
  1967   apply uint_arith
  1968   done
  1969 
  1970 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
  1971 
  1972 lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
  1973   apply (simp add : unat_word_ariths)
  1974   apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1975   apply (rule div_le_dividend)
  1976   done
  1977 
  1978 lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
  1979   apply (clarsimp simp add : unat_word_ariths)
  1980   apply (cases "unat y")
  1981    prefer 2
  1982    apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
  1983    apply (rule mod_le_divisor)
  1984    apply auto
  1985   done
  1986 
  1987 lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
  1988   unfolding uint_nat by (simp add : unat_div zdiv_int)
  1989 
  1990 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
  1991   unfolding uint_nat by (simp add : unat_mod zmod_int)
  1992 
  1993 
  1994 subsection {* Definition of @[text unat_arith} tactic *}
  1995 
  1996 lemma unat_split:
  1997   fixes x::"'a::len word"
  1998   shows "P (unat x) = 
  1999          (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
  2000   by (auto simp: unat_of_nat)
  2001 
  2002 lemma unat_split_asm:
  2003   fixes x::"'a::len word"
  2004   shows "P (unat x) = 
  2005          (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
  2006   by (auto simp: unat_of_nat)
  2007 
  2008 lemmas of_nat_inverse = 
  2009   word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
  2010 
  2011 lemmas unat_splits = unat_split unat_split_asm
  2012 
  2013 lemmas unat_arith_simps =
  2014   word_le_nat_alt word_less_nat_alt
  2015   word_unat.Rep_inject [symmetric]
  2016   unat_sub_if' unat_plus_if' unat_div unat_mod
  2017 
  2018 (* unat_arith_tac: tactic to reduce word arithmetic to nat, 
  2019    try to solve via arith *)
  2020 ML {*
  2021 fun unat_arith_simpset ctxt = 
  2022   ctxt addsimps @{thms unat_arith_simps}
  2023      delsimps @{thms word_unat.Rep_inject}
  2024      |> fold Splitter.add_split @{thms split_if_asm}
  2025      |> fold Simplifier.add_cong @{thms power_False_cong}
  2026 
  2027 fun unat_arith_tacs ctxt =   
  2028   let
  2029     fun arith_tac' n t =
  2030       Arith_Data.verbose_arith_tac ctxt n t
  2031         handle Cooper.COOPER _ => Seq.empty;
  2032   in 
  2033     [ clarify_tac ctxt 1,
  2034       full_simp_tac (unat_arith_simpset ctxt) 1,
  2035       ALLGOALS (full_simp_tac
  2036         (put_simpset HOL_ss ctxt
  2037           |> fold Splitter.add_split @{thms unat_splits}
  2038           |> fold Simplifier.add_cong @{thms power_False_cong})),
  2039       rewrite_goals_tac ctxt @{thms word_size}, 
  2040       ALLGOALS  (fn n => REPEAT (resolve_tac [allI, impI] n) THEN      
  2041                          REPEAT (etac conjE n) THEN
  2042                          REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
  2043       TRYALL arith_tac' ] 
  2044   end
  2045 
  2046 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
  2047 *}
  2048 
  2049 method_setup unat_arith = 
  2050   {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
  2051   "solving word arithmetic via natural numbers and arith"
  2052 
  2053 lemma no_plus_overflow_unat_size: 
  2054   "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)" 
  2055   unfolding word_size by unat_arith
  2056 
  2057 lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
  2058 
  2059 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]
  2060 
  2061 lemma word_div_mult: 
  2062   "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow> 
  2063     x * y div y = x"
  2064   apply unat_arith
  2065   apply clarsimp
  2066   apply (subst unat_mult_lem [THEN iffD1])
  2067   apply auto
  2068   done
  2069 
  2070 lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow> 
  2071     unat i * unat x < 2 ^ len_of TYPE('a)"
  2072   apply unat_arith
  2073   apply clarsimp
  2074   apply (drule mult_le_mono1)
  2075   apply (erule order_le_less_trans)
  2076   apply (rule xtr7 [OF unat_lt2p div_mult_le])
  2077   done
  2078 
  2079 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
  2080 
  2081 lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
  2082   apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
  2083   apply (simp add: unat_arith_simps)
  2084   apply (drule (1) mult_less_mono1)
  2085   apply (erule order_less_le_trans)
  2086   apply (rule div_mult_le)
  2087   done
  2088 
  2089 lemma div_le_mult: 
  2090   "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
  2091   apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
  2092   apply (simp add: unat_arith_simps)
  2093   apply (drule mult_le_mono1)
  2094   apply (erule order_trans)
  2095   apply (rule div_mult_le)
  2096   done
  2097 
  2098 lemma div_lt_uint': 
  2099   "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
  2100   apply (unfold uint_nat)
  2101   apply (drule div_lt')
  2102   apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric] 
  2103                    nat_power_eq)
  2104   done
  2105 
  2106 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
  2107 
  2108 lemma word_le_exists': 
  2109   "(x :: 'a :: len0 word) <= y \<Longrightarrow> 
  2110     (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
  2111   apply (rule exI)
  2112   apply (rule conjI)
  2113   apply (rule zadd_diff_inverse)
  2114   apply uint_arith
  2115   done
  2116 
  2117 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
  2118 
  2119 lemmas plus_minus_no_overflow =
  2120   order_less_imp_le [THEN plus_minus_no_overflow_ab]
  2121   
  2122 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
  2123   word_le_minus_cancel word_le_minus_mono_left
  2124 
  2125 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x
  2126 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
  2127 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
  2128 
  2129 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
  2130 
  2131 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
  2132 
  2133 lemma thd1:
  2134   "a div b * b \<le> (a::nat)"
  2135   using gt_or_eq_0 [of b]
  2136   apply (rule disjE)
  2137    apply (erule xtr4 [OF thd mult_commute])
  2138   apply clarsimp
  2139   done
  2140 
  2141 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1 
  2142 
  2143 lemma word_mod_div_equality:
  2144   "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
  2145   apply (unfold word_less_nat_alt word_arith_nat_defs)
  2146   apply (cut_tac y="unat b" in gt_or_eq_0)
  2147   apply (erule disjE)
  2148    apply (simp add: mod_div_equality uno_simps)
  2149   apply simp
  2150   done
  2151 
  2152 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
  2153   apply (unfold word_le_nat_alt word_arith_nat_defs)
  2154   apply (cut_tac y="unat b" in gt_or_eq_0)
  2155   apply (erule disjE)
  2156    apply (simp add: div_mult_le uno_simps)
  2157   apply simp
  2158   done
  2159 
  2160 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
  2161   apply (simp only: word_less_nat_alt word_arith_nat_defs)
  2162   apply (clarsimp simp add : uno_simps)
  2163   done
  2164 
  2165 lemma word_of_int_power_hom: 
  2166   "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
  2167   by (induct n) (simp_all add: wi_hom_mult [symmetric])
  2168 
  2169 lemma word_arith_power_alt: 
  2170   "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
  2171   by (simp add : word_of_int_power_hom [symmetric])
  2172 
  2173 lemma of_bl_length_less: 
  2174   "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
  2175   apply (unfold of_bl_def word_less_alt word_numeral_alt)
  2176   apply safe
  2177   apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm 
  2178                        del: word_of_int_numeral)
  2179   apply (simp add: mod_pos_pos_trivial)
  2180   apply (subst mod_pos_pos_trivial)
  2181     apply (rule bl_to_bin_ge0)
  2182    apply (rule order_less_trans)
  2183     apply (rule bl_to_bin_lt2p)
  2184    apply simp
  2185   apply (rule bl_to_bin_lt2p)
  2186   done
  2187 
  2188 
  2189 subsection {* Cardinality, finiteness of set of words *}
  2190 
  2191 instance word :: (len0) finite
  2192   by (default, simp add: type_definition.univ [OF type_definition_word])
  2193 
  2194 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
  2195   by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
  2196 
  2197 lemma card_word_size: 
  2198   "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
  2199 unfolding word_size by (rule card_word)
  2200 
  2201 
  2202 subsection {* Bitwise Operations on Words *}
  2203 
  2204 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
  2205   
  2206 (* following definitions require both arithmetic and bit-wise word operations *)
  2207 
  2208 (* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
  2209 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
  2210   folded word_ubin.eq_norm, THEN eq_reflection]
  2211 
  2212 (* the binary operations only *)
  2213 (* BH: why is this needed? *)
  2214 lemmas word_log_binary_defs = 
  2215   word_and_def word_or_def word_xor_def
  2216 
  2217 lemma word_wi_log_defs:
  2218   "NOT word_of_int a = word_of_int (NOT a)"
  2219   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
  2220   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
  2221   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
  2222   by (transfer, rule refl)+
  2223 
  2224 lemma word_no_log_defs [simp]:
  2225   "NOT (numeral a) = word_of_int (NOT (numeral a))"
  2226   "NOT (- numeral a) = word_of_int (NOT (- numeral a))"
  2227   "numeral a AND numeral b = word_of_int (numeral a AND numeral b)"
  2228   "numeral a AND - numeral b = word_of_int (numeral a AND - numeral b)"
  2229   "- numeral a AND numeral b = word_of_int (- numeral a AND numeral b)"
  2230   "- numeral a AND - numeral b = word_of_int (- numeral a AND - numeral b)"
  2231   "numeral a OR numeral b = word_of_int (numeral a OR numeral b)"
  2232   "numeral a OR - numeral b = word_of_int (numeral a OR - numeral b)"
  2233   "- numeral a OR numeral b = word_of_int (- numeral a OR numeral b)"
  2234   "- numeral a OR - numeral b = word_of_int (- numeral a OR - numeral b)"
  2235   "numeral a XOR numeral b = word_of_int (numeral a XOR numeral b)"
  2236   "numeral a XOR - numeral b = word_of_int (numeral a XOR - numeral b)"
  2237   "- numeral a XOR numeral b = word_of_int (- numeral a XOR numeral b)"
  2238   "- numeral a XOR - numeral b = word_of_int (- numeral a XOR - numeral b)"
  2239   by (transfer, rule refl)+
  2240 
  2241 text {* Special cases for when one of the arguments equals 1. *}
  2242 
  2243 lemma word_bitwise_1_simps [simp]:
  2244   "NOT (1::'a::len0 word) = -2"
  2245   "1 AND numeral b = word_of_int (1 AND numeral b)"
  2246   "1 AND - numeral b = word_of_int (1 AND - numeral b)"
  2247   "numeral a AND 1 = word_of_int (numeral a AND 1)"
  2248   "- numeral a AND 1 = word_of_int (- numeral a AND 1)"
  2249   "1 OR numeral b = word_of_int (1 OR numeral b)"
  2250   "1 OR - numeral b = word_of_int (1 OR - numeral b)"
  2251   "numeral a OR 1 = word_of_int (numeral a OR 1)"
  2252   "- numeral a OR 1 = word_of_int (- numeral a OR 1)"
  2253   "1 XOR numeral b = word_of_int (1 XOR numeral b)"
  2254   "1 XOR - numeral b = word_of_int (1 XOR - numeral b)"
  2255   "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
  2256   "- numeral a XOR 1 = word_of_int (- numeral a XOR 1)"
  2257   by (transfer, simp)+
  2258 
  2259 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
  2260   by (transfer, simp add: bin_trunc_ao)
  2261 
  2262 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
  2263   by (transfer, simp add: bin_trunc_ao)
  2264 
  2265 lemma test_bit_wi [simp]:
  2266   "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
  2267   unfolding word_test_bit_def
  2268   by (simp add: word_ubin.eq_norm nth_bintr)
  2269 
  2270 lemma word_test_bit_transfer [transfer_rule]:
  2271   "(fun_rel pcr_word (fun_rel op = op =))
  2272     (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
  2273   unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
  2274 
  2275 lemma word_ops_nth_size:
  2276   "n < size (x::'a::len0 word) \<Longrightarrow> 
  2277     (x OR y) !! n = (x !! n | y !! n) & 
  2278     (x AND y) !! n = (x !! n & y !! n) & 
  2279     (x XOR y) !! n = (x !! n ~= y !! n) & 
  2280     (NOT x) !! n = (~ x !! n)"
  2281   unfolding word_size by transfer (simp add: bin_nth_ops)
  2282 
  2283 lemma word_ao_nth:
  2284   fixes x :: "'a::len0 word"
  2285   shows "(x OR y) !! n = (x !! n | y !! n) & 
  2286          (x AND y) !! n = (x !! n & y !! n)"
  2287   by transfer (auto simp add: bin_nth_ops)
  2288 
  2289 lemma test_bit_numeral [simp]:
  2290   "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2291     n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
  2292   by transfer (rule refl)
  2293 
  2294 lemma test_bit_neg_numeral [simp]:
  2295   "(- numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
  2296     n < len_of TYPE('a) \<and> bin_nth (- numeral w) n"
  2297   by transfer (rule refl)
  2298 
  2299 lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
  2300   by transfer auto
  2301   
  2302 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
  2303   by transfer simp
  2304 
  2305 lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
  2306   by transfer simp
  2307 
  2308 (* get from commutativity, associativity etc of int_and etc
  2309   to same for word_and etc *)
  2310 
  2311 lemmas bwsimps = 
  2312   wi_hom_add
  2313   word_wi_log_defs
  2314 
  2315 lemma word_bw_assocs:
  2316   fixes x :: "'a::len0 word"
  2317   shows
  2318   "(x AND y) AND z = x AND y AND z"
  2319   "(x OR y) OR z = x OR y OR z"
  2320   "(x XOR y) XOR z = x XOR y XOR z"
  2321   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2322   
  2323 lemma word_bw_comms:
  2324   fixes x :: "'a::len0 word"
  2325   shows
  2326   "x AND y = y AND x"
  2327   "x OR y = y OR x"
  2328   "x XOR y = y XOR x"
  2329   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2330   
  2331 lemma word_bw_lcs:
  2332   fixes x :: "'a::len0 word"
  2333   shows
  2334   "y AND x AND z = x AND y AND z"
  2335   "y OR x OR z = x OR y OR z"
  2336   "y XOR x XOR z = x XOR y XOR z"
  2337   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2338 
  2339 lemma word_log_esimps [simp]:
  2340   fixes x :: "'a::len0 word"
  2341   shows
  2342   "x AND 0 = 0"
  2343   "x AND -1 = x"
  2344   "x OR 0 = x"
  2345   "x OR -1 = -1"
  2346   "x XOR 0 = x"
  2347   "x XOR -1 = NOT x"
  2348   "0 AND x = 0"
  2349   "-1 AND x = x"
  2350   "0 OR x = x"
  2351   "-1 OR x = -1"
  2352   "0 XOR x = x"
  2353   "-1 XOR x = NOT x"
  2354   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2355 
  2356 lemma word_not_dist:
  2357   fixes x :: "'a::len0 word"
  2358   shows
  2359   "NOT (x OR y) = NOT x AND NOT y"
  2360   "NOT (x AND y) = NOT x OR NOT y"
  2361   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2362 
  2363 lemma word_bw_same:
  2364   fixes x :: "'a::len0 word"
  2365   shows
  2366   "x AND x = x"
  2367   "x OR x = x"
  2368   "x XOR x = 0"
  2369   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2370 
  2371 lemma word_ao_absorbs [simp]:
  2372   fixes x :: "'a::len0 word"
  2373   shows
  2374   "x AND (y OR x) = x"
  2375   "x OR y AND x = x"
  2376   "x AND (x OR y) = x"
  2377   "y AND x OR x = x"
  2378   "(y OR x) AND x = x"
  2379   "x OR x AND y = x"
  2380   "(x OR y) AND x = x"
  2381   "x AND y OR x = x"
  2382   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2383 
  2384 lemma word_not_not [simp]:
  2385   "NOT NOT (x::'a::len0 word) = x"
  2386   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2387 
  2388 lemma word_ao_dist:
  2389   fixes x :: "'a::len0 word"
  2390   shows "(x OR y) AND z = x AND z OR y AND z"
  2391   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2392 
  2393 lemma word_oa_dist:
  2394   fixes x :: "'a::len0 word"
  2395   shows "x AND y OR z = (x OR z) AND (y OR z)"
  2396   by (auto simp: word_eq_iff word_ops_nth_size [unfolded word_size])
  2397 
  2398 lemma word_add_not [simp]: 
  2399   fixes x :: "'a::len0 word"
  2400   shows "x + NOT x = -1"
  2401   by transfer (simp add: bin_add_not)
  2402 
  2403 lemma word_plus_and_or [simp]:
  2404   fixes x :: "'a::len0 word"
  2405   shows "(x AND y) + (x OR y) = x + y"
  2406   by transfer (simp add: plus_and_or)
  2407 
  2408 lemma leoa:   
  2409   fixes x :: "'a::len0 word"
  2410   shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
  2411 lemma leao: 
  2412   fixes x' :: "'a::len0 word"
  2413   shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto 
  2414 
  2415 lemma word_ao_equiv:
  2416   fixes w w' :: "'a::len0 word"
  2417   shows "(w = w OR w') = (w' = w AND w')"
  2418   by (auto intro: leoa leao)
  2419 
  2420 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
  2421   unfolding word_le_def uint_or
  2422   by (auto intro: le_int_or) 
  2423 
  2424 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
  2425 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
  2426 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
  2427 
  2428 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)" 
  2429   unfolding to_bl_def word_log_defs bl_not_bin
  2430   by (simp add: word_ubin.eq_norm)
  2431 
  2432 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)" 
  2433   unfolding to_bl_def word_log_defs bl_xor_bin
  2434   by (simp add: word_ubin.eq_norm)
  2435 
  2436 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)" 
  2437   unfolding to_bl_def word_log_defs bl_or_bin
  2438   by (simp add: word_ubin.eq_norm)
  2439 
  2440 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)" 
  2441   unfolding to_bl_def word_log_defs bl_and_bin
  2442   by (simp add: word_ubin.eq_norm)
  2443 
  2444 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
  2445   by (auto simp: word_test_bit_def word_lsb_def)
  2446 
  2447 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
  2448   unfolding word_lsb_def uint_eq_0 uint_1 by simp
  2449 
  2450 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
  2451   apply (unfold word_lsb_def uint_bl bin_to_bl_def) 
  2452   apply (rule_tac bin="uint w" in bin_exhaust)
  2453   apply (cases "size w")
  2454    apply auto
  2455    apply (auto simp add: bin_to_bl_aux_alt)
  2456   done
  2457 
  2458 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
  2459   unfolding word_lsb_def bin_last_def by auto
  2460 
  2461 lemma word_msb_sint: "msb w = (sint w < 0)" 
  2462   unfolding word_msb_def sign_Min_lt_0 ..
  2463 
  2464 lemma msb_word_of_int:
  2465   "msb (word_of_int x::'a::len word) = bin_nth x (len_of TYPE('a) - 1)"
  2466   unfolding word_msb_def by (simp add: word_sbin.eq_norm bin_sign_lem)
  2467 
  2468 lemma word_msb_numeral [simp]:
  2469   "msb (numeral w::'a::len word) = bin_nth (numeral w) (len_of TYPE('a) - 1)"
  2470   unfolding word_numeral_alt by (rule msb_word_of_int)
  2471 
  2472 lemma word_msb_neg_numeral [simp]:
  2473   "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (len_of TYPE('a) - 1)"
  2474   unfolding word_neg_numeral_alt by (rule msb_word_of_int)
  2475 
  2476 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
  2477   unfolding word_msb_def by simp
  2478 
  2479 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> len_of TYPE('a) = 1"
  2480   unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
  2481   by (simp add: Suc_le_eq)
  2482 
  2483 lemma word_msb_nth:
  2484   "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
  2485   unfolding word_msb_def sint_uint by (simp add: bin_sign_lem)
  2486 
  2487 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
  2488   apply (unfold word_msb_nth uint_bl)
  2489   apply (subst hd_conv_nth)
  2490   apply (rule length_greater_0_conv [THEN iffD1])
  2491    apply simp
  2492   apply (simp add : nth_bin_to_bl word_size)
  2493   done
  2494 
  2495 lemma word_set_nth [simp]:
  2496   "set_bit w n (test_bit w n) = (w::'a::len0 word)"
  2497   unfolding word_test_bit_def word_set_bit_def by auto
  2498 
  2499 lemma bin_nth_uint':
  2500   "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
  2501   apply (unfold word_size)
  2502   apply (safe elim!: bin_nth_uint_imp)
  2503    apply (frule bin_nth_uint_imp)
  2504    apply (fast dest!: bin_nth_bl)+
  2505   done
  2506 
  2507 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
  2508 
  2509 lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
  2510   unfolding to_bl_def word_test_bit_def word_size
  2511   by (rule bin_nth_uint)
  2512 
  2513 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
  2514   apply (unfold test_bit_bl)
  2515   apply clarsimp
  2516   apply (rule trans)
  2517    apply (rule nth_rev_alt)
  2518    apply (auto simp add: word_size)
  2519   done
  2520 
  2521 lemma test_bit_set: 
  2522   fixes w :: "'a::len0 word"
  2523   shows "(set_bit w n x) !! n = (n < size w & x)"
  2524   unfolding word_size word_test_bit_def word_set_bit_def
  2525   by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
  2526 
  2527 lemma test_bit_set_gen: 
  2528   fixes w :: "'a::len0 word"
  2529   shows "test_bit (set_bit w n x) m = 
  2530          (if m = n then n < size w & x else test_bit w m)"
  2531   apply (unfold word_size word_test_bit_def word_set_bit_def)
  2532   apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
  2533   apply (auto elim!: test_bit_size [unfolded word_size]
  2534               simp add: word_test_bit_def [symmetric])
  2535   done
  2536 
  2537 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
  2538   unfolding of_bl_def bl_to_bin_rep_F by auto
  2539   
  2540 lemma msb_nth:
  2541   fixes w :: "'a::len word"
  2542   shows "msb w = w !! (len_of TYPE('a) - 1)"
  2543   unfolding word_msb_nth word_test_bit_def by simp
  2544 
  2545 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
  2546 lemmas msb1 = msb0 [where i = 0]
  2547 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
  2548 
  2549 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
  2550 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
  2551 
  2552 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
  2553   "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow> 
  2554     td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
  2555   apply (unfold word_size td_ext_def')
  2556   apply safe
  2557      apply (rule_tac [3] ext)
  2558      apply (rule_tac [4] ext)
  2559      apply (unfold word_size of_nth_def test_bit_bl)
  2560      apply safe
  2561        defer
  2562        apply (clarsimp simp: word_bl.Abs_inverse)+
  2563   apply (rule word_bl.Rep_inverse')
  2564   apply (rule sym [THEN trans])
  2565   apply (rule bl_of_nth_nth)
  2566   apply simp
  2567   apply (rule bl_of_nth_inj)
  2568   apply (clarsimp simp add : test_bit_bl word_size)
  2569   done
  2570 
  2571 interpretation test_bit:
  2572   td_ext "op !! :: 'a::len0 word => nat => bool"
  2573          set_bits
  2574          "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
  2575          "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
  2576   by (rule td_ext_nth)
  2577 
  2578 lemmas td_nth = test_bit.td_thm
  2579 
  2580 lemma word_set_set_same [simp]:
  2581   fixes w :: "'a::len0 word"
  2582   shows "set_bit (set_bit w n x) n y = set_bit w n y" 
  2583   by (rule word_eqI) (simp add : test_bit_set_gen word_size)
  2584     
  2585 lemma word_set_set_diff: 
  2586   fixes w :: "'a::len0 word"
  2587   assumes "m ~= n"
  2588   shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" 
  2589   by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
  2590 
  2591 lemma nth_sint: 
  2592   fixes w :: "'a::len word"
  2593   defines "l \<equiv> len_of TYPE ('a)"
  2594   shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
  2595   unfolding sint_uint l_def
  2596   by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
  2597 
  2598 lemma word_lsb_numeral [simp]:
  2599   "lsb (numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (numeral bin)"
  2600   unfolding word_lsb_alt test_bit_numeral by simp
  2601 
  2602 lemma word_lsb_neg_numeral [simp]:
  2603   "lsb (- numeral bin :: 'a :: len word) \<longleftrightarrow> bin_last (- numeral bin)"
  2604   unfolding word_lsb_alt test_bit_neg_numeral by simp
  2605 
  2606 lemma set_bit_word_of_int:
  2607   "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
  2608   unfolding word_set_bit_def
  2609   apply (rule word_eqI)
  2610   apply (simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
  2611   done
  2612 
  2613 lemma word_set_numeral [simp]:
  2614   "set_bit (numeral bin::'a::len0 word) n b = 
  2615     word_of_int (bin_sc n b (numeral bin))"
  2616   unfolding word_numeral_alt by (rule set_bit_word_of_int)
  2617 
  2618 lemma word_set_neg_numeral [simp]:
  2619   "set_bit (- numeral bin::'a::len0 word) n b = 
  2620     word_of_int (bin_sc n b (- numeral bin))"
  2621   unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
  2622 
  2623 lemma word_set_bit_0 [simp]:
  2624   "set_bit 0 n b = word_of_int (bin_sc n b 0)"
  2625   unfolding word_0_wi by (rule set_bit_word_of_int)
  2626 
  2627 lemma word_set_bit_1 [simp]:
  2628   "set_bit 1 n b = word_of_int (bin_sc n b 1)"
  2629   unfolding word_1_wi by (rule set_bit_word_of_int)
  2630 
  2631 lemma setBit_no [simp]:
  2632   "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
  2633   by (simp add: setBit_def)
  2634 
  2635 lemma clearBit_no [simp]:
  2636   "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
  2637   by (simp add: clearBit_def)
  2638 
  2639 lemma to_bl_n1: 
  2640   "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
  2641   apply (rule word_bl.Abs_inverse')
  2642    apply simp
  2643   apply (rule word_eqI)
  2644   apply (clarsimp simp add: word_size)
  2645   apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
  2646   done
  2647 
  2648 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
  2649   unfolding word_msb_alt to_bl_n1 by simp
  2650 
  2651 lemma word_set_nth_iff: 
  2652   "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
  2653   apply (rule iffI)
  2654    apply (rule disjCI)
  2655    apply (drule word_eqD)
  2656    apply (erule sym [THEN trans])
  2657    apply (simp add: test_bit_set)
  2658   apply (erule disjE)
  2659    apply clarsimp
  2660   apply (rule word_eqI)
  2661   apply (clarsimp simp add : test_bit_set_gen)
  2662   apply (drule test_bit_size)
  2663   apply force
  2664   done
  2665 
  2666 lemma test_bit_2p:
  2667   "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
  2668   unfolding word_test_bit_def
  2669   by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
  2670 
  2671 lemma nth_w2p:
  2672   "((2\<Colon>'a\<Colon>len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a\<Colon>len)"
  2673   unfolding test_bit_2p [symmetric] word_of_int [symmetric]
  2674   by (simp add:  of_int_power)
  2675 
  2676 lemma uint_2p: 
  2677   "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
  2678   apply (unfold word_arith_power_alt)
  2679   apply (case_tac "len_of TYPE ('a)")
  2680    apply clarsimp
  2681   apply (case_tac "nat")
  2682    apply clarsimp
  2683    apply (case_tac "n")
  2684     apply clarsimp
  2685    apply clarsimp
  2686   apply (drule word_gt_0 [THEN iffD1])
  2687   apply (safe intro!: word_eqI)
  2688   apply (auto simp add: nth_2p_bin)
  2689   apply (erule notE)
  2690   apply (simp (no_asm_use) add: uint_word_of_int word_size)
  2691   apply (subst mod_pos_pos_trivial)
  2692   apply simp
  2693   apply (rule power_strict_increasing)
  2694   apply simp_all
  2695   done
  2696 
  2697 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n" 
  2698   apply (unfold word_arith_power_alt)
  2699   apply (case_tac "len_of TYPE ('a)")
  2700    apply clarsimp
  2701   apply (case_tac "nat")
  2702    apply (rule word_ubin.norm_eq_iff [THEN iffD1]) 
  2703    apply (rule box_equals) 
  2704      apply (rule_tac [2] bintr_ariths (1))+ 
  2705    apply simp
  2706   apply simp
  2707   done
  2708 
  2709 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)" 
  2710   apply (rule xtr3) 
  2711   apply (rule_tac [2] y = "x" in le_word_or2)
  2712   apply (rule word_eqI)
  2713   apply (auto simp add: word_ao_nth nth_w2p word_size)
  2714   done
  2715 
  2716 lemma word_clr_le: 
  2717   fixes w :: "'a::len0 word"
  2718   shows "w >= set_bit w n False"
  2719   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2720   apply (rule order_trans)
  2721    apply (rule bintr_bin_clr_le)
  2722   apply simp
  2723   done
  2724 
  2725 lemma word_set_ge: 
  2726   fixes w :: "'a::len word"
  2727   shows "w <= set_bit w n True"
  2728   apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
  2729   apply (rule order_trans [OF _ bintr_bin_set_ge])
  2730   apply simp
  2731   done
  2732 
  2733 
  2734 subsection {* Shifting, Rotating, and Splitting Words *}
  2735 
  2736 lemma shiftl1_wi [simp]: "shiftl1 (word_of_int w) = word_of_int (w BIT False)"
  2737   unfolding shiftl1_def
  2738   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
  2739   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
  2740   apply (subst bintrunc_bintrunc_min)
  2741   apply simp
  2742   done
  2743 
  2744 lemma shiftl1_numeral [simp]:
  2745   "shiftl1 (numeral w) = numeral (Num.Bit0 w)"
  2746   unfolding word_numeral_alt shiftl1_wi by simp
  2747 
  2748 lemma shiftl1_neg_numeral [simp]:
  2749   "shiftl1 (- numeral w) = - numeral (Num.Bit0 w)"
  2750   unfolding word_neg_numeral_alt shiftl1_wi by simp
  2751 
  2752 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
  2753   unfolding shiftl1_def by simp
  2754 
  2755 lemma shiftl1_def_u: "shiftl1 w = word_of_int (uint w BIT False)"
  2756   by (simp only: shiftl1_def) (* FIXME: duplicate *)
  2757 
  2758 lemma shiftl1_def_s: "shiftl1 w = word_of_int (sint w BIT False)"
  2759   unfolding shiftl1_def Bit_B0 wi_hom_syms by simp
  2760 
  2761 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
  2762   unfolding shiftr1_def by simp
  2763 
  2764 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
  2765   unfolding sshiftr1_def by simp
  2766 
  2767 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
  2768   unfolding sshiftr1_def by simp
  2769 
  2770 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
  2771   unfolding shiftl_def by (induct n) auto
  2772 
  2773 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
  2774   unfolding shiftr_def by (induct n) auto
  2775 
  2776 lemma sshiftr_0 [simp] : "0 >>> n = 0"
  2777   unfolding sshiftr_def by (induct n) auto
  2778 
  2779 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
  2780   unfolding sshiftr_def by (induct n) auto
  2781 
  2782 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
  2783   apply (unfold shiftl1_def word_test_bit_def)
  2784   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
  2785   apply (cases n)
  2786    apply auto
  2787   done
  2788 
  2789 lemma nth_shiftl' [rule_format]:
  2790   "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
  2791   apply (unfold shiftl_def)
  2792   apply (induct "m")
  2793    apply (force elim!: test_bit_size)
  2794   apply (clarsimp simp add : nth_shiftl1 word_size)
  2795   apply arith
  2796   done
  2797 
  2798 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
  2799 
  2800 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
  2801   apply (unfold shiftr1_def word_test_bit_def)
  2802   apply (simp add: nth_bintr word_ubin.eq_norm)
  2803   apply safe
  2804   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
  2805   apply simp
  2806   done
  2807 
  2808 lemma nth_shiftr: 
  2809   "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
  2810   apply (unfold shiftr_def)
  2811   apply (induct "m")
  2812    apply (auto simp add : nth_shiftr1)
  2813   done
  2814    
  2815 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
  2816   where f (ie bin_rest) takes normal arguments to normal results,
  2817   thus we get (2) from (1) *)
  2818 
  2819 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
  2820   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
  2821   apply (subst bintr_uint [symmetric, OF order_refl])
  2822   apply (simp only : bintrunc_bintrunc_l)
  2823   apply simp 
  2824   done
  2825 
  2826 lemma nth_sshiftr1: 
  2827   "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
  2828   apply (unfold sshiftr1_def word_test_bit_def)
  2829   apply (simp add: nth_bintr word_ubin.eq_norm
  2830                    bin_nth.Suc [symmetric] word_size 
  2831              del: bin_nth.simps)
  2832   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
  2833   apply (auto simp add: bin_nth_sint)
  2834   done
  2835 
  2836 lemma nth_sshiftr [rule_format] : 
  2837   "ALL n. sshiftr w m !! n = (n < size w & 
  2838     (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
  2839   apply (unfold sshiftr_def)
  2840   apply (induct_tac "m")
  2841    apply (simp add: test_bit_bl)
  2842   apply (clarsimp simp add: nth_sshiftr1 word_size)
  2843   apply safe
  2844        apply arith
  2845       apply arith
  2846      apply (erule thin_rl)
  2847      apply (case_tac n)
  2848       apply safe
  2849       apply simp
  2850      apply simp
  2851     apply (erule thin_rl)
  2852     apply (case_tac n)
  2853      apply safe
  2854      apply simp
  2855     apply simp
  2856    apply arith+
  2857   done
  2858     
  2859 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
  2860   apply (unfold shiftr1_def bin_rest_def)
  2861   apply (rule word_uint.Abs_inverse)
  2862   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
  2863   apply (rule xtr7)
  2864    prefer 2
  2865    apply (rule zdiv_le_dividend)
  2866     apply auto
  2867   done
  2868 
  2869 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
  2870   apply (unfold sshiftr1_def bin_rest_def [symmetric])
  2871   apply (simp add: word_sbin.eq_norm)
  2872   apply (rule trans)
  2873    defer
  2874    apply (subst word_sbin.norm_Rep [symmetric])
  2875    apply (rule refl)
  2876   apply (subst word_sbin.norm_Rep [symmetric])
  2877   apply (unfold One_nat_def)
  2878   apply (rule sbintrunc_rest)
  2879   done
  2880 
  2881 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
  2882   apply (unfold shiftr_def)
  2883   apply (induct "n")
  2884    apply simp
  2885   apply (simp add: shiftr1_div_2 mult_commute
  2886                    zdiv_zmult2_eq [symmetric])
  2887   done
  2888 
  2889 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
  2890   apply (unfold sshiftr_def)
  2891   apply (induct "n")
  2892    apply simp
  2893   apply (simp add: sshiftr1_div_2 mult_commute
  2894                    zdiv_zmult2_eq [symmetric])
  2895   done
  2896 
  2897 
  2898 subsubsection {* shift functions in terms of lists of bools *}
  2899 
  2900 lemmas bshiftr1_numeral [simp] = 
  2901   bshiftr1_def [where w="numeral w", unfolded to_bl_numeral] for w
  2902 
  2903 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
  2904   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
  2905 
  2906 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
  2907   by (simp add: of_bl_def bl_to_bin_append)
  2908 
  2909 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
  2910 proof -
  2911   have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
  2912   also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
  2913   finally show ?thesis .
  2914 qed
  2915 
  2916 lemma bl_shiftl1:
  2917   "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
  2918   apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
  2919   apply (fast intro!: Suc_leI)
  2920   done
  2921 
  2922 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
  2923 lemma bl_shiftl1':
  2924   "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
  2925   unfolding shiftl1_bl
  2926   by (simp add: word_rep_drop drop_Suc del: drop_append)
  2927 
  2928 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
  2929   apply (unfold shiftr1_def uint_bl of_bl_def)
  2930   apply (simp add: butlast_rest_bin word_size)
  2931   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
  2932   done
  2933 
  2934 lemma bl_shiftr1: 
  2935   "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
  2936   unfolding shiftr1_bl
  2937   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
  2938 
  2939 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
  2940 lemma bl_shiftr1':
  2941   "to_bl (shiftr1 w) = butlast (False # to_bl w)"
  2942   apply (rule word_bl.Abs_inverse')
  2943   apply (simp del: butlast.simps)
  2944   apply (simp add: shiftr1_bl of_bl_def)
  2945   done
  2946 
  2947 lemma shiftl1_rev: 
  2948   "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
  2949   apply (unfold word_reverse_def)
  2950   apply (rule word_bl.Rep_inverse' [symmetric])
  2951   apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
  2952   apply (cases "to_bl w")
  2953    apply auto
  2954   done
  2955 
  2956 lemma shiftl_rev: 
  2957   "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
  2958   apply (unfold shiftl_def shiftr_def)
  2959   apply (induct "n")
  2960    apply (auto simp add : shiftl1_rev)
  2961   done
  2962 
  2963 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
  2964   by (simp add: shiftl_rev)
  2965 
  2966 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
  2967   by (simp add: rev_shiftl)
  2968 
  2969 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
  2970   by (simp add: shiftr_rev)
  2971 
  2972 lemma bl_sshiftr1:
  2973   "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
  2974   apply (unfold sshiftr1_def uint_bl word_size)
  2975   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
  2976   apply (simp add: sint_uint)
  2977   apply (rule nth_equalityI)
  2978    apply clarsimp
  2979   apply clarsimp
  2980   apply (case_tac i)
  2981    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
  2982                         nth_bin_to_bl bin_nth.Suc [symmetric] 
  2983                         nth_sbintr 
  2984                    del: bin_nth.Suc)
  2985    apply force
  2986   apply (rule impI)
  2987   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
  2988   apply simp
  2989   done
  2990 
  2991 lemma drop_shiftr: 
  2992   "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
  2993   apply (unfold shiftr_def)
  2994   apply (induct n)
  2995    prefer 2
  2996    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
  2997    apply (rule butlast_take [THEN trans])
  2998   apply (auto simp: word_size)
  2999   done
  3000 
  3001 lemma drop_sshiftr: 
  3002   "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
  3003   apply (unfold sshiftr_def)
  3004   apply (induct n)
  3005    prefer 2
  3006    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
  3007    apply (rule butlast_take [THEN trans])
  3008   apply (auto simp: word_size)
  3009   done
  3010 
  3011 lemma take_shiftr:
  3012   "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
  3013   apply (unfold shiftr_def)
  3014   apply (induct n)
  3015    prefer 2
  3016    apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
  3017    apply (rule take_butlast [THEN trans])
  3018   apply (auto simp: word_size)
  3019   done
  3020 
  3021 lemma take_sshiftr' [rule_format] :
  3022   "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
  3023     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
  3024   apply (unfold sshiftr_def)
  3025   apply (induct n)
  3026    prefer 2
  3027    apply (simp add: bl_sshiftr1)
  3028    apply (rule impI)
  3029    apply (rule take_butlast [THEN trans])
  3030   apply (auto simp: word_size)
  3031   done
  3032 
  3033 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
  3034 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
  3035 
  3036 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
  3037   by (auto intro: append_take_drop_id [symmetric])
  3038 
  3039 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
  3040 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
  3041 
  3042 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
  3043   unfolding shiftl_def
  3044   by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
  3045 
  3046 lemma shiftl_bl:
  3047   "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
  3048 proof -
  3049   have "w << n = of_bl (to_bl w) << n" by simp
  3050   also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
  3051   finally show ?thesis .
  3052 qed
  3053 
  3054 lemmas shiftl_numeral [simp] = shiftl_def [where w="numeral w"] for w
  3055 
  3056 lemma bl_shiftl:
  3057   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
  3058   by (simp add: shiftl_bl word_rep_drop word_size)
  3059 
  3060 lemma shiftl_zero_size: 
  3061   fixes x :: "'a::len0 word"
  3062   shows "size x <= n \<Longrightarrow> x << n = 0"
  3063   apply (unfold word_size)
  3064   apply (rule word_eqI)
  3065   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
  3066   done
  3067 
  3068 (* note - the following results use 'a :: len word < number_ring *)
  3069 
  3070 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
  3071   by (simp add: shiftl1_def Bit_def wi_hom_mult [symmetric])
  3072 
  3073 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
  3074   by (simp add: shiftl1_2t)
  3075 
  3076 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
  3077   unfolding shiftl_def 
  3078   by (induct n) (auto simp: shiftl1_2t)
  3079 
  3080 lemma shiftr1_bintr [simp]:
  3081   "(shiftr1 (numeral w) :: 'a :: len0 word) =
  3082     word_of_int (bin_rest (bintrunc (len_of TYPE ('a)) (numeral w)))"
  3083   unfolding shiftr1_def word_numeral_alt
  3084   by (simp add: word_ubin.eq_norm)
  3085 
  3086 lemma sshiftr1_sbintr [simp]:
  3087   "(sshiftr1 (numeral w) :: 'a :: len word) =
  3088     word_of_int (bin_rest (sbintrunc (len_of TYPE ('a) - 1) (numeral w)))"
  3089   unfolding sshiftr1_def word_numeral_alt
  3090   by (simp add: word_sbin.eq_norm)
  3091 
  3092 lemma shiftr_no [simp]:
  3093   (* FIXME: neg_numeral *)
  3094   "(numeral w::'a::len0 word) >> n = word_of_int
  3095     ((bin_rest ^^ n) (bintrunc (len_of TYPE('a)) (numeral w)))"
  3096   apply (rule word_eqI)
  3097   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
  3098   done
  3099 
  3100 lemma sshiftr_no [simp]:
  3101   (* FIXME: neg_numeral *)
  3102   "(numeral w::'a::len word) >>> n = word_of_int
  3103     ((bin_rest ^^ n) (sbintrunc (len_of TYPE('a) - 1) (numeral w)))"
  3104   apply (rule word_eqI)
  3105   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
  3106    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
  3107   done
  3108 
  3109 lemma shiftr1_bl_of:
  3110   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3111     shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
  3112   by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin 
  3113                      word_ubin.eq_norm trunc_bl2bin)
  3114 
  3115 lemma shiftr_bl_of:
  3116   "length bl \<le> len_of TYPE('a) \<Longrightarrow>
  3117     (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
  3118   apply (unfold shiftr_def)
  3119   apply (induct n)
  3120    apply clarsimp
  3121   apply clarsimp
  3122   apply (subst shiftr1_bl_of)
  3123    apply simp
  3124   apply (simp add: butlast_take)
  3125   done
  3126 
  3127 lemma shiftr_bl:
  3128   "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
  3129   using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
  3130 
  3131 lemma msb_shift:
  3132   "msb (w::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
  3133   apply (unfold shiftr_bl word_msb_alt)
  3134   apply (simp add: word_size Suc_le_eq take_Suc)
  3135   apply (cases "hd (to_bl w)")
  3136    apply (auto simp: word_1_bl
  3137                      of_bl_rep_False [where n=1 and bs="[]", simplified])
  3138   done
  3139 
  3140 lemma align_lem_or [rule_format] :
  3141   "ALL x m. length x = n + m --> length y = n + m --> 
  3142     drop m x = replicate n False --> take m y = replicate m False --> 
  3143     map2 op | x y = take m x @ drop m y"
  3144   apply (induct_tac y)
  3145    apply force
  3146   apply clarsimp
  3147   apply (case_tac x, force)
  3148   apply (case_tac m, auto)
  3149   apply (drule sym)
  3150   apply auto
  3151   apply (induct_tac list, auto)
  3152   done
  3153 
  3154 lemma align_lem_and [rule_format] :
  3155   "ALL x m. length x = n + m --> length y = n + m --> 
  3156     drop m x = replicate n False --> take m y = replicate m False --> 
  3157     map2 op & x y = replicate (n + m) False"
  3158   apply (induct_tac y)
  3159    apply force
  3160   apply clarsimp
  3161   apply (case_tac x, force)
  3162   apply (case_tac m, auto)
  3163   apply (drule sym)
  3164   apply auto
  3165   apply (induct_tac list, auto)
  3166   done
  3167 
  3168 lemma aligned_bl_add_size [OF refl]:
  3169   "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
  3170     take m (to_bl y) = replicate m False \<Longrightarrow> 
  3171     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
  3172   apply (subgoal_tac "x AND y = 0")
  3173    prefer 2
  3174    apply (rule word_bl.Rep_eqD)
  3175    apply (simp add: bl_word_and)
  3176    apply (rule align_lem_and [THEN trans])
  3177        apply (simp_all add: word_size)[5]
  3178    apply simp
  3179   apply (subst word_plus_and_or [symmetric])
  3180   apply (simp add : bl_word_or)
  3181   apply (rule align_lem_or)
  3182      apply (simp_all add: word_size)
  3183   done
  3184 
  3185 
  3186 subsubsection {* Mask *}
  3187 
  3188 lemma nth_mask [OF refl, simp]:
  3189   "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
  3190   apply (unfold mask_def test_bit_bl)
  3191   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
  3192   apply (clarsimp simp add: word_size)
  3193   apply (simp only: of_bl_def mask_lem word_of_int_hom_syms add_diff_cancel2)
  3194   apply (fold of_bl_def)
  3195   apply (simp add: word_1_bl)
  3196   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
  3197   apply auto
  3198   done
  3199 
  3200 lemma mask_bl: "mask n = of_bl (replicate n True)"
  3201   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
  3202 
  3203 lemma mask_bin: "mask n = word_of_int (bintrunc n -1)"
  3204   by (auto simp add: nth_bintr word_size intro: word_eqI)
  3205 
  3206 lemma and_mask_bintr: "w AND mask n = word_of_int (bintrunc n (uint w))"
  3207   apply (rule word_eqI)
  3208   apply (simp add: nth_bintr word_size word_ops_nth_size)
  3209   apply (auto simp add: test_bit_bin)
  3210   done
  3211 
  3212 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
  3213   by (auto simp add: nth_bintr word_size word_ops_nth_size word_eq_iff)
  3214 
  3215 lemma and_mask_no: "numeral i AND mask n = word_of_int (bintrunc n (numeral i))"
  3216   unfolding word_numeral_alt by (rule and_mask_wi)
  3217 
  3218 lemma bl_and_mask':
  3219   "to_bl (w AND mask n :: 'a :: len word) = 
  3220     replicate (len_of TYPE('a) - n) False @ 
  3221     drop (len_of TYPE('a) - n) (to_bl w)"
  3222   apply (rule nth_equalityI)
  3223    apply simp
  3224   apply (clarsimp simp add: to_bl_nth word_size)
  3225   apply (simp add: word_size word_ops_nth_size)
  3226   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
  3227   done
  3228 
  3229 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
  3230   by (simp only: and_mask_bintr bintrunc_mod2p)
  3231 
  3232 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
  3233   apply (simp add: and_mask_bintr word_ubin.eq_norm)
  3234   apply (simp add: bintrunc_mod2p)
  3235   apply (rule xtr8)
  3236    prefer 2
  3237    apply (rule pos_mod_bound)
  3238   apply auto
  3239   done
  3240 
  3241 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  3242   by (simp add: int_mod_lem eq_sym_conv)
  3243 
  3244 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
  3245   apply (simp add: and_mask_bintr)
  3246   apply (simp add: word_ubin.inverse_norm)
  3247   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
  3248   apply (fast intro!: lt2p_lem)
  3249   done
  3250 
  3251 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
  3252   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
  3253   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
  3254     del: word_of_int_0)
  3255   apply (subst word_uint.norm_Rep [symmetric])
  3256   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
  3257   apply auto
  3258   done
  3259 
  3260 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
  3261   apply (unfold unat_def)
  3262   apply (rule trans [OF _ and_mask_dvd])
  3263   apply (unfold dvd_def) 
  3264   apply auto 
  3265   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
  3266   apply (simp add : int_mult int_power)
  3267   apply (simp add : nat_mult_distrib nat_power_eq)
  3268   done
  3269 
  3270 lemma word_2p_lem: 
  3271   "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
  3272   apply (unfold word_size word_less_alt word_numeral_alt)
  3273   apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
  3274                             mod_pos_pos_trivial
  3275                   simp del: word_of_int_numeral)
  3276   done
  3277 
  3278 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
  3279   apply (unfold word_less_alt word_numeral_alt)
  3280   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
  3281                             word_uint.eq_norm
  3282                   simp del: word_of_int_numeral)
  3283   apply (drule xtr8 [rotated])
  3284   apply (rule int_mod_le)
  3285   apply (auto simp add : mod_pos_pos_trivial)
  3286   done
  3287 
  3288 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
  3289 
  3290 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
  3291 
  3292 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
  3293   unfolding word_size by (erule and_mask_less')
  3294 
  3295 lemma word_mod_2p_is_mask [OF refl]:
  3296   "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n" 
  3297   by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
  3298 
  3299 lemma mask_eqs:
  3300   "(a AND mask n) + b AND mask n = a + b AND mask n"
  3301   "a + (b AND mask n) AND mask n = a + b AND mask n"
  3302   "(a AND mask n) - b AND mask n = a - b AND mask n"
  3303   "a - (b AND mask n) AND mask n = a - b AND mask n"
  3304   "a * (b AND mask n) AND mask n = a * b AND mask n"
  3305   "(b AND mask n) * a AND mask n = b * a AND mask n"
  3306   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
  3307   "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
  3308   "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
  3309   "- (a AND mask n) AND mask n = - a AND mask n"
  3310   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
  3311   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
  3312   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
  3313   by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
  3314 
  3315 lemma mask_power_eq:
  3316   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
  3317   using word_of_int_Ex [where x=x]
  3318   by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
  3319 
  3320 
  3321 subsubsection {* Revcast *}
  3322 
  3323 lemmas revcast_def' = revcast_def [simplified]
  3324 lemmas revcast_def'' = revcast_def' [simplified word_size]
  3325 lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
  3326 
  3327 lemma to_bl_revcast: 
  3328   "to_bl (revcast w :: 'a :: len0 word) = 
  3329    takefill False (len_of TYPE ('a)) (to_bl w)"
  3330   apply (unfold revcast_def' word_size)
  3331   apply (rule word_bl.Abs_inverse)
  3332   apply simp
  3333   done
  3334 
  3335 lemma revcast_rev_ucast [OF refl refl refl]: 
  3336   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow> 
  3337     rc = word_reverse uc"
  3338   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
  3339   apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
  3340   apply (simp add : word_bl.Abs_inverse word_size)
  3341   done
  3342 
  3343 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
  3344   using revcast_rev_ucast [of "word_reverse w"] by simp
  3345 
  3346 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
  3347   by (fact revcast_rev_ucast [THEN word_rev_gal'])
  3348 
  3349 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
  3350   by (fact revcast_ucast [THEN word_rev_gal'])
  3351 
  3352 
  3353 -- "linking revcast and cast via shift"
  3354 
  3355 lemmas wsst_TYs = source_size target_size word_size
  3356 
  3357 lemma revcast_down_uu [OF refl]:
  3358   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3359     rc (w :: 'a :: len word) = ucast (w >> n)"
  3360   apply (simp add: revcast_def')
  3361   apply (rule word_bl.Rep_inverse')
  3362   apply (rule trans, rule ucast_down_drop)
  3363    prefer 2
  3364    apply (rule trans, rule drop_shiftr)
  3365    apply (auto simp: takefill_alt wsst_TYs)
  3366   done
  3367 
  3368 lemma revcast_down_us [OF refl]:
  3369   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3370     rc (w :: 'a :: len word) = ucast (w >>> n)"
  3371   apply (simp add: revcast_def')
  3372   apply (rule word_bl.Rep_inverse')
  3373   apply (rule trans, rule ucast_down_drop)
  3374    prefer 2
  3375    apply (rule trans, rule drop_sshiftr)
  3376    apply (auto simp: takefill_alt wsst_TYs)
  3377   done
  3378 
  3379 lemma revcast_down_su [OF refl]:
  3380   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3381     rc (w :: 'a :: len word) = scast (w >> n)"
  3382   apply (simp add: revcast_def')
  3383   apply (rule word_bl.Rep_inverse')
  3384   apply (rule trans, rule scast_down_drop)
  3385    prefer 2
  3386    apply (rule trans, rule drop_shiftr)
  3387    apply (auto simp: takefill_alt wsst_TYs)
  3388   done
  3389 
  3390 lemma revcast_down_ss [OF refl]:
  3391   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> 
  3392     rc (w :: 'a :: len word) = scast (w >>> n)"
  3393   apply (simp add: revcast_def')
  3394   apply (rule word_bl.Rep_inverse')
  3395   apply (rule trans, rule scast_down_drop)
  3396    prefer 2
  3397    apply (rule trans, rule drop_sshiftr)
  3398    apply (auto simp: takefill_alt wsst_TYs)
  3399   done
  3400 
  3401 (* FIXME: should this also be [OF refl] ? *)
  3402 lemma cast_down_rev: 
  3403   "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow> 
  3404     uc w = revcast ((w :: 'a :: len word) << n)"
  3405   apply (unfold shiftl_rev)
  3406   apply clarify
  3407   apply (simp add: revcast_rev_ucast)
  3408   apply (rule word_rev_gal')
  3409   apply (rule trans [OF _ revcast_rev_ucast])
  3410   apply (rule revcast_down_uu [symmetric])
  3411   apply (auto simp add: wsst_TYs)
  3412   done
  3413 
  3414 lemma revcast_up [OF refl]:
  3415   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow> 
  3416     rc w = (ucast w :: 'a :: len word) << n" 
  3417   apply (simp add: revcast_def')
  3418   apply (rule word_bl.Rep_inverse')
  3419   apply (simp add: takefill_alt)
  3420   apply (rule bl_shiftl [THEN trans])
  3421   apply (subst ucast_up_app)
  3422   apply (auto simp add: wsst_TYs)
  3423   done
  3424 
  3425 lemmas rc1 = revcast_up [THEN 
  3426   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3427 lemmas rc2 = revcast_down_uu [THEN 
  3428   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
  3429 
  3430 lemmas ucast_up =
  3431  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
  3432 lemmas ucast_down = 
  3433   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
  3434 
  3435 
  3436 subsubsection {* Slices *}
  3437 
  3438 lemma slice1_no_bin [simp]:
  3439   "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3440   by (simp add: slice1_def) (* TODO: neg_numeral *)
  3441 
  3442 lemma slice_no_bin [simp]:
  3443   "slice n (numeral w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
  3444     (bin_to_bl (len_of TYPE('b :: len0)) (numeral w)))"
  3445   by (simp add: slice_def word_size) (* TODO: neg_numeral *)
  3446 
  3447 lemma slice1_0 [simp] : "slice1 n 0 = 0"
  3448   unfolding slice1_def by simp
  3449 
  3450 lemma slice_0 [simp] : "slice n 0 = 0"
  3451   unfolding slice_def by auto
  3452 
  3453 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
  3454   unfolding slice_def' slice1_def
  3455   by (simp add : takefill_alt word_size)
  3456 
  3457 lemmas slice_take = slice_take' [unfolded word_size]
  3458 
  3459 -- "shiftr to a word of the same size is just slice, 
  3460     slice is just shiftr then ucast"
  3461 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
  3462 
  3463 lemma slice_shiftr: "slice n w = ucast (w >> n)"
  3464   apply (unfold slice_take shiftr_bl)
  3465   apply (rule ucast_of_bl_up [symmetric])
  3466   apply (simp add: word_size)
  3467   done
  3468 
  3469 lemma nth_slice: 
  3470   "(slice n w :: 'a :: len0 word) !! m = 
  3471    (w !! (m + n) & m < len_of TYPE ('a))"
  3472   unfolding slice_shiftr 
  3473   by (simp add : nth_ucast nth_shiftr)
  3474 
  3475 lemma slice1_down_alt': 
  3476   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow> 
  3477     to_bl sl = takefill False fs (drop k (to_bl w))"
  3478   unfolding slice1_def word_size of_bl_def uint_bl
  3479   by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
  3480 
  3481 lemma slice1_up_alt': 
  3482   "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow> 
  3483     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
  3484   apply (unfold slice1_def word_size of_bl_def uint_bl)
  3485   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
  3486                         takefill_append [symmetric])
  3487   apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
  3488     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
  3489   apply arith
  3490   done
  3491     
  3492 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
  3493 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
  3494 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
  3495 lemmas slice1_up_alts = 
  3496   le_add_diff_inverse [symmetric, THEN su1] 
  3497   le_add_diff_inverse2 [symmetric, THEN su1]
  3498 
  3499 lemma ucast_slice1: "ucast w = slice1 (size w) w"
  3500   unfolding slice1_def ucast_bl
  3501   by (simp add : takefill_same' word_size)
  3502 
  3503 lemma ucast_slice: "ucast w = slice 0 w"
  3504   unfolding slice_def by (simp add : ucast_slice1)
  3505 
  3506 lemma slice_id: "slice 0 t = t"
  3507   by (simp only: ucast_slice [symmetric] ucast_id)
  3508 
  3509 lemma revcast_slice1 [OF refl]: 
  3510   "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
  3511   unfolding slice1_def revcast_def' by (simp add : word_size)
  3512 
  3513 lemma slice1_tf_tf': 
  3514   "to_bl (slice1 n w :: 'a :: len0 word) = 
  3515    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
  3516   unfolding slice1_def by (rule word_rev_tf)
  3517 
  3518 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
  3519 
  3520 lemma rev_slice1:
  3521   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
  3522   slice1 n (word_reverse w :: 'b :: len0 word) = 
  3523   word_reverse (slice1 k w :: 'a :: len0 word)"
  3524   apply (unfold word_reverse_def slice1_tf_tf)
  3525   apply (rule word_bl.Rep_inverse')
  3526   apply (rule rev_swap [THEN iffD1])
  3527   apply (rule trans [symmetric])
  3528   apply (rule tf_rev)
  3529    apply (simp add: word_bl.Abs_inverse)
  3530   apply (simp add: word_bl.Abs_inverse)
  3531   done
  3532 
  3533 lemma rev_slice:
  3534   "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
  3535     slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
  3536   apply (unfold slice_def word_size)
  3537   apply (rule rev_slice1)
  3538   apply arith
  3539   done
  3540 
  3541 lemmas sym_notr = 
  3542   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
  3543 
  3544 -- {* problem posed by TPHOLs referee:
  3545       criterion for overflow of addition of signed integers *}
  3546 
  3547 lemma sofl_test:
  3548   "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
  3549      ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
  3550   apply (unfold word_size)
  3551   apply (cases "len_of TYPE('a)", simp) 
  3552   apply (subst msb_shift [THEN sym_notr])
  3553   apply (simp add: word_ops_msb)
  3554   apply (simp add: word_msb_sint)
  3555   apply safe
  3556        apply simp_all
  3557      apply (unfold sint_word_ariths)
  3558      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
  3559      apply safe
  3560         apply (insert sint_range' [where x=x])
  3561         apply (insert sint_range' [where x=y])
  3562         defer 
  3563         apply (simp (no_asm), arith)
  3564        apply (simp (no_asm), arith)
  3565       defer
  3566       defer
  3567       apply (simp (no_asm), arith)
  3568      apply (simp (no_asm), arith)
  3569     apply (rule notI [THEN notnotD],
  3570            drule leI not_leE,
  3571            drule sbintrunc_inc sbintrunc_dec,      
  3572            simp)+
  3573   done
  3574 
  3575 
  3576 subsection {* Split and cat *}
  3577 
  3578 lemmas word_split_bin' = word_split_def
  3579 lemmas word_cat_bin' = word_cat_def
  3580 
  3581 lemma word_rsplit_no:
  3582   "(word_rsplit (numeral bin :: 'b :: len0 word) :: 'a word list) = 
  3583     map word_of_int (bin_rsplit (len_of TYPE('a :: len)) 
  3584       (len_of TYPE('b), bintrunc (len_of TYPE('b)) (numeral bin)))"
  3585   unfolding word_rsplit_def by (simp add: word_ubin.eq_norm)
  3586 
  3587 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
  3588   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
  3589 
  3590 lemma test_bit_cat:
  3591   "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc & 
  3592     (if n < size b then b !! n else a !! (n - size b)))"
  3593   apply (unfold word_cat_bin' test_bit_bin)
  3594   apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
  3595   apply (erule bin_nth_uint_imp)
  3596   done
  3597 
  3598 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
  3599   apply (unfold of_bl_def to_bl_def word_cat_bin')
  3600   apply (simp add: bl_to_bin_app_cat)
  3601   done
  3602 
  3603 lemma of_bl_append:
  3604   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
  3605   apply (unfold of_bl_def)
  3606   apply (simp add: bl_to_bin_app_cat bin_cat_num)
  3607   apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
  3608   done
  3609 
  3610 lemma of_bl_False [simp]:
  3611   "of_bl (False#xs) = of_bl xs"
  3612   by (rule word_eqI)
  3613      (auto simp add: test_bit_of_bl nth_append)
  3614 
  3615 lemma of_bl_True [simp]:
  3616   "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
  3617   by (subst of_bl_append [where xs="[True]", simplified])
  3618      (simp add: word_1_bl)
  3619 
  3620 lemma of_bl_Cons:
  3621   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
  3622   by (cases x) simp_all
  3623 
  3624 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow> 
  3625   a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
  3626   apply (frule word_ubin.norm_Rep [THEN ssubst])
  3627   apply (drule bin_split_trunc1)
  3628   apply (drule sym [THEN trans])
  3629   apply assumption
  3630   apply safe
  3631   done
  3632 
  3633 lemma word_split_bl': 
  3634   "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow> 
  3635     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
  3636   apply (unfold word_split_bin')
  3637   apply safe
  3638    defer
  3639    apply (clarsimp split: prod.splits)
  3640    apply (drule word_ubin.norm_Rep [THEN ssubst])
  3641    apply (drule split_bintrunc)
  3642    apply (simp add : of_bl_def bl2bin_drop word_size
  3643        word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
  3644   apply (clarsimp split: prod.splits)
  3645   apply (frule split_uint_lem [THEN conjunct1])
  3646   apply (unfold word_size)
  3647   apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
  3648    defer
  3649    apply simp
  3650   apply (simp add : of_bl_def to_bl_def)
  3651   apply (subst bin_split_take1 [symmetric])
  3652     prefer 2
  3653     apply assumption
  3654    apply simp
  3655   apply (erule thin_rl)
  3656   apply (erule arg_cong [THEN trans])
  3657   apply (simp add : word_ubin.norm_eq_iff [symmetric])
  3658   done
  3659 
  3660 lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
  3661     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
  3662     word_split c = (a, b)"
  3663   apply (rule iffI)
  3664    defer
  3665    apply (erule (1) word_split_bl')
  3666   apply (case_tac "word_split c")
  3667   apply (auto simp add : word_size)
  3668   apply (frule word_split_bl' [rotated])
  3669   apply (auto simp add : word_size)
  3670   done
  3671 
  3672 lemma word_split_bl_eq:
  3673    "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
  3674       (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
  3675        of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
  3676   apply (rule word_split_bl [THEN iffD1])
  3677   apply (unfold word_size)
  3678   apply (rule refl conjI)+
  3679   done
  3680 
  3681 -- "keep quantifiers for use in simplification"
  3682 lemma test_bit_split':
  3683   "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
  3684     a !! m = (m < size a & c !! (m + size b)))"
  3685   apply (unfold word_split_bin' test_bit_bin)
  3686   apply (clarify)
  3687   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
  3688   apply (drule bin_nth_split)
  3689   apply safe
  3690        apply (simp_all add: add_commute)
  3691    apply (erule bin_nth_uint_imp)+
  3692   done
  3693 
  3694 lemma test_bit_split:
  3695   "word_split c = (a, b) \<Longrightarrow>
  3696     (\<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))"
  3697   by (simp add: test_bit_split')
  3698 
  3699 lemma test_bit_split_eq: "word_split c = (a, b) <-> 
  3700   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
  3701     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
  3702   apply (rule_tac iffI)
  3703    apply (rule_tac conjI)
  3704     apply (erule test_bit_split [THEN conjunct1])
  3705    apply (erule test_bit_split [THEN conjunct2])
  3706   apply (case_tac "word_split c")
  3707   apply (frule test_bit_split)
  3708   apply (erule trans)
  3709   apply (fastforce intro ! : word_eqI simp add : word_size)
  3710   done
  3711 
  3712 -- {* this odd result is analogous to @{text "ucast_id"}, 
  3713       result to the length given by the result type *}
  3714 
  3715 lemma word_cat_id: "word_cat a b = b"
  3716   unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
  3717 
  3718 -- "limited hom result"
  3719 lemma word_cat_hom:
  3720   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  3721   \<Longrightarrow>
  3722   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
  3723   word_of_int (bin_cat w (size b) (uint b))"
  3724   apply (unfold word_cat_def word_size) 
  3725   apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
  3726       word_ubin.eq_norm bintr_cat min.absorb1)
  3727   done
  3728 
  3729 lemma word_cat_split_alt:
  3730   "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
  3731   apply (rule word_eqI)
  3732   apply (drule test_bit_split)
  3733   apply (clarsimp simp add : test_bit_cat word_size)
  3734   apply safe
  3735   apply arith
  3736   done
  3737 
  3738 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
  3739 
  3740 
  3741 subsubsection {* Split and slice *}
  3742 
  3743 lemma split_slices: 
  3744   "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
  3745   apply (drule test_bit_split)
  3746   apply (rule conjI)
  3747    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  3748   done
  3749 
  3750 lemma slice_cat1 [OF refl]:
  3751   "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
  3752   apply safe
  3753   apply (rule word_eqI)
  3754   apply (simp add: nth_slice test_bit_cat word_size)
  3755   done
  3756 
  3757 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  3758 
  3759 lemma cat_slices:
  3760   "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
  3761     size a + size b >= size c \<Longrightarrow> word_cat a b = c"
  3762   apply safe
  3763   apply (rule word_eqI)
  3764   apply (simp add: nth_slice test_bit_cat word_size)
  3765   apply safe
  3766   apply arith
  3767   done
  3768 
  3769 lemma word_split_cat_alt:
  3770   "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
  3771   apply (case_tac "word_split ?w")
  3772   apply (rule trans, assumption)
  3773   apply (drule test_bit_split)
  3774   apply safe
  3775    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  3776   done
  3777 
  3778 lemmas word_cat_bl_no_bin [simp] =
  3779   word_cat_bl [where a="numeral a" and b="numeral b",
  3780     unfolded to_bl_numeral]
  3781   for a b (* FIXME: negative numerals, 0 and 1 *)
  3782 
  3783 lemmas word_split_bl_no_bin [simp] =
  3784   word_split_bl_eq [where c="numeral c", unfolded to_bl_numeral] for c
  3785 
  3786 text {* this odd result arises from the fact that the statement of the
  3787       result implies that the decoded words are of the same type, 
  3788       and therefore of the same length, as the original word *}
  3789 
  3790 lemma word_rsplit_same: "word_rsplit w = [w]"
  3791   unfolding word_rsplit_def by (simp add : bin_rsplit_all)
  3792 
  3793 lemma word_rsplit_empty_iff_size:
  3794   "(word_rsplit w = []) = (size w = 0)" 
  3795   unfolding word_rsplit_def bin_rsplit_def word_size
  3796   by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
  3797 
  3798 lemma test_bit_rsplit:
  3799   "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow> 
  3800     k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  3801   apply (unfold word_rsplit_def word_test_bit_def)
  3802   apply (rule trans)
  3803    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  3804    apply (rule nth_map [symmetric])
  3805    apply simp
  3806   apply (rule bin_nth_rsplit)
  3807      apply simp_all
  3808   apply (simp add : word_size rev_map)
  3809   apply (rule trans)
  3810    defer
  3811    apply (rule map_ident [THEN fun_cong])
  3812   apply (rule refl [THEN map_cong])
  3813   apply (simp add : word_ubin.eq_norm)
  3814   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  3815   done
  3816 
  3817 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
  3818   unfolding word_rcat_def to_bl_def' of_bl_def
  3819   by (clarsimp simp add : bin_rcat_bl)
  3820 
  3821 lemma size_rcat_lem':
  3822   "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  3823   unfolding word_size by (induct wl) auto
  3824 
  3825 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  3826 
  3827 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
  3828 
  3829 lemma nth_rcat_lem:
  3830   "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
  3831     rev (concat (map to_bl wl)) ! n =
  3832     rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
  3833   apply (induct "wl")
  3834    apply clarsimp
  3835   apply (clarsimp simp add : nth_append size_rcat_lem)
  3836   apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
  3837          td_gal_lt_len less_Suc_eq_le mod_div_equality')
  3838   apply clarsimp
  3839   done
  3840 
  3841 lemma test_bit_rcat:
  3842   "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n = 
  3843     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
  3844   apply (unfold word_rcat_bl word_size)
  3845   apply (clarsimp simp add : 
  3846     test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  3847   apply safe
  3848    apply (auto simp add : 
  3849     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  3850   done
  3851 
  3852 lemma foldl_eq_foldr:
  3853   "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
  3854   by (induct xs arbitrary: x) (auto simp add : add_assoc)
  3855 
  3856 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  3857 
  3858 lemmas test_bit_rsplit_alt = 
  3859   trans [OF nth_rev_alt [THEN test_bit_cong] 
  3860   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  3861 
  3862 -- "lazy way of expressing that u and v, and su and sv, have same types"
  3863 lemma word_rsplit_len_indep [OF refl refl refl refl]:
  3864   "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow> 
  3865     word_rsplit v = sv \<Longrightarrow> length su = length sv"
  3866   apply (unfold word_rsplit_def)
  3867   apply (auto simp add : bin_rsplit_len_indep)
  3868   done
  3869 
  3870 lemma length_word_rsplit_size: 
  3871   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3872     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
  3873   apply (unfold word_rsplit_def word_size)
  3874   apply (clarsimp simp add : bin_rsplit_len_le)
  3875   done
  3876 
  3877 lemmas length_word_rsplit_lt_size = 
  3878   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  3879 
  3880 lemma length_word_rsplit_exp_size:
  3881   "n = len_of TYPE ('a :: len) \<Longrightarrow> 
  3882     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  3883   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
  3884 
  3885 lemma length_word_rsplit_even_size: 
  3886   "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow> 
  3887     length (word_rsplit w :: 'a word list) = m"
  3888   by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
  3889 
  3890 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  3891 
  3892 (* alternative proof of word_rcat_rsplit *)
  3893 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
  3894 lemmas dtle = xtr4 [OF tdle mult_commute]
  3895 
  3896 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  3897   apply (rule word_eqI)
  3898   apply (clarsimp simp add : test_bit_rcat word_size)
  3899   apply (subst refl [THEN test_bit_rsplit])
  3900     apply (simp_all add: word_size 
  3901       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  3902    apply safe
  3903    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  3904   done
  3905 
  3906 lemma size_word_rsplit_rcat_size:
  3907   "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
  3908      size frcw = length ws * len_of TYPE('a)\<rbrakk>
  3909     \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
  3910   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
  3911   apply (fast intro: given_quot_alt)
  3912   done
  3913 
  3914 lemma msrevs:
  3915   fixes n::nat
  3916   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  3917   and   "(k * n + m) mod n = m mod n"
  3918   by (auto simp: add_commute)
  3919 
  3920 lemma word_rsplit_rcat_size [OF refl]:
  3921   "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow> 
  3922     size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws" 
  3923   apply (frule size_word_rsplit_rcat_size, assumption)
  3924   apply (clarsimp simp add : word_size)
  3925   apply (rule nth_equalityI, assumption)
  3926   apply clarsimp
  3927   apply (rule word_eqI [rule_format])
  3928   apply (rule trans)
  3929    apply (rule test_bit_rsplit_alt)
  3930      apply (clarsimp simp: word_size)+
  3931   apply (rule trans)
  3932   apply (rule test_bit_rcat [OF refl refl])
  3933   apply (simp add: word_size msrevs)
  3934   apply (subst nth_rev)
  3935    apply arith
  3936   apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
  3937   apply safe
  3938   apply (simp add: diff_mult_distrib)
  3939   apply (rule mpl_lem)
  3940   apply (cases "size ws")
  3941    apply simp_all
  3942   done
  3943 
  3944 
  3945 subsection {* Rotation *}
  3946 
  3947 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  3948 
  3949 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  3950 
  3951 lemma rotate_eq_mod: 
  3952   "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
  3953   apply (rule box_equals)
  3954     defer
  3955     apply (rule rotate_conv_mod [symmetric])+
  3956   apply simp
  3957   done
  3958 
  3959 lemmas rotate_eqs = 
  3960   trans [OF rotate0 [THEN fun_cong] id_apply]
  3961   rotate_rotate [symmetric] 
  3962   rotate_id
  3963   rotate_conv_mod 
  3964   rotate_eq_mod
  3965 
  3966 
  3967 subsubsection {* Rotation of list to right *}
  3968 
  3969 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  3970   unfolding rotater1_def by (cases l) auto
  3971 
  3972 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  3973   apply (unfold rotater1_def)
  3974   apply (cases "l")
  3975   apply (case_tac [2] "list")
  3976   apply auto
  3977   done
  3978 
  3979 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  3980   unfolding rotater1_def by (cases l) auto
  3981 
  3982 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  3983   apply (cases "xs")
  3984   apply (simp add : rotater1_def)
  3985   apply (simp add : rotate1_rl')
  3986   done
  3987   
  3988 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  3989   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
  3990 
  3991 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
  3992   using rotater_rev' [where xs = "rev ys"] by simp
  3993 
  3994 lemma rotater_drop_take: 
  3995   "rotater n xs = 
  3996    drop (length xs - n mod length xs) xs @
  3997    take (length xs - n mod length xs) xs"
  3998   by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
  3999 
  4000 lemma rotater_Suc [simp] : 
  4001   "rotater (Suc n) xs = rotater1 (rotater n xs)"
  4002   unfolding rotater_def by auto
  4003 
  4004 lemma rotate_inv_plus [rule_format] :
  4005   "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs & 
  4006     rotate k (rotater n xs) = rotate m xs & 
  4007     rotater n (rotate k xs) = rotate m xs & 
  4008     rotate n (rotater k xs) = rotater m xs"
  4009   unfolding rotater_def rotate_def
  4010   by (induct n) (auto intro: funpow_swap1 [THEN trans])
  4011   
  4012 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  4013 
  4014 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  4015 
  4016 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
  4017 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
  4018 
  4019 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
  4020   by auto
  4021 
  4022 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
  4023   by auto
  4024 
  4025 lemma length_rotater [simp]: 
  4026   "length (rotater n xs) = length xs"
  4027   by (simp add : rotater_rev)
  4028 
  4029 lemma restrict_to_left:
  4030   assumes "x = y"
  4031   shows "(x = z) = (y = z)"
  4032   using assms by simp
  4033 
  4034 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
  4035   simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
  4036 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  4037 lemmas rotater_eqs = rrs1 [simplified length_rotater]
  4038 lemmas rotater_0 = rotater_eqs (1)
  4039 lemmas rotater_add = rotater_eqs (2)
  4040 
  4041 
  4042 subsubsection {* map, map2, commuting with rotate(r) *}
  4043 
  4044 lemma butlast_map:
  4045   "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
  4046   by (induct xs) auto
  4047 
  4048 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
  4049   unfolding rotater1_def
  4050   by (cases xs) (auto simp add: last_map butlast_map)
  4051 
  4052 lemma rotater_map:
  4053   "rotater n (map f xs) = map f (rotater n xs)" 
  4054   unfolding rotater_def
  4055   by (induct n) (auto simp add : rotater1_map)
  4056 
  4057 lemma but_last_zip [rule_format] :
  4058   "ALL ys. length xs = length ys --> xs ~= [] --> 
  4059     last (zip xs ys) = (last xs, last ys) & 
  4060     butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 
  4061   apply (induct "xs")
  4062   apply auto
  4063      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  4064   done
  4065 
  4066 lemma but_last_map2 [rule_format] :
  4067   "ALL ys. length xs = length ys --> xs ~= [] --> 
  4068     last (map2 f xs ys) = f (last xs) (last ys) & 
  4069     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 
  4070   apply (induct "xs")
  4071   apply auto
  4072      apply (unfold map2_def)
  4073      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  4074   done
  4075 
  4076 lemma rotater1_zip:
  4077   "length xs = length ys \<Longrightarrow> 
  4078     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  4079   apply (unfold rotater1_def)
  4080   apply (cases "xs")
  4081    apply auto
  4082    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  4083   done
  4084 
  4085 lemma rotater1_map2:
  4086   "length xs = length ys \<Longrightarrow> 
  4087     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
  4088   unfolding map2_def by (simp add: rotater1_map rotater1_zip)
  4089 
  4090 lemmas lrth = 
  4091   box_equals [OF asm_rl length_rotater [symmetric] 
  4092                  length_rotater [symmetric], 
  4093               THEN rotater1_map2]
  4094 
  4095 lemma rotater_map2: 
  4096   "length xs = length ys \<Longrightarrow> 
  4097     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
  4098   by (induct n) (auto intro!: lrth)
  4099 
  4100 lemma rotate1_map2:
  4101   "length xs = length ys \<Longrightarrow> 
  4102     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  4103   apply (unfold map2_def)
  4104   apply (cases xs)
  4105    apply (cases ys, auto)+
  4106   done
  4107 
  4108 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
  4109   length_rotate [symmetric], THEN rotate1_map2]
  4110 
  4111 lemma rotate_map2: 
  4112   "length xs = length ys \<Longrightarrow> 
  4113     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
  4114   by (induct n) (auto intro!: lth)
  4115 
  4116 
  4117 -- "corresponding equalities for word rotation"
  4118 
  4119 lemma to_bl_rotl: 
  4120   "to_bl (word_rotl n w) = rotate n (to_bl w)"
  4121   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  4122 
  4123 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  4124 
  4125 lemmas word_rotl_eqs =
  4126   blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  4127 
  4128 lemma to_bl_rotr: 
  4129   "to_bl (word_rotr n w) = rotater n (to_bl w)"
  4130   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  4131 
  4132 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  4133 
  4134 lemmas word_rotr_eqs =
  4135   brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  4136 
  4137 declare word_rotr_eqs (1) [simp]
  4138 declare word_rotl_eqs (1) [simp]
  4139 
  4140 lemma
  4141   word_rot_rl [simp]:
  4142   "word_rotl k (word_rotr k v) = v" and
  4143   word_rot_lr [simp]:
  4144   "word_rotr k (word_rotl k v) = v"
  4145   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  4146 
  4147 lemma
  4148   word_rot_gal:
  4149   "(word_rotr n v = w) = (word_rotl n w = v)" and
  4150   word_rot_gal':
  4151   "(w = word_rotr n v) = (v = word_rotl n w)"
  4152   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] 
  4153            dest: sym)
  4154 
  4155 lemma word_rotr_rev:
  4156   "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  4157   by (simp only: word_bl.Rep_inject [symmetric] to_bl_word_rev
  4158                 to_bl_rotr to_bl_rotl rotater_rev)
  4159   
  4160 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  4161   by (unfold word_rot_defs) auto
  4162 
  4163 lemmas abl_cong = arg_cong [where f = "of_bl"]
  4164 
  4165 lemma word_roti_add: 
  4166   "word_roti (m + n) w = word_roti m (word_roti n w)"
  4167 proof -
  4168   have rotater_eq_lem: 
  4169     "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
  4170     by auto
  4171 
  4172   have rotate_eq_lem: 
  4173     "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
  4174     by auto
  4175 
  4176   note rpts [symmetric] = 
  4177     rotate_inv_plus [THEN conjunct1]
  4178     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  4179     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  4180     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  4181 
  4182   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  4183   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  4184 
  4185   show ?thesis
  4186   apply (unfold word_rot_defs)
  4187   apply (simp only: split: split_if)
  4188   apply (safe intro!: abl_cong)
  4189   apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
  4190                     to_bl_rotl
  4191                     to_bl_rotr [THEN word_bl.Rep_inverse']
  4192                     to_bl_rotr)
  4193   apply (rule rrp rrrp rpts,
  4194          simp add: nat_add_distrib [symmetric] 
  4195                    nat_diff_distrib [symmetric])+
  4196   done
  4197 qed
  4198     
  4199 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
  4200   apply (unfold word_rot_defs)
  4201   apply (cut_tac y="size w" in gt_or_eq_0)
  4202   apply (erule disjE)
  4203    apply simp_all
  4204   apply (safe intro!: abl_cong)
  4205    apply (rule rotater_eqs)
  4206    apply (simp add: word_size nat_mod_distrib)
  4207   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  4208   apply (rule rotater_eqs)
  4209   apply (simp add: word_size nat_mod_distrib)
  4210   apply (rule int_eq_0_conv [THEN iffD1])
  4211   apply (simp only: zmod_int of_nat_add)
  4212   apply (simp add: rdmods)
  4213   done
  4214 
  4215 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  4216 
  4217 
  4218 subsubsection {* "Word rotation commutes with bit-wise operations *}
  4219 
  4220 (* using locale to not pollute lemma namespace *)
  4221 locale word_rotate 
  4222 begin
  4223 
  4224 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  4225 
  4226 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  4227 
  4228 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
  4229 
  4230 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  4231 
  4232 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
  4233 
  4234 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  4235 
  4236 lemma word_rot_logs:
  4237   "word_rotl n (NOT v) = NOT word_rotl n v"
  4238   "word_rotr n (NOT v) = NOT word_rotr n v"
  4239   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  4240   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  4241   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  4242   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  4243   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  4244   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"  
  4245   by (rule word_bl.Rep_eqD,
  4246       rule word_rot_defs' [THEN trans],
  4247       simp only: blwl_syms [symmetric],
  4248       rule th1s [THEN trans], 
  4249       rule refl)+
  4250 end
  4251 
  4252 lemmas word_rot_logs = word_rotate.word_rot_logs
  4253 
  4254 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  4255   simplified word_bl_Rep']
  4256 
  4257 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  4258   simplified word_bl_Rep']
  4259 
  4260 lemma bl_word_roti_dt': 
  4261   "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow> 
  4262     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  4263   apply (unfold word_roti_def)
  4264   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  4265   apply safe
  4266    apply (simp add: zmod_zminus1_eq_if)
  4267    apply safe
  4268     apply (simp add: nat_mult_distrib)
  4269    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 
  4270                                       [THEN conjunct2, THEN order_less_imp_le]]
  4271                     nat_mod_distrib)
  4272   apply (simp add: nat_mod_distrib)
  4273   done
  4274 
  4275 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  4276 
  4277 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]] 
  4278 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4279 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
  4280 
  4281 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
  4282   by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
  4283 
  4284 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  4285   unfolding word_roti_def by auto
  4286 
  4287 lemmas word_rotr_dt_no_bin' [simp] = 
  4288   word_rotr_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4289   (* FIXME: negative numerals, 0 and 1 *)
  4290 
  4291 lemmas word_rotl_dt_no_bin' [simp] = 
  4292   word_rotl_dt [where w="numeral w", unfolded to_bl_numeral] for w
  4293   (* FIXME: negative numerals, 0 and 1 *)
  4294 
  4295 declare word_roti_def [simp]
  4296 
  4297 
  4298 subsection {* Maximum machine word *}
  4299 
  4300 lemma word_int_cases:
  4301   obtains n where "(x ::'a::len0 word) = word_of_int n" and "0 \<le> n" and "n < 2^len_of TYPE('a)"
  4302   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
  4303 
  4304 lemma word_nat_cases [cases type: word]:
  4305   obtains n where "(x ::'a::len word) = of_nat n" and "n < 2^len_of TYPE('a)"
  4306   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
  4307 
  4308 lemma max_word_eq: "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
  4309   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
  4310 
  4311 lemma max_word_max [simp,intro!]: "n \<le> max_word"
  4312   by (cases n rule: word_int_cases)
  4313     (simp add: max_word_def word_le_def int_word_uint mod_pos_pos_trivial del: minus_mod_self1)
  4314   
  4315 lemma word_of_int_2p_len: "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
  4316   by (subst word_uint.Abs_norm [symmetric]) simp
  4317 
  4318 lemma word_pow_0:
  4319   "(2::'a::len word) ^ len_of TYPE('a) = 0"
  4320 proof -
  4321   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
  4322     by (rule word_of_int_2p_len)
  4323   thus ?thesis by (simp add: word_of_int_2p)
  4324 qed
  4325 
  4326 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
  4327   apply (simp add: max_word_eq)
  4328   apply uint_arith
  4329   apply auto
  4330   apply (simp add: word_pow_0)
  4331   done
  4332 
  4333 lemma max_word_minus: 
  4334   "max_word = (-1::'a::len word)"
  4335 proof -
  4336   have "-1 + 1 = (0::'a word)" by simp
  4337   thus ?thesis by (rule max_word_wrap [symmetric])
  4338 qed
  4339 
  4340 lemma max_word_bl [simp]:
  4341   "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
  4342   by (subst max_word_minus to_bl_n1)+ simp
  4343 
  4344 lemma max_test_bit [simp]:
  4345   "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
  4346   by (auto simp add: test_bit_bl word_size)
  4347 
  4348 lemma word_and_max [simp]:
  4349   "x AND max_word = x"
  4350   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4351 
  4352 lemma word_or_max [simp]:
  4353   "x OR max_word = max_word"
  4354   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
  4355 
  4356 lemma word_ao_dist2:
  4357   "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
  4358   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4359 
  4360 lemma word_oa_dist2:
  4361   "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
  4362   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4363 
  4364 lemma word_and_not [simp]:
  4365   "x AND NOT x = (0::'a::len0 word)"
  4366   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4367 
  4368 lemma word_or_not [simp]:
  4369   "x OR NOT x = max_word"
  4370   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4371 
  4372 lemma word_boolean:
  4373   "boolean (op AND) (op OR) bitNOT 0 max_word"
  4374   apply (rule boolean.intro)
  4375            apply (rule word_bw_assocs)
  4376           apply (rule word_bw_assocs)
  4377          apply (rule word_bw_comms)
  4378         apply (rule word_bw_comms)
  4379        apply (rule word_ao_dist2)
  4380       apply (rule word_oa_dist2)
  4381      apply (rule word_and_max)
  4382     apply (rule word_log_esimps)
  4383    apply (rule word_and_not)
  4384   apply (rule word_or_not)
  4385   done
  4386 
  4387 interpretation word_bool_alg:
  4388   boolean "op AND" "op OR" bitNOT 0 max_word
  4389   by (rule word_boolean)
  4390 
  4391 lemma word_xor_and_or:
  4392   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
  4393   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
  4394 
  4395 interpretation word_bool_alg:
  4396   boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
  4397   apply (rule boolean_xor.intro)
  4398    apply (rule word_boolean)
  4399   apply (rule boolean_xor_axioms.intro)
  4400   apply (rule word_xor_and_or)
  4401   done
  4402 
  4403 lemma shiftr_x_0 [iff]:
  4404   "(x::'a::len0 word) >> 0 = x"
  4405   by (simp add: shiftr_bl)
  4406 
  4407 lemma shiftl_x_0 [simp]: 
  4408   "(x :: 'a :: len word) << 0 = x"
  4409   by (simp add: shiftl_t2n)
  4410 
  4411 lemma shiftl_1 [simp]:
  4412   "(1::'a::len word) << n = 2^n"
  4413   by (simp add: shiftl_t2n)
  4414 
  4415 lemma uint_lt_0 [simp]:
  4416   "uint x < 0 = False"
  4417   by (simp add: linorder_not_less)
  4418 
  4419 lemma shiftr1_1 [simp]: 
  4420   "shiftr1 (1::'a::len word) = 0"
  4421   unfolding shiftr1_def by simp
  4422 
  4423 lemma shiftr_1[simp]: 
  4424   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
  4425   by (induct n) (auto simp: shiftr_def)
  4426 
  4427 lemma word_less_1 [simp]: 
  4428   "((x::'a::len word) < 1) = (x = 0)"
  4429   by (simp add: word_less_nat_alt unat_0_iff)
  4430 
  4431 lemma to_bl_mask:
  4432   "to_bl (mask n :: 'a::len word) = 
  4433   replicate (len_of TYPE('a) - n) False @ 
  4434     replicate (min (len_of TYPE('a)) n) True"
  4435   by (simp add: mask_bl word_rep_drop min_def)
  4436 
  4437 lemma map_replicate_True:
  4438   "n = length xs \<Longrightarrow>
  4439     map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
  4440   by (induct xs arbitrary: n) auto
  4441 
  4442 lemma map_replicate_False:
  4443   "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
  4444     (zip xs (replicate n False)) = replicate n False"
  4445   by (induct xs arbitrary: n) auto
  4446 
  4447 lemma bl_and_mask:
  4448   fixes w :: "'a::len word"
  4449   fixes n
  4450   defines "n' \<equiv> len_of TYPE('a) - n"
  4451   shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
  4452 proof - 
  4453   note [simp] = map_replicate_True map_replicate_False
  4454   have "to_bl (w AND mask n) = 
  4455         map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
  4456     by (simp add: bl_word_and)
  4457   also
  4458   have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
  4459   also
  4460   have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = 
  4461         replicate n' False @ drop n' (to_bl w)"
  4462     unfolding to_bl_mask n'_def map2_def
  4463     by (subst zip_append) auto
  4464   finally
  4465   show ?thesis .
  4466 qed
  4467 
  4468 lemma drop_rev_takefill:
  4469   "length xs \<le> n \<Longrightarrow>
  4470     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
  4471   by (simp add: takefill_alt rev_take)
  4472 
  4473 lemma map_nth_0 [simp]:
  4474   "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
  4475   by (induct xs) auto
  4476 
  4477 lemma uint_plus_if_size:
  4478   "uint (x + y) = 
  4479   (if uint x + uint y < 2^size x then 
  4480       uint x + uint y 
  4481    else 
  4482       uint x + uint y - 2^size x)" 
  4483   by (simp add: word_arith_alts int_word_uint mod_add_if_z 
  4484                 word_size)
  4485 
  4486 lemma unat_plus_if_size:
  4487   "unat (x + (y::'a::len word)) = 
  4488   (if unat x + unat y < 2^size x then 
  4489       unat x + unat y 
  4490    else 
  4491       unat x + unat y - 2^size x)" 
  4492   apply (subst word_arith_nat_defs)
  4493   apply (subst unat_of_nat)
  4494   apply (simp add:  mod_nat_add word_size)
  4495   done
  4496 
  4497 lemma word_neq_0_conv:
  4498   fixes w :: "'a :: len word"
  4499   shows "(w \<noteq> 0) = (0 < w)"
  4500   unfolding word_gt_0 by simp
  4501 
  4502 lemma max_lt:
  4503   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
  4504   apply (subst word_arith_nat_defs)
  4505   apply (subst word_unat.eq_norm)
  4506   apply (subst mod_if)
  4507   apply clarsimp
  4508   apply (erule notE)
  4509   apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
  4510   apply (erule order_le_less_trans)
  4511   apply (insert unat_lt2p [of "max a b"])
  4512   apply simp
  4513   done
  4514 
  4515 lemma uint_sub_if_size:
  4516   "uint (x - y) = 
  4517   (if uint y \<le> uint x then 
  4518       uint x - uint y 
  4519    else 
  4520       uint x - uint y + 2^size x)"
  4521   by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
  4522                 word_size)
  4523 
  4524 lemma unat_sub:
  4525   "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
  4526   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
  4527 
  4528 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "numeral w"] for w
  4529 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "numeral w"] for w
  4530   
  4531 lemma word_of_int_minus: 
  4532   "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
  4533 proof -
  4534   have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
  4535   show ?thesis
  4536     apply (subst x)
  4537     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
  4538     apply simp
  4539     done
  4540 qed
  4541   
  4542 lemmas word_of_int_inj = 
  4543   word_uint.Abs_inject [unfolded uints_num, simplified]
  4544 
  4545 lemma word_le_less_eq:
  4546   "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
  4547   by (auto simp add: order_class.le_less)
  4548 
  4549 lemma mod_plus_cong:
  4550   assumes 1: "(b::int) = b'"
  4551       and 2: "x mod b' = x' mod b'"
  4552       and 3: "y mod b' = y' mod b'"
  4553       and 4: "x' + y' = z'"
  4554   shows "(x + y) mod b = z' mod b'"
  4555 proof -
  4556   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
  4557     by (simp add: mod_add_eq[symmetric])
  4558   also have "\<dots> = (x' + y') mod b'"
  4559     by (simp add: mod_add_eq[symmetric])
  4560   finally show ?thesis by (simp add: 4)
  4561 qed
  4562 
  4563 lemma mod_minus_cong:
  4564   assumes 1: "(b::int) = b'"
  4565       and 2: "x mod b' = x' mod b'"
  4566       and 3: "y mod b' = y' mod b'"
  4567       and 4: "x' - y' = z'"
  4568   shows "(x - y) mod b = z' mod b'"
  4569   using assms
  4570   apply (subst mod_diff_left_eq)
  4571   apply (subst mod_diff_right_eq)
  4572   apply (simp add: mod_diff_left_eq [symmetric] mod_diff_right_eq [symmetric])
  4573   done
  4574 
  4575 lemma word_induct_less: 
  4576   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4577   apply (cases m)
  4578   apply atomize
  4579   apply (erule rev_mp)+
  4580   apply (rule_tac x=m in spec)
  4581   apply (induct_tac n)
  4582    apply simp
  4583   apply clarsimp
  4584   apply (erule impE)
  4585    apply clarsimp
  4586    apply (erule_tac x=n in allE)
  4587    apply (erule impE)
  4588     apply (simp add: unat_arith_simps)
  4589     apply (clarsimp simp: unat_of_nat)
  4590    apply simp
  4591   apply (erule_tac x="of_nat na" in allE)
  4592   apply (erule impE)
  4593    apply (simp add: unat_arith_simps)
  4594    apply (clarsimp simp: unat_of_nat)
  4595   apply simp
  4596   done
  4597   
  4598 lemma word_induct: 
  4599   "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
  4600   by (erule word_induct_less, simp)
  4601 
  4602 lemma word_induct2 [induct type]: 
  4603   "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
  4604   apply (rule word_induct, simp)
  4605   apply (case_tac "1+n = 0", auto)
  4606   done
  4607 
  4608 
  4609 subsection {* Recursion combinator for words *}
  4610 
  4611 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
  4612 where
  4613   "word_rec forZero forSuc n = rec_nat forZero (forSuc \<circ> of_nat) (unat n)"
  4614 
  4615 lemma word_rec_0: "word_rec z s 0 = z"
  4616   by (simp add: word_rec_def)
  4617 
  4618 lemma word_rec_Suc: 
  4619   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
  4620   apply (simp add: word_rec_def unat_word_ariths)
  4621   apply (subst nat_mod_eq')
  4622    apply (cut_tac x=n in unat_lt2p)
  4623    apply (drule Suc_mono)
  4624    apply (simp add: less_Suc_eq_le)
  4625    apply (simp only: order_less_le, simp)
  4626    apply (erule contrapos_pn, simp)
  4627    apply (drule arg_cong[where f=of_nat])
  4628    apply simp
  4629    apply (subst (asm) word_unat.Rep_inverse[of n])
  4630    apply simp
  4631   apply simp
  4632   done
  4633 
  4634 lemma word_rec_Pred: 
  4635   "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
  4636   apply (rule subst[where t="n" and s="1 + (n - 1)"])
  4637    apply simp
  4638   apply (subst word_rec_Suc)
  4639    apply simp
  4640   apply simp
  4641   done
  4642 
  4643 lemma word_rec_in: 
  4644   "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
  4645   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4646 
  4647 lemma word_rec_in2: 
  4648   "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
  4649   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
  4650 
  4651 lemma word_rec_twice: 
  4652   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
  4653 apply (erule rev_mp)
  4654 apply (rule_tac x=z in spec)
  4655 apply (rule_tac x=f in spec)
  4656 apply (induct n)
  4657  apply (simp add: word_rec_0)
  4658 apply clarsimp
  4659 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
  4660  apply simp
  4661 apply (case_tac "1 + (n - m) = 0")
  4662  apply (simp add: word_rec_0)
  4663  apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
  4664  apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
  4665   apply simp
  4666  apply (simp (no_asm_use))
  4667 apply (simp add: word_rec_Suc word_rec_in2)
  4668 apply (erule impE)
  4669  apply uint_arith
  4670 apply (drule_tac x="x \<circ> op + 1" in spec)
  4671 apply (drule_tac x="x 0 xa" in spec)
  4672 apply simp
  4673 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
  4674        in subst)
  4675  apply (clarsimp simp add: fun_eq_iff)
  4676  apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
  4677   apply simp
  4678  apply (rule refl)
  4679 apply (rule refl)
  4680 done
  4681 
  4682 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
  4683   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
  4684 
  4685 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
  4686 apply (erule rev_mp)
  4687 apply (induct n)
  4688  apply (auto simp add: word_rec_0 word_rec_Suc)
  4689  apply (drule spec, erule mp)
  4690  apply uint_arith
  4691 apply (drule_tac x=n in spec, erule impE)
  4692  apply uint_arith
  4693 apply simp
  4694 done
  4695 
  4696 lemma word_rec_max: 
  4697   "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
  4698 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
  4699  apply simp
  4700 apply simp
  4701 apply (rule word_rec_id_eq)
  4702 apply clarsimp
  4703 apply (drule spec, rule mp, erule mp)
  4704  apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
  4705   prefer 2 
  4706   apply assumption
  4707  apply simp
  4708 apply (erule contrapos_pn)
  4709 apply simp
  4710 apply (drule arg_cong[where f="\<lambda>x. x - n"])
  4711 apply simp
  4712 done
  4713 
  4714 lemma unatSuc: 
  4715   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
  4716   by unat_arith
  4717 
  4718 declare bin_to_bl_def [simp]
  4719 
  4720 ML_file "Tools/word_lib.ML"
  4721 ML_file "Tools/smt_word.ML"
  4722 setup SMT_Word.setup
  4723 
  4724 hide_const (open) Word
  4725 
  4726 end
  4727 
  4728 
  4729