1 (* Title: HOL/Word/Word.thy
2 Author: Jeremy Dawson and Gerwin Klein, NICTA
5 header {* A type of finite bit strings *}
11 "~~/src/HOL/Library/Boolean_Algebra"
12 Bool_List_Representation
13 uses ("~~/src/HOL/Word/Tools/smt_word.ML")
16 text {* see @{text "Examples/WordExamples.thy"} for examples *}
18 subsection {* Type definition *}
20 typedef (open) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
21 morphisms uint Abs_word by auto
23 definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
24 -- {* representation of words using unsigned or signed bins,
25 only difference in these is the type class *}
26 "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)"
28 lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
29 by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
31 code_datatype word_of_int
33 subsection {* Random instance *}
35 notation fcomp (infixl "\<circ>>" 60)
36 notation scomp (infixl "\<circ>\<rightarrow>" 60)
38 instantiation word :: ("{len0, typerep}") random
42 "random_word i = Random.range (max i (2 ^ len_of TYPE('a))) \<circ>\<rightarrow> (\<lambda>k. Pair (
43 let j = word_of_int (Code_Numeral.int_of k) :: 'a word
44 in (j, \<lambda>_::unit. Code_Evaluation.term_of j)))"
50 no_notation fcomp (infixl "\<circ>>" 60)
51 no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
54 subsection {* Type conversions and casting *}
56 definition sint :: "'a :: len word => int" where
57 -- {* treats the most-significant-bit as a sign bit *}
58 sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
60 definition unat :: "'a :: len0 word => nat" where
61 "unat w = nat (uint w)"
63 definition uints :: "nat => int set" where
64 -- "the sets of integers representing the words"
65 "uints n = range (bintrunc n)"
67 definition sints :: "nat => int set" where
68 "sints n = range (sbintrunc (n - 1))"
70 definition unats :: "nat => nat set" where
71 "unats n = {i. i < 2 ^ n}"
73 definition norm_sint :: "nat => int => int" where
74 "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
76 definition scast :: "'a :: len word => 'b :: len word" where
77 -- "cast a word to a different length"
78 "scast w = word_of_int (sint w)"
80 definition ucast :: "'a :: len0 word => 'b :: len0 word" where
81 "ucast w = word_of_int (uint w)"
83 instantiation word :: (len0) size
87 word_size: "size (w :: 'a word) = len_of TYPE('a)"
93 definition source_size :: "('a :: len0 word => 'b) => nat" where
94 -- "whether a cast (or other) function is to a longer or shorter length"
95 "source_size c = (let arb = undefined ; x = c arb in size arb)"
97 definition target_size :: "('a => 'b :: len0 word) => nat" where
98 "target_size c = size (c undefined)"
100 definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
101 "is_up c \<longleftrightarrow> source_size c <= target_size c"
103 definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
104 "is_down c \<longleftrightarrow> target_size c <= source_size c"
106 definition of_bl :: "bool list => 'a :: len0 word" where
107 "of_bl bl = word_of_int (bl_to_bin bl)"
109 definition to_bl :: "'a :: len0 word => bool list" where
110 "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
112 definition word_reverse :: "'a :: len0 word => 'a word" where
113 "word_reverse w = of_bl (rev (to_bl w))"
115 definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
116 "word_int_case f w = f (uint w)"
119 of_int :: "int => 'a"
121 "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
123 subsection {* Type-definition locale instantiations *}
125 lemma word_size_gt_0 [iff]: "0 < size (w::'a::len word)"
126 by (fact xtr1 [OF word_size len_gt_0])
128 lemmas lens_gt_0 = word_size_gt_0 len_gt_0
129 lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0]
131 lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
132 by (simp add: uints_def range_bintrunc)
134 lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
135 by (simp add: sints_def range_sbintrunc)
137 lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
141 uint_0:"0 <= uint x" and
142 uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
143 by (auto simp: uint [unfolded atLeastLessThan_iff])
146 "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
147 by (simp add: int_mod_eq uint_lt uint_0)
150 "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0)))
151 (%w::int. w mod 2 ^ len_of TYPE('a))"
152 apply (unfold td_ext_def')
153 apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
154 apply (simp add: uint_mod_same uint_0 uint_lt
155 word.uint_inverse word.Abs_word_inverse int_mod_lem)
159 "uint (word_of_int x::'a::len0 word) = x mod 2 ^ len_of TYPE('a)"
160 by (fact td_ext_uint [THEN td_ext.eq_norm])
162 interpretation word_uint:
163 td_ext "uint::'a::len0 word \<Rightarrow> int"
165 "uints (len_of TYPE('a::len0))"
166 "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
167 by (rule td_ext_uint)
169 lemmas td_uint = word_uint.td_thm
171 lemmas td_ext_ubin = td_ext_uint
172 [unfolded len_gt_0 no_bintr_alt1 [symmetric]]
174 interpretation word_ubin:
175 td_ext "uint::'a::len0 word \<Rightarrow> int"
177 "uints (len_of TYPE('a::len0))"
178 "bintrunc (len_of TYPE('a::len0))"
179 by (rule td_ext_ubin)
181 lemma split_word_all:
182 "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
185 assume "\<And>x. PROP P (word_of_int x)"
186 hence "PROP P (word_of_int (uint x))" .
187 thus "PROP P x" by simp
190 subsection "Arithmetic operations"
193 word_succ :: "'a :: len0 word => 'a word"
195 "word_succ a = word_of_int (Int.succ (uint a))"
198 word_pred :: "'a :: len0 word => 'a word"
200 "word_pred a = word_of_int (Int.pred (uint a))"
202 instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
206 word_0_wi: "0 = word_of_int 0"
209 word_1_wi: "1 = word_of_int 1"
212 word_add_def: "a + b = word_of_int (uint a + uint b)"
215 word_sub_wi: "a - b = word_of_int (uint a - uint b)"
218 word_minus_def: "- a = word_of_int (- uint a)"
221 word_mult_def: "a * b = word_of_int (uint a * uint b)"
224 word_div_def: "a div b = word_of_int (uint a div uint b)"
227 word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
230 word_number_of_def: "number_of w = word_of_int w"
232 lemmas word_arith_wis =
233 word_add_def word_mult_def word_minus_def
234 word_succ_def word_pred_def word_0_wi word_1_wi
237 bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
241 wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
242 wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
243 wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
244 wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
245 wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
246 by (auto simp: word_arith_wis arths)
248 lemmas wi_hom_syms = wi_homs [symmetric]
250 lemma word_of_int_sub_hom:
251 "(word_of_int a) - word_of_int b = word_of_int (a - b)"
252 by (simp add: word_sub_wi arths)
254 lemmas new_word_of_int_homs =
255 word_of_int_sub_hom wi_homs word_0_wi word_1_wi
257 lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
259 lemmas word_of_int_hom_syms =
260 new_word_of_int_hom_syms [unfolded succ_def pred_def]
262 lemmas word_of_int_homs =
263 new_word_of_int_homs [unfolded succ_def pred_def]
265 (* FIXME: provide only one copy of these theorems! *)
266 lemmas word_of_int_add_hom = wi_hom_add
267 lemmas word_of_int_mult_hom = wi_hom_mult
268 lemmas word_of_int_minus_hom = wi_hom_neg
269 lemmas word_of_int_succ_hom = wi_hom_succ [unfolded succ_def]
270 lemmas word_of_int_pred_hom = wi_hom_pred [unfolded pred_def]
271 lemmas word_of_int_0_hom = word_0_wi
272 lemmas word_of_int_1_hom = word_1_wi
275 by default (auto simp: split_word_all word_of_int_homs algebra_simps)
279 instance word :: (len) comm_ring_1
281 have "0 < len_of TYPE('a)" by (rule len_gt_0)
282 then show "(0::'a word) \<noteq> 1"
283 unfolding word_0_wi word_1_wi
284 by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
287 lemma word_of_nat: "of_nat n = word_of_int (int n)"
288 by (induct n) (auto simp add : word_of_int_hom_syms)
290 lemma word_of_int: "of_int = word_of_int"
292 apply (case_tac x rule: int_diff_cases)
293 apply (simp add: word_of_nat word_of_int_sub_hom)
296 instance word :: (len) number_ring
297 by (default, simp add: word_number_of_def word_of_int)
299 definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
300 "a udvd b = (EX n>=0. uint b = n * uint a)"
303 subsection "Ordering"
305 instantiation word :: (len0) linorder
309 word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
312 word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
315 by default (auto simp: word_less_def word_le_def)
319 definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
320 "a <=s b = (sint a <= sint b)"
322 definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
323 "(x <s y) = (x <=s y & x ~= y)"
326 subsection "Bit-wise operations"
328 instantiation word :: (len0) bits
333 "(a::'a word) AND b = word_of_int (uint a AND uint b)"
337 "(a::'a word) OR b = word_of_int (uint a OR uint b)"
341 "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
345 "NOT (a::'a word) = word_of_int (NOT (uint a))"
348 word_test_bit_def: "test_bit a = bin_nth (uint a)"
351 word_set_bit_def: "set_bit a n x =
352 word_of_int (bin_sc n (If x 1 0) (uint a))"
355 word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE ('a)) f)"
358 word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a) = 1"
360 definition shiftl1 :: "'a word \<Rightarrow> 'a word" where
361 "shiftl1 w = word_of_int (uint w BIT 0)"
363 definition shiftr1 :: "'a word \<Rightarrow> 'a word" where
364 -- "shift right as unsigned or as signed, ie logical or arithmetic"
365 "shiftr1 w = word_of_int (bin_rest (uint w))"
368 shiftl_def: "w << n = (shiftl1 ^^ n) w"
371 shiftr_def: "w >> n = (shiftr1 ^^ n) w"
377 instantiation word :: (len) bitss
382 "msb a \<longleftrightarrow> bin_sign (sint a) = Int.Min"
389 "msb a \<longleftrightarrow> bin_sign (sint a) = (- 1 :: int)"
390 by (simp only: word_msb_def Min_def)
392 definition setBit :: "'a :: len0 word => nat => 'a word" where
393 "setBit w n = set_bit w n True"
395 definition clearBit :: "'a :: len0 word => nat => 'a word" where
396 "clearBit w n = set_bit w n False"
399 subsection "Shift operations"
401 definition sshiftr1 :: "'a :: len word => 'a word" where
402 "sshiftr1 w = word_of_int (bin_rest (sint w))"
404 definition bshiftr1 :: "bool => 'a :: len word => 'a word" where
405 "bshiftr1 b w = of_bl (b # butlast (to_bl w))"
407 definition sshiftr :: "'a :: len word => nat => 'a word" (infixl ">>>" 55) where
408 "w >>> n = (sshiftr1 ^^ n) w"
410 definition mask :: "nat => 'a::len word" where
411 "mask n = (1 << n) - 1"
413 definition revcast :: "'a :: len0 word => 'b :: len0 word" where
414 "revcast w = of_bl (takefill False (len_of TYPE('b)) (to_bl w))"
416 definition slice1 :: "nat => 'a :: len0 word => 'b :: len0 word" where
417 "slice1 n w = of_bl (takefill False n (to_bl w))"
419 definition slice :: "nat => 'a :: len0 word => 'b :: len0 word" where
420 "slice n w = slice1 (size w - n) w"
423 subsection "Rotation"
425 definition rotater1 :: "'a list => 'a list" where
427 (case ys of [] => [] | x # xs => last ys # butlast ys)"
429 definition rotater :: "nat => 'a list => 'a list" where
430 "rotater n = rotater1 ^^ n"
432 definition word_rotr :: "nat => 'a :: len0 word => 'a :: len0 word" where
433 "word_rotr n w = of_bl (rotater n (to_bl w))"
435 definition word_rotl :: "nat => 'a :: len0 word => 'a :: len0 word" where
436 "word_rotl n w = of_bl (rotate n (to_bl w))"
438 definition word_roti :: "int => 'a :: len0 word => 'a :: len0 word" where
439 "word_roti i w = (if i >= 0 then word_rotr (nat i) w
440 else word_rotl (nat (- i)) w)"
443 subsection "Split and cat operations"
445 definition word_cat :: "'a :: len0 word => 'b :: len0 word => 'c :: len0 word" where
446 "word_cat a b = word_of_int (bin_cat (uint a) (len_of TYPE ('b)) (uint b))"
448 definition word_split :: "'a :: len0 word => ('b :: len0 word) * ('c :: len0 word)" where
450 (case bin_split (len_of TYPE ('c)) (uint a) of
451 (u, v) => (word_of_int u, word_of_int v))"
453 definition word_rcat :: "'a :: len0 word list => 'b :: len0 word" where
455 word_of_int (bin_rcat (len_of TYPE ('a)) (map uint ws))"
457 definition word_rsplit :: "'a :: len0 word => 'b :: len word list" where
459 map word_of_int (bin_rsplit (len_of TYPE ('b)) (len_of TYPE ('a), uint w))"
461 definition max_word :: "'a::len word" -- "Largest representable machine integer." where
462 "max_word = word_of_int (2 ^ len_of TYPE('a) - 1)"
464 primrec of_bool :: "bool \<Rightarrow> 'a::len word" where
468 (* FIXME: only provide one theorem name *)
469 lemmas of_nth_def = word_set_bits_def
471 lemma sint_sbintrunc':
472 "sint (word_of_int bin :: 'a word) =
473 (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
475 by (auto simp: word_ubin.eq_norm sbintrunc_bintrunc_lt)
478 "uint w = bintrunc (len_of TYPE('a)) (sint (w :: 'a :: len word))"
479 unfolding sint_uint by (auto simp: bintrunc_sbintrunc_le)
482 "n >= size w \<Longrightarrow> bintrunc n (uint w) = uint w"
483 apply (unfold word_size)
484 apply (subst word_ubin.norm_Rep [symmetric])
485 apply (simp only: bintrunc_bintrunc_min word_size)
486 apply (simp add: min_max.inf_absorb2)
490 "wb = word_of_int bin \<Longrightarrow> n >= size wb \<Longrightarrow>
491 word_of_int (bintrunc n bin) = wb"
493 by (clarsimp simp add: word_ubin.norm_eq_iff [symmetric] min_max.inf_absorb1)
495 lemmas bintr_uint = bintr_uint' [unfolded word_size]
496 lemmas wi_bintr = wi_bintr' [unfolded word_size]
499 "td_ext (sint :: 'a word => int) word_of_int (sints (len_of TYPE('a::len)))
500 (sbintrunc (len_of TYPE('a) - 1))"
501 apply (unfold td_ext_def' sint_uint)
502 apply (simp add : word_ubin.eq_norm)
503 apply (cases "len_of TYPE('a)")
504 apply (auto simp add : sints_def)
505 apply (rule sym [THEN trans])
506 apply (rule word_ubin.Abs_norm)
507 apply (simp only: bintrunc_sbintrunc)
512 lemmas td_ext_sint = td_ext_sbin
513 [simplified len_gt_0 no_sbintr_alt2 Suc_pred' [symmetric]]
515 (* We do sint before sbin, before sint is the user version
516 and interpretations do not produce thm duplicates. I.e.
517 we get the name word_sint.Rep_eqD, but not word_sbin.Req_eqD,
518 because the latter is the same thm as the former *)
519 interpretation word_sint:
520 td_ext "sint ::'a::len word => int"
522 "sints (len_of TYPE('a::len))"
523 "%w. (w + 2^(len_of TYPE('a::len) - 1)) mod 2^len_of TYPE('a::len) -
524 2 ^ (len_of TYPE('a::len) - 1)"
525 by (rule td_ext_sint)
527 interpretation word_sbin:
528 td_ext "sint ::'a::len word => int"
530 "sints (len_of TYPE('a::len))"
531 "sbintrunc (len_of TYPE('a::len) - 1)"
532 by (rule td_ext_sbin)
534 lemmas int_word_sint = td_ext_sint [THEN td_ext.eq_norm]
536 lemmas td_sint = word_sint.td
538 lemma word_number_of_alt [code_unfold_post]:
539 "number_of b = word_of_int (number_of b)"
540 by (simp add: number_of_eq word_number_of_def)
542 lemma word_no_wi: "number_of = word_of_int"
543 by (auto simp: word_number_of_def)
546 "(to_bl :: 'a :: len0 word => bool list) =
547 bin_to_bl (len_of TYPE('a)) o uint"
548 by (auto simp: to_bl_def)
550 lemmas word_reverse_no_def [simp] = word_reverse_def [of "number_of w"] for w
552 lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
553 by (fact uints_def [unfolded no_bintr_alt1])
555 lemma uint_bintrunc [simp]:
556 "uint (number_of bin :: 'a word) =
557 number_of (bintrunc (len_of TYPE ('a :: len0)) bin)"
558 unfolding word_number_of_def number_of_eq
559 by (auto intro: word_ubin.eq_norm)
561 lemma sint_sbintrunc [simp]:
562 "sint (number_of bin :: 'a word) =
563 number_of (sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
564 unfolding word_number_of_def number_of_eq
565 by (subst word_sbin.eq_norm) simp
567 lemma unat_bintrunc [simp]:
568 "unat (number_of bin :: 'a :: len0 word) =
569 number_of (bintrunc (len_of TYPE('a)) bin)"
570 unfolding unat_def nat_number_of_def
571 by (simp only: uint_bintrunc)
573 lemma size_0_eq: "size (w :: 'a :: len0 word) = 0 \<Longrightarrow> v = w"
574 apply (unfold word_size)
575 apply (rule word_uint.Rep_eqD)
576 apply (rule box_equals)
578 apply (rule word_ubin.norm_Rep)+
582 lemma uint_ge_0 [iff]: "0 \<le> uint (x::'a::len0 word)"
583 using word_uint.Rep [of x] by (simp add: uints_num)
585 lemma uint_lt2p [iff]: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
586 using word_uint.Rep [of x] by (simp add: uints_num)
588 lemma sint_ge: "- (2 ^ (len_of TYPE('a) - 1)) \<le> sint (x::'a::len word)"
589 using word_sint.Rep [of x] by (simp add: sints_num)
591 lemma sint_lt: "sint (x::'a::len word) < 2 ^ (len_of TYPE('a) - 1)"
592 using word_sint.Rep [of x] by (simp add: sints_num)
594 lemma sign_uint_Pls [simp]:
595 "bin_sign (uint x) = Int.Pls"
596 by (simp add: sign_Pls_ge_0 number_of_eq)
598 lemma uint_m2p_neg: "uint (x::'a::len0 word) - 2 ^ len_of TYPE('a) < 0"
599 by (simp only: diff_less_0_iff_less uint_lt2p)
601 lemma uint_m2p_not_non_neg:
602 "\<not> 0 \<le> uint (x::'a::len0 word) - 2 ^ len_of TYPE('a)"
603 by (simp only: not_le uint_m2p_neg)
606 "len_of TYPE('a) <= n \<Longrightarrow> uint (w :: 'a :: len0 word) < 2 ^ n"
607 by (rule xtr8 [OF _ uint_lt2p]) simp
609 lemma uint_le_0_iff [simp]: "uint x \<le> 0 \<longleftrightarrow> uint x = 0"
610 by (fact uint_ge_0 [THEN leD, THEN linorder_antisym_conv1])
612 lemma uint_nat: "uint w = int (unat w)"
613 unfolding unat_def by auto
615 lemma uint_number_of:
616 "uint (number_of b :: 'a :: len0 word) = number_of b mod 2 ^ len_of TYPE('a)"
617 unfolding word_number_of_alt
618 by (simp only: int_word_uint)
620 lemma unat_number_of:
621 "bin_sign b = Int.Pls \<Longrightarrow>
622 unat (number_of b::'a::len0 word) = number_of b mod 2 ^ len_of TYPE ('a)"
623 apply (unfold unat_def)
624 apply (clarsimp simp only: uint_number_of)
625 apply (rule nat_mod_distrib [THEN trans])
626 apply (erule sign_Pls_ge_0 [THEN iffD1])
627 apply (simp_all add: nat_power_eq)
630 lemma sint_number_of: "sint (number_of b :: 'a :: len word) = (number_of b +
631 2 ^ (len_of TYPE('a) - 1)) mod 2 ^ len_of TYPE('a) -
632 2 ^ (len_of TYPE('a) - 1)"
633 unfolding word_number_of_alt by (rule int_word_sint)
635 lemma word_of_int_0 [simp]: "word_of_int 0 = 0"
636 unfolding word_0_wi ..
638 lemma word_of_int_1 [simp]: "word_of_int 1 = 1"
639 unfolding word_1_wi ..
641 lemma word_of_int_bin [simp] :
642 "(word_of_int (number_of bin) :: 'a :: len0 word) = (number_of bin)"
643 unfolding word_number_of_alt by auto
645 lemma word_int_case_wi:
646 "word_int_case f (word_of_int i :: 'b word) =
647 f (i mod 2 ^ len_of TYPE('b::len0))"
648 unfolding word_int_case_def by (simp add: word_uint.eq_norm)
650 lemma word_int_split:
651 "P (word_int_case f x) =
652 (ALL i. x = (word_of_int i :: 'b :: len0 word) &
653 0 <= i & i < 2 ^ len_of TYPE('b) --> P (f i))"
654 unfolding word_int_case_def
655 by (auto simp: word_uint.eq_norm int_mod_eq')
657 lemma word_int_split_asm:
658 "P (word_int_case f x) =
659 (~ (EX n. x = (word_of_int n :: 'b::len0 word) &
660 0 <= n & n < 2 ^ len_of TYPE('b::len0) & ~ P (f n)))"
661 unfolding word_int_case_def
662 by (auto simp: word_uint.eq_norm int_mod_eq')
664 lemmas uint_range' = word_uint.Rep [unfolded uints_num mem_Collect_eq]
665 lemmas sint_range' = word_sint.Rep [unfolded One_nat_def sints_num mem_Collect_eq]
667 lemma uint_range_size: "0 <= uint w & uint w < 2 ^ size w"
668 unfolding word_size by (rule uint_range')
670 lemma sint_range_size:
671 "- (2 ^ (size w - Suc 0)) <= sint w & sint w < 2 ^ (size w - Suc 0)"
672 unfolding word_size by (rule sint_range')
674 lemma sint_above_size: "2 ^ (size (w::'a::len word) - 1) \<le> x \<Longrightarrow> sint w < x"
675 unfolding word_size by (rule less_le_trans [OF sint_lt])
677 lemma sint_below_size:
678 "x \<le> - (2 ^ (size (w::'a::len word) - 1)) \<Longrightarrow> x \<le> sint w"
679 unfolding word_size by (rule order_trans [OF _ sint_ge])
681 lemma test_bit_eq_iff: "(test_bit (u::'a::len0 word) = test_bit v) = (u = v)"
682 unfolding word_test_bit_def by (simp add: bin_nth_eq_iff)
684 lemma test_bit_size [rule_format] : "(w::'a::len0 word) !! n --> n < size w"
685 apply (unfold word_test_bit_def)
686 apply (subst word_ubin.norm_Rep [symmetric])
687 apply (simp only: nth_bintr word_size)
691 lemma word_eqI [rule_format] :
692 fixes u :: "'a::len0 word"
693 shows "(ALL n. n < size u --> u !! n = v !! n) \<Longrightarrow> u = v"
694 apply (rule test_bit_eq_iff [THEN iffD1])
700 apply (auto dest!: test_bit_size simp add: word_size)
703 lemma word_eqD: "(u::'a::len0 word) = v \<Longrightarrow> u !! x = v !! x"
706 lemma test_bit_bin': "w !! n = (n < size w & bin_nth (uint w) n)"
707 unfolding word_test_bit_def word_size
708 by (simp add: nth_bintr [symmetric])
710 lemmas test_bit_bin = test_bit_bin' [unfolded word_size]
712 lemma bin_nth_uint_imp': "bin_nth (uint w) n --> n < size w"
713 apply (unfold word_size)
715 apply (rule nth_bintr [THEN iffD1, THEN conjunct1])
716 apply (subst word_ubin.norm_Rep)
721 "n >= size w --> bin_nth (sint w) n = bin_nth (sint w) (size w - 1)"
723 apply (subst word_sbin.norm_Rep [symmetric])
724 apply (simp add : nth_sbintr word_size)
728 lemmas bin_nth_uint_imp = bin_nth_uint_imp' [rule_format, unfolded word_size]
729 lemmas bin_nth_sint = bin_nth_sint' [rule_format, unfolded word_size]
731 (* type definitions theorem for in terms of equivalent bool list *)
733 "type_definition (to_bl :: 'a::len0 word => bool list)
735 {bl. length bl = len_of TYPE('a)}"
736 apply (unfold type_definition_def of_bl_def to_bl_def)
737 apply (simp add: word_ubin.eq_norm)
743 interpretation word_bl:
744 type_definition "to_bl :: 'a::len0 word => bool list"
746 "{bl. length bl = len_of TYPE('a::len0)}"
749 lemmas word_bl_Rep' = word_bl.Rep [unfolded mem_Collect_eq, iff]
751 lemma word_size_bl: "size w = size (to_bl w)"
752 unfolding word_size by auto
754 lemma to_bl_use_of_bl:
755 "(to_bl w = bl) = (w = of_bl bl \<and> length bl = length (to_bl w))"
756 by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
758 lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
759 unfolding word_reverse_def by (simp add: word_bl.Abs_inverse)
761 lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
762 unfolding word_reverse_def by (simp add : word_bl.Abs_inverse)
764 lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
767 lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
770 lemma length_bl_gt_0 [iff]: "0 < length (to_bl (x::'a::len word))"
771 unfolding word_bl_Rep' by (rule len_gt_0)
773 lemma bl_not_Nil [iff]: "to_bl (x::'a::len word) \<noteq> []"
774 by (fact length_bl_gt_0 [unfolded length_greater_0_conv])
776 lemma length_bl_neq_0 [iff]: "length (to_bl (x::'a::len word)) \<noteq> 0"
777 by (fact length_bl_gt_0 [THEN gr_implies_not0])
779 lemma hd_bl_sign_sint: "hd (to_bl w) = (bin_sign (sint w) = Int.Min)"
780 apply (unfold to_bl_def sint_uint)
781 apply (rule trans [OF _ bl_sbin_sign])
786 "lend = length bl - len_of TYPE ('a :: len0) \<Longrightarrow>
787 of_bl (drop lend bl) = (of_bl bl :: 'a word)"
788 apply (unfold of_bl_def)
789 apply (clarsimp simp add : trunc_bl2bin [symmetric])
792 lemma of_bl_no: "of_bl bl = number_of (bl_to_bin bl)"
793 by (fact of_bl_def [folded word_number_of_def])
795 lemma test_bit_of_bl:
796 "(of_bl bl::'a::len0 word) !! n = (rev bl ! n \<and> n < len_of TYPE('a) \<and> n < length bl)"
797 apply (unfold of_bl_def word_test_bit_def)
798 apply (auto simp add: word_size word_ubin.eq_norm nth_bintr bin_nth_of_bl)
802 "(number_of bin ::'a::len0 word) = of_bl (bin_to_bl (len_of TYPE ('a)) bin)"
803 unfolding word_size of_bl_no by (simp add : word_number_of_def)
805 lemma uint_bl: "to_bl w = bin_to_bl (size w) (uint w)"
806 unfolding word_size to_bl_def by auto
808 lemma to_bl_bin: "bl_to_bin (to_bl w) = uint w"
809 unfolding uint_bl by (simp add : word_size)
812 "to_bl (word_of_int bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
813 unfolding uint_bl by (clarsimp simp add: word_ubin.eq_norm word_size)
815 lemma to_bl_no_bin [simp]:
816 "to_bl (number_of bin::'a::len0 word) = bin_to_bl (len_of TYPE('a)) bin"
817 by (fact to_bl_of_bin [folded word_number_of_def])
819 lemma to_bl_to_bin [simp] : "bl_to_bin (to_bl w) = uint w"
820 unfolding uint_bl by (simp add : word_size)
822 lemmas uint_bl_bin [simp] = trans [OF bin_bl_bin word_ubin.norm_Rep]
824 (* FIXME: the next two lemmas should be unnecessary, because the lhs
825 terms should never occur in practice *)
826 lemma num_AB_u [simp]: "number_of (uint x) = x"
827 unfolding word_number_of_def by (rule word_uint.Rep_inverse)
829 lemma num_AB_s [simp]: "number_of (sint x) = x"
830 unfolding word_number_of_def by (rule word_sint.Rep_inverse)
833 lemma uints_unats: "uints n = int ` unats n"
834 apply (unfold unats_def uints_num)
836 apply (rule_tac image_eqI)
837 apply (erule_tac nat_0_le [symmetric])
839 apply (erule_tac nat_less_iff [THEN iffD2])
840 apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
841 apply (auto simp add : nat_power_eq int_power)
844 lemma unats_uints: "unats n = nat ` uints n"
845 by (auto simp add : uints_unats image_iff)
847 lemmas bintr_num = word_ubin.norm_eq_iff [symmetric, folded word_number_of_def]
848 lemmas sbintr_num = word_sbin.norm_eq_iff [symmetric, folded word_number_of_def]
850 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def]
851 lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def]
853 (* don't add these to simpset, since may want bintrunc n w to be simplified;
854 may want these in reverse, but loop as simp rules, so use following *)
857 "bintrunc (len_of TYPE('a :: len0)) a = b \<Longrightarrow>
858 number_of a = (number_of b :: 'a word)"
860 apply (rule_tac num_of_bintr [symmetric])
863 lemma num_of_sbintr':
864 "sbintrunc (len_of TYPE('a :: len) - 1) a = b \<Longrightarrow>
865 number_of a = (number_of b :: 'a word)"
867 apply (rule_tac num_of_sbintr [symmetric])
870 lemmas num_abs_bintr = sym [THEN trans, OF num_of_bintr word_number_of_def]
871 lemmas num_abs_sbintr = sym [THEN trans, OF num_of_sbintr word_number_of_def]
873 (** cast - note, no arg for new length, as it's determined by type of result,
874 thus in "cast w = w, the type means cast to length of w! **)
876 lemma ucast_id: "ucast w = w"
877 unfolding ucast_def by auto
879 lemma scast_id: "scast w = w"
880 unfolding scast_def by auto
882 lemma ucast_bl: "ucast w = of_bl (to_bl w)"
883 unfolding ucast_def of_bl_def uint_bl
884 by (auto simp add : word_size)
887 "(ucast w::'a::len0 word) !! n = (w !! n & n < len_of TYPE('a))"
888 apply (unfold ucast_def test_bit_bin)
889 apply (simp add: word_ubin.eq_norm nth_bintr word_size)
890 apply (fast elim!: bin_nth_uint_imp)
893 (* for literal u(s)cast *)
895 lemma ucast_bintr [simp]:
896 "ucast (number_of w ::'a::len0 word) =
897 number_of (bintrunc (len_of TYPE('a)) w)"
898 unfolding ucast_def by simp
900 lemma scast_sbintr [simp]:
901 "scast (number_of w ::'a::len word) =
902 number_of (sbintrunc (len_of TYPE('a) - Suc 0) w)"
903 unfolding scast_def by simp
905 lemmas source_size = source_size_def [unfolded Let_def word_size]
906 lemmas target_size = target_size_def [unfolded Let_def word_size]
907 lemmas is_down = is_down_def [unfolded source_size target_size]
908 lemmas is_up = is_up_def [unfolded source_size target_size]
910 lemmas is_up_down = trans [OF is_up is_down [symmetric]]
912 lemma down_cast_same [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc = scast"
913 apply (unfold is_down)
916 apply (unfold ucast_def scast_def uint_sint)
917 apply (rule word_ubin.norm_eq_iff [THEN iffD1])
922 "to_bl (of_bl bl::'a::len0 word) =
923 rev (takefill False (len_of TYPE('a)) (rev bl))"
924 unfolding of_bl_def uint_bl
925 by (clarsimp simp add: bl_bin_bl_rtf word_ubin.eq_norm word_size)
928 "to_bl (of_bl bl::'a::len0 word) =
929 replicate (len_of TYPE('a) - length bl) False @
930 drop (length bl - len_of TYPE('a)) bl"
931 by (simp add: word_rev_tf takefill_alt rev_take)
934 "to_bl (ucast (w::'b::len0 word) ::'a::len0 word) =
935 replicate (len_of TYPE('a) - len_of TYPE('b)) False @
936 drop (len_of TYPE('b) - len_of TYPE('a)) (to_bl w)"
937 apply (unfold ucast_bl)
939 apply (rule word_rep_drop)
943 lemma ucast_up_app [OF refl]:
944 "uc = ucast \<Longrightarrow> source_size uc + n = target_size uc \<Longrightarrow>
945 to_bl (uc w) = replicate n False @ (to_bl w)"
946 by (auto simp add : source_size target_size to_bl_ucast)
948 lemma ucast_down_drop [OF refl]:
949 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
950 to_bl (uc w) = drop n (to_bl w)"
951 by (auto simp add : source_size target_size to_bl_ucast)
953 lemma scast_down_drop [OF refl]:
954 "sc = scast \<Longrightarrow> source_size sc = target_size sc + n \<Longrightarrow>
955 to_bl (sc w) = drop n (to_bl w)"
956 apply (subgoal_tac "sc = ucast")
959 apply (erule ucast_down_drop)
960 apply (rule down_cast_same [symmetric])
961 apply (simp add : source_size target_size is_down)
964 lemma sint_up_scast [OF refl]:
965 "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> sint (sc w) = sint w"
968 apply (simp add: scast_def word_sbin.eq_norm)
969 apply (rule box_equals)
971 apply (rule word_sbin.norm_Rep)
972 apply (rule sbintrunc_sbintrunc_l)
974 apply (subst word_sbin.norm_Rep)
979 lemma uint_up_ucast [OF refl]:
980 "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> uint (uc w) = uint w"
984 apply (fold word_test_bit_def)
985 apply (auto simp add: nth_ucast)
986 apply (auto simp add: test_bit_bin)
989 lemma ucast_up_ucast [OF refl]:
990 "uc = ucast \<Longrightarrow> is_up uc \<Longrightarrow> ucast (uc w) = ucast w"
991 apply (simp (no_asm) add: ucast_def)
992 apply (clarsimp simp add: uint_up_ucast)
995 lemma scast_up_scast [OF refl]:
996 "sc = scast \<Longrightarrow> is_up sc \<Longrightarrow> scast (sc w) = scast w"
997 apply (simp (no_asm) add: scast_def)
998 apply (clarsimp simp add: sint_up_scast)
1001 lemma ucast_of_bl_up [OF refl]:
1002 "w = of_bl bl \<Longrightarrow> size bl <= size w \<Longrightarrow> ucast w = of_bl bl"
1003 by (auto simp add : nth_ucast word_size test_bit_of_bl intro!: word_eqI)
1005 lemmas ucast_up_ucast_id = trans [OF ucast_up_ucast ucast_id]
1006 lemmas scast_up_scast_id = trans [OF scast_up_scast scast_id]
1008 lemmas isduu = is_up_down [where c = "ucast", THEN iffD2]
1009 lemmas isdus = is_up_down [where c = "scast", THEN iffD2]
1010 lemmas ucast_down_ucast_id = isduu [THEN ucast_up_ucast_id]
1011 lemmas scast_down_scast_id = isdus [THEN ucast_up_ucast_id]
1013 lemma up_ucast_surj:
1014 "is_up (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
1015 surj (ucast :: 'a word => 'b word)"
1016 by (rule surjI, erule ucast_up_ucast_id)
1018 lemma up_scast_surj:
1019 "is_up (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
1020 surj (scast :: 'a word => 'b word)"
1021 by (rule surjI, erule scast_up_scast_id)
1023 lemma down_scast_inj:
1024 "is_down (scast :: 'b::len word => 'a::len word) \<Longrightarrow>
1025 inj_on (ucast :: 'a word => 'b word) A"
1026 by (rule inj_on_inverseI, erule scast_down_scast_id)
1028 lemma down_ucast_inj:
1029 "is_down (ucast :: 'b::len0 word => 'a::len0 word) \<Longrightarrow>
1030 inj_on (ucast :: 'a word => 'b word) A"
1031 by (rule inj_on_inverseI, erule ucast_down_ucast_id)
1033 lemma of_bl_append_same: "of_bl (X @ to_bl w) = w"
1034 by (rule word_bl.Rep_eqD) (simp add: word_rep_drop)
1036 lemma ucast_down_no [OF refl]:
1037 "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (number_of bin) = number_of bin"
1038 apply (unfold word_number_of_def is_down)
1039 apply (clarsimp simp add: ucast_def word_ubin.eq_norm)
1040 apply (rule word_ubin.norm_eq_iff [THEN iffD1])
1041 apply (erule bintrunc_bintrunc_ge)
1044 lemma ucast_down_bl [OF refl]:
1045 "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
1046 unfolding of_bl_no by clarify (erule ucast_down_no)
1048 lemmas slice_def' = slice_def [unfolded word_size]
1049 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
1051 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
1052 lemmas word_log_bin_defs = word_log_defs
1054 text {* Executable equality *}
1056 instantiation word :: (len0) equal
1059 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
1060 "equal_word k l \<longleftrightarrow> HOL.equal (uint k) (uint l)"
1063 qed (simp add: equal equal_word_def)
1068 subsection {* Word Arithmetic *}
1070 lemma word_less_alt: "(a < b) = (uint a < uint b)"
1071 unfolding word_less_def word_le_def
1072 by (auto simp del: word_uint.Rep_inject
1073 simp: word_uint.Rep_inject [symmetric])
1075 lemma signed_linorder: "class.linorder word_sle word_sless"
1077 qed (unfold word_sle_def word_sless_def, auto)
1079 interpretation signed: linorder "word_sle" "word_sless"
1080 by (rule signed_linorder)
1083 "0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
1084 by (auto simp: udvd_def)
1086 lemmas word_div_no [simp] = word_div_def [of "number_of a" "number_of b"] for a b
1088 lemmas word_mod_no [simp] = word_mod_def [of "number_of a" "number_of b"] for a b
1090 lemmas word_less_no [simp] = word_less_def [of "number_of a" "number_of b"] for a b
1092 lemmas word_le_no [simp] = word_le_def [of "number_of a" "number_of b"] for a b
1094 lemmas word_sless_no [simp] = word_sless_def [of "number_of a" "number_of b"] for a b
1096 lemmas word_sle_no [simp] = word_sle_def [of "number_of a" "number_of b"] for a b
1098 (* following two are available in class number_ring,
1099 but convenient to have them here here;
1100 note - the number_ring versions, numeral_0_eq_0 and numeral_1_eq_1
1101 are in the default simpset, so to use the automatic simplifications for
1102 (eg) sint (number_of bin) on sint 1, must do
1103 (simp add: word_1_no del: numeral_1_eq_1)
1105 lemma word_0_wi_Pls: "0 = word_of_int Int.Pls"
1106 by (simp only: Pls_def word_0_wi)
1108 lemma word_0_no: "(0::'a::len0 word) = Numeral0"
1109 by (simp add: word_number_of_alt)
1111 lemma int_one_bin: "(1 :: int) = (Int.Pls BIT 1)"
1112 unfolding Pls_def Bit_def by auto
1115 "(1 :: 'a :: len0 word) = number_of (Int.Pls BIT 1)"
1116 unfolding word_1_wi word_number_of_def int_one_bin by auto
1118 lemma word_m1_wi: "-1 = word_of_int -1"
1119 by (rule word_number_of_alt)
1121 lemma word_m1_wi_Min: "-1 = word_of_int Int.Min"
1122 by (simp add: word_m1_wi number_of_eq)
1124 lemma word_0_bl [simp]: "of_bl [] = 0"
1125 unfolding of_bl_def by (simp add: Pls_def)
1127 lemma word_1_bl: "of_bl [True] = 1"
1129 by (simp add: bl_to_bin_def Bit_def Pls_def)
1131 lemma uint_eq_0 [simp] : "(uint 0 = 0)"
1133 by (simp add: word_ubin.eq_norm Pls_def [symmetric])
1135 lemma of_bl_0 [simp]: "of_bl (replicate n False) = 0"
1136 by (simp add: of_bl_def bl_to_bin_rep_False Pls_def)
1138 lemma to_bl_0 [simp]:
1139 "to_bl (0::'a::len0 word) = replicate (len_of TYPE('a)) False"
1141 by (simp add : word_size bin_to_bl_Pls Pls_def [symmetric])
1143 lemma uint_0_iff: "(uint x = 0) = (x = 0)"
1144 by (auto intro!: word_uint.Rep_eqD)
1146 lemma unat_0_iff: "(unat x = 0) = (x = 0)"
1147 unfolding unat_def by (auto simp add : nat_eq_iff uint_0_iff)
1149 lemma unat_0 [simp]: "unat 0 = 0"
1150 unfolding unat_def by auto
1152 lemma size_0_same': "size w = 0 \<Longrightarrow> w = (v :: 'a :: len0 word)"
1153 apply (unfold word_size)
1154 apply (rule box_equals)
1156 apply (rule word_uint.Rep_inverse)+
1157 apply (rule word_ubin.norm_eq_iff [THEN iffD1])
1161 lemmas size_0_same = size_0_same' [unfolded word_size]
1163 lemmas unat_eq_0 = unat_0_iff
1164 lemmas unat_eq_zero = unat_0_iff
1166 lemma unat_gt_0: "(0 < unat x) = (x ~= 0)"
1167 by (auto simp: unat_0_iff [symmetric])
1169 lemma ucast_0 [simp]: "ucast 0 = 0"
1170 unfolding ucast_def by simp
1172 lemma sint_0 [simp]: "sint 0 = 0"
1173 unfolding sint_uint by simp
1175 lemma scast_0 [simp]: "scast 0 = 0"
1176 unfolding scast_def by simp
1178 lemma sint_n1 [simp] : "sint -1 = -1"
1179 unfolding word_m1_wi by (simp add: word_sbin.eq_norm)
1181 lemma scast_n1 [simp]: "scast -1 = -1"
1182 unfolding scast_def by simp
1184 lemma uint_1 [simp]: "uint (1::'a::len word) = 1"
1186 by (simp add: word_ubin.eq_norm bintrunc_minus_simps del: word_of_int_1)
1188 lemma unat_1 [simp]: "unat (1::'a::len word) = 1"
1189 unfolding unat_def by simp
1191 lemma ucast_1 [simp]: "ucast (1::'a::len word) = 1"
1192 unfolding ucast_def by simp
1194 (* now, to get the weaker results analogous to word_div/mod_def *)
1196 lemmas word_arith_alts =
1197 word_sub_wi [unfolded succ_def pred_def]
1198 word_arith_wis [unfolded succ_def pred_def]
1200 lemmas word_succ_alt = word_arith_alts (5)
1201 lemmas word_pred_alt = word_arith_alts (6)
1203 subsection "Transferring goals from words to ints"
1207 word_succ_p1: "word_succ a = a + 1" and
1208 word_pred_m1: "word_pred a = a - 1" and
1209 word_pred_succ: "word_pred (word_succ a) = a" and
1210 word_succ_pred: "word_succ (word_pred a) = a" and
1211 word_mult_succ: "word_succ a * b = b + a * b"
1212 by (rule word_uint.Abs_cases [of b],
1213 rule word_uint.Abs_cases [of a],
1214 simp add: pred_def succ_def add_commute mult_commute
1215 ring_distribs new_word_of_int_homs
1216 del: word_of_int_0 word_of_int_1)+
1218 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
1221 lemmas uint_word_ariths =
1222 word_arith_alts [THEN trans [OF uint_cong int_word_uint]]
1224 lemmas uint_word_arith_bintrs = uint_word_ariths [folded bintrunc_mod2p]
1226 (* similar expressions for sint (arith operations) *)
1227 lemmas sint_word_ariths = uint_word_arith_bintrs
1228 [THEN uint_sint [symmetric, THEN trans],
1229 unfolded uint_sint bintr_arith1s bintr_ariths
1230 len_gt_0 [THEN bin_sbin_eq_iff'] word_sbin.norm_Rep]
1232 lemmas uint_div_alt = word_div_def [THEN trans [OF uint_cong int_word_uint]]
1233 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
1235 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
1236 unfolding word_pred_def uint_eq_0 pred_def by simp
1238 lemma word_pred_0_Min: "word_pred 0 = word_of_int Int.Min"
1239 by (simp add: word_pred_0_n1 number_of_eq)
1241 lemma word_m1_Min: "- 1 = word_of_int Int.Min"
1242 unfolding Min_def by (simp only: word_of_int_hom_syms)
1244 lemma succ_pred_no [simp]:
1245 "word_succ (number_of bin) = number_of (Int.succ bin) &
1246 word_pred (number_of bin) = number_of (Int.pred bin)"
1247 unfolding word_number_of_def by (simp add : new_word_of_int_homs)
1249 lemma word_sp_01 [simp] :
1250 "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
1251 by (unfold word_0_no word_1_no) (auto simp: BIT_simps)
1253 (* alternative approach to lifting arithmetic equalities *)
1254 lemma word_of_int_Ex:
1255 "\<exists>y. x = word_of_int y"
1256 by (rule_tac x="uint x" in exI) simp
1259 subsection "Order on fixed-length words"
1261 lemma word_zero_le [simp] :
1262 "0 <= (y :: 'a :: len0 word)"
1263 unfolding word_le_def by auto
1265 lemma word_m1_ge [simp] : "word_pred 0 >= y" (* FIXME: delete *)
1266 unfolding word_le_def
1267 by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
1269 lemma word_n1_ge [simp]: "y \<le> (-1::'a::len0 word)"
1270 unfolding word_le_def
1271 by (simp only: word_m1_wi word_uint.eq_norm m1mod2k) auto
1273 lemmas word_not_simps [simp] =
1274 word_zero_le [THEN leD] word_m1_ge [THEN leD] word_n1_ge [THEN leD]
1276 lemma word_gt_0: "0 < y = (0 ~= (y :: 'a :: len0 word))"
1277 unfolding word_less_def by auto
1279 lemmas word_gt_0_no [simp] = word_gt_0 [of "number_of y"] for y
1281 lemma word_sless_alt: "(a <s b) = (sint a < sint b)"
1282 unfolding word_sle_def word_sless_def
1283 by (auto simp add: less_le)
1285 lemma word_le_nat_alt: "(a <= b) = (unat a <= unat b)"
1286 unfolding unat_def word_le_def
1287 by (rule nat_le_eq_zle [symmetric]) simp
1289 lemma word_less_nat_alt: "(a < b) = (unat a < unat b)"
1290 unfolding unat_def word_less_alt
1291 by (rule nat_less_eq_zless [symmetric]) simp
1294 "(word_of_int n < (word_of_int m :: 'a :: len0 word)) =
1295 (n mod 2 ^ len_of TYPE('a) < m mod 2 ^ len_of TYPE('a))"
1296 unfolding word_less_alt by (simp add: word_uint.eq_norm)
1299 "(word_of_int n <= (word_of_int m :: 'a :: len0 word)) =
1300 (n mod 2 ^ len_of TYPE('a) <= m mod 2 ^ len_of TYPE('a))"
1301 unfolding word_le_def by (simp add: word_uint.eq_norm)
1303 lemma udvd_nat_alt: "a udvd b = (EX n>=0. unat b = n * unat a)"
1304 apply (unfold udvd_def)
1306 apply (simp add: unat_def nat_mult_distrib)
1307 apply (simp add: uint_nat int_mult)
1316 lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
1317 unfolding dvd_def udvd_nat_alt by force
1319 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
1321 lemma unat_minus_one: "x ~= 0 \<Longrightarrow> unat (x - 1) = unat x - 1"
1322 apply (unfold unat_def)
1323 apply (simp only: int_word_uint word_arith_alts rdmods)
1324 apply (subgoal_tac "uint x >= 1")
1326 apply (drule contrapos_nn)
1327 apply (erule word_uint.Rep_inverse' [symmetric])
1328 apply (insert uint_ge_0 [of x])[1]
1330 apply (rule box_equals)
1331 apply (rule nat_diff_distrib)
1335 apply (subst mod_pos_pos_trivial)
1337 apply (insert uint_lt2p [of x])[1]
1343 lemma measure_unat: "p ~= 0 \<Longrightarrow> unat (p - 1) < unat p"
1344 by (simp add: unat_minus_one) (simp add: unat_0_iff [symmetric])
1346 lemmas uint_add_ge0 [simp] = add_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
1347 lemmas uint_mult_ge0 [simp] = mult_nonneg_nonneg [OF uint_ge_0 uint_ge_0]
1349 lemma uint_sub_lt2p [simp]:
1350 "uint (x :: 'a :: len0 word) - uint (y :: 'b :: len0 word) <
1351 2 ^ len_of TYPE('a)"
1352 using uint_ge_0 [of y] uint_lt2p [of x] by arith
1355 subsection "Conditions for the addition (etc) of two words to overflow"
1358 "(uint x + uint y < 2 ^ len_of TYPE('a)) =
1359 (uint (x + y :: 'a :: len0 word) = uint x + uint y)"
1360 by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
1362 lemma uint_mult_lem:
1363 "(uint x * uint y < 2 ^ len_of TYPE('a)) =
1364 (uint (x * y :: 'a :: len0 word) = uint x * uint y)"
1365 by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
1368 "(uint x >= uint y) = (uint (x - y) = uint x - uint y)"
1369 by (unfold uint_word_ariths) (auto intro!: trans [OF _ int_mod_lem])
1371 lemma uint_add_le: "uint (x + y) <= uint x + uint y"
1372 unfolding uint_word_ariths by (auto simp: mod_add_if_z)
1374 lemma uint_sub_ge: "uint (x - y) >= uint x - uint y"
1375 unfolding uint_word_ariths by (auto simp: mod_sub_if_z)
1377 lemmas uint_sub_if' = trans [OF uint_word_ariths(1) mod_sub_if_z, simplified]
1378 lemmas uint_plus_if' = trans [OF uint_word_ariths(2) mod_add_if_z, simplified]
1381 subsection {* Definition of uint\_arith *}
1383 lemma word_of_int_inverse:
1384 "word_of_int r = a \<Longrightarrow> 0 <= r \<Longrightarrow> r < 2 ^ len_of TYPE('a) \<Longrightarrow>
1385 uint (a::'a::len0 word) = r"
1386 apply (erule word_uint.Abs_inverse' [rotated])
1387 apply (simp add: uints_num)
1391 fixes x::"'a::len0 word"
1393 (ALL i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) --> P i)"
1394 apply (fold word_int_case_def)
1395 apply (auto dest!: word_of_int_inverse simp: int_word_uint int_mod_eq'
1396 split: word_int_split)
1399 lemma uint_split_asm:
1400 fixes x::"'a::len0 word"
1402 (~(EX i. word_of_int i = x & 0 <= i & i < 2^len_of TYPE('a) & ~ P i))"
1403 by (auto dest!: word_of_int_inverse
1404 simp: int_word_uint int_mod_eq'
1407 lemmas uint_splits = uint_split uint_split_asm
1409 lemmas uint_arith_simps =
1410 word_le_def word_less_alt
1411 word_uint.Rep_inject [symmetric]
1412 uint_sub_if' uint_plus_if'
1414 (* use this to stop, eg, 2 ^ len_of TYPE (32) being simplified *)
1415 lemma power_False_cong: "False \<Longrightarrow> a ^ b = c ^ d"
1418 (* uint_arith_tac: reduce to arithmetic on int, try to solve by arith *)
1420 fun uint_arith_ss_of ss =
1421 ss addsimps @{thms uint_arith_simps}
1422 delsimps @{thms word_uint.Rep_inject}
1423 |> fold Splitter.add_split @{thms split_if_asm}
1424 |> fold Simplifier.add_cong @{thms power_False_cong}
1426 fun uint_arith_tacs ctxt =
1428 fun arith_tac' n t =
1429 Arith_Data.verbose_arith_tac ctxt n t
1430 handle Cooper.COOPER _ => Seq.empty;
1432 [ clarify_tac ctxt 1,
1433 full_simp_tac (uint_arith_ss_of (simpset_of ctxt)) 1,
1434 ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms uint_splits}
1435 |> fold Simplifier.add_cong @{thms power_False_cong})),
1436 rewrite_goals_tac @{thms word_size},
1437 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
1438 REPEAT (etac conjE n) THEN
1439 REPEAT (dtac @{thm word_of_int_inverse} n
1445 fun uint_arith_tac ctxt = SELECT_GOAL (EVERY (uint_arith_tacs ctxt))
1448 method_setup uint_arith =
1449 {* Scan.succeed (SIMPLE_METHOD' o uint_arith_tac) *}
1450 "solving word arithmetic via integers and arith"
1453 subsection "More on overflows and monotonicity"
1455 lemma no_plus_overflow_uint_size:
1456 "((x :: 'a :: len0 word) <= x + y) = (uint x + uint y < 2 ^ size x)"
1457 unfolding word_size by uint_arith
1459 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
1461 lemma no_ulen_sub: "((x :: 'a :: len0 word) >= x - y) = (uint y <= uint x)"
1465 fixes x :: "'a::len0 word"
1466 shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
1467 by (simp add: add_ac no_olen_add)
1469 lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric]]
1471 lemmas uint_plus_simple_iff = trans [OF no_olen_add uint_add_lem]
1472 lemmas uint_plus_simple = uint_plus_simple_iff [THEN iffD1]
1473 lemmas uint_minus_simple_iff = trans [OF no_ulen_sub uint_sub_lem]
1474 lemmas uint_minus_simple_alt = uint_sub_lem [folded word_le_def]
1475 lemmas word_sub_le_iff = no_ulen_sub [folded word_le_def]
1476 lemmas word_sub_le = word_sub_le_iff [THEN iffD2]
1478 lemma word_less_sub1:
1479 "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 < x) = (0 < x - 1)"
1483 "(x :: 'a :: len word) ~= 0 \<Longrightarrow> (1 <= x) = (0 <= x - 1)"
1487 "((x :: 'a :: len0 word) < x - z) = (x < z)"
1491 "((x :: 'a :: len0 word) <= x - z) = (z = 0 | x < z)"
1494 lemma plus_minus_not_NULL_ab:
1495 "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> c ~= 0 \<Longrightarrow> x + c ~= 0"
1498 lemma plus_minus_no_overflow_ab:
1499 "(x :: 'a :: len0 word) <= ab - c \<Longrightarrow> c <= ab \<Longrightarrow> x <= x + c"
1503 "(a :: 'a :: len0 word) + c <= b \<Longrightarrow> a <= a + c \<Longrightarrow> c <= b - a"
1507 "(a :: 'a :: len0 word) <= b \<Longrightarrow> c <= b - a \<Longrightarrow> a + c <= b"
1510 lemmas le_plus = le_plus' [rotated]
1512 lemmas le_minus = leD [THEN thin_rl, THEN le_minus']
1514 lemma word_plus_mono_right:
1515 "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= x + z \<Longrightarrow> x + y <= x + z"
1518 lemma word_less_minus_cancel:
1519 "y - x < z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) < z"
1522 lemma word_less_minus_mono_left:
1523 "(y :: 'a :: len0 word) < z \<Longrightarrow> x <= y \<Longrightarrow> y - x < z - x"
1526 lemma word_less_minus_mono:
1527 "a < c \<Longrightarrow> d < b \<Longrightarrow> a - b < a \<Longrightarrow> c - d < c
1528 \<Longrightarrow> a - b < c - (d::'a::len word)"
1531 lemma word_le_minus_cancel:
1532 "y - x <= z - x \<Longrightarrow> x <= z \<Longrightarrow> (y :: 'a :: len0 word) <= z"
1535 lemma word_le_minus_mono_left:
1536 "(y :: 'a :: len0 word) <= z \<Longrightarrow> x <= y \<Longrightarrow> y - x <= z - x"
1539 lemma word_le_minus_mono:
1540 "a <= c \<Longrightarrow> d <= b \<Longrightarrow> a - b <= a \<Longrightarrow> c - d <= c
1541 \<Longrightarrow> a - b <= c - (d::'a::len word)"
1544 lemma plus_le_left_cancel_wrap:
1545 "(x :: 'a :: len0 word) + y' < x \<Longrightarrow> x + y < x \<Longrightarrow> (x + y' < x + y) = (y' < y)"
1548 lemma plus_le_left_cancel_nowrap:
1549 "(x :: 'a :: len0 word) <= x + y' \<Longrightarrow> x <= x + y \<Longrightarrow>
1550 (x + y' < x + y) = (y' < y)"
1553 lemma word_plus_mono_right2:
1554 "(a :: 'a :: len0 word) <= a + b \<Longrightarrow> c <= b \<Longrightarrow> a <= a + c"
1557 lemma word_less_add_right:
1558 "(x :: 'a :: len0 word) < y - z \<Longrightarrow> z <= y \<Longrightarrow> x + z < y"
1561 lemma word_less_sub_right:
1562 "(x :: 'a :: len0 word) < y + z \<Longrightarrow> y <= x \<Longrightarrow> x - y < z"
1565 lemma word_le_plus_either:
1566 "(x :: 'a :: len0 word) <= y | x <= z \<Longrightarrow> y <= y + z \<Longrightarrow> x <= y + z"
1569 lemma word_less_nowrapI:
1570 "(x :: 'a :: len0 word) < z - k \<Longrightarrow> k <= z \<Longrightarrow> 0 < k \<Longrightarrow> x < x + k"
1573 lemma inc_le: "(i :: 'a :: len word) < m \<Longrightarrow> i + 1 <= m"
1577 "(1 :: 'a :: len word) <= i \<Longrightarrow> i < m \<Longrightarrow> 1 <= (i + 1) & i + 1 <= m"
1580 lemma udvd_incr_lem:
1581 "up < uq \<Longrightarrow> up = ua + n * uint K \<Longrightarrow>
1582 uq = ua + n' * uint K \<Longrightarrow> up + uint K <= uq"
1584 apply (drule less_le_mult)
1589 "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
1590 uint q = ua + n' * uint K \<Longrightarrow> p + K <= q"
1591 apply (unfold word_less_alt word_le_def)
1592 apply (drule (2) udvd_incr_lem)
1593 apply (erule uint_add_le [THEN order_trans])
1597 "p < q \<Longrightarrow> uint p = ua + n * uint K \<Longrightarrow>
1598 uint q = ua + n' * uint K \<Longrightarrow> p <= q - K"
1599 apply (unfold word_less_alt word_le_def)
1600 apply (drule (2) udvd_incr_lem)
1601 apply (drule le_diff_eq [THEN iffD2])
1602 apply (erule order_trans)
1603 apply (rule uint_sub_ge)
1606 lemmas udvd_incr_lem0 = udvd_incr_lem [where ua=0, unfolded add_0_left]
1607 lemmas udvd_incr0 = udvd_incr' [where ua=0, unfolded add_0_left]
1608 lemmas udvd_decr0 = udvd_decr' [where ua=0, unfolded add_0_left]
1610 lemma udvd_minus_le':
1611 "xy < k \<Longrightarrow> z udvd xy \<Longrightarrow> z udvd k \<Longrightarrow> xy <= k - z"
1612 apply (unfold udvd_def)
1614 apply (erule (2) udvd_decr0)
1617 ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
1620 "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow>
1621 0 < K \<Longrightarrow> p <= p + K & p + K <= a + s"
1622 apply (unfold udvd_def)
1624 apply (simp add: uint_arith_simps split: split_if_asm)
1626 apply (insert uint_range' [of s])[1]
1628 apply (drule add_commute [THEN xtr1])
1629 apply (simp add: diff_less_eq [symmetric])
1630 apply (drule less_le_mult)
1635 ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
1637 (* links with rbl operations *)
1638 lemma word_succ_rbl:
1639 "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = (rev (rbl_succ (rev bl)))"
1640 apply (unfold word_succ_def)
1642 apply (simp add: to_bl_of_bin)
1643 apply (simp add: to_bl_def rbl_succ)
1646 lemma word_pred_rbl:
1647 "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = (rev (rbl_pred (rev bl)))"
1648 apply (unfold word_pred_def)
1650 apply (simp add: to_bl_of_bin)
1651 apply (simp add: to_bl_def rbl_pred)
1655 "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
1656 to_bl (v + w) = (rev (rbl_add (rev vbl) (rev wbl)))"
1657 apply (unfold word_add_def)
1659 apply (simp add: to_bl_of_bin)
1660 apply (simp add: to_bl_def rbl_add)
1663 lemma word_mult_rbl:
1664 "to_bl v = vbl \<Longrightarrow> to_bl w = wbl \<Longrightarrow>
1665 to_bl (v * w) = (rev (rbl_mult (rev vbl) (rev wbl)))"
1666 apply (unfold word_mult_def)
1668 apply (simp add: to_bl_of_bin)
1669 apply (simp add: to_bl_def rbl_mult)
1672 lemma rtb_rbl_ariths:
1673 "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_succ w)) = rbl_succ ys"
1674 "rev (to_bl w) = ys \<Longrightarrow> rev (to_bl (word_pred w)) = rbl_pred ys"
1675 "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v * w)) = rbl_mult ys xs"
1676 "rev (to_bl v) = ys \<Longrightarrow> rev (to_bl w) = xs \<Longrightarrow> rev (to_bl (v + w)) = rbl_add ys xs"
1677 by (auto simp: rev_swap [symmetric] word_succ_rbl
1678 word_pred_rbl word_mult_rbl word_add_rbl)
1681 subsection "Arithmetic type class instantiations"
1683 (* note that iszero_def is only for class comm_semiring_1_cancel,
1684 which requires word length >= 1, ie 'a :: len word *)
1685 lemma zero_bintrunc:
1686 "iszero (number_of x :: 'a :: len word) =
1687 (bintrunc (len_of TYPE('a)) x = Int.Pls)"
1688 apply (unfold iszero_def word_0_wi word_no_wi)
1689 apply (rule word_ubin.norm_eq_iff [symmetric, THEN trans])
1690 apply (simp add : Pls_def [symmetric])
1693 lemmas word_le_0_iff [simp] =
1694 word_zero_le [THEN leD, THEN linorder_antisym_conv1]
1696 lemma word_of_int_nat:
1697 "0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
1698 by (simp add: of_nat_nat word_of_int)
1700 lemma iszero_word_no [simp] :
1701 "iszero (number_of bin :: 'a :: len word) =
1702 iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
1703 apply (simp add: zero_bintrunc number_of_is_id)
1704 apply (unfold iszero_def Pls_def)
1709 subsection "Word and nat"
1711 lemma td_ext_unat [OF refl]:
1712 "n = len_of TYPE ('a :: len) \<Longrightarrow>
1713 td_ext (unat :: 'a word => nat) of_nat
1714 (unats n) (%i. i mod 2 ^ n)"
1715 apply (unfold td_ext_def' unat_def word_of_nat unats_uints)
1716 apply (auto intro!: imageI simp add : word_of_int_hom_syms)
1717 apply (erule word_uint.Abs_inverse [THEN arg_cong])
1718 apply (simp add: int_word_uint nat_mod_distrib nat_power_eq)
1721 lemmas unat_of_nat = td_ext_unat [THEN td_ext.eq_norm]
1723 interpretation word_unat:
1724 td_ext "unat::'a::len word => nat"
1726 "unats (len_of TYPE('a::len))"
1727 "%i. i mod 2 ^ len_of TYPE('a::len)"
1728 by (rule td_ext_unat)
1730 lemmas td_unat = word_unat.td_thm
1732 lemmas unat_lt2p [iff] = word_unat.Rep [unfolded unats_def mem_Collect_eq]
1734 lemma unat_le: "y <= unat (z :: 'a :: len word) \<Longrightarrow> y : unats (len_of TYPE ('a))"
1735 apply (unfold unats_def)
1737 apply (rule xtrans, rule unat_lt2p, assumption)
1740 lemma word_nchotomy:
1741 "ALL w. EX n. (w :: 'a :: len word) = of_nat n & n < 2 ^ len_of TYPE ('a)"
1743 apply (rule word_unat.Abs_cases)
1744 apply (unfold unats_def)
1749 fixes w :: "'a::len word"
1750 shows "(of_nat n = w) = (\<exists>q. n = unat w + q * 2 ^ len_of TYPE('a))"
1752 apply (rule word_unat.inverse_norm)
1754 apply (rule mod_eqD)
1759 lemma of_nat_eq_size:
1760 "(of_nat n = w) = (EX q. n = unat w + q * 2 ^ size w)"
1761 unfolding word_size by (rule of_nat_eq)
1764 "(of_nat m = (0::'a::len word)) = (\<exists>q. m = q * 2 ^ len_of TYPE('a))"
1765 by (simp add: of_nat_eq)
1767 lemma of_nat_2p [simp]:
1768 "of_nat (2 ^ len_of TYPE('a)) = (0::'a::len word)"
1769 by (fact mult_1 [symmetric, THEN iffD2 [OF of_nat_0 exI]])
1771 lemma of_nat_gt_0: "of_nat k ~= 0 \<Longrightarrow> 0 < k"
1775 "0 < k \<Longrightarrow> k < 2 ^ len_of TYPE ('a :: len) \<Longrightarrow> of_nat k ~= (0 :: 'a word)"
1776 by (clarsimp simp add : of_nat_0)
1778 lemma Abs_fnat_hom_add:
1779 "of_nat a + of_nat b = of_nat (a + b)"
1782 lemma Abs_fnat_hom_mult:
1783 "of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
1784 by (simp add: word_of_nat word_of_int_mult_hom zmult_int)
1786 lemma Abs_fnat_hom_Suc:
1787 "word_succ (of_nat a) = of_nat (Suc a)"
1788 by (simp add: word_of_nat word_of_int_succ_hom add_ac)
1790 lemma Abs_fnat_hom_0: "(0::'a::len word) = of_nat 0"
1793 lemma Abs_fnat_hom_1: "(1::'a::len word) = of_nat (Suc 0)"
1796 lemmas Abs_fnat_homs =
1797 Abs_fnat_hom_add Abs_fnat_hom_mult Abs_fnat_hom_Suc
1798 Abs_fnat_hom_0 Abs_fnat_hom_1
1800 lemma word_arith_nat_add:
1801 "a + b = of_nat (unat a + unat b)"
1804 lemma word_arith_nat_mult:
1805 "a * b = of_nat (unat a * unat b)"
1806 by (simp add: of_nat_mult)
1808 lemma word_arith_nat_Suc:
1809 "word_succ a = of_nat (Suc (unat a))"
1810 by (subst Abs_fnat_hom_Suc [symmetric]) simp
1812 lemma word_arith_nat_div:
1813 "a div b = of_nat (unat a div unat b)"
1814 by (simp add: word_div_def word_of_nat zdiv_int uint_nat)
1816 lemma word_arith_nat_mod:
1817 "a mod b = of_nat (unat a mod unat b)"
1818 by (simp add: word_mod_def word_of_nat zmod_int uint_nat)
1820 lemmas word_arith_nat_defs =
1821 word_arith_nat_add word_arith_nat_mult
1822 word_arith_nat_Suc Abs_fnat_hom_0
1823 Abs_fnat_hom_1 word_arith_nat_div
1826 lemma unat_cong: "x = y \<Longrightarrow> unat x = unat y"
1829 lemmas unat_word_ariths = word_arith_nat_defs
1830 [THEN trans [OF unat_cong unat_of_nat]]
1832 lemmas word_sub_less_iff = word_sub_le_iff
1833 [unfolded linorder_not_less [symmetric] Not_eq_iff]
1836 "(unat x + unat y < 2 ^ len_of TYPE('a)) =
1837 (unat (x + y :: 'a :: len word) = unat x + unat y)"
1838 unfolding unat_word_ariths
1839 by (auto intro!: trans [OF _ nat_mod_lem])
1841 lemma unat_mult_lem:
1842 "(unat x * unat y < 2 ^ len_of TYPE('a)) =
1843 (unat (x * y :: 'a :: len word) = unat x * unat y)"
1844 unfolding unat_word_ariths
1845 by (auto intro!: trans [OF _ nat_mod_lem])
1847 lemmas unat_plus_if' = trans [OF unat_word_ariths(1) mod_nat_add, simplified]
1849 lemma le_no_overflow:
1850 "x <= b \<Longrightarrow> a <= a + b \<Longrightarrow> x <= a + (b :: 'a :: len0 word)"
1851 apply (erule order_trans)
1852 apply (erule olen_add_eqv [THEN iffD1])
1855 lemmas un_ui_le = trans [OF word_le_nat_alt [symmetric] word_le_def]
1857 lemma unat_sub_if_size:
1858 "unat (x - y) = (if unat y <= unat x
1859 then unat x - unat y
1860 else unat x + 2 ^ size x - unat y)"
1861 apply (unfold word_size)
1862 apply (simp add: un_ui_le)
1863 apply (auto simp add: unat_def uint_sub_if')
1864 apply (rule nat_diff_distrib)
1866 apply (simp add: algebra_simps)
1867 apply (rule nat_diff_distrib [THEN trans])
1869 apply (subst nat_add_distrib)
1871 apply (simp add: nat_power_eq)
1876 lemmas unat_sub_if' = unat_sub_if_size [unfolded word_size]
1878 lemma unat_div: "unat ((x :: 'a :: len word) div y) = unat x div unat y"
1879 apply (simp add : unat_word_ariths)
1880 apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
1881 apply (rule div_le_dividend)
1884 lemma unat_mod: "unat ((x :: 'a :: len word) mod y) = unat x mod unat y"
1885 apply (clarsimp simp add : unat_word_ariths)
1886 apply (cases "unat y")
1888 apply (rule unat_lt2p [THEN xtr7, THEN nat_mod_eq'])
1889 apply (rule mod_le_divisor)
1893 lemma uint_div: "uint ((x :: 'a :: len word) div y) = uint x div uint y"
1894 unfolding uint_nat by (simp add : unat_div zdiv_int)
1896 lemma uint_mod: "uint ((x :: 'a :: len word) mod y) = uint x mod uint y"
1897 unfolding uint_nat by (simp add : unat_mod zmod_int)
1900 subsection {* Definition of unat\_arith tactic *}
1903 fixes x::"'a::len word"
1905 (ALL n. of_nat n = x & n < 2^len_of TYPE('a) --> P n)"
1906 by (auto simp: unat_of_nat)
1908 lemma unat_split_asm:
1909 fixes x::"'a::len word"
1911 (~(EX n. of_nat n = x & n < 2^len_of TYPE('a) & ~ P n))"
1912 by (auto simp: unat_of_nat)
1914 lemmas of_nat_inverse =
1915 word_unat.Abs_inverse' [rotated, unfolded unats_def, simplified]
1917 lemmas unat_splits = unat_split unat_split_asm
1919 lemmas unat_arith_simps =
1920 word_le_nat_alt word_less_nat_alt
1921 word_unat.Rep_inject [symmetric]
1922 unat_sub_if' unat_plus_if' unat_div unat_mod
1924 (* unat_arith_tac: tactic to reduce word arithmetic to nat,
1925 try to solve via arith *)
1927 fun unat_arith_ss_of ss =
1928 ss addsimps @{thms unat_arith_simps}
1929 delsimps @{thms word_unat.Rep_inject}
1930 |> fold Splitter.add_split @{thms split_if_asm}
1931 |> fold Simplifier.add_cong @{thms power_False_cong}
1933 fun unat_arith_tacs ctxt =
1935 fun arith_tac' n t =
1936 Arith_Data.verbose_arith_tac ctxt n t
1937 handle Cooper.COOPER _ => Seq.empty;
1939 [ clarify_tac ctxt 1,
1940 full_simp_tac (unat_arith_ss_of (simpset_of ctxt)) 1,
1941 ALLGOALS (full_simp_tac (HOL_ss |> fold Splitter.add_split @{thms unat_splits}
1942 |> fold Simplifier.add_cong @{thms power_False_cong})),
1943 rewrite_goals_tac @{thms word_size},
1944 ALLGOALS (fn n => REPEAT (resolve_tac [allI, impI] n) THEN
1945 REPEAT (etac conjE n) THEN
1946 REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)),
1950 fun unat_arith_tac ctxt = SELECT_GOAL (EVERY (unat_arith_tacs ctxt))
1953 method_setup unat_arith =
1954 {* Scan.succeed (SIMPLE_METHOD' o unat_arith_tac) *}
1955 "solving word arithmetic via natural numbers and arith"
1957 lemma no_plus_overflow_unat_size:
1958 "((x :: 'a :: len word) <= x + y) = (unat x + unat y < 2 ^ size x)"
1959 unfolding word_size by unat_arith
1961 lemmas no_olen_add_nat = no_plus_overflow_unat_size [unfolded word_size]
1963 lemmas unat_plus_simple = trans [OF no_olen_add_nat unat_add_lem]
1965 lemma word_div_mult:
1966 "(0 :: 'a :: len word) < y \<Longrightarrow> unat x * unat y < 2 ^ len_of TYPE('a) \<Longrightarrow>
1970 apply (subst unat_mult_lem [THEN iffD1])
1974 lemma div_lt': "(i :: 'a :: len word) <= k div x \<Longrightarrow>
1975 unat i * unat x < 2 ^ len_of TYPE('a)"
1978 apply (drule mult_le_mono1)
1979 apply (erule order_le_less_trans)
1980 apply (rule xtr7 [OF unat_lt2p div_mult_le])
1983 lemmas div_lt'' = order_less_imp_le [THEN div_lt']
1985 lemma div_lt_mult: "(i :: 'a :: len word) < k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x < k"
1986 apply (frule div_lt'' [THEN unat_mult_lem [THEN iffD1]])
1987 apply (simp add: unat_arith_simps)
1988 apply (drule (1) mult_less_mono1)
1989 apply (erule order_less_le_trans)
1990 apply (rule div_mult_le)
1994 "(i :: 'a :: len word) <= k div x \<Longrightarrow> 0 < x \<Longrightarrow> i * x <= k"
1995 apply (frule div_lt' [THEN unat_mult_lem [THEN iffD1]])
1996 apply (simp add: unat_arith_simps)
1997 apply (drule mult_le_mono1)
1998 apply (erule order_trans)
1999 apply (rule div_mult_le)
2003 "(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
2004 apply (unfold uint_nat)
2005 apply (drule div_lt')
2006 apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric]
2010 lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
2012 lemma word_le_exists':
2013 "(x :: 'a :: len0 word) <= y \<Longrightarrow>
2014 (EX z. y = x + z & uint x + uint z < 2 ^ len_of TYPE('a))"
2017 apply (rule zadd_diff_inverse)
2021 lemmas plus_minus_not_NULL = order_less_imp_le [THEN plus_minus_not_NULL_ab]
2023 lemmas plus_minus_no_overflow =
2024 order_less_imp_le [THEN plus_minus_no_overflow_ab]
2026 lemmas mcs = word_less_minus_cancel word_less_minus_mono_left
2027 word_le_minus_cancel word_le_minus_mono_left
2029 lemmas word_l_diffs = mcs [where y = "w + x", unfolded add_diff_cancel] for w x
2030 lemmas word_diff_ls = mcs [where z = "w + x", unfolded add_diff_cancel] for w x
2031 lemmas word_plus_mcs = word_diff_ls [where y = "v + x", unfolded add_diff_cancel] for v x
2033 lemmas le_unat_uoi = unat_le [THEN word_unat.Abs_inverse]
2035 lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
2038 "a div b * b \<le> (a::nat)"
2039 using gt_or_eq_0 [of b]
2041 apply (erule xtr4 [OF thd mult_commute])
2045 lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1
2047 lemma word_mod_div_equality:
2048 "(n div b) * b + (n mod b) = (n :: 'a :: len word)"
2049 apply (unfold word_less_nat_alt word_arith_nat_defs)
2050 apply (cut_tac y="unat b" in gt_or_eq_0)
2052 apply (simp add: mod_div_equality uno_simps)
2056 lemma word_div_mult_le: "a div b * b <= (a::'a::len word)"
2057 apply (unfold word_le_nat_alt word_arith_nat_defs)
2058 apply (cut_tac y="unat b" in gt_or_eq_0)
2060 apply (simp add: div_mult_le uno_simps)
2064 lemma word_mod_less_divisor: "0 < n \<Longrightarrow> m mod n < (n :: 'a :: len word)"
2065 apply (simp only: word_less_nat_alt word_arith_nat_defs)
2066 apply (clarsimp simp add : uno_simps)
2069 lemma word_of_int_power_hom:
2070 "word_of_int a ^ n = (word_of_int (a ^ n) :: 'a :: len word)"
2071 by (induct n) (simp_all add: wi_hom_mult [symmetric])
2073 lemma word_arith_power_alt:
2074 "a ^ n = (word_of_int (uint a ^ n) :: 'a :: len word)"
2075 by (simp add : word_of_int_power_hom [symmetric])
2077 lemma of_bl_length_less:
2078 "length x = k \<Longrightarrow> k < len_of TYPE('a) \<Longrightarrow> (of_bl x :: 'a :: len word) < 2 ^ k"
2079 apply (unfold of_bl_no [unfolded word_number_of_def]
2080 word_less_alt word_number_of_alt)
2082 apply (simp (no_asm) add: word_of_int_power_hom word_uint.eq_norm
2083 del: word_of_int_bin)
2084 apply (simp add: mod_pos_pos_trivial)
2085 apply (subst mod_pos_pos_trivial)
2086 apply (rule bl_to_bin_ge0)
2087 apply (rule order_less_trans)
2088 apply (rule bl_to_bin_lt2p)
2090 apply (rule bl_to_bin_lt2p)
2094 subsection "Cardinality, finiteness of set of words"
2096 instance word :: (len0) finite
2097 by (default, simp add: type_definition.univ [OF type_definition_word])
2099 lemma card_word: "CARD('a::len0 word) = 2 ^ len_of TYPE('a)"
2100 by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
2102 lemma card_word_size:
2103 "card (UNIV :: 'a :: len0 word set) = (2 ^ size (x :: 'a word))"
2104 unfolding word_size by (rule card_word)
2107 subsection {* Bitwise Operations on Words *}
2109 lemmas bin_log_bintrs = bin_trunc_not bin_trunc_xor bin_trunc_and bin_trunc_or
2111 (* following definitions require both arithmetic and bit-wise word operations *)
2113 (* to get word_no_log_defs from word_log_defs, using bin_log_bintrs *)
2114 lemmas wils1 = bin_log_bintrs [THEN word_ubin.norm_eq_iff [THEN iffD1],
2115 folded word_ubin.eq_norm, THEN eq_reflection]
2117 (* the binary operations only *)
2118 lemmas word_log_binary_defs =
2119 word_and_def word_or_def word_xor_def
2121 lemmas word_no_log_defs [simp] =
2122 word_not_def [where a="number_of a",
2123 unfolded word_no_wi wils1, folded word_no_wi]
2124 word_log_binary_defs [where a="number_of a" and b="number_of b",
2125 unfolded word_no_wi wils1, folded word_no_wi]
2128 lemmas word_wi_log_defs = word_no_log_defs [unfolded word_no_wi]
2130 lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
2131 by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
2132 bin_trunc_ao(2) [symmetric])
2134 lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
2135 by (simp add: word_and_def word_wi_log_defs word_ubin.eq_norm
2136 bin_trunc_ao(1) [symmetric])
2138 lemma word_ops_nth_size:
2139 "n < size (x::'a::len0 word) \<Longrightarrow>
2140 (x OR y) !! n = (x !! n | y !! n) &
2141 (x AND y) !! n = (x !! n & y !! n) &
2142 (x XOR y) !! n = (x !! n ~= y !! n) &
2143 (NOT x) !! n = (~ x !! n)"
2144 unfolding word_size word_test_bit_def word_log_defs
2145 by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
2148 fixes x :: "'a::len0 word"
2149 shows "(x OR y) !! n = (x !! n | y !! n) &
2150 (x AND y) !! n = (x !! n & y !! n)"
2151 apply (cases "n < size x")
2152 apply (drule_tac y = "y" in word_ops_nth_size)
2154 apply (simp add : test_bit_bin word_size)
2157 (* get from commutativity, associativity etc of int_and etc
2158 to same for word_and etc *)
2166 lemma word_bw_assocs:
2167 fixes x :: "'a::len0 word"
2169 "(x AND y) AND z = x AND y AND z"
2170 "(x OR y) OR z = x OR y OR z"
2171 "(x XOR y) XOR z = x XOR y XOR z"
2172 using word_of_int_Ex [where x=x]
2173 word_of_int_Ex [where x=y]
2174 word_of_int_Ex [where x=z]
2175 by (auto simp: bwsimps bbw_assocs)
2177 lemma word_bw_comms:
2178 fixes x :: "'a::len0 word"
2183 using word_of_int_Ex [where x=x]
2184 word_of_int_Ex [where x=y]
2185 by (auto simp: bwsimps bin_ops_comm)
2188 fixes x :: "'a::len0 word"
2190 "y AND x AND z = x AND y AND z"
2191 "y OR x OR z = x OR y OR z"
2192 "y XOR x XOR z = x XOR y XOR z"
2193 using word_of_int_Ex [where x=x]
2194 word_of_int_Ex [where x=y]
2195 word_of_int_Ex [where x=z]
2196 by (auto simp: bwsimps)
2198 lemma word_log_esimps [simp]:
2199 fixes x :: "'a::len0 word"
2213 using word_of_int_Ex [where x=x]
2214 by (auto simp: bwsimps)
2216 lemma word_not_dist:
2217 fixes x :: "'a::len0 word"
2219 "NOT (x OR y) = NOT x AND NOT y"
2220 "NOT (x AND y) = NOT x OR NOT y"
2221 using word_of_int_Ex [where x=x]
2222 word_of_int_Ex [where x=y]
2223 by (auto simp: bwsimps bbw_not_dist)
2226 fixes x :: "'a::len0 word"
2231 using word_of_int_Ex [where x=x]
2232 by (auto simp: bwsimps)
2234 lemma word_ao_absorbs [simp]:
2235 fixes x :: "'a::len0 word"
2237 "x AND (y OR x) = x"
2239 "x AND (x OR y) = x"
2241 "(y OR x) AND x = x"
2243 "(x OR y) AND x = x"
2245 using word_of_int_Ex [where x=x]
2246 word_of_int_Ex [where x=y]
2247 by (auto simp: bwsimps)
2249 lemma word_not_not [simp]:
2250 "NOT NOT (x::'a::len0 word) = x"
2251 using word_of_int_Ex [where x=x]
2252 by (auto simp: bwsimps)
2255 fixes x :: "'a::len0 word"
2256 shows "(x OR y) AND z = x AND z OR y AND z"
2257 using word_of_int_Ex [where x=x]
2258 word_of_int_Ex [where x=y]
2259 word_of_int_Ex [where x=z]
2260 by (auto simp: bwsimps bbw_ao_dist)
2263 fixes x :: "'a::len0 word"
2264 shows "x AND y OR z = (x OR z) AND (y OR z)"
2265 using word_of_int_Ex [where x=x]
2266 word_of_int_Ex [where x=y]
2267 word_of_int_Ex [where x=z]
2268 by (auto simp: bwsimps bbw_oa_dist)
2270 lemma word_add_not [simp]:
2271 fixes x :: "'a::len0 word"
2272 shows "x + NOT x = -1"
2273 using word_of_int_Ex [where x=x]
2274 by (auto simp: bwsimps bin_add_not)
2276 lemma word_plus_and_or [simp]:
2277 fixes x :: "'a::len0 word"
2278 shows "(x AND y) + (x OR y) = x + y"
2279 using word_of_int_Ex [where x=x]
2280 word_of_int_Ex [where x=y]
2281 by (auto simp: bwsimps plus_and_or)
2284 fixes x :: "'a::len0 word"
2285 shows "(w = (x OR y)) \<Longrightarrow> (y = (w AND y))" by auto
2287 fixes x' :: "'a::len0 word"
2288 shows "(w' = (x' AND y')) \<Longrightarrow> (x' = (x' OR w'))" by auto
2290 lemmas word_ao_equiv = leao [COMP leoa [COMP iffI]]
2292 lemma le_word_or2: "x <= x OR (y::'a::len0 word)"
2293 unfolding word_le_def uint_or
2294 by (auto intro: le_int_or)
2296 lemmas le_word_or1 = xtr3 [OF word_bw_comms (2) le_word_or2]
2297 lemmas word_and_le1 = xtr3 [OF word_ao_absorbs (4) [symmetric] le_word_or2]
2298 lemmas word_and_le2 = xtr3 [OF word_ao_absorbs (8) [symmetric] le_word_or2]
2300 lemma bl_word_not: "to_bl (NOT w) = map Not (to_bl w)"
2301 unfolding to_bl_def word_log_defs bl_not_bin
2302 by (simp add: word_ubin.eq_norm)
2304 lemma bl_word_xor: "to_bl (v XOR w) = map2 op ~= (to_bl v) (to_bl w)"
2305 unfolding to_bl_def word_log_defs bl_xor_bin
2306 by (simp add: word_ubin.eq_norm)
2308 lemma bl_word_or: "to_bl (v OR w) = map2 op | (to_bl v) (to_bl w)"
2309 unfolding to_bl_def word_log_defs bl_or_bin
2310 by (simp add: word_ubin.eq_norm)
2312 lemma bl_word_and: "to_bl (v AND w) = map2 op & (to_bl v) (to_bl w)"
2313 unfolding to_bl_def word_log_defs bl_and_bin
2314 by (simp add: word_ubin.eq_norm)
2316 lemma word_lsb_alt: "lsb (w::'a::len0 word) = test_bit w 0"
2317 by (auto simp: word_test_bit_def word_lsb_def)
2319 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) & ~ lsb (0::'b::len0 word)"
2320 unfolding word_lsb_def uint_eq_0 uint_1 by simp
2322 lemma word_lsb_last: "lsb (w::'a::len word) = last (to_bl w)"
2323 apply (unfold word_lsb_def uint_bl bin_to_bl_def)
2324 apply (rule_tac bin="uint w" in bin_exhaust)
2325 apply (cases "size w")
2327 apply (auto simp add: bin_to_bl_aux_alt)
2330 lemma word_lsb_int: "lsb w = (uint w mod 2 = 1)"
2331 unfolding word_lsb_def bin_last_def by auto
2333 lemma word_msb_sint: "msb w = (sint w < 0)"
2334 unfolding word_msb_def
2335 by (simp add : sign_Min_lt_0 number_of_is_id)
2337 lemma word_msb_no [simp]:
2338 "msb (number_of bin :: 'a::len word) = bin_nth bin (len_of TYPE('a) - 1)"
2339 unfolding word_msb_def word_number_of_def
2340 by (clarsimp simp add: word_sbin.eq_norm bin_sign_lem)
2343 "msb (w::'a::len word) = bin_nth (uint w) (len_of TYPE('a) - 1)"
2344 apply (rule trans [OF _ word_msb_no])
2345 apply (simp add : word_number_of_def)
2348 lemma word_msb_alt: "msb (w::'a::len word) = hd (to_bl w)"
2349 apply (unfold word_msb_nth uint_bl)
2350 apply (subst hd_conv_nth)
2351 apply (rule length_greater_0_conv [THEN iffD1])
2353 apply (simp add : nth_bin_to_bl word_size)
2356 lemma word_set_nth [simp]:
2357 "set_bit w n (test_bit w n) = (w::'a::len0 word)"
2358 unfolding word_test_bit_def word_set_bit_def by auto
2360 lemma bin_nth_uint':
2361 "bin_nth (uint w) n = (rev (bin_to_bl (size w) (uint w)) ! n & n < size w)"
2362 apply (unfold word_size)
2363 apply (safe elim!: bin_nth_uint_imp)
2364 apply (frule bin_nth_uint_imp)
2365 apply (fast dest!: bin_nth_bl)+
2368 lemmas bin_nth_uint = bin_nth_uint' [unfolded word_size]
2370 lemma test_bit_bl: "w !! n = (rev (to_bl w) ! n & n < size w)"
2371 unfolding to_bl_def word_test_bit_def word_size
2372 by (rule bin_nth_uint)
2374 lemma to_bl_nth: "n < size w \<Longrightarrow> to_bl w ! n = w !! (size w - Suc n)"
2375 apply (unfold test_bit_bl)
2378 apply (rule nth_rev_alt)
2379 apply (auto simp add: word_size)
2383 fixes w :: "'a::len0 word"
2384 shows "(set_bit w n x) !! n = (n < size w & x)"
2385 unfolding word_size word_test_bit_def word_set_bit_def
2386 by (clarsimp simp add : word_ubin.eq_norm nth_bintr)
2388 lemma test_bit_set_gen:
2389 fixes w :: "'a::len0 word"
2390 shows "test_bit (set_bit w n x) m =
2391 (if m = n then n < size w & x else test_bit w m)"
2392 apply (unfold word_size word_test_bit_def word_set_bit_def)
2393 apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
2394 apply (auto elim!: test_bit_size [unfolded word_size]
2395 simp add: word_test_bit_def [symmetric])
2398 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
2399 unfolding of_bl_def bl_to_bin_rep_F by auto
2402 fixes w :: "'a::len word"
2403 shows "msb w = w !! (len_of TYPE('a) - 1)"
2404 unfolding word_msb_nth word_test_bit_def by simp
2406 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
2407 lemmas msb1 = msb0 [where i = 0]
2408 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
2410 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
2411 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
2413 lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
2414 "n = size (w::'a::len0 word) \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
2415 td_ext test_bit ofn {f. ALL i. f i --> i < n} (%h i. h i & i < n)"
2416 apply (unfold word_size td_ext_def')
2417 apply (safe del: subset_antisym)
2418 apply (rule_tac [3] ext)
2419 apply (rule_tac [4] ext)
2420 apply (unfold word_size of_nth_def test_bit_bl)
2423 apply (clarsimp simp: word_bl.Abs_inverse)+
2424 apply (rule word_bl.Rep_inverse')
2425 apply (rule sym [THEN trans])
2426 apply (rule bl_of_nth_nth)
2428 apply (rule bl_of_nth_inj)
2429 apply (clarsimp simp add : test_bit_bl word_size)
2432 interpretation test_bit:
2433 td_ext "op !! :: 'a::len0 word => nat => bool"
2435 "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}"
2436 "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))"
2437 by (rule td_ext_nth)
2439 lemmas td_nth = test_bit.td_thm
2441 lemma word_set_set_same [simp]:
2442 fixes w :: "'a::len0 word"
2443 shows "set_bit (set_bit w n x) n y = set_bit w n y"
2444 by (rule word_eqI) (simp add : test_bit_set_gen word_size)
2446 lemma word_set_set_diff:
2447 fixes w :: "'a::len0 word"
2449 shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
2450 by (rule word_eqI) (clarsimp simp add: test_bit_set_gen word_size assms)
2452 lemma test_bit_no [simp]:
2453 "(number_of bin :: 'a::len0 word) !! n \<equiv> n < len_of TYPE('a) \<and> bin_nth bin n"
2454 unfolding word_test_bit_def word_number_of_def word_size
2455 by (simp add : nth_bintr [symmetric] word_ubin.eq_norm)
2457 lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
2458 unfolding test_bit_no word_0_no by auto
2461 fixes w :: "'a::len word"
2462 defines "l \<equiv> len_of TYPE ('a)"
2463 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))"
2464 unfolding sint_uint l_def
2465 by (clarsimp simp add: nth_sbintr word_test_bit_def [symmetric])
2467 lemma word_lsb_no [simp]:
2468 "lsb (number_of bin :: 'a :: len word) = (bin_last bin = 1)"
2469 unfolding word_lsb_alt test_bit_no by auto
2471 lemma word_set_no [simp]:
2472 "set_bit (number_of bin::'a::len0 word) n b =
2473 number_of (bin_sc n (if b then 1 else 0) bin)"
2474 apply (unfold word_set_bit_def word_number_of_def [symmetric])
2475 apply (rule word_eqI)
2476 apply (clarsimp simp: word_size bin_nth_sc_gen number_of_is_id
2480 lemma setBit_no [simp]:
2481 "setBit (number_of bin) n = number_of (bin_sc n 1 bin) "
2482 by (simp add: setBit_def)
2484 lemma clearBit_no [simp]:
2485 "clearBit (number_of bin) n = number_of (bin_sc n 0 bin)"
2486 by (simp add: clearBit_def)
2489 "to_bl (-1::'a::len0 word) = replicate (len_of TYPE ('a)) True"
2490 apply (rule word_bl.Abs_inverse')
2492 apply (rule word_eqI)
2493 apply (clarsimp simp add: word_size)
2494 apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
2497 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
2498 unfolding word_msb_alt to_bl_n1 by simp
2500 lemma word_set_nth_iff:
2501 "(set_bit w n b = w) = (w !! n = b | n >= size (w::'a::len0 word))"
2504 apply (drule word_eqD)
2505 apply (erule sym [THEN trans])
2506 apply (simp add: test_bit_set)
2509 apply (rule word_eqI)
2510 apply (clarsimp simp add : test_bit_set_gen)
2511 apply (drule test_bit_size)
2516 "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a)"
2517 unfolding word_test_bit_def
2518 by (auto simp add: word_ubin.eq_norm nth_bintr nth_2p_bin)
2521 "((2\<Colon>'a\<Colon>len word) ^ n) !! m \<longleftrightarrow> m = n \<and> m < len_of TYPE('a\<Colon>len)"
2522 unfolding test_bit_2p [symmetric] word_of_int [symmetric]
2523 by (simp add: of_int_power)
2526 "(0::'a::len word) < 2 ^ n \<Longrightarrow> uint (2 ^ n::'a::len word) = 2 ^ n"
2527 apply (unfold word_arith_power_alt)
2528 apply (case_tac "len_of TYPE ('a)")
2530 apply (case_tac "nat")
2532 apply (case_tac "n")
2533 apply (clarsimp simp add : word_1_wi [symmetric])
2534 apply (clarsimp simp add : word_0_wi [symmetric] BIT_simps)
2535 apply (drule word_gt_0 [THEN iffD1])
2536 apply (safe intro!: word_eqI bin_nth_lem ext)
2537 apply (auto simp add: test_bit_2p nth_2p_bin word_test_bit_def [symmetric] BIT_simps)
2540 lemma word_of_int_2p: "(word_of_int (2 ^ n) :: 'a :: len word) = 2 ^ n"
2541 apply (unfold word_arith_power_alt)
2542 apply (case_tac "len_of TYPE ('a)")
2544 apply (case_tac "nat")
2545 apply (rule word_ubin.norm_eq_iff [THEN iffD1])
2546 apply (rule box_equals)
2547 apply (rule_tac [2] bintr_ariths (1))+
2548 apply (clarsimp simp add : number_of_is_id)
2549 apply (simp add: BIT_simps)
2552 lemma bang_is_le: "x !! m \<Longrightarrow> 2 ^ m <= (x :: 'a :: len word)"
2554 apply (rule_tac [2] y = "x" in le_word_or2)
2555 apply (rule word_eqI)
2556 apply (auto simp add: word_ao_nth nth_w2p word_size)
2560 fixes w :: "'a::len0 word"
2561 shows "w >= set_bit w n False"
2562 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
2564 apply (rule order_trans)
2565 apply (rule bintr_bin_clr_le)
2570 fixes w :: "'a::len word"
2571 shows "w <= set_bit w n True"
2572 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
2574 apply (rule order_trans [OF _ bintr_bin_set_ge])
2579 subsection {* Shifting, Rotating, and Splitting Words *}
2581 lemma shiftl1_number [simp] :
2582 "shiftl1 (number_of w) = number_of (w BIT 0)"
2583 apply (unfold shiftl1_def word_number_of_def)
2584 apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
2586 apply (subst refl [THEN bintrunc_BIT_I, symmetric])
2587 apply (subst bintrunc_bintrunc_min)
2591 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
2592 unfolding word_0_no shiftl1_number by (auto simp: BIT_simps)
2594 lemma shiftl1_def_u: "shiftl1 w = number_of (uint w BIT 0)"
2595 by (simp only: word_number_of_def shiftl1_def)
2597 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT 0)"
2598 by (rule trans [OF _ shiftl1_number]) simp
2600 lemma shiftr1_0 [simp]: "shiftr1 0 = 0"
2601 unfolding shiftr1_def by simp
2603 lemma sshiftr1_0 [simp]: "sshiftr1 0 = 0"
2604 unfolding sshiftr1_def by simp
2606 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
2607 unfolding sshiftr1_def by auto
2609 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
2610 unfolding shiftl_def by (induct n) auto
2612 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
2613 unfolding shiftr_def by (induct n) auto
2615 lemma sshiftr_0 [simp] : "0 >>> n = 0"
2616 unfolding sshiftr_def by (induct n) auto
2618 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
2619 unfolding sshiftr_def by (induct n) auto
2621 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
2622 apply (unfold shiftl1_def word_test_bit_def)
2623 apply (simp add: nth_bintr word_ubin.eq_norm word_size)
2628 lemma nth_shiftl' [rule_format]:
2629 "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
2630 apply (unfold shiftl_def)
2632 apply (force elim!: test_bit_size)
2633 apply (clarsimp simp add : nth_shiftl1 word_size)
2637 lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
2639 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
2640 apply (unfold shiftr1_def word_test_bit_def)
2641 apply (simp add: nth_bintr word_ubin.eq_norm)
2643 apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
2648 "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
2649 apply (unfold shiftr_def)
2651 apply (auto simp add : nth_shiftr1)
2654 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
2655 where f (ie bin_rest) takes normal arguments to normal results,
2656 thus we get (2) from (1) *)
2658 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
2659 apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
2660 apply (subst bintr_uint [symmetric, OF order_refl])
2661 apply (simp only : bintrunc_bintrunc_l)
2666 "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
2667 apply (unfold sshiftr1_def word_test_bit_def)
2668 apply (simp add: nth_bintr word_ubin.eq_norm
2669 bin_nth.Suc [symmetric] word_size
2671 apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
2672 apply (auto simp add: bin_nth_sint)
2675 lemma nth_sshiftr [rule_format] :
2676 "ALL n. sshiftr w m !! n = (n < size w &
2677 (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
2678 apply (unfold sshiftr_def)
2679 apply (induct_tac "m")
2680 apply (simp add: test_bit_bl)
2681 apply (clarsimp simp add: nth_sshiftr1 word_size)
2685 apply (erule thin_rl)
2690 apply (erule thin_rl)
2698 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
2699 apply (unfold shiftr1_def bin_rest_def)
2700 apply (rule word_uint.Abs_inverse)
2701 apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
2704 apply (rule zdiv_le_dividend)
2708 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
2709 apply (unfold sshiftr1_def bin_rest_def [symmetric])
2710 apply (simp add: word_sbin.eq_norm)
2713 apply (subst word_sbin.norm_Rep [symmetric])
2715 apply (subst word_sbin.norm_Rep [symmetric])
2716 apply (unfold One_nat_def)
2717 apply (rule sbintrunc_rest)
2720 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
2721 apply (unfold shiftr_def)
2724 apply (simp add: shiftr1_div_2 mult_commute
2725 zdiv_zmult2_eq [symmetric])
2728 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
2729 apply (unfold sshiftr_def)
2732 apply (simp add: sshiftr1_div_2 mult_commute
2733 zdiv_zmult2_eq [symmetric])
2736 subsubsection "shift functions in terms of lists of bools"
2738 lemmas bshiftr1_no_bin [simp] =
2739 bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin] for w
2741 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
2742 unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
2744 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
2745 unfolding uint_bl of_bl_no
2746 by (simp add: bl_to_bin_aux_append bl_to_bin_def)
2748 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
2750 have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
2751 also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
2752 finally show ?thesis .
2756 "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
2757 apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
2758 apply (fast intro!: Suc_leI)
2761 (* Generalized version of bl_shiftl1. Maybe this one should replace it? *)
2763 "to_bl (shiftl1 w) = tl (to_bl w @ [False])"
2764 unfolding shiftl1_bl
2765 by (simp add: word_rep_drop drop_Suc del: drop_append)
2767 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
2768 apply (unfold shiftr1_def uint_bl of_bl_def)
2769 apply (simp add: butlast_rest_bin word_size)
2770 apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
2774 "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
2775 unfolding shiftr1_bl
2776 by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
2778 (* Generalized version of bl_shiftr1. Maybe this one should replace it? *)
2780 "to_bl (shiftr1 w) = butlast (False # to_bl w)"
2781 apply (rule word_bl.Abs_inverse')
2782 apply (simp del: butlast.simps)
2783 apply (simp add: shiftr1_bl of_bl_def)
2787 "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
2788 apply (unfold word_reverse_def)
2789 apply (rule word_bl.Rep_inverse' [symmetric])
2790 apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
2791 apply (cases "to_bl w")
2796 "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
2797 apply (unfold shiftl_def shiftr_def)
2799 apply (auto simp add : shiftl1_rev)
2802 lemma rev_shiftl: "word_reverse w << n = word_reverse (w >> n)"
2803 by (simp add: shiftl_rev)
2805 lemma shiftr_rev: "w >> n = word_reverse (word_reverse w << n)"
2806 by (simp add: rev_shiftl)
2808 lemma rev_shiftr: "word_reverse w >> n = word_reverse (w << n)"
2809 by (simp add: shiftr_rev)
2812 "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
2813 apply (unfold sshiftr1_def uint_bl word_size)
2814 apply (simp add: butlast_rest_bin word_ubin.eq_norm)
2815 apply (simp add: sint_uint)
2816 apply (rule nth_equalityI)
2820 apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
2821 nth_bin_to_bl bin_nth.Suc [symmetric]
2826 apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
2831 "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)"
2832 apply (unfold shiftr_def)
2835 apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
2836 apply (rule butlast_take [THEN trans])
2837 apply (auto simp: word_size)
2841 "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
2842 apply (unfold sshiftr_def)
2845 apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
2846 apply (rule butlast_take [THEN trans])
2847 apply (auto simp: word_size)
2851 "n \<le> size w \<Longrightarrow> take n (to_bl (w >> n)) = replicate n False"
2852 apply (unfold shiftr_def)
2855 apply (simp add: bl_shiftr1' length_0_conv [symmetric] word_size)
2856 apply (rule take_butlast [THEN trans])
2857 apply (auto simp: word_size)
2860 lemma take_sshiftr' [rule_format] :
2861 "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
2862 take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
2863 apply (unfold sshiftr_def)
2866 apply (simp add: bl_sshiftr1)
2868 apply (rule take_butlast [THEN trans])
2869 apply (auto simp: word_size)
2872 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1]
2873 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2]
2875 lemma atd_lem: "take n xs = t \<Longrightarrow> drop n xs = d \<Longrightarrow> xs = t @ d"
2876 by (auto intro: append_take_drop_id [symmetric])
2878 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
2879 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
2881 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
2882 unfolding shiftl_def
2883 by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
2886 "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
2888 have "w << n = of_bl (to_bl w) << n" by simp
2889 also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
2890 finally show ?thesis .
2893 lemmas shiftl_number [simp] = shiftl_def [where w="number_of w"] for w
2896 "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
2897 by (simp add: shiftl_bl word_rep_drop word_size)
2899 lemma shiftl_zero_size:
2900 fixes x :: "'a::len0 word"
2901 shows "size x <= n \<Longrightarrow> x << n = 0"
2902 apply (unfold word_size)
2903 apply (rule word_eqI)
2904 apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
2907 (* note - the following results use 'a :: len word < number_ring *)
2909 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
2910 apply (simp add: shiftl1_def_u BIT_simps)
2911 apply (simp only: double_number_of_Bit0 [symmetric])
2915 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
2916 apply (simp add: shiftl1_def_u BIT_simps)
2917 apply (simp only: double_number_of_Bit0 [symmetric])
2921 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
2922 unfolding shiftl_def
2923 by (induct n) (auto simp: shiftl1_2t)
2925 lemma shiftr1_bintr [simp]:
2926 "(shiftr1 (number_of w) :: 'a :: len0 word) =
2927 number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))"
2928 unfolding shiftr1_def word_number_of_def
2929 by (simp add : word_ubin.eq_norm)
2931 lemma sshiftr1_sbintr [simp] :
2932 "(sshiftr1 (number_of w) :: 'a :: len word) =
2933 number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))"
2934 unfolding sshiftr1_def word_number_of_def
2935 by (simp add : word_sbin.eq_norm)
2938 "w = number_of bin \<Longrightarrow>
2939 (w::'a::len0 word) >> n = number_of ((bin_rest ^^ n) (bintrunc (size w) bin))"
2941 apply (rule word_eqI)
2942 apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
2946 "w = number_of bin \<Longrightarrow> w >>> n = number_of ((bin_rest ^^ n)
2947 (sbintrunc (size w - 1) bin))"
2949 apply (rule word_eqI)
2950 apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
2951 apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
2954 lemmas sshiftr_no [simp] =
2955 sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size] for w
2957 lemmas shiftr_no [simp] =
2958 shiftr_no' [where w = "number_of w", OF refl, unfolded word_size] for w
2960 lemma shiftr1_bl_of:
2961 "length bl \<le> len_of TYPE('a) \<Longrightarrow>
2962 shiftr1 (of_bl bl::'a::len0 word) = of_bl (butlast bl)"
2963 by (clarsimp simp: shiftr1_def of_bl_def butlast_rest_bl2bin
2964 word_ubin.eq_norm trunc_bl2bin)
2967 "length bl \<le> len_of TYPE('a) \<Longrightarrow>
2968 (of_bl bl::'a::len0 word) >> n = of_bl (take (length bl - n) bl)"
2969 apply (unfold shiftr_def)
2973 apply (subst shiftr1_bl_of)
2975 apply (simp add: butlast_take)
2979 "(x::'a::len0 word) >> n \<equiv> of_bl (take (len_of TYPE('a) - n) (to_bl x))"
2980 using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
2983 "msb (w::'a::len word) \<longleftrightarrow> (w >> (len_of TYPE('a) - 1)) \<noteq> 0"
2984 apply (unfold shiftr_bl word_msb_alt)
2985 apply (simp add: word_size Suc_le_eq take_Suc)
2986 apply (cases "hd (to_bl w)")
2987 apply (auto simp: word_1_bl
2988 of_bl_rep_False [where n=1 and bs="[]", simplified])
2991 lemma align_lem_or [rule_format] :
2992 "ALL x m. length x = n + m --> length y = n + m -->
2993 drop m x = replicate n False --> take m y = replicate m False -->
2994 map2 op | x y = take m x @ drop m y"
2995 apply (induct_tac y)
2998 apply (case_tac x, force)
2999 apply (case_tac m, auto)
3002 apply (induct_tac list, auto)
3005 lemma align_lem_and [rule_format] :
3006 "ALL x m. length x = n + m --> length y = n + m -->
3007 drop m x = replicate n False --> take m y = replicate m False -->
3008 map2 op & x y = replicate (n + m) False"
3009 apply (induct_tac y)
3012 apply (case_tac x, force)
3013 apply (case_tac m, auto)
3016 apply (induct_tac list, auto)
3019 lemma aligned_bl_add_size [OF refl]:
3020 "size x - n = m \<Longrightarrow> n <= size x \<Longrightarrow> drop m (to_bl x) = replicate n False \<Longrightarrow>
3021 take m (to_bl y) = replicate m False \<Longrightarrow>
3022 to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
3023 apply (subgoal_tac "x AND y = 0")
3025 apply (rule word_bl.Rep_eqD)
3026 apply (simp add: bl_word_and)
3027 apply (rule align_lem_and [THEN trans])
3028 apply (simp_all add: word_size)[5]
3030 apply (subst word_plus_and_or [symmetric])
3031 apply (simp add : bl_word_or)
3032 apply (rule align_lem_or)
3033 apply (simp_all add: word_size)
3036 subsubsection "Mask"
3038 lemma nth_mask [OF refl, simp]:
3039 "m = mask n \<Longrightarrow> test_bit m i = (i < n & i < size m)"
3040 apply (unfold mask_def test_bit_bl)
3041 apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
3042 apply (clarsimp simp add: word_size)
3043 apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
3044 apply (fold of_bl_no)
3045 apply (simp add: word_1_bl)
3046 apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
3050 lemma mask_bl: "mask n = of_bl (replicate n True)"
3051 by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
3053 lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
3054 by (auto simp add: nth_bintr word_size intro: word_eqI)
3056 lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
3057 apply (rule word_eqI)
3058 apply (simp add: nth_bintr word_size word_ops_nth_size)
3059 apply (auto simp add: test_bit_bin)
3062 lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)"
3063 by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
3065 lemma and_mask_wi: "word_of_int i AND mask n = word_of_int (bintrunc n i)"
3066 by (fact and_mask_no [unfolded word_number_of_def])
3069 "to_bl (w AND mask n :: 'a :: len word) =
3070 replicate (len_of TYPE('a) - n) False @
3071 drop (len_of TYPE('a) - n) (to_bl w)"
3072 apply (rule nth_equalityI)
3074 apply (clarsimp simp add: to_bl_nth word_size)
3075 apply (simp add: word_size word_ops_nth_size)
3076 apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
3079 lemma and_mask_mod_2p: "w AND mask n = word_of_int (uint w mod 2 ^ n)"
3080 by (fact and_mask_bintr [unfolded word_number_of_alt no_bintr_alt])
3082 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
3083 apply (simp add : and_mask_bintr no_bintr_alt)
3086 apply (rule pos_mod_bound)
3090 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
3091 by (simp add: int_mod_lem eq_sym_conv)
3093 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
3094 apply (simp add: and_mask_bintr word_number_of_def)
3095 apply (simp add: word_ubin.inverse_norm)
3096 apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
3097 apply (fast intro!: lt2p_lem)
3100 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
3101 apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
3102 apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs
3104 apply (subst word_uint.norm_Rep [symmetric])
3105 apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
3109 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
3110 apply (unfold unat_def)
3111 apply (rule trans [OF _ and_mask_dvd])
3112 apply (unfold dvd_def)
3114 apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
3115 apply (simp add : int_mult int_power)
3116 apply (simp add : nat_mult_distrib nat_power_eq)
3120 "n < size w \<Longrightarrow> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
3121 apply (unfold word_size word_less_alt word_number_of_alt)
3122 apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
3124 simp del: word_of_int_bin)
3127 lemma less_mask_eq: "x < 2 ^ n \<Longrightarrow> x AND mask n = (x :: 'a :: len word)"
3128 apply (unfold word_less_alt word_number_of_alt)
3129 apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
3131 simp del: word_of_int_bin)
3132 apply (drule xtr8 [rotated])
3133 apply (rule int_mod_le)
3134 apply (auto simp add : mod_pos_pos_trivial)
3137 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]
3139 lemmas and_mask_less' = iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size]
3141 lemma and_mask_less_size: "n < size x \<Longrightarrow> x AND mask n < 2^n"
3142 unfolding word_size by (erule and_mask_less')
3144 lemma word_mod_2p_is_mask [OF refl]:
3145 "c = 2 ^ n \<Longrightarrow> c > 0 \<Longrightarrow> x mod c = (x :: 'a :: len word) AND mask n"
3146 by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
3149 "(a AND mask n) + b AND mask n = a + b AND mask n"
3150 "a + (b AND mask n) AND mask n = a + b AND mask n"
3151 "(a AND mask n) - b AND mask n = a - b AND mask n"
3152 "a - (b AND mask n) AND mask n = a - b AND mask n"
3153 "a * (b AND mask n) AND mask n = a * b AND mask n"
3154 "(b AND mask n) * a AND mask n = b * a AND mask n"
3155 "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
3156 "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
3157 "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
3158 "- (a AND mask n) AND mask n = - a AND mask n"
3159 "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
3160 "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
3161 using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
3162 by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
3164 lemma mask_power_eq:
3165 "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
3166 using word_of_int_Ex [where x=x]
3167 by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
3170 subsubsection "Revcast"
3172 lemmas revcast_def' = revcast_def [simplified]
3173 lemmas revcast_def'' = revcast_def' [simplified word_size]
3174 lemmas revcast_no_def [simp] = revcast_def' [where w="number_of w", unfolded word_size] for w
3176 lemma to_bl_revcast:
3177 "to_bl (revcast w :: 'a :: len0 word) =
3178 takefill False (len_of TYPE ('a)) (to_bl w)"
3179 apply (unfold revcast_def' word_size)
3180 apply (rule word_bl.Abs_inverse)
3184 lemma revcast_rev_ucast [OF refl refl refl]:
3185 "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
3186 rc = word_reverse uc"
3187 apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
3188 apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
3189 apply (simp add : word_bl.Abs_inverse word_size)
3192 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
3193 using revcast_rev_ucast [of "word_reverse w"] by simp
3195 lemma ucast_revcast: "ucast w = word_reverse (revcast (word_reverse w))"
3196 by (fact revcast_rev_ucast [THEN word_rev_gal'])
3198 lemma ucast_rev_revcast: "ucast (word_reverse w) = word_reverse (revcast w)"
3199 by (fact revcast_ucast [THEN word_rev_gal'])
3202 -- "linking revcast and cast via shift"
3204 lemmas wsst_TYs = source_size target_size word_size
3206 lemma revcast_down_uu [OF refl]:
3207 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
3208 rc (w :: 'a :: len word) = ucast (w >> n)"
3209 apply (simp add: revcast_def')
3210 apply (rule word_bl.Rep_inverse')
3211 apply (rule trans, rule ucast_down_drop)
3213 apply (rule trans, rule drop_shiftr)
3214 apply (auto simp: takefill_alt wsst_TYs)
3217 lemma revcast_down_us [OF refl]:
3218 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
3219 rc (w :: 'a :: len word) = ucast (w >>> n)"
3220 apply (simp add: revcast_def')
3221 apply (rule word_bl.Rep_inverse')
3222 apply (rule trans, rule ucast_down_drop)
3224 apply (rule trans, rule drop_sshiftr)
3225 apply (auto simp: takefill_alt wsst_TYs)
3228 lemma revcast_down_su [OF refl]:
3229 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
3230 rc (w :: 'a :: len word) = scast (w >> n)"
3231 apply (simp add: revcast_def')
3232 apply (rule word_bl.Rep_inverse')
3233 apply (rule trans, rule scast_down_drop)
3235 apply (rule trans, rule drop_shiftr)
3236 apply (auto simp: takefill_alt wsst_TYs)
3239 lemma revcast_down_ss [OF refl]:
3240 "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow>
3241 rc (w :: 'a :: len word) = scast (w >>> n)"
3242 apply (simp add: revcast_def')
3243 apply (rule word_bl.Rep_inverse')
3244 apply (rule trans, rule scast_down_drop)
3246 apply (rule trans, rule drop_sshiftr)
3247 apply (auto simp: takefill_alt wsst_TYs)
3250 (* FIXME: should this also be [OF refl] ? *)
3251 lemma cast_down_rev:
3252 "uc = ucast \<Longrightarrow> source_size uc = target_size uc + n \<Longrightarrow>
3253 uc w = revcast ((w :: 'a :: len word) << n)"
3254 apply (unfold shiftl_rev)
3256 apply (simp add: revcast_rev_ucast)
3257 apply (rule word_rev_gal')
3258 apply (rule trans [OF _ revcast_rev_ucast])
3259 apply (rule revcast_down_uu [symmetric])
3260 apply (auto simp add: wsst_TYs)
3263 lemma revcast_up [OF refl]:
3264 "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
3265 rc w = (ucast w :: 'a :: len word) << n"
3266 apply (simp add: revcast_def')
3267 apply (rule word_bl.Rep_inverse')
3268 apply (simp add: takefill_alt)
3269 apply (rule bl_shiftl [THEN trans])
3270 apply (subst ucast_up_app)
3271 apply (auto simp add: wsst_TYs)
3274 lemmas rc1 = revcast_up [THEN
3275 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
3276 lemmas rc2 = revcast_down_uu [THEN
3277 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
3280 rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
3282 rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
3285 subsubsection "Slices"
3287 lemma slice1_no_bin [simp]:
3288 "slice1 n (number_of w :: 'b word) = of_bl (takefill False n (bin_to_bl (len_of TYPE('b :: len0)) w))"
3289 by (simp add: slice1_def)
3291 lemma slice_no_bin [simp]:
3292 "slice n (number_of w :: 'b word) = of_bl (takefill False (len_of TYPE('b :: len0) - n)
3293 (bin_to_bl (len_of TYPE('b :: len0)) w))"
3294 by (simp add: slice_def word_size)
3296 lemma slice1_0 [simp] : "slice1 n 0 = 0"
3297 unfolding slice1_def by simp
3299 lemma slice_0 [simp] : "slice n 0 = 0"
3300 unfolding slice_def by auto
3302 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
3303 unfolding slice_def' slice1_def
3304 by (simp add : takefill_alt word_size)
3306 lemmas slice_take = slice_take' [unfolded word_size]
3308 -- "shiftr to a word of the same size is just slice,
3309 slice is just shiftr then ucast"
3310 lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
3312 lemma slice_shiftr: "slice n w = ucast (w >> n)"
3313 apply (unfold slice_take shiftr_bl)
3314 apply (rule ucast_of_bl_up [symmetric])
3315 apply (simp add: word_size)
3319 "(slice n w :: 'a :: len0 word) !! m =
3320 (w !! (m + n) & m < len_of TYPE ('a))"
3321 unfolding slice_shiftr
3322 by (simp add : nth_ucast nth_shiftr)
3324 lemma slice1_down_alt':
3325 "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
3326 to_bl sl = takefill False fs (drop k (to_bl w))"
3327 unfolding slice1_def word_size of_bl_def uint_bl
3328 by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
3330 lemma slice1_up_alt':
3331 "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
3332 to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
3333 apply (unfold slice1_def word_size of_bl_def uint_bl)
3334 apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
3335 takefill_append [symmetric])
3336 apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
3337 (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
3341 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
3342 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
3343 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
3344 lemmas slice1_up_alts =
3345 le_add_diff_inverse [symmetric, THEN su1]
3346 le_add_diff_inverse2 [symmetric, THEN su1]
3348 lemma ucast_slice1: "ucast w = slice1 (size w) w"
3349 unfolding slice1_def ucast_bl
3350 by (simp add : takefill_same' word_size)
3352 lemma ucast_slice: "ucast w = slice 0 w"
3353 unfolding slice_def by (simp add : ucast_slice1)
3355 lemma slice_id: "slice 0 t = t"
3356 by (simp only: ucast_slice [symmetric] ucast_id)
3358 lemma revcast_slice1 [OF refl]:
3359 "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
3360 unfolding slice1_def revcast_def' by (simp add : word_size)
3362 lemma slice1_tf_tf':
3363 "to_bl (slice1 n w :: 'a :: len0 word) =
3364 rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
3365 unfolding slice1_def by (rule word_rev_tf)
3367 lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
3370 "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
3371 slice1 n (word_reverse w :: 'b :: len0 word) =
3372 word_reverse (slice1 k w :: 'a :: len0 word)"
3373 apply (unfold word_reverse_def slice1_tf_tf)
3374 apply (rule word_bl.Rep_inverse')
3375 apply (rule rev_swap [THEN iffD1])
3376 apply (rule trans [symmetric])
3378 apply (simp add: word_bl.Abs_inverse)
3379 apply (simp add: word_bl.Abs_inverse)
3383 "n + k + len_of TYPE('a::len0) = len_of TYPE('b::len0) \<Longrightarrow>
3384 slice n (word_reverse (w::'b word)) = word_reverse (slice k w::'a word)"
3385 apply (unfold slice_def word_size)
3386 apply (rule rev_slice1)
3391 not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
3393 -- {* problem posed by TPHOLs referee:
3394 criterion for overflow of addition of signed integers *}
3397 "(sint (x :: 'a :: len word) + sint y = sint (x + y)) =
3398 ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
3399 apply (unfold word_size)
3400 apply (cases "len_of TYPE('a)", simp)
3401 apply (subst msb_shift [THEN sym_notr])
3402 apply (simp add: word_ops_msb)
3403 apply (simp add: word_msb_sint)
3406 apply (unfold sint_word_ariths)
3407 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
3409 apply (insert sint_range' [where x=x])
3410 apply (insert sint_range' [where x=y])
3412 apply (simp (no_asm), arith)
3413 apply (simp (no_asm), arith)
3416 apply (simp (no_asm), arith)
3417 apply (simp (no_asm), arith)
3418 apply (rule notI [THEN notnotD],
3420 drule sbintrunc_inc sbintrunc_dec,
3425 subsection "Split and cat"
3427 lemmas word_split_bin' = word_split_def
3428 lemmas word_cat_bin' = word_cat_def
3430 lemma word_rsplit_no:
3431 "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) =
3432 map number_of (bin_rsplit (len_of TYPE('a :: len))
3433 (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
3434 apply (unfold word_rsplit_def word_no_wi)
3435 apply (simp add: word_ubin.eq_norm)
3438 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
3439 [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
3442 "wc = word_cat a b \<Longrightarrow> wc !! n = (n < size wc &
3443 (if n < size b then b !! n else a !! (n - size b)))"
3444 apply (unfold word_cat_bin' test_bit_bin)
3445 apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
3446 apply (erule bin_nth_uint_imp)
3449 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
3450 apply (unfold of_bl_def to_bl_def word_cat_bin')
3451 apply (simp add: bl_to_bin_app_cat)
3455 "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
3456 apply (unfold of_bl_def)
3457 apply (simp add: bl_to_bin_app_cat bin_cat_num)
3458 apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
3461 lemma of_bl_False [simp]:
3462 "of_bl (False#xs) = of_bl xs"
3464 (auto simp add: test_bit_of_bl nth_append)
3466 lemma of_bl_True [simp]:
3467 "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
3468 by (subst of_bl_append [where xs="[True]", simplified])
3469 (simp add: word_1_bl)
3472 "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
3473 by (cases x) simp_all
3475 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) \<Longrightarrow>
3476 a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
3477 apply (frule word_ubin.norm_Rep [THEN ssubst])
3478 apply (drule bin_split_trunc1)
3479 apply (drule sym [THEN trans])
3484 lemma word_split_bl':
3485 "std = size c - size b \<Longrightarrow> (word_split c = (a, b)) \<Longrightarrow>
3486 (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
3487 apply (unfold word_split_bin')
3490 apply (clarsimp split: prod.splits)
3491 apply (drule word_ubin.norm_Rep [THEN ssubst])
3492 apply (drule split_bintrunc)
3493 apply (simp add : of_bl_def bl2bin_drop word_size
3494 word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
3495 apply (clarsimp split: prod.splits)
3496 apply (frule split_uint_lem [THEN conjunct1])
3497 apply (unfold word_size)
3498 apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
3500 apply (simp add: word_0_wi_Pls)
3501 apply (simp add : of_bl_def to_bl_def)
3502 apply (subst bin_split_take1 [symmetric])
3506 apply (erule thin_rl)
3507 apply (erule arg_cong [THEN trans])
3508 apply (simp add : word_ubin.norm_eq_iff [symmetric])
3511 lemma word_split_bl: "std = size c - size b \<Longrightarrow>
3512 (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <->
3513 word_split c = (a, b)"
3516 apply (erule (1) word_split_bl')
3517 apply (case_tac "word_split c")
3518 apply (auto simp add : word_size)
3519 apply (frule word_split_bl' [rotated])
3520 apply (auto simp add : word_size)
3523 lemma word_split_bl_eq:
3524 "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
3525 (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
3526 of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
3527 apply (rule word_split_bl [THEN iffD1])
3528 apply (unfold word_size)
3529 apply (rule refl conjI)+
3532 -- "keep quantifiers for use in simplification"
3533 lemma test_bit_split':
3534 "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
3535 a !! m = (m < size a & c !! (m + size b)))"
3536 apply (unfold word_split_bin' test_bit_bin)
3538 apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
3539 apply (drule bin_nth_split)
3541 apply (simp_all add: add_commute)
3542 apply (erule bin_nth_uint_imp)+
3545 lemma test_bit_split:
3546 "word_split c = (a, b) \<Longrightarrow>
3547 (\<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))"
3548 by (simp add: test_bit_split')
3550 lemma test_bit_split_eq: "word_split c = (a, b) <->
3551 ((ALL n::nat. b !! n = (n < size b & c !! n)) &
3552 (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
3553 apply (rule_tac iffI)
3554 apply (rule_tac conjI)
3555 apply (erule test_bit_split [THEN conjunct1])
3556 apply (erule test_bit_split [THEN conjunct2])
3557 apply (case_tac "word_split c")
3558 apply (frule test_bit_split)
3560 apply (fastforce intro ! : word_eqI simp add : word_size)
3563 -- {* this odd result is analogous to @{text "ucast_id"},
3564 result to the length given by the result type *}
3566 lemma word_cat_id: "word_cat a b = b"
3567 unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
3569 -- "limited hom result"
3571 "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
3573 (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
3574 word_of_int (bin_cat w (size b) (uint b))"
3575 apply (unfold word_cat_def word_size)
3576 apply (clarsimp simp add: word_ubin.norm_eq_iff [symmetric]
3577 word_ubin.eq_norm bintr_cat min_max.inf_absorb1)
3580 lemma word_cat_split_alt:
3581 "size w <= size u + size v \<Longrightarrow> word_split w = (u, v) \<Longrightarrow> word_cat u v = w"
3582 apply (rule word_eqI)
3583 apply (drule test_bit_split)
3584 apply (clarsimp simp add : test_bit_cat word_size)
3589 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
3592 subsubsection "Split and slice"
3595 "word_split w = (u, v) \<Longrightarrow> u = slice (size v) w & v = slice 0 w"
3596 apply (drule test_bit_split)
3598 apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
3601 lemma slice_cat1 [OF refl]:
3602 "wc = word_cat a b \<Longrightarrow> size wc >= size a + size b \<Longrightarrow> slice (size b) wc = a"
3604 apply (rule word_eqI)
3605 apply (simp add: nth_slice test_bit_cat word_size)
3608 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
3611 "a = slice n c \<Longrightarrow> b = slice 0 c \<Longrightarrow> n = size b \<Longrightarrow>
3612 size a + size b >= size c \<Longrightarrow> word_cat a b = c"
3614 apply (rule word_eqI)
3615 apply (simp add: nth_slice test_bit_cat word_size)
3620 lemma word_split_cat_alt:
3621 "w = word_cat u v \<Longrightarrow> size u + size v <= size w \<Longrightarrow> word_split w = (u, v)"
3622 apply (case_tac "word_split ?w")
3623 apply (rule trans, assumption)
3624 apply (drule test_bit_split)
3626 apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
3629 lemmas word_cat_bl_no_bin [simp] =
3630 word_cat_bl [where a="number_of a"
3631 and b="number_of b",
3632 unfolded to_bl_no_bin]
3635 lemmas word_split_bl_no_bin [simp] =
3636 word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin] for c
3638 -- {* this odd result arises from the fact that the statement of the
3639 result implies that the decoded words are of the same type,
3640 and therefore of the same length, as the original word *}
3642 lemma word_rsplit_same: "word_rsplit w = [w]"
3643 unfolding word_rsplit_def by (simp add : bin_rsplit_all)
3645 lemma word_rsplit_empty_iff_size:
3646 "(word_rsplit w = []) = (size w = 0)"
3647 unfolding word_rsplit_def bin_rsplit_def word_size
3648 by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
3650 lemma test_bit_rsplit:
3651 "sw = word_rsplit w \<Longrightarrow> m < size (hd sw :: 'a :: len word) \<Longrightarrow>
3652 k < length sw \<Longrightarrow> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
3653 apply (unfold word_rsplit_def word_test_bit_def)
3655 apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
3656 apply (rule nth_map [symmetric])
3658 apply (rule bin_nth_rsplit)
3660 apply (simp add : word_size rev_map)
3663 apply (rule map_ident [THEN fun_cong])
3664 apply (rule refl [THEN map_cong])
3665 apply (simp add : word_ubin.eq_norm)
3666 apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
3669 lemma word_rcat_bl: "word_rcat wl = of_bl (concat (map to_bl wl))"
3670 unfolding word_rcat_def to_bl_def' of_bl_def
3671 by (clarsimp simp add : bin_rcat_bl)
3673 lemma size_rcat_lem':
3674 "size (concat (map to_bl wl)) = length wl * size (hd wl)"
3675 unfolding word_size by (induct wl) auto
3677 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
3679 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt]
3682 "n < length (wl::'a word list) * len_of TYPE('a::len) \<Longrightarrow>
3683 rev (concat (map to_bl wl)) ! n =
3684 rev (to_bl (rev wl ! (n div len_of TYPE('a)))) ! (n mod len_of TYPE('a))"
3687 apply (clarsimp simp add : nth_append size_rcat_lem)
3688 apply (simp (no_asm_use) only: mult_Suc [symmetric]
3689 td_gal_lt_len less_Suc_eq_le mod_div_equality')
3693 lemma test_bit_rcat:
3694 "sw = size (hd wl :: 'a :: len word) \<Longrightarrow> rc = word_rcat wl \<Longrightarrow> rc !! n =
3695 (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
3696 apply (unfold word_rcat_bl word_size)
3697 apply (clarsimp simp add :
3698 test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
3700 apply (auto simp add :
3701 test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
3704 lemma foldl_eq_foldr:
3705 "foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
3706 by (induct xs arbitrary: x) (auto simp add : add_assoc)
3708 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
3710 lemmas test_bit_rsplit_alt =
3711 trans [OF nth_rev_alt [THEN test_bit_cong]
3712 test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
3714 -- "lazy way of expressing that u and v, and su and sv, have same types"
3715 lemma word_rsplit_len_indep [OF refl refl refl refl]:
3716 "[u,v] = p \<Longrightarrow> [su,sv] = q \<Longrightarrow> word_rsplit u = su \<Longrightarrow>
3717 word_rsplit v = sv \<Longrightarrow> length su = length sv"
3718 apply (unfold word_rsplit_def)
3719 apply (auto simp add : bin_rsplit_len_indep)
3722 lemma length_word_rsplit_size:
3723 "n = len_of TYPE ('a :: len) \<Longrightarrow>
3724 (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
3725 apply (unfold word_rsplit_def word_size)
3726 apply (clarsimp simp add : bin_rsplit_len_le)
3729 lemmas length_word_rsplit_lt_size =
3730 length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
3732 lemma length_word_rsplit_exp_size:
3733 "n = len_of TYPE ('a :: len) \<Longrightarrow>
3734 length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
3735 unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
3737 lemma length_word_rsplit_even_size:
3738 "n = len_of TYPE ('a :: len) \<Longrightarrow> size w = m * n \<Longrightarrow>
3739 length (word_rsplit w :: 'a word list) = m"
3740 by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
3742 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
3744 (* alternative proof of word_rcat_rsplit *)
3745 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
3746 lemmas dtle = xtr4 [OF tdle mult_commute]
3748 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
3749 apply (rule word_eqI)
3750 apply (clarsimp simp add : test_bit_rcat word_size)
3751 apply (subst refl [THEN test_bit_rsplit])
3752 apply (simp_all add: word_size
3753 refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
3755 apply (erule xtr7, rule len_gt_0 [THEN dtle])+
3758 lemma size_word_rsplit_rcat_size:
3759 "\<lbrakk>word_rcat (ws::'a::len word list) = (frcw::'b::len0 word);
3760 size frcw = length ws * len_of TYPE('a)\<rbrakk>
3761 \<Longrightarrow> length (word_rsplit frcw::'a word list) = length ws"
3762 apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
3763 apply (fast intro: given_quot_alt)
3768 shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
3769 and "(k * n + m) mod n = m mod n"
3770 by (auto simp: add_commute)
3772 lemma word_rsplit_rcat_size [OF refl]:
3773 "word_rcat (ws :: 'a :: len word list) = frcw \<Longrightarrow>
3774 size frcw = length ws * len_of TYPE ('a) \<Longrightarrow> word_rsplit frcw = ws"
3775 apply (frule size_word_rsplit_rcat_size, assumption)
3776 apply (clarsimp simp add : word_size)
3777 apply (rule nth_equalityI, assumption)
3779 apply (rule word_eqI)
3781 apply (rule test_bit_rsplit_alt)
3782 apply (clarsimp simp: word_size)+
3784 apply (rule test_bit_rcat [OF refl refl])
3785 apply (simp add: word_size msrevs)
3786 apply (subst nth_rev)
3788 apply (simp add: le0 [THEN [2] xtr7, THEN diff_Suc_less])
3790 apply (simp add: diff_mult_distrib)
3791 apply (rule mpl_lem)
3792 apply (cases "size ws")
3797 subsection "Rotation"
3799 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
3801 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
3803 lemma rotate_eq_mod:
3804 "m mod length xs = n mod length xs \<Longrightarrow> rotate m xs = rotate n xs"
3805 apply (rule box_equals)
3807 apply (rule rotate_conv_mod [symmetric])+
3812 trans [OF rotate0 [THEN fun_cong] id_apply]
3813 rotate_rotate [symmetric]
3819 subsubsection "Rotation of list to right"
3821 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
3822 unfolding rotater1_def by (cases l) auto
3824 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
3825 apply (unfold rotater1_def)
3827 apply (case_tac [2] "list")
3831 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
3832 unfolding rotater1_def by (cases l) auto
3834 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
3836 apply (simp add : rotater1_def)
3837 apply (simp add : rotate1_rl')
3840 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
3841 unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
3843 lemma rotater_rev: "rotater n ys = rev (rotate n (rev ys))"
3844 using rotater_rev' [where xs = "rev ys"] by simp
3846 lemma rotater_drop_take:
3848 drop (length xs - n mod length xs) xs @
3849 take (length xs - n mod length xs) xs"
3850 by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
3852 lemma rotater_Suc [simp] :
3853 "rotater (Suc n) xs = rotater1 (rotater n xs)"
3854 unfolding rotater_def by auto
3856 lemma rotate_inv_plus [rule_format] :
3857 "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
3858 rotate k (rotater n xs) = rotate m xs &
3859 rotater n (rotate k xs) = rotate m xs &
3860 rotate n (rotater k xs) = rotater m xs"
3861 unfolding rotater_def rotate_def
3862 by (induct n) (auto intro: funpow_swap1 [THEN trans])
3864 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
3866 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
3868 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1]
3869 lemmas rotate_rl [simp] = rotate_inv_eq [THEN conjunct2, THEN conjunct1]
3871 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
3874 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
3877 lemma length_rotater [simp]:
3878 "length (rotater n xs) = length xs"
3879 by (simp add : rotater_rev)
3881 lemma restrict_to_left:
3883 shows "(x = z) = (y = z)"
3886 lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
3887 simplified rotate_gal [symmetric] rotate_gal' [symmetric]]
3888 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
3889 lemmas rotater_eqs = rrs1 [simplified length_rotater]
3890 lemmas rotater_0 = rotater_eqs (1)
3891 lemmas rotater_add = rotater_eqs (2)
3894 subsubsection "map, map2, commuting with rotate(r)"
3896 lemma last_map: "xs ~= [] \<Longrightarrow> last (map f xs) = f (last xs)"
3900 "xs ~= [] \<Longrightarrow> butlast (map f xs) = map f (butlast xs)"
3903 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
3904 unfolding rotater1_def
3905 by (cases xs) (auto simp add: last_map butlast_map)
3908 "rotater n (map f xs) = map f (rotater n xs)"
3909 unfolding rotater_def
3910 by (induct n) (auto simp add : rotater1_map)
3912 lemma but_last_zip [rule_format] :
3913 "ALL ys. length xs = length ys --> xs ~= [] -->
3914 last (zip xs ys) = (last xs, last ys) &
3915 butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
3918 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
3921 lemma but_last_map2 [rule_format] :
3922 "ALL ys. length xs = length ys --> xs ~= [] -->
3923 last (map2 f xs ys) = f (last xs) (last ys) &
3924 butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
3927 apply (unfold map2_def)
3928 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
3932 "length xs = length ys \<Longrightarrow>
3933 rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
3934 apply (unfold rotater1_def)
3937 apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
3940 lemma rotater1_map2:
3941 "length xs = length ys \<Longrightarrow>
3942 rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
3943 unfolding map2_def by (simp add: rotater1_map rotater1_zip)
3946 box_equals [OF asm_rl length_rotater [symmetric]
3947 length_rotater [symmetric],
3951 "length xs = length ys \<Longrightarrow>
3952 rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
3953 by (induct n) (auto intro!: lrth)
3956 "length xs = length ys \<Longrightarrow>
3957 rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
3958 apply (unfold map2_def)
3960 apply (cases ys, auto simp add : rotate1_def)+
3963 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
3964 length_rotate [symmetric], THEN rotate1_map2]
3967 "length xs = length ys \<Longrightarrow>
3968 rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
3969 by (induct n) (auto intro!: lth)
3972 -- "corresponding equalities for word rotation"
3975 "to_bl (word_rotl n w) = rotate n (to_bl w)"
3976 by (simp add: word_bl.Abs_inverse' word_rotl_def)
3978 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
3980 lemmas word_rotl_eqs =
3981 blrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
3984 "to_bl (word_rotr n w) = rotater n (to_bl w)"
3985 by (simp add: word_bl.Abs_inverse' word_rotr_def)
3987 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
3989 lemmas word_rotr_eqs =
3990 brrs0 [simplified word_bl_Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
3992 declare word_rotr_eqs (1) [simp]
3993 declare word_rotl_eqs (1) [simp]
3997 "word_rotl k (word_rotr k v) = v" and
3999 "word_rotr k (word_rotl k v) = v"
4000 by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
4004 "(word_rotr n v = w) = (word_rotl n w = v)" and
4006 "(w = word_rotr n v) = (v = word_rotl n w)"
4007 by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
4010 lemma word_rotr_rev:
4011 "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
4012 by (simp add: word_bl.Rep_inject [symmetric] to_bl_word_rev
4013 to_bl_rotr to_bl_rotl rotater_rev)
4015 lemma word_roti_0 [simp]: "word_roti 0 w = w"
4016 by (unfold word_rot_defs) auto
4018 lemmas abl_cong = arg_cong [where f = "of_bl"]
4020 lemma word_roti_add:
4021 "word_roti (m + n) w = word_roti m (word_roti n w)"
4023 have rotater_eq_lem:
4024 "\<And>m n xs. m = n \<Longrightarrow> rotater m xs = rotater n xs"
4028 "\<And>m n xs. m = n \<Longrightarrow> rotate m xs = rotate n xs"
4031 note rpts [symmetric] =
4032 rotate_inv_plus [THEN conjunct1]
4033 rotate_inv_plus [THEN conjunct2, THEN conjunct1]
4034 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
4035 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
4037 note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
4038 note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
4041 apply (unfold word_rot_defs)
4042 apply (simp only: split: split_if)
4043 apply (safe intro!: abl_cong)
4044 apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
4046 to_bl_rotr [THEN word_bl.Rep_inverse']
4048 apply (rule rrp rrrp rpts,
4049 simp add: nat_add_distrib [symmetric]
4050 nat_diff_distrib [symmetric])+
4054 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
4055 apply (unfold word_rot_defs)
4056 apply (cut_tac y="size w" in gt_or_eq_0)
4059 apply (safe intro!: abl_cong)
4060 apply (rule rotater_eqs)
4061 apply (simp add: word_size nat_mod_distrib)
4062 apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
4063 apply (rule rotater_eqs)
4064 apply (simp add: word_size nat_mod_distrib)
4065 apply (rule int_eq_0_conv [THEN iffD1])
4066 apply (simp only: zmod_int of_nat_add)
4067 apply (simp add: rdmods)
4070 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
4073 subsubsection "Word rotation commutes with bit-wise operations"
4075 (* using locale to not pollute lemma namespace *)
4079 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
4081 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
4083 lemmas lbl_lbl = trans [OF word_bl_Rep' word_bl_Rep' [symmetric]]
4085 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
4087 lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map for v
4089 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
4091 lemma word_rot_logs:
4092 "word_rotl n (NOT v) = NOT word_rotl n v"
4093 "word_rotr n (NOT v) = NOT word_rotr n v"
4094 "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
4095 "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
4096 "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
4097 "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
4098 "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
4099 "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
4100 by (rule word_bl.Rep_eqD,
4101 rule word_rot_defs' [THEN trans],
4102 simp only: blwl_syms [symmetric],
4103 rule th1s [THEN trans],
4107 lemmas word_rot_logs = word_rotate.word_rot_logs
4109 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
4110 simplified word_bl_Rep']
4112 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
4113 simplified word_bl_Rep']
4115 lemma bl_word_roti_dt':
4116 "n = nat ((- i) mod int (size (w :: 'a :: len word))) \<Longrightarrow>
4117 to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
4118 apply (unfold word_roti_def)
4119 apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
4121 apply (simp add: zmod_zminus1_eq_if)
4123 apply (simp add: nat_mult_distrib)
4124 apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
4125 [THEN conjunct2, THEN order_less_imp_le]]
4127 apply (simp add: nat_mod_distrib)
4130 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
4132 lemmas word_rotl_dt = bl_word_rotl_dt [THEN word_bl.Rep_inverse' [symmetric]]
4133 lemmas word_rotr_dt = bl_word_rotr_dt [THEN word_bl.Rep_inverse' [symmetric]]
4134 lemmas word_roti_dt = bl_word_roti_dt [THEN word_bl.Rep_inverse' [symmetric]]
4136 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
4137 by (simp add : word_rotr_dt word_rotl_dt replicate_add [symmetric])
4139 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
4140 unfolding word_roti_def by auto
4142 lemmas word_rotr_dt_no_bin' [simp] =
4143 word_rotr_dt [where w="number_of w", unfolded to_bl_no_bin] for w
4145 lemmas word_rotl_dt_no_bin' [simp] =
4146 word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin] for w
4148 declare word_roti_def [simp]
4151 subsection {* Miscellaneous *}
4153 lemma word_int_cases:
4154 "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
4155 \<Longrightarrow> P"
4156 by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
4158 lemma word_nat_cases [cases type: word]:
4159 "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
4160 \<Longrightarrow> P"
4161 by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
4164 "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
4165 by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
4167 lemma max_word_max [simp,intro!]:
4169 by (cases n rule: word_int_cases)
4170 (simp add: max_word_def word_le_def int_word_uint int_mod_eq')
4172 lemma word_of_int_2p_len:
4173 "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
4174 by (subst word_uint.Abs_norm [symmetric])
4175 (simp add: word_of_int_hom_syms)
4178 "(2::'a::len word) ^ len_of TYPE('a) = 0"
4180 have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
4181 by (rule word_of_int_2p_len)
4182 thus ?thesis by (simp add: word_of_int_2p)
4185 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
4186 apply (simp add: max_word_eq)
4189 apply (simp add: word_pow_0)
4192 lemma max_word_minus:
4193 "max_word = (-1::'a::len word)"
4195 have "-1 + 1 = (0::'a word)" by simp
4196 thus ?thesis by (rule max_word_wrap [symmetric])
4199 lemma max_word_bl [simp]:
4200 "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
4201 by (subst max_word_minus to_bl_n1)+ simp
4203 lemma max_test_bit [simp]:
4204 "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
4205 by (auto simp add: test_bit_bl word_size)
4207 lemma word_and_max [simp]:
4208 "x AND max_word = x"
4209 by (rule word_eqI) (simp add: word_ops_nth_size word_size)
4211 lemma word_or_max [simp]:
4212 "x OR max_word = max_word"
4213 by (rule word_eqI) (simp add: word_ops_nth_size word_size)
4215 lemma word_ao_dist2:
4216 "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
4217 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
4219 lemma word_oa_dist2:
4220 "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
4221 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
4223 lemma word_and_not [simp]:
4224 "x AND NOT x = (0::'a::len0 word)"
4225 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
4227 lemma word_or_not [simp]:
4228 "x OR NOT x = max_word"
4229 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
4232 "boolean (op AND) (op OR) bitNOT 0 max_word"
4233 apply (rule boolean.intro)
4234 apply (rule word_bw_assocs)
4235 apply (rule word_bw_assocs)
4236 apply (rule word_bw_comms)
4237 apply (rule word_bw_comms)
4238 apply (rule word_ao_dist2)
4239 apply (rule word_oa_dist2)
4240 apply (rule word_and_max)
4241 apply (rule word_log_esimps)
4242 apply (rule word_and_not)
4243 apply (rule word_or_not)
4246 interpretation word_bool_alg:
4247 boolean "op AND" "op OR" bitNOT 0 max_word
4248 by (rule word_boolean)
4250 lemma word_xor_and_or:
4251 "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
4252 by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
4254 interpretation word_bool_alg:
4255 boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
4256 apply (rule boolean_xor.intro)
4257 apply (rule word_boolean)
4258 apply (rule boolean_xor_axioms.intro)
4259 apply (rule word_xor_and_or)
4262 lemma shiftr_x_0 [iff]:
4263 "(x::'a::len0 word) >> 0 = x"
4264 by (simp add: shiftr_bl)
4266 lemma shiftl_x_0 [simp]:
4267 "(x :: 'a :: len word) << 0 = x"
4268 by (simp add: shiftl_t2n)
4270 lemma shiftl_1 [simp]:
4271 "(1::'a::len word) << n = 2^n"
4272 by (simp add: shiftl_t2n)
4274 lemma uint_lt_0 [simp]:
4275 "uint x < 0 = False"
4276 by (simp add: linorder_not_less)
4278 lemma shiftr1_1 [simp]:
4279 "shiftr1 (1::'a::len word) = 0"
4280 unfolding shiftr1_def by simp
4282 lemma shiftr_1[simp]:
4283 "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
4284 by (induct n) (auto simp: shiftr_def)
4286 lemma word_less_1 [simp]:
4287 "((x::'a::len word) < 1) = (x = 0)"
4288 by (simp add: word_less_nat_alt unat_0_iff)
4291 "to_bl (mask n :: 'a::len word) =
4292 replicate (len_of TYPE('a) - n) False @
4293 replicate (min (len_of TYPE('a)) n) True"
4294 by (simp add: mask_bl word_rep_drop min_def)
4296 lemma map_replicate_True:
4297 "n = length xs \<Longrightarrow>
4298 map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
4299 by (induct xs arbitrary: n) auto
4301 lemma map_replicate_False:
4302 "n = length xs \<Longrightarrow> map (\<lambda>(x,y). x & y)
4303 (zip xs (replicate n False)) = replicate n False"
4304 by (induct xs arbitrary: n) auto
4307 fixes w :: "'a::len word"
4309 defines "n' \<equiv> len_of TYPE('a) - n"
4310 shows "to_bl (w AND mask n) = replicate n' False @ drop n' (to_bl w)"
4312 note [simp] = map_replicate_True map_replicate_False
4313 have "to_bl (w AND mask n) =
4314 map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
4315 by (simp add: bl_word_and)
4317 have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
4319 have "map2 op & \<dots> (to_bl (mask n::'a::len word)) =
4320 replicate n' False @ drop n' (to_bl w)"
4321 unfolding to_bl_mask n'_def map2_def
4322 by (subst zip_append) auto
4327 lemma drop_rev_takefill:
4328 "length xs \<le> n \<Longrightarrow>
4329 drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
4330 by (simp add: takefill_alt rev_take)
4332 lemma map_nth_0 [simp]:
4333 "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
4336 lemma uint_plus_if_size:
4338 (if uint x + uint y < 2^size x then
4341 uint x + uint y - 2^size x)"
4342 by (simp add: word_arith_alts int_word_uint mod_add_if_z
4345 lemma unat_plus_if_size:
4346 "unat (x + (y::'a::len word)) =
4347 (if unat x + unat y < 2^size x then
4350 unat x + unat y - 2^size x)"
4351 apply (subst word_arith_nat_defs)
4352 apply (subst unat_of_nat)
4353 apply (simp add: mod_nat_add word_size)
4356 lemma word_neq_0_conv:
4357 fixes w :: "'a :: len word"
4358 shows "(w \<noteq> 0) = (0 < w)"
4360 have "0 \<le> w" by (rule word_zero_le)
4361 thus ?thesis by (auto simp add: word_less_def)
4365 "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
4366 apply (subst word_arith_nat_defs)
4367 apply (subst word_unat.eq_norm)
4368 apply (subst mod_if)
4371 apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
4372 apply (erule order_le_less_trans)
4373 apply (insert unat_lt2p [of "max a b"])
4377 lemma uint_sub_if_size:
4379 (if uint y \<le> uint x then
4382 uint x - uint y + 2^size x)"
4383 by (simp add: word_arith_alts int_word_uint mod_sub_if_z
4387 "b <= a \<Longrightarrow> unat (a - b) = unat a - unat b"
4388 by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
4390 lemmas word_less_sub1_numberof [simp] = word_less_sub1 [of "number_of w"] for w
4391 lemmas word_le_sub1_numberof [simp] = word_le_sub1 [of "number_of w"] for w
4393 lemma word_of_int_minus:
4394 "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
4396 have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
4399 apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
4404 lemmas word_of_int_inj =
4405 word_uint.Abs_inject [unfolded uints_num, simplified]
4407 lemma word_le_less_eq:
4408 "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
4409 by (auto simp add: word_less_def)
4411 lemma mod_plus_cong:
4412 assumes 1: "(b::int) = b'"
4413 and 2: "x mod b' = x' mod b'"
4414 and 3: "y mod b' = y' mod b'"
4415 and 4: "x' + y' = z'"
4416 shows "(x + y) mod b = z' mod b'"
4418 from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
4419 by (simp add: mod_add_eq[symmetric])
4420 also have "\<dots> = (x' + y') mod b'"
4421 by (simp add: mod_add_eq[symmetric])
4422 finally show ?thesis by (simp add: 4)
4425 lemma mod_minus_cong:
4426 assumes 1: "(b::int) = b'"
4427 and 2: "x mod b' = x' mod b'"
4428 and 3: "y mod b' = y' mod b'"
4429 and 4: "x' - y' = z'"
4430 shows "(x - y) mod b = z' mod b'"
4432 apply (subst zmod_zsub_left_eq)
4433 apply (subst zmod_zsub_right_eq)
4434 apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric])
4437 lemma word_induct_less:
4438 "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
4441 apply (erule rev_mp)+
4442 apply (rule_tac x=m in spec)
4443 apply (induct_tac n)
4448 apply (erule_tac x=n in allE)
4450 apply (simp add: unat_arith_simps)
4451 apply (clarsimp simp: unat_of_nat)
4453 apply (erule_tac x="of_nat na" in allE)
4455 apply (simp add: unat_arith_simps)
4456 apply (clarsimp simp: unat_of_nat)
4461 "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
4462 by (erule word_induct_less, simp)
4464 lemma word_induct2 [induct type]:
4465 "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
4466 apply (rule word_induct, simp)
4467 apply (case_tac "1+n = 0", auto)
4470 definition word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a" where
4471 "word_rec forZero forSuc n = nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
4473 lemma word_rec_0: "word_rec z s 0 = z"
4474 by (simp add: word_rec_def)
4477 "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
4478 apply (simp add: word_rec_def unat_word_ariths)
4479 apply (subst nat_mod_eq')
4480 apply (cut_tac x=n in unat_lt2p)
4481 apply (drule Suc_mono)
4482 apply (simp add: less_Suc_eq_le)
4483 apply (simp only: order_less_le, simp)
4484 apply (erule contrapos_pn, simp)
4485 apply (drule arg_cong[where f=of_nat])
4487 apply (subst (asm) word_unat.Rep_inverse[of n])
4492 lemma word_rec_Pred:
4493 "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
4494 apply (rule subst[where t="n" and s="1 + (n - 1)"])
4496 apply (subst word_rec_Suc)
4502 "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
4503 by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
4506 "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
4507 by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
4509 lemma word_rec_twice:
4510 "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
4511 apply (erule rev_mp)
4512 apply (rule_tac x=z in spec)
4513 apply (rule_tac x=f in spec)
4515 apply (simp add: word_rec_0)
4517 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
4519 apply (case_tac "1 + (n - m) = 0")
4520 apply (simp add: word_rec_0)
4521 apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
4522 apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
4524 apply (simp (no_asm_use))
4525 apply (simp add: word_rec_Suc word_rec_in2)
4528 apply (drule_tac x="x \<circ> op + 1" in spec)
4529 apply (drule_tac x="x 0 xa" in spec)
4531 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
4533 apply (clarsimp simp add: fun_eq_iff)
4534 apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
4540 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
4541 by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
4543 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
4544 apply (erule rev_mp)
4546 apply (auto simp add: word_rec_0 word_rec_Suc)
4547 apply (drule spec, erule mp)
4549 apply (drule_tac x=n in spec, erule impE)
4555 "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
4556 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
4559 apply (rule word_rec_id_eq)
4561 apply (drule spec, rule mp, erule mp)
4562 apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
4566 apply (erule contrapos_pn)
4568 apply (drule arg_cong[where f="\<lambda>x. x - n"])
4573 "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
4577 lemma word_no_1 [simp]: "(Numeral1::'a::len0 word) = 1"
4578 by (fact word_1_no [symmetric, unfolded BIT_simps])
4580 lemma word_no_0 [simp]: "(Numeral0::'a::len0 word) = 0"
4581 by (fact word_0_no [symmetric])
4583 declare bin_to_bl_def [simp]
4586 use "~~/src/HOL/Word/Tools/smt_word.ML"
4588 setup {* SMT_Word.setup *}
4590 text {* Legacy simp rules *}
4591 declare BIT_simps [simp]