New tactic "word_bitwise" expands word equalities/inequalities into logic.
authorThomas Sewell <thomas.sewell@nicta.com.au>
Tue Apr 17 16:21:47 2012 +1000 (2012-04-17)
changeset 47567407cabf66f21
parent 47566 c201a1fe0a81
child 47568 98c8b7542b72
New tactic "word_bitwise" expands word equalities/inequalities into logic.
CONTRIBUTORS
NEWS
src/HOL/IsaMakefile
src/HOL/Word/Examples/WordExamples.thy
src/HOL/Word/Tools/smt_word.ML
src/HOL/Word/Tools/word_lib.ML
src/HOL/Word/Word.thy
src/HOL/Word/WordBitwise.thy
     1.1 --- a/CONTRIBUTORS	Wed Apr 18 23:57:44 2012 +0200
     1.2 +++ b/CONTRIBUTORS	Tue Apr 17 16:21:47 2012 +1000
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to Isabelle2012
     1.5  -----------------------------
     1.6  
     1.7 +* April 2012: Thomas Sewell, NICTA
     1.8 +    (based on work done with Sascha Boehme, TUM in 2010)
     1.9 +  WordBitwise: logic/circuit expansion of bitvector equalities/inequalities.
    1.10 +
    1.11  * March 2012: Christian Sternagel, Japan Advanced Institute of Science
    1.12    and Technology
    1.13    Consolidated theory of relation composition.
     2.1 --- a/NEWS	Wed Apr 18 23:57:44 2012 +0200
     2.2 +++ b/NEWS	Tue Apr 17 16:21:47 2012 +1000
     2.3 @@ -521,6 +521,14 @@
     2.4    word_of_int_0_hom ~> word_0_wi
     2.5    word_of_int_1_hom ~> word_1_wi
     2.6  
     2.7 +* New tactic "word_bitwise" for splitting machine word equalities and
     2.8 +inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word
     2.9 +session. Supports addition, subtraction, multiplication, shifting by
    2.10 +constants, bitwise operators and numeric constants. Requires fixed-length word
    2.11 +types, cannot operate on 'a word. Solves many standard word identies outright
    2.12 +and converts more into first order problems amenable to blast or similar. See
    2.13 +HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy.
    2.14 +
    2.15  * Clarified attribute "mono_set": pure declaration without modifying
    2.16  the result of the fact expression.
    2.17  
     3.1 --- a/src/HOL/IsaMakefile	Wed Apr 18 23:57:44 2012 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Apr 17 16:21:47 2012 +1000
     3.3 @@ -1265,8 +1265,8 @@
     3.4    Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
     3.5    Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
     3.6    Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
     3.7 -  Word/Word.thy Word/document/root.tex					\
     3.8 -  Word/document/root.bib Word/Tools/smt_word.ML
     3.9 +  Word/Word.thy Word/WordBitwise.thy Word/document/root.tex		\
    3.10 +  Word/document/root.bib Word/Tools/smt_word.ML Word/Tools/word_lib.ML
    3.11  	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
    3.12  
    3.13  
     4.1 --- a/src/HOL/Word/Examples/WordExamples.thy	Wed Apr 18 23:57:44 2012 +0200
     4.2 +++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Apr 17 16:21:47 2012 +1000
     4.3 @@ -1,5 +1,5 @@
     4.4  (* 
     4.5 -  Author: Gerwin Klein, NICTA
     4.6 +  Authors: Gerwin Klein and Thomas Sewell, NICTA
     4.7  
     4.8    Examples demonstrating and testing various word operations.
     4.9  *)
    4.10 @@ -7,7 +7,7 @@
    4.11  header "Examples of word operations"
    4.12  
    4.13  theory WordExamples
    4.14 -imports "../Word"
    4.15 +imports "../Word" "../WordBitwise"
    4.16  begin
    4.17  
    4.18  type_synonym word32 = "32 word"
    4.19 @@ -164,4 +164,39 @@
    4.20    finally show ?thesis .
    4.21  qed
    4.22  
    4.23 +text "alternative proof using bitwise expansion"
    4.24 +
    4.25 +lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
    4.26 +  by word_bitwise
    4.27 +
    4.28 +text "more proofs using bitwise expansion"
    4.29 +
    4.30 +lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
    4.31 +  by word_bitwise
    4.32 +
    4.33 +lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3"
    4.34 +  by word_bitwise
    4.35 +
    4.36 +text "some problems require further reasoning after bit expansion"
    4.37 +
    4.38 +lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89"
    4.39 +  apply word_bitwise
    4.40 +  apply blast
    4.41 +  done
    4.42 +
    4.43 +lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
    4.44 +  apply word_bitwise
    4.45 +  apply clarsimp
    4.46 +  done
    4.47 +
    4.48 +text "operations like shifts by non-numerals will expose some internal list
    4.49 + representations but may still be easy to solve"
    4.50 +
    4.51 +lemma shiftr_overflow:
    4.52 +  "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0"
    4.53 +  apply (word_bitwise)
    4.54 +  apply simp
    4.55 +  done
    4.56 +
    4.57 +
    4.58  end
     5.1 --- a/src/HOL/Word/Tools/smt_word.ML	Wed Apr 18 23:57:44 2012 +0200
     5.2 +++ b/src/HOL/Word/Tools/smt_word.ML	Tue Apr 17 16:21:47 2012 +1000
     5.3 @@ -12,23 +12,7 @@
     5.4  structure SMT_Word: SMT_WORD =
     5.5  struct
     5.6  
     5.7 -
     5.8 -(* utilities *)
     5.9 -
    5.10 -fun dest_binT T =
    5.11 -  (case T of
    5.12 -    Type (@{type_name "Numeral_Type.num0"}, _) => 0
    5.13 -  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    5.14 -  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
    5.15 -  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
    5.16 -  | _ => raise TYPE ("dest_binT", [T], []))
    5.17 -
    5.18 -fun is_wordT (Type (@{type_name word}, _)) = true
    5.19 -  | is_wordT _ = false
    5.20 -
    5.21 -fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
    5.22 -  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
    5.23 -
    5.24 +open Word_Lib
    5.25  
    5.26  (* SMT-LIB logic *)
    5.27  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Word/Tools/word_lib.ML	Tue Apr 17 16:21:47 2012 +1000
     6.3 @@ -0,0 +1,40 @@
     6.4 +(*  Title:      HOL/Word/Tools/word_lib.ML
     6.5 +    Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
     6.6 +
     6.7 +Helper routines for operating on the word type at the ML level.
     6.8 +*)
     6.9 +
    6.10 +
    6.11 +structure Word_Lib = struct
    6.12 +
    6.13 +fun dest_binT T =
    6.14 +  (case T of
    6.15 +    Type (@{type_name "Numeral_Type.num0"}, _) => 0
    6.16 +  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
    6.17 +  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
    6.18 +  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
    6.19 +  | _ => raise TYPE ("dest_binT", [T], []))
    6.20 +
    6.21 +fun is_wordT (Type (@{type_name word}, _)) = true
    6.22 +  | is_wordT _ = false
    6.23 +
    6.24 +fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
    6.25 +  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
    6.26 +
    6.27 +local
    6.28 +  fun mk_bitT i T =
    6.29 +    if i = 0
    6.30 +    then Type (@{type_name "Numeral_Type.bit0"}, [T])
    6.31 +    else Type (@{type_name "Numeral_Type.bit1"}, [T])
    6.32 +
    6.33 +  fun mk_binT size = 
    6.34 +    if size = 0 then @{typ "Numeral_Type.num0"}
    6.35 +    else if size = 1 then @{typ "Numeral_Type.num1"}
    6.36 +    else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
    6.37 +in
    6.38 +fun mk_wordT size =
    6.39 +  if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
    6.40 +  else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], [])
    6.41 +end
    6.42 +
    6.43 +end
     7.1 --- a/src/HOL/Word/Word.thy	Wed Apr 18 23:57:44 2012 +0200
     7.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 17 16:21:47 2012 +1000
     7.3 @@ -10,7 +10,9 @@
     7.4    Misc_Typedef
     7.5    "~~/src/HOL/Library/Boolean_Algebra"
     7.6    Bool_List_Representation
     7.7 -uses ("~~/src/HOL/Word/Tools/smt_word.ML")
     7.8 +uses
     7.9 +  ("~~/src/HOL/Word/Tools/smt_word.ML")
    7.10 +  ("~~/src/HOL/Word/Tools/word_lib.ML")
    7.11  begin
    7.12  
    7.13  text {* see @{text "Examples/WordExamples.thy"} for examples *}
    7.14 @@ -4642,7 +4644,7 @@
    7.15  
    7.16  declare bin_to_bl_def [simp]
    7.17  
    7.18 -
    7.19 +use "~~/src/HOL/Word/Tools/word_lib.ML"
    7.20  use "~~/src/HOL/Word/Tools/smt_word.ML"
    7.21  setup {* SMT_Word.setup *}
    7.22  
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Word/WordBitwise.thy	Tue Apr 17 16:21:47 2012 +1000
     8.3 @@ -0,0 +1,613 @@
     8.4 +(*  Title:      HOL/Word/WordBitwise.thy
     8.5 +    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
     8.6 +*)
     8.7 +
     8.8 +
     8.9 +theory WordBitwise
    8.10 +
    8.11 +imports Word
    8.12 +
    8.13 +begin
    8.14 +
    8.15 +text {* Helper constants used in defining addition *}
    8.16 +
    8.17 +definition
    8.18 +  xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    8.19 +where
    8.20 + "xor3 a b c = (a = (b = c))"
    8.21 +
    8.22 +definition
    8.23 +  carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
    8.24 +where
    8.25 + "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
    8.26 +
    8.27 +lemma carry_simps:
    8.28 +  "carry True a b = (a \<or> b)"
    8.29 +  "carry a True b = (a \<or> b)"
    8.30 +  "carry a b True = (a \<or> b)"
    8.31 +  "carry False a b = (a \<and> b)"
    8.32 +  "carry a False b = (a \<and> b)"
    8.33 +  "carry a b False = (a \<and> b)"
    8.34 +  by (auto simp add: carry_def)
    8.35 +
    8.36 +lemma xor3_simps:
    8.37 +  "xor3 True a b = (a = b)"
    8.38 +  "xor3 a True b = (a = b)"
    8.39 +  "xor3 a b True = (a = b)"
    8.40 +  "xor3 False a b = (a \<noteq> b)"
    8.41 +  "xor3 a False b = (a \<noteq> b)"
    8.42 +  "xor3 a b False = (a \<noteq> b)"
    8.43 +  by (simp_all add: xor3_def)
    8.44 +
    8.45 +text {* Breaking up word equalities into equalities on their
    8.46 +bit lists. Equalities are generated and manipulated in the
    8.47 +reverse order to to_bl. *}
    8.48 +
    8.49 +lemma word_eq_rbl_eq:
    8.50 +  "(x = y) = (rev (to_bl x) = rev (to_bl y))"
    8.51 +  by simp
    8.52 +
    8.53 +lemma rbl_word_or:
    8.54 +  "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
    8.55 +  by (simp add: map2_def zip_rev bl_word_or rev_map)
    8.56 +
    8.57 +lemma rbl_word_and:
    8.58 +  "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
    8.59 +  by (simp add: map2_def zip_rev bl_word_and rev_map)
    8.60 +
    8.61 +lemma rbl_word_xor:
    8.62 +  "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
    8.63 +  by (simp add: map2_def zip_rev bl_word_xor rev_map)
    8.64 +
    8.65 +lemma rbl_word_not:
    8.66 +  "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
    8.67 +  by (simp add: bl_word_not rev_map)
    8.68 +
    8.69 +lemma bl_word_sub:
    8.70 +  "to_bl (x - y) = to_bl (x + (- y))"
    8.71 +  by (simp add: diff_def)
    8.72 +
    8.73 +lemma rbl_word_1:
    8.74 +  "rev (to_bl (1 :: ('a :: len0) word))
    8.75 +     = takefill False (len_of TYPE('a)) [True]"
    8.76 +  apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
    8.77 +   apply simp
    8.78 +  apply (simp only: rtb_rbl_ariths(1)[OF refl])
    8.79 +  apply simp
    8.80 +  apply (case_tac "len_of TYPE('a)")
    8.81 +   apply simp
    8.82 +  apply (simp add: takefill_alt)
    8.83 +  done
    8.84 +
    8.85 +lemma rbl_word_if:
    8.86 +  "rev (to_bl (if P then x else y))
    8.87 +      = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
    8.88 +  by (simp add: map2_def split_def)
    8.89 +
    8.90 +lemma rbl_add_carry_Cons:
    8.91 +  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
    8.92 +        = xor3 x y car # (if carry x y car then rbl_succ else id)
    8.93 +             (rbl_add xs ys)"
    8.94 +  by (simp add: carry_def xor3_def)
    8.95 +
    8.96 +lemma rbl_add_suc_carry_fold:
    8.97 +  "length xs = length ys \<Longrightarrow>
    8.98 +   \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
    8.99 +        = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
   8.100 +                 (zip xs ys) (\<lambda>_. [])) car"
   8.101 +  apply (erule list_induct2)
   8.102 +   apply simp
   8.103 +  apply (simp only: rbl_add_carry_Cons)
   8.104 +  apply simp
   8.105 +  done
   8.106 +
   8.107 +lemma to_bl_plus_carry:
   8.108 +  "to_bl (x + y)
   8.109 +     = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
   8.110 +                 (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
   8.111 +  using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
   8.112 +  apply (simp add: word_add_rbl[OF refl refl])
   8.113 +  apply (drule_tac x=False in spec)
   8.114 +  apply (simp add: zip_rev)
   8.115 +  done
   8.116 +
   8.117 +definition
   8.118 + "rbl_plus cin xs ys = foldr
   8.119 +       (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
   8.120 +       (zip xs ys) (\<lambda>_. []) cin"
   8.121 +
   8.122 +lemma rbl_plus_simps:
   8.123 +  "rbl_plus cin (x # xs) (y # ys)
   8.124 +      = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
   8.125 +  "rbl_plus cin [] ys = []"
   8.126 +  "rbl_plus cin xs [] = []"
   8.127 +  by (simp_all add: rbl_plus_def)
   8.128 +
   8.129 +lemma rbl_word_plus:
   8.130 +  "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
   8.131 +  by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
   8.132 +
   8.133 +definition
   8.134 + "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
   8.135 +
   8.136 +lemma rbl_succ2_simps:
   8.137 +  "rbl_succ2 b [] = []"
   8.138 +  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
   8.139 +  by (simp_all add: rbl_succ2_def)
   8.140 +
   8.141 +lemma twos_complement:
   8.142 +  "- x = word_succ (NOT x)"
   8.143 +  using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
   8.144 +  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
   8.145 +           del: word_add_not)
   8.146 +
   8.147 +lemma rbl_word_neg:
   8.148 +  "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
   8.149 +  by (simp add: twos_complement word_succ_rbl[OF refl]
   8.150 +                bl_word_not rev_map rbl_succ2_def)
   8.151 +
   8.152 +lemma rbl_word_cat:
   8.153 +  "rev (to_bl (word_cat x y :: ('a :: len0) word))
   8.154 +     = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
   8.155 +  by (simp add: word_cat_bl word_rev_tf)
   8.156 +
   8.157 +lemma rbl_word_slice:
   8.158 +  "rev (to_bl (slice n w :: ('a :: len0) word))
   8.159 +     = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
   8.160 +  apply (simp add: slice_take word_rev_tf rev_take)
   8.161 +  apply (cases "n < len_of TYPE('b)", simp_all)
   8.162 +  done
   8.163 +
   8.164 +lemma rbl_word_ucast:
   8.165 +  "rev (to_bl (ucast x :: ('a :: len0) word))
   8.166 +     = takefill False (len_of TYPE('a)) (rev (to_bl x))"
   8.167 +  apply (simp add: to_bl_ucast takefill_alt)
   8.168 +  apply (simp add: rev_drop)
   8.169 +  apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
   8.170 +   apply simp_all
   8.171 +  done
   8.172 +
   8.173 +lemma rbl_shiftl:
   8.174 +  "rev (to_bl (w << n)) = takefill False (size w)
   8.175 +     (replicate n False @ rev (to_bl w))"
   8.176 +  by (simp add: bl_shiftl takefill_alt word_size rev_drop)
   8.177 +
   8.178 +lemma rbl_shiftr:
   8.179 +  "rev (to_bl (w >> n)) = takefill False (size w)
   8.180 +     (drop n (rev (to_bl w)))"
   8.181 +  by (simp add: shiftr_slice rbl_word_slice word_size)
   8.182 +
   8.183 +definition
   8.184 + "drop_nonempty v n xs
   8.185 +     = (if n < length xs then drop n xs else [last (v # xs)])"
   8.186 +
   8.187 +lemma drop_nonempty_simps:
   8.188 +  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
   8.189 +  "drop_nonempty v 0 (x # xs) = (x # xs)"
   8.190 +  "drop_nonempty v n [] = [v]"
   8.191 +  by (simp_all add: drop_nonempty_def)
   8.192 +
   8.193 +definition
   8.194 +  "takefill_last x n xs = takefill (last (x # xs)) n xs"
   8.195 +
   8.196 +lemma takefill_last_simps:
   8.197 +  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
   8.198 +  "takefill_last z 0 xs = []"
   8.199 +  "takefill_last z n [] = replicate n z"
   8.200 +  apply (simp_all add: takefill_last_def)
   8.201 +  apply (simp_all add: takefill_alt)
   8.202 +  done
   8.203 +
   8.204 +lemma rbl_sshiftr:
   8.205 +  "rev (to_bl (w >>> n)) = 
   8.206 +     takefill_last False (size w) 
   8.207 +        (drop_nonempty False n (rev (to_bl w)))"
   8.208 +  apply (cases "n < size w")
   8.209 +   apply (simp add: bl_sshiftr takefill_last_def word_size
   8.210 +                    takefill_alt rev_take last_rev
   8.211 +                    drop_nonempty_def)
   8.212 +  apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
   8.213 +   apply (simp add: word_size takefill_last_def takefill_alt
   8.214 +                    last_rev word_msb_alt word_rev_tf
   8.215 +                    drop_nonempty_def take_Cons')
   8.216 +   apply (case_tac "len_of TYPE('a)", simp_all)
   8.217 +  apply (rule word_eqI)
   8.218 +  apply (simp add: nth_sshiftr word_size test_bit_of_bl
   8.219 +                   msb_nth)
   8.220 +  done
   8.221 +
   8.222 +lemma nth_word_of_int:
   8.223 +  "(word_of_int x :: ('a :: len0) word) !! n
   8.224 +      = (n < len_of TYPE('a) \<and> bin_nth x n)"
   8.225 +  apply (simp add: test_bit_bl word_size to_bl_of_bin)
   8.226 +  apply (subst conj_cong[OF refl], erule bin_nth_bl)
   8.227 +  apply (auto)
   8.228 +  done
   8.229 +
   8.230 +lemma nth_scast:
   8.231 +  "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
   8.232 +     = (n < len_of TYPE('b) \<and>
   8.233 +          (if n < len_of TYPE('a) - 1 then x !! n
   8.234 +           else x !! (len_of TYPE('a) - 1)))"
   8.235 +  by (simp add: scast_def nth_word_of_int nth_sint)
   8.236 +
   8.237 +lemma rbl_word_scast:
   8.238 +  "rev (to_bl (scast x :: ('a :: len) word))
   8.239 +     = takefill_last False (len_of TYPE('a))
   8.240 +           (rev (to_bl x))"
   8.241 +  apply (rule nth_equalityI)
   8.242 +   apply (simp add: word_size takefill_last_def)
   8.243 +  apply (clarsimp simp: nth_scast takefill_last_def
   8.244 +                        nth_takefill word_size nth_rev to_bl_nth)
   8.245 +  apply (cases "len_of TYPE('b)")
   8.246 +   apply simp
   8.247 +  apply (clarsimp simp: less_Suc_eq_le linorder_not_less
   8.248 +                        last_rev word_msb_alt[symmetric]
   8.249 +                        msb_nth)
   8.250 +  done
   8.251 +
   8.252 +definition
   8.253 +  rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
   8.254 +where
   8.255 + "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
   8.256 +    xs []"
   8.257 +
   8.258 +lemma rbl_mul_simps:
   8.259 +  "rbl_mul (x # xs) ys
   8.260 +     = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
   8.261 +  "rbl_mul [] ys = []"
   8.262 +  by (simp_all add: rbl_mul_def)
   8.263 +
   8.264 +lemma takefill_le2:
   8.265 +  "length xs \<le> n \<Longrightarrow>
   8.266 +   takefill x m (takefill x n xs)
   8.267 +     = takefill x m xs"
   8.268 +  by (simp add: takefill_alt replicate_add[symmetric])
   8.269 +
   8.270 +lemma take_rbl_plus:
   8.271 +  "\<forall>n b. take n (rbl_plus b xs ys)
   8.272 +    = rbl_plus b (take n xs) (take n ys)"
   8.273 +  apply (simp add: rbl_plus_def take_zip[symmetric])
   8.274 +  apply (rule_tac list="zip xs ys" in list.induct)
   8.275 +   apply simp
   8.276 +  apply (clarsimp simp: split_def)
   8.277 +  apply (case_tac n, simp_all)
   8.278 +  done
   8.279 +
   8.280 +lemma word_rbl_mul_induct:
   8.281 +  fixes y :: "'a :: len word" shows
   8.282 +  "length xs \<le> size y
   8.283 +   \<Longrightarrow> rbl_mul xs (rev (to_bl y))
   8.284 +     = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
   8.285 +proof (induct xs)
   8.286 +  case Nil
   8.287 +  show ?case
   8.288 +    by (simp add: rbl_mul_simps)
   8.289 +next
   8.290 +  case (Cons z zs)
   8.291 +
   8.292 +  have rbl_word_plus':
   8.293 +    "\<And>(x :: 'a word) y.
   8.294 +      to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
   8.295 +    by (simp add: rbl_word_plus[symmetric])
   8.296 +  
   8.297 +  have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
   8.298 +    apply (cases z)
   8.299 +     apply (simp cong: map_cong)
   8.300 +    apply (simp add: map_replicate_const cong: map_cong)
   8.301 +    done
   8.302 + 
   8.303 +  have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
   8.304 +    by (simp add: shiftl_t2n)
   8.305 +
   8.306 +  have zip_take_triv: "\<And>xs ys n. n = length ys
   8.307 +      \<Longrightarrow> zip (take n xs) ys = zip xs ys"
   8.308 +    by (rule nth_equalityI, simp_all)
   8.309 +
   8.310 +  show ?case
   8.311 +    using Cons
   8.312 +    apply (simp add: trans [OF of_bl_append add_commute]
   8.313 +                     rbl_mul_simps rbl_word_plus'
   8.314 +                     Cons.hyps left_distrib mult_bit
   8.315 +                     shiftl rbl_shiftl)
   8.316 +    apply (simp add: takefill_alt word_size rev_map take_rbl_plus
   8.317 +                     min_def)
   8.318 +    apply (simp add: rbl_plus_def zip_take_triv)
   8.319 +    done
   8.320 +qed
   8.321 +
   8.322 +lemma rbl_word_mul:
   8.323 +  fixes x :: "'a :: len word"
   8.324 +  shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
   8.325 +  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
   8.326 +  by (simp add: word_size)
   8.327 +
   8.328 +text {* Breaking up inequalities into bitlist properties. *}
   8.329 +
   8.330 +definition
   8.331 +  "rev_bl_order F xs ys =
   8.332 +     (length xs = length ys \<and>
   8.333 +       ((xs = ys \<and> F)
   8.334 +          \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
   8.335 +                   \<and> \<not> xs ! n \<and> ys ! n)))"
   8.336 +
   8.337 +lemma rev_bl_order_simps:
   8.338 +  "rev_bl_order F [] [] = F"
   8.339 +  "rev_bl_order F (x # xs) (y # ys)
   8.340 +     = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
   8.341 +  apply (simp_all add: rev_bl_order_def)
   8.342 +  apply (rule conj_cong[OF refl])
   8.343 +  apply (cases "xs = ys")
   8.344 +   apply (simp add: nth_Cons')
   8.345 +   apply blast
   8.346 +  apply (simp add: nth_Cons')
   8.347 +  apply safe
   8.348 +   apply (rule_tac x="n - 1" in exI)
   8.349 +   apply simp
   8.350 +  apply (rule_tac x="Suc n" in exI)
   8.351 +  apply simp
   8.352 +  done
   8.353 +
   8.354 +lemma rev_bl_order_rev_simp:
   8.355 +  "length xs = length ys \<Longrightarrow>
   8.356 +   rev_bl_order F (xs @ [x]) (ys @ [y])
   8.357 +     = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
   8.358 +  apply (induct arbitrary: F rule: list_induct2)
   8.359 +   apply (auto simp add: rev_bl_order_simps)
   8.360 +  done
   8.361 +
   8.362 +lemma rev_bl_order_bl_to_bin:
   8.363 +  "length xs = length ys
   8.364 +     \<Longrightarrow> rev_bl_order True xs ys
   8.365 +            = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
   8.366 +       \<and> rev_bl_order False xs ys
   8.367 +            = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
   8.368 +  apply (induct xs ys rule: list_induct2)
   8.369 +   apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
   8.370 +  apply (simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq)
   8.371 +  apply arith?
   8.372 +  done
   8.373 +
   8.374 +lemma word_le_rbl:
   8.375 +  fixes x :: "('a :: len0) word"
   8.376 +  shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
   8.377 +  by (simp add: rev_bl_order_bl_to_bin word_le_def)
   8.378 +
   8.379 +lemma word_less_rbl:
   8.380 +  fixes x :: "('a :: len0) word"
   8.381 +  shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
   8.382 +  by (simp add: word_less_alt rev_bl_order_bl_to_bin)
   8.383 +
   8.384 +lemma word_sint_msb_eq:
   8.385 +  "sint x = uint x - (if msb x then 2 ^ size x else 0)"
   8.386 +  apply (cases "msb x")
   8.387 +   apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
   8.388 +    apply (simp add: word_size wi_hom_syms
   8.389 +                     word_of_int_2p_len)
   8.390 +   apply (simp add: sints_num word_size)
   8.391 +   apply (rule conjI)
   8.392 +    apply (simp add: le_diff_eq')
   8.393 +    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
   8.394 +     apply (simp add: power_Suc[symmetric])
   8.395 +    apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
   8.396 +    apply (rule notI, drule word_eqD[where x="size x - 1"])
   8.397 +    apply (simp add: msb_nth word_ops_nth_size word_size)
   8.398 +   apply (simp add: order_less_le_trans[where y=0])
   8.399 +  apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
   8.400 +  apply (simp add: linorder_not_less uints_num word_msb_sint)
   8.401 +  apply (rule order_less_le_trans[OF sint_lt])
   8.402 +  apply simp
   8.403 +  done
   8.404 +
   8.405 +lemma word_sle_msb_le:
   8.406 +  "(x <=s y) = ((msb y --> msb x) \<and> 
   8.407 +                  ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
   8.408 +  apply (simp add: word_sle_def word_sint_msb_eq word_size
   8.409 +                   word_le_def)
   8.410 +  apply safe
   8.411 +   apply (rule order_trans[OF _ uint_ge_0])
   8.412 +   apply (simp add: order_less_imp_le)
   8.413 +  apply (erule notE[OF leD])
   8.414 +  apply (rule order_less_le_trans[OF _ uint_ge_0])
   8.415 +  apply simp
   8.416 +  done
   8.417 +
   8.418 +lemma word_sless_msb_less:
   8.419 +  "(x <s y) = ((msb y --> msb x) \<and> 
   8.420 +                  ((msb x \<and> \<not> msb y) \<or> (x < y)))"
   8.421 +  by (auto simp add: word_sless_def word_sle_msb_le)
   8.422 +
   8.423 +definition
   8.424 +  "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
   8.425 +
   8.426 +lemma map_last_simps:
   8.427 +  "map_last f [] = []"
   8.428 +  "map_last f [x] = [f x]"
   8.429 +  "map_last f (x # y # zs) = x # map_last f (y # zs)"
   8.430 +  by (simp_all add: map_last_def)
   8.431 +
   8.432 +lemma word_sle_rbl:
   8.433 +  "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
   8.434 +     (map_last Not (rev (to_bl y)))"
   8.435 +  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   8.436 +  apply (simp add: word_sle_msb_le word_le_rbl)
   8.437 +  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   8.438 +   apply (cases "to_bl x", simp)
   8.439 +   apply (cases "to_bl y", simp)
   8.440 +   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   8.441 +   apply auto
   8.442 +  done
   8.443 +
   8.444 +lemma word_sless_rbl:
   8.445 +  "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
   8.446 +     (map_last Not (rev (to_bl y)))"
   8.447 +  using word_msb_alt[where w=x] word_msb_alt[where w=y]
   8.448 +  apply (simp add: word_sless_msb_less word_less_rbl)
   8.449 +  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
   8.450 +   apply (cases "to_bl x", simp)
   8.451 +   apply (cases "to_bl y", simp)
   8.452 +   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
   8.453 +   apply auto
   8.454 +  done
   8.455 +
   8.456 +text {* Lemmas for unpacking rev (to_bl n) for numerals n and also
   8.457 +for irreducible values and expressions. *}
   8.458 +
   8.459 +lemma rev_bin_to_bl_simps:
   8.460 +  "rev (bin_to_bl 0 x) = []"
   8.461 +  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
   8.462 +    = False # rev (bin_to_bl n (numeral nm))"
   8.463 +  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
   8.464 +    = True # rev (bin_to_bl n (numeral nm))"
   8.465 +  "rev (bin_to_bl (Suc n) (numeral (num.One)))
   8.466 +    = True # replicate n False"
   8.467 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm)))
   8.468 +    = False # rev (bin_to_bl n (neg_numeral nm))"
   8.469 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm)))
   8.470 +    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   8.471 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.One)))
   8.472 +    = True # replicate n True"
   8.473 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm + num.One)))
   8.474 +    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   8.475 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm + num.One)))
   8.476 +    = False # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
   8.477 +  "rev (bin_to_bl (Suc n) (neg_numeral (num.One + num.One)))
   8.478 +    = False # rev (bin_to_bl n (neg_numeral num.One))"
   8.479 +  apply (simp_all add: bin_to_bl_def)
   8.480 +  apply (simp_all only: bin_to_bl_aux_alt)
   8.481 +  apply (simp_all)
   8.482 +  apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
   8.483 +  done
   8.484 +
   8.485 +lemma to_bl_upt:
   8.486 +  "to_bl x = rev (map (op !! x) [0 ..< size x])"
   8.487 +  apply (rule nth_equalityI)
   8.488 +   apply (simp add: word_size)
   8.489 +  apply (clarsimp simp: to_bl_nth word_size nth_rev)
   8.490 +  done
   8.491 +
   8.492 +lemma rev_to_bl_upt:
   8.493 +  "rev (to_bl x) = map (op !! x) [0 ..< size x]"
   8.494 +  by (simp add: to_bl_upt)
   8.495 +
   8.496 +lemma upt_eq_list_intros:
   8.497 +  "j <= i \<Longrightarrow> [i ..< j] = []"
   8.498 +  "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
   8.499 +  by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
   8.500 +
   8.501 +text {* Tactic definition *}
   8.502 +
   8.503 +ML {*
   8.504 +
   8.505 +structure Word_Bitwise_Tac = struct
   8.506 +
   8.507 +val word_ss = global_simpset_of @{theory Word};
   8.508 +
   8.509 +fun mk_nat_clist ns = List.foldr
   8.510 +  (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
   8.511 +  @{cterm "[] :: nat list"} ns;
   8.512 +
   8.513 +fun upt_conv ct = case term_of ct of
   8.514 +  (@{const upt} $ n $ m) => let
   8.515 +    val (i, j) = pairself (snd o HOLogic.dest_number) (n, m);
   8.516 +    val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
   8.517 +      |> mk_nat_clist;
   8.518 +    val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
   8.519 +                 |> Thm.apply @{cterm Trueprop};
   8.520 +  in Goal.prove_internal [] prop 
   8.521 +      (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
   8.522 +          ORELSE simp_tac word_ss 1))) |> mk_meta_eq |> SOME end
   8.523 +    handle TERM _ => NONE
   8.524 +  | _ => NONE;
   8.525 +
   8.526 +val expand_upt_simproc = Simplifier.make_simproc
   8.527 +  {lhss = [@{cpat "upt _ _"}],
   8.528 +   name = "expand_upt", identifier = [],
   8.529 +   proc = K (K upt_conv)};
   8.530 +
   8.531 +fun word_len_simproc_fn ct = case term_of ct of
   8.532 +    Const (@{const_name len_of}, _) $ t => (let
   8.533 +        val T = fastype_of t |> dest_Type |> snd |> the_single
   8.534 +        val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
   8.535 +        val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
   8.536 +                 |> Thm.apply @{cterm Trueprop};
   8.537 +      in Goal.prove_internal [] prop (K (simp_tac word_ss 1))
   8.538 +             |> mk_meta_eq |> SOME end
   8.539 +    handle TERM _ => NONE | TYPE _ => NONE)
   8.540 +  | _ => NONE;
   8.541 +
   8.542 +val word_len_simproc = Simplifier.make_simproc
   8.543 +  {lhss = [@{cpat "len_of _"}],
   8.544 +   name = "word_len", identifier = [],
   8.545 +   proc = K (K word_len_simproc_fn)};
   8.546 +
   8.547 +(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
   8.548 +   or just 5 (discarding nat) when n_sucs = 0 *)
   8.549 +
   8.550 +fun nat_get_Suc_simproc_fn n_sucs thy ct = let
   8.551 +    val (f $ arg) = (term_of ct);
   8.552 +    val n = (case arg of @{term nat} $ n => n | n => n)
   8.553 +      |> HOLogic.dest_number |> snd;
   8.554 +    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs)
   8.555 +      else (n, 0);
   8.556 +    val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j)
   8.557 +        (replicate i @{term Suc});
   8.558 +    val _ = if arg = arg' then raise TERM ("", []) else ();
   8.559 +    fun propfn g = HOLogic.mk_eq (g arg, g arg')
   8.560 +      |> HOLogic.mk_Trueprop |> cterm_of thy;
   8.561 +    val eq1 = Goal.prove_internal [] (propfn I)
   8.562 +      (K (simp_tac word_ss 1));
   8.563 +  in Goal.prove_internal [] (propfn (curry (op $) f))
   8.564 +      (K (simp_tac (HOL_ss addsimps [eq1]) 1))
   8.565 +       |> mk_meta_eq |> SOME end
   8.566 +    handle TERM _ => NONE;
   8.567 +
   8.568 +fun nat_get_Suc_simproc n_sucs thy cts = Simplifier.make_simproc
   8.569 +  {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
   8.570 +   name = "nat_get_Suc", identifier = [],
   8.571 +   proc = K (K (nat_get_Suc_simproc_fn n_sucs thy))};
   8.572 +
   8.573 +val no_split_ss = Splitter.del_split @{thm split_if} HOL_ss;
   8.574 +
   8.575 +val expand_word_eq_sss = (HOL_basic_ss addsimps
   8.576 +       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl},
   8.577 +  [no_split_ss addsimps @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
   8.578 +                                rbl_word_neg bl_word_sub rbl_word_xor
   8.579 +                                rbl_word_cat rbl_word_slice rbl_word_scast
   8.580 +                                rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
   8.581 +                                rbl_word_if},
   8.582 +   no_split_ss addsimps @{thms to_bl_numeral to_bl_neg_numeral
   8.583 +                               to_bl_0 rbl_word_1},
   8.584 +   no_split_ss addsimps @{thms rev_rev_ident
   8.585 +                                rev_replicate rev_map to_bl_upt word_size}
   8.586 +          addsimprocs [word_len_simproc],
   8.587 +   no_split_ss addsimps @{thms list.simps split_conv replicate.simps map.simps
   8.588 +                                zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
   8.589 +                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
   8.590 +                                takefill_Suc_Nil takefill.Z rbl_succ2_simps
   8.591 +                                rbl_plus_simps rev_bin_to_bl_simps append.simps
   8.592 +                                takefill_last_simps drop_nonempty_simps
   8.593 +                                rev_bl_order_simps}
   8.594 +          addsimprocs [expand_upt_simproc,
   8.595 +                       nat_get_Suc_simproc 4 @{theory}
   8.596 +                         [@{cpat replicate}, @{cpat "takefill ?x"},
   8.597 +                          @{cpat drop}, @{cpat "bin_to_bl"},
   8.598 +                          @{cpat "takefill_last ?x"},
   8.599 +                          @{cpat "drop_nonempty ?x"}]],
   8.600 +    no_split_ss addsimps @{thms xor3_simps carry_simps if_bool_simps}
   8.601 +  ])
   8.602 +
   8.603 +val tac = let
   8.604 +    val (ss, sss) = expand_word_eq_sss;
   8.605 +    val st = generic_simp_tac true (true, false, false);
   8.606 +  in foldr1 (op THEN_ALL_NEW) ((CHANGED o st ss) :: map st sss) end;
   8.607 +
   8.608 +end
   8.609 +
   8.610 +*}
   8.611 +
   8.612 +method_setup word_bitwise =
   8.613 +  {* Scan.succeed (K (Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac 1)))  *}
   8.614 +  "decomposer for word equalities and inequalities into bit propositions"
   8.615 +
   8.616 +end