(* 

    ID:         $Id$

    Author:     Jeremy Dawson and Gerwin Klein, NICTA

  contains theorems to do with shifting, rotating, splitting words

*)

header {* Shifting, Rotating, and Splitting Words *}

theory WordShift

imports WordBitwise

begin

subsection "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

              del: BIT_simps)

  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

subsubsection "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, standard]

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)

lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"

proof -

  have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp

  also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)

  finally show ?thesis .

qed

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 w", 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)

lemma shiftl_bl:

  "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"

proof -

  have "w << n = of_bl (to_bl w) << n" by simp

  also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)

  finally show ?thesis .

qed

lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]

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_Bit0 [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_Bit0 [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, standard]

lemmas shiftr_no [simp] = 

  shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]

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 --> 

    map2 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 --> 

    map2 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 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']

subsubsection "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 Int.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)

subsubsection "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, standard]

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 w", 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)

  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]]

subsubsection "Slices"

lemmas slice1_no_bin [simp] =

  slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]

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

subsection "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]