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