# HG changeset patch
# User Thomas Sewell <thomas.sewell@nicta.com.au>
# Date 1334643707 -36000
# Node ID 407cabf66f2166a771ece9f9b1f82a61e1e897c3
# Parent  c201a1fe0a81efdb368a861009cf1f82c56fc1db
New tactic "word_bitwise" expands word equalities/inequalities into logic.

diff -r c201a1fe0a81 -r 407cabf66f21 CONTRIBUTORS
--- a/CONTRIBUTORS	Wed Apr 18 23:57:44 2012 +0200
+++ b/CONTRIBUTORS	Tue Apr 17 16:21:47 2012 +1000
@@ -6,6 +6,10 @@
 Contributions to Isabelle2012
 -----------------------------
 
+* April 2012: Thomas Sewell, NICTA
+    (based on work done with Sascha Boehme, TUM in 2010)
+  WordBitwise: logic/circuit expansion of bitvector equalities/inequalities.
+
 * March 2012: Christian Sternagel, Japan Advanced Institute of Science
   and Technology
   Consolidated theory of relation composition.
diff -r c201a1fe0a81 -r 407cabf66f21 NEWS
--- a/NEWS	Wed Apr 18 23:57:44 2012 +0200
+++ b/NEWS	Tue Apr 17 16:21:47 2012 +1000
@@ -521,6 +521,14 @@
   word_of_int_0_hom ~> word_0_wi
   word_of_int_1_hom ~> word_1_wi
 
+* New tactic "word_bitwise" for splitting machine word equalities and
+inequalities into logical circuits. Requires theory "WordBitwise" from HOL-Word
+session. Supports addition, subtraction, multiplication, shifting by
+constants, bitwise operators and numeric constants. Requires fixed-length word
+types, cannot operate on 'a word. Solves many standard word identies outright
+and converts more into first order problems amenable to blast or similar. See
+HOL/Word/WordBitwise.thy and examples in HOL/Word/Examples/WordExamples.thy.
+
 * Clarified attribute "mono_set": pure declaration without modifying
 the result of the fact expression.
 
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Apr 18 23:57:44 2012 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 17 16:21:47 2012 +1000
@@ -1265,8 +1265,8 @@
   Library/Numeral_Type.thy Word/Misc_Numeric.thy Word/Misc_Typedef.thy	\
   Word/Type_Length.thy Word/Bit_Representation.thy Word/Bit_Int.thy	\
   Word/Bool_List_Representation.thy Word/Bit_Operations.thy		\
-  Word/Word.thy Word/document/root.tex					\
-  Word/document/root.bib Word/Tools/smt_word.ML
+  Word/Word.thy Word/WordBitwise.thy Word/document/root.tex		\
+  Word/document/root.bib Word/Tools/smt_word.ML Word/Tools/word_lib.ML
 	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 
 
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Wed Apr 18 23:57:44 2012 +0200
+++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Apr 17 16:21:47 2012 +1000
@@ -1,5 +1,5 @@
 (* 
-  Author: Gerwin Klein, NICTA
+  Authors: Gerwin Klein and Thomas Sewell, NICTA
 
   Examples demonstrating and testing various word operations.
 *)
@@ -7,7 +7,7 @@
 header "Examples of word operations"
 
 theory WordExamples
-imports "../Word"
+imports "../Word" "../WordBitwise"
 begin
 
 type_synonym word32 = "32 word"
@@ -164,4 +164,39 @@
   finally show ?thesis .
 qed
 
+text "alternative proof using bitwise expansion"
+
+lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
+  by word_bitwise
+
+text "more proofs using bitwise expansion"
+
+lemma "((x :: 10 word) AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+  by word_bitwise
+
+lemma "(((x :: 12 word) AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+  by word_bitwise
+
+text "some problems require further reasoning after bit expansion"
+
+lemma "x \<le> (42 :: 8 word) \<Longrightarrow> x \<le> 89"
+  apply word_bitwise
+  apply blast
+  done
+
+lemma "((x :: word32) AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+  apply word_bitwise
+  apply clarsimp
+  done
+
+text "operations like shifts by non-numerals will expose some internal list
+ representations but may still be easy to solve"
+
+lemma shiftr_overflow:
+  "32 \<le> a \<Longrightarrow> (b::word32) >> a = 0"
+  apply (word_bitwise)
+  apply simp
+  done
+
+
 end
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Wed Apr 18 23:57:44 2012 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML	Tue Apr 17 16:21:47 2012 +1000
@@ -12,23 +12,7 @@
 structure SMT_Word: SMT_WORD =
 struct
 
-
-(* utilities *)
-
-fun dest_binT T =
-  (case T of
-    Type (@{type_name "Numeral_Type.num0"}, _) => 0
-  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
-  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
-  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
-  | _ => raise TYPE ("dest_binT", [T], []))
-
-fun is_wordT (Type (@{type_name word}, _)) = true
-  | is_wordT _ = false
-
-fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
-  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
-
+open Word_Lib
 
 (* SMT-LIB logic *)
 
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/Word/Tools/word_lib.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Tools/word_lib.ML	Tue Apr 17 16:21:47 2012 +1000
@@ -0,0 +1,40 @@
+(*  Title:      HOL/Word/Tools/word_lib.ML
+    Author:     Sascha Boehme, TU Muenchen and Thomas Sewell, NICTA
+
+Helper routines for operating on the word type at the ML level.
+*)
+
+
+structure Word_Lib = struct
+
+fun dest_binT T =
+  (case T of
+    Type (@{type_name "Numeral_Type.num0"}, _) => 0
+  | Type (@{type_name "Numeral_Type.num1"}, _) => 1
+  | Type (@{type_name "Numeral_Type.bit0"}, [T]) => 2 * dest_binT T
+  | Type (@{type_name "Numeral_Type.bit1"}, [T]) => 1 + 2 * dest_binT T
+  | _ => raise TYPE ("dest_binT", [T], []))
+
+fun is_wordT (Type (@{type_name word}, _)) = true
+  | is_wordT _ = false
+
+fun dest_wordT (Type (@{type_name word}, [T])) = dest_binT T
+  | dest_wordT T = raise TYPE ("dest_wordT", [T], [])
+
+local
+  fun mk_bitT i T =
+    if i = 0
+    then Type (@{type_name "Numeral_Type.bit0"}, [T])
+    else Type (@{type_name "Numeral_Type.bit1"}, [T])
+
+  fun mk_binT size = 
+    if size = 0 then @{typ "Numeral_Type.num0"}
+    else if size = 1 then @{typ "Numeral_Type.num1"}
+    else let val (q, r) = Integer.div_mod size 2 in mk_bitT r (mk_binT q) end
+in
+fun mk_wordT size =
+  if size >= 0 then Type (@{type_name "word"}, [mk_binT size])
+  else raise TYPE ("mk_wordT: " ^ quote (string_of_int size), [], [])
+end
+
+end
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Apr 18 23:57:44 2012 +0200
+++ b/src/HOL/Word/Word.thy	Tue Apr 17 16:21:47 2012 +1000
@@ -10,7 +10,9 @@
   Misc_Typedef
   "~~/src/HOL/Library/Boolean_Algebra"
   Bool_List_Representation
-uses ("~~/src/HOL/Word/Tools/smt_word.ML")
+uses
+  ("~~/src/HOL/Word/Tools/smt_word.ML")
+  ("~~/src/HOL/Word/Tools/word_lib.ML")
 begin
 
 text {* see @{text "Examples/WordExamples.thy"} for examples *}
@@ -4642,7 +4644,7 @@
 
 declare bin_to_bl_def [simp]
 
-
+use "~~/src/HOL/Word/Tools/word_lib.ML"
 use "~~/src/HOL/Word/Tools/smt_word.ML"
 setup {* SMT_Word.setup *}
 
diff -r c201a1fe0a81 -r 407cabf66f21 src/HOL/Word/WordBitwise.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/WordBitwise.thy	Tue Apr 17 16:21:47 2012 +1000
@@ -0,0 +1,613 @@
+(*  Title:      HOL/Word/WordBitwise.thy
+    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
+*)
+
+
+theory WordBitwise
+
+imports Word
+
+begin
+
+text {* Helper constants used in defining addition *}
+
+definition
+  xor3 :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+where
+ "xor3 a b c = (a = (b = c))"
+
+definition
+  carry :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool"
+where
+ "carry a b c = ((a \<and> (b \<or> c)) \<or> (b \<and> c))"
+
+lemma carry_simps:
+  "carry True a b = (a \<or> b)"
+  "carry a True b = (a \<or> b)"
+  "carry a b True = (a \<or> b)"
+  "carry False a b = (a \<and> b)"
+  "carry a False b = (a \<and> b)"
+  "carry a b False = (a \<and> b)"
+  by (auto simp add: carry_def)
+
+lemma xor3_simps:
+  "xor3 True a b = (a = b)"
+  "xor3 a True b = (a = b)"
+  "xor3 a b True = (a = b)"
+  "xor3 False a b = (a \<noteq> b)"
+  "xor3 a False b = (a \<noteq> b)"
+  "xor3 a b False = (a \<noteq> b)"
+  by (simp_all add: xor3_def)
+
+text {* Breaking up word equalities into equalities on their
+bit lists. Equalities are generated and manipulated in the
+reverse order to to_bl. *}
+
+lemma word_eq_rbl_eq:
+  "(x = y) = (rev (to_bl x) = rev (to_bl y))"
+  by simp
+
+lemma rbl_word_or:
+  "rev (to_bl (x OR y)) = map2 op \<or> (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: map2_def zip_rev bl_word_or rev_map)
+
+lemma rbl_word_and:
+  "rev (to_bl (x AND y)) = map2 op \<and> (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: map2_def zip_rev bl_word_and rev_map)
+
+lemma rbl_word_xor:
+  "rev (to_bl (x XOR y)) = map2 op \<noteq> (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: map2_def zip_rev bl_word_xor rev_map)
+
+lemma rbl_word_not:
+  "rev (to_bl (NOT x)) = map Not (rev (to_bl x))"
+  by (simp add: bl_word_not rev_map)
+
+lemma bl_word_sub:
+  "to_bl (x - y) = to_bl (x + (- y))"
+  by (simp add: diff_def)
+
+lemma rbl_word_1:
+  "rev (to_bl (1 :: ('a :: len0) word))
+     = takefill False (len_of TYPE('a)) [True]"
+  apply (rule_tac s="rev (to_bl (word_succ (0 :: 'a word)))" in trans)
+   apply simp
+  apply (simp only: rtb_rbl_ariths(1)[OF refl])
+  apply simp
+  apply (case_tac "len_of TYPE('a)")
+   apply simp
+  apply (simp add: takefill_alt)
+  done
+
+lemma rbl_word_if:
+  "rev (to_bl (if P then x else y))
+      = map2 (If P) (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: map2_def split_def)
+
+lemma rbl_add_carry_Cons:
+  "(if car then rbl_succ else id) (rbl_add (x # xs) (y # ys))
+        = xor3 x y car # (if carry x y car then rbl_succ else id)
+             (rbl_add xs ys)"
+  by (simp add: carry_def xor3_def)
+
+lemma rbl_add_suc_carry_fold:
+  "length xs = length ys \<Longrightarrow>
+   \<forall>car. (if car then rbl_succ else id) (rbl_add xs ys)
+        = (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
+                 (zip xs ys) (\<lambda>_. [])) car"
+  apply (erule list_induct2)
+   apply simp
+  apply (simp only: rbl_add_carry_Cons)
+  apply simp
+  done
+
+lemma to_bl_plus_carry:
+  "to_bl (x + y)
+     = rev (foldr (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
+                 (rev (zip (to_bl x) (to_bl y))) (\<lambda>_. []) False)"
+  using rbl_add_suc_carry_fold[where xs="rev (to_bl x)" and ys="rev (to_bl y)"]
+  apply (simp add: word_add_rbl[OF refl refl])
+  apply (drule_tac x=False in spec)
+  apply (simp add: zip_rev)
+  done
+
+definition
+ "rbl_plus cin xs ys = foldr
+       (\<lambda>(x, y) res car. xor3 x y car # res (carry x y car))
+       (zip xs ys) (\<lambda>_. []) cin"
+
+lemma rbl_plus_simps:
+  "rbl_plus cin (x # xs) (y # ys)
+      = xor3 x y cin # rbl_plus (carry x y cin) xs ys"
+  "rbl_plus cin [] ys = []"
+  "rbl_plus cin xs [] = []"
+  by (simp_all add: rbl_plus_def)
+
+lemma rbl_word_plus:
+  "rev (to_bl (x + y)) = rbl_plus False (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: rbl_plus_def to_bl_plus_carry zip_rev)
+
+definition
+ "rbl_succ2 b xs = (if b then rbl_succ xs else xs)"
+
+lemma rbl_succ2_simps:
+  "rbl_succ2 b [] = []"
+  "rbl_succ2 b (x # xs) = (b \<noteq> x) # rbl_succ2 (x \<and> b) xs"
+  by (simp_all add: rbl_succ2_def)
+
+lemma twos_complement:
+  "- x = word_succ (NOT x)"
+  using arg_cong[OF word_add_not[where x=x], where f="\<lambda>a. a - x + 1"]
+  by (simp add: word_succ_p1 word_sp_01[unfolded word_succ_p1]
+           del: word_add_not)
+
+lemma rbl_word_neg:
+  "rev (to_bl (- x)) = rbl_succ2 True (map Not (rev (to_bl x)))"
+  by (simp add: twos_complement word_succ_rbl[OF refl]
+                bl_word_not rev_map rbl_succ2_def)
+
+lemma rbl_word_cat:
+  "rev (to_bl (word_cat x y :: ('a :: len0) word))
+     = takefill False (len_of TYPE('a)) (rev (to_bl y) @ rev (to_bl x))"
+  by (simp add: word_cat_bl word_rev_tf)
+
+lemma rbl_word_slice:
+  "rev (to_bl (slice n w :: ('a :: len0) word))
+     = takefill False (len_of TYPE('a)) (drop n (rev (to_bl w)))"
+  apply (simp add: slice_take word_rev_tf rev_take)
+  apply (cases "n < len_of TYPE('b)", simp_all)
+  done
+
+lemma rbl_word_ucast:
+  "rev (to_bl (ucast x :: ('a :: len0) word))
+     = takefill False (len_of TYPE('a)) (rev (to_bl x))"
+  apply (simp add: to_bl_ucast takefill_alt)
+  apply (simp add: rev_drop)
+  apply (case_tac "len_of TYPE('a) < len_of TYPE('b)")
+   apply simp_all
+  done
+
+lemma rbl_shiftl:
+  "rev (to_bl (w << n)) = takefill False (size w)
+     (replicate n False @ rev (to_bl w))"
+  by (simp add: bl_shiftl takefill_alt word_size rev_drop)
+
+lemma rbl_shiftr:
+  "rev (to_bl (w >> n)) = takefill False (size w)
+     (drop n (rev (to_bl w)))"
+  by (simp add: shiftr_slice rbl_word_slice word_size)
+
+definition
+ "drop_nonempty v n xs
+     = (if n < length xs then drop n xs else [last (v # xs)])"
+
+lemma drop_nonempty_simps:
+  "drop_nonempty v (Suc n) (x # xs) = drop_nonempty x n xs"
+  "drop_nonempty v 0 (x # xs) = (x # xs)"
+  "drop_nonempty v n [] = [v]"
+  by (simp_all add: drop_nonempty_def)
+
+definition
+  "takefill_last x n xs = takefill (last (x # xs)) n xs"
+
+lemma takefill_last_simps:
+  "takefill_last z (Suc n) (x # xs) = x # takefill_last x n xs"
+  "takefill_last z 0 xs = []"
+  "takefill_last z n [] = replicate n z"
+  apply (simp_all add: takefill_last_def)
+  apply (simp_all add: takefill_alt)
+  done
+
+lemma rbl_sshiftr:
+  "rev (to_bl (w >>> n)) = 
+     takefill_last False (size w) 
+        (drop_nonempty False n (rev (to_bl w)))"
+  apply (cases "n < size w")
+   apply (simp add: bl_sshiftr takefill_last_def word_size
+                    takefill_alt rev_take last_rev
+                    drop_nonempty_def)
+  apply (subgoal_tac "(w >>> n) = of_bl (replicate (size w) (msb w))")
+   apply (simp add: word_size takefill_last_def takefill_alt
+                    last_rev word_msb_alt word_rev_tf
+                    drop_nonempty_def take_Cons')
+   apply (case_tac "len_of TYPE('a)", simp_all)
+  apply (rule word_eqI)
+  apply (simp add: nth_sshiftr word_size test_bit_of_bl
+                   msb_nth)
+  done
+
+lemma nth_word_of_int:
+  "(word_of_int x :: ('a :: len0) word) !! n
+      = (n < len_of TYPE('a) \<and> bin_nth x n)"
+  apply (simp add: test_bit_bl word_size to_bl_of_bin)
+  apply (subst conj_cong[OF refl], erule bin_nth_bl)
+  apply (auto)
+  done
+
+lemma nth_scast:
+  "(scast (x :: ('a :: len) word) :: ('b :: len) word) !! n
+     = (n < len_of TYPE('b) \<and>
+          (if n < len_of TYPE('a) - 1 then x !! n
+           else x !! (len_of TYPE('a) - 1)))"
+  by (simp add: scast_def nth_word_of_int nth_sint)
+
+lemma rbl_word_scast:
+  "rev (to_bl (scast x :: ('a :: len) word))
+     = takefill_last False (len_of TYPE('a))
+           (rev (to_bl x))"
+  apply (rule nth_equalityI)
+   apply (simp add: word_size takefill_last_def)
+  apply (clarsimp simp: nth_scast takefill_last_def
+                        nth_takefill word_size nth_rev to_bl_nth)
+  apply (cases "len_of TYPE('b)")
+   apply simp
+  apply (clarsimp simp: less_Suc_eq_le linorder_not_less
+                        last_rev word_msb_alt[symmetric]
+                        msb_nth)
+  done
+
+definition
+  rbl_mul :: "bool list \<Rightarrow> bool list \<Rightarrow> bool list"
+where
+ "rbl_mul xs ys = foldr (\<lambda>x sm. rbl_plus False (map (op \<and> x) ys) (False # sm))
+    xs []"
+
+lemma rbl_mul_simps:
+  "rbl_mul (x # xs) ys
+     = rbl_plus False (map (op \<and> x) ys) (False # rbl_mul xs ys)"
+  "rbl_mul [] ys = []"
+  by (simp_all add: rbl_mul_def)
+
+lemma takefill_le2:
+  "length xs \<le> n \<Longrightarrow>
+   takefill x m (takefill x n xs)
+     = takefill x m xs"
+  by (simp add: takefill_alt replicate_add[symmetric])
+
+lemma take_rbl_plus:
+  "\<forall>n b. take n (rbl_plus b xs ys)
+    = rbl_plus b (take n xs) (take n ys)"
+  apply (simp add: rbl_plus_def take_zip[symmetric])
+  apply (rule_tac list="zip xs ys" in list.induct)
+   apply simp
+  apply (clarsimp simp: split_def)
+  apply (case_tac n, simp_all)
+  done
+
+lemma word_rbl_mul_induct:
+  fixes y :: "'a :: len word" shows
+  "length xs \<le> size y
+   \<Longrightarrow> rbl_mul xs (rev (to_bl y))
+     = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+proof (induct xs)
+  case Nil
+  show ?case
+    by (simp add: rbl_mul_simps)
+next
+  case (Cons z zs)
+
+  have rbl_word_plus':
+    "\<And>(x :: 'a word) y.
+      to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+    by (simp add: rbl_word_plus[symmetric])
+  
+  have mult_bit: "to_bl (of_bl [z] * y) = map (op \<and> z) (to_bl y)"
+    apply (cases z)
+     apply (simp cong: map_cong)
+    apply (simp add: map_replicate_const cong: map_cong)
+    done
+ 
+  have shiftl: "\<And>xs. of_bl xs * 2 * y = (of_bl xs * y) << 1"
+    by (simp add: shiftl_t2n)
+
+  have zip_take_triv: "\<And>xs ys n. n = length ys
+      \<Longrightarrow> zip (take n xs) ys = zip xs ys"
+    by (rule nth_equalityI, simp_all)
+
+  show ?case
+    using Cons
+    apply (simp add: trans [OF of_bl_append add_commute]
+                     rbl_mul_simps rbl_word_plus'
+                     Cons.hyps left_distrib mult_bit
+                     shiftl rbl_shiftl)
+    apply (simp add: takefill_alt word_size rev_map take_rbl_plus
+                     min_def)
+    apply (simp add: rbl_plus_def zip_take_triv)
+    done
+qed
+
+lemma rbl_word_mul:
+  fixes x :: "'a :: len word"
+  shows "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
+  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y]
+  by (simp add: word_size)
+
+text {* Breaking up inequalities into bitlist properties. *}
+
+definition
+  "rev_bl_order F xs ys =
+     (length xs = length ys \<and>
+       ((xs = ys \<and> F)
+          \<or> (\<exists>n < length xs. drop (Suc n) xs = drop (Suc n) ys
+                   \<and> \<not> xs ! n \<and> ys ! n)))"
+
+lemma rev_bl_order_simps:
+  "rev_bl_order F [] [] = F"
+  "rev_bl_order F (x # xs) (y # ys)
+     = rev_bl_order ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> F)) xs ys"
+  apply (simp_all add: rev_bl_order_def)
+  apply (rule conj_cong[OF refl])
+  apply (cases "xs = ys")
+   apply (simp add: nth_Cons')
+   apply blast
+  apply (simp add: nth_Cons')
+  apply safe
+   apply (rule_tac x="n - 1" in exI)
+   apply simp
+  apply (rule_tac x="Suc n" in exI)
+  apply simp
+  done
+
+lemma rev_bl_order_rev_simp:
+  "length xs = length ys \<Longrightarrow>
+   rev_bl_order F (xs @ [x]) (ys @ [y])
+     = ((y \<and> \<not> x) \<or> ((y \<or> \<not> x) \<and> rev_bl_order F xs ys))"
+  apply (induct arbitrary: F rule: list_induct2)
+   apply (auto simp add: rev_bl_order_simps)
+  done
+
+lemma rev_bl_order_bl_to_bin:
+  "length xs = length ys
+     \<Longrightarrow> rev_bl_order True xs ys
+            = (bl_to_bin (rev xs) \<le> bl_to_bin (rev ys))
+       \<and> rev_bl_order False xs ys
+            = (bl_to_bin (rev xs) < bl_to_bin (rev ys))"
+  apply (induct xs ys rule: list_induct2)
+   apply (simp_all add: rev_bl_order_simps bl_to_bin_app_cat)
+  apply (simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq)
+  apply arith?
+  done
+
+lemma word_le_rbl:
+  fixes x :: "('a :: len0) word"
+  shows "(x \<le> y) = rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: rev_bl_order_bl_to_bin word_le_def)
+
+lemma word_less_rbl:
+  fixes x :: "('a :: len0) word"
+  shows "(x < y) = rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+  by (simp add: word_less_alt rev_bl_order_bl_to_bin)
+
+lemma word_sint_msb_eq:
+  "sint x = uint x - (if msb x then 2 ^ size x else 0)"
+  apply (cases "msb x")
+   apply (rule word_sint.Abs_eqD[where 'a='a], simp_all)
+    apply (simp add: word_size wi_hom_syms
+                     word_of_int_2p_len)
+   apply (simp add: sints_num word_size)
+   apply (rule conjI)
+    apply (simp add: le_diff_eq')
+    apply (rule order_trans[where y="2 ^ (len_of TYPE('a) - 1)"])
+     apply (simp add: power_Suc[symmetric])
+    apply (simp add: linorder_not_less[symmetric] mask_eq_iff[symmetric])
+    apply (rule notI, drule word_eqD[where x="size x - 1"])
+    apply (simp add: msb_nth word_ops_nth_size word_size)
+   apply (simp add: order_less_le_trans[where y=0])
+  apply (rule word_uint.Abs_eqD[where 'a='a], simp_all)
+  apply (simp add: linorder_not_less uints_num word_msb_sint)
+  apply (rule order_less_le_trans[OF sint_lt])
+  apply simp
+  done
+
+lemma word_sle_msb_le:
+  "(x <=s y) = ((msb y --> msb x) \<and> 
+                  ((msb x \<and> \<not> msb y) \<or> (x <= y)))"
+  apply (simp add: word_sle_def word_sint_msb_eq word_size
+                   word_le_def)
+  apply safe
+   apply (rule order_trans[OF _ uint_ge_0])
+   apply (simp add: order_less_imp_le)
+  apply (erule notE[OF leD])
+  apply (rule order_less_le_trans[OF _ uint_ge_0])
+  apply simp
+  done
+
+lemma word_sless_msb_less:
+  "(x <s y) = ((msb y --> msb x) \<and> 
+                  ((msb x \<and> \<not> msb y) \<or> (x < y)))"
+  by (auto simp add: word_sless_def word_sle_msb_le)
+
+definition
+  "map_last f xs = (if xs = [] then [] else butlast xs @ [f (last xs)])"
+
+lemma map_last_simps:
+  "map_last f [] = []"
+  "map_last f [x] = [f x]"
+  "map_last f (x # y # zs) = x # map_last f (y # zs)"
+  by (simp_all add: map_last_def)
+
+lemma word_sle_rbl:
+  "(x <=s y) = rev_bl_order True (map_last Not (rev (to_bl x)))
+     (map_last Not (rev (to_bl y)))"
+  using word_msb_alt[where w=x] word_msb_alt[where w=y]
+  apply (simp add: word_sle_msb_le word_le_rbl)
+  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
+   apply (cases "to_bl x", simp)
+   apply (cases "to_bl y", simp)
+   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
+   apply auto
+  done
+
+lemma word_sless_rbl:
+  "(x <s y) = rev_bl_order False (map_last Not (rev (to_bl x)))
+     (map_last Not (rev (to_bl y)))"
+  using word_msb_alt[where w=x] word_msb_alt[where w=y]
+  apply (simp add: word_sless_msb_less word_less_rbl)
+  apply (subgoal_tac "length (to_bl x) = length (to_bl y)")
+   apply (cases "to_bl x", simp)
+   apply (cases "to_bl y", simp)
+   apply (clarsimp simp: map_last_def rev_bl_order_rev_simp)
+   apply auto
+  done
+
+text {* Lemmas for unpacking rev (to_bl n) for numerals n and also
+for irreducible values and expressions. *}
+
+lemma rev_bin_to_bl_simps:
+  "rev (bin_to_bl 0 x) = []"
+  "rev (bin_to_bl (Suc n) (numeral (num.Bit0 nm)))
+    = False # rev (bin_to_bl n (numeral nm))"
+  "rev (bin_to_bl (Suc n) (numeral (num.Bit1 nm)))
+    = True # rev (bin_to_bl n (numeral nm))"
+  "rev (bin_to_bl (Suc n) (numeral (num.One)))
+    = True # replicate n False"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm)))
+    = False # rev (bin_to_bl n (neg_numeral nm))"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm)))
+    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.One)))
+    = True # replicate n True"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit0 nm + num.One)))
+    = True # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.Bit1 nm + num.One)))
+    = False # rev (bin_to_bl n (neg_numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (neg_numeral (num.One + num.One)))
+    = False # rev (bin_to_bl n (neg_numeral num.One))"
+  apply (simp_all add: bin_to_bl_def)
+  apply (simp_all only: bin_to_bl_aux_alt)
+  apply (simp_all)
+  apply (simp_all add: bin_to_bl_zero_aux bin_to_bl_minus1_aux)
+  done
+
+lemma to_bl_upt:
+  "to_bl x = rev (map (op !! x) [0 ..< size x])"
+  apply (rule nth_equalityI)
+   apply (simp add: word_size)
+  apply (clarsimp simp: to_bl_nth word_size nth_rev)
+  done
+
+lemma rev_to_bl_upt:
+  "rev (to_bl x) = map (op !! x) [0 ..< size x]"
+  by (simp add: to_bl_upt)
+
+lemma upt_eq_list_intros:
+  "j <= i \<Longrightarrow> [i ..< j] = []"
+  "\<lbrakk> i = x; x < j; [x + 1 ..< j] = xs \<rbrakk> \<Longrightarrow> [i ..< j] = (x # xs)"
+  by (simp_all add: upt_eq_Nil_conv upt_eq_Cons_conv)
+
+text {* Tactic definition *}
+
+ML {*
+
+structure Word_Bitwise_Tac = struct
+
+val word_ss = global_simpset_of @{theory Word};
+
+fun mk_nat_clist ns = List.foldr
+  (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
+  @{cterm "[] :: nat list"} ns;
+
+fun upt_conv ct = case term_of ct of
+  (@{const upt} $ n $ m) => let
+    val (i, j) = pairself (snd o HOLogic.dest_number) (n, m);
+    val ns = map (Numeral.mk_cnumber @{ctyp nat}) (i upto (j - 1))
+      |> mk_nat_clist;
+    val prop = Thm.mk_binop @{cterm "op = :: nat list => _"} ct ns
+                 |> Thm.apply @{cterm Trueprop};
+  in Goal.prove_internal [] prop 
+      (K (REPEAT_DETERM (resolve_tac @{thms upt_eq_list_intros} 1
+          ORELSE simp_tac word_ss 1))) |> mk_meta_eq |> SOME end
+    handle TERM _ => NONE
+  | _ => NONE;
+
+val expand_upt_simproc = Simplifier.make_simproc
+  {lhss = [@{cpat "upt _ _"}],
+   name = "expand_upt", identifier = [],
+   proc = K (K upt_conv)};
+
+fun word_len_simproc_fn ct = case term_of ct of
+    Const (@{const_name len_of}, _) $ t => (let
+        val T = fastype_of t |> dest_Type |> snd |> the_single
+        val n = Numeral.mk_cnumber @{ctyp nat} (Word_Lib.dest_binT T);
+        val prop = Thm.mk_binop @{cterm "op = :: nat => _"} ct n
+                 |> Thm.apply @{cterm Trueprop};
+      in Goal.prove_internal [] prop (K (simp_tac word_ss 1))
+             |> mk_meta_eq |> SOME end
+    handle TERM _ => NONE | TYPE _ => NONE)
+  | _ => NONE;
+
+val word_len_simproc = Simplifier.make_simproc
+  {lhss = [@{cpat "len_of _"}],
+   name = "word_len", identifier = [],
+   proc = K (K word_len_simproc_fn)};
+
+(* convert 5 or nat 5 to Suc 4 when n_sucs = 1, Suc (Suc 4) when n_sucs = 2,
+   or just 5 (discarding nat) when n_sucs = 0 *)
+
+fun nat_get_Suc_simproc_fn n_sucs thy ct = let
+    val (f $ arg) = (term_of ct);
+    val n = (case arg of @{term nat} $ n => n | n => n)
+      |> HOLogic.dest_number |> snd;
+    val (i, j) = if n > n_sucs then (n_sucs, n - n_sucs)
+      else (n, 0);
+    val arg' = List.foldr (op $) (HOLogic.mk_number @{typ nat} j)
+        (replicate i @{term Suc});
+    val _ = if arg = arg' then raise TERM ("", []) else ();
+    fun propfn g = HOLogic.mk_eq (g arg, g arg')
+      |> HOLogic.mk_Trueprop |> cterm_of thy;
+    val eq1 = Goal.prove_internal [] (propfn I)
+      (K (simp_tac word_ss 1));
+  in Goal.prove_internal [] (propfn (curry (op $) f))
+      (K (simp_tac (HOL_ss addsimps [eq1]) 1))
+       |> mk_meta_eq |> SOME end
+    handle TERM _ => NONE;
+
+fun nat_get_Suc_simproc n_sucs thy cts = Simplifier.make_simproc
+  {lhss = map (fn t => Thm.apply t @{cpat "?n :: nat"}) cts,
+   name = "nat_get_Suc", identifier = [],
+   proc = K (K (nat_get_Suc_simproc_fn n_sucs thy))};
+
+val no_split_ss = Splitter.del_split @{thm split_if} HOL_ss;
+
+val expand_word_eq_sss = (HOL_basic_ss addsimps
+       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl},
+  [no_split_ss addsimps @{thms rbl_word_plus rbl_word_and rbl_word_or rbl_word_not
+                                rbl_word_neg bl_word_sub rbl_word_xor
+                                rbl_word_cat rbl_word_slice rbl_word_scast
+                                rbl_word_ucast rbl_shiftl rbl_shiftr rbl_sshiftr
+                                rbl_word_if},
+   no_split_ss addsimps @{thms to_bl_numeral to_bl_neg_numeral
+                               to_bl_0 rbl_word_1},
+   no_split_ss addsimps @{thms rev_rev_ident
+                                rev_replicate rev_map to_bl_upt word_size}
+          addsimprocs [word_len_simproc],
+   no_split_ss addsimps @{thms list.simps split_conv replicate.simps map.simps
+                                zip_Cons_Cons zip_Nil drop_Suc_Cons drop_0 drop_Nil
+                                foldr.simps map2_Cons map2_Nil takefill_Suc_Cons
+                                takefill_Suc_Nil takefill.Z rbl_succ2_simps
+                                rbl_plus_simps rev_bin_to_bl_simps append.simps
+                                takefill_last_simps drop_nonempty_simps
+                                rev_bl_order_simps}
+          addsimprocs [expand_upt_simproc,
+                       nat_get_Suc_simproc 4 @{theory}
+                         [@{cpat replicate}, @{cpat "takefill ?x"},
+                          @{cpat drop}, @{cpat "bin_to_bl"},
+                          @{cpat "takefill_last ?x"},
+                          @{cpat "drop_nonempty ?x"}]],
+    no_split_ss addsimps @{thms xor3_simps carry_simps if_bool_simps}
+  ])
+
+val tac = let
+    val (ss, sss) = expand_word_eq_sss;
+    val st = generic_simp_tac true (true, false, false);
+  in foldr1 (op THEN_ALL_NEW) ((CHANGED o st ss) :: map st sss) end;
+
+end
+
+*}
+
+method_setup word_bitwise =
+  {* Scan.succeed (K (Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac 1)))  *}
+  "decomposer for word equalities and inequalities into bit propositions"
+
+end