src/HOL/Word/WordShift.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30042 31039ee583fa
child 30952 7ab2716dd93b
permissions -rw-r--r--
added lemmas
     1 (* 
     2     Author:     Jeremy Dawson and Gerwin Klein, NICTA
     3 
     4   contains theorems to do with shifting, rotating, splitting words
     5 *)
     6 
     7 header {* Shifting, Rotating, and Splitting Words *}
     8 
     9 theory WordShift
    10 imports WordBitwise
    11 begin
    12 
    13 subsection "Bit shifting"
    14 
    15 lemma shiftl1_number [simp] :
    16   "shiftl1 (number_of w) = number_of (w BIT bit.B0)"
    17   apply (unfold shiftl1_def word_number_of_def)
    18   apply (simp add: word_ubin.norm_eq_iff [symmetric] word_ubin.eq_norm
    19               del: BIT_simps)
    20   apply (subst refl [THEN bintrunc_BIT_I, symmetric])
    21   apply (subst bintrunc_bintrunc_min)
    22   apply simp
    23   done
    24 
    25 lemma shiftl1_0 [simp] : "shiftl1 0 = 0"
    26   unfolding word_0_no shiftl1_number by auto
    27 
    28 lemmas shiftl1_def_u = shiftl1_def [folded word_number_of_def]
    29 
    30 lemma shiftl1_def_s: "shiftl1 w = number_of (sint w BIT bit.B0)"
    31   by (rule trans [OF _ shiftl1_number]) simp
    32 
    33 lemma shiftr1_0 [simp] : "shiftr1 0 = 0"
    34   unfolding shiftr1_def 
    35   by simp (simp add: word_0_wi)
    36 
    37 lemma sshiftr1_0 [simp] : "sshiftr1 0 = 0"
    38   apply (unfold sshiftr1_def)
    39   apply simp
    40   apply (simp add : word_0_wi)
    41   done
    42 
    43 lemma sshiftr1_n1 [simp] : "sshiftr1 -1 = -1"
    44   unfolding sshiftr1_def by auto
    45 
    46 lemma shiftl_0 [simp] : "(0::'a::len0 word) << n = 0"
    47   unfolding shiftl_def by (induct n) auto
    48 
    49 lemma shiftr_0 [simp] : "(0::'a::len0 word) >> n = 0"
    50   unfolding shiftr_def by (induct n) auto
    51 
    52 lemma sshiftr_0 [simp] : "0 >>> n = 0"
    53   unfolding sshiftr_def by (induct n) auto
    54 
    55 lemma sshiftr_n1 [simp] : "-1 >>> n = -1"
    56   unfolding sshiftr_def by (induct n) auto
    57 
    58 lemma nth_shiftl1: "shiftl1 w !! n = (n < size w & n > 0 & w !! (n - 1))"
    59   apply (unfold shiftl1_def word_test_bit_def)
    60   apply (simp add: nth_bintr word_ubin.eq_norm word_size)
    61   apply (cases n)
    62    apply auto
    63   done
    64 
    65 lemma nth_shiftl' [rule_format]:
    66   "ALL n. ((w::'a::len0 word) << m) !! n = (n < size w & n >= m & w !! (n - m))"
    67   apply (unfold shiftl_def)
    68   apply (induct "m")
    69    apply (force elim!: test_bit_size)
    70   apply (clarsimp simp add : nth_shiftl1 word_size)
    71   apply arith
    72   done
    73 
    74 lemmas nth_shiftl = nth_shiftl' [unfolded word_size] 
    75 
    76 lemma nth_shiftr1: "shiftr1 w !! n = w !! Suc n"
    77   apply (unfold shiftr1_def word_test_bit_def)
    78   apply (simp add: nth_bintr word_ubin.eq_norm)
    79   apply safe
    80   apply (drule bin_nth.Suc [THEN iffD2, THEN bin_nth_uint_imp])
    81   apply simp
    82   done
    83 
    84 lemma nth_shiftr: 
    85   "\<And>n. ((w::'a::len0 word) >> m) !! n = w !! (n + m)"
    86   apply (unfold shiftr_def)
    87   apply (induct "m")
    88    apply (auto simp add : nth_shiftr1)
    89   done
    90    
    91 (* see paper page 10, (1), (2), shiftr1_def is of the form of (1),
    92   where f (ie bin_rest) takes normal arguments to normal results,
    93   thus we get (2) from (1) *)
    94 
    95 lemma uint_shiftr1: "uint (shiftr1 w) = bin_rest (uint w)" 
    96   apply (unfold shiftr1_def word_ubin.eq_norm bin_rest_trunc_i)
    97   apply (subst bintr_uint [symmetric, OF order_refl])
    98   apply (simp only : bintrunc_bintrunc_l)
    99   apply simp 
   100   done
   101 
   102 lemma nth_sshiftr1: 
   103   "sshiftr1 w !! n = (if n = size w - 1 then w !! n else w !! Suc n)"
   104   apply (unfold sshiftr1_def word_test_bit_def)
   105   apply (simp add: nth_bintr word_ubin.eq_norm
   106                    bin_nth.Suc [symmetric] word_size 
   107              del: bin_nth.simps)
   108   apply (simp add: nth_bintr uint_sint del : bin_nth.simps)
   109   apply (auto simp add: bin_nth_sint)
   110   done
   111 
   112 lemma nth_sshiftr [rule_format] : 
   113   "ALL n. sshiftr w m !! n = (n < size w & 
   114     (if n + m >= size w then w !! (size w - 1) else w !! (n + m)))"
   115   apply (unfold sshiftr_def)
   116   apply (induct_tac "m")
   117    apply (simp add: test_bit_bl)
   118   apply (clarsimp simp add: nth_sshiftr1 word_size)
   119   apply safe
   120        apply arith
   121       apply arith
   122      apply (erule thin_rl)
   123      apply (case_tac n)
   124       apply safe
   125       apply simp
   126      apply simp
   127     apply (erule thin_rl)
   128     apply (case_tac n)
   129      apply safe
   130      apply simp
   131     apply simp
   132    apply arith+
   133   done
   134     
   135 lemma shiftr1_div_2: "uint (shiftr1 w) = uint w div 2"
   136   apply (unfold shiftr1_def bin_rest_div)
   137   apply (rule word_uint.Abs_inverse)
   138   apply (simp add: uints_num pos_imp_zdiv_nonneg_iff)
   139   apply (rule xtr7)
   140    prefer 2
   141    apply (rule zdiv_le_dividend)
   142     apply auto
   143   done
   144 
   145 lemma sshiftr1_div_2: "sint (sshiftr1 w) = sint w div 2"
   146   apply (unfold sshiftr1_def bin_rest_div [symmetric])
   147   apply (simp add: word_sbin.eq_norm)
   148   apply (rule trans)
   149    defer
   150    apply (subst word_sbin.norm_Rep [symmetric])
   151    apply (rule refl)
   152   apply (subst word_sbin.norm_Rep [symmetric])
   153   apply (unfold One_nat_def)
   154   apply (rule sbintrunc_rest)
   155   done
   156 
   157 lemma shiftr_div_2n: "uint (shiftr w n) = uint w div 2 ^ n"
   158   apply (unfold shiftr_def)
   159   apply (induct "n")
   160    apply simp
   161   apply (simp add: shiftr1_div_2 mult_commute
   162                    zdiv_zmult2_eq [symmetric])
   163   done
   164 
   165 lemma sshiftr_div_2n: "sint (sshiftr w n) = sint w div 2 ^ n"
   166   apply (unfold sshiftr_def)
   167   apply (induct "n")
   168    apply simp
   169   apply (simp add: sshiftr1_div_2 mult_commute
   170                    zdiv_zmult2_eq [symmetric])
   171   done
   172 
   173 subsubsection "shift functions in terms of lists of bools"
   174 
   175 lemmas bshiftr1_no_bin [simp] = 
   176   bshiftr1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
   177 
   178 lemma bshiftr1_bl: "to_bl (bshiftr1 b w) = b # butlast (to_bl w)"
   179   unfolding bshiftr1_def by (rule word_bl.Abs_inverse) simp
   180 
   181 lemma shiftl1_of_bl: "shiftl1 (of_bl bl) = of_bl (bl @ [False])"
   182   unfolding uint_bl of_bl_no 
   183   by (simp add: bl_to_bin_aux_append bl_to_bin_def)
   184 
   185 lemma shiftl1_bl: "shiftl1 (w::'a::len0 word) = of_bl (to_bl w @ [False])"
   186 proof -
   187   have "shiftl1 w = shiftl1 (of_bl (to_bl w))" by simp
   188   also have "\<dots> = of_bl (to_bl w @ [False])" by (rule shiftl1_of_bl)
   189   finally show ?thesis .
   190 qed
   191 
   192 lemma bl_shiftl1:
   193   "to_bl (shiftl1 (w :: 'a :: len word)) = tl (to_bl w) @ [False]"
   194   apply (simp add: shiftl1_bl word_rep_drop drop_Suc drop_Cons')
   195   apply (fast intro!: Suc_leI)
   196   done
   197 
   198 lemma shiftr1_bl: "shiftr1 w = of_bl (butlast (to_bl w))"
   199   apply (unfold shiftr1_def uint_bl of_bl_def)
   200   apply (simp add: butlast_rest_bin word_size)
   201   apply (simp add: bin_rest_trunc [symmetric, unfolded One_nat_def])
   202   done
   203 
   204 lemma bl_shiftr1: 
   205   "to_bl (shiftr1 (w :: 'a :: len word)) = False # butlast (to_bl w)"
   206   unfolding shiftr1_bl
   207   by (simp add : word_rep_drop len_gt_0 [THEN Suc_leI])
   208 
   209 
   210 (* relate the two above : TODO - remove the :: len restriction on
   211   this theorem and others depending on it *)
   212 lemma shiftl1_rev: 
   213   "shiftl1 (w :: 'a :: len word) = word_reverse (shiftr1 (word_reverse w))"
   214   apply (unfold word_reverse_def)
   215   apply (rule word_bl.Rep_inverse' [symmetric])
   216   apply (simp add: bl_shiftl1 bl_shiftr1 word_bl.Abs_inverse)
   217   apply (cases "to_bl w")
   218    apply auto
   219   done
   220 
   221 lemma shiftl_rev: 
   222   "shiftl (w :: 'a :: len word) n = word_reverse (shiftr (word_reverse w) n)"
   223   apply (unfold shiftl_def shiftr_def)
   224   apply (induct "n")
   225    apply (auto simp add : shiftl1_rev)
   226   done
   227 
   228 lemmas rev_shiftl =
   229   shiftl_rev [where w = "word_reverse w", simplified, standard]
   230 
   231 lemmas shiftr_rev = rev_shiftl [THEN word_rev_gal', standard]
   232 lemmas rev_shiftr = shiftl_rev [THEN word_rev_gal', standard]
   233 
   234 lemma bl_sshiftr1:
   235   "to_bl (sshiftr1 (w :: 'a :: len word)) = hd (to_bl w) # butlast (to_bl w)"
   236   apply (unfold sshiftr1_def uint_bl word_size)
   237   apply (simp add: butlast_rest_bin word_ubin.eq_norm)
   238   apply (simp add: sint_uint)
   239   apply (rule nth_equalityI)
   240    apply clarsimp
   241   apply clarsimp
   242   apply (case_tac i)
   243    apply (simp_all add: hd_conv_nth length_0_conv [symmetric]
   244                         nth_bin_to_bl bin_nth.Suc [symmetric] 
   245                         nth_sbintr 
   246                    del: bin_nth.Suc)
   247    apply force
   248   apply (rule impI)
   249   apply (rule_tac f = "bin_nth (uint w)" in arg_cong)
   250   apply simp
   251   done
   252 
   253 lemma drop_shiftr: 
   254   "drop n (to_bl ((w :: 'a :: len word) >> n)) = take (size w - n) (to_bl w)" 
   255   apply (unfold shiftr_def)
   256   apply (induct n)
   257    prefer 2
   258    apply (simp add: drop_Suc bl_shiftr1 butlast_drop [symmetric])
   259    apply (rule butlast_take [THEN trans])
   260   apply (auto simp: word_size)
   261   done
   262 
   263 lemma drop_sshiftr: 
   264   "drop n (to_bl ((w :: 'a :: len word) >>> n)) = take (size w - n) (to_bl w)"
   265   apply (unfold sshiftr_def)
   266   apply (induct n)
   267    prefer 2
   268    apply (simp add: drop_Suc bl_sshiftr1 butlast_drop [symmetric])
   269    apply (rule butlast_take [THEN trans])
   270   apply (auto simp: word_size)
   271   done
   272 
   273 lemma take_shiftr [rule_format] :
   274   "n <= size (w :: 'a :: len word) --> take n (to_bl (w >> n)) = 
   275     replicate n False" 
   276   apply (unfold shiftr_def)
   277   apply (induct n)
   278    prefer 2
   279    apply (simp add: bl_shiftr1)
   280    apply (rule impI)
   281    apply (rule take_butlast [THEN trans])
   282   apply (auto simp: word_size)
   283   done
   284 
   285 lemma take_sshiftr' [rule_format] :
   286   "n <= size (w :: 'a :: len word) --> hd (to_bl (w >>> n)) = hd (to_bl w) & 
   287     take n (to_bl (w >>> n)) = replicate n (hd (to_bl w))" 
   288   apply (unfold sshiftr_def)
   289   apply (induct n)
   290    prefer 2
   291    apply (simp add: bl_sshiftr1)
   292    apply (rule impI)
   293    apply (rule take_butlast [THEN trans])
   294   apply (auto simp: word_size)
   295   done
   296 
   297 lemmas hd_sshiftr = take_sshiftr' [THEN conjunct1, standard]
   298 lemmas take_sshiftr = take_sshiftr' [THEN conjunct2, standard]
   299 
   300 lemma atd_lem: "take n xs = t ==> drop n xs = d ==> xs = t @ d"
   301   by (auto intro: append_take_drop_id [symmetric])
   302 
   303 lemmas bl_shiftr = atd_lem [OF take_shiftr drop_shiftr]
   304 lemmas bl_sshiftr = atd_lem [OF take_sshiftr drop_sshiftr]
   305 
   306 lemma shiftl_of_bl: "of_bl bl << n = of_bl (bl @ replicate n False)"
   307   unfolding shiftl_def
   308   by (induct n) (auto simp: shiftl1_of_bl replicate_app_Cons_same)
   309 
   310 lemma shiftl_bl:
   311   "(w::'a::len0 word) << (n::nat) = of_bl (to_bl w @ replicate n False)"
   312 proof -
   313   have "w << n = of_bl (to_bl w) << n" by simp
   314   also have "\<dots> = of_bl (to_bl w @ replicate n False)" by (rule shiftl_of_bl)
   315   finally show ?thesis .
   316 qed
   317 
   318 lemmas shiftl_number [simp] = shiftl_def [where w="number_of w", standard]
   319 
   320 lemma bl_shiftl:
   321   "to_bl (w << n) = drop n (to_bl w) @ replicate (min (size w) n) False"
   322   by (simp add: shiftl_bl word_rep_drop word_size min_def)
   323 
   324 lemma shiftl_zero_size: 
   325   fixes x :: "'a::len0 word"
   326   shows "size x <= n ==> x << n = 0"
   327   apply (unfold word_size)
   328   apply (rule word_eqI)
   329   apply (clarsimp simp add: shiftl_bl word_size test_bit_of_bl nth_append)
   330   done
   331 
   332 (* note - the following results use 'a :: len word < number_ring *)
   333 
   334 lemma shiftl1_2t: "shiftl1 (w :: 'a :: len word) = 2 * w"
   335   apply (simp add: shiftl1_def_u)
   336   apply (simp only:  double_number_of_Bit0 [symmetric])
   337   apply simp
   338   done
   339 
   340 lemma shiftl1_p: "shiftl1 (w :: 'a :: len word) = w + w"
   341   apply (simp add: shiftl1_def_u)
   342   apply (simp only: double_number_of_Bit0 [symmetric])
   343   apply simp
   344   done
   345 
   346 lemma shiftl_t2n: "shiftl (w :: 'a :: len word) n = 2 ^ n * w"
   347   unfolding shiftl_def 
   348   by (induct n) (auto simp: shiftl1_2t power_Suc)
   349 
   350 lemma shiftr1_bintr [simp]:
   351   "(shiftr1 (number_of w) :: 'a :: len0 word) = 
   352     number_of (bin_rest (bintrunc (len_of TYPE ('a)) w))" 
   353   unfolding shiftr1_def word_number_of_def
   354   by (simp add : word_ubin.eq_norm)
   355 
   356 lemma sshiftr1_sbintr [simp] :
   357   "(sshiftr1 (number_of w) :: 'a :: len word) = 
   358     number_of (bin_rest (sbintrunc (len_of TYPE ('a) - 1) w))" 
   359   unfolding sshiftr1_def word_number_of_def
   360   by (simp add : word_sbin.eq_norm)
   361 
   362 lemma shiftr_no': 
   363   "w = number_of bin ==> 
   364   (w::'a::len0 word) >> n = number_of ((bin_rest ^ n) (bintrunc (size w) bin))"
   365   apply clarsimp
   366   apply (rule word_eqI)
   367   apply (auto simp: nth_shiftr nth_rest_power_bin nth_bintr word_size)
   368   done
   369 
   370 lemma sshiftr_no': 
   371   "w = number_of bin ==> w >>> n = number_of ((bin_rest ^ n) 
   372     (sbintrunc (size w - 1) bin))"
   373   apply clarsimp
   374   apply (rule word_eqI)
   375   apply (auto simp: nth_sshiftr nth_rest_power_bin nth_sbintr word_size)
   376    apply (subgoal_tac "na + n = len_of TYPE('a) - Suc 0", simp, simp)+
   377   done
   378 
   379 lemmas sshiftr_no [simp] = 
   380   sshiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
   381 
   382 lemmas shiftr_no [simp] = 
   383   shiftr_no' [where w = "number_of w", OF refl, unfolded word_size, standard]
   384 
   385 lemma shiftr1_bl_of': 
   386   "us = shiftr1 (of_bl bl) ==> length bl <= size us ==> 
   387     us = of_bl (butlast bl)"
   388   by (clarsimp simp: shiftr1_def of_bl_def word_size butlast_rest_bl2bin 
   389                      word_ubin.eq_norm trunc_bl2bin)
   390 
   391 lemmas shiftr1_bl_of = refl [THEN shiftr1_bl_of', unfolded word_size]
   392 
   393 lemma shiftr_bl_of' [rule_format]: 
   394   "us = of_bl bl >> n ==> length bl <= size us --> 
   395    us = of_bl (take (length bl - n) bl)"
   396   apply (unfold shiftr_def)
   397   apply hypsubst
   398   apply (unfold word_size)
   399   apply (induct n)
   400    apply clarsimp
   401   apply clarsimp
   402   apply (subst shiftr1_bl_of)
   403    apply simp
   404   apply (simp add: butlast_take)
   405   done
   406 
   407 lemmas shiftr_bl_of = refl [THEN shiftr_bl_of', unfolded word_size]
   408 
   409 lemmas shiftr_bl = word_bl.Rep' [THEN eq_imp_le, THEN shiftr_bl_of,
   410   simplified word_size, simplified, THEN eq_reflection, standard]
   411 
   412 lemma msb_shift': "msb (w::'a::len word) <-> (w >> (size w - 1)) ~= 0"
   413   apply (unfold shiftr_bl word_msb_alt)
   414   apply (simp add: word_size Suc_le_eq take_Suc)
   415   apply (cases "hd (to_bl w)")
   416    apply (auto simp: word_1_bl word_0_bl 
   417                      of_bl_rep_False [where n=1 and bs="[]", simplified])
   418   done
   419 
   420 lemmas msb_shift = msb_shift' [unfolded word_size]
   421 
   422 lemma align_lem_or [rule_format] :
   423   "ALL x m. length x = n + m --> length y = n + m --> 
   424     drop m x = replicate n False --> take m y = replicate m False --> 
   425     map2 op | x y = take m x @ drop m y"
   426   apply (induct_tac y)
   427    apply force
   428   apply clarsimp
   429   apply (case_tac x, force)
   430   apply (case_tac m, auto)
   431   apply (drule sym)
   432   apply auto
   433   apply (induct_tac list, auto)
   434   done
   435 
   436 lemma align_lem_and [rule_format] :
   437   "ALL x m. length x = n + m --> length y = n + m --> 
   438     drop m x = replicate n False --> take m y = replicate m False --> 
   439     map2 op & x y = replicate (n + m) False"
   440   apply (induct_tac y)
   441    apply force
   442   apply clarsimp
   443   apply (case_tac x, force)
   444   apply (case_tac m, auto)
   445   apply (drule sym)
   446   apply auto
   447   apply (induct_tac list, auto)
   448   done
   449 
   450 lemma aligned_bl_add_size':
   451   "size x - n = m ==> n <= size x ==> drop m (to_bl x) = replicate n False ==>
   452     take m (to_bl y) = replicate m False ==> 
   453     to_bl (x + y) = take m (to_bl x) @ drop m (to_bl y)"
   454   apply (subgoal_tac "x AND y = 0")
   455    prefer 2
   456    apply (rule word_bl.Rep_eqD)
   457    apply (simp add: bl_word_and to_bl_0)
   458    apply (rule align_lem_and [THEN trans])
   459        apply (simp_all add: word_size)[5]
   460    apply simp
   461   apply (subst word_plus_and_or [symmetric])
   462   apply (simp add : bl_word_or)
   463   apply (rule align_lem_or)
   464      apply (simp_all add: word_size)
   465   done
   466 
   467 lemmas aligned_bl_add_size = refl [THEN aligned_bl_add_size']
   468 
   469 subsubsection "Mask"
   470 
   471 lemma nth_mask': "m = mask n ==> test_bit m i = (i < n & i < size m)"
   472   apply (unfold mask_def test_bit_bl)
   473   apply (simp only: word_1_bl [symmetric] shiftl_of_bl)
   474   apply (clarsimp simp add: word_size)
   475   apply (simp only: of_bl_no mask_lem number_of_succ add_diff_cancel2)
   476   apply (fold of_bl_no)
   477   apply (simp add: word_1_bl)
   478   apply (rule test_bit_of_bl [THEN trans, unfolded test_bit_bl word_size])
   479   apply auto
   480   done
   481 
   482 lemmas nth_mask [simp] = refl [THEN nth_mask']
   483 
   484 lemma mask_bl: "mask n = of_bl (replicate n True)"
   485   by (auto simp add : test_bit_of_bl word_size intro: word_eqI)
   486 
   487 lemma mask_bin: "mask n = number_of (bintrunc n Int.Min)"
   488   by (auto simp add: nth_bintr word_size intro: word_eqI)
   489 
   490 lemma and_mask_bintr: "w AND mask n = number_of (bintrunc n (uint w))"
   491   apply (rule word_eqI)
   492   apply (simp add: nth_bintr word_size word_ops_nth_size)
   493   apply (auto simp add: test_bit_bin)
   494   done
   495 
   496 lemma and_mask_no: "number_of i AND mask n = number_of (bintrunc n i)" 
   497   by (auto simp add : nth_bintr word_size word_ops_nth_size intro: word_eqI)
   498 
   499 lemmas and_mask_wi = and_mask_no [unfolded word_number_of_def] 
   500 
   501 lemma bl_and_mask:
   502   "to_bl (w AND mask n :: 'a :: len word) = 
   503     replicate (len_of TYPE('a) - n) False @ 
   504     drop (len_of TYPE('a) - n) (to_bl w)"
   505   apply (rule nth_equalityI)
   506    apply simp
   507   apply (clarsimp simp add: to_bl_nth word_size)
   508   apply (simp add: word_size word_ops_nth_size)
   509   apply (auto simp add: word_size test_bit_bl nth_append nth_rev)
   510   done
   511 
   512 lemmas and_mask_mod_2p = 
   513   and_mask_bintr [unfolded word_number_of_alt no_bintr_alt]
   514 
   515 lemma and_mask_lt_2p: "uint (w AND mask n) < 2 ^ n"
   516   apply (simp add : and_mask_bintr no_bintr_alt)
   517   apply (rule xtr8)
   518    prefer 2
   519    apply (rule pos_mod_bound)
   520   apply auto
   521   done
   522 
   523 lemmas eq_mod_iff = trans [symmetric, OF int_mod_lem eq_sym_conv]
   524 
   525 lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
   526   apply (simp add: and_mask_bintr word_number_of_def)
   527   apply (simp add: word_ubin.inverse_norm)
   528   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
   529   apply (fast intro!: lt2p_lem)
   530   done
   531 
   532 lemma and_mask_dvd: "2 ^ n dvd uint w = (w AND mask n = 0)"
   533   apply (simp add: dvd_eq_mod_eq_0 and_mask_mod_2p)
   534   apply (simp add: word_uint.norm_eq_iff [symmetric] word_of_int_homs)
   535   apply (subst word_uint.norm_Rep [symmetric])
   536   apply (simp only: bintrunc_bintrunc_min bintrunc_mod2p [symmetric] min_def)
   537   apply auto
   538   done
   539 
   540 lemma and_mask_dvd_nat: "2 ^ n dvd unat w = (w AND mask n = 0)"
   541   apply (unfold unat_def)
   542   apply (rule trans [OF _ and_mask_dvd])
   543   apply (unfold dvd_def) 
   544   apply auto 
   545   apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
   546   apply (simp add : int_mult int_power)
   547   apply (simp add : nat_mult_distrib nat_power_eq)
   548   done
   549 
   550 lemma word_2p_lem: 
   551   "n < size w ==> w < 2 ^ n = (uint (w :: 'a :: len word) < 2 ^ n)"
   552   apply (unfold word_size word_less_alt word_number_of_alt)
   553   apply (clarsimp simp add: word_of_int_power_hom word_uint.eq_norm 
   554                             int_mod_eq'
   555                   simp del: word_of_int_bin)
   556   done
   557 
   558 lemma less_mask_eq: "x < 2 ^ n ==> x AND mask n = (x :: 'a :: len word)"
   559   apply (unfold word_less_alt word_number_of_alt)
   560   apply (clarsimp simp add: and_mask_mod_2p word_of_int_power_hom 
   561                             word_uint.eq_norm
   562                   simp del: word_of_int_bin)
   563   apply (drule xtr8 [rotated])
   564   apply (rule int_mod_le)
   565   apply (auto simp add : mod_pos_pos_trivial)
   566   done
   567 
   568 lemmas mask_eq_iff_w2p =
   569   trans [OF mask_eq_iff word_2p_lem [symmetric], standard]
   570 
   571 lemmas and_mask_less' = 
   572   iffD2 [OF word_2p_lem and_mask_lt_2p, simplified word_size, standard]
   573 
   574 lemma and_mask_less_size: "n < size x ==> x AND mask n < 2^n"
   575   unfolding word_size by (erule and_mask_less')
   576 
   577 lemma word_mod_2p_is_mask':
   578   "c = 2 ^ n ==> c > 0 ==> x mod c = (x :: 'a :: len word) AND mask n" 
   579   by (clarsimp simp add: word_mod_def uint_2p and_mask_mod_2p) 
   580 
   581 lemmas word_mod_2p_is_mask = refl [THEN word_mod_2p_is_mask'] 
   582 
   583 lemma mask_eqs:
   584   "(a AND mask n) + b AND mask n = a + b AND mask n"
   585   "a + (b AND mask n) AND mask n = a + b AND mask n"
   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 * (b AND mask n) AND mask n = a * b AND mask n"
   589   "(b AND mask n) * a AND mask n = b * a AND mask n"
   590   "(a AND mask n) + (b AND mask n) AND mask n = a + b AND mask n"
   591   "(a AND mask n) - (b AND mask n) AND mask n = a - b 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) AND mask n = - a AND mask n"
   594   "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
   595   "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
   596   using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
   597   by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
   598 
   599 lemma mask_power_eq:
   600   "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
   601   using word_of_int_Ex [where x=x]
   602   by (clarsimp simp: and_mask_wi word_of_int_power_hom bintr_ariths)
   603 
   604 
   605 subsubsection "Revcast"
   606 
   607 lemmas revcast_def' = revcast_def [simplified]
   608 lemmas revcast_def'' = revcast_def' [simplified word_size]
   609 lemmas revcast_no_def [simp] =
   610   revcast_def' [where w="number_of w", unfolded word_size, standard]
   611 
   612 lemma to_bl_revcast: 
   613   "to_bl (revcast w :: 'a :: len0 word) = 
   614    takefill False (len_of TYPE ('a)) (to_bl w)"
   615   apply (unfold revcast_def' word_size)
   616   apply (rule word_bl.Abs_inverse)
   617   apply simp
   618   done
   619 
   620 lemma revcast_rev_ucast': 
   621   "cs = [rc, uc] ==> rc = revcast (word_reverse w) ==> uc = ucast w ==> 
   622     rc = word_reverse uc"
   623   apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
   624   apply (clarsimp simp add : to_bl_of_bin takefill_bintrunc)
   625   apply (simp add : word_bl.Abs_inverse word_size)
   626   done
   627 
   628 lemmas revcast_rev_ucast = revcast_rev_ucast' [OF refl refl refl]
   629 
   630 lemmas revcast_ucast = revcast_rev_ucast
   631   [where w = "word_reverse w", simplified word_rev_rev, standard]
   632 
   633 lemmas ucast_revcast = revcast_rev_ucast [THEN word_rev_gal', standard]
   634 lemmas ucast_rev_revcast = revcast_ucast [THEN word_rev_gal', standard]
   635 
   636 
   637 -- "linking revcast and cast via shift"
   638 
   639 lemmas wsst_TYs = source_size target_size word_size
   640 
   641 lemma revcast_down_uu': 
   642   "rc = revcast ==> source_size rc = target_size rc + n ==> 
   643     rc (w :: 'a :: len word) = ucast (w >> n)"
   644   apply (simp add: revcast_def')
   645   apply (rule word_bl.Rep_inverse')
   646   apply (rule trans, rule ucast_down_drop)
   647    prefer 2
   648    apply (rule trans, rule drop_shiftr)
   649    apply (auto simp: takefill_alt wsst_TYs)
   650   done
   651 
   652 lemma revcast_down_us': 
   653   "rc = revcast ==> source_size rc = target_size rc + n ==> 
   654     rc (w :: 'a :: len word) = ucast (w >>> n)"
   655   apply (simp add: revcast_def')
   656   apply (rule word_bl.Rep_inverse')
   657   apply (rule trans, rule ucast_down_drop)
   658    prefer 2
   659    apply (rule trans, rule drop_sshiftr)
   660    apply (auto simp: takefill_alt wsst_TYs)
   661   done
   662 
   663 lemma revcast_down_su': 
   664   "rc = revcast ==> source_size rc = target_size rc + n ==> 
   665     rc (w :: 'a :: len word) = scast (w >> n)"
   666   apply (simp add: revcast_def')
   667   apply (rule word_bl.Rep_inverse')
   668   apply (rule trans, rule scast_down_drop)
   669    prefer 2
   670    apply (rule trans, rule drop_shiftr)
   671    apply (auto simp: takefill_alt wsst_TYs)
   672   done
   673 
   674 lemma revcast_down_ss': 
   675   "rc = revcast ==> source_size rc = target_size rc + n ==> 
   676     rc (w :: 'a :: len word) = scast (w >>> n)"
   677   apply (simp add: revcast_def')
   678   apply (rule word_bl.Rep_inverse')
   679   apply (rule trans, rule scast_down_drop)
   680    prefer 2
   681    apply (rule trans, rule drop_sshiftr)
   682    apply (auto simp: takefill_alt wsst_TYs)
   683   done
   684 
   685 lemmas revcast_down_uu = refl [THEN revcast_down_uu']
   686 lemmas revcast_down_us = refl [THEN revcast_down_us']
   687 lemmas revcast_down_su = refl [THEN revcast_down_su']
   688 lemmas revcast_down_ss = refl [THEN revcast_down_ss']
   689 
   690 lemma cast_down_rev: 
   691   "uc = ucast ==> source_size uc = target_size uc + n ==> 
   692     uc w = revcast ((w :: 'a :: len word) << n)"
   693   apply (unfold shiftl_rev)
   694   apply clarify
   695   apply (simp add: revcast_rev_ucast)
   696   apply (rule word_rev_gal')
   697   apply (rule trans [OF _ revcast_rev_ucast])
   698   apply (rule revcast_down_uu [symmetric])
   699   apply (auto simp add: wsst_TYs)
   700   done
   701 
   702 lemma revcast_up': 
   703   "rc = revcast ==> source_size rc + n = target_size rc ==> 
   704     rc w = (ucast w :: 'a :: len word) << n" 
   705   apply (simp add: revcast_def')
   706   apply (rule word_bl.Rep_inverse')
   707   apply (simp add: takefill_alt)
   708   apply (rule bl_shiftl [THEN trans])
   709   apply (subst ucast_up_app)
   710   apply (auto simp add: wsst_TYs)
   711   done
   712 
   713 lemmas revcast_up = refl [THEN revcast_up']
   714 
   715 lemmas rc1 = revcast_up [THEN 
   716   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
   717 lemmas rc2 = revcast_down_uu [THEN 
   718   revcast_rev_ucast [symmetric, THEN trans, THEN word_rev_gal, symmetric]]
   719 
   720 lemmas ucast_up =
   721  rc1 [simplified rev_shiftr [symmetric] revcast_ucast [symmetric]]
   722 lemmas ucast_down = 
   723   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
   724 
   725 
   726 subsubsection "Slices"
   727 
   728 lemmas slice1_no_bin [simp] =
   729   slice1_def [where w="number_of w", unfolded to_bl_no_bin, standard]
   730 
   731 lemmas slice_no_bin [simp] = 
   732    trans [OF slice_def [THEN meta_eq_to_obj_eq] 
   733              slice1_no_bin [THEN meta_eq_to_obj_eq], 
   734           unfolded word_size, standard]
   735 
   736 lemma slice1_0 [simp] : "slice1 n 0 = 0"
   737   unfolding slice1_def by (simp add : to_bl_0)
   738 
   739 lemma slice_0 [simp] : "slice n 0 = 0"
   740   unfolding slice_def by auto
   741 
   742 lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
   743   unfolding slice_def' slice1_def
   744   by (simp add : takefill_alt word_size)
   745 
   746 lemmas slice_take = slice_take' [unfolded word_size]
   747 
   748 -- "shiftr to a word of the same size is just slice, 
   749     slice is just shiftr then ucast"
   750 lemmas shiftr_slice = trans
   751   [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric], standard]
   752 
   753 lemma slice_shiftr: "slice n w = ucast (w >> n)"
   754   apply (unfold slice_take shiftr_bl)
   755   apply (rule ucast_of_bl_up [symmetric])
   756   apply (simp add: word_size)
   757   done
   758 
   759 lemma nth_slice: 
   760   "(slice n w :: 'a :: len0 word) !! m = 
   761    (w !! (m + n) & m < len_of TYPE ('a))"
   762   unfolding slice_shiftr 
   763   by (simp add : nth_ucast nth_shiftr)
   764 
   765 lemma slice1_down_alt': 
   766   "sl = slice1 n w ==> fs = size sl ==> fs + k = n ==> 
   767     to_bl sl = takefill False fs (drop k (to_bl w))"
   768   unfolding slice1_def word_size of_bl_def uint_bl
   769   by (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
   770 
   771 lemma slice1_up_alt': 
   772   "sl = slice1 n w ==> fs = size sl ==> fs = n + k ==> 
   773     to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
   774   apply (unfold slice1_def word_size of_bl_def uint_bl)
   775   apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop 
   776                         takefill_append [symmetric])
   777   apply (rule_tac f = "%k. takefill False (len_of TYPE('a))
   778     (replicate k False @ bin_to_bl (len_of TYPE('b)) (uint w))" in arg_cong)
   779   apply arith
   780   done
   781     
   782 lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
   783 lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
   784 lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
   785 lemmas slice1_up_alts = 
   786   le_add_diff_inverse [symmetric, THEN su1] 
   787   le_add_diff_inverse2 [symmetric, THEN su1]
   788 
   789 lemma ucast_slice1: "ucast w = slice1 (size w) w"
   790   unfolding slice1_def ucast_bl
   791   by (simp add : takefill_same' word_size)
   792 
   793 lemma ucast_slice: "ucast w = slice 0 w"
   794   unfolding slice_def by (simp add : ucast_slice1)
   795 
   796 lemmas slice_id = trans [OF ucast_slice [symmetric] ucast_id]
   797 
   798 lemma revcast_slice1': 
   799   "rc = revcast w ==> slice1 (size rc) w = rc"
   800   unfolding slice1_def revcast_def' by (simp add : word_size)
   801 
   802 lemmas revcast_slice1 = refl [THEN revcast_slice1']
   803 
   804 lemma slice1_tf_tf': 
   805   "to_bl (slice1 n w :: 'a :: len0 word) = 
   806    rev (takefill False (len_of TYPE('a)) (rev (takefill False n (to_bl w))))"
   807   unfolding slice1_def by (rule word_rev_tf)
   808 
   809 lemmas slice1_tf_tf = slice1_tf_tf'
   810   [THEN word_bl.Rep_inverse', symmetric, standard]
   811 
   812 lemma rev_slice1:
   813   "n + k = len_of TYPE('a) + len_of TYPE('b) \<Longrightarrow> 
   814   slice1 n (word_reverse w :: 'b :: len0 word) = 
   815   word_reverse (slice1 k w :: 'a :: len0 word)"
   816   apply (unfold word_reverse_def slice1_tf_tf)
   817   apply (rule word_bl.Rep_inverse')
   818   apply (rule rev_swap [THEN iffD1])
   819   apply (rule trans [symmetric])
   820   apply (rule tf_rev)
   821    apply (simp add: word_bl.Abs_inverse)
   822   apply (simp add: word_bl.Abs_inverse)
   823   done
   824 
   825 lemma rev_slice': 
   826   "res = slice n (word_reverse w) ==> n + k + size res = size w ==> 
   827     res = word_reverse (slice k w)"
   828   apply (unfold slice_def word_size)
   829   apply clarify
   830   apply (rule rev_slice1)
   831   apply arith
   832   done
   833 
   834 lemmas rev_slice = refl [THEN rev_slice', unfolded word_size]
   835 
   836 lemmas sym_notr = 
   837   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]
   838 
   839 -- {* problem posed by TPHOLs referee:
   840       criterion for overflow of addition of signed integers *}
   841 
   842 lemma sofl_test:
   843   "(sint (x :: 'a :: len word) + sint y = sint (x + y)) = 
   844      ((((x+y) XOR x) AND ((x+y) XOR y)) >> (size x - 1) = 0)"
   845   apply (unfold word_size)
   846   apply (cases "len_of TYPE('a)", simp) 
   847   apply (subst msb_shift [THEN sym_notr])
   848   apply (simp add: word_ops_msb)
   849   apply (simp add: word_msb_sint)
   850   apply safe
   851        apply simp_all
   852      apply (unfold sint_word_ariths)
   853      apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
   854      apply safe
   855         apply (insert sint_range' [where x=x])
   856         apply (insert sint_range' [where x=y])
   857         defer 
   858         apply (simp (no_asm), arith)
   859        apply (simp (no_asm), arith)
   860       defer
   861       defer
   862       apply (simp (no_asm), arith)
   863      apply (simp (no_asm), arith)
   864     apply (rule notI [THEN notnotD],
   865            drule leI not_leE,
   866            drule sbintrunc_inc sbintrunc_dec,      
   867            simp)+
   868   done
   869 
   870 
   871 subsection "Split and cat"
   872 
   873 lemmas word_split_bin' = word_split_def [THEN meta_eq_to_obj_eq, standard]
   874 lemmas word_cat_bin' = word_cat_def [THEN meta_eq_to_obj_eq, standard]
   875 
   876 lemma word_rsplit_no:
   877   "(word_rsplit (number_of bin :: 'b :: len0 word) :: 'a word list) = 
   878     map number_of (bin_rsplit (len_of TYPE('a :: len)) 
   879       (len_of TYPE('b), bintrunc (len_of TYPE('b)) bin))"
   880   apply (unfold word_rsplit_def word_no_wi)
   881   apply (simp add: word_ubin.eq_norm)
   882   done
   883 
   884 lemmas word_rsplit_no_cl [simp] = word_rsplit_no
   885   [unfolded bin_rsplitl_def bin_rsplit_l [symmetric]]
   886 
   887 lemma test_bit_cat:
   888   "wc = word_cat a b ==> wc !! n = (n < size wc & 
   889     (if n < size b then b !! n else a !! (n - size b)))"
   890   apply (unfold word_cat_bin' test_bit_bin)
   891   apply (auto simp add : word_ubin.eq_norm nth_bintr bin_nth_cat word_size)
   892   apply (erule bin_nth_uint_imp)
   893   done
   894 
   895 lemma word_cat_bl: "word_cat a b = of_bl (to_bl a @ to_bl b)"
   896   apply (unfold of_bl_def to_bl_def word_cat_bin')
   897   apply (simp add: bl_to_bin_app_cat)
   898   done
   899 
   900 lemma of_bl_append:
   901   "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
   902   apply (unfold of_bl_def)
   903   apply (simp add: bl_to_bin_app_cat bin_cat_num)
   904   apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
   905   done
   906 
   907 lemma of_bl_False [simp]:
   908   "of_bl (False#xs) = of_bl xs"
   909   by (rule word_eqI)
   910      (auto simp add: test_bit_of_bl nth_append)
   911 
   912 lemma of_bl_True: 
   913   "(of_bl (True#xs)::'a::len word) = 2^length xs + of_bl xs"
   914   by (subst of_bl_append [where xs="[True]", simplified])
   915      (simp add: word_1_bl)
   916 
   917 lemma of_bl_Cons:
   918   "of_bl (x#xs) = of_bool x * 2^length xs + of_bl xs"
   919   by (cases x) (simp_all add: of_bl_True)
   920 
   921 lemma split_uint_lem: "bin_split n (uint (w :: 'a :: len0 word)) = (a, b) ==> 
   922   a = bintrunc (len_of TYPE('a) - n) a & b = bintrunc (len_of TYPE('a)) b"
   923   apply (frule word_ubin.norm_Rep [THEN ssubst])
   924   apply (drule bin_split_trunc1)
   925   apply (drule sym [THEN trans])
   926   apply assumption
   927   apply safe
   928   done
   929 
   930 lemma word_split_bl': 
   931   "std = size c - size b ==> (word_split c = (a, b)) ==> 
   932     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c)))"
   933   apply (unfold word_split_bin')
   934   apply safe
   935    defer
   936    apply (clarsimp split: prod.splits)
   937    apply (drule word_ubin.norm_Rep [THEN ssubst])
   938    apply (drule split_bintrunc)
   939    apply (simp add : of_bl_def bl2bin_drop word_size
   940        word_ubin.norm_eq_iff [symmetric] min_def del : word_ubin.norm_Rep)    
   941   apply (clarsimp split: prod.splits)
   942   apply (frule split_uint_lem [THEN conjunct1])
   943   apply (unfold word_size)
   944   apply (cases "len_of TYPE('a) >= len_of TYPE('b)")
   945    defer
   946    apply (simp add: word_0_bl word_0_wi_Pls)
   947   apply (simp add : of_bl_def to_bl_def)
   948   apply (subst bin_split_take1 [symmetric])
   949     prefer 2
   950     apply assumption
   951    apply simp
   952   apply (erule thin_rl)
   953   apply (erule arg_cong [THEN trans])
   954   apply (simp add : word_ubin.norm_eq_iff [symmetric])
   955   done
   956 
   957 lemma word_split_bl: "std = size c - size b ==> 
   958     (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
   959     word_split c = (a, b)"
   960   apply (rule iffI)
   961    defer
   962    apply (erule (1) word_split_bl')
   963   apply (case_tac "word_split c")
   964   apply (auto simp add : word_size)
   965   apply (frule word_split_bl' [rotated])
   966   apply (auto simp add : word_size)
   967   done
   968 
   969 lemma word_split_bl_eq:
   970    "(word_split (c::'a::len word) :: ('c :: len0 word * 'd :: len0 word)) =
   971       (of_bl (take (len_of TYPE('a::len) - len_of TYPE('d::len0)) (to_bl c)),
   972        of_bl (drop (len_of TYPE('a) - len_of TYPE('d)) (to_bl c)))"
   973   apply (rule word_split_bl [THEN iffD1])
   974   apply (unfold word_size)
   975   apply (rule refl conjI)+
   976   done
   977 
   978 -- "keep quantifiers for use in simplification"
   979 lemma test_bit_split':
   980   "word_split c = (a, b) --> (ALL n m. b !! n = (n < size b & c !! n) & 
   981     a !! m = (m < size a & c !! (m + size b)))"
   982   apply (unfold word_split_bin' test_bit_bin)
   983   apply (clarify)
   984   apply (clarsimp simp: word_ubin.eq_norm nth_bintr word_size split: prod.splits)
   985   apply (drule bin_nth_split)
   986   apply safe
   987        apply (simp_all add: add_commute)
   988    apply (erule bin_nth_uint_imp)+
   989   done
   990 
   991 lemmas test_bit_split = 
   992   test_bit_split' [THEN mp, simplified all_simps, standard]
   993 
   994 lemma test_bit_split_eq: "word_split c = (a, b) <-> 
   995   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
   996     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   997   apply (rule_tac iffI)
   998    apply (rule_tac conjI)
   999     apply (erule test_bit_split [THEN conjunct1])
  1000    apply (erule test_bit_split [THEN conjunct2])
  1001   apply (case_tac "word_split c")
  1002   apply (frule test_bit_split)
  1003   apply (erule trans)
  1004   apply (fastsimp intro ! : word_eqI simp add : word_size)
  1005   done
  1006 
  1007 -- {* this odd result is analogous to @{text "ucast_id"}, 
  1008       result to the length given by the result type *}
  1009 
  1010 lemma word_cat_id: "word_cat a b = b"
  1011   unfolding word_cat_bin' by (simp add: word_ubin.inverse_norm)
  1012 
  1013 -- "limited hom result"
  1014 lemma word_cat_hom:
  1015   "len_of TYPE('a::len0) <= len_of TYPE('b::len0) + len_of TYPE ('c::len0)
  1016   ==>
  1017   (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) = 
  1018   word_of_int (bin_cat w (size b) (uint b))"
  1019   apply (unfold word_cat_def word_size) 
  1020   apply (clarsimp simp add : word_ubin.norm_eq_iff [symmetric]
  1021       word_ubin.eq_norm bintr_cat min_def)
  1022   apply arith
  1023   done
  1024 
  1025 lemma word_cat_split_alt:
  1026   "size w <= size u + size v ==> word_split w = (u, v) ==> word_cat u v = w"
  1027   apply (rule word_eqI)
  1028   apply (drule test_bit_split)
  1029   apply (clarsimp simp add : test_bit_cat word_size)
  1030   apply safe
  1031   apply arith
  1032   done
  1033 
  1034 lemmas word_cat_split_size = 
  1035   sym [THEN [2] word_cat_split_alt [symmetric], standard]
  1036 
  1037 
  1038 subsubsection "Split and slice"
  1039 
  1040 lemma split_slices: 
  1041   "word_split w = (u, v) ==> u = slice (size v) w & v = slice 0 w"
  1042   apply (drule test_bit_split)
  1043   apply (rule conjI)
  1044    apply (rule word_eqI, clarsimp simp: nth_slice word_size)+
  1045   done
  1046 
  1047 lemma slice_cat1':
  1048   "wc = word_cat a b ==> size wc >= size a + size b ==> slice (size b) wc = a"
  1049   apply safe
  1050   apply (rule word_eqI)
  1051   apply (simp add: nth_slice test_bit_cat word_size)
  1052   done
  1053 
  1054 lemmas slice_cat1 = refl [THEN slice_cat1']
  1055 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
  1056 
  1057 lemma cat_slices:
  1058   "a = slice n c ==> b = slice 0 c ==> n = size b ==>
  1059     size a + size b >= size c ==> word_cat a b = c"
  1060   apply safe
  1061   apply (rule word_eqI)
  1062   apply (simp add: nth_slice test_bit_cat word_size)
  1063   apply safe
  1064   apply arith
  1065   done
  1066 
  1067 lemma word_split_cat_alt:
  1068   "w = word_cat u v ==> size u + size v <= size w ==> word_split w = (u, v)"
  1069   apply (case_tac "word_split ?w")
  1070   apply (rule trans, assumption)
  1071   apply (drule test_bit_split)
  1072   apply safe
  1073    apply (rule word_eqI, clarsimp simp: test_bit_cat word_size)+
  1074   done
  1075 
  1076 lemmas word_cat_bl_no_bin [simp] =
  1077   word_cat_bl [where a="number_of a" 
  1078                  and b="number_of b", 
  1079                unfolded to_bl_no_bin, standard]
  1080 
  1081 lemmas word_split_bl_no_bin [simp] =
  1082   word_split_bl_eq [where c="number_of c", unfolded to_bl_no_bin, standard]
  1083 
  1084 -- {* this odd result arises from the fact that the statement of the
  1085       result implies that the decoded words are of the same type, 
  1086       and therefore of the same length, as the original word *}
  1087 
  1088 lemma word_rsplit_same: "word_rsplit w = [w]"
  1089   unfolding word_rsplit_def by (simp add : bin_rsplit_all)
  1090 
  1091 lemma word_rsplit_empty_iff_size:
  1092   "(word_rsplit w = []) = (size w = 0)" 
  1093   unfolding word_rsplit_def bin_rsplit_def word_size
  1094   by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
  1095 
  1096 lemma test_bit_rsplit:
  1097   "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
  1098     k < length sw ==> (rev sw ! k) !! m = (w !! (k * size (hd sw) + m))"
  1099   apply (unfold word_rsplit_def word_test_bit_def)
  1100   apply (rule trans)
  1101    apply (rule_tac f = "%x. bin_nth x m" in arg_cong)
  1102    apply (rule nth_map [symmetric])
  1103    apply simp
  1104   apply (rule bin_nth_rsplit)
  1105      apply simp_all
  1106   apply (simp add : word_size rev_map map_compose [symmetric])
  1107   apply (rule trans)
  1108    defer
  1109    apply (rule map_ident [THEN fun_cong])
  1110   apply (rule refl [THEN map_cong])
  1111   apply (simp add : word_ubin.eq_norm)
  1112   apply (erule bin_rsplit_size_sign [OF len_gt_0 refl])
  1113   done
  1114 
  1115 lemma word_rcat_bl: "word_rcat wl == of_bl (concat (map to_bl wl))"
  1116   unfolding word_rcat_def to_bl_def' of_bl_def
  1117   by (clarsimp simp add : bin_rcat_bl map_compose)
  1118 
  1119 lemma size_rcat_lem':
  1120   "size (concat (map to_bl wl)) = length wl * size (hd wl)"
  1121   unfolding word_size by (induct wl) auto
  1122 
  1123 lemmas size_rcat_lem = size_rcat_lem' [unfolded word_size]
  1124 
  1125 lemmas td_gal_lt_len = len_gt_0 [THEN td_gal_lt, standard]
  1126 
  1127 lemma nth_rcat_lem' [rule_format] :
  1128   "sw = size (hd wl  :: 'a :: len word) ==> (ALL n. n < size wl * sw --> 
  1129     rev (concat (map to_bl wl)) ! n = 
  1130     rev (to_bl (rev wl ! (n div sw))) ! (n mod sw))"
  1131   apply (unfold word_size)
  1132   apply (induct "wl")
  1133    apply clarsimp
  1134   apply (clarsimp simp add : nth_append size_rcat_lem)
  1135   apply (simp (no_asm_use) only:  mult_Suc [symmetric] 
  1136          td_gal_lt_len less_Suc_eq_le mod_div_equality')
  1137   apply clarsimp
  1138   done
  1139 
  1140 lemmas nth_rcat_lem = refl [THEN nth_rcat_lem', unfolded word_size]
  1141 
  1142 lemma test_bit_rcat:
  1143   "sw = size (hd wl :: 'a :: len word) ==> rc = word_rcat wl ==> rc !! n = 
  1144     (n < size rc & n div sw < size wl & (rev wl) ! (n div sw) !! (n mod sw))"
  1145   apply (unfold word_rcat_bl word_size)
  1146   apply (clarsimp simp add : 
  1147     test_bit_of_bl size_rcat_lem word_size td_gal_lt_len)
  1148   apply safe
  1149    apply (auto simp add : 
  1150     test_bit_bl word_size td_gal_lt_len [THEN iffD2, THEN nth_rcat_lem])
  1151   done
  1152 
  1153 lemma foldl_eq_foldr [rule_format] :
  1154   "ALL x. foldl op + x xs = foldr op + (x # xs) (0 :: 'a :: comm_monoid_add)" 
  1155   by (induct xs) (auto simp add : add_assoc)
  1156 
  1157 lemmas test_bit_cong = arg_cong [where f = "test_bit", THEN fun_cong]
  1158 
  1159 lemmas test_bit_rsplit_alt = 
  1160   trans [OF nth_rev_alt [THEN test_bit_cong] 
  1161   test_bit_rsplit [OF refl asm_rl diff_Suc_less]]
  1162 
  1163 -- "lazy way of expressing that u and v, and su and sv, have same types"
  1164 lemma word_rsplit_len_indep':
  1165   "[u,v] = p ==> [su,sv] = q ==> word_rsplit u = su ==> 
  1166     word_rsplit v = sv ==> length su = length sv"
  1167   apply (unfold word_rsplit_def)
  1168   apply (auto simp add : bin_rsplit_len_indep)
  1169   done
  1170 
  1171 lemmas word_rsplit_len_indep = word_rsplit_len_indep' [OF refl refl refl refl]
  1172 
  1173 lemma length_word_rsplit_size: 
  1174   "n = len_of TYPE ('a :: len) ==> 
  1175     (length (word_rsplit w :: 'a word list) <= m) = (size w <= m * n)"
  1176   apply (unfold word_rsplit_def word_size)
  1177   apply (clarsimp simp add : bin_rsplit_len_le)
  1178   done
  1179 
  1180 lemmas length_word_rsplit_lt_size = 
  1181   length_word_rsplit_size [unfolded Not_eq_iff linorder_not_less [symmetric]]
  1182 
  1183 lemma length_word_rsplit_exp_size: 
  1184   "n = len_of TYPE ('a :: len) ==> 
  1185     length (word_rsplit w :: 'a word list) = (size w + n - 1) div n"
  1186   unfolding word_rsplit_def by (clarsimp simp add : word_size bin_rsplit_len)
  1187 
  1188 lemma length_word_rsplit_even_size: 
  1189   "n = len_of TYPE ('a :: len) ==> size w = m * n ==> 
  1190     length (word_rsplit w :: 'a word list) = m"
  1191   by (clarsimp simp add : length_word_rsplit_exp_size given_quot_alt)
  1192 
  1193 lemmas length_word_rsplit_exp_size' = refl [THEN length_word_rsplit_exp_size]
  1194 
  1195 (* alternative proof of word_rcat_rsplit *)
  1196 lemmas tdle = iffD2 [OF split_div_lemma refl, THEN conjunct1] 
  1197 lemmas dtle = xtr4 [OF tdle mult_commute]
  1198 
  1199 lemma word_rcat_rsplit: "word_rcat (word_rsplit w) = w"
  1200   apply (rule word_eqI)
  1201   apply (clarsimp simp add : test_bit_rcat word_size)
  1202   apply (subst refl [THEN test_bit_rsplit])
  1203     apply (simp_all add: word_size 
  1204       refl [THEN length_word_rsplit_size [simplified not_less [symmetric], simplified]])
  1205    apply safe
  1206    apply (erule xtr7, rule len_gt_0 [THEN dtle])+
  1207   done
  1208 
  1209 lemma size_word_rsplit_rcat_size':
  1210   "word_rcat (ws :: 'a :: len word list) = frcw ==> 
  1211     size frcw = length ws * len_of TYPE ('a) ==> 
  1212     size (hd [word_rsplit frcw, ws]) = size ws" 
  1213   apply (clarsimp simp add : word_size length_word_rsplit_exp_size')
  1214   apply (fast intro: given_quot_alt)
  1215   done
  1216 
  1217 lemmas size_word_rsplit_rcat_size = 
  1218   size_word_rsplit_rcat_size' [simplified]
  1219 
  1220 lemma msrevs:
  1221   fixes n::nat
  1222   shows "0 < n \<Longrightarrow> (k * n + m) div n = m div n + k"
  1223   and   "(k * n + m) mod n = m mod n"
  1224   by (auto simp: add_commute)
  1225 
  1226 lemma word_rsplit_rcat_size':
  1227   "word_rcat (ws :: 'a :: len word list) = frcw ==> 
  1228     size frcw = length ws * len_of TYPE ('a) ==> word_rsplit frcw = ws" 
  1229   apply (frule size_word_rsplit_rcat_size, assumption)
  1230   apply (clarsimp simp add : word_size)
  1231   apply (rule nth_equalityI, assumption)
  1232   apply clarsimp
  1233   apply (rule word_eqI)
  1234   apply (rule trans)
  1235    apply (rule test_bit_rsplit_alt)
  1236      apply (clarsimp simp: word_size)+
  1237   apply (rule trans)
  1238   apply (rule test_bit_rcat [OF refl refl])
  1239   apply (simp add : word_size msrevs)
  1240   apply (subst nth_rev)
  1241    apply arith
  1242   apply (simp add : le0 [THEN [2] xtr7, THEN diff_Suc_less])
  1243   apply safe
  1244   apply (simp add : diff_mult_distrib)
  1245   apply (rule mpl_lem)
  1246   apply (cases "size ws")
  1247    apply simp_all
  1248   done
  1249 
  1250 lemmas word_rsplit_rcat_size = refl [THEN word_rsplit_rcat_size']
  1251 
  1252 
  1253 subsection "Rotation"
  1254 
  1255 lemmas rotater_0' [simp] = rotater_def [where n = "0", simplified]
  1256 
  1257 lemmas word_rot_defs = word_roti_def word_rotr_def word_rotl_def
  1258 
  1259 lemma rotate_eq_mod: 
  1260   "m mod length xs = n mod length xs ==> rotate m xs = rotate n xs"
  1261   apply (rule box_equals)
  1262     defer
  1263     apply (rule rotate_conv_mod [symmetric])+
  1264   apply simp
  1265   done
  1266 
  1267 lemmas rotate_eqs [standard] = 
  1268   trans [OF rotate0 [THEN fun_cong] id_apply]
  1269   rotate_rotate [symmetric] 
  1270   rotate_id 
  1271   rotate_conv_mod 
  1272   rotate_eq_mod
  1273 
  1274 
  1275 subsubsection "Rotation of list to right"
  1276 
  1277 lemma rotate1_rl': "rotater1 (l @ [a]) = a # l"
  1278   unfolding rotater1_def by (cases l) auto
  1279 
  1280 lemma rotate1_rl [simp] : "rotater1 (rotate1 l) = l"
  1281   apply (unfold rotater1_def)
  1282   apply (cases "l")
  1283   apply (case_tac [2] "list")
  1284   apply auto
  1285   done
  1286 
  1287 lemma rotate1_lr [simp] : "rotate1 (rotater1 l) = l"
  1288   unfolding rotater1_def by (cases l) auto
  1289 
  1290 lemma rotater1_rev': "rotater1 (rev xs) = rev (rotate1 xs)"
  1291   apply (cases "xs")
  1292   apply (simp add : rotater1_def)
  1293   apply (simp add : rotate1_rl')
  1294   done
  1295   
  1296 lemma rotater_rev': "rotater n (rev xs) = rev (rotate n xs)"
  1297   unfolding rotater_def by (induct n) (auto intro: rotater1_rev')
  1298 
  1299 lemmas rotater_rev = rotater_rev' [where xs = "rev ys", simplified, standard]
  1300 
  1301 lemma rotater_drop_take: 
  1302   "rotater n xs = 
  1303    drop (length xs - n mod length xs) xs @
  1304    take (length xs - n mod length xs) xs"
  1305   by (clarsimp simp add : rotater_rev rotate_drop_take rev_take rev_drop)
  1306 
  1307 lemma rotater_Suc [simp] : 
  1308   "rotater (Suc n) xs = rotater1 (rotater n xs)"
  1309   unfolding rotater_def by auto
  1310 
  1311 lemma rotate_inv_plus [rule_format] :
  1312   "ALL k. k = m + n --> rotater k (rotate n xs) = rotater m xs & 
  1313     rotate k (rotater n xs) = rotate m xs & 
  1314     rotater n (rotate k xs) = rotate m xs & 
  1315     rotate n (rotater k xs) = rotater m xs"
  1316   unfolding rotater_def rotate_def
  1317   by (induct n) (auto intro: funpow_swap1 [THEN trans])
  1318   
  1319 lemmas rotate_inv_rel = le_add_diff_inverse2 [symmetric, THEN rotate_inv_plus]
  1320 
  1321 lemmas rotate_inv_eq = order_refl [THEN rotate_inv_rel, simplified]
  1322 
  1323 lemmas rotate_lr [simp] = rotate_inv_eq [THEN conjunct1, standard]
  1324 lemmas rotate_rl [simp] =
  1325   rotate_inv_eq [THEN conjunct2, THEN conjunct1, standard]
  1326 
  1327 lemma rotate_gal: "(rotater n xs = ys) = (rotate n ys = xs)"
  1328   by auto
  1329 
  1330 lemma rotate_gal': "(ys = rotater n xs) = (xs = rotate n ys)"
  1331   by auto
  1332 
  1333 lemma length_rotater [simp]: 
  1334   "length (rotater n xs) = length xs"
  1335   by (simp add : rotater_rev)
  1336 
  1337 lemmas rrs0 = rotate_eqs [THEN restrict_to_left, 
  1338   simplified rotate_gal [symmetric] rotate_gal' [symmetric], standard]
  1339 lemmas rrs1 = rrs0 [THEN refl [THEN rev_iffD1]]
  1340 lemmas rotater_eqs = rrs1 [simplified length_rotater, standard]
  1341 lemmas rotater_0 = rotater_eqs (1)
  1342 lemmas rotater_add = rotater_eqs (2)
  1343 
  1344 
  1345 subsubsection "map, map2, commuting with rotate(r)"
  1346 
  1347 lemma last_map: "xs ~= [] ==> last (map f xs) = f (last xs)"
  1348   by (induct xs) auto
  1349 
  1350 lemma butlast_map:
  1351   "xs ~= [] ==> butlast (map f xs) = map f (butlast xs)"
  1352   by (induct xs) auto
  1353 
  1354 lemma rotater1_map: "rotater1 (map f xs) = map f (rotater1 xs)" 
  1355   unfolding rotater1_def
  1356   by (cases xs) (auto simp add: last_map butlast_map)
  1357 
  1358 lemma rotater_map:
  1359   "rotater n (map f xs) = map f (rotater n xs)" 
  1360   unfolding rotater_def
  1361   by (induct n) (auto simp add : rotater1_map)
  1362 
  1363 lemma but_last_zip [rule_format] :
  1364   "ALL ys. length xs = length ys --> xs ~= [] --> 
  1365     last (zip xs ys) = (last xs, last ys) & 
  1366     butlast (zip xs ys) = zip (butlast xs) (butlast ys)" 
  1367   apply (induct "xs")
  1368   apply auto
  1369      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  1370   done
  1371 
  1372 lemma but_last_map2 [rule_format] :
  1373   "ALL ys. length xs = length ys --> xs ~= [] --> 
  1374     last (map2 f xs ys) = f (last xs) (last ys) & 
  1375     butlast (map2 f xs ys) = map2 f (butlast xs) (butlast ys)" 
  1376   apply (induct "xs")
  1377   apply auto
  1378      apply (unfold map2_def)
  1379      apply ((case_tac ys, auto simp: neq_Nil_conv)[1])+
  1380   done
  1381 
  1382 lemma rotater1_zip:
  1383   "length xs = length ys ==> 
  1384     rotater1 (zip xs ys) = zip (rotater1 xs) (rotater1 ys)" 
  1385   apply (unfold rotater1_def)
  1386   apply (cases "xs")
  1387    apply auto
  1388    apply ((case_tac ys, auto simp: neq_Nil_conv but_last_zip)[1])+
  1389   done
  1390 
  1391 lemma rotater1_map2:
  1392   "length xs = length ys ==> 
  1393     rotater1 (map2 f xs ys) = map2 f (rotater1 xs) (rotater1 ys)" 
  1394   unfolding map2_def by (simp add: rotater1_map rotater1_zip)
  1395 
  1396 lemmas lrth = 
  1397   box_equals [OF asm_rl length_rotater [symmetric] 
  1398                  length_rotater [symmetric], 
  1399               THEN rotater1_map2]
  1400 
  1401 lemma rotater_map2: 
  1402   "length xs = length ys ==> 
  1403     rotater n (map2 f xs ys) = map2 f (rotater n xs) (rotater n ys)" 
  1404   by (induct n) (auto intro!: lrth)
  1405 
  1406 lemma rotate1_map2:
  1407   "length xs = length ys ==> 
  1408     rotate1 (map2 f xs ys) = map2 f (rotate1 xs) (rotate1 ys)" 
  1409   apply (unfold map2_def)
  1410   apply (cases xs)
  1411    apply (cases ys, auto simp add : rotate1_def)+
  1412   done
  1413 
  1414 lemmas lth = box_equals [OF asm_rl length_rotate [symmetric] 
  1415   length_rotate [symmetric], THEN rotate1_map2]
  1416 
  1417 lemma rotate_map2: 
  1418   "length xs = length ys ==> 
  1419     rotate n (map2 f xs ys) = map2 f (rotate n xs) (rotate n ys)" 
  1420   by (induct n) (auto intro!: lth)
  1421 
  1422 
  1423 -- "corresponding equalities for word rotation"
  1424 
  1425 lemma to_bl_rotl: 
  1426   "to_bl (word_rotl n w) = rotate n (to_bl w)"
  1427   by (simp add: word_bl.Abs_inverse' word_rotl_def)
  1428 
  1429 lemmas blrs0 = rotate_eqs [THEN to_bl_rotl [THEN trans]]
  1430 
  1431 lemmas word_rotl_eqs =
  1432   blrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotl [symmetric]]
  1433 
  1434 lemma to_bl_rotr: 
  1435   "to_bl (word_rotr n w) = rotater n (to_bl w)"
  1436   by (simp add: word_bl.Abs_inverse' word_rotr_def)
  1437 
  1438 lemmas brrs0 = rotater_eqs [THEN to_bl_rotr [THEN trans]]
  1439 
  1440 lemmas word_rotr_eqs =
  1441   brrs0 [simplified word_bl.Rep' word_bl.Rep_inject to_bl_rotr [symmetric]]
  1442 
  1443 declare word_rotr_eqs (1) [simp]
  1444 declare word_rotl_eqs (1) [simp]
  1445 
  1446 lemma
  1447   word_rot_rl [simp]:
  1448   "word_rotl k (word_rotr k v) = v" and
  1449   word_rot_lr [simp]:
  1450   "word_rotr k (word_rotl k v) = v"
  1451   by (auto simp add: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric])
  1452 
  1453 lemma
  1454   word_rot_gal:
  1455   "(word_rotr n v = w) = (word_rotl n w = v)" and
  1456   word_rot_gal':
  1457   "(w = word_rotr n v) = (v = word_rotl n w)"
  1458   by (auto simp: to_bl_rotr to_bl_rotl word_bl.Rep_inject [symmetric] 
  1459            dest: sym)
  1460 
  1461 lemma word_rotr_rev:
  1462   "word_rotr n w = word_reverse (word_rotl n (word_reverse w))"
  1463   by (simp add: word_bl.Rep_inject [symmetric] to_bl_word_rev
  1464                 to_bl_rotr to_bl_rotl rotater_rev)
  1465   
  1466 lemma word_roti_0 [simp]: "word_roti 0 w = w"
  1467   by (unfold word_rot_defs) auto
  1468 
  1469 lemmas abl_cong = arg_cong [where f = "of_bl"]
  1470 
  1471 lemma word_roti_add: 
  1472   "word_roti (m + n) w = word_roti m (word_roti n w)"
  1473 proof -
  1474   have rotater_eq_lem: 
  1475     "\<And>m n xs. m = n ==> rotater m xs = rotater n xs"
  1476     by auto
  1477 
  1478   have rotate_eq_lem: 
  1479     "\<And>m n xs. m = n ==> rotate m xs = rotate n xs"
  1480     by auto
  1481 
  1482   note rpts [symmetric, standard] = 
  1483     rotate_inv_plus [THEN conjunct1]
  1484     rotate_inv_plus [THEN conjunct2, THEN conjunct1]
  1485     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct1]
  1486     rotate_inv_plus [THEN conjunct2, THEN conjunct2, THEN conjunct2]
  1487 
  1488   note rrp = trans [symmetric, OF rotate_rotate rotate_eq_lem]
  1489   note rrrp = trans [symmetric, OF rotater_add [symmetric] rotater_eq_lem]
  1490 
  1491   show ?thesis
  1492   apply (unfold word_rot_defs)
  1493   apply (simp only: split: split_if)
  1494   apply (safe intro!: abl_cong)
  1495   apply (simp_all only: to_bl_rotl [THEN word_bl.Rep_inverse'] 
  1496                     to_bl_rotl
  1497                     to_bl_rotr [THEN word_bl.Rep_inverse']
  1498                     to_bl_rotr)
  1499   apply (rule rrp rrrp rpts,
  1500          simp add: nat_add_distrib [symmetric] 
  1501                    nat_diff_distrib [symmetric])+
  1502   done
  1503 qed
  1504     
  1505 lemma word_roti_conv_mod': "word_roti n w = word_roti (n mod int (size w)) w"
  1506   apply (unfold word_rot_defs)
  1507   apply (cut_tac y="size w" in gt_or_eq_0)
  1508   apply (erule disjE)
  1509    apply simp_all
  1510   apply (safe intro!: abl_cong)
  1511    apply (rule rotater_eqs)
  1512    apply (simp add: word_size nat_mod_distrib)
  1513   apply (simp add: rotater_add [symmetric] rotate_gal [symmetric])
  1514   apply (rule rotater_eqs)
  1515   apply (simp add: word_size nat_mod_distrib)
  1516   apply (rule int_eq_0_conv [THEN iffD1])
  1517   apply (simp only: zmod_int zadd_int [symmetric])
  1518   apply (simp add: rdmods)
  1519   done
  1520 
  1521 lemmas word_roti_conv_mod = word_roti_conv_mod' [unfolded word_size]
  1522 
  1523 
  1524 subsubsection "Word rotation commutes with bit-wise operations"
  1525 
  1526 (* using locale to not pollute lemma namespace *)
  1527 locale word_rotate 
  1528 
  1529 context word_rotate
  1530 begin
  1531 
  1532 lemmas word_rot_defs' = to_bl_rotl to_bl_rotr
  1533 
  1534 lemmas blwl_syms [symmetric] = bl_word_not bl_word_and bl_word_or bl_word_xor
  1535 
  1536 lemmas lbl_lbl = trans [OF word_bl.Rep' word_bl.Rep' [symmetric]]
  1537 
  1538 lemmas ths_map2 [OF lbl_lbl] = rotate_map2 rotater_map2
  1539 
  1540 lemmas ths_map [where xs = "to_bl v", standard] = rotate_map rotater_map
  1541 
  1542 lemmas th1s [simplified word_rot_defs' [symmetric]] = ths_map2 ths_map
  1543 
  1544 lemma word_rot_logs:
  1545   "word_rotl n (NOT v) = NOT word_rotl n v"
  1546   "word_rotr n (NOT v) = NOT word_rotr n v"
  1547   "word_rotl n (x AND y) = word_rotl n x AND word_rotl n y"
  1548   "word_rotr n (x AND y) = word_rotr n x AND word_rotr n y"
  1549   "word_rotl n (x OR y) = word_rotl n x OR word_rotl n y"
  1550   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
  1551   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
  1552   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"  
  1553   by (rule word_bl.Rep_eqD,
  1554       rule word_rot_defs' [THEN trans],
  1555       simp only: blwl_syms [symmetric],
  1556       rule th1s [THEN trans], 
  1557       rule refl)+
  1558 end
  1559 
  1560 lemmas word_rot_logs = word_rotate.word_rot_logs
  1561 
  1562 lemmas bl_word_rotl_dt = trans [OF to_bl_rotl rotate_drop_take,
  1563   simplified word_bl.Rep', standard]
  1564 
  1565 lemmas bl_word_rotr_dt = trans [OF to_bl_rotr rotater_drop_take,
  1566   simplified word_bl.Rep', standard]
  1567 
  1568 lemma bl_word_roti_dt': 
  1569   "n = nat ((- i) mod int (size (w :: 'a :: len word))) ==> 
  1570     to_bl (word_roti i w) = drop n (to_bl w) @ take n (to_bl w)"
  1571   apply (unfold word_roti_def)
  1572   apply (simp add: bl_word_rotl_dt bl_word_rotr_dt word_size)
  1573   apply safe
  1574    apply (simp add: zmod_zminus1_eq_if)
  1575    apply safe
  1576     apply (simp add: nat_mult_distrib)
  1577    apply (simp add: nat_diff_distrib [OF pos_mod_sign pos_mod_conj 
  1578                                       [THEN conjunct2, THEN order_less_imp_le]]
  1579                     nat_mod_distrib)
  1580   apply (simp add: nat_mod_distrib)
  1581   done
  1582 
  1583 lemmas bl_word_roti_dt = bl_word_roti_dt' [unfolded word_size]
  1584 
  1585 lemmas word_rotl_dt = bl_word_rotl_dt 
  1586   [THEN word_bl.Rep_inverse' [symmetric], standard] 
  1587 lemmas word_rotr_dt = bl_word_rotr_dt 
  1588   [THEN word_bl.Rep_inverse' [symmetric], standard]
  1589 lemmas word_roti_dt = bl_word_roti_dt 
  1590   [THEN word_bl.Rep_inverse' [symmetric], standard]
  1591 
  1592 lemma word_rotx_0 [simp] : "word_rotr i 0 = 0 & word_rotl i 0 = 0"
  1593   by (simp add : word_rotr_dt word_rotl_dt to_bl_0 replicate_add [symmetric])
  1594 
  1595 lemma word_roti_0' [simp] : "word_roti n 0 = 0"
  1596   unfolding word_roti_def by auto
  1597 
  1598 lemmas word_rotr_dt_no_bin' [simp] = 
  1599   word_rotr_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
  1600 
  1601 lemmas word_rotl_dt_no_bin' [simp] = 
  1602   word_rotl_dt [where w="number_of w", unfolded to_bl_no_bin, standard]
  1603 
  1604 declare word_roti_def [simp]
  1605 
  1606 end
  1607