src/HOL/Word/WordBitwise.thy
 author wenzelm Sun Sep 18 20:33:48 2016 +0200 (2016-09-18) changeset 63915 bab633745c7f parent 62913 13252110a6fe child 65363 5eb619751b14 permissions -rw-r--r--
tuned proofs;
```     1 (*  Title:      HOL/Word/WordBitwise.thy
```
```     2     Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
```
```     3 *)
```
```     4
```
```     5
```
```     6 theory WordBitwise
```
```     7
```
```     8 imports Word
```
```     9
```
```    10 begin
```
```    11
```
```    12 text \<open>Helper constants used in defining addition\<close>
```
```    13
```
```    14 definition
```
```    15   xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
```
```    16 where
```
```    17  "xor3 a b c = (a = (b = c))"
```
```    18
```
```    19 definition
```
```    20   carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
```
```    21 where
```
```    22  "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
```
```    23
```
```    24 lemma carry_simps:
```
```    25   "carry True a b = (a \<or> b)"
```
```    26   "carry a True b = (a \<or> b)"
```
```    27   "carry a b True = (a \<or> b)"
```
```    28   "carry False a b = (a \<and> b)"
```
```    29   "carry a False b = (a \<and> b)"
```
```    30   "carry a b False = (a \<and> b)"
```
```    31   by (auto simp add: carry_def)
```
```    32
```
```    33 lemma xor3_simps:
```
```    34   "xor3 True a b = (a = b)"
```
```    35   "xor3 a True b = (a = b)"
```
```    36   "xor3 a b True = (a = b)"
```
```    37   "xor3 False a b = (a \<noteq> b)"
```
```    38   "xor3 a False b = (a \<noteq> b)"
```
```    39   "xor3 a b False = (a \<noteq> b)"
```
```    40   by (simp_all add: xor3_def)
```
```    41
```
```    42 text \<open>Breaking up word equalities into equalities on their
```
```    43 bit lists. Equalities are generated and manipulated in the
```
```    44 reverse order to to_bl.\<close>
```
```    45
```
```    46 lemma word_eq_rbl_eq:
```
```    47   "(x = y) = (rev (to_bl x) = rev (to_bl y))"
```
```    48   by simp
```
```    49
```
```    50 lemma rbl_word_or:
```
```    51   "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
```
```    52   by (simp add: map2_def zip_rev bl_word_or rev_map)
```
```    53
```
```    54 lemma rbl_word_and:
```
```    55   "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
```
```    56   by (simp add: map2_def zip_rev bl_word_and rev_map)
```
```    57
```
```    58 lemma rbl_word_xor:
```
```    59   "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
```
```    60   by (simp add: map2_def zip_rev bl_word_xor rev_map)
```
```    61
```
```    62 lemma rbl_word_not:
```
```    63   "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
```
```    64   by (simp add: bl_word_not rev_map)
```
```    65
```
```    66 lemma bl_word_sub:
```
```    67   "to_bl (x - y) = to_bl (x + (- y))"
```
```    68   by simp
```
```    69
```
```    70 lemma rbl_word_1:
```
```    71   "rev (to_bl (1 :: ('a :: len0) word))
```
```    72      = takefill False (len_of TYPE('a)) [True]"
```
```    73   apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
```
```    74    apply simp
```
```    75   apply (simp only: rtb_rbl_ariths(1)[OF refl])
```
```    76   apply simp
```
```    77   apply (case_tac "len_of TYPE('a)")
```
```    78    apply simp
```
```    79   apply (simp add: takefill_alt)
```
```    80   done
```
```    81
```
```    82 lemma rbl_word_if:
```
```    83   "rev (to_bl (if P then x else y))
```
```    84       = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
```
```    85   by (simp add: map2_def split_def)
```
```    86
```
```    87 lemma rbl_add_carry_Cons:
```
```    88   "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
```
```    89         = xor3 x y car # (if carry x y car then rbl_succ else id)
```
```    90              (rbl_add xs ys)"
```
```    91   by (simp add: carry_def xor3_def)
```
```    92
```
```    93 lemma rbl_add_suc_carry_fold:
```
```    94   "length xs = length ys \<Longrightarrow>
```
```    95    \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
```
```    96         = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
```
```    97                  (zip xs ys) (\<lambda>_. [])) car"
```
```    98   apply (erule list_induct2)
```
```    99    apply simp
```
```   100   apply (simp only: rbl_add_carry_Cons)
```
```   101   apply simp
```
```   102   done
```
```   103
```
```   104 lemma to_bl_plus_carry:
```
```   105   "to_bl (x + y)
```
```   106      = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
```
```   107                  (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
```
```   108   using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
```
```   109   apply (simp add: word_add_rbl[OF refl refl])
```
```   110   apply (drule_tac x=False in spec)
```
```   111   apply (simp add: zip_rev)
```
```   112   done
```
```   113
```
```   114 definition
```
```   115  "rbl_plus cin xs ys = foldr
```
```   116        (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
```
```   117        (zip xs ys) (\<lambda>_. []) cin"
```
```   118
```
```   119 lemma rbl_plus_simps:
```
```   120   "rbl_plus cin (x # xs) (y # ys)
```
```   121       = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
```
```   122   "rbl_plus cin [] ys = []"
```
```   123   "rbl_plus cin xs [] = []"
```
```   124   by (simp_all add: rbl_plus_def)
```
```   125
```
```   126 lemma rbl_word_plus:
```
```   127   "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
```
```   128   by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
```
```   129
```
```   130 definition
```
```   131  "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
```
```   132
```
```   133 lemma rbl_succ2_simps:
```
```   134   "rbl_succ2 b [] = []"
```
```   135   "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
```
```   136   by (simp_all add: rbl_succ2_def)
```
```   137
```
```   138 lemma twos_complement:
```
```   139   "- x = word_succ (NOT x)"
```
```   140   using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
```
```   141   by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
```
```   142            del: word_add_not)
```
```   143
```
```   144 lemma rbl_word_neg:
```
```   145   "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
```
```   146   by (simp add: twos_complement word_succ_rbl[OF refl]
```
```   147                 bl_word_not rev_map rbl_succ2_def)
```
```   148
```
```   149 lemma rbl_word_cat:
```
```   150   "rev (to_bl (word_cat x y :: ('a :: len0) word))
```
```   151      = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
```
```   152   by (simp add: word_cat_bl word_rev_tf)
```
```   153
```
```   154 lemma rbl_word_slice:
```
```   155   "rev (to_bl (slice n w :: ('a :: len0) word))
```
```   156      = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
```
```   157   apply (simp add: slice_take word_rev_tf rev_take)
```
```   158   apply (cases "n < len_of TYPE('b)", simp_all)
```
```   159   done
```
```   160
```
```   161 lemma rbl_word_ucast:
```
```   162   "rev (to_bl (ucast x :: ('a :: len0) word))
```
```   163      = takefill False (len_of TYPE('a)) (rev (to_bl x))"
```
```   164   apply (simp add: to_bl_ucast takefill_alt)
```
```   165   apply (simp add: rev_drop)
```
```   166   apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
```
```   167    apply simp_all
```
```   168   done
```
```   169
```
```   170 lemma rbl_shiftl:
```
```   171   "rev (to_bl (w << n)) = takefill False (size w)
```
```   172      (replicate n False @ rev (to_bl w))"
```
```   173   by (simp add: bl_shiftl takefill_alt word_size rev_drop)
```
```   174
```
```   175 lemma rbl_shiftr:
```
```   176   "rev (to_bl (w >> n)) = takefill False (size w)
```
```   177      (drop n (rev (to_bl w)))"
```
```   178   by (simp add: shiftr_slice rbl_word_slice word_size)
```
```   179
```
```   180 definition
```
```   181  "drop_nonempty v n xs
```
```   182      = (if n < length xs then drop n xs else [last (v # xs)])"
```
```   183
```
```   184 lemma drop_nonempty_simps:
```
```   185   "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
```
```   186   "drop_nonempty v 0 (x # xs) = (x # xs)"
```
```   187   "drop_nonempty v n [] = [v]"
```
```   188   by (simp_all add: drop_nonempty_def)
```
```   189
```
```   190 definition
```
```   191   "takefill_last x n xs = takefill (last (x # xs)) n xs"
```
```   192
```
```   193 lemma takefill_last_simps:
```
```   194   "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
```
```   195   "takefill_last z 0 xs = []"
```
```   196   "takefill_last z n [] = replicate n z"
```
```   197   apply (simp_all add: takefill_last_def)
```
```   198   apply (simp_all add: takefill_alt)
```
```   199   done
```
```   200
```
```   201 lemma rbl_sshiftr:
```
```   202   "rev (to_bl (w >>> n)) =
```
```   203      takefill_last False (size w)
```
```   204         (drop_nonempty False n (rev (to_bl w)))"
```
```   205   apply (cases "n < size w")
```
```   206    apply (simp add: bl_sshiftr takefill_last_def word_size
```
```   207                     takefill_alt rev_take last_rev
```
```   208                     drop_nonempty_def)
```
```   209   apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
```
```   210    apply (simp add: word_size takefill_last_def takefill_alt
```
```   211                     last_rev word_msb_alt word_rev_tf
```
```   212                     drop_nonempty_def take_Cons')
```
```   213    apply (case_tac "len_of TYPE('a)", simp_all)
```
```   214   apply (rule word_eqI)
```
```   215   apply (simp add: nth_sshiftr word_size test_bit_of_bl
```
```   216                    msb_nth)
```
```   217   done
```
```   218
```
```   219 lemma nth_word_of_int:
```
```   220   "(word_of_int x :: ('a :: len0) word) !! n
```
```   221       = (n < len_of TYPE('a) \<and> bin_nth x n)"
```
```   222   apply (simp add: test_bit_bl word_size to_bl_of_bin)
```
```   223   apply (subst conj_cong[OF refl], erule bin_nth_bl)
```
```   224   apply (auto)
```
```   225   done
```
```   226
```
```   227 lemma nth_scast:
```
```   228   "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
```
```   229      = (n < len_of TYPE('b) \<and>
```
```   230           (if n < len_of TYPE('a) - 1 then x !! n
```
```   231            else x !! (len_of TYPE('a) - 1)))"
```
```   232   by (simp add: scast_def nth_word_of_int nth_sint)
```
```   233
```
```   234 lemma rbl_word_scast:
```
```   235   "rev (to_bl (scast x :: ('a :: len) word))
```
```   236      = takefill_last False (len_of TYPE('a))
```
```   237            (rev (to_bl x))"
```
```   238   apply (rule nth_equalityI)
```
```   239    apply (simp add: word_size takefill_last_def)
```
```   240   apply (clarsimp simp: nth_scast takefill_last_def
```
```   241                         nth_takefill word_size nth_rev to_bl_nth)
```
```   242   apply (cases "len_of TYPE('b)")
```
```   243    apply simp
```
```   244   apply (clarsimp simp: less_Suc_eq_le linorder_not_less
```
```   245                         last_rev word_msb_alt[symmetric]
```
```   246                         msb_nth)
```
```   247   done
```
```   248
```
```   249 definition
```
```   250   rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
```
```   251 where
```
```   252  "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
```
```   253     xs []"
```
```   254
```
```   255 lemma rbl_mul_simps:
```
```   256   "rbl_mul (x # xs) ys
```
```   257      = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
```
```   258   "rbl_mul [] ys = []"
```
```   259   by (simp_all add: rbl_mul_def)
```
```   260
```
```   261 lemma takefill_le2:
```
```   262   "length xs \<le> n \<Longrightarrow>
```
```   263    takefill x m (takefill x n xs)
```
```   264      = takefill x m xs"
```
```   265   by (simp add: takefill_alt replicate_add[symmetric])
```
```   266
```
```   267 lemma take_rbl_plus:
```
```   268   "\<forall>n b. take n (rbl_plus b xs ys)
```
```   269     = rbl_plus b (take n xs) (take n ys)"
```
```   270   apply (simp add: rbl_plus_def take_zip[symmetric])
```
```   271   apply (rule_tac list="zip xs ys" in list.induct)
```
```   272    apply simp
```
```   273   apply (clarsimp simp: split_def)
```
```   274   apply (case_tac n, simp_all)
```
```   275   done
```
```   276
```
```   277 lemma word_rbl_mul_induct:
```
```   278   fixes y :: "'a :: len word" shows
```
```   279   "length xs \<le> size y
```
```   280    \<Longrightarrow> rbl_mul xs (rev (to_bl y))
```
```   281      = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
```
```   282 proof (induct xs)
```
```   283   case Nil
```
```   284   show ?case
```
```   285     by (simp add: rbl_mul_simps)
```
```   286 next
```
```   287   case (Cons z zs)
```
```   288
```
```   289   have rbl_word_plus':
```
```   290     "\<And>(x :: 'a word) y.
```
```   291       to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
```
```   292     by (simp add: rbl_word_plus[symmetric])
```
```   293
```
```   294   have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
```
```   295     apply (cases z)
```
```   296      apply (simp cong: map_cong)
```
```   297     apply (simp add: map_replicate_const cong: map_cong)
```
```   298     done
```
```   299
```
```   300   have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
```
```   301     by (simp add: shiftl_t2n)
```
```   302
```
```   303   have zip_take_triv: "\<And>xs ys n. n = length ys
```
```   304       \<Longrightarrow> zip (take n xs) ys = zip xs ys"
```
```   305     by (rule nth_equalityI, simp_all)
```
```   306
```
```   307   show ?case
```
```   308     using Cons
```
```   309     apply (simp add: trans [OF of_bl_append add.commute]
```
```   310                      rbl_mul_simps rbl_word_plus'
```
```   311                      Cons.hyps distrib_right mult_bit
```
```   312                      shiftl rbl_shiftl)
```
```   313     apply (simp add: takefill_alt word_size rev_map take_rbl_plus
```
```   314                      min_def)
```
```   315     apply (simp add: rbl_plus_def zip_take_triv)
```
```   316     done
```
```   317 qed
```
```   318
```
```   319 lemma rbl_word_mul:
```
```   320   fixes x :: "'a :: len word"
```
```   321   shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
```
```   322   using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
```
```   323   by (simp add: word_size)
```
```   324
```
```   325 text \<open>Breaking up inequalities into bitlist properties.\<close>
```
```   326
```
```   327 definition
```
```   328   "rev_bl_order F xs ys =
```
```   329      (length xs = length ys \<and>
```
```   330        ((xs = ys \<and> F)
```
```   331           \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
```
```   332                    \<and> \<not> xs ! n \<and> ys ! n)))"
```
```   333
```
```   334 lemma rev_bl_order_simps:
```
```   335   "rev_bl_order F [] [] = F"
```
```   336   "rev_bl_order F (x # xs) (y # ys)
```
```   337      = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
```
```   338   apply (simp_all add: rev_bl_order_def)
```
```   339   apply (rule conj_cong[OF refl])
```
```   340   apply (cases "xs = ys")
```
```   341    apply (simp add: nth_Cons')
```
```   342    apply blast
```
```   343   apply (simp add: nth_Cons')
```
```   344   apply safe
```
```   345    apply (rule_tac x="n - 1" in exI)
```
```   346    apply simp
```
```   347   apply (rule_tac x="Suc n" in exI)
```
```   348   apply simp
```
```   349   done
```
```   350
```
```   351 lemma rev_bl_order_rev_simp:
```
```   352   "length xs = length ys \<Longrightarrow>
```
```   353    rev_bl_order F (xs @ [x]) (ys @ [y])
```
```   354      = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
```
```   355   apply (induct arbitrary: F rule: list_induct2)
```
```   356    apply (auto simp add: rev_bl_order_simps)
```
```   357   done
```
```   358
```
```   359 lemma rev_bl_order_bl_to_bin:
```
```   360   "length xs = length ys
```
```   361      \<Longrightarrow> rev_bl_order True xs ys
```
```   362             = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
```
```   363        \<and> rev_bl_order False xs ys
```
```   364             = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
```
```   365   apply (induct xs ys rule: list_induct2)
```
```   366    apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
```
```   367   apply (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
```
```   368   done
```
```   369
```
```   370 lemma word_le_rbl:
```
```   371   fixes x :: "('a :: len0) word"
```
```   372   shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
```
```   373   by (simp add: rev_bl_order_bl_to_bin word_le_def)
```
```   374
```
```   375 lemma word_less_rbl:
```
```   376   fixes x :: "('a :: len0) word"
```
```   377   shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
```
```   378   by (simp add: word_less_alt rev_bl_order_bl_to_bin)
```
```   379
```
```   380 lemma word_sint_msb_eq:
```
```   381   "sint x = uint x - (if msb x then 2 ^ size x else 0)"
```
```   382   apply (cases "msb x")
```
```   383    apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
```
```   384     apply (simp add: word_size wi_hom_syms
```
```   385                      word_of_int_2p_len)
```
```   386    apply (simp add: sints_num word_size)
```
```   387    apply (rule conjI)
```
```   388     apply (simp add: le_diff_eq')
```
```   389     apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
```
```   390      apply (simp add: power_Suc[symmetric])
```
```   391     apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
```
```   392     apply (rule notI, drule word_eqD[where x="size x - 1"])
```
```   393     apply (simp add: msb_nth word_ops_nth_size word_size)
```
```   394    apply (simp add: order_less_le_trans[where y=0])
```
```   395   apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
```
```   396   apply (simp add: linorder_not_less uints_num word_msb_sint)
```
```   397   apply (rule order_less_le_trans[OF sint_lt])
```
```   398   apply simp
```
```   399   done
```
```   400
```
```   401 lemma word_sle_msb_le:
```
```   402   "(x <=s y) = ((msb y --> msb x) \<and>
```
```   403                   ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
```
```   404   apply (simp add: word_sle_def word_sint_msb_eq word_size
```
```   405                    word_le_def)
```
```   406   apply safe
```
```   407    apply (rule order_trans[OF _ uint_ge_0])
```
```   408    apply (simp add: order_less_imp_le)
```
```   409   apply (erule notE[OF leD])
```
```   410   apply (rule order_less_le_trans[OF _ uint_ge_0])
```
```   411   apply simp
```
```   412   done
```
```   413
```
```   414 lemma word_sless_msb_less:
```
```   415   "(x <s y) = ((msb y --> msb x) \<and>
```
```   416                   ((msb x \<and> \<not> msb y) \<or> (x < y)))"
```
```   417   by (auto simp add: word_sless_def word_sle_msb_le)
```
```   418
```
```   419 definition
```
```   420   "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
```
```   421
```
```   422 lemma map_last_simps:
```
```   423   "map_last f [] = []"
```
```   424   "map_last f [x] = [f x]"
```
```   425   "map_last f (x # y # zs) = x # map_last f (y # zs)"
```
```   426   by (simp_all add: map_last_def)
```
```   427
```
```   428 lemma word_sle_rbl:
```
```   429   "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
```
```   430      (map_last Not (rev (to_bl y)))"
```
```   431   using word_msb_alt[where w=x] word_msb_alt[where w=y]
```
```   432   apply (simp add: word_sle_msb_le word_le_rbl)
```
```   433   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
```
```   434    apply (cases "to_bl x", simp)
```
```   435    apply (cases "to_bl y", simp)
```
```   436    apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
```
```   437    apply auto
```
```   438   done
```
```   439
```
```   440 lemma word_sless_rbl:
```
```   441   "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
```
```   442      (map_last Not (rev (to_bl y)))"
```
```   443   using word_msb_alt[where w=x] word_msb_alt[where w=y]
```
```   444   apply (simp add: word_sless_msb_less word_less_rbl)
```
```   445   apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
```
```   446    apply (cases "to_bl x", simp)
```
```   447    apply (cases "to_bl y", simp)
```
```   448    apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
```
```   449    apply auto
```
```   450   done
```
```   451
```
```   452 text \<open>Lemmas for unpacking rev (to_bl n) for numerals n and also
```
```   453 for irreducible values and expressions.\<close>
```
```   454
```
```   455 lemma rev_bin_to_bl_simps:
```
```   456   "rev (bin_to_bl 0 x) = []"
```
```   457   "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
```
```   458     = False # rev (bin_to_bl n (numeral nm))"
```
```   459   "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
```
```   460     = True # rev (bin_to_bl n (numeral nm))"
```
```   461   "rev (bin_to_bl (Suc n) (numeral (num.One)))
```
```   462     = True # replicate n False"
```
```   463   "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm)))
```
```   464     = False # rev (bin_to_bl n (- numeral nm))"
```
```   465   "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm)))
```
```   466     = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
```
```   467   "rev (bin_to_bl (Suc n) (- numeral (num.One)))
```
```   468     = True # replicate n True"
```
```   469   "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One)))
```
```   470     = True # rev (bin_to_bl n (- numeral (nm + num.One)))"
```
```   471   "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One)))
```
```   472     = False # rev (bin_to_bl n (- numeral (nm + num.One)))"
```
```   473   "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One)))
```
```   474     = False # rev (bin_to_bl n (- numeral num.One))"
```
```   475   apply (simp_all add: bin_to_bl_def)
```
```   476   apply (simp_all only: bin_to_bl_aux_alt)
```
```   477   apply (simp_all)
```
```   478   apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
```
```   479   done
```
```   480
```
```   481 lemma to_bl_upt:
```
```   482   "to_bl x = rev (map (op !! x) [0 ..< size x])"
```
```   483   apply (rule nth_equalityI)
```
```   484    apply (simp add: word_size)
```
```   485   apply (clarsimp simp: to_bl_nth word_size nth_rev)
```
```   486   done
```
```   487
```
```   488 lemma rev_to_bl_upt:
```
```   489   "rev (to_bl x) = map (op !! x) [0 ..< size x]"
```
```   490   by (simp add: to_bl_upt)
```
```   491
```
```   492 lemma upt_eq_list_intros:
```
```   493   "j <= i \<Longrightarrow> [i ..< j] = []"
```
```   494   "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
```
```   495   by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
```
```   496
```
```   497 text \<open>Tactic definition\<close>
```
```   498
```
```   499 ML \<open>
```
```   500 structure Word_Bitwise_Tac =
```
```   501 struct
```
```   502
```
```   503 val word_ss = simpset_of @{theory_context Word};
```
```   504
```
```   505 fun mk_nat_clist ns = List.foldr
```
```   506   (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
```
```   507   @{cterm "[] :: nat list"} ns;
```
```   508
```
```   509 fun upt_conv ctxt ct =
```
```   510   case Thm.term_of ct of
```
```   511     (@{const upt} \$ n \$ m) =>
```
```   512       let
```
```   513         val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
```
```   514         val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
```
```   515           |> mk_nat_clist;
```
```   516         val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
```
```   517                      |> Thm.apply @{cterm Trueprop};
```
```   518       in
```
```   519         try (fn () =>
```
```   520           Goal.prove_internal ctxt [] prop
```
```   521             (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
```
```   522                 ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
```
```   523       end
```
```   524   | _ => NONE;
```
```   525
```
```   526 val expand_upt_simproc =
```
```   527   Simplifier.make_simproc @{context} "expand_upt"
```
```   528    {lhss = [@{term "upt x y"}], proc = K upt_conv};
```
```   529
```
```   530 fun word_len_simproc_fn ctxt ct =
```
```   531   case Thm.term_of ct of
```
```   532     Const (@{const_name len_of}, _) \$ t => (let
```
```   533         val T = fastype_of t |> dest_Type |> snd |> the_single
```
```   534         val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
```
```   535         val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
```
```   536                  |> Thm.apply @{cterm Trueprop};
```
```   537       in Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
```
```   538              |> mk_meta_eq |> SOME end
```
```   539     handle TERM _ => NONE | TYPE _ => NONE)
```
```   540   | _ => NONE;
```
```   541
```
```   542 val word_len_simproc =
```
```   543   Simplifier.make_simproc @{context} "word_len"
```
```   544    {lhss = [@{term "len_of x"}], proc = K word_len_simproc_fn};
```
```   545
```
```   546 (* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
```
```   547    or just 5 (discarding nat) when n_sucs = 0 *)
```
```   548
```
```   549 fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
```
```   550   let
```
```   551     val (f \$ arg) = Thm.term_of ct;
```
```   552     val n = (case arg of @{term nat} \$ n => n | n => n)
```
```   553       |> HOLogic.dest_number |> snd;
```
```   554     val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs)
```
```   555       else (n, 0);
```
```   556     val arg' = List.foldr (op \$) (HOLogic.mk_number @{typ nat} j)
```
```   557         (replicate i @{term Suc});
```
```   558     val _ = if arg = arg' then raise TERM ("", []) else ();
```
```   559     fun propfn g = HOLogic.mk_eq (g arg, g arg')
```
```   560       |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
```
```   561     val eq1 = Goal.prove_internal ctxt [] (propfn I)
```
```   562       (K (simp_tac (put_simpset word_ss ctxt) 1));
```
```   563   in Goal.prove_internal ctxt [] (propfn (curry (op \$) f))
```
```   564       (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
```
```   565        |> mk_meta_eq |> SOME end
```
```   566     handle TERM _ => NONE;
```
```   567
```
```   568 fun nat_get_Suc_simproc n_sucs ts =
```
```   569   Simplifier.make_simproc @{context} "nat_get_Suc"
```
```   570    {lhss = map (fn t => t \$ @{term "n :: nat"}) ts,
```
```   571     proc = K (nat_get_Suc_simproc_fn n_sucs)};
```
```   572
```
```   573 val no_split_ss =
```
```   574   simpset_of (put_simpset HOL_ss @{context}
```
```   575     |> Splitter.del_split @{thm if_split});
```
```   576
```
```   577 val expand_word_eq_sss =
```
```   578   (simpset_of (put_simpset HOL_basic_ss @{context} addsimps
```
```   579        @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
```
```   580   map simpset_of [
```
```   581    put_simpset no_split_ss @{context} addsimps
```
```   582     @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
```
```   583                                 rbl_word_neg bl_word_sub rbl_word_xor
```
```   584                                 rbl_word_cat rbl_word_slice rbl_word_scast
```
```   585                                 rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
```
```   586                                 rbl_word_if},
```
```   587    put_simpset no_split_ss @{context} addsimps
```
```   588     @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
```
```   589    put_simpset no_split_ss @{context} addsimps
```
```   590     @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
```
```   591           addsimprocs [word_len_simproc],
```
```   592    put_simpset no_split_ss @{context} addsimps
```
```   593     @{thms list.simps split_conv replicate.simps list.map
```
```   594                                 zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
```
```   595                                 foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
```
```   596                                 takefill_Suc_Nil takefill.Z rbl_succ2_simps
```
```   597                                 rbl_plus_simps rev_bin_to_bl_simps append.simps
```
```   598                                 takefill_last_simps drop_nonempty_simps
```
```   599                                 rev_bl_order_simps}
```
```   600           addsimprocs [expand_upt_simproc,
```
```   601                        nat_get_Suc_simproc 4
```
```   602                          [@{term replicate}, @{term "takefill x"},
```
```   603                           @{term drop}, @{term "bin_to_bl"},
```
```   604                           @{term "takefill_last x"},
```
```   605                           @{term "drop_nonempty x"}]],
```
```   606     put_simpset no_split_ss @{context} addsimps @{thms xor3_simps carry_simps if_bool_simps}
```
```   607   ])
```
```   608
```
```   609 fun tac ctxt =
```
```   610   let
```
```   611     val (ss, sss) = expand_word_eq_sss;
```
```   612   in
```
```   613     foldr1 (op THEN_ALL_NEW)
```
```   614       ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
```
```   615         map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
```
```   616   end;
```
```   617
```
```   618 end
```
```   619
```
```   620 \<close>
```
```   621
```
```   622 method_setup word_bitwise =
```
```   623   \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
```
```   624   "decomposer for word equalities and inequalities into bit propositions"
```
```   625
```
```   626 end
```