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