src/HOL/Word/WordShift.thy

+(* 
+    ID:         $Id$
+    Author:     Jeremy Dawson and Gerwin Klein, NICTA
+
+  contains theorems to do with shifting, rotating, splitting words
+*)
+
+theory WordShift imports WordBitwise begin
+
+section "Bit shifting"
+
+lemma shiftl1_number [simp] :
+  "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
+  apply (unfold shiftl1_def word_number_of_def)
+  apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm)
+  apply (subst refl [THEN bintrunc_BIT_I, symmetric])
+  apply (subst bintrunc_bintrunc_min)
+  apply simp
+  done
+
+lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
+  unfolding word_0_no shiftl1_number by auto
+
+lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
+
+lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
+  by (rule trans [OF _ shiftl1_number]) simp
+
+lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
+  unfolding shiftr1_def 
+  by simp (simp add: word_0_wi)
+
+lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
+  apply (unfold sshiftr1_def)
+  apply simp
+  apply (simp add : word_0_wi)
+  done
+
+lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
+  unfolding sshiftr1_def by auto
+
+lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
+  unfolding shiftl_def by (induct n) auto
+
+lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
+  unfolding shiftr_def by (induct n) auto
+
+lemma sshiftr_0 [simp] : "0 >>> n = 0"
+  unfolding sshiftr_def by (induct n) auto
+
+lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
+  unfolding sshiftr_def by (induct n) auto
+
+lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
+  apply (unfold shiftl1_def word_test_bit_def)
+  apply (simp add: nth_bintr word_ubin.eq_norm word_size)
+  apply (cases n)
+   apply auto
+  done
+
+lemma nth_shiftl' [rule_format]:
+  "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
+  apply (unfold shiftl_def)
+  apply (induct "m")
+   apply (force elim!: test_bit_size)
+  apply (clarsimp simp add : nth_shiftl1 word_size)
+  apply arith
+  done
+
+lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
+
+lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
+  apply (unfold shiftr1_def word_test_bit_def)
+  apply (simp add: nth_bintr word_ubin.eq_norm)
+  apply safe
+  apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
+  apply simp
+  done
+
+lemma nth_shiftr: 
+  "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
+  apply (unfold shiftr_def)
+  apply (induct "m")
+   apply (auto simp add : nth_shiftr1)
+  done
+   
+(* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
+  where f (ie bin_rest) takes normal arguments to normal results,
+  thus we get (2) from (1) *)
+
+lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
+  apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
+  apply (subst bintr_uint [symmetric, OF order_refl])
+  apply (simp only : bintrunc_bintrunc_l)
+  apply simp 
+  done
+
+lemma nth_sshiftr1: 
+  "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
+  apply (unfold sshiftr1_def word_test_bit_def)
+  apply (simp add: nth_bintr word_ubin.eq_norm
+                   bin_nth.Suc [symmetric] word_size 
+             del: bin_nth.simps)
+  apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
+  apply (auto simp add: bin_nth_sint)
+  done
+
+lemma nth_sshiftr [rule_format] : 
+  "ALL n. sshiftr w m !! n = (n < size w & 
+    (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
+  apply (unfold sshiftr_def)
+  apply (induct_tac "m")
+   apply (simp add: test_bit_bl)
+  apply (clarsimp simp add: nth_sshiftr1 word_size)
+  apply safe
+       apply arith
+      apply arith
+     apply (erule thin_rl)
+     apply (case_tac n)
+      apply safe
+      apply simp
+     apply simp
+    apply (erule thin_rl)
+    apply (case_tac n)
+     apply safe
+     apply simp
+    apply simp
+   apply arith+
+  done
+    
+lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
+  apply (unfold shiftr1_def bin_rest_div)
+  apply (rule word_uint.Abs_inverse)
+  apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
+  apply (rule xtr7)
+   prefer 2
+   apply (rule zdiv_le_dividend)
+    apply auto
+  done
+
+lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
+  apply (unfold sshiftr1_def bin_rest_div [symmetric])
+  apply (simp add: word_sbin.eq_norm)
+  apply (rule trans)
+   defer
+   apply (subst word_sbin.norm_Rep [symmetric])
+   apply (rule refl)
+  apply (subst word_sbin.norm_Rep [symmetric])
+  apply (unfold One_nat_def)
+  apply (rule sbintrunc_rest)
+  done
+
+lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
+  apply (unfold shiftr_def)
+  apply (induct "n")
+   apply simp
+  apply (simp add: shiftr1_div_2 mult_commute
+                   zdiv_zmult2_eq [symmetric])
+  done
+
+lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
+  apply (unfold sshiftr_def)
+  apply (induct "n")
+   apply simp
+  apply (simp add: sshiftr1_div_2 mult_commute
+                   zdiv_zmult2_eq [symmetric])
+  done
+
+subsection "shift functions in terms of lists of bools"
+
+lemmas bshiftr1_no_bin [simp] = 
+  bshiftr1_def [where w="number_of ?w", unfolded to_bl_no_bin]
+
+lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
+  unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
+
+lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
+  unfolding uint_bl of_bl_no 
+  by (simp add: bl_to_bin_aux_append bl_to_bin_def)
+
+lemmas shiftl1_bl = shiftl1_of_bl 
+  [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
+
+lemma bl_shiftl1:
+  "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
+  apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
+  apply (fast intro!: Suc_leI)
+  done
+
+lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
+  apply (unfold shiftr1_def uint_bl of_bl_def)
+  apply (simp add: butlast_rest_bin word_size)
+  apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
+  done
+
+lemma bl_shiftr1: 
+  "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
+  unfolding shiftr1_bl
+  by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
+
+
+(* relate the two above : TODO - remove the :: len restriction on
+  this theorem and others depending on it *)
+lemma shiftl1_rev: 
+  "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
+  apply (unfold word_reverse_def)
+  apply (rule word_bl.Rep_inverse' [symmetric])
+  apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
+  apply (cases "to_bl w")
+   apply auto
+  done
+
+lemma shiftl_rev: 
+  "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
+  apply (unfold shiftl_def shiftr_def)
+  apply (induct "n")
+   apply (auto simp add : shiftl1_rev)
+  done
+
+lemmas rev_shiftl =
+  shiftl_rev [where w = "word_reverse ?w1", simplified, standard]
+
+lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
+lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
+
+lemma bl_sshiftr1:
+  "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
+  apply (unfold sshiftr1_def uint_bl word_size)
+  apply (simp add: butlast_rest_bin word_ubin.eq_norm)
+  apply (simp add: sint_uint)
+  apply (rule nth_equalityI)
+   apply clarsimp
+  apply clarsimp
+  apply (case_tac i)
+   apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
+                        nth_bin_to_bl bin_nth.Suc [symmetric] 
+                        nth_sbintr 
+                   del: bin_nth.Suc)
+   apply force
+  apply (rule impI)
+  apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
+  apply simp
+  done
+
+lemma drop_shiftr: 
+  "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
+  apply (unfold shiftr_def)
+  apply (induct n)
+   prefer 2
+   apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
+   apply (rule butlast_take [THEN trans])
+  apply (auto simp: word_size)
+  done
+
+lemma drop_sshiftr: 
+  "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
+  apply (unfold sshiftr_def)
+  apply (induct n)
+   prefer 2
+   apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
+   apply (rule butlast_take [THEN trans])
+  apply (auto simp: word_size)
+  done
+
+lemma take_shiftr [rule_format] :
+  "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = 
+    replicate n False" 
+  apply (unfold shiftr_def)
+  apply (induct n)
+   prefer 2
+   apply (simp add: bl_shiftr1)
+   apply (rule impI)
+   apply (rule take_butlast [THEN trans])
+  apply (auto simp: word_size)
+  done
+
+lemma take_sshiftr' [rule_format] :
+  "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
+    take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
+  apply (unfold sshiftr_def)
+  apply (induct n)
+   prefer 2
+   apply (simp add: bl_sshiftr1)
+   apply (rule impI)
+   apply (rule take_butlast [THEN trans])
+  apply (auto simp: word_size)
+  done
+
+lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
+lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
+
+lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
+  by (auto intro: append_take_drop_id [symmetric])
+
+lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
+lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
+
+lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
+  unfolding shiftl_def
+  by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
+
+lemmas shiftl_bl =
+  shiftl_of_bl [where bl = "to_bl (?w :: ?'a :: len0 word)", simplified]
+
+lemmas shiftl_number [simp] = shiftl_def [where w="number_of ?w"]
+
+lemma bl_shiftl:
+  "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
+  by (simp add: shiftl_bl word_rep_drop word_size min_def)
+
+lemma shiftl_zero_size: 
+  fixes x :: "'a::len0 word"
+  shows "size x <= n ==> x << n = 0"
+  apply (unfold word_size)
+  apply (rule word_eqI)
+  apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
+  done
+
+(* note - the following results use 'a :: len word < number_ring *)
+
+lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
+  apply (simp add: shiftl1_def_u)
+  apply (simp only:  double_number_of_BIT [symmetric])
+  apply simp
+  done
+
+lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
+  apply (simp add: shiftl1_def_u)
+  apply (simp only: double_number_of_BIT [symmetric])
+  apply simp
+  done
+
+lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
+  unfolding shiftl_def 
+  by (induct n) (auto simp: shiftl1_2t power_Suc)
+
+lemma shiftr1_bintr [simp]:
+  "(shiftr1 (number_of w) :: 'a :: len0 word) = 
+    number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
+  unfolding shiftr1_def word_number_of_def
+  by (simp add : word_ubin.eq_norm)
+
+lemma sshiftr1_sbintr [simp] :
+  "(sshiftr1 (number_of w) :: 'a :: len word) = 
+    number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" 
+  unfolding sshiftr1_def word_number_of_def
+  by (simp add : word_sbin.eq_norm)
+
+lemma shiftr_no': 
+  "w = number_of bin ==> 
+  (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
+  apply clarsimp
+  apply (rule word_eqI)
+  apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
+  done
+
+lemma sshiftr_no': 
+  "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n) 
+    (sbintrunc (size w - 1) bin))"
+  apply clarsimp
+  apply (rule word_eqI)
+  apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
+   apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
+  done
+
+lemmas sshiftr_no [simp] = 
+  sshiftr_no' [where w = "number_of ?w", OF refl, unfolded word_size]
+
+lemmas shiftr_no [simp] = 
+  shiftr_no' [where w = "number_of ?w", OF refl, unfolded word_size]
+
+lemma shiftr1_bl_of': 
+  "us = shiftr1 (of_bl bl) ==> length bl <= size us ==> 
+    us = of_bl (butlast bl)"
+  by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin 
+                     word_ubin.eq_norm trunc_bl2bin)
+
+lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
+
+lemma shiftr_bl_of' [rule_format]: 
+  "us = of_bl bl >> n ==> length bl <= size us --> 
+   us = of_bl (take (length bl - n) bl)"
+  apply (unfold shiftr_def)
+  apply hypsubst
+  apply (unfold word_size)
+  apply (induct n)
+   apply clarsimp
+  apply clarsimp
+  apply (subst shiftr1_bl_of)
+   apply simp
+  apply (simp add: butlast_take)
+  done
+
+lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
+
+lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
+  simplified word_size, simplified, THEN eq_reflection, standard]
+
+lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
+  apply (unfold shiftr_bl word_msb_alt)
+  apply (simp add: word_size Suc_le_eq take_Suc)
+  apply (cases "hd (to_bl w)")
+   apply (auto simp: word_1_bl word_0_bl 
+                     of_bl_rep_False [where n=1 and bs="[]", simplified])
+  done
+
+lemmas msb_shift = msb_shift' [unfolded word_size]
+
+lemma align_lem_or [rule_format] :
+  "ALL x m. length x = n + m --> length y = n + m --> 
+    drop m x = replicate n False --> take m y = replicate m False --> 
+    app2 op | x y = take m x @ drop m y"
+  apply (induct_tac y)
+   apply force
+  apply clarsimp
+  apply (case_tac x, force)
+  apply (case_tac m, auto)
+  apply (drule sym)
+  apply auto
+  apply (induct_tac list, auto)
+  done
+
+lemma align_lem_and [rule_format] :
+  "ALL x m. length x = n + m --> length y = n + m --> 
+    drop m x = replicate n False --> take m y = replicate m False --> 
+    app2 op & x y = replicate (n + m) False"
+  apply (induct_tac y)
+   apply force
+  apply clarsimp
+  apply (case_tac x, force)
+  apply (case_tac m, auto)
+  apply (drule sym)
+  apply auto
+  apply (induct_tac list, auto)
+  done
+
+lemma aligned_bl_add_size':
+  "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
+    take m (to_bl y) = replicate m False ==> 
+    to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
+  apply (subgoal_tac "x AND y = 0")
+   prefer 2
+   apply (rule word_bl.Rep_eqD)
+   apply (simp add: bl_word_and to_bl_0)
+   apply (rule align_lem_and [THEN trans])
+       apply (simp_all add: word_size)[5]
+   apply (rule_tac f = "%n. replicate n False" in arg_cong)
+   apply simp
+  apply (subst word_plus_and_or [symmetric])
+  apply (simp add : bl_word_or)
+  apply (rule align_lem_or)
+     apply (simp_all add: word_size)
+  done
+
+lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
+
+subsection "Mask"
+
+lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
+  apply (unfold mask_def test_bit_bl)
+  apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
+  apply (clarsimp simp add: word_size)
+  apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
+  apply (fold of_bl_no)
+  apply (simp add: word_1_bl)
+  apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
+  apply auto
+  done
+
+lemmas nth_mask [simp] = refl [THEN nth_mask']
+
+lemma mask_bl: "mask n = of_bl (replicate n True)"
+  by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
+
+lemma mask_bin: "mask n = number_of (bintrunc n Numeral.Min)"
+  by (auto simp add: nth_bintr word_size intro: word_eqI)
+
+lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
+  apply (rule word_eqI)
+  apply (simp add: nth_bintr word_size word_ops_nth_size)
+  apply (auto simp add: test_bit_bin)
+  done
+
+lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)" 
+  by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
+
+lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def] 
+
+lemma bl_and_mask:
+  "to_bl (w AND mask n :: 'a :: len word) = 
+    replicate (len_of TYPE('a) - n) False @ 
+    drop (len_of TYPE('a) - n) (to_bl w)"
+  apply (rule nth_equalityI)
+   apply simp
+  apply (clarsimp simp add: to_bl_nth word_size)
+  apply (simp add: word_size word_ops_nth_size)
+  apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
+  done
+
+lemmas and_mask_mod_2p = 
+  and_mask_bintr [unfolded word_number_of_alt no_bintr_alt]
+
+lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
+  apply (simp add : and_mask_bintr no_bintr_alt)
+  apply (rule xtr8)
+   prefer 2
+   apply (rule pos_mod_bound)
+  apply auto
+  done
+
+lemmas eq_mod_iff = trans [symmetric, OF int_mod_lem eq_sym_conv]
+
+lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
+  apply (simp add: and_mask_bintr word_number_of_def)
+  apply (simp add: word_ubin.inverse_norm)
+  apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
+  apply (fast intro!: lt2p_lem)
+  done
+
+lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
+  apply (simp add: zdvd_iff_zmod_eq_0 and_mask_mod_2p)
+  apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
+  apply (subst word_uint.norm_Rep [symmetric])
+  apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
+  apply auto
+  done
+
+lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
+  apply (unfold unat_def)
+  apply (rule trans [OF _ and_mask_dvd])
+  apply (unfold dvd_def) 
+  apply auto 
+  apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
+  apply (simp add : int_mult int_power)
+  apply (simp add : nat_mult_distrib nat_power_eq)
+  done
+
+lemma word_2p_lem: 
+  "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
+  apply (unfold word_size word_less_alt word_number_of_alt)
+  apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
+                            int_mod_eq'
+                  simp del: word_of_int_bin)
+  done
+
+lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
+  apply (unfold word_less_alt word_number_of_alt)
+  apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
+                            word_uint.eq_norm
+                  simp del: word_of_int_bin)
+  apply (drule xtr8 [rotated])
+  apply (rule int_mod_le)
+  apply (auto simp add : mod_pos_pos_trivial)
+  done
+
+lemmas mask_eq_iff_w2p =
+  trans [OF mask_eq_iff word_2p_lem [symmetric], standard]
+
+lemmas and_mask_less' = 
+  iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
+
+lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
+  unfolding word_size by (erule and_mask_less')
+
+lemma word_mod_2p_is_mask':
+  "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" 
+  by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
+
+lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
+
+lemma mask_eqs:
+  "(a AND mask n) + b AND mask n = a + b AND mask n"
+  "a + (b AND mask n) AND mask n = a + b AND mask n"
+  "(a AND mask n) - b AND mask n = a - b AND mask n"
+  "a - (b AND mask n) AND mask n = a - b AND mask n"
+  "a * (b AND mask n) AND mask n = a * b AND mask n"
+  "(b AND mask n) * a AND mask n = b * a AND mask n"
+  "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
+  "(a AND mask n) - (b AND mask n) AND mask n = a - b AND mask n"
+  "(a AND mask n) * (b AND mask n) AND mask n = a * b AND mask n"
+  "- (a AND mask n) AND mask n = - a AND mask n"
+  "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
+  "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
+  using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
+  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
+
+lemma mask_power_eq:
+  "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
+  using word_of_int_Ex [where x=x]
+  by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
+
+
+subsection "Revcast"
+
+lemmas revcast_def' = revcast_def [simplified]
+lemmas revcast_def'' = revcast_def' [simplified word_size]
+lemmas revcast_no_def [simp] =
+  revcast_def' [where w="number_of ?w", unfolded word_size]
+
+lemma to_bl_revcast: 
+  "to_bl (revcast w :: 'a :: len0 word) = 
+   takefill False (len_of TYPE ('a)) (to_bl w)"
+  apply (unfold revcast_def' word_size)
+  apply (rule word_bl.Abs_inverse)
+  apply simp
+  done
+
+lemma revcast_rev_ucast': 
+  "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==> 
+    rc = word_reverse uc"
+  apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
+  apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
+  apply (simp add : word_bl.Abs_inverse word_size)
+  done
+
+lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
+
+lemmas revcast_ucast = revcast_rev_ucast
+  [where w = "word_reverse ?w1", simplified word_rev_rev, standard]
+
+lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
+lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
+
+
+-- "linking revcast and cast via shift"
+
+lemmas wsst_TYs = source_size target_size word_size
+
+lemma revcast_down_uu': 
+  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+    rc (w :: 'a :: len word) = ucast (w >> n)"
+  apply (simp add: revcast_def')
+  apply (rule word_bl.Rep_inverse')
+  apply (rule trans, rule ucast_down_drop)
+   prefer 2
+   apply (rule trans, rule drop_shiftr)
+   apply (auto simp: takefill_alt wsst_TYs)
+  done
+
+lemma revcast_down_us': 
+  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+    rc (w :: 'a :: len word) = ucast (w >>> n)"
+  apply (simp add: revcast_def')
+  apply (rule word_bl.Rep_inverse')
+  apply (rule trans, rule ucast_down_drop)
+   prefer 2
+   apply (rule trans, rule drop_sshiftr)
+   apply (auto simp: takefill_alt wsst_TYs)
+  done
+
+lemma revcast_down_su': 
+  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+    rc (w :: 'a :: len word) = scast (w >> n)"
+  apply (simp add: revcast_def')
+  apply (rule word_bl.Rep_inverse')
+  apply (rule trans, rule scast_down_drop)
+   prefer 2
+   apply (rule trans, rule drop_shiftr)
+   apply (auto simp: takefill_alt wsst_TYs)
+  done
+
+lemma revcast_down_ss': 
+  "rc = revcast ==> source_size rc = target_size rc + n ==> 
+    rc (w :: 'a :: len word) = scast (w >>> n)"
+  apply (simp add: revcast_def')
+  apply (rule word_bl.Rep_inverse')
+  apply (rule trans, rule scast_down_drop)
+   prefer 2
+   apply (rule trans, rule drop_sshiftr)
+   apply (auto simp: takefill_alt wsst_TYs)
+  done
+
+lemmas revcast_down_uu = refl [THEN revcast_down_uu']
+lemmas revcast_down_us = refl [THEN revcast_down_us']
+lemmas revcast_down_su = refl [THEN revcast_down_su']
+lemmas revcast_down_ss = refl [THEN revcast_down_ss']
+
+lemma cast_down_rev: 
+  "uc = ucast ==> source_size uc = target_size uc + n ==> 
+    uc w = revcast ((w :: 'a :: len word) << n)"
+  apply (unfold shiftl_rev)
+  apply clarify
+  apply (simp add: revcast_rev_ucast)
+  apply (rule word_rev_gal')
+  apply (rule trans [OF _ revcast_rev_ucast])
+  apply (rule revcast_down_uu [symmetric])
+  apply (auto simp add: wsst_TYs)
+  done
+
+lemma revcast_up': 
+  "rc = revcast ==> source_size rc + n = target_size rc ==> 
+    rc w = (ucast w :: 'a :: len word) << n" 
+  apply (simp add: revcast_def')
+  apply (rule word_bl.Rep_inverse')
+  apply (simp add: takefill_alt)
+  apply (rule bl_shiftl [THEN trans])
+  apply (subst ucast_up_app)
+  apply (auto simp add: wsst_TYs)
+  apply (drule sym)
+  apply (simp add: min_def)
+  done
+
+lemmas revcast_up = refl [THEN revcast_up']
+
+lemmas rc1 = revcast_up [THEN 
+  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
+lemmas rc2 = revcast_down_uu [THEN 
+  revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
+
+lemmas ucast_up =
+ rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
+lemmas ucast_down = 
+  rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
+
+
+subsection "Slices"
+
+lemmas slice1_no_bin [simp] =
+  slice1_def [where w="number_of ?w", unfolded to_bl_no_bin]
+
+lemmas slice_no_bin [simp] = 
+   trans [OF slice_def [THEN meta_eq_to_obj_eq] 
+             slice1_no_bin [THEN meta_eq_to_obj_eq], 
+          unfolded word_size, standard]
+
+lemma slice1_0 [simp] : "slice1 n 0 = 0"
+  unfolding slice1_def by (simp add : to_bl_0)
+
+lemma slice_0 [simp] : "slice n 0 = 0"
+  unfolding slice_def by auto
+
+lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
+  unfolding slice_def' slice1_def
+  by (simp add : takefill_alt word_size)
+
+lemmas slice_take = slice_take' [unfolded word_size]
+
+-- "shiftr to a word of the same size is just slice, 
+    slice is just shiftr then ucast"
+lemmas shiftr_slice = trans
+  [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric], standard]
+
+lemma slice_shiftr: "slice n w = ucast (w >> n)"
+  apply (unfold slice_take shiftr_bl)
+  apply (rule ucast_of_bl_up [symmetric])
+  apply (simp add: word_size)
+  done
+
+lemma nth_slice: 
+  "(slice n w :: 'a :: len0 word) !! m = 
+   (w !! (m + n) & m < len_of TYPE ('a))"
+  unfolding slice_shiftr 
+  by (simp add : nth_ucast nth_shiftr)
+
+lemma slice1_down_alt': 
+  "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==> 
+    to_bl sl = takefill False fs (drop k (to_bl w))"
+  unfolding slice1_def word_size of_bl_def uint_bl
+  by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
+
+lemma slice1_up_alt': 
+  "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==> 
+    to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
+  apply (unfold slice1_def word_size of_bl_def uint_bl)
+  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
+                        takefill_append [symmetric])
+  apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
+    (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
+  apply arith
+  done
+    
+lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
+lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
+lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
+lemmas slice1_up_alts = 
+  le_add_diff_inverse [symmetric, THEN su1] 
+  le_add_diff_inverse2 [symmetric, THEN su1]
+
+lemma ucast_slice1: "ucast w = slice1 (size w) w"
+  unfolding slice1_def ucast_bl
+  by (simp add : takefill_same' word_size)
+
+lemma ucast_slice: "ucast w = slice 0 w"
+  unfolding slice_def by (simp add : ucast_slice1)
+
+lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
+
+lemma revcast_slice1': 
+  "rc = revcast w ==> slice1 (size rc) w = rc"
+  unfolding slice1_def revcast_def' by (simp add : word_size)
+
+lemmas revcast_slice1 = refl [THEN revcast_slice1']
+
+lemma slice1_tf_tf': 
+  "to_bl (slice1 n w :: 'a :: len0 word) = 
+   rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
+  unfolding slice1_def by (rule word_rev_tf)
+
+lemmas slice1_tf_tf = slice1_tf_tf'
+  [THEN word_bl.Rep_inverse', symmetric, standard]
+
+lemma rev_slice1:
+  "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
+  slice1 n (word_reverse w :: 'b :: len0 word) = 
+  word_reverse (slice1 k w :: 'a :: len0 word)"
+  apply (unfold word_reverse_def slice1_tf_tf)
+  apply (rule word_bl.Rep_inverse')
+  apply (rule rev_swap [THEN iffD1])
+  apply (rule trans [symmetric])
+  apply (rule tf_rev)
+   apply (simp add: word_bl.Abs_inverse)
+  apply (simp add: word_bl.Abs_inverse)
+  done
+
+lemma rev_slice': 
+  "res = slice n (word_reverse w) ==> n + k + size res = size w ==> 
+    res = word_reverse (slice k w)"
+  apply (unfold slice_def word_size)
+  apply clarify
+  apply (rule rev_slice1)
+  apply arith
+  done
+
+lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
+
+lemmas sym_notr = 
+  not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
+
+-- {* problem posed by TPHOLs referee:
+      criterion for overflow of addition of signed integers *}
+
+lemma sofl_test:
+  "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
+     ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
+  apply (unfold word_size)
+  apply (cases "len_of TYPE('a)", simp) 
+  apply (subst msb_shift [THEN sym_notr])
+  apply (simp add: word_ops_msb)
+  apply (simp add: word_msb_sint)
+  apply safe
+       apply simp_all
+     apply (unfold sint_word_ariths)
+     apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
+     apply safe
+        apply (insert sint_range' [where x=x])
+        apply (insert sint_range' [where x=y])
+        defer 
+        apply (simp (no_asm), arith)
+       apply (simp (no_asm), arith)
+      defer
+      defer
+      apply (simp (no_asm), arith)
+     apply (simp (no_asm), arith)
+    apply (rule notI [THEN notnotD],
+           drule leI not_leE,
+           drule sbintrunc_inc sbintrunc_dec,      
+           simp)+
+  done
+
+
+section "Split and cat"
+
+lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
+lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
+
+lemma word_rsplit_no:
+  "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
+    map number_of (bin_rsplit (len_of TYPE('a :: len)) 
+      (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
+  apply (unfold word_rsplit_def word_no_wi)
+  apply (simp add: word_ubin.eq_norm)
+  done
+
+lemmas word_rsplit_no_cl [simp] = word_rsplit_no
+  [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
+
+lemma test_bit_cat:
+  "wc = word_cat a b ==> wc !! n = (n < size wc & 
+    (if n < size b then b !! n else a !! (n - size b)))"
+  apply (unfold word_cat_bin' test_bit_bin)
+  apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
+  apply (erule bin_nth_uint_imp)
+  done
+
+lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
+  apply (unfold of_bl_def to_bl_def word_cat_bin')
+  apply (simp add: bl_to_bin_app_cat)
+  done
+
+lemma of_bl_append:
+  "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
+  apply (unfold of_bl_def)
+  apply (simp add: bl_to_bin_app_cat bin_cat_num)
+  apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
+  done
+
+lemma of_bl_False [simp]:
+  "of_bl (False#xs) = of_bl xs"
+  by (rule word_eqI)
+     (auto simp add: test_bit_of_bl nth_append)
+
+lemma of_bl_True: 
+  "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
+  by (subst of_bl_append [where xs="[True]", simplified])
+     (simp add: word_1_bl)
+
+lemma of_bl_Cons:
+  "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
+  by (cases x) (simp_all add: of_bl_True)
+
+lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> 
+  a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
+  apply (frule word_ubin.norm_Rep [THEN ssubst])
+  apply (drule bin_split_trunc1)
+  apply (drule sym [THEN trans])
+  apply assumption
+  apply safe
+  done
+
+lemma word_split_bl': 
+  "std = size c - size b ==> (word_split c = (a, b)) ==> 
+    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
+  apply (unfold word_split_bin')
+  apply safe
+   defer
+   apply (clarsimp split: prod.splits)
+   apply (drule word_ubin.norm_Rep [THEN ssubst])
+   apply (drule split_bintrunc)
+   apply (simp add : of_bl_def bl2bin_drop word_size
+       word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
+  apply (clarsimp split: prod.splits)
+  apply (frule split_uint_lem [THEN conjunct1])
+  apply (unfold word_size)
+  apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
+   defer
+   apply (simp add: word_0_bl word_0_wi_Pls)
+  apply (simp add : of_bl_def to_bl_def)
+  apply (subst bin_split_take1 [symmetric])
+    prefer 2
+    apply assumption
+   apply simp
+  apply (erule thin_rl)
+  apply (erule arg_cong [THEN trans])
+  apply (simp add : word_ubin.norm_eq_iff [symmetric])
+  done
+
+lemma word_split_bl: "std = size c - size b ==> 
+    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
+    word_split c = (a, b)"
+  apply (rule iffI)
+   defer
+   apply (erule (1) word_split_bl')
+  apply (case_tac "word_split c")
+  apply (auto simp add : word_size)
+  apply (frule word_split_bl' [rotated])
+  apply (auto simp add : word_size)
+  done
+
+lemma word_split_bl_eq:
+   "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
+      (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
+       of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
+  apply (rule word_split_bl [THEN iffD1])
+  apply (unfold word_size)
+  apply (rule refl conjI)+
+  done
+
+-- "keep quantifiers for use in simplification"
+lemma test_bit_split':
+  "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
+    a !! m = (m < size a & c !! (m + size b)))"
+  apply (unfold word_split_bin' test_bit_bin)
+  apply (clarify)
+  apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
+  apply (drule bin_nth_split)
+  apply safe
+       apply (simp_all add: add_commute)
+   apply (erule bin_nth_uint_imp)+
+  done
+
+lemmas test_bit_split = 
+  test_bit_split' [THEN mp, simplified all_simps, standard]
+
+lemma test_bit_split_eq: "word_split c = (a, b) <-> 
+  ((ALL n::nat. b !! n = (n < size b & c !! n)) &
+    (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
+  apply (rule_tac iffI)
+   apply (rule_tac conjI)
+    apply (erule test_bit_split [THEN conjunct1])
+   apply (erule test_bit_split [THEN conjunct2])
+  apply (case_tac "word_split c")
+  apply (frule test_bit_split)
+  apply (erule trans)
+  apply (fastsimp intro ! : word_eqI simp add : word_size)
+  done
+
+-- {* this odd result is analogous to ucast\_id, 
+      result to the length given by the result type *}
+
+lemma word_cat_id: "word_cat a b = b"
+  unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
+
+-- "limited hom result"
+lemma word_cat_hom:
+  "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
+  ==>
+  (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
+  word_of_int (bin_cat w (size b) (uint b))"
+  apply (unfold word_cat_def word_size) 
+  apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
+      word_ubin.eq_norm bintr_cat min_def)
+  apply arith
+  done
+
+lemma word_cat_split_alt:
+  "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
+  apply (rule word_eqI)
+  apply (drule test_bit_split)
+  apply (clarsimp simp add : test_bit_cat word_size)
+  apply safe
+  apply arith
+  done
+
+lemmas word_cat_split_size = 
+  sym [THEN [2] word_cat_split_alt [symmetric], standard]
+
+
+subsection "Split and slice"
+
+lemma split_slices: 
+  "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
+  apply (drule test_bit_split)
+  apply (rule conjI)
+   apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
+  done
+
+lemma slice_cat1':
+  "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
+  apply safe
+  apply (rule word_eqI)
+  apply (simp add: nth_slice test_bit_cat word_size)
+  done
+
+lemmas slice_cat1 = refl [THEN slice_cat1']
+lemmas slice_cat2 = trans [OF slice_id word_cat_id]
+
+lemma cat_slices:
+  "a = slice n c ==> b = slice 0 c ==> n = size b ==> \  
+    size a + size b >= size c ==> word_cat a b = c"
+  apply safe
+  apply (rule word_eqI)
+  apply (simp add: nth_slice test_bit_cat word_size)
+  apply safe
+  apply arith
+  done
+
+lemma word_split_cat_alt:
+  "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
+  apply (case_tac "word_split ?w")
+  apply (rule trans, assumption)
+  apply (drule test_bit_split)
+  apply safe
+   apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
+  done
+
+lemmas word_cat_bl_no_bin [simp] =
+  word_cat_bl [where a="number_of ?a" 
+                 and b="number_of ?b", 
+               unfolded to_bl_no_bin]
+
+lemmas word_split_bl_no_bin [simp] =
+  word_split_bl_eq [where c="number_of ?c", unfolded to_bl_no_bin]
+
+-- {* this odd result arises from the fact that the statement of the
+      result implies that the decoded words are of the same type, 
+      and therefore of the same length, as the original word *}
+
+lemma word_rsplit_same: "word_rsplit w = [w]"
+  unfolding word_rsplit_def by (simp add : bin_rsplit_all)
+
+lemma word_rsplit_empty_iff_size:
+  "(word_rsplit w = []) = (size w = 0)" 
+  unfolding word_rsplit_def bin_rsplit_def word_size
+  by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split)
+
+lemma test_bit_rsplit:
+  "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
+    k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
+  apply (unfold word_rsplit_def word_test_bit_def)
+  apply (rule trans)
+   apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
+   apply (rule nth_map [symmetric])
+   apply simp
+  apply (rule bin_nth_rsplit)
+     apply simp_all
+  apply (simp add : word_size rev_map map_compose [symmetric])
+  apply (rule trans)
+   defer
+   apply (rule map_ident [THEN fun_cong])
+  apply (rule refl [THEN map_cong])
+  apply (simp add : word_ubin.eq_norm)
+  apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
+  done
+
+lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
+  unfolding word_rcat_def to_bl_def' of_bl_def
+  by (clarsimp simp add : bin_rcat_bl map_compose)
+
+lemma size_rcat_lem':
+  "size (concat (map to_bl wl)) = length wl * size (hd wl)"
+  unfolding word_size by (induct wl) auto
+
+lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
+
+lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
+
+lemma nth_rcat_lem' [rule_format] :
+  "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw --> 
+    rev (concat (map to_bl wl)) ! n = 
+    rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
+  apply (unfold word_size)
+  apply (induct "wl")
+   apply clarsimp
+  apply (clarsimp simp add : nth_append size_rcat_lem)
+  apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
+         td_gal_lt_len less_Suc_eq_le mod_div_equality')
+  apply clarsimp
+  done
+
+lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
+
+lemma test_bit_rcat:
+  "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = 
+    (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
+  apply (unfold word_rcat_bl word_size)
+  apply (clarsimp simp add : 
+    test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
+  apply safe
+   apply (auto simp add : 
+    test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
+  done
+
+lemma foldl_eq_foldr [rule_format] :
+  "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
+  by (induct xs) (auto simp add : add_assoc)
+
+lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
+
+lemmas test_bit_rsplit_alt = 
+  trans [OF nth_rev_alt [THEN test_bit_cong] 
+  test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
+
+-- "lazy way of expressing that u and v, and su and sv, have same types"
+lemma word_rsplit_len_indep':
+  "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==> 
+    word_rsplit v = sv ==> length su = length sv"
+  apply (unfold word_rsplit_def)
+  apply (auto simp add : bin_rsplit_len_indep)
+  done
+
+lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
+
+lemma length_word_rsplit_size: 
+  "n = len_of TYPE ('a :: len) ==> 
+    (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
+  apply (unfold word_rsplit_def word_size)
+  apply (clarsimp simp add : bin_rsplit_len_le)
+  done
+
+lemmas length_word_rsplit_lt_size = 
+  length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
+
+lemma length_word_rsplit_exp_size: 
+  "n = len_of TYPE ('a :: len) ==> 
+    length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
+  unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
+
+lemma length_word_rsplit_even_size: 
+  "n = len_of TYPE ('a :: len) ==> size w = m * n ==> 
+    length (word_rsplit w :: 'a word list) = m"
+  by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
+
+lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
+
+(* alternative proof of word_rcat_rsplit *)
+lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
+lemmas dtle = xtr4 [OF tdle mult_commute]
+
+lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
+  apply (rule word_eqI)
+  apply (clarsimp simp add : test_bit_rcat word_size)
+  apply (subst refl [THEN test_bit_rsplit])
+    apply (simp_all add: word_size 
+      refl [THEN length_word_rsplit_size [simplified le_def, simplified]])
+   apply safe
+   apply (erule xtr7, rule len_gt_0 [THEN dtle])+
+  done
+
+lemma size_word_rsplit_rcat_size':
+  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
+    size frcw = length ws * len_of TYPE ('a) ==> 
+    size (hd [word_rsplit frcw, ws]) = size ws" 
+  apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
+  apply (fast intro: given_quot_alt)
+  done
+
+lemmas size_word_rsplit_rcat_size = 
+  size_word_rsplit_rcat_size' [simplified]
+
+lemma msrevs:
+  fixes n::nat
+  shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
+  and   "(k * n + m) mod n = m mod n"
+  by (auto simp: add_commute)
+
+lemma word_rsplit_rcat_size':
+  "word_rcat (ws :: 'a :: len word list) = frcw ==> 
+    size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws" 
+  apply (frule size_word_rsplit_rcat_size, assumption)
+  apply (clarsimp simp add : word_size)
+  apply (rule nth_equalityI, assumption)
+  apply clarsimp
+  apply (rule word_eqI)
+  apply (rule trans)
+   apply (rule test_bit_rsplit_alt)
+     apply (clarsimp simp: word_size)+
+  apply (rule trans)
+  apply (rule test_bit_rcat [OF refl refl])
+  apply (simp add : word_size msrevs)
+  apply (subst nth_rev)
+   apply arith
+  apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
+  apply safe
+  apply (simp add : diff_mult_distrib)
+  apply (rule mpl_lem)
+  apply (cases "size ws")
+   apply simp_all
+  done
+
+lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
+
+
+section "Rotation"
+
+lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
+
+lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
+
+lemma rotate_eq_mod: 
+  "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
+  apply (rule box_equals)
+    defer
+    apply (rule rotate_conv_mod [symmetric])+
+  apply simp
+  done
+
+lemmas rotate_eqs [standard] = 
+  trans [OF rotate0 [THEN fun_cong] id_apply]
+  rotate_rotate [symmetric] 
+  rotate_id 
+  rotate_conv_mod 
+  rotate_eq_mod
+
+
+subsection "Rotation of list to right"
+
+lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
+  unfolding rotater1_def by (cases l) auto
+
+lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
+  apply (unfold rotater1_def)
+  apply (cases "l")
+  apply (case_tac [2] "list")
+  apply auto
+  done
+
+lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
+  unfolding rotater1_def by (cases l) auto
+
+lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
+  apply (cases "xs")
+  apply (simp add : rotater1_def)
+  apply (simp add : rotate1_rl')
+  done
+  
+lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
+  unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
+
+lemmas rotater_rev = rotater_rev' [where xs = "rev ?ys", simplified]
+
+lemma rotater_drop_take: 
+  "rotater n xs = 
+   drop (length xs - n mod length xs) xs @
+   take (length xs - n mod length xs) xs"
+  by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
+
+lemma rotater_Suc [simp] : 
+  "rotater (Suc n) xs = rotater1 (rotater n xs)"
+  unfolding rotater_def by auto
+
+lemma rotate_inv_plus [rule_format] :
+  "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs & 
+    rotate k (rotater n xs) = rotate m xs & 
+    rotater n (rotate k xs) = rotate m xs & 
+    rotate n (rotater k xs) = rotater m xs"
+  unfolding rotater_def rotate_def
+  by (induct n) (auto intro: funpow_swap1 [THEN trans])
+  
+lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
+
+lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
+
+lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1, standard]
+lemmas rotate_rl [simp] =
+  rotate_inv_eq [THEN conjunct2, THEN conjunct1, standard]
+
+lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
+  by auto
+
+lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
+  by auto
+
+lemma length_rotater [simp]: 
+  "length (rotater n xs) = length xs"
+  by (simp add : rotater_rev)
+
+lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
+  simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
+lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
+lemmas rotater_eqs = rrs1 [simplified length_rotater, standard]
+lemmas rotater_0 = rotater_eqs (1)
+lemmas rotater_add = rotater_eqs (2)
+
+
+subsection "map, app2, commuting with rotate(r)"
+
+lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
+  by (induct xs) auto
+
+lemma butlast_map:
+  "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
+  by (induct xs) auto
+
+lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
+  unfolding rotater1_def
+  by (cases xs) (auto simp add: last_map butlast_map)
+
+lemma rotater_map:
+  "rotater n (map f xs) = map f (rotater n xs)" 
+  unfolding rotater_def
+  by (induct n) (auto simp add : rotater1_map)
+
+lemma but_last_zip [rule_format] :
+  "ALL ys. length xs = length ys --> xs ~= [] --> 
+    last (zip xs ys) = (last xs, last ys) & 
+    butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 
+  apply (induct "xs")
+  apply auto
+     apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+  done
+
+lemma but_last_app2 [rule_format] :
+  "ALL ys. length xs = length ys --> xs ~= [] --> 
+    last (app2 f xs ys) = f (last xs) (last ys) & 
+    butlast (app2 f xs ys) = app2 f (butlast xs) (butlast ys)" 
+  apply (induct "xs")
+  apply auto
+     apply (unfold app2_def)
+     apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
+  done
+
+lemma rotater1_zip:
+  "length xs = length ys ==> 
+    rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
+  apply (unfold rotater1_def)
+  apply (cases "xs")
+   apply auto
+   apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
+  done
+
+lemma rotater1_app2:
+  "length xs = length ys ==> 
+    rotater1 (app2 f xs ys) = app2 f (rotater1 xs) (rotater1 ys)" 
+  unfolding app2_def by (simp add: rotater1_map rotater1_zip)
+
+lemmas lrth = 
+  box_equals [OF asm_rl length_rotater [symmetric] 
+                 length_rotater [symmetric], 
+              THEN rotater1_app2]
+
+lemma rotater_app2: 
+  "length xs = length ys ==> 
+    rotater n (app2 f xs ys) = app2 f (rotater n xs) (rotater n ys)" 
+  by (induct n) (auto intro!: lrth)
+
+lemma rotate1_app2:
+  "length xs = length ys ==> 
+    rotate1 (app2 f xs ys) = app2 f (rotate1 xs) (rotate1 ys)" 
+  apply (unfold app2_def)
+  apply (cases xs)
+   apply (cases ys, auto simp add : rotate1_def)+
+  done
+
+lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
+  length_rotate [symmetric], THEN rotate1_app2]
+
+lemma rotate_app2: 
+  "length xs = length ys ==> 
+    rotate n (app2 f xs ys) = app2 f (rotate n xs) (rotate n ys)" 
+  by (induct n) (auto intro!: lth)
+
+
+-- "corresponding equalities for word rotation"
+
+lemma to_bl_rotl: 
+  "to_bl (word_rotl n w) = rotate n (to_bl w)"
+  by (simp add: word_bl.Abs_inverse' word_rotl_def)
+
+lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
+
+lemmas word_rotl_eqs =
+  blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
+
+lemma to_bl_rotr: 
+  "to_bl (word_rotr n w) = rotater n (to_bl w)"
+  by (simp add: word_bl.Abs_inverse' word_rotr_def)
+
+lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
+
+lemmas word_rotr_eqs =
+  brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
+
+declare word_rotr_eqs (1) [simp]
+declare word_rotl_eqs (1) [simp]
+
+lemma
+  word_rot_rl [simp]:
+  "word_rotl k (word_rotr k v) = v" and
+  word_rot_lr [simp]:
+  "word_rotr k (word_rotl k v) = v"
+  by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
+
+lemma
+  word_rot_gal:
+  "(word_rotr n v = w) = (word_rotl n w = v)" and
+  word_rot_gal':
+  "(w = word_rotr n v) = (v = word_rotl n w)"
+  by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] 
+           dest: sym)
+
+lemma word_rotr_rev:
+  "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
+  by (simp add: word_bl.Rep_inject [symmetric] to_bl_word_rev
+                to_bl_rotr to_bl_rotl rotater_rev)
+  
+lemma word_roti_0 [simp]: "word_roti 0 w = w"
+  by (unfold word_rot_defs) auto
+
+lemmas abl_cong = arg_cong [where f = "of_bl"]
+
+lemma word_roti_add: 
+  "word_roti (m + n) w = word_roti m (word_roti n w)"
+proof -
+  have rotater_eq_lem: 
+    "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
+    by auto
+
+  have rotate_eq_lem: 
+    "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
+    by auto
+
+  note rpts [symmetric, standard] = 
+    rotate_inv_plus [THEN conjunct1]
+    rotate_inv_plus [THEN conjunct2, THEN conjunct1]
+    rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
+    rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
+
+  note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
+  note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
+
+  show ?thesis
+  apply (unfold word_rot_defs)
+  apply (simp only: split: split_if)
+  apply (safe intro!: abl_cong)
+  apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
+                    to_bl_rotl
+                    to_bl_rotr [THEN word_bl.Rep_inverse']
+                    to_bl_rotr)
+  apply (rule rrp rrrp rpts,
+         simp add: nat_add_distrib [symmetric] 
+                   nat_diff_distrib [symmetric])+
+  done
+qed
+    
+lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
+  apply (unfold word_rot_defs)
+  apply (cut_tac y="size w" in gt_or_eq_0)
+  apply (erule disjE)
+   apply simp_all
+  apply (safe intro!: abl_cong)
+   apply (rule rotater_eqs)
+   apply (simp add: word_size nat_mod_distrib)
+  apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
+  apply (rule rotater_eqs)
+  apply (simp add: word_size nat_mod_distrib)
+  apply (rule int_eq_0_conv [THEN iffD1])
+  apply (simp only: zmod_int zadd_int [symmetric])
+  apply (simp add: rdmods)
+  done
+
+lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
+
+
+subsection "Word rotation commutes with bit-wise operations"
+
+(* using locale to not pollute lemma namespace *)
+locale word_rotate 
+
+context word_rotate
+begin
+
+lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
+
+lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
+
+lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
+
+lemmas ths_app2 [OF lbl_lbl] = rotate_app2 rotater_app2
+
+lemmas ths_map [where xs = "to_bl v"] = rotate_map rotater_map
+
+lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_app2 ths_map
+
+lemma word_rot_logs:
+  "word_rotl n (NOT v) = NOT word_rotl n v"
+  "word_rotr n (NOT v) = NOT word_rotr n v"
+  "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
+  "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
+  "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
+  "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
+  "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
+  "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"  
+  by (rule word_bl.Rep_eqD,
+      rule word_rot_defs' [THEN trans],
+      simp only: blwl_syms [symmetric],
+      rule th1s [THEN trans], 
+      rule refl)+
+end
+
+lemmas word_rot_logs = word_rotate.word_rot_logs
+
+lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
+  simplified word_bl.Rep', standard]
+
+lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
+  simplified word_bl.Rep', standard]
+
+lemma bl_word_roti_dt': 
+  "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==> 
+    to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
+  apply (unfold word_roti_def)
+  apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
+  apply safe
+   apply (simp add: zmod_zminus1_eq_if)
+   apply safe
+    apply (simp add: nat_mult_distrib)
+   apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 
+                                      [THEN conjunct2, THEN order_less_imp_le]]
+                    nat_mod_distrib)
+  apply (simp add: nat_mod_distrib)
+  done
+
+lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
+
+lemmas word_rotl_dt = bl_word_rotl_dt 
+  [THEN word_bl.Rep_inverse' [symmetric], standard] 
+lemmas word_rotr_dt = bl_word_rotr_dt 
+  [THEN word_bl.Rep_inverse' [symmetric], standard]
+lemmas word_roti_dt = bl_word_roti_dt 
+  [THEN word_bl.Rep_inverse' [symmetric], standard]
+
+lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
+  by (simp add : word_rotr_dt word_rotl_dt to_bl_0 replicate_add [symmetric])
+
+lemma word_roti_0' [simp] : "word_roti n 0 = 0"
+  unfolding word_roti_def by auto
+
+lemmas word_rotr_dt_no_bin' [simp] = 
+  word_rotr_dt [where w="number_of ?w", unfolded to_bl_no_bin]
+
+lemmas word_rotl_dt_no_bin' [simp] = 
+  word_rotl_dt [where w="number_of ?w", unfolded to_bl_no_bin]
+
+declare word_roti_def [simp]
+
+end
+