word_lib: reduce warnings

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib/Word_Lib/Bits_Int.thy

@@ -86,10 +86,6 @@ lemma bin_nth_numeral: "bin_rest x = y \<Longrightarrow> bin_nth x (numeral n) =
   by (simp add: numeral_eq_Suc bit_Suc)
 
 lemmas bin_nth_numeral_simps [simp] =
-  bin_nth_numeral [OF bin_rest_numeral_simps(2)]
-  bin_nth_numeral [OF bin_rest_numeral_simps(5)]
-  bin_nth_numeral [OF bin_rest_numeral_simps(6)]
-  bin_nth_numeral [OF bin_rest_numeral_simps(7)]
   bin_nth_numeral [OF bin_rest_numeral_simps(8)]
 
 lemmas bin_nth_simps =
@@ -207,7 +203,7 @@ lemma bin_nth_Bit1:
   by auto
 
 lemma bintrunc_bintrunc_l: "n \<le> m \<Longrightarrow> bintrunc m (bintrunc n w) = bintrunc n w"
-  by (simp add: min.absorb2)
+  by simp
 
 lemma sbintrunc_sbintrunc_l: "n \<le> m \<Longrightarrow> sbintrunc m (sbintrunc n w) = sbintrunc n w"
   by (simp add: min_def)
@@ -216,10 +212,10 @@ lemma bintrunc_bintrunc_ge: "n \<le> m \<Longrightarrow> bintrunc n (bintrunc m
   by (rule bin_eqI) (auto simp: nth_bintr)
 
 lemma bintrunc_bintrunc_min [simp]: "bintrunc m (bintrunc n w) = bintrunc (min m n) w"
-  by (rule bin_eqI) (auto simp: nth_bintr)
+  by (rule take_bit_take_bit)
 
 lemma sbintrunc_sbintrunc_min [simp]: "sbintrunc m (sbintrunc n w) = sbintrunc (min m n) w"
-  by (rule bin_eqI) (auto simp: nth_sbintr min.absorb1 min.absorb2)
+  by (rule signed_take_bit_signed_take_bit)
 
 lemmas sbintrunc_Suc_Pls =
   signed_take_bit_Suc [where a="0::int", simplified bin_last_numeral_simps bin_rest_numeral_simps]
@@ -262,7 +258,7 @@ lemma sbintrunc_Suc_Is:
   by auto
 
 lemma sbintrunc_Suc_lem: "sbintrunc (Suc n) x = y \<Longrightarrow> m = Suc n \<Longrightarrow> sbintrunc m x = y"
-  by auto
+  by (rule ssubst)
 
 lemmas sbintrunc_Suc_Ialts =
   sbintrunc_Suc_Is [THEN sbintrunc_Suc_lem]
@@ -271,9 +267,7 @@ lemma sbintrunc_bintrunc_lt: "m > n \<Longrightarrow> sbintrunc n (bintrunc m w)
   by (rule bin_eqI) (auto simp: nth_sbintr nth_bintr)
 
 lemma bintrunc_sbintrunc_le: "m \<le> Suc n \<Longrightarrow> bintrunc m (sbintrunc n w) = bintrunc m w"
-  apply (rule bin_eqI)
-  using le_Suc_eq less_Suc_eq_le apply (auto simp: nth_sbintr nth_bintr)
-  done
+  by (rule take_bit_signed_take_bit)
 
 lemmas bintrunc_sbintrunc [simp] = order_refl [THEN bintrunc_sbintrunc_le]
 lemmas sbintrunc_bintrunc [simp] = lessI [THEN sbintrunc_bintrunc_lt]

lib/Word_Lib/Bitwise.thy

@@ -427,7 +427,7 @@ val word_len_simproc =
 
 fun nat_get_Suc_simproc_fn n_sucs ctxt ct =
   let
-    val (f $ arg) = Thm.term_of ct;
+    val (f, arg) = dest_comb (Thm.term_of ct);
     val n =
       (case arg of \<^term>\<open>nat\<close> $ n => n | n => n)
       |> HOLogic.dest_number |> snd;

lib/Word_Lib/Generic_set_bit.thy

@@ -89,7 +89,7 @@ lemma set_bit_unfold:
 lemma bit_set_bit_word_iff [bit_simps]:
   \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
   for w :: \<open>'a::len word\<close>
-  by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length)
+  by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff not_le bit_imp_le_length)
 
 lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
   for w :: "'a::len word"

lib/Word_Lib/More_Word_Operations.thy

@@ -238,13 +238,11 @@ lemma word_log2_max:
 
 lemma word_clz_0[simp]:
   "word_clz (0::'a::len word) = LENGTH('a)"
-  unfolding word_clz_def
-  by (simp add: takeWhile_replicate)
+  unfolding word_clz_def by simp
 
 lemma word_clz_minus_one[simp]:
   "word_clz (-1::'a::len word) = 0"
-  unfolding word_clz_def
-  by (simp add: takeWhile_replicate)
+  unfolding word_clz_def by simp
 
 lemma is_aligned_alignUp[simp]:
   "is_aligned (alignUp p n) n"
@@ -334,7 +332,7 @@ next
     apply (subst unat_word_ariths)
     apply simp
     apply (subst mult_mod_left)
-    apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power min.absorb2)
+    apply (simp add: unat_div field_simps power_add[symmetric] mod_mod_power)
     done
   ultimately have lt: "2 ^ n * (unat a div 2 ^ n + 1) < 2 ^ LENGTH('a)" by simp
 
@@ -527,8 +525,7 @@ proof -
     hence allj: "\<forall>j\<in>set(to_bl w). \<not> j"
       by (metis a length_takeWhile_less less_irrefl_nat word_clz_def)
     hence "to_bl w = replicate (length (to_bl w)) False"
-      by (auto simp add: to_bl_unfold rev_map simp flip: map_replicate_trivial)
-        (metis allj eq_zero_set_bl nz)
+      using eq_zero_set_bl nz by fastforce
     hence "w = 0"
       by (metis to_bl_0 word_bl.Rep_eqD word_bl_Rep')
     with nz have False by simp

lib/Word_Lib/Reversed_Bit_Lists.thy

@@ -936,7 +936,7 @@ lemma bin_cat_foldl_lem:
   apply (drule meta_spec)
   apply (erule trans)
   apply (drule_tac x = "bin_cat y n a" in meta_spec)
-  apply (simp add: bin_cat_assoc_sym min.absorb2)
+  apply (simp add: bin_cat_assoc_sym)
   done
 
 lemma bin_rcat_bl: "bin_rcat n wl = bl_to_bin (concat (map (bin_to_bl n) wl))"

lib/Word_Lib/Traditional_Infix_Syntax.thy

@@ -173,7 +173,7 @@ qed
 lemma bit_shiftl_word_iff [bit_simps]:
   \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le)
+  by (simp add: shiftl_word_eq bit_push_bit_iff not_le)
 
 lemma bit_shiftr_word_iff [bit_simps]:
   \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
@@ -473,9 +473,8 @@ lemma test_bit_split':
     (\<forall>n m.
       b !! n = (n < size b \<and> c !! n) \<and>
       a !! m = (m < size a \<and> c !! (m + size b)))"
-  by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size
-    bit_drop_bit_eq ac_simps exp_eq_zero_iff
-    dest: bit_imp_le_length)
+  by (auto simp add: word_split_bin' test_bit_bin bit_unsigned_iff word_size bit_drop_bit_eq ac_simps
+           dest: bit_imp_le_length)
 
 lemma test_bit_split:
   "word_split c = (a, b) \<Longrightarrow>