# HG changeset patch
# User haftmann
# Date 1594577406 0
# Node ID 759532ef0885b637a62ce9718faa417e21a8a1d1
# Parent  5689f0db45082c35b5767d6a60fab4f7f75f8496
prefer canonically oriented lists of bits and more direct characterizations in definitions

diff -r 5689f0db4508 -r 759532ef0885 src/HOL/Word/Bit_Comprehension.thy
--- a/src/HOL/Word/Bit_Comprehension.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Word/Bit_Comprehension.thy	Sun Jul 12 18:10:06 2020 +0000
@@ -18,10 +18,10 @@
   "set_bits f =
     (if \<exists>n. \<forall>n'\<ge>n. \<not> f n' then
       let n = LEAST n. \<forall>n'\<ge>n. \<not> f n'
-      in bl_to_bin (rev (map f [0..<n]))
+      in horner_sum of_bool 2 (map f [0..<n])
      else if \<exists>n. \<forall>n'\<ge>n. f n' then
       let n = LEAST n. \<forall>n'\<ge>n. f n'
-      in sbintrunc n (bl_to_bin (True # rev (map f [0..<n])))
+      in signed_take_bit n (horner_sum of_bool 2 (map f [0..<n] @ [True]))
      else 0 :: int)"
 
 instance ..
diff -r 5689f0db4508 -r 759532ef0885 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Jul 12 18:10:06 2020 +0000
+++ b/src/HOL/Word/Word.thy	Sun Jul 12 18:10:06 2020 +0000
@@ -128,9 +128,6 @@
 definition to_bl :: "'a::len word \<Rightarrow> bool list"
   where "to_bl w = bin_to_bl (LENGTH('a)) (uint w)"
 
-definition word_reverse :: "'a::len word \<Rightarrow> 'a word"
-  where "word_reverse w = of_bl (rev (to_bl w))"
-
 definition word_int_case :: "(int \<Rightarrow> 'b) \<Rightarrow> 'a::len word \<Rightarrow> 'b"
   where "word_int_case f w = f (uint w)"
 
@@ -823,6 +820,10 @@
   \<open>\<not> bit w LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
   by transfer simp
 
+lemma take_bit_length_eq [simp]:
+  \<open>take_bit LENGTH('a) w = w\<close> for w :: \<open>'a::len word\<close>
+  by transfer simp
+
 lemma bit_word_of_int_iff:
   \<open>bit (word_of_int k :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> bit k n\<close>
   by transfer rule
@@ -1041,19 +1042,6 @@
 definition mask :: "nat \<Rightarrow> 'a::len word"
   where "mask n = (1 << n) - 1"
 
-definition slice1 :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word"
-  where "slice1 n w = of_bl (takefill False n (to_bl w))"
-
-definition revcast :: "'a::len word \<Rightarrow> 'b::len word"
-  where "revcast w =  of_bl (takefill False (LENGTH('b)) (to_bl w))"
-
-lemma revcast_eq:
-  \<open>(revcast :: 'a::len word \<Rightarrow> 'b::len word) = slice1 LENGTH('b)\<close>
-  by (simp add: fun_eq_iff revcast_def slice1_def)
-
-definition slice :: "nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word"
-  where "slice n w = slice1 (size w - n) w"
-
 
 subsection \<open>Rotation\<close>
 
@@ -1179,9 +1167,6 @@
 lemma to_bl_def': "(to_bl :: 'a::len word \<Rightarrow> bool list) = bin_to_bl (LENGTH('a)) \<circ> uint"
   by (auto simp: to_bl_def)
 
-lemmas word_reverse_no_def [simp] =
-  word_reverse_def [of "numeral w"] for w
-
 lemma uints_mod: "uints n = range (\<lambda>w. w mod 2 ^ n)"
   by (fact uints_def [unfolded no_bintr_alt1])
 
@@ -1440,18 +1425,6 @@
 lemma to_bl_use_of_bl: "to_bl w = bl \<longleftrightarrow> w = of_bl bl \<and> length bl = length (to_bl w)"
   by (fastforce elim!: word_bl.Abs_inverse [unfolded mem_Collect_eq])
 
-lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
-  by (simp add: word_reverse_def word_bl.Abs_inverse)
-
-lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
-  by (simp add: word_reverse_def word_bl.Abs_inverse)
-
-lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
-  by (metis word_rev_rev)
-
-lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
-  by simp
-
 lemma length_bl_gt_0 [iff]: "0 < length (to_bl x)"
   for x :: "'a::len word"
   unfolding word_bl_Rep' by (rule len_gt_0)
@@ -1745,7 +1718,6 @@
 lemma ucast_down_bl [OF refl]: "uc = ucast \<Longrightarrow> is_down uc \<Longrightarrow> uc (of_bl bl) = of_bl bl"
   unfolding of_bl_def by clarify (erule ucast_down_wi)
 
-lemmas slice_def' = slice_def [unfolded word_size]
 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong]
 
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
@@ -2098,7 +2070,7 @@
    apply (simp only: flip: mod_add_self2 [of \<open>x - y\<close> z])
    apply (rule zmod_le_nonneg_dividend)
    apply simp
-  apply (metis add.commute add.right_neutral add_le_cancel_left diff_ge_0_iff_ge int_mod_ge le_less le_less_trans mod_add_self1 not_le not_less)
+  apply (metis add.commute add.right_neutral add_le_cancel_left diff_ge_0_iff_ge int_mod_ge le_less le_less_trans mod_add_self1 not_less)
   done
 
 lemma uint_sub_if':
@@ -3109,29 +3081,44 @@
 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
   by (auto simp: of_bl_def bl_to_bin_rep_F)
 
+lemma bit_horner_sum_bit_word_iff:
+  \<open>bit (horner_sum of_bool (2 :: 'a::len word) bs) n
+    \<longleftrightarrow> n < min LENGTH('a) (length bs) \<and> bs ! n\<close>
+  by transfer (simp add: bit_horner_sum_bit_iff)
+
+lemma of_bl_eq:
+  \<open>of_bl bs = horner_sum of_bool 2 (rev bs)\<close>
+  by (rule bit_word_eqI) (simp add: bit_of_bl_iff bit_horner_sum_bit_word_iff ac_simps)
+
+definition word_reverse :: \<open>'a::len word \<Rightarrow> 'a word\<close>
+  where \<open>word_reverse w = horner_sum of_bool 2 (rev (map (bit w) [0..<LENGTH('a)]))\<close>
+
 lemma bit_word_reverse_iff:
   \<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close>
   for w :: \<open>'a::len word\<close>
-  by (cases \<open>n < LENGTH('a)\<close>) (simp_all add: word_reverse_def bit_of_bl_iff nth_to_bl)
-
-lemma bit_slice1_iff:
-  \<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
-    \<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (cases \<open>n + (LENGTH('a) - m) - (m - LENGTH('a)) < LENGTH('a)\<close>)
-    (auto simp add: slice1_def bit_of_bl_iff takefill_alt rev_take nth_append not_less nth_rev_to_bl ac_simps)
-
-lemma bit_revcast_iff:
-  \<open>bit (revcast w :: 'b::len word) n \<longleftrightarrow> LENGTH('b) - LENGTH('a) \<le> n \<and> n < LENGTH('b)
-    \<and> bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: revcast_eq bit_slice1_iff)
-
-lemma bit_slice_iff:
-  \<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close>
-  for w :: \<open>'a::len word\<close>
-  by (simp add: slice_def word_size bit_slice1_iff)
-
+  by (cases \<open>n < LENGTH('a)\<close>)
+    (simp_all add: word_reverse_def bit_horner_sum_bit_word_iff rev_nth)
+
+lemma word_reverse_eq_of_bl_rev_to_bl:
+  \<open>word_reverse w = of_bl (rev (to_bl w))\<close>
+  by (rule bit_word_eqI)
+    (auto simp add: bit_word_reverse_iff bit_of_bl_iff nth_to_bl)
+
+lemmas word_reverse_no_def [simp] =
+  word_reverse_eq_of_bl_rev_to_bl [of "numeral w"] for w
+
+lemma to_bl_word_rev: "to_bl (word_reverse w) = rev (to_bl w)"
+  by (rule nth_equalityI) (simp_all add: nth_rev_to_bl word_reverse_def word_rep_drop flip: of_bl_eq)
+
+lemma word_rev_rev [simp] : "word_reverse (word_reverse w) = w"
+  by (rule bit_word_eqI)
+    (auto simp add: bit_word_reverse_iff bit_imp_le_length Suc_diff_Suc)
+
+lemma word_rev_gal: "word_reverse w = u \<Longrightarrow> word_reverse u = w"
+  by (metis word_rev_rev)
+
+lemma word_rev_gal': "u = word_reverse w \<Longrightarrow> w = word_reverse u"
+  by simp
 
 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
 
@@ -3218,7 +3205,8 @@
 instantiation word :: (len) bit_comprehension
 begin
 
-definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
+definition word_set_bits_def:
+  \<open>(BITS n. P n) = (horner_sum of_bool 2 (map P [0..<LENGTH('a)]) :: 'a word)\<close>
 
 instance ..
 
@@ -3226,44 +3214,29 @@
 
 lemma bit_set_bits_word_iff:
   \<open>bit (set_bits P :: 'a::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> P n\<close>
-  by (auto simp add: word_set_bits_def bit_of_bl_iff)
+  by (auto simp add: word_set_bits_def bit_horner_sum_bit_word_iff)
+
+lemma set_bits_bit_eq:
+  \<open>set_bits (bit w) = w\<close> for w :: \<open>'a::len word\<close>
+  by (rule bit_word_eqI) (auto simp add: bit_set_bits_word_iff bit_imp_le_length)
+
+lemma set_bits_K_False [simp]:
+  \<open>set_bits (\<lambda>_. False) = (0 :: 'a :: len word)\<close>
+  by (rule bit_word_eqI) (simp add: bit_set_bits_word_iff)
 
 lemmas of_nth_def = word_set_bits_def (* FIXME duplicate *)
 
-lemma td_ext_nth [OF refl refl refl, unfolded word_size]:
-  "n = size w \<Longrightarrow> ofn = set_bits \<Longrightarrow> [w, ofn g] = l \<Longrightarrow>
-    td_ext test_bit ofn {f. \<forall>i. f i \<longrightarrow> i < n} (\<lambda>h i. h i \<and> i < n)"
-  for w :: "'a::len word"
-  apply (unfold word_size td_ext_def')
-  apply safe
-     apply (rule_tac [3] ext)
-     apply (rule_tac [4] ext)
-     apply (unfold word_size of_nth_def test_bit_bl)
-     apply safe
-       defer
-       apply (clarsimp simp: word_bl.Abs_inverse)+
-  apply (rule word_bl.Rep_inverse')
-  apply (rule sym [THEN trans])
-   apply (rule bl_of_nth_nth)
-  apply simp
-  apply (rule bl_of_nth_inj)
-  apply (clarsimp simp add : test_bit_bl word_size)
-  done
-
 interpretation test_bit:
   td_ext
     "(!!) :: 'a::len word \<Rightarrow> nat \<Rightarrow> bool"
     set_bits
     "{f. \<forall>i. f i \<longrightarrow> i < LENGTH('a::len)}"
     "(\<lambda>h i. h i \<and> i < LENGTH('a::len))"
-  by (rule td_ext_nth)
+  by standard
+    (auto simp add: test_bit_word_eq bit_imp_le_length bit_set_bits_word_iff set_bits_bit_eq)
 
 lemmas td_nth = test_bit.td_thm
 
-lemma set_bits_K_False [simp]:
-  "set_bits (\<lambda>_. False) = (0 :: 'a :: len word)"
-  by (rule word_eqI) (simp add: test_bit.eq_norm)
-
 
 subsection \<open>Shifting, Rotating, and Splitting Words\<close>
 
@@ -3492,9 +3465,8 @@
   done
 
 lemma shiftl1_rev: "shiftl1 w = word_reverse (shiftr1 (word_reverse w))"
-  apply (unfold word_reverse_def)
-  apply (rule word_bl.Rep_inverse' [symmetric])
-  apply (simp add: bl_shiftl1' bl_shiftr1' word_bl.Abs_inverse)
+  apply (rule bit_word_eqI)
+  apply (auto simp add: bit_shiftl1_iff bit_word_reverse_iff bit_shiftr1_iff Suc_diff_Suc)
   done
 
 lemma shiftl_rev: "shiftl w n = word_reverse (shiftr (word_reverse w) n)"
@@ -3873,25 +3845,172 @@
   by (simp add: mask_def word_size shiftl_zero_size)
 
 
+subsubsection \<open>Slices\<close>
+
+definition slice1 :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
+  where \<open>slice1 n w = (if n < LENGTH('a)
+    then ucast (drop_bit (LENGTH('a) - n) w)
+    else push_bit (n - LENGTH('a)) (ucast w))\<close>
+
+lemma bit_slice1_iff:
+  \<open>bit (slice1 m w :: 'b::len word) n \<longleftrightarrow> m - LENGTH('a) \<le> n \<and> n < min LENGTH('b) m
+    \<and> bit w (n + (LENGTH('a) - m) - (m - LENGTH('a)))\<close>
+  for w :: \<open>'a::len word\<close>
+  by (auto simp add: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff exp_eq_zero_iff not_less not_le ac_simps
+    dest: bit_imp_le_length)
+
+lemma slice1_eq_of_bl:
+  \<open>(slice1 n w :: 'b::len word) = of_bl (takefill False n (to_bl w))\<close>
+  for w :: \<open>'a::len word\<close>
+proof (rule bit_word_eqI)
+  fix m
+  assume \<open>m \<le> LENGTH('b)\<close>
+  show \<open>bit (slice1 n w :: 'b::len word) m \<longleftrightarrow> bit (of_bl (takefill False n (to_bl w)) :: 'b word) m\<close>
+    by (cases \<open>m \<ge> n\<close>; cases \<open>LENGTH('a) \<ge> n\<close>)
+      (auto simp add: bit_slice1_iff bit_of_bl_iff not_less rev_nth not_le nth_takefill nth_to_bl algebra_simps)
+qed
+
+definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
+  where \<open>slice n = slice1 (LENGTH('a) - n)\<close>
+
+lemma bit_slice_iff:
+  \<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp add: slice_def word_size bit_slice1_iff)
+
+lemma slice1_no_bin [simp]:
+  "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
+  by (simp add: slice1_eq_of_bl) (* TODO: neg_numeral *)
+
+lemma slice_no_bin [simp]:
+  "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n)
+    (bin_to_bl (LENGTH('b::len)) (numeral w)))"
+  by (simp add: slice_def) (* TODO: neg_numeral *)
+
+lemma slice1_0 [simp] : "slice1 n 0 = 0"
+  unfolding slice1_def by simp
+
+lemma slice_0 [simp] : "slice n 0 = 0"
+  unfolding slice_def by auto
+
+lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
+  by (simp add: slice_def word_size slice1_eq_of_bl takefill_alt)
+
+lemmas slice_take = slice_take' [unfolded word_size]
+
+\<comment> \<open>shiftr to a word of the same size is just slice,
+    slice is just shiftr then ucast\<close>
+lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
+
+lemma slice_shiftr: "slice n w = ucast (w >> n)"
+  apply (unfold slice_take shiftr_bl)
+  apply (rule ucast_of_bl_up [symmetric])
+  apply (simp add: word_size)
+  done
+
+lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
+  by (simp add: slice_shiftr nth_ucast nth_shiftr)
+
+lemma slice1_down_alt':
+  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
+    to_bl sl = takefill False fs (drop k (to_bl w))"
+  by (auto simp: slice1_eq_of_bl word_size of_bl_def uint_bl
+      word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
+
+lemma slice1_up_alt':
+  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
+    to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
+  apply (unfold slice1_eq_of_bl word_size of_bl_def uint_bl)
+  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
+  apply (rule_tac f = "\<lambda>k. takefill False (LENGTH('a))
+    (replicate k False @ bin_to_bl (LENGTH('b)) (uint w))" in arg_cong)
+  apply arith
+  done
+
+lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
+lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
+lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
+lemmas slice1_up_alts =
+  le_add_diff_inverse [symmetric, THEN su1]
+  le_add_diff_inverse2 [symmetric, THEN su1]
+
+lemma ucast_slice1: "ucast w = slice1 (size w) w"
+  by (simp add: slice1_def ucast_bl takefill_same' word_size)
+
+lemma ucast_slice: "ucast w = slice 0 w"
+  by (simp add: slice_def slice1_def)
+
+lemma slice_id: "slice 0 t = t"
+  by (simp only: ucast_slice [symmetric] ucast_id)
+
+lemma slice1_tf_tf':
+  "to_bl (slice1 n w :: 'a::len word) =
+    rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
+  unfolding slice1_eq_of_bl by (rule word_rev_tf)
+
+lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
+
+lemma rev_slice1:
+  "n + k = LENGTH('a) + LENGTH('b) \<Longrightarrow>
+    slice1 n (word_reverse w :: 'b::len word) =
+    word_reverse (slice1 k w :: 'a::len word)"
+  apply (unfold word_reverse_eq_of_bl_rev_to_bl slice1_tf_tf)
+  apply (rule word_bl.Rep_inverse')
+  apply (rule rev_swap [THEN iffD1])
+  apply (rule trans [symmetric])
+   apply (rule tf_rev)
+   apply (simp add: word_bl.Abs_inverse)
+  apply (simp add: word_bl.Abs_inverse)
+  done
+
+lemma rev_slice:
+  "n + k + LENGTH('a::len) = LENGTH('b::len) \<Longrightarrow>
+    slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
+  apply (unfold slice_def word_size)
+  apply (rule rev_slice1)
+  apply arith
+  done
+
+
 subsubsection \<open>Revcast\<close>
 
-lemmas revcast_def' = revcast_def [simplified]
-lemmas revcast_def'' = revcast_def' [simplified word_size]
-lemmas revcast_no_def [simp] = revcast_def' [where w="numeral w", unfolded word_size] for w
+definition revcast :: \<open>'a::len word \<Rightarrow> 'b::len word\<close>
+  where \<open>revcast = slice1 LENGTH('b)\<close>
+
+lemma bit_revcast_iff:
+  \<open>bit (revcast w :: 'b::len word) n \<longleftrightarrow> LENGTH('b) - LENGTH('a) \<le> n \<and> n < LENGTH('b)
+    \<and> bit w (n + (LENGTH('a) - LENGTH('b)) - (LENGTH('b) - LENGTH('a)))\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp add: revcast_def bit_slice1_iff)
+
+lemma revcast_eq_of_bl:
+  \<open>(revcast w :: 'b::len word) = of_bl (takefill False (LENGTH('b)) (to_bl w))\<close>
+  for w :: \<open>'a::len word\<close>
+  by (simp add: revcast_def slice1_eq_of_bl)
+
+lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
+  by (simp add: revcast_def word_size)
+
+lemmas revcast_no_def [simp] = revcast_eq_of_bl [where w="numeral w", unfolded word_size] for w
 
 lemma to_bl_revcast:
   "to_bl (revcast w :: 'a::len word) = takefill False (LENGTH('a)) (to_bl w)"
-  apply (unfold revcast_def' word_size)
-  apply (rule word_bl.Abs_inverse)
+  apply (rule nth_equalityI)
   apply simp
+  apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
+   apply (auto simp add: nth_to_bl nth_takefill bit_revcast_iff)
   done
 
 lemma revcast_rev_ucast [OF refl refl refl]:
   "cs = [rc, uc] \<Longrightarrow> rc = revcast (word_reverse w) \<Longrightarrow> uc = ucast w \<Longrightarrow>
     rc = word_reverse uc"
-  apply (unfold ucast_def revcast_def' Let_def word_reverse_def)
-  apply (auto simp: to_bl_of_bin takefill_bintrunc)
-  apply (simp add: word_bl.Abs_inverse word_size)
+  apply auto
+  apply (rule bit_word_eqI)
+  apply (cases \<open>LENGTH('a) \<le> LENGTH('b)\<close>)
+   apply (simp_all add: bit_revcast_iff bit_word_reverse_iff bit_ucast_iff not_le
+     bit_imp_le_length)
+  using bit_imp_le_length apply fastforce
+  using bit_imp_le_length apply fastforce
   done
 
 lemma revcast_ucast: "revcast w = word_reverse (ucast (word_reverse w))"
@@ -3911,7 +4030,7 @@
 lemma revcast_down_uu [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >> n)"
   for w :: "'a::len word"
-  apply (simp add: revcast_def')
+  apply (simp add: revcast_eq_of_bl)
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule ucast_down_drop)
    prefer 2
@@ -3922,7 +4041,7 @@
 lemma revcast_down_us [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = ucast (w >>> n)"
   for w :: "'a::len word"
-  apply (simp add: revcast_def')
+  apply (simp add: revcast_eq_of_bl)
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule ucast_down_drop)
    prefer 2
@@ -3933,7 +4052,7 @@
 lemma revcast_down_su [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >> n)"
   for w :: "'a::len word"
-  apply (simp add: revcast_def')
+  apply (simp add: revcast_eq_of_bl)
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule scast_down_drop)
    prefer 2
@@ -3944,7 +4063,7 @@
 lemma revcast_down_ss [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc = target_size rc + n \<Longrightarrow> rc w = scast (w >>> n)"
   for w :: "'a::len word"
-  apply (simp add: revcast_def')
+  apply (simp add: revcast_eq_of_bl)
   apply (rule word_bl.Rep_inverse')
   apply (rule trans, rule scast_down_drop)
    prefer 2
@@ -3968,7 +4087,7 @@
 lemma revcast_up [OF refl]:
   "rc = revcast \<Longrightarrow> source_size rc + n = target_size rc \<Longrightarrow>
     rc w = (ucast w :: 'a::len word) << n"
-  apply (simp add: revcast_def')
+  apply (simp add: revcast_eq_of_bl)
   apply (rule word_bl.Rep_inverse')
   apply (simp add: takefill_alt)
   apply (rule bl_shiftl [THEN trans])
@@ -3986,106 +4105,6 @@
 lemmas ucast_down =
   rc2 [simplified rev_shiftr revcast_ucast [symmetric]]
 
-
-subsubsection \<open>Slices\<close>
-
-lemma slice1_no_bin [simp]:
-  "slice1 n (numeral w :: 'b word) = of_bl (takefill False n (bin_to_bl (LENGTH('b::len)) (numeral w)))"
-  by (simp add: slice1_def) (* TODO: neg_numeral *)
-
-lemma slice_no_bin [simp]:
-  "slice n (numeral w :: 'b word) = of_bl (takefill False (LENGTH('b::len) - n)
-    (bin_to_bl (LENGTH('b::len)) (numeral w)))"
-  by (simp add: slice_def word_size) (* TODO: neg_numeral *)
-
-lemma slice1_0 [simp] : "slice1 n 0 = 0"
-  unfolding slice1_def by simp
-
-lemma slice_0 [simp] : "slice n 0 = 0"
-  unfolding slice_def by auto
-
-lemma slice_take': "slice n w = of_bl (take (size w - n) (to_bl w))"
-  unfolding slice_def' slice1_def
-  by (simp add : takefill_alt word_size)
-
-lemmas slice_take = slice_take' [unfolded word_size]
-
-\<comment> \<open>shiftr to a word of the same size is just slice,
-    slice is just shiftr then ucast\<close>
-lemmas shiftr_slice = trans [OF shiftr_bl [THEN meta_eq_to_obj_eq] slice_take [symmetric]]
-
-lemma slice_shiftr: "slice n w = ucast (w >> n)"
-  apply (unfold slice_take shiftr_bl)
-  apply (rule ucast_of_bl_up [symmetric])
-  apply (simp add: word_size)
-  done
-
-lemma nth_slice: "(slice n w :: 'a::len word) !! m = (w !! (m + n) \<and> m < LENGTH('a))"
-  by (simp add: slice_shiftr nth_ucast nth_shiftr)
-
-lemma slice1_down_alt':
-  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs + k = n \<Longrightarrow>
-    to_bl sl = takefill False fs (drop k (to_bl w))"
-  by (auto simp: slice1_def word_size of_bl_def uint_bl
-      word_ubin.eq_norm bl_bin_bl_rep_drop drop_takefill)
-
-lemma slice1_up_alt':
-  "sl = slice1 n w \<Longrightarrow> fs = size sl \<Longrightarrow> fs = n + k \<Longrightarrow>
-    to_bl sl = takefill False fs (replicate k False @ (to_bl w))"
-  apply (unfold slice1_def word_size of_bl_def uint_bl)
-  apply (clarsimp simp: word_ubin.eq_norm bl_bin_bl_rep_drop takefill_append [symmetric])
-  apply (rule_tac f = "\<lambda>k. takefill False (LENGTH('a))
-    (replicate k False @ bin_to_bl (LENGTH('b)) (uint w))" in arg_cong)
-  apply arith
-  done
-
-lemmas sd1 = slice1_down_alt' [OF refl refl, unfolded word_size]
-lemmas su1 = slice1_up_alt' [OF refl refl, unfolded word_size]
-lemmas slice1_down_alt = le_add_diff_inverse [THEN sd1]
-lemmas slice1_up_alts =
-  le_add_diff_inverse [symmetric, THEN su1]
-  le_add_diff_inverse2 [symmetric, THEN su1]
-
-lemma ucast_slice1: "ucast w = slice1 (size w) w"
-  by (simp add: slice1_def ucast_bl takefill_same' word_size)
-
-lemma ucast_slice: "ucast w = slice 0 w"
-  by (simp add: slice_def ucast_slice1)
-
-lemma slice_id: "slice 0 t = t"
-  by (simp only: ucast_slice [symmetric] ucast_id)
-
-lemma revcast_slice1 [OF refl]: "rc = revcast w \<Longrightarrow> slice1 (size rc) w = rc"
-  by (simp add: slice1_def revcast_def' word_size)
-
-lemma slice1_tf_tf':
-  "to_bl (slice1 n w :: 'a::len word) =
-    rev (takefill False (LENGTH('a)) (rev (takefill False n (to_bl w))))"
-  unfolding slice1_def by (rule word_rev_tf)
-
-lemmas slice1_tf_tf = slice1_tf_tf' [THEN word_bl.Rep_inverse', symmetric]
-
-lemma rev_slice1:
-  "n + k = LENGTH('a) + LENGTH('b) \<Longrightarrow>
-    slice1 n (word_reverse w :: 'b::len word) =
-    word_reverse (slice1 k w :: 'a::len word)"
-  apply (unfold word_reverse_def slice1_tf_tf)
-  apply (rule word_bl.Rep_inverse')
-  apply (rule rev_swap [THEN iffD1])
-  apply (rule trans [symmetric])
-   apply (rule tf_rev)
-   apply (simp add: word_bl.Abs_inverse)
-  apply (simp add: word_bl.Abs_inverse)
-  done
-
-lemma rev_slice:
-  "n + k + LENGTH('a::len) = LENGTH('b::len) \<Longrightarrow>
-    slice n (word_reverse (w::'b word)) = word_reverse (slice k w :: 'a word)"
-  apply (unfold slice_def word_size)
-  apply (rule rev_slice1)
-  apply arith
-  done
-
 lemmas sym_notr =
   not_iff [THEN iffD2, THEN not_sym, THEN not_iff [THEN iffD1]]