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