src/HOL/Word/WordShift.thy
author wenzelm
Wed Sep 17 21:27:14 2008 +0200 (2008-09-17)
changeset 28263 69eaa97e7e96
parent 27136 06a8f65e32f6
child 28643 caa1137d25dc
permissions -rw-r--r--
moved global ML bindings to global place;
     1 (* 
     2     ID:         $Id$
     3     Author:     Jeremy Dawson and Gerwin Klein, NICTA
     4 
     5   contains theorems to do with shifting, rotating, splitting words
     6 *)
     7 
     8 header {* Shifting, Rotating, and Splitting Words *}
     9 
    10 theory WordShift
    11 imports WordBitwise
    12 begin
    13 
    14 subsection "Bit shifting"
    15 
    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
    20               del: BIT_simps)
    21   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
    22   apply (subst bintrunc_bintrunc_min)
    23   apply simp
    24   done
    25 
    26 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
    27   unfolding word_0_no shiftl1_number by auto
    28 
    29 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
    30 
    31 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
    32   by (rule trans [OF _ shiftl1_number]) simp
    33 
    34 lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
    35   unfolding shiftr1_def 
    36   by simp (simp add: word_0_wi)
    37 
    38 lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
    39   apply (unfold sshiftr1_def)
    40   apply simp
    41   apply (simp add : word_0_wi)
    42   done
    43 
    44 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
    45   unfolding sshiftr1_def by auto
    46 
    47 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
    48   unfolding shiftl_def by (induct n) auto
    49 
    50 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
    51   unfolding shiftr_def by (induct n) auto
    52 
    53 lemma sshiftr_0 [simp] : "0 >>> n = 0"
    54   unfolding sshiftr_def by (induct n) auto
    55 
    56 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
    57   unfolding sshiftr_def by (induct n) auto
    58 
    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)
    62   apply (cases n)
    63    apply auto
    64   done
    65 
    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)
    69   apply (induct "m")
    70    apply (force elim!: test_bit_size)
    71   apply (clarsimp simp add : nth_shiftl1 word_size)
    72   apply arith
    73   done
    74 
    75 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
    76 
    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)
    80   apply safe
    81   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
    82   apply simp
    83   done
    84 
    85 lemma nth_shiftr: 
    86   "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
    87   apply (unfold shiftr_def)
    88   apply (induct "m")
    89    apply (auto simp add : nth_shiftr1)
    90   done
    91    
    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) *)
    95 
    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)
   100   apply simp 
   101   done
   102 
   103 lemma nth_sshiftr1: 
   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 
   108              del: bin_nth.simps)
   109   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
   110   apply (auto simp add: bin_nth_sint)
   111   done
   112 
   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)
   120   apply safe
   121        apply arith
   122       apply arith
   123      apply (erule thin_rl)
   124      apply (case_tac n)
   125       apply safe
   126       apply simp
   127      apply simp
   128     apply (erule thin_rl)
   129     apply (case_tac n)
   130      apply safe
   131      apply simp
   132     apply simp
   133    apply arith+
   134   done
   135     
   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)
   140   apply (rule xtr7)
   141    prefer 2
   142    apply (rule zdiv_le_dividend)
   143     apply auto
   144   done
   145 
   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)
   149   apply (rule trans)
   150    defer
   151    apply (subst word_sbin.norm_Rep [symmetric])
   152    apply (rule refl)
   153   apply (subst word_sbin.norm_Rep [symmetric])
   154   apply (unfold One_nat_def)
   155   apply (rule sbintrunc_rest)
   156   done
   157 
   158 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
   159   apply (unfold shiftr_def)
   160   apply (induct "n")
   161    apply simp
   162   apply (simp add: shiftr1_div_2 mult_commute
   163                    zdiv_zmult2_eq [symmetric])
   164   done
   165 
   166 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
   167   apply (unfold sshiftr_def)
   168   apply (induct "n")
   169    apply simp
   170   apply (simp add: sshiftr1_div_2 mult_commute
   171                    zdiv_zmult2_eq [symmetric])
   172   done
   173 
   174 subsubsection "shift functions in terms of lists of bools"
   175 
   176 lemmas bshiftr1_no_bin [simp] = 
   177   bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
   178 
   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
   181 
   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)
   185 
   186 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
   187 proof -
   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 .
   191 qed
   192 
   193 lemma bl_shiftl1:
   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)
   197   done
   198 
   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])
   203   done
   204 
   205 lemma bl_shiftr1: 
   206   "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
   207   unfolding shiftr1_bl
   208   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
   209 
   210 
   211 (* relate the two above : TODO - remove the :: len restriction on
   212   this theorem and others depending on it *)
   213 lemma shiftl1_rev: 
   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")
   219    apply auto
   220   done
   221 
   222 lemma shiftl_rev: 
   223   "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
   224   apply (unfold shiftl_def shiftr_def)
   225   apply (induct "n")
   226    apply (auto simp add : shiftl1_rev)
   227   done
   228 
   229 lemmas rev_shiftl =
   230   shiftl_rev [where w = "word_reverse w", simplified, standard]
   231 
   232 lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
   233 lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
   234 
   235 lemma bl_sshiftr1:
   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)
   241    apply clarsimp
   242   apply clarsimp
   243   apply (case_tac i)
   244    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
   245                         nth_bin_to_bl bin_nth.Suc [symmetric] 
   246                         nth_sbintr 
   247                    del: bin_nth.Suc)
   248    apply force
   249   apply (rule impI)
   250   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
   251   apply simp
   252   done
   253 
   254 lemma drop_shiftr: 
   255   "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
   256   apply (unfold shiftr_def)
   257   apply (induct n)
   258    prefer 2
   259    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
   260    apply (rule butlast_take [THEN trans])
   261   apply (auto simp: word_size)
   262   done
   263 
   264 lemma drop_sshiftr: 
   265   "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
   266   apply (unfold sshiftr_def)
   267   apply (induct n)
   268    prefer 2
   269    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
   270    apply (rule butlast_take [THEN trans])
   271   apply (auto simp: word_size)
   272   done
   273 
   274 lemma take_shiftr [rule_format] :
   275   "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = 
   276     replicate n False" 
   277   apply (unfold shiftr_def)
   278   apply (induct n)
   279    prefer 2
   280    apply (simp add: bl_shiftr1)
   281    apply (rule impI)
   282    apply (rule take_butlast [THEN trans])
   283   apply (auto simp: word_size)
   284   done
   285 
   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)
   290   apply (induct n)
   291    prefer 2
   292    apply (simp add: bl_sshiftr1)
   293    apply (rule impI)
   294    apply (rule take_butlast [THEN trans])
   295   apply (auto simp: word_size)
   296   done
   297 
   298 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
   299 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
   300 
   301 lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
   302   by (auto intro: append_take_drop_id [symmetric])
   303 
   304 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
   305 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
   306 
   307 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
   308   unfolding shiftl_def
   309   by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
   310 
   311 lemma shiftl_bl:
   312   "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
   313 proof -
   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 .
   317 qed
   318 
   319 lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]
   320 
   321 lemma bl_shiftl:
   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)
   324 
   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)
   331   done
   332 
   333 (* note - the following results use 'a :: len word < number_ring *)
   334 
   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])
   338   apply simp
   339   done
   340 
   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])
   344   apply simp
   345   done
   346 
   347 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   348   unfolding shiftl_def 
   349   by (induct n) (auto simp: shiftl1_2t power_Suc)
   350 
   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)
   356 
   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)
   362 
   363 lemma shiftr_no': 
   364   "w = number_of bin ==> 
   365   (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
   366   apply clarsimp
   367   apply (rule word_eqI)
   368   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
   369   done
   370 
   371 lemma sshiftr_no': 
   372   "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n) 
   373     (sbintrunc (size w - 1) bin))"
   374   apply clarsimp
   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)+
   378   done
   379 
   380 lemmas sshiftr_no [simp] = 
   381   sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
   382 
   383 lemmas shiftr_no [simp] = 
   384   shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
   385 
   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)
   391 
   392 lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
   393 
   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)
   398   apply hypsubst
   399   apply (unfold word_size)
   400   apply (induct n)
   401    apply clarsimp
   402   apply clarsimp
   403   apply (subst shiftr1_bl_of)
   404    apply simp
   405   apply (simp add: butlast_take)
   406   done
   407 
   408 lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
   409 
   410 lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
   411   simplified word_size, simplified, THEN eq_reflection, standard]
   412 
   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])
   419   done
   420 
   421 lemmas msb_shift = msb_shift' [unfolded word_size]
   422 
   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"
   427   apply (induct_tac y)
   428    apply force
   429   apply clarsimp
   430   apply (case_tac x, force)
   431   apply (case_tac m, auto)
   432   apply (drule sym)
   433   apply auto
   434   apply (induct_tac list, auto)
   435   done
   436 
   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"
   441   apply (induct_tac y)
   442    apply force
   443   apply clarsimp
   444   apply (case_tac x, force)
   445   apply (case_tac m, auto)
   446   apply (drule sym)
   447   apply auto
   448   apply (induct_tac list, auto)
   449   done
   450 
   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")
   456    prefer 2
   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)
   462    apply simp
   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)
   467   done
   468 
   469 lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
   470 
   471 subsubsection "Mask"
   472 
   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])
   481   apply auto
   482   done
   483 
   484 lemmas nth_mask [simp] = refl [THEN nth_mask']
   485 
   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)
   488 
   489 lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
   490   by (auto simp add: nth_bintr word_size intro: word_eqI)
   491 
   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)
   496   done
   497 
   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)
   500 
   501 lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def] 
   502 
   503 lemma bl_and_mask:
   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)
   508    apply simp
   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)
   512   done
   513 
   514 lemmas and_mask_mod_2p = 
   515   and_mask_bintr [unfolded word_number_of_alt no_bintr_alt]
   516 
   517 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
   518   apply (simp add : and_mask_bintr no_bintr_alt)
   519   apply (rule xtr8)
   520    prefer 2
   521    apply (rule pos_mod_bound)
   522   apply auto
   523   done
   524 
   525 lemmas eq_mod_iff = trans [symmetric, OF int_mod_lem eq_sym_conv]
   526 
   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)
   532   done
   533 
   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)
   539   apply auto
   540   done
   541 
   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) 
   546   apply auto 
   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)
   550   done
   551 
   552 lemma word_2p_lem: 
   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 
   556                             int_mod_eq'
   557                   simp del: word_of_int_bin)
   558   done
   559 
   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 
   563                             word_uint.eq_norm
   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)
   568   done
   569 
   570 lemmas mask_eq_iff_w2p =
   571   trans [OF mask_eq_iff word_2p_lem [symmetric], standard]
   572 
   573 lemmas and_mask_less' = 
   574   iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
   575 
   576 lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
   577   unfolding word_size by (erule and_mask_less')
   578 
   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) 
   582 
   583 lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
   584 
   585 lemma mask_eqs:
   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)
   600 
   601 lemma mask_power_eq:
   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)
   605 
   606 
   607 subsubsection "Revcast"
   608 
   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]
   613 
   614 lemma to_bl_revcast: 
   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)
   619   apply simp
   620   done
   621 
   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)
   628   done
   629 
   630 lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
   631 
   632 lemmas revcast_ucast = revcast_rev_ucast
   633   [where w = "word_reverse w", simplified word_rev_rev, standard]
   634 
   635 lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
   636 lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
   637 
   638 
   639 -- "linking revcast and cast via shift"
   640 
   641 lemmas wsst_TYs = source_size target_size word_size
   642 
   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)
   649    prefer 2
   650    apply (rule trans, rule drop_shiftr)
   651    apply (auto simp: takefill_alt wsst_TYs)
   652   done
   653 
   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)
   660    prefer 2
   661    apply (rule trans, rule drop_sshiftr)
   662    apply (auto simp: takefill_alt wsst_TYs)
   663   done
   664 
   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)
   671    prefer 2
   672    apply (rule trans, rule drop_shiftr)
   673    apply (auto simp: takefill_alt wsst_TYs)
   674   done
   675 
   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)
   682    prefer 2
   683    apply (rule trans, rule drop_sshiftr)
   684    apply (auto simp: takefill_alt wsst_TYs)
   685   done
   686 
   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']
   691 
   692 lemma cast_down_rev: 
   693   "uc = ucast ==> source_size uc = target_size uc + n ==> 
   694     uc w = revcast ((w :: 'a :: len word) << n)"
   695   apply (unfold shiftl_rev)
   696   apply clarify
   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)
   702   done
   703 
   704 lemma revcast_up': 
   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)
   713   apply (drule sym)
   714   apply (simp add: min_def)
   715   done
   716 
   717 lemmas revcast_up = refl [THEN revcast_up']
   718 
   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]]
   723 
   724 lemmas ucast_up =
   725  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
   726 lemmas ucast_down = 
   727   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
   728 
   729 
   730 subsubsection "Slices"
   731 
   732 lemmas slice1_no_bin [simp] =
   733   slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
   734 
   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]
   739 
   740 lemma slice1_0 [simp] : "slice1 n 0 = 0"
   741   unfolding slice1_def by (simp add : to_bl_0)
   742 
   743 lemma slice_0 [simp] : "slice n 0 = 0"
   744   unfolding slice_def by auto
   745 
   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)
   749 
   750 lemmas slice_take = slice_take' [unfolded word_size]
   751 
   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]
   756 
   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)
   761   done
   762 
   763 lemma nth_slice: 
   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)
   768 
   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)
   774 
   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)
   783   apply arith
   784   done
   785     
   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]
   792 
   793 lemma ucast_slice1: "ucast w = slice1 (size w) w"
   794   unfolding slice1_def ucast_bl
   795   by (simp add : takefill_same' word_size)
   796 
   797 lemma ucast_slice: "ucast w = slice 0 w"
   798   unfolding slice_def by (simp add : ucast_slice1)
   799 
   800 lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
   801 
   802 lemma revcast_slice1': 
   803   "rc = revcast w ==> slice1 (size rc) w = rc"
   804   unfolding slice1_def revcast_def' by (simp add : word_size)
   805 
   806 lemmas revcast_slice1 = refl [THEN revcast_slice1']
   807 
   808 lemma slice1_tf_tf': 
   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)
   812 
   813 lemmas slice1_tf_tf = slice1_tf_tf'
   814   [THEN word_bl.Rep_inverse', symmetric, standard]
   815 
   816 lemma rev_slice1:
   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])
   824   apply (rule tf_rev)
   825    apply (simp add: word_bl.Abs_inverse)
   826   apply (simp add: word_bl.Abs_inverse)
   827   done
   828 
   829 lemma rev_slice': 
   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)
   833   apply clarify
   834   apply (rule rev_slice1)
   835   apply arith
   836   done
   837 
   838 lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
   839 
   840 lemmas sym_notr = 
   841   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
   842 
   843 -- {* problem posed by TPHOLs referee:
   844       criterion for overflow of addition of signed integers *}
   845 
   846 lemma sofl_test:
   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)
   854   apply safe
   855        apply simp_all
   856      apply (unfold sint_word_ariths)
   857      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
   858      apply safe
   859         apply (insert sint_range' [where x=x])
   860         apply (insert sint_range' [where x=y])
   861         defer 
   862         apply (simp (no_asm), arith)
   863        apply (simp (no_asm), arith)
   864       defer
   865       defer
   866       apply (simp (no_asm), arith)
   867      apply (simp (no_asm), arith)
   868     apply (rule notI [THEN notnotD],
   869            drule leI not_leE,
   870            drule sbintrunc_inc sbintrunc_dec,      
   871            simp)+
   872   done
   873 
   874 
   875 subsection "Split and cat"
   876 
   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]
   879 
   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)
   886   done
   887 
   888 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   889   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
   890 
   891 lemma test_bit_cat:
   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)
   897   done
   898 
   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)
   902   done
   903 
   904 lemma of_bl_append:
   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)
   909   done
   910 
   911 lemma of_bl_False [simp]:
   912   "of_bl (False#xs) = of_bl xs"
   913   by (rule word_eqI)
   914      (auto simp add: test_bit_of_bl nth_append)
   915 
   916 lemma of_bl_True: 
   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)
   920 
   921 lemma of_bl_Cons:
   922   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   923   by (cases x) (simp_all add: of_bl_True)
   924 
   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])
   930   apply assumption
   931   apply safe
   932   done
   933 
   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')
   938   apply safe
   939    defer
   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)")
   949    defer
   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])
   953     prefer 2
   954     apply assumption
   955    apply simp
   956   apply (erule thin_rl)
   957   apply (erule arg_cong [THEN trans])
   958   apply (simp add : word_ubin.norm_eq_iff [symmetric])
   959   done
   960 
   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)"
   964   apply (rule iffI)
   965    defer
   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)
   971   done
   972 
   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)+
   980   done
   981 
   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)
   987   apply (clarify)
   988   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
   989   apply (drule bin_nth_split)
   990   apply safe
   991        apply (simp_all add: add_commute)
   992    apply (erule bin_nth_uint_imp)+
   993   done
   994 
   995 lemmas test_bit_split = 
   996   test_bit_split' [THEN mp, simplified all_simps, standard]
   997 
   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)
  1007   apply (erule trans)
  1008   apply (fastsimp intro ! : word_eqI simp add : word_size)
  1009   done
  1010 
  1011 -- {* this odd result is analogous to @{text "ucast_id"}, 
  1012       result to the length given by the result type *}
  1013 
  1014 lemma word_cat_id: "word_cat a b = b"
  1015   unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
  1016 
  1017 -- "limited hom result"
  1018 lemma word_cat_hom:
  1019   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  1020   ==>
  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)
  1026   apply arith
  1027   done
  1028 
  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)
  1034   apply safe
  1035   apply arith
  1036   done
  1037 
  1038 lemmas word_cat_split_size = 
  1039   sym [THEN [2] word_cat_split_alt [symmetric], standard]
  1040 
  1041 
  1042 subsubsection "Split and slice"
  1043 
  1044 lemma split_slices: 
  1045   "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
  1046   apply (drule test_bit_split)
  1047   apply (rule conjI)
  1048    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  1049   done
  1050 
  1051 lemma slice_cat1':
  1052   "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
  1053   apply safe
  1054   apply (rule word_eqI)
  1055   apply (simp add: nth_slice test_bit_cat word_size)
  1056   done
  1057 
  1058 lemmas slice_cat1 = refl [THEN slice_cat1']
  1059 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  1060 
  1061 lemma cat_slices:
  1062   "a = slice n c ==> b = slice 0 c ==> n = size b ==>
  1063     size a + size b >= size c ==> word_cat a b = c"
  1064   apply safe
  1065   apply (rule word_eqI)
  1066   apply (simp add: nth_slice test_bit_cat word_size)
  1067   apply safe
  1068   apply arith
  1069   done
  1070 
  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)
  1076   apply safe
  1077    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  1078   done
  1079 
  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]
  1084 
  1085 lemmas word_split_bl_no_bin [simp] =
  1086   word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin, standard]
  1087 
  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 *}
  1091 
  1092 lemma word_rsplit_same: "word_rsplit w = [w]"
  1093   unfolding word_rsplit_def by (simp add : bin_rsplit_all)
  1094 
  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)
  1099 
  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)
  1104   apply (rule trans)
  1105    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  1106    apply (rule nth_map [symmetric])
  1107    apply simp
  1108   apply (rule bin_nth_rsplit)
  1109      apply simp_all
  1110   apply (simp add : word_size rev_map map_compose [symmetric])
  1111   apply (rule trans)
  1112    defer
  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])
  1117   done
  1118 
  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)
  1122 
  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
  1126 
  1127 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  1128 
  1129 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
  1130 
  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)
  1136   apply (induct "wl")
  1137    apply clarsimp
  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')
  1141   apply clarsimp
  1142   done
  1143 
  1144 lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
  1145 
  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)
  1152   apply safe
  1153    apply (auto simp add : 
  1154     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  1155   done
  1156 
  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)
  1160 
  1161 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  1162 
  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]]
  1166 
  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)
  1173   done
  1174 
  1175 lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
  1176 
  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)
  1182   done
  1183 
  1184 lemmas length_word_rsplit_lt_size = 
  1185   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  1186 
  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)
  1191 
  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)
  1196 
  1197 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  1198 
  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]
  1202 
  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]])
  1209    apply safe
  1210    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  1211   done
  1212 
  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)
  1219   done
  1220 
  1221 lemmas size_word_rsplit_rcat_size = 
  1222   size_word_rsplit_rcat_size' [simplified]
  1223 
  1224 lemma msrevs:
  1225   fixes n::nat
  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)
  1229 
  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)
  1236   apply clarsimp
  1237   apply (rule word_eqI)
  1238   apply (rule trans)
  1239    apply (rule test_bit_rsplit_alt)
  1240      apply (clarsimp simp: word_size)+
  1241   apply (rule trans)
  1242   apply (rule test_bit_rcat [OF refl refl])
  1243   apply (simp add : word_size msrevs)
  1244   apply (subst nth_rev)
  1245    apply arith
  1246   apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
  1247   apply safe
  1248   apply (simp add : diff_mult_distrib)
  1249   apply (rule mpl_lem)
  1250   apply (cases "size ws")
  1251    apply simp_all
  1252   done
  1253 
  1254 lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
  1255 
  1256 
  1257 subsection "Rotation"
  1258 
  1259 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  1260 
  1261 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  1262 
  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)
  1266     defer
  1267     apply (rule rotate_conv_mod [symmetric])+
  1268   apply simp
  1269   done
  1270 
  1271 lemmas rotate_eqs [standard] = 
  1272   trans [OF rotate0 [THEN fun_cong] id_apply]
  1273   rotate_rotate [symmetric] 
  1274   rotate_id 
  1275   rotate_conv_mod 
  1276   rotate_eq_mod
  1277 
  1278 
  1279 subsubsection "Rotation of list to right"
  1280 
  1281 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  1282   unfolding rotater1_def by (cases l) auto
  1283 
  1284 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  1285   apply (unfold rotater1_def)
  1286   apply (cases "l")
  1287   apply (case_tac [2] "list")
  1288   apply auto
  1289   done
  1290 
  1291 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  1292   unfolding rotater1_def by (cases l) auto
  1293 
  1294 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  1295   apply (cases "xs")
  1296   apply (simp add : rotater1_def)
  1297   apply (simp add : rotate1_rl')
  1298   done
  1299   
  1300 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  1301   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
  1302 
  1303 lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified, standard]
  1304 
  1305 lemma rotater_drop_take: 
  1306   "rotater n xs = 
  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)
  1310 
  1311 lemma rotater_Suc [simp] : 
  1312   "rotater (Suc n) xs = rotater1 (rotater n xs)"
  1313   unfolding rotater_def by auto
  1314 
  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])
  1322   
  1323 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  1324 
  1325 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  1326 
  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]
  1330 
  1331 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
  1332   by auto
  1333 
  1334 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
  1335   by auto
  1336 
  1337 lemma length_rotater [simp]: 
  1338   "length (rotater n xs) = length xs"
  1339   by (simp add : rotater_rev)
  1340 
  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)
  1347 
  1348 
  1349 subsubsection "map, map2, commuting with rotate(r)"
  1350 
  1351 lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
  1352   by (induct xs) auto
  1353 
  1354 lemma butlast_map:
  1355   "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
  1356   by (induct xs) auto
  1357 
  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)
  1361 
  1362 lemma rotater_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)
  1366 
  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)" 
  1371   apply (induct "xs")
  1372   apply auto
  1373      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  1374   done
  1375 
  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)" 
  1380   apply (induct "xs")
  1381   apply auto
  1382      apply (unfold map2_def)
  1383      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  1384   done
  1385 
  1386 lemma rotater1_zip:
  1387   "length xs = length ys ==> 
  1388     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  1389   apply (unfold rotater1_def)
  1390   apply (cases "xs")
  1391    apply auto
  1392    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  1393   done
  1394 
  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)
  1399 
  1400 lemmas lrth = 
  1401   box_equals [OF asm_rl length_rotater [symmetric] 
  1402                  length_rotater [symmetric], 
  1403               THEN rotater1_map2]
  1404 
  1405 lemma rotater_map2: 
  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)
  1409 
  1410 lemma rotate1_map2:
  1411   "length xs = length ys ==> 
  1412     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  1413   apply (unfold map2_def)
  1414   apply (cases xs)
  1415    apply (cases ys, auto simp add : rotate1_def)+
  1416   done
  1417 
  1418 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
  1419   length_rotate [symmetric], THEN rotate1_map2]
  1420 
  1421 lemma rotate_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)
  1425 
  1426 
  1427 -- "corresponding equalities for word rotation"
  1428 
  1429 lemma to_bl_rotl: 
  1430   "to_bl (word_rotl n w) = rotate n (to_bl w)"
  1431   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  1432 
  1433 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  1434 
  1435 lemmas word_rotl_eqs =
  1436   blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  1437 
  1438 lemma to_bl_rotr: 
  1439   "to_bl (word_rotr n w) = rotater n (to_bl w)"
  1440   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  1441 
  1442 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  1443 
  1444 lemmas word_rotr_eqs =
  1445   brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  1446 
  1447 declare word_rotr_eqs (1) [simp]
  1448 declare word_rotl_eqs (1) [simp]
  1449 
  1450 lemma
  1451   word_rot_rl [simp]:
  1452   "word_rotl k (word_rotr k v) = v" and
  1453   word_rot_lr [simp]:
  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])
  1456 
  1457 lemma
  1458   word_rot_gal:
  1459   "(word_rotr n v = w) = (word_rotl n w = v)" and
  1460   word_rot_gal':
  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] 
  1463            dest: sym)
  1464 
  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)
  1469   
  1470 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  1471   by (unfold word_rot_defs) auto
  1472 
  1473 lemmas abl_cong = arg_cong [where f = "of_bl"]
  1474 
  1475 lemma word_roti_add: 
  1476   "word_roti (m + n) w = word_roti m (word_roti n w)"
  1477 proof -
  1478   have rotater_eq_lem: 
  1479     "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
  1480     by auto
  1481 
  1482   have rotate_eq_lem: 
  1483     "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
  1484     by auto
  1485 
  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]
  1491 
  1492   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  1493   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  1494 
  1495   show ?thesis
  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'] 
  1500                     to_bl_rotl
  1501                     to_bl_rotr [THEN word_bl.Rep_inverse']
  1502                     to_bl_rotr)
  1503   apply (rule rrp rrrp rpts,
  1504          simp add: nat_add_distrib [symmetric] 
  1505                    nat_diff_distrib [symmetric])+
  1506   done
  1507 qed
  1508     
  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)
  1512   apply (erule disjE)
  1513    apply simp_all
  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)
  1523   done
  1524 
  1525 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  1526 
  1527 
  1528 subsubsection "Word rotation commutes with bit-wise operations"
  1529 
  1530 (* using locale to not pollute lemma namespace *)
  1531 locale word_rotate 
  1532 
  1533 context word_rotate
  1534 begin
  1535 
  1536 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  1537 
  1538 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  1539 
  1540 lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
  1541 
  1542 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  1543 
  1544 lemmas ths_map [where xs = "to_bl v", standard] = rotate_map rotater_map
  1545 
  1546 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  1547 
  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], 
  1561       rule refl)+
  1562 end
  1563 
  1564 lemmas word_rot_logs = word_rotate.word_rot_logs
  1565 
  1566 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  1567   simplified word_bl.Rep', standard]
  1568 
  1569 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  1570   simplified word_bl.Rep', standard]
  1571 
  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)
  1577   apply safe
  1578    apply (simp add: zmod_zminus1_eq_if)
  1579    apply safe
  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]]
  1583                     nat_mod_distrib)
  1584   apply (simp add: nat_mod_distrib)
  1585   done
  1586 
  1587 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  1588 
  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]
  1595 
  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])
  1598 
  1599 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  1600   unfolding word_roti_def by auto
  1601 
  1602 lemmas word_rotr_dt_no_bin' [simp] = 
  1603   word_rotr_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
  1604 
  1605 lemmas word_rotl_dt_no_bin' [simp] = 
  1606   word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
  1607 
  1608 declare word_roti_def [simp]
  1609 
  1610 end
  1611