# HG changeset patch
# User haftmann
# Date 1555444218 0
# Node ID c2786fe88064c202f6b0ee6557f63e3eff9741aa
# Parent  c247bf924d25b476abee045f7ebec1fd6755acbf
tuned theory names

diff -r c247bf924d25 -r c2786fe88064 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 16 19:50:09 2019 +0000
+++ b/src/HOL/ROOT	Tue Apr 16 19:50:18 2019 +0000
@@ -829,8 +829,8 @@
     "HOL-Library"
   theories
     Word
-    WordBitwise
-    WordExamples
+    Word_Bitwise
+    Word_Examples
   document_files "root.bib" "root.tex"
 
 session "HOL-Statespace" in Statespace = HOL +
diff -r c247bf924d25 -r c2786fe88064 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:09 2019 +0000
+++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:18 2019 +0000
@@ -14,7 +14,7 @@
   Misc_Arithmetic
 begin
 
-text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close>
+text \<open>See \<^file>\<open>Word_Examples.thy\<close> for examples.\<close>
 
 subsection \<open>Type definition\<close>
 
diff -r c247bf924d25 -r c2786fe88064 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Tue Apr 16 19:50:09 2019 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,544 +0,0 @@
-(*  Title:      HOL/Word/WordBitwise.thy
-    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
-*)
-
-theory WordBitwise
-  imports Word
-begin
-
-text \<open>Helper constants used in defining addition\<close>
-
-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 \<open>Breaking up word equalities into equalities on their
-  bit lists. Equalities are generated and manipulated in the
-  reverse order to \<^const>\<open>to_bl\<close>.\<close>
-
-lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
-  by simp
-
-lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<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 (\<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 (\<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
-
-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 (cases "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"
-  by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
-
-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_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 ((\<and>) x) ys) (False # sm)) xs []"
-
-lemma rbl_mul_simps:
-  "rbl_mul (x # xs) ys = rbl_plus False (map ((\<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:
-  "length xs \<le> size y \<Longrightarrow>
-    rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
-  for y :: "'a::len word"
-proof (induct xs)
-  case Nil
-  show ?case by (simp add: rbl_mul_simps)
-next
-  case (Cons z zs)
-
-  have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
-    for x y :: "'a word"
-    by (simp add: rbl_word_plus[symmetric])
-
-  have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)"
-    by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
-
-  have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
-    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
-
-  from Cons show ?case
-    apply (simp add: trans [OF of_bl_append add.commute]
-        rbl_mul_simps rbl_word_plus' distrib_right 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: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
-  for x :: "'a::len word"
-  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
-
-text \<open>Breaking up inequalities into bitlist properties.\<close>
-
-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))"
-  by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
-
-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 (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
-  done
-
-lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
-  for x y :: "'a::len0 word"
-  by (simp add: rev_bl_order_bl_to_bin word_le_def)
-
-lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
-  for x y :: "'a::len0 word"
-  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 \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> 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 \<longleftrightarrow> (msb y \<longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also
-  for irreducible values and expressions.\<close>
-
-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) (- 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 + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
-    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
-    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
-  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
-    False # rev (bin_to_bl n (- numeral num.One))"
-  apply simp_all
-  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 ((!!) x) [0 ..< size x])"
-  apply (rule nth_equalityI)
-   apply (simp add: word_size)
-  apply (auto simp: to_bl_nth word_size nth_rev)
-  done
-
-lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
-  by (simp add: to_bl_upt)
-
-lemma upt_eq_list_intros:
-  "j \<le> i \<Longrightarrow> [i ..< j] = []"
-  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
-  by (simp_all add: upt_eq_Cons_conv)
-
-
-subsection \<open>Tactic definition\<close>
-
-ML \<open>
-structure Word_Bitwise_Tac =
-struct
-
-val word_ss = simpset_of \<^theory_context>\<open>Word\<close>;
-
-fun mk_nat_clist ns =
-  fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>)
-    ns \<^cterm>\<open>[] :: nat list\<close>;
-
-fun upt_conv ctxt ct =
-  case Thm.term_of ct of
-    (\<^const>\<open>upt\<close> $ n $ m) =>
-      let
-        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
-        val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
-          |> mk_nat_clist;
-        val prop =
-          Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns
-          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
-      in
-        try (fn () =>
-          Goal.prove_internal ctxt [] prop
-            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
-                ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
-      end
-  | _ => NONE;
-
-val expand_upt_simproc =
-  Simplifier.make_simproc \<^context> "expand_upt"
-   {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv};
-
-fun word_len_simproc_fn ctxt ct =
-  (case Thm.term_of ct of
-    Const (\<^const_name>\<open>len_of\<close>, _) $ t =>
-     (let
-        val T = fastype_of t |> dest_Type |> snd |> the_single
-        val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);
-        val prop =
-          Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n
-          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
-      in
-        Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
-        |> mk_meta_eq |> SOME
-      end handle TERM _ => NONE | TYPE _ => NONE)
-  | _ => NONE);
-
-val word_len_simproc =
-  Simplifier.make_simproc \<^context> "word_len"
-   {lhss = [\<^term>\<open>len_of x\<close>], proc = 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 ctxt ct =
-  let
-    val (f $ arg) = Thm.term_of ct;
-    val n =
-      (case arg of \<^term>\<open>nat\<close> $ 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' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j);
-    val _ = if arg = arg' then raise TERM ("", []) else ();
-    fun propfn g =
-      HOLogic.mk_eq (g arg, g arg')
-      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
-    val eq1 =
-      Goal.prove_internal ctxt [] (propfn I)
-        (K (simp_tac (put_simpset word_ss ctxt) 1));
-  in
-    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
-      (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
-    |> mk_meta_eq |> SOME
-  end handle TERM _ => NONE;
-
-fun nat_get_Suc_simproc n_sucs ts =
-  Simplifier.make_simproc \<^context> "nat_get_Suc"
-   {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts,
-    proc = K (nat_get_Suc_simproc_fn n_sucs)};
-
-val no_split_ss =
-  simpset_of (put_simpset HOL_ss \<^context>
-    |> Splitter.del_split @{thm if_split});
-
-val expand_word_eq_sss =
-  (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps
-       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
-  map simpset_of [
-   put_simpset no_split_ss \<^context> 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},
-   put_simpset no_split_ss \<^context> addsimps
-    @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
-   put_simpset no_split_ss \<^context> addsimps
-    @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
-          addsimprocs [word_len_simproc],
-   put_simpset no_split_ss \<^context> addsimps
-    @{thms list.simps split_conv replicate.simps list.map
-                                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
-                         [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>,
-                          \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>,
-                          \<^term>\<open>takefill_last x\<close>,
-                          \<^term>\<open>drop_nonempty x\<close>]],
-    put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps}
-  ])
-
-fun tac ctxt =
-  let
-    val (ss, sss) = expand_word_eq_sss;
-  in
-    foldr1 (op THEN_ALL_NEW)
-      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
-        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
-  end;
-
-end
-\<close>
-
-method_setup word_bitwise =
-  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
-  "decomposer for word equalities and inequalities into bit propositions"
-
-end
diff -r c247bf924d25 -r c2786fe88064 src/HOL/Word/WordExamples.thy
--- a/src/HOL/Word/WordExamples.thy	Tue Apr 16 19:50:09 2019 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,207 +0,0 @@
-(*  Title:      HOL/Word/WordExamples.thy
-    Authors:    Gerwin Klein and Thomas Sewell, NICTA
-
-Examples demonstrating and testing various word operations.
-*)
-
-section "Examples of word operations"
-
-theory WordExamples
-  imports WordBitwise
-begin
-
-type_synonym word32 = "32 word"
-type_synonym word8 = "8 word"
-type_synonym byte = word8
-
-text "modulus"
-
-lemma "(27 :: 4 word) = -5" by simp
-
-lemma "(27 :: 4 word) = 11" by simp
-
-lemma "27 \<noteq> (11 :: 6 word)" by simp
-
-text "signed"
-
-lemma "(127 :: 6 word) = -1" by simp
-
-text "number ring simps"
-
-lemma
-  "27 + 11 = (38::'a::len word)"
-  "27 + 11 = (6::5 word)"
-  "7 * 3 = (21::'a::len word)"
-  "11 - 27 = (-16::'a::len word)"
-  "- (- 11) = (11::'a::len word)"
-  "-40 + 1 = (-39::'a::len word)"
-  by simp_all
-
-lemma "word_pred 2 = 1" by simp
-
-lemma "word_succ (- 3) = -2" by simp
-
-lemma "23 < (27::8 word)" by simp
-lemma "23 \<le> (27::8 word)" by simp
-lemma "\<not> 23 < (27::2 word)" by simp
-lemma "0 < (4::3 word)" by simp
-lemma "1 < (4::3 word)" by simp
-lemma "0 < (1::3 word)" by simp
-
-text "ring operations"
-
-lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
-
-text "casting"
-
-lemma "uint (234567 :: 10 word) = 71" by simp
-lemma "uint (-234567 :: 10 word) = 953" by simp
-lemma "sint (234567 :: 10 word) = 71" by simp
-lemma "sint (-234567 :: 10 word) = -71" by simp
-lemma "uint (1 :: 10 word) = 1" by simp
-
-lemma "unat (-234567 :: 10 word) = 953" by simp
-lemma "unat (1 :: 10 word) = 1" by simp
-
-lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
-lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
-lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
-lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
-
-text "reducing goals to nat or int and arith:"
-lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
-  by unat_arith
-lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
-  by unat_arith
-
-text "bool lists"
-
-lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
-
-lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
-
-text "this is not exactly fast, but bearable"
-lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
-
-text "this works only for replicate n True"
-lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
-  by (unfold mask_bl [symmetric]) (simp add: mask_def)
-
-
-text "bit operations"
-
-lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
-lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
-lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
-lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
-lemma "0 AND 5 = (0 :: byte)" by simp
-lemma "1 AND 1 = (1 :: byte)" by simp
-lemma "1 AND 0 = (0 :: byte)" by simp
-lemma "1 AND 5 = (1 :: byte)" by simp
-lemma "1 OR 6 = (7 :: byte)" by simp
-lemma "1 OR 1 = (1 :: byte)" by simp
-lemma "1 XOR 7 = (6 :: byte)" by simp
-lemma "1 XOR 1 = (0 :: byte)" by simp
-lemma "NOT 1 = (254 :: byte)" by simp
-lemma "NOT 0 = (255 :: byte)" apply simp oops
-(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
-
-lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
-
-lemma "(0b0010 :: 4 word) !! 1" by simp
-lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
-lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
-lemma "\<not> (1 :: 3 word) !! 2" by simp
-
-lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
-  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
-
-lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
-lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
-lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
-lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp
-lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp
-lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp
-lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp
-
-lemma "lsb (0b0101::'a::len word)" by simp
-lemma "\<not> lsb (0b1000::'a::len word)" by simp
-lemma "lsb (1::'a::len word)" by simp
-lemma "\<not> lsb (0::'a::len word)" by simp
-
-lemma "\<not> msb (0b0101::4 word)" by simp
-lemma   "msb (0b1000::4 word)" by simp
-lemma "\<not> msb (1::4 word)" by simp
-lemma "\<not> msb (0::4 word)" by simp
-
-lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
-lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
-  by simp
-
-lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
-lemma "0b1011 >> 2 = (0b10::8 word)" by simp
-lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
-lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
-
-lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
-lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
-
-lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
-lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
-lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
-lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
-lemma "word_rotr 2 0 = (0::4 word)" by simp
-lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
-lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
-lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
-
-lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
-proof -
-  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
-    by (simp only: word_ao_dist2)
-  also have "0xff00 OR 0x00ff = (-1::16 word)"
-    by simp
-  also have "x AND -1 = x"
-    by simp
-  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 AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
-  for x :: "10 word"
-  by word_bitwise
-
-lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
-  for x :: "12 word"
-  by word_bitwise
-
-text "some problems require further reasoning after bit expansion"
-
-lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
-  for x :: "8 word"
-  apply word_bitwise
-  apply blast
-  done
-
-lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
-  for x :: word32
-  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 >> a = 0"
-  for b :: word32
-  apply word_bitwise
-  apply simp
-  done
-
-end
diff -r c247bf924d25 -r c2786fe88064 src/HOL/Word/Word_Bitwise.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word_Bitwise.thy	Tue Apr 16 19:50:18 2019 +0000
@@ -0,0 +1,544 @@
+(*  Title:      HOL/Word/Word_Bitwise.thy
+    Authors:    Thomas Sewell, NICTA and Sascha Boehme, TU Muenchen
+*)
+
+theory Word_Bitwise
+  imports Word
+begin
+
+text \<open>Helper constants used in defining addition\<close>
+
+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 \<open>Breaking up word equalities into equalities on their
+  bit lists. Equalities are generated and manipulated in the
+  reverse order to \<^const>\<open>to_bl\<close>.\<close>
+
+lemma word_eq_rbl_eq: "x = y \<longleftrightarrow> rev (to_bl x) = rev (to_bl y)"
+  by simp
+
+lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<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 (\<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 (\<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
+
+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 (cases "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"
+  by (simp_all add: takefill_last_def) (simp_all add: takefill_alt)
+
+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_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 ((\<and>) x) ys) (False # sm)) xs []"
+
+lemma rbl_mul_simps:
+  "rbl_mul (x # xs) ys = rbl_plus False (map ((\<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:
+  "length xs \<le> size y \<Longrightarrow>
+    rbl_mul xs (rev (to_bl y)) = take (length xs) (rev (to_bl (of_bl (rev xs) * y)))"
+  for y :: "'a::len word"
+proof (induct xs)
+  case Nil
+  show ?case by (simp add: rbl_mul_simps)
+next
+  case (Cons z zs)
+
+  have rbl_word_plus': "to_bl (x + y) = rev (rbl_plus False (rev (to_bl x)) (rev (to_bl y)))"
+    for x y :: "'a word"
+    by (simp add: rbl_word_plus[symmetric])
+
+  have mult_bit: "to_bl (of_bl [z] * y) = map ((\<and>) z) (to_bl y)"
+    by (cases z) (simp cong: map_cong, simp add: map_replicate_const cong: map_cong)
+
+  have shiftl: "of_bl xs * 2 * y = (of_bl xs * y) << 1" for xs
+    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
+
+  from Cons show ?case
+    apply (simp add: trans [OF of_bl_append add.commute]
+        rbl_mul_simps rbl_word_plus' distrib_right 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: "rev (to_bl (x * y)) = rbl_mul (rev (to_bl x)) (rev (to_bl y))"
+  for x :: "'a::len word"
+  using word_rbl_mul_induct[where xs="rev (to_bl x)" and y=y] by (simp add: word_size)
+
+text \<open>Breaking up inequalities into bitlist properties.\<close>
+
+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))"
+  by (induct arbitrary: F rule: list_induct2) (auto simp: rev_bl_order_simps)
+
+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 (auto simp add: bl_to_bin_def Bit_B0 Bit_B1 add1_zle_eq Bit_def)
+  done
+
+lemma word_le_rbl: "x \<le> y \<longleftrightarrow> rev_bl_order True (rev (to_bl x)) (rev (to_bl y))"
+  for x y :: "'a::len0 word"
+  by (simp add: rev_bl_order_bl_to_bin word_le_def)
+
+lemma word_less_rbl: "x < y \<longleftrightarrow> rev_bl_order False (rev (to_bl x)) (rev (to_bl y))"
+  for x y :: "'a::len0 word"
+  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 \<longleftrightarrow> (msb y \<longrightarrow> msb x) \<and> ((msb x \<and> \<not> msb y) \<or> x \<le> 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 \<longleftrightarrow> (msb y \<longrightarrow> 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 \<longleftrightarrow> 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 \<longleftrightarrow> 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 \<open>Lemmas for unpacking \<^term>\<open>rev (to_bl n)\<close> for numerals n and also
+  for irreducible values and expressions.\<close>
+
+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) (- 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 + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One))) = True # replicate n True"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit0 nm + num.One))) =
+    True # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.Bit1 nm + num.One))) =
+    False # rev (bin_to_bl n (- numeral (nm + num.One)))"
+  "rev (bin_to_bl (Suc n) (- numeral (num.One + num.One))) =
+    False # rev (bin_to_bl n (- numeral num.One))"
+  apply simp_all
+  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 ((!!) x) [0 ..< size x])"
+  apply (rule nth_equalityI)
+   apply (simp add: word_size)
+  apply (auto simp: to_bl_nth word_size nth_rev)
+  done
+
+lemma rev_to_bl_upt: "rev (to_bl x) = map ((!!) x) [0 ..< size x]"
+  by (simp add: to_bl_upt)
+
+lemma upt_eq_list_intros:
+  "j \<le> i \<Longrightarrow> [i ..< j] = []"
+  "i = x \<Longrightarrow> x < j \<Longrightarrow> [x + 1 ..< j] = xs \<Longrightarrow> [i ..< j] = (x # xs)"
+  by (simp_all add: upt_eq_Cons_conv)
+
+
+subsection \<open>Tactic definition\<close>
+
+ML \<open>
+structure Word_Bitwise_Tac =
+struct
+
+val word_ss = simpset_of \<^theory_context>\<open>Word\<close>;
+
+fun mk_nat_clist ns =
+  fold_rev (Thm.mk_binop \<^cterm>\<open>Cons :: nat \<Rightarrow> _\<close>)
+    ns \<^cterm>\<open>[] :: nat list\<close>;
+
+fun upt_conv ctxt ct =
+  case Thm.term_of ct of
+    (\<^const>\<open>upt\<close> $ n $ m) =>
+      let
+        val (i, j) = apply2 (snd o HOLogic.dest_number) (n, m);
+        val ns = map (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close>) (i upto (j - 1))
+          |> mk_nat_clist;
+        val prop =
+          Thm.mk_binop \<^cterm>\<open>(=) :: nat list \<Rightarrow> _\<close> ct ns
+          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
+      in
+        try (fn () =>
+          Goal.prove_internal ctxt [] prop
+            (K (REPEAT_DETERM (resolve_tac ctxt @{thms upt_eq_list_intros} 1
+                ORELSE simp_tac (put_simpset word_ss ctxt) 1))) |> mk_meta_eq) ()
+      end
+  | _ => NONE;
+
+val expand_upt_simproc =
+  Simplifier.make_simproc \<^context> "expand_upt"
+   {lhss = [\<^term>\<open>upt x y\<close>], proc = K upt_conv};
+
+fun word_len_simproc_fn ctxt ct =
+  (case Thm.term_of ct of
+    Const (\<^const_name>\<open>len_of\<close>, _) $ t =>
+     (let
+        val T = fastype_of t |> dest_Type |> snd |> the_single
+        val n = Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> (Word_Lib.dest_binT T);
+        val prop =
+          Thm.mk_binop \<^cterm>\<open>(=) :: nat \<Rightarrow> _\<close> ct n
+          |> Thm.apply \<^cterm>\<open>Trueprop\<close>;
+      in
+        Goal.prove_internal ctxt [] prop (K (simp_tac (put_simpset word_ss ctxt) 1))
+        |> mk_meta_eq |> SOME
+      end handle TERM _ => NONE | TYPE _ => NONE)
+  | _ => NONE);
+
+val word_len_simproc =
+  Simplifier.make_simproc \<^context> "word_len"
+   {lhss = [\<^term>\<open>len_of x\<close>], proc = 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 ctxt ct =
+  let
+    val (f $ arg) = Thm.term_of ct;
+    val n =
+      (case arg of \<^term>\<open>nat\<close> $ 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' = funpow i HOLogic.mk_Suc (HOLogic.mk_number \<^typ>\<open>nat\<close> j);
+    val _ = if arg = arg' then raise TERM ("", []) else ();
+    fun propfn g =
+      HOLogic.mk_eq (g arg, g arg')
+      |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt;
+    val eq1 =
+      Goal.prove_internal ctxt [] (propfn I)
+        (K (simp_tac (put_simpset word_ss ctxt) 1));
+  in
+    Goal.prove_internal ctxt [] (propfn (curry (op $) f))
+      (K (simp_tac (put_simpset HOL_ss ctxt addsimps [eq1]) 1))
+    |> mk_meta_eq |> SOME
+  end handle TERM _ => NONE;
+
+fun nat_get_Suc_simproc n_sucs ts =
+  Simplifier.make_simproc \<^context> "nat_get_Suc"
+   {lhss = map (fn t => t $ \<^term>\<open>n :: nat\<close>) ts,
+    proc = K (nat_get_Suc_simproc_fn n_sucs)};
+
+val no_split_ss =
+  simpset_of (put_simpset HOL_ss \<^context>
+    |> Splitter.del_split @{thm if_split});
+
+val expand_word_eq_sss =
+  (simpset_of (put_simpset HOL_basic_ss \<^context> addsimps
+       @{thms word_eq_rbl_eq word_le_rbl word_less_rbl word_sle_rbl word_sless_rbl}),
+  map simpset_of [
+   put_simpset no_split_ss \<^context> 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},
+   put_simpset no_split_ss \<^context> addsimps
+    @{thms to_bl_numeral to_bl_neg_numeral to_bl_0 rbl_word_1},
+   put_simpset no_split_ss \<^context> addsimps
+    @{thms rev_rev_ident rev_replicate rev_map to_bl_upt word_size}
+          addsimprocs [word_len_simproc],
+   put_simpset no_split_ss \<^context> addsimps
+    @{thms list.simps split_conv replicate.simps list.map
+                                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
+                         [\<^term>\<open>replicate\<close>, \<^term>\<open>takefill x\<close>,
+                          \<^term>\<open>drop\<close>, \<^term>\<open>bin_to_bl\<close>,
+                          \<^term>\<open>takefill_last x\<close>,
+                          \<^term>\<open>drop_nonempty x\<close>]],
+    put_simpset no_split_ss \<^context> addsimps @{thms xor3_simps carry_simps if_bool_simps}
+  ])
+
+fun tac ctxt =
+  let
+    val (ss, sss) = expand_word_eq_sss;
+  in
+    foldr1 (op THEN_ALL_NEW)
+      ((CHANGED o safe_full_simp_tac (put_simpset ss ctxt)) ::
+        map (fn ss => safe_full_simp_tac (put_simpset ss ctxt)) sss)
+  end;
+
+end
+\<close>
+
+method_setup word_bitwise =
+  \<open>Scan.succeed (fn ctxt => Method.SIMPLE_METHOD (Word_Bitwise_Tac.tac ctxt 1))\<close>
+  "decomposer for word equalities and inequalities into bit propositions"
+
+end
diff -r c247bf924d25 -r c2786fe88064 src/HOL/Word/Word_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word_Examples.thy	Tue Apr 16 19:50:18 2019 +0000
@@ -0,0 +1,207 @@
+(*  Title:      HOL/Word/Word_Examples.thy
+    Authors:    Gerwin Klein and Thomas Sewell, NICTA
+
+Examples demonstrating and testing various word operations.
+*)
+
+section "Examples of word operations"
+
+theory Word_Examples
+  imports Word_Bitwise
+begin
+
+type_synonym word32 = "32 word"
+type_synonym word8 = "8 word"
+type_synonym byte = word8
+
+text "modulus"
+
+lemma "(27 :: 4 word) = -5" by simp
+
+lemma "(27 :: 4 word) = 11" by simp
+
+lemma "27 \<noteq> (11 :: 6 word)" by simp
+
+text "signed"
+
+lemma "(127 :: 6 word) = -1" by simp
+
+text "number ring simps"
+
+lemma
+  "27 + 11 = (38::'a::len word)"
+  "27 + 11 = (6::5 word)"
+  "7 * 3 = (21::'a::len word)"
+  "11 - 27 = (-16::'a::len word)"
+  "- (- 11) = (11::'a::len word)"
+  "-40 + 1 = (-39::'a::len word)"
+  by simp_all
+
+lemma "word_pred 2 = 1" by simp
+
+lemma "word_succ (- 3) = -2" by simp
+
+lemma "23 < (27::8 word)" by simp
+lemma "23 \<le> (27::8 word)" by simp
+lemma "\<not> 23 < (27::2 word)" by simp
+lemma "0 < (4::3 word)" by simp
+lemma "1 < (4::3 word)" by simp
+lemma "0 < (1::3 word)" by simp
+
+text "ring operations"
+
+lemma "a + 2 * b + c - b = (b + c) + (a :: 32 word)" by simp
+
+text "casting"
+
+lemma "uint (234567 :: 10 word) = 71" by simp
+lemma "uint (-234567 :: 10 word) = 953" by simp
+lemma "sint (234567 :: 10 word) = 71" by simp
+lemma "sint (-234567 :: 10 word) = -71" by simp
+lemma "uint (1 :: 10 word) = 1" by simp
+
+lemma "unat (-234567 :: 10 word) = 953" by simp
+lemma "unat (1 :: 10 word) = 1" by simp
+
+lemma "ucast (0b1010 :: 4 word) = (0b10 :: 2 word)" by simp
+lemma "ucast (0b1010 :: 4 word) = (0b1010 :: 10 word)" by simp
+lemma "scast (0b1010 :: 4 word) = (0b111010 :: 6 word)" by simp
+lemma "ucast (1 :: 4 word) = (1 :: 2 word)" by simp
+
+text "reducing goals to nat or int and arith:"
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
+lemma "i < x \<Longrightarrow> i < i + 1" for i x :: "'a::len word"
+  by unat_arith
+
+text "bool lists"
+
+lemma "of_bl [True, False, True, True] = (0b1011::'a::len word)" by simp
+
+lemma "to_bl (0b110::4 word) = [False, True, True, False]" by simp
+
+text "this is not exactly fast, but bearable"
+lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)" by simp
+
+text "this works only for replicate n True"
+lemma "of_bl (replicate 32 True) = (0xFFFFFFFF::32 word)"
+  by (unfold mask_bl [symmetric]) (simp add: mask_def)
+
+
+text "bit operations"
+
+lemma "0b110 AND 0b101 = (0b100 :: 32 word)" by simp
+lemma "0b110 OR 0b011 = (0b111 :: 8 word)" by simp
+lemma "0xF0 XOR 0xFF = (0x0F :: byte)" by simp
+lemma "NOT (0xF0 :: 16 word) = 0xFF0F" by simp
+lemma "0 AND 5 = (0 :: byte)" by simp
+lemma "1 AND 1 = (1 :: byte)" by simp
+lemma "1 AND 0 = (0 :: byte)" by simp
+lemma "1 AND 5 = (1 :: byte)" by simp
+lemma "1 OR 6 = (7 :: byte)" by simp
+lemma "1 OR 1 = (1 :: byte)" by simp
+lemma "1 XOR 7 = (6 :: byte)" by simp
+lemma "1 XOR 1 = (0 :: byte)" by simp
+lemma "NOT 1 = (254 :: byte)" by simp
+lemma "NOT 0 = (255 :: byte)" apply simp oops
+(* FIXME: "NOT 0" rewrites to "max_word" instead of "-1" *)
+
+lemma "(-1 :: 32 word) = 0xFFFFFFFF" by simp
+
+lemma "(0b0010 :: 4 word) !! 1" by simp
+lemma "\<not> (0b0010 :: 4 word) !! 0" by simp
+lemma "\<not> (0b1000 :: 3 word) !! 4" by simp
+lemma "\<not> (1 :: 3 word) !! 2" by simp
+
+lemma "(0b11000 :: 10 word) !! n = (n = 4 \<or> n = 3)"
+  by (auto simp add: bin_nth_Bit0 bin_nth_Bit1)
+
+lemma "set_bit 55 7 True = (183::'a::len0 word)" by simp
+lemma "set_bit 0b0010 7 True = (0b10000010::'a::len0 word)" by simp
+lemma "set_bit 0b0010 1 False = (0::'a::len0 word)" by simp
+lemma "set_bit 1 3 True = (0b1001::'a::len0 word)" by simp
+lemma "set_bit 1 0 False = (0::'a::len0 word)" by simp
+lemma "set_bit 0 3 True = (0b1000::'a::len0 word)" by simp
+lemma "set_bit 0 3 False = (0::'a::len0 word)" by simp
+
+lemma "lsb (0b0101::'a::len word)" by simp
+lemma "\<not> lsb (0b1000::'a::len word)" by simp
+lemma "lsb (1::'a::len word)" by simp
+lemma "\<not> lsb (0::'a::len word)" by simp
+
+lemma "\<not> msb (0b0101::4 word)" by simp
+lemma   "msb (0b1000::4 word)" by simp
+lemma "\<not> msb (1::4 word)" by simp
+lemma "\<not> msb (0::4 word)" by simp
+
+lemma "word_cat (27::4 word) (27::8 word) = (2843::'a::len word)" by simp
+lemma "word_cat (0b0011::4 word) (0b1111::6word) = (0b0011001111 :: 10 word)"
+  by simp
+
+lemma "0b1011 << 2 = (0b101100::'a::len0 word)" by simp
+lemma "0b1011 >> 2 = (0b10::8 word)" by simp
+lemma "0b1011 >>> 2 = (0b10::8 word)" by simp
+lemma "1 << 2 = (0b100::'a::len0 word)" apply simp? oops
+
+lemma "slice 3 (0b101111::6 word) = (0b101::3 word)" by simp
+lemma "slice 3 (1::6 word) = (0::3 word)" apply simp? oops
+
+lemma "word_rotr 2 0b0110 = (0b1001::4 word)" by simp
+lemma "word_rotl 1 0b1110 = (0b1101::4 word)" by simp
+lemma "word_roti 2 0b1110 = (0b1011::4 word)" by simp
+lemma "word_roti (- 2) 0b0110 = (0b1001::4 word)" by simp
+lemma "word_rotr 2 0 = (0::4 word)" by simp
+lemma "word_rotr 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_rotl 2 1 = (0b0100::4 word)" apply simp? oops
+lemma "word_roti (- 2) 1 = (0b0100::4 word)" apply simp? oops
+
+lemma "(x AND 0xff00) OR (x AND 0x00ff) = (x::16 word)"
+proof -
+  have "(x AND 0xff00) OR (x AND 0x00ff) = x AND (0xff00 OR 0x00ff)"
+    by (simp only: word_ao_dist2)
+  also have "0xff00 OR 0x00ff = (-1::16 word)"
+    by simp
+  also have "x AND -1 = x"
+    by simp
+  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 AND NOT 3) >> 4 << 2 = ((x >> 2) AND NOT 3)"
+  for x :: "10 word"
+  by word_bitwise
+
+lemma "((x AND -8) >> 3) AND 7 = (x AND 56) >> 3"
+  for x :: "12 word"
+  by word_bitwise
+
+text "some problems require further reasoning after bit expansion"
+
+lemma "x \<le> 42 \<Longrightarrow> x \<le> 89"
+  for x :: "8 word"
+  apply word_bitwise
+  apply blast
+  done
+
+lemma "(x AND 1023) = 0 \<Longrightarrow> x \<le> -1024"
+  for x :: word32
+  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 >> a = 0"
+  for b :: word32
+  apply word_bitwise
+  apply simp
+  done
+
+end