3 Author: Jeremy Dawson and Gerwin Klein, NICTA
5 contains theorems to do with shifting, rotating, splitting words
8 header {* Shifting, Rotating, and Splitting Words *}
14 subsection "Bit shifting"
16 lemma shiftl1_number [simp] :
17 "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
18 apply (unfold shiftl1_def word_number_of_def)
19 apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
21 apply (subst refl [THEN bintrunc_BIT_I, symmetric])
22 apply (subst bintrunc_bintrunc_min)
26 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
27 unfolding word_0_no shiftl1_number by auto
29 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
31 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
32 by (rule trans [OF _ shiftl1_number]) simp
34 lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
36 by simp (simp add: word_0_wi)
38 lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
39 apply (unfold sshiftr1_def)
41 apply (simp add : word_0_wi)
44 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
45 unfolding sshiftr1_def by auto
47 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
48 unfolding shiftl_def by (induct n) auto
50 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
51 unfolding shiftr_def by (induct n) auto
53 lemma sshiftr_0 [simp] : "0 >>> n = 0"
54 unfolding sshiftr_def by (induct n) auto
56 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
57 unfolding sshiftr_def by (induct n) auto
59 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
60 apply (unfold shiftl1_def word_test_bit_def)
61 apply (simp add: nth_bintr word_ubin.eq_norm word_size)
66 lemma nth_shiftl' [rule_format]:
67 "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
68 apply (unfold shiftl_def)
70 apply (force elim!: test_bit_size)
71 apply (clarsimp simp add : nth_shiftl1 word_size)
75 lemmas nth_shiftl = nth_shiftl' [unfolded word_size]
77 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
78 apply (unfold shiftr1_def word_test_bit_def)
79 apply (simp add: nth_bintr word_ubin.eq_norm)
81 apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
86 "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
87 apply (unfold shiftr_def)
89 apply (auto simp add : nth_shiftr1)
92 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
93 where f (ie bin_rest) takes normal arguments to normal results,
94 thus we get (2) from (1) *)
96 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)"
97 apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
98 apply (subst bintr_uint [symmetric, OF order_refl])
99 apply (simp only : bintrunc_bintrunc_l)
104 "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
105 apply (unfold sshiftr1_def word_test_bit_def)
106 apply (simp add: nth_bintr word_ubin.eq_norm
107 bin_nth.Suc [symmetric] word_size
109 apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
110 apply (auto simp add: bin_nth_sint)
113 lemma nth_sshiftr [rule_format] :
114 "ALL n. sshiftr w m !! n = (n < size w &
115 (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
116 apply (unfold sshiftr_def)
117 apply (induct_tac "m")
118 apply (simp add: test_bit_bl)
119 apply (clarsimp simp add: nth_sshiftr1 word_size)
123 apply (erule thin_rl)
128 apply (erule thin_rl)
136 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
137 apply (unfold shiftr1_def bin_rest_div)
138 apply (rule word_uint.Abs_inverse)
139 apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
142 apply (rule zdiv_le_dividend)
146 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
147 apply (unfold sshiftr1_def bin_rest_div [symmetric])
148 apply (simp add: word_sbin.eq_norm)
151 apply (subst word_sbin.norm_Rep [symmetric])
153 apply (subst word_sbin.norm_Rep [symmetric])
154 apply (unfold One_nat_def)
155 apply (rule sbintrunc_rest)
158 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
159 apply (unfold shiftr_def)
162 apply (simp add: shiftr1_div_2 mult_commute
163 zdiv_zmult2_eq [symmetric])
166 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
167 apply (unfold sshiftr_def)
170 apply (simp add: sshiftr1_div_2 mult_commute
171 zdiv_zmult2_eq [symmetric])
174 subsubsection "shift functions in terms of lists of bools"
176 lemmas bshiftr1_no_bin [simp] =
177 bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
179 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
180 unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
182 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
183 unfolding uint_bl of_bl_no
184 by (simp add: bl_to_bin_aux_append bl_to_bin_def)
186 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
188 have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
189 also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
190 finally show ?thesis .
194 "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
195 apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
196 apply (fast intro!: Suc_leI)
199 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
200 apply (unfold shiftr1_def uint_bl of_bl_def)
201 apply (simp add: butlast_rest_bin word_size)
202 apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
206 "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
208 by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
211 (* relate the two above : TODO - remove the :: len restriction on
212 this theorem and others depending on it *)
214 "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
215 apply (unfold word_reverse_def)
216 apply (rule word_bl.Rep_inverse' [symmetric])
217 apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
218 apply (cases "to_bl w")
223 "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
224 apply (unfold shiftl_def shiftr_def)
226 apply (auto simp add : shiftl1_rev)
230 shiftl_rev [where w = "word_reverse w", simplified, standard]
232 lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
233 lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
236 "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
237 apply (unfold sshiftr1_def uint_bl word_size)
238 apply (simp add: butlast_rest_bin word_ubin.eq_norm)
239 apply (simp add: sint_uint)
240 apply (rule nth_equalityI)
244 apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
245 nth_bin_to_bl bin_nth.Suc [symmetric]
250 apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
255 "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)"
256 apply (unfold shiftr_def)
259 apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
260 apply (rule butlast_take [THEN trans])
261 apply (auto simp: word_size)
265 "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
266 apply (unfold sshiftr_def)
269 apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
270 apply (rule butlast_take [THEN trans])
271 apply (auto simp: word_size)
274 lemma take_shiftr [rule_format] :
275 "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) =
277 apply (unfold shiftr_def)
280 apply (simp add: bl_shiftr1)
282 apply (rule take_butlast [THEN trans])
283 apply (auto simp: word_size)
286 lemma take_sshiftr' [rule_format] :
287 "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) &
288 take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))"
289 apply (unfold sshiftr_def)
292 apply (simp add: bl_sshiftr1)
294 apply (rule take_butlast [THEN trans])
295 apply (auto simp: word_size)
298 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
299 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
301 lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
302 by (auto intro: append_take_drop_id [symmetric])
304 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
305 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
307 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
309 by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
312 "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
314 have "w << n = of_bl (to_bl w) << n" by simp
315 also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
316 finally show ?thesis .
319 lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]
322 "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
323 by (simp add: shiftl_bl word_rep_drop word_size min_def)
325 lemma shiftl_zero_size:
326 fixes x :: "'a::len0 word"
327 shows "size x <= n ==> x << n = 0"
328 apply (unfold word_size)
329 apply (rule word_eqI)
330 apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
333 (* note - the following results use 'a :: len word < number_ring *)
335 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
336 apply (simp add: shiftl1_def_u)
337 apply (simp only: double_number_of_Bit0 [symmetric])
341 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
342 apply (simp add: shiftl1_def_u)
343 apply (simp only: double_number_of_Bit0 [symmetric])
347 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
349 by (induct n) (auto simp: shiftl1_2t power_Suc)
351 lemma shiftr1_bintr [simp]:
352 "(shiftr1 (number_of w) :: 'a :: len0 word) =
353 number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))"
354 unfolding shiftr1_def word_number_of_def
355 by (simp add : word_ubin.eq_norm)
357 lemma sshiftr1_sbintr [simp] :
358 "(sshiftr1 (number_of w) :: 'a :: len word) =
359 number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))"
360 unfolding sshiftr1_def word_number_of_def
361 by (simp add : word_sbin.eq_norm)
364 "w = number_of bin ==>
365 (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
367 apply (rule word_eqI)
368 apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
372 "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n)
373 (sbintrunc (size w - 1) bin))"
375 apply (rule word_eqI)
376 apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
377 apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
380 lemmas sshiftr_no [simp] =
381 sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
383 lemmas shiftr_no [simp] =
384 shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
386 lemma shiftr1_bl_of':
387 "us = shiftr1 (of_bl bl) ==> length bl <= size us ==>
388 us = of_bl (butlast bl)"
389 by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin
390 word_ubin.eq_norm trunc_bl2bin)
392 lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
394 lemma shiftr_bl_of' [rule_format]:
395 "us = of_bl bl >> n ==> length bl <= size us -->
396 us = of_bl (take (length bl - n) bl)"
397 apply (unfold shiftr_def)
399 apply (unfold word_size)
403 apply (subst shiftr1_bl_of)
405 apply (simp add: butlast_take)
408 lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
410 lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
411 simplified word_size, simplified, THEN eq_reflection, standard]
413 lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
414 apply (unfold shiftr_bl word_msb_alt)
415 apply (simp add: word_size Suc_le_eq take_Suc)
416 apply (cases "hd (to_bl w)")
417 apply (auto simp: word_1_bl word_0_bl
418 of_bl_rep_False [where n=1 and bs="[]", simplified])
421 lemmas msb_shift = msb_shift' [unfolded word_size]
423 lemma align_lem_or [rule_format] :
424 "ALL x m. length x = n + m --> length y = n + m -->
425 drop m x = replicate n False --> take m y = replicate m False -->
426 map2 op | x y = take m x @ drop m y"
430 apply (case_tac x, force)
431 apply (case_tac m, auto)
434 apply (induct_tac list, auto)
437 lemma align_lem_and [rule_format] :
438 "ALL x m. length x = n + m --> length y = n + m -->
439 drop m x = replicate n False --> take m y = replicate m False -->
440 map2 op & x y = replicate (n + m) False"
444 apply (case_tac x, force)
445 apply (case_tac m, auto)
448 apply (induct_tac list, auto)
451 lemma aligned_bl_add_size':
452 "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
453 take m (to_bl y) = replicate m False ==>
454 to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
455 apply (subgoal_tac "x AND y = 0")
457 apply (rule word_bl.Rep_eqD)
458 apply (simp add: bl_word_and to_bl_0)
459 apply (rule align_lem_and [THEN trans])
460 apply (simp_all add: word_size)[5]
461 apply (rule_tac f = "%n. replicate n False" in arg_cong)
463 apply (subst word_plus_and_or [symmetric])
464 apply (simp add : bl_word_or)
465 apply (rule align_lem_or)
466 apply (simp_all add: word_size)
469 lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
473 lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
474 apply (unfold mask_def test_bit_bl)
475 apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
476 apply (clarsimp simp add: word_size)
477 apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
478 apply (fold of_bl_no)
479 apply (simp add: word_1_bl)
480 apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
484 lemmas nth_mask [simp] = refl [THEN nth_mask']
486 lemma mask_bl: "mask n = of_bl (replicate n True)"
487 by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
489 lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
490 by (auto simp add: nth_bintr word_size intro: word_eqI)
492 lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
493 apply (rule word_eqI)
494 apply (simp add: nth_bintr word_size word_ops_nth_size)
495 apply (auto simp add: test_bit_bin)
498 lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)"
499 by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
501 lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def]
504 "to_bl (w AND mask n :: 'a :: len word) =
505 replicate (len_of TYPE('a) - n) False @
506 drop (len_of TYPE('a) - n) (to_bl w)"
507 apply (rule nth_equalityI)
509 apply (clarsimp simp add: to_bl_nth word_size)
510 apply (simp add: word_size word_ops_nth_size)
511 apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
514 lemmas and_mask_mod_2p =
515 and_mask_bintr [unfolded word_number_of_alt no_bintr_alt]
517 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
518 apply (simp add : and_mask_bintr no_bintr_alt)
521 apply (rule pos_mod_bound)
525 lemmas eq_mod_iff = trans [symmetric, OF int_mod_lem eq_sym_conv]
527 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
528 apply (simp add: and_mask_bintr word_number_of_def)
529 apply (simp add: word_ubin.inverse_norm)
530 apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
531 apply (fast intro!: lt2p_lem)
534 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
535 apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
536 apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
537 apply (subst word_uint.norm_Rep [symmetric])
538 apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
542 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
543 apply (unfold unat_def)
544 apply (rule trans [OF _ and_mask_dvd])
545 apply (unfold dvd_def)
547 apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
548 apply (simp add : int_mult int_power)
549 apply (simp add : nat_mult_distrib nat_power_eq)
553 "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
554 apply (unfold word_size word_less_alt word_number_of_alt)
555 apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm
557 simp del: word_of_int_bin)
560 lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
561 apply (unfold word_less_alt word_number_of_alt)
562 apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom
564 simp del: word_of_int_bin)
565 apply (drule xtr8 [rotated])
566 apply (rule int_mod_le)
567 apply (auto simp add : mod_pos_pos_trivial)
570 lemmas mask_eq_iff_w2p =
571 trans [OF mask_eq_iff word_2p_lem [symmetric], standard]
573 lemmas and_mask_less' =
574 iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
576 lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
577 unfolding word_size by (erule and_mask_less')
579 lemma word_mod_2p_is_mask':
580 "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n"
581 by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p)
583 lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask']
586 "(a AND mask n) + b AND mask n = a + b AND mask n"
587 "a + (b AND mask n) AND mask n = a + b AND mask n"
588 "(a AND mask n) - b AND mask n = a - b AND mask n"
589 "a - (b AND mask n) AND mask n = a - b AND mask n"
590 "a * (b AND mask n) AND mask n = a * b AND mask n"
591 "(b AND mask n) * a AND mask n = b * a AND mask n"
592 "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
593 "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
594 "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
595 "- (a AND mask n) AND mask n = - a AND mask n"
596 "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
597 "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
598 using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
599 by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
602 "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
603 using word_of_int_Ex [where x=x]
604 by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
607 subsubsection "Revcast"
609 lemmas revcast_def' = revcast_def [simplified]
610 lemmas revcast_def'' = revcast_def' [simplified word_size]
611 lemmas revcast_no_def [simp] =
612 revcast_def' [where w="number_of w", unfolded word_size, standard]
615 "to_bl (revcast w :: 'a :: len0 word) =
616 takefill False (len_of TYPE ('a)) (to_bl w)"
617 apply (unfold revcast_def' word_size)
618 apply (rule word_bl.Abs_inverse)
622 lemma revcast_rev_ucast':
623 "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==>
624 rc = word_reverse uc"
625 apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
626 apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
627 apply (simp add : word_bl.Abs_inverse word_size)
630 lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
632 lemmas revcast_ucast = revcast_rev_ucast
633 [where w = "word_reverse w", simplified word_rev_rev, standard]
635 lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
636 lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
639 -- "linking revcast and cast via shift"
641 lemmas wsst_TYs = source_size target_size word_size
643 lemma revcast_down_uu':
644 "rc = revcast ==> source_size rc = target_size rc + n ==>
645 rc (w :: 'a :: len word) = ucast (w >> n)"
646 apply (simp add: revcast_def')
647 apply (rule word_bl.Rep_inverse')
648 apply (rule trans, rule ucast_down_drop)
650 apply (rule trans, rule drop_shiftr)
651 apply (auto simp: takefill_alt wsst_TYs)
654 lemma revcast_down_us':
655 "rc = revcast ==> source_size rc = target_size rc + n ==>
656 rc (w :: 'a :: len word) = ucast (w >>> n)"
657 apply (simp add: revcast_def')
658 apply (rule word_bl.Rep_inverse')
659 apply (rule trans, rule ucast_down_drop)
661 apply (rule trans, rule drop_sshiftr)
662 apply (auto simp: takefill_alt wsst_TYs)
665 lemma revcast_down_su':
666 "rc = revcast ==> source_size rc = target_size rc + n ==>
667 rc (w :: 'a :: len word) = scast (w >> n)"
668 apply (simp add: revcast_def')
669 apply (rule word_bl.Rep_inverse')
670 apply (rule trans, rule scast_down_drop)
672 apply (rule trans, rule drop_shiftr)
673 apply (auto simp: takefill_alt wsst_TYs)
676 lemma revcast_down_ss':
677 "rc = revcast ==> source_size rc = target_size rc + n ==>
678 rc (w :: 'a :: len word) = scast (w >>> n)"
679 apply (simp add: revcast_def')
680 apply (rule word_bl.Rep_inverse')
681 apply (rule trans, rule scast_down_drop)
683 apply (rule trans, rule drop_sshiftr)
684 apply (auto simp: takefill_alt wsst_TYs)
687 lemmas revcast_down_uu = refl [THEN revcast_down_uu']
688 lemmas revcast_down_us = refl [THEN revcast_down_us']
689 lemmas revcast_down_su = refl [THEN revcast_down_su']
690 lemmas revcast_down_ss = refl [THEN revcast_down_ss']
693 "uc = ucast ==> source_size uc = target_size uc + n ==>
694 uc w = revcast ((w :: 'a :: len word) << n)"
695 apply (unfold shiftl_rev)
697 apply (simp add: revcast_rev_ucast)
698 apply (rule word_rev_gal')
699 apply (rule trans [OF _ revcast_rev_ucast])
700 apply (rule revcast_down_uu [symmetric])
701 apply (auto simp add: wsst_TYs)
705 "rc = revcast ==> source_size rc + n = target_size rc ==>
706 rc w = (ucast w :: 'a :: len word) << n"
707 apply (simp add: revcast_def')
708 apply (rule word_bl.Rep_inverse')
709 apply (simp add: takefill_alt)
710 apply (rule bl_shiftl [THEN trans])
711 apply (subst ucast_up_app)
712 apply (auto simp add: wsst_TYs)
714 apply (simp add: min_def)
717 lemmas revcast_up = refl [THEN revcast_up']
719 lemmas rc1 = revcast_up [THEN
720 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
721 lemmas rc2 = revcast_down_uu [THEN
722 revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
725 rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
727 rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
730 subsubsection "Slices"
732 lemmas slice1_no_bin [simp] =
733 slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
735 lemmas slice_no_bin [simp] =
736 trans [OF slice_def [THEN meta_eq_to_obj_eq]
737 slice1_no_bin [THEN meta_eq_to_obj_eq],
738 unfolded word_size, standard]
740 lemma slice1_0 [simp] : "slice1 n 0 = 0"
741 unfolding slice1_def by (simp add : to_bl_0)
743 lemma slice_0 [simp] : "slice n 0 = 0"
744 unfolding slice_def by auto
746 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
747 unfolding slice_def' slice1_def
748 by (simp add : takefill_alt word_size)
750 lemmas slice_take = slice_take' [unfolded word_size]
752 -- "shiftr to a word of the same size is just slice,
753 slice is just shiftr then ucast"
754 lemmas shiftr_slice = trans
755 [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric], standard]
757 lemma slice_shiftr: "slice n w = ucast (w >> n)"
758 apply (unfold slice_take shiftr_bl)
759 apply (rule ucast_of_bl_up [symmetric])
760 apply (simp add: word_size)
764 "(slice n w :: 'a :: len0 word) !! m =
765 (w !! (m + n) & m < len_of TYPE ('a))"
766 unfolding slice_shiftr
767 by (simp add : nth_ucast nth_shiftr)
769 lemma slice1_down_alt':
770 "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==>
771 to_bl sl = takefill False fs (drop k (to_bl w))"
772 unfolding slice1_def word_size of_bl_def uint_bl
773 by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
775 lemma slice1_up_alt':
776 "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==>
777 to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
778 apply (unfold slice1_def word_size of_bl_def uint_bl)
779 apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop
780 takefill_append [symmetric])
781 apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
782 (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
786 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
787 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
788 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
789 lemmas slice1_up_alts =
790 le_add_diff_inverse [symmetric, THEN su1]
791 le_add_diff_inverse2 [symmetric, THEN su1]
793 lemma ucast_slice1: "ucast w = slice1 (size w) w"
794 unfolding slice1_def ucast_bl
795 by (simp add : takefill_same' word_size)
797 lemma ucast_slice: "ucast w = slice 0 w"
798 unfolding slice_def by (simp add : ucast_slice1)
800 lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
802 lemma revcast_slice1':
803 "rc = revcast w ==> slice1 (size rc) w = rc"
804 unfolding slice1_def revcast_def' by (simp add : word_size)
806 lemmas revcast_slice1 = refl [THEN revcast_slice1']
809 "to_bl (slice1 n w :: 'a :: len0 word) =
810 rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
811 unfolding slice1_def by (rule word_rev_tf)
813 lemmas slice1_tf_tf = slice1_tf_tf'
814 [THEN word_bl.Rep_inverse', symmetric, standard]
817 "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow>
818 slice1 n (word_reverse w :: 'b :: len0 word) =
819 word_reverse (slice1 k w :: 'a :: len0 word)"
820 apply (unfold word_reverse_def slice1_tf_tf)
821 apply (rule word_bl.Rep_inverse')
822 apply (rule rev_swap [THEN iffD1])
823 apply (rule trans [symmetric])
825 apply (simp add: word_bl.Abs_inverse)
826 apply (simp add: word_bl.Abs_inverse)
830 "res = slice n (word_reverse w) ==> n + k + size res = size w ==>
831 res = word_reverse (slice k w)"
832 apply (unfold slice_def word_size)
834 apply (rule rev_slice1)
838 lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
841 not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
843 -- {* problem posed by TPHOLs referee:
844 criterion for overflow of addition of signed integers *}
847 "(sint (x :: 'a :: len word) + sint y = sint (x + y)) =
848 ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
849 apply (unfold word_size)
850 apply (cases "len_of TYPE('a)", simp)
851 apply (subst msb_shift [THEN sym_notr])
852 apply (simp add: word_ops_msb)
853 apply (simp add: word_msb_sint)
856 apply (unfold sint_word_ariths)
857 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
859 apply (insert sint_range' [where x=x])
860 apply (insert sint_range' [where x=y])
862 apply (simp (no_asm), arith)
863 apply (simp (no_asm), arith)
866 apply (simp (no_asm), arith)
867 apply (simp (no_asm), arith)
868 apply (rule notI [THEN notnotD],
870 drule sbintrunc_inc sbintrunc_dec,
875 subsection "Split and cat"
877 lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
878 lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
880 lemma word_rsplit_no:
881 "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) =
882 map number_of (bin_rsplit (len_of TYPE('a :: len))
883 (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
884 apply (unfold word_rsplit_def word_no_wi)
885 apply (simp add: word_ubin.eq_norm)
888 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
889 [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
892 "wc = word_cat a b ==> wc !! n = (n < size wc &
893 (if n < size b then b !! n else a !! (n - size b)))"
894 apply (unfold word_cat_bin' test_bit_bin)
895 apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
896 apply (erule bin_nth_uint_imp)
899 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
900 apply (unfold of_bl_def to_bl_def word_cat_bin')
901 apply (simp add: bl_to_bin_app_cat)
905 "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
906 apply (unfold of_bl_def)
907 apply (simp add: bl_to_bin_app_cat bin_cat_num)
908 apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
911 lemma of_bl_False [simp]:
912 "of_bl (False#xs) = of_bl xs"
914 (auto simp add: test_bit_of_bl nth_append)
917 "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
918 by (subst of_bl_append [where xs="[True]", simplified])
919 (simp add: word_1_bl)
922 "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
923 by (cases x) (simp_all add: of_bl_True)
925 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==>
926 a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
927 apply (frule word_ubin.norm_Rep [THEN ssubst])
928 apply (drule bin_split_trunc1)
929 apply (drule sym [THEN trans])
934 lemma word_split_bl':
935 "std = size c - size b ==> (word_split c = (a, b)) ==>
936 (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
937 apply (unfold word_split_bin')
940 apply (clarsimp split: prod.splits)
941 apply (drule word_ubin.norm_Rep [THEN ssubst])
942 apply (drule split_bintrunc)
943 apply (simp add : of_bl_def bl2bin_drop word_size
944 word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)
945 apply (clarsimp split: prod.splits)
946 apply (frule split_uint_lem [THEN conjunct1])
947 apply (unfold word_size)
948 apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
950 apply (simp add: word_0_bl word_0_wi_Pls)
951 apply (simp add : of_bl_def to_bl_def)
952 apply (subst bin_split_take1 [symmetric])
956 apply (erule thin_rl)
957 apply (erule arg_cong [THEN trans])
958 apply (simp add : word_ubin.norm_eq_iff [symmetric])
961 lemma word_split_bl: "std = size c - size b ==>
962 (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <->
963 word_split c = (a, b)"
966 apply (erule (1) word_split_bl')
967 apply (case_tac "word_split c")
968 apply (auto simp add : word_size)
969 apply (frule word_split_bl' [rotated])
970 apply (auto simp add : word_size)
973 lemma word_split_bl_eq:
974 "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
975 (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
976 of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
977 apply (rule word_split_bl [THEN iffD1])
978 apply (unfold word_size)
979 apply (rule refl conjI)+
982 -- "keep quantifiers for use in simplification"
983 lemma test_bit_split':
984 "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) &
985 a !! m = (m < size a & c !! (m + size b)))"
986 apply (unfold word_split_bin' test_bit_bin)
988 apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
989 apply (drule bin_nth_split)
991 apply (simp_all add: add_commute)
992 apply (erule bin_nth_uint_imp)+
995 lemmas test_bit_split =
996 test_bit_split' [THEN mp, simplified all_simps, standard]
998 lemma test_bit_split_eq: "word_split c = (a, b) <->
999 ((ALL n::nat. b !! n = (n < size b & c !! n)) &
1000 (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
1001 apply (rule_tac iffI)
1002 apply (rule_tac conjI)
1003 apply (erule test_bit_split [THEN conjunct1])
1004 apply (erule test_bit_split [THEN conjunct2])
1005 apply (case_tac "word_split c")
1006 apply (frule test_bit_split)
1008 apply (fastsimp intro ! : word_eqI simp add : word_size)
1011 -- {* this odd result is analogous to @{text "ucast_id"},
1012 result to the length given by the result type *}
1014 lemma word_cat_id: "word_cat a b = b"
1015 unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
1017 -- "limited hom result"
1019 "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
1021 (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
1022 word_of_int (bin_cat w (size b) (uint b))"
1023 apply (unfold word_cat_def word_size)
1024 apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
1025 word_ubin.eq_norm bintr_cat min_def)
1029 lemma word_cat_split_alt:
1030 "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
1031 apply (rule word_eqI)
1032 apply (drule test_bit_split)
1033 apply (clarsimp simp add : test_bit_cat word_size)
1038 lemmas word_cat_split_size =
1039 sym [THEN [2] word_cat_split_alt [symmetric], standard]
1042 subsubsection "Split and slice"
1045 "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
1046 apply (drule test_bit_split)
1048 apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
1052 "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
1054 apply (rule word_eqI)
1055 apply (simp add: nth_slice test_bit_cat word_size)
1058 lemmas slice_cat1 = refl [THEN slice_cat1']
1059 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
1062 "a = slice n c ==> b = slice 0 c ==> n = size b ==>
1063 size a + size b >= size c ==> word_cat a b = c"
1065 apply (rule word_eqI)
1066 apply (simp add: nth_slice test_bit_cat word_size)
1071 lemma word_split_cat_alt:
1072 "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
1073 apply (case_tac "word_split ?w")
1074 apply (rule trans, assumption)
1075 apply (drule test_bit_split)
1077 apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
1080 lemmas word_cat_bl_no_bin [simp] =
1081 word_cat_bl [where a="number_of a"
1082 and b="number_of b",
1083 unfolded to_bl_no_bin, standard]
1085 lemmas word_split_bl_no_bin [simp] =
1086 word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin, standard]
1088 -- {* this odd result arises from the fact that the statement of the
1089 result implies that the decoded words are of the same type,
1090 and therefore of the same length, as the original word *}
1092 lemma word_rsplit_same: "word_rsplit w = [w]"
1093 unfolding word_rsplit_def by (simp add : bin_rsplit_all)
1095 lemma word_rsplit_empty_iff_size:
1096 "(word_rsplit w = []) = (size w = 0)"
1097 unfolding word_rsplit_def bin_rsplit_def word_size
1098 by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
1100 lemma test_bit_rsplit:
1101 "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==>
1102 k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
1103 apply (unfold word_rsplit_def word_test_bit_def)
1105 apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
1106 apply (rule nth_map [symmetric])
1108 apply (rule bin_nth_rsplit)
1110 apply (simp add : word_size rev_map map_compose [symmetric])
1113 apply (rule map_ident [THEN fun_cong])
1114 apply (rule refl [THEN map_cong])
1115 apply (simp add : word_ubin.eq_norm)
1116 apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
1119 lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
1120 unfolding word_rcat_def to_bl_def' of_bl_def
1121 by (clarsimp simp add : bin_rcat_bl map_compose)
1123 lemma size_rcat_lem':
1124 "size (concat (map to_bl wl)) = length wl * size (hd wl)"
1125 unfolding word_size by (induct wl) auto
1127 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
1129 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
1131 lemma nth_rcat_lem' [rule_format] :
1132 "sw = size (hd wl :: 'a :: len word) ==> (ALL n. n < size wl * sw -->
1133 rev (concat (map to_bl wl)) ! n =
1134 rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
1135 apply (unfold word_size)
1138 apply (clarsimp simp add : nth_append size_rcat_lem)
1139 apply (simp (no_asm_use) only: mult_Suc [symmetric]
1140 td_gal_lt_len less_Suc_eq_le mod_div_equality')
1144 lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
1146 lemma test_bit_rcat:
1147 "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n =
1148 (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
1149 apply (unfold word_rcat_bl word_size)
1150 apply (clarsimp simp add :
1151 test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
1153 apply (auto simp add :
1154 test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
1157 lemma foldl_eq_foldr [rule_format] :
1158 "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)"
1159 by (induct xs) (auto simp add : add_assoc)
1161 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
1163 lemmas test_bit_rsplit_alt =
1164 trans [OF nth_rev_alt [THEN test_bit_cong]
1165 test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
1167 -- "lazy way of expressing that u and v, and su and sv, have same types"
1168 lemma word_rsplit_len_indep':
1169 "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==>
1170 word_rsplit v = sv ==> length su = length sv"
1171 apply (unfold word_rsplit_def)
1172 apply (auto simp add : bin_rsplit_len_indep)
1175 lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
1177 lemma length_word_rsplit_size:
1178 "n = len_of TYPE ('a :: len) ==>
1179 (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
1180 apply (unfold word_rsplit_def word_size)
1181 apply (clarsimp simp add : bin_rsplit_len_le)
1184 lemmas length_word_rsplit_lt_size =
1185 length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
1187 lemma length_word_rsplit_exp_size:
1188 "n = len_of TYPE ('a :: len) ==>
1189 length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
1190 unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
1192 lemma length_word_rsplit_even_size:
1193 "n = len_of TYPE ('a :: len) ==> size w = m * n ==>
1194 length (word_rsplit w :: 'a word list) = m"
1195 by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
1197 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
1199 (* alternative proof of word_rcat_rsplit *)
1200 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1]
1201 lemmas dtle = xtr4 [OF tdle mult_commute]
1203 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
1204 apply (rule word_eqI)
1205 apply (clarsimp simp add : test_bit_rcat word_size)
1206 apply (subst refl [THEN test_bit_rsplit])
1207 apply (simp_all add: word_size
1208 refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
1210 apply (erule xtr7, rule len_gt_0 [THEN dtle])+
1213 lemma size_word_rsplit_rcat_size':
1214 "word_rcat (ws :: 'a :: len word list) = frcw ==>
1215 size frcw = length ws * len_of TYPE ('a) ==>
1216 size (hd [word_rsplit frcw, ws]) = size ws"
1217 apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
1218 apply (fast intro: given_quot_alt)
1221 lemmas size_word_rsplit_rcat_size =
1222 size_word_rsplit_rcat_size' [simplified]
1226 shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
1227 and "(k * n + m) mod n = m mod n"
1228 by (auto simp: add_commute)
1230 lemma word_rsplit_rcat_size':
1231 "word_rcat (ws :: 'a :: len word list) = frcw ==>
1232 size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws"
1233 apply (frule size_word_rsplit_rcat_size, assumption)
1234 apply (clarsimp simp add : word_size)
1235 apply (rule nth_equalityI, assumption)
1237 apply (rule word_eqI)
1239 apply (rule test_bit_rsplit_alt)
1240 apply (clarsimp simp: word_size)+
1242 apply (rule test_bit_rcat [OF refl refl])
1243 apply (simp add : word_size msrevs)
1244 apply (subst nth_rev)
1246 apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
1248 apply (simp add : diff_mult_distrib)
1249 apply (rule mpl_lem)
1250 apply (cases "size ws")
1254 lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
1257 subsection "Rotation"
1259 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
1261 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
1263 lemma rotate_eq_mod:
1264 "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
1265 apply (rule box_equals)
1267 apply (rule rotate_conv_mod [symmetric])+
1271 lemmas rotate_eqs [standard] =
1272 trans [OF rotate0 [THEN fun_cong] id_apply]
1273 rotate_rotate [symmetric]
1279 subsubsection "Rotation of list to right"
1281 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
1282 unfolding rotater1_def by (cases l) auto
1284 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
1285 apply (unfold rotater1_def)
1287 apply (case_tac [2] "list")
1291 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
1292 unfolding rotater1_def by (cases l) auto
1294 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
1296 apply (simp add : rotater1_def)
1297 apply (simp add : rotate1_rl')
1300 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
1301 unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
1303 lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified, standard]
1305 lemma rotater_drop_take:
1307 drop (length xs - n mod length xs) xs @
1308 take (length xs - n mod length xs) xs"
1309 by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
1311 lemma rotater_Suc [simp] :
1312 "rotater (Suc n) xs = rotater1 (rotater n xs)"
1313 unfolding rotater_def by auto
1315 lemma rotate_inv_plus [rule_format] :
1316 "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs &
1317 rotate k (rotater n xs) = rotate m xs &
1318 rotater n (rotate k xs) = rotate m xs &
1319 rotate n (rotater k xs) = rotater m xs"
1320 unfolding rotater_def rotate_def
1321 by (induct n) (auto intro: funpow_swap1 [THEN trans])
1323 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
1325 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
1327 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1, standard]
1328 lemmas rotate_rl [simp] =
1329 rotate_inv_eq [THEN conjunct2, THEN conjunct1, standard]
1331 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
1334 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
1337 lemma length_rotater [simp]:
1338 "length (rotater n xs) = length xs"
1339 by (simp add : rotater_rev)
1341 lemmas rrs0 = rotate_eqs [THEN restrict_to_left,
1342 simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
1343 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
1344 lemmas rotater_eqs = rrs1 [simplified length_rotater, standard]
1345 lemmas rotater_0 = rotater_eqs (1)
1346 lemmas rotater_add = rotater_eqs (2)
1349 subsubsection "map, map2, commuting with rotate(r)"
1351 lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
1355 "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
1358 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)"
1359 unfolding rotater1_def
1360 by (cases xs) (auto simp add: last_map butlast_map)
1363 "rotater n (map f xs) = map f (rotater n xs)"
1364 unfolding rotater_def
1365 by (induct n) (auto simp add : rotater1_map)
1367 lemma but_last_zip [rule_format] :
1368 "ALL ys. length xs = length ys --> xs ~= [] -->
1369 last (zip xs ys) = (last xs, last ys) &
1370 butlast (zip xs ys) = zip (butlast xs) (butlast ys)"
1373 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
1376 lemma but_last_map2 [rule_format] :
1377 "ALL ys. length xs = length ys --> xs ~= [] -->
1378 last (map2 f xs ys) = f (last xs) (last ys) &
1379 butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)"
1382 apply (unfold map2_def)
1383 apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
1387 "length xs = length ys ==>
1388 rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)"
1389 apply (unfold rotater1_def)
1392 apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
1395 lemma rotater1_map2:
1396 "length xs = length ys ==>
1397 rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)"
1398 unfolding map2_def by (simp add: rotater1_map rotater1_zip)
1401 box_equals [OF asm_rl length_rotater [symmetric]
1402 length_rotater [symmetric],
1406 "length xs = length ys ==>
1407 rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)"
1408 by (induct n) (auto intro!: lrth)
1411 "length xs = length ys ==>
1412 rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)"
1413 apply (unfold map2_def)
1415 apply (cases ys, auto simp add : rotate1_def)+
1418 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric]
1419 length_rotate [symmetric], THEN rotate1_map2]
1422 "length xs = length ys ==>
1423 rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)"
1424 by (induct n) (auto intro!: lth)
1427 -- "corresponding equalities for word rotation"
1430 "to_bl (word_rotl n w) = rotate n (to_bl w)"
1431 by (simp add: word_bl.Abs_inverse' word_rotl_def)
1433 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
1435 lemmas word_rotl_eqs =
1436 blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
1439 "to_bl (word_rotr n w) = rotater n (to_bl w)"
1440 by (simp add: word_bl.Abs_inverse' word_rotr_def)
1442 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
1444 lemmas word_rotr_eqs =
1445 brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
1447 declare word_rotr_eqs (1) [simp]
1448 declare word_rotl_eqs (1) [simp]
1452 "word_rotl k (word_rotr k v) = v" and
1454 "word_rotr k (word_rotl k v) = v"
1455 by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
1459 "(word_rotr n v = w) = (word_rotl n w = v)" and
1461 "(w = word_rotr n v) = (v = word_rotl n w)"
1462 by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric]
1465 lemma word_rotr_rev:
1466 "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
1467 by (simp add: word_bl.Rep_inject [symmetric] to_bl_word_rev
1468 to_bl_rotr to_bl_rotl rotater_rev)
1470 lemma word_roti_0 [simp]: "word_roti 0 w = w"
1471 by (unfold word_rot_defs) auto
1473 lemmas abl_cong = arg_cong [where f = "of_bl"]
1475 lemma word_roti_add:
1476 "word_roti (m + n) w = word_roti m (word_roti n w)"
1478 have rotater_eq_lem:
1479 "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
1483 "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
1486 note rpts [symmetric, standard] =
1487 rotate_inv_plus [THEN conjunct1]
1488 rotate_inv_plus [THEN conjunct2, THEN conjunct1]
1489 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
1490 rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
1492 note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
1493 note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
1496 apply (unfold word_rot_defs)
1497 apply (simp only: split: split_if)
1498 apply (safe intro!: abl_cong)
1499 apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse']
1501 to_bl_rotr [THEN word_bl.Rep_inverse']
1503 apply (rule rrp rrrp rpts,
1504 simp add: nat_add_distrib [symmetric]
1505 nat_diff_distrib [symmetric])+
1509 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
1510 apply (unfold word_rot_defs)
1511 apply (cut_tac y="size w" in gt_or_eq_0)
1514 apply (safe intro!: abl_cong)
1515 apply (rule rotater_eqs)
1516 apply (simp add: word_size nat_mod_distrib)
1517 apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
1518 apply (rule rotater_eqs)
1519 apply (simp add: word_size nat_mod_distrib)
1520 apply (rule int_eq_0_conv [THEN iffD1])
1521 apply (simp only: zmod_int zadd_int [symmetric])
1522 apply (simp add: rdmods)
1525 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
1528 subsubsection "Word rotation commutes with bit-wise operations"
1530 (* using locale to not pollute lemma namespace *)
1536 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
1538 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
1540 lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
1542 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
1544 lemmas ths_map [where xs = "to_bl v", standard] = rotate_map rotater_map
1546 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
1548 lemma word_rot_logs:
1549 "word_rotl n (NOT v) = NOT word_rotl n v"
1550 "word_rotr n (NOT v) = NOT word_rotr n v"
1551 "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
1552 "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
1553 "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
1554 "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
1555 "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
1556 "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
1557 by (rule word_bl.Rep_eqD,
1558 rule word_rot_defs' [THEN trans],
1559 simp only: blwl_syms [symmetric],
1560 rule th1s [THEN trans],
1564 lemmas word_rot_logs = word_rotate.word_rot_logs
1566 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
1567 simplified word_bl.Rep', standard]
1569 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
1570 simplified word_bl.Rep', standard]
1572 lemma bl_word_roti_dt':
1573 "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==>
1574 to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
1575 apply (unfold word_roti_def)
1576 apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
1578 apply (simp add: zmod_zminus1_eq_if)
1580 apply (simp add: nat_mult_distrib)
1581 apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj
1582 [THEN conjunct2, THEN order_less_imp_le]]
1584 apply (simp add: nat_mod_distrib)
1587 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
1589 lemmas word_rotl_dt = bl_word_rotl_dt
1590 [THEN word_bl.Rep_inverse' [symmetric], standard]
1591 lemmas word_rotr_dt = bl_word_rotr_dt
1592 [THEN word_bl.Rep_inverse' [symmetric], standard]
1593 lemmas word_roti_dt = bl_word_roti_dt
1594 [THEN word_bl.Rep_inverse' [symmetric], standard]
1596 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
1597 by (simp add : word_rotr_dt word_rotl_dt to_bl_0 replicate_add [symmetric])
1599 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
1600 unfolding word_roti_def by auto
1602 lemmas word_rotr_dt_no_bin' [simp] =
1603 word_rotr_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
1605 lemmas word_rotl_dt_no_bin' [simp] =
1606 word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
1608 declare word_roti_def [simp]