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