# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1724539445 -3600
# Node ID 8f96e1329845348c1d82e8180e2194fd680bf587
# Parent  32f0e953cc96fe65a607fe395a8ebc6319dde74e
Some tidying

diff -r 32f0e953cc96 -r 8f96e1329845 src/HOL/Bit_Operations.thy
--- a/src/HOL/Bit_Operations.thy	Sat Aug 24 14:14:57 2024 +0100
+++ b/src/HOL/Bit_Operations.thy	Sat Aug 24 23:44:05 2024 +0100
@@ -148,7 +148,7 @@
 
 lemma bit_imp_possible_bit:
   \<open>possible_bit TYPE('a) n\<close> if \<open>bit a n\<close>
-  by (rule ccontr) (use that in \<open>auto simp add: bit_iff_odd possible_bit_def\<close>)
+  by (rule ccontr) (use that in \<open>auto simp: bit_iff_odd possible_bit_def\<close>)
 
 lemma impossible_bit:
   \<open>\<not> bit a n\<close> if \<open>\<not> possible_bit TYPE('a) n\<close>
@@ -161,7 +161,7 @@
 
 lemma possible_bit_min [simp]:
   \<open>possible_bit TYPE('a) (min i j) \<longleftrightarrow> possible_bit TYPE('a) i \<or> possible_bit TYPE('a) j\<close>
-  by (auto simp add: min_def elim: possible_bit_less_imp)
+  by (auto simp: min_def elim: possible_bit_less_imp)
 
 lemma bit_eqI:
   \<open>a = b\<close> if \<open>\<And>n. possible_bit TYPE('a) n \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
@@ -213,7 +213,7 @@
     also have \<open>\<dots> = b\<close>
       by (fact mod_mult_div_eq)
     finally show ?case
-      by (auto simp add: mod2_eq_if)
+      by (auto simp: mod2_eq_if)
   qed
 qed
 
@@ -262,7 +262,7 @@
   \<open>bit (2 * a) (Suc n) \<longleftrightarrow> possible_bit TYPE('a) (Suc n) \<and> bit a n\<close>
   using even_double_div_exp_iff [of n a]
   by (cases \<open>possible_bit TYPE('a) (Suc n)\<close>)
-    (auto simp add: bit_iff_odd possible_bit_def)
+    (auto simp: bit_iff_odd possible_bit_def)
 
 lemma bit_double_iff [bit_simps]:
   \<open>bit (2 * a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> 0 \<and> bit a (n - 1)\<close>
@@ -382,7 +382,7 @@
     with rec [of n True] show ?case
       by simp
   qed
-qed (auto simp add: div_mult2_eq bit_nat_def)
+qed (auto simp: div_mult2_eq bit_nat_def)
 
 end
 
@@ -422,12 +422,12 @@
     case (even m)
     then show ?case
       by (cases n)
-        (auto simp add: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero)
+        (auto simp: bit_double_iff Bit_Operations.bit_double_iff possible_bit_def bit_0 dest: mult_not_zero)
   next
     case (odd m)
     then show ?case
       by (cases n)
-        (auto simp add: bit_double_iff even_bit_succ_iff possible_bit_def
+        (auto simp: bit_double_iff even_bit_succ_iff possible_bit_def
           Bit_Operations.bit_Suc Bit_Operations.bit_0 dest: mult_not_zero)
   qed
   with True show ?thesis
@@ -521,7 +521,7 @@
     with rec [of k True] show ?case
       by (simp add: ac_simps)
   qed
-qed (auto simp add: zdiv_zmult2_eq bit_int_def)
+qed (auto simp: zdiv_zmult2_eq bit_int_def)
 
 end
 
@@ -637,25 +637,25 @@
 qed
 
 sublocale "and": semilattice \<open>(AND)\<close>
-  by standard (auto simp add: bit_eq_iff bit_and_iff)
+  by standard (auto simp: bit_eq_iff bit_and_iff)
 
 sublocale or: semilattice_neutr \<open>(OR)\<close> 0
-  by standard (auto simp add: bit_eq_iff bit_or_iff)
+  by standard (auto simp: bit_eq_iff bit_or_iff)
 
 sublocale xor: comm_monoid \<open>(XOR)\<close> 0
-  by standard (auto simp add: bit_eq_iff bit_xor_iff)
+  by standard (auto simp: bit_eq_iff bit_xor_iff)
 
 lemma even_and_iff:
   \<open>even (a AND b) \<longleftrightarrow> even a \<or> even b\<close>
-  using bit_and_iff [of a b 0] by (auto simp add: bit_0)
+  using bit_and_iff [of a b 0] by (auto simp: bit_0)
 
 lemma even_or_iff:
   \<open>even (a OR b) \<longleftrightarrow> even a \<and> even b\<close>
-  using bit_or_iff [of a b 0] by (auto simp add: bit_0)
+  using bit_or_iff [of a b 0] by (auto simp: bit_0)
 
 lemma even_xor_iff:
   \<open>even (a XOR b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)\<close>
-  using bit_xor_iff [of a b 0] by (auto simp add: bit_0)
+  using bit_xor_iff [of a b 0] by (auto simp: bit_0)
 
 lemma zero_and_eq [simp]:
   \<open>0 AND a = 0\<close>
@@ -667,7 +667,7 @@
 
 lemma one_and_eq:
   \<open>1 AND a = a mod 2\<close>
-  by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff bit_0)
+  by (simp add: bit_eq_iff bit_and_iff) (auto simp: bit_1_iff bit_0)
 
 lemma and_one_eq:
   \<open>a AND 1 = a mod 2\<close>
@@ -676,7 +676,7 @@
 lemma one_or_eq:
   \<open>1 OR a = a + of_bool (even a)\<close>
   by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff)
-    (auto simp add: bit_1_iff bit_0)
+    (auto simp: bit_1_iff bit_0)
 
 lemma or_one_eq:
   \<open>a OR 1 = a + of_bool (even a)\<close>
@@ -685,7 +685,7 @@
 lemma one_xor_eq:
   \<open>1 XOR a = a + of_bool (even a) - of_bool (odd a)\<close>
   by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff)
-    (auto simp add: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE)
+    (auto simp: bit_1_iff odd_bit_iff_bit_pred bit_0 elim: oddE)
 
 lemma xor_one_eq:
   \<open>a XOR 1 = a + of_bool (even a) - of_bool (odd a)\<close>
@@ -762,7 +762,7 @@
 
 lemma even_mask_iff:
   \<open>even (mask n) \<longleftrightarrow> n = 0\<close>
-  using bit_mask_iff [of n 0] by (auto simp add: bit_0)
+  using bit_mask_iff [of n 0] by (auto simp: bit_0)
 
 lemma mask_Suc_0 [simp]:
   \<open>mask (Suc 0) = 1\<close>
@@ -770,7 +770,7 @@
 
 lemma mask_Suc_exp:
   \<open>mask (Suc n) = 2 ^ n OR mask n\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma mask_numeral:
   \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close>
@@ -793,20 +793,19 @@
 proof (induction n arbitrary: m)
   case 0
   then show ?case
-    by (auto simp add: bit_0 push_bit_eq_mult)
+    by (auto simp: bit_0 push_bit_eq_mult)
 next
   case (Suc n)
   show ?case
   proof (cases m)
     case 0
     then show ?thesis
-      by (auto simp add: bit_imp_possible_bit)
+      by (auto simp: bit_imp_possible_bit)
   next
-    case (Suc m)
-    with Suc.prems Suc.IH [of m] show ?thesis
+    case (Suc m')
+    with Suc.prems Suc.IH [of m'] show ?thesis
       apply (simp add: push_bit_double)
-      apply (simp add: bit_simps mult.commute [of _ 2])
-      apply (auto simp add: possible_bit_less_imp)
+      apply (auto simp: possible_bit_less_imp bit_simps mult.commute [of _ 2])
       done
   qed
 qed
@@ -849,7 +848,7 @@
 
 lemma disjunctive_xor_eq_or:
   \<open>a XOR b = a OR b\<close> if \<open>a AND b = 0\<close>
-  using that by (auto simp add: bit_eq_iff bit_simps)
+  using that by (auto simp: bit_eq_iff bit_simps)
 
 lemma disjunctive_add_eq_or:
   \<open>a + b = a OR b\<close> if \<open>a AND b = 0\<close>
@@ -864,11 +863,11 @@
   proof (induction n arbitrary: a b)
     case 0
     from "0"(2)[of 0] show ?case
-      by (auto simp add: even_or_iff bit_0)
+      by (auto simp: even_or_iff bit_0)
   next
     case (Suc n)
     from Suc.prems(2) [of 0] have even: \<open>even a \<or> even b\<close>
-      by (auto simp add: bit_0)
+      by (auto simp: bit_0)
     have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
       using Suc.prems(2) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
     from Suc.prems have \<open>possible_bit TYPE('a) n\<close>
@@ -879,7 +878,7 @@
     have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
       using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
     also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
-      using even by (auto simp add: algebra_simps mod2_eq_if)
+      using even by (auto simp: algebra_simps mod2_eq_if)
     finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
       using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
     also have \<open>\<dots> \<longleftrightarrow> bit (a div 2 OR b div 2) n\<close>
@@ -929,9 +928,9 @@
   also have \<open>\<dots> \<longleftrightarrow> m \<le> n \<and> bit a n \<or> n < m \<and> bit a n\<close>
     by auto
   also have \<open>m \<le> n \<and> bit a n \<longleftrightarrow> bit (push_bit m (drop_bit m a)) n\<close>
-    by (auto simp add: bit_simps bit_imp_possible_bit)
+    by (auto simp: bit_simps bit_imp_possible_bit)
   finally show ?thesis
-    by (auto simp add: bit_simps)
+    by (auto simp: bit_simps)
 qed
 
 lemma take_bit_Suc:
@@ -1004,19 +1003,19 @@
 
 lemma push_bit_take_bit:
   \<open>push_bit m (take_bit n a) = take_bit (m + n) (push_bit m a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma take_bit_push_bit:
   \<open>take_bit m (push_bit n a) = push_bit n (take_bit (m - n) a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma take_bit_drop_bit:
   \<open>take_bit m (drop_bit n a) = drop_bit n (take_bit (m + n) a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma drop_bit_take_bit:
   \<open>drop_bit m (take_bit n a) = take_bit (n - m) (drop_bit m a)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma even_push_bit_iff [simp]:
   \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
@@ -1091,49 +1090,49 @@
     then have \<open> \<not> bit a (n + (m - n))\<close>
       by (simp add: bit_simps)
     then show \<open>bit (take_bit n a) m \<longleftrightarrow> bit a m\<close>
-      by (cases \<open>m < n\<close>) (auto simp add: bit_simps)
+      by (cases \<open>m < n\<close>) (auto simp: bit_simps)
   qed
 qed
 
 lemma drop_bit_exp_eq:
   \<open>drop_bit m (2 ^ n) = of_bool (m \<le> n \<and> possible_bit TYPE('a) n) * 2 ^ (n - m)\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma take_bit_and [simp]:
   \<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma take_bit_or [simp]:
   \<open>take_bit n (a OR b) = take_bit n a OR take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma take_bit_xor [simp]:
   \<open>take_bit n (a XOR b) = take_bit n a XOR take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma push_bit_and [simp]:
   \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma push_bit_or [simp]:
   \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma push_bit_xor [simp]:
   \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma drop_bit_and [simp]:
   \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma drop_bit_or [simp]:
   \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma drop_bit_xor [simp]:
   \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma take_bit_of_mask [simp]:
   \<open>take_bit m (mask n) = mask (min m n)\<close>
@@ -1141,11 +1140,11 @@
 
 lemma take_bit_eq_mask:
   \<open>take_bit n a = a AND mask n\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma or_eq_0_iff:
   \<open>a OR b = 0 \<longleftrightarrow> a = 0 \<and> b = 0\<close>
-  by (auto simp add: bit_eq_iff bit_or_iff)
+  by (auto simp: bit_eq_iff bit_or_iff)
 
 lemma bit_iff_and_drop_bit_eq_1:
   \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
@@ -1157,23 +1156,23 @@
 
 lemma bit_set_bit_iff [bit_simps]:
   \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> possible_bit TYPE('a) n)\<close>
-  by (auto simp add: set_bit_eq_or bit_or_iff bit_exp_iff)
+  by (auto simp: set_bit_eq_or bit_or_iff bit_exp_iff)
 
 lemma even_set_bit_iff:
   \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
-  using bit_set_bit_iff [of m a 0] by (auto simp add: bit_0)
+  using bit_set_bit_iff [of m a 0] by (auto simp: bit_0)
 
 lemma bit_unset_bit_iff [bit_simps]:
   \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
-  by (auto simp add: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit)
+  by (auto simp: unset_bit_eq_or_xor bit_simps dest: bit_imp_possible_bit)
 
 lemma even_unset_bit_iff:
   \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
-  using bit_unset_bit_iff [of m a 0] by (auto simp add: bit_0)
+  using bit_unset_bit_iff [of m a 0] by (auto simp: bit_0)
 
 lemma bit_flip_bit_iff [bit_simps]:
   \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> possible_bit TYPE('a) n\<close>
-  by (auto simp add: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)
+  by (auto simp: bit_eq_iff bit_simps flip_bit_eq_xor bit_imp_possible_bit)
 
 lemma even_flip_bit_iff:
   \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
@@ -1182,7 +1181,7 @@
 lemma and_exp_eq_0_iff_not_bit:
   \<open>a AND 2 ^ n = 0 \<longleftrightarrow> \<not> bit a n\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
   using bit_imp_possible_bit[of a n]
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma bit_sum_mult_2_cases:
   assumes a: \<open>\<forall>j. \<not> bit a (Suc j)\<close>
@@ -1191,52 +1190,52 @@
   from a have \<open>n = 0\<close> if \<open>bit a n\<close> for n using that
     by (cases n) simp_all
   then have \<open>a = 0 \<or> a = 1\<close>
-    by (auto simp add: bit_eq_iff bit_1_iff)
+    by (auto simp: bit_eq_iff bit_1_iff)
   then show ?thesis
-    by (cases n) (auto simp add: bit_0 bit_double_iff even_bit_succ_iff)
+    by (cases n) (auto simp: bit_0 bit_double_iff even_bit_succ_iff)
 qed
 
 lemma set_bit_0 [simp]:
   \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
+  by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff simp flip: bit_Suc)
 
 lemma set_bit_Suc:
   \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
+  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
     elim: possible_bit_less_imp)
 
 lemma unset_bit_0 [simp]:
   \<open>unset_bit 0 a = 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps simp flip: bit_Suc)
+  by (auto simp: bit_eq_iff bit_simps simp flip: bit_Suc)
 
 lemma unset_bit_Suc:
   \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
+  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc)
 
 lemma flip_bit_0 [simp]:
   \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
+  by (auto simp: bit_eq_iff bit_simps even_bit_succ_iff bit_0 simp flip: bit_Suc)
 
 lemma flip_bit_Suc:
   \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
-  by (auto simp add: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
+  by (auto simp: bit_eq_iff bit_sum_mult_2_cases bit_simps bit_0 simp flip: bit_Suc
     elim: possible_bit_less_imp)
 
 lemma flip_bit_eq_if:
   \<open>flip_bit n a = (if bit a n then unset_bit else set_bit) n a\<close>
-  by (rule bit_eqI) (auto simp add: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)
+  by (rule bit_eqI) (auto simp: bit_set_bit_iff bit_unset_bit_iff bit_flip_bit_iff)
 
 lemma take_bit_set_bit_eq:
   \<open>take_bit n (set_bit m a) = (if n \<le> m then take_bit n a else set_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_set_bit_iff)
+  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_set_bit_iff)
 
 lemma take_bit_unset_bit_eq:
   \<open>take_bit n (unset_bit m a) = (if n \<le> m then take_bit n a else unset_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_unset_bit_iff)
+  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_unset_bit_iff)
 
 lemma take_bit_flip_bit_eq:
   \<open>take_bit n (flip_bit m a) = (if n \<le> m then take_bit n a else flip_bit m (take_bit n a))\<close>
-  by (rule bit_eqI) (auto simp add: bit_take_bit_iff bit_flip_bit_iff)
+  by (rule bit_eqI) (auto simp: bit_take_bit_iff bit_flip_bit_iff)
 
 lemma bit_1_0 [simp]:
   \<open>bit 1 0\<close>
@@ -1272,17 +1271,17 @@
     with bit_rec [of _ n] Cons.prems Cons.IH [of m]
     show ?thesis
       by (simp add: bit_simps)
-        (auto simp add: possible_bit_less_imp bit_simps simp flip: bit_Suc)
+        (auto simp: possible_bit_less_imp bit_simps simp flip: bit_Suc)
   qed
 qed
 
 lemma horner_sum_bit_eq_take_bit:
   \<open>horner_sum of_bool 2 (map (bit a) [0..<n]) = take_bit n a\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma take_bit_horner_sum_bit_eq:
   \<open>take_bit n (horner_sum of_bool 2 bs) = horner_sum of_bool 2 (take n bs)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
+  by (auto simp: bit_eq_iff bit_take_bit_iff bit_horner_sum_bit_iff)
 
 lemma take_bit_sum:
   \<open>take_bit n a = (\<Sum>k = 0..<n. push_bit k (of_bool (bit a k)))\<close>
@@ -1292,9 +1291,9 @@
   \<open>set_bit n a = a + of_bool (\<not> bit a n) * 2 ^ n\<close>
 proof -
   have \<open>a AND of_bool (\<not> bit a n) * 2 ^ n = 0\<close>
-    by (auto simp add: bit_eq_iff bit_simps)
+    by (auto simp: bit_eq_iff bit_simps)
   then show ?thesis
-    by (auto simp add: bit_eq_iff bit_simps disjunctive_add_eq_or)
+    by (auto simp: bit_eq_iff bit_simps disjunctive_add_eq_or)
 qed
 
 end
@@ -1360,7 +1359,7 @@
 
 lemma bit_not_exp_iff [bit_simps]:
   \<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<noteq> m\<close>
-  by (auto simp add: bit_not_iff bit_exp_iff)
+  by (auto simp: bit_not_iff bit_exp_iff)
 
 lemma bit_minus_iff [bit_simps]:
   \<open>bit (- a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> \<not> bit (a - 1) n\<close>
@@ -1372,7 +1371,7 @@
 
 lemma bit_minus_exp_iff [bit_simps]:
   \<open>bit (- (2 ^ m)) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n \<ge> m\<close>
-  by (auto simp add: bit_simps simp flip: mask_eq_exp_minus_1)
+  by (auto simp: bit_simps simp flip: mask_eq_exp_minus_1)
 
 lemma bit_minus_2_iff [simp]:
   \<open>bit (- 2) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> n > 0\<close>
@@ -1394,13 +1393,13 @@
   by standard (rule bit_eqI, simp add: bit_and_iff)
 
 sublocale bit: abstract_boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
-  by standard (auto simp add: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
+  by standard (auto simp: bit_and_iff bit_or_iff bit_not_iff intro: bit_eqI)
 
 sublocale bit: abstract_boolean_algebra_sym_diff \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close> \<open>(XOR)\<close>
-  apply standard
-  apply (rule bit_eqI)
-  apply (auto simp add: bit_simps)
-  done
+proof
+  show \<open>\<And>x y. x XOR y = x AND NOT y OR NOT x AND y\<close>
+    by (intro bit_eqI) (auto simp: bit_simps)
+qed
 
 lemma and_eq_not_not_or:
   \<open>a AND b = NOT (NOT a OR NOT b)\<close>
@@ -1424,7 +1423,7 @@
 
 lemma disjunctive_and_not_eq_xor:
   \<open>a AND NOT b = a XOR b\<close> if \<open>NOT a AND b = 0\<close>
-  using that by (auto simp add: bit_eq_iff bit_simps)
+  using that by (auto simp: bit_eq_iff bit_simps)
 
 lemma disjunctive_diff_eq_and_not:
   \<open>a - b = a AND NOT b\<close> if \<open>NOT a AND b = 0\<close>
@@ -1447,11 +1446,11 @@
 
 lemma take_bit_not_take_bit:
   \<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
-  by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff)
+  by (auto simp: bit_eq_iff bit_take_bit_iff bit_not_iff)
 
 lemma take_bit_not_iff:
   \<open>take_bit n (NOT a) = take_bit n (NOT b) \<longleftrightarrow> take_bit n a = take_bit n b\<close>
-  by (auto simp add: bit_eq_iff bit_simps)
+  by (auto simp: bit_eq_iff bit_simps)
 
 lemma take_bit_not_eq_mask_diff:
   \<open>take_bit n (NOT a) = mask n - take_bit n a\<close>
@@ -1459,7 +1458,7 @@
   have \<open>NOT (mask n) AND take_bit n a = 0\<close>
     by (simp add: bit_eq_iff bit_simps)
   moreover have \<open>take_bit n (NOT a) = mask n AND NOT (take_bit n a)\<close>
-    by (auto simp add: bit_eq_iff bit_simps)
+    by (auto simp: bit_eq_iff bit_simps)
   ultimately show ?thesis
     by (simp add: disjunctive_diff_eq_and_not)
 qed
@@ -1486,14 +1485,11 @@
 
 lemma unset_bit_eq_and_not:
   \<open>unset_bit n a = a AND NOT (push_bit n 1)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma push_bit_Suc_minus_numeral [simp]:
   \<open>push_bit (Suc n) (- numeral k) = push_bit n (- numeral (Num.Bit0 k))\<close>
-  apply (simp only: numeral_Bit0)
-  apply simp
-  apply (simp only: numeral_mult mult_2_right numeral_add)
-  done
+  using local.push_bit_Suc_numeral push_bit_minus by presburger
 
 lemma push_bit_minus_numeral [simp]:
   \<open>push_bit (numeral l) (- numeral k) = push_bit (pred_numeral l) (- numeral (Num.Bit0 k))\<close>
@@ -1509,11 +1505,11 @@
 
 lemma push_bit_mask_eq:
   \<open>push_bit m (mask n) = mask (n + m) AND NOT (mask m)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps not_less possible_bit_less_imp)
+  by (rule bit_eqI) (auto simp: bit_simps not_less possible_bit_less_imp)
 
 lemma slice_eq_mask:
   \<open>push_bit n (take_bit m (drop_bit n a)) = a AND mask (m + n) AND NOT (mask n)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps)
+  by (rule bit_eqI) (auto simp: bit_simps)
 
 lemma push_bit_numeral_minus_1 [simp]:
   \<open>push_bit (numeral n) (- 1) = - (2 ^ numeral n)\<close>
@@ -1523,9 +1519,9 @@
   \<open>unset_bit n a = a - of_bool (bit a n) * 2 ^ n\<close>
 proof -
   have \<open>NOT a AND of_bool (bit a n) * 2 ^ n = 0\<close>
-    by (auto simp add: bit_eq_iff bit_simps)
+    by (auto simp: bit_eq_iff bit_simps)
   moreover have \<open>unset_bit n a = a AND NOT (of_bool (bit a n) * 2 ^ n)\<close>
-    by (auto simp add: bit_eq_iff bit_simps)
+    by (auto simp: bit_eq_iff bit_simps)
   ultimately show ?thesis
     by (simp add: disjunctive_diff_eq_and_not)
 qed
@@ -1616,7 +1612,7 @@
 
 lemma drop_bit_mask_eq:
   \<open>drop_bit m (mask n) = mask (n - m)\<close>
-  by (rule bit_eqI) (auto simp add: bit_simps possible_bit_def)
+  by (rule bit_eqI) (auto simp: bit_simps possible_bit_def)
 
 lemma bit_push_bit_iff':
   \<open>bit (push_bit m a) n \<longleftrightarrow> m \<le> n \<and> bit a (n - m)\<close>
@@ -1645,7 +1641,7 @@
 proof (rule ccontr)
   assume \<open>\<not> 0 < take_bit m a\<close>
   then have \<open>take_bit m a = 0\<close>
-    by (auto simp add: not_less intro: order_antisym)
+    by (auto simp: not_less intro: order_antisym)
   then have \<open>bit (take_bit m a) n = bit 0 n\<close>
     by simp
   with that show False
@@ -1659,7 +1655,7 @@
 lemma drop_bit_push_bit:
   \<open>drop_bit m (push_bit n a) = drop_bit (m - n) (push_bit (n - m) a)\<close>
   by (cases \<open>m \<le> n\<close>)
-    (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
+    (auto simp: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
     mult.commute [of a] drop_bit_eq_div push_bit_eq_mult not_le power_add Orderings.not_le dest!: le_Suc_ex less_imp_Suc_add)
 
 end
@@ -1684,7 +1680,7 @@
   have less_eq: \<open>\<bar>k div 2\<bar> \<le> \<bar>k\<bar>\<close> for k :: int
     by (cases k) (simp_all add: divide_int_def nat_add_distrib)
   then have less: \<open>\<bar>k div 2\<bar> < \<bar>k\<bar>\<close> if \<open>k \<notin> {0, - 1}\<close> for k :: int
-    using that by (auto simp add: less_le [of k])
+    using that by (auto simp: less_le [of k])
   show \<open>wf (measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>)))\<close>
     by simp
   show \<open>((k div 2, l div 2), k, l) \<in> measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>
@@ -1721,11 +1717,11 @@
 proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
   case True
   then show ?thesis
-    by (auto simp add: F.simps [of 0] F.simps [of \<open>- 1\<close>])
+    by (auto simp: F.simps [of 0] F.simps [of \<open>- 1\<close>])
 next
   case False
   then show ?thesis
-    by (auto simp add: ac_simps F.simps [of k l])
+    by (auto simp: ac_simps F.simps [of k l])
 qed
 
 lemma bit_iff:
@@ -1800,7 +1796,7 @@
   fix k l :: int and m n :: nat
   show \<open>unset_bit n k = (k OR push_bit n 1) XOR push_bit n 1\<close>
     by (rule bit_eqI)
-      (auto simp add: unset_bit_int_def
+      (auto simp: unset_bit_int_def
         and_int.bit_iff or_int.bit_iff xor_int.bit_iff bit_not_int_iff push_bit_int_def bit_simps)
 qed (fact and_int.rec or_int.rec xor_int.rec mask_int_def set_bit_int_def flip_bit_int_def
   push_bit_int_def drop_bit_int_def take_bit_int_def not_int_def)+
@@ -1837,13 +1833,13 @@
     case (even k)
     then show ?case
       using bit_double_iff [of \<open>of_int k\<close> n] Bit_Operations.bit_double_iff [of k n]
-      by (cases n) (auto simp add: ac_simps possible_bit_def dest: mult_not_zero)
+      by (cases n) (auto simp: ac_simps possible_bit_def dest: mult_not_zero)
   next
     case (odd k)
     then show ?case
       using bit_double_iff [of \<open>of_int k\<close> n]
       by (cases n)
-        (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_0 Bit_Operations.bit_Suc
+        (auto simp: ac_simps bit_double_iff even_bit_succ_iff Bit_Operations.bit_0 Bit_Operations.bit_Suc
           possible_bit_def dest: mult_not_zero)
   qed
   with True show ?thesis
@@ -1953,7 +1949,7 @@
     by simp
   with and_int.rec [of \<open>1 + k * 2\<close> l]
   show ?case
-    by (auto simp add: zero_le_mult_iff not_le)
+    by (auto simp: zero_le_mult_iff not_le)
 qed
 
 lemma and_negative_int_iff [simp]:
@@ -2018,7 +2014,7 @@
 
 lemma xor_negative_int_iff [simp]:
   \<open>k XOR l < 0 \<longleftrightarrow> (k < 0) \<noteq> (l < 0)\<close> for k l :: int
-  by (subst Not_eq_iff [symmetric]) (auto simp add: not_less)
+  by (subst Not_eq_iff [symmetric]) (auto simp: not_less)
 
 lemma OR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
   \<open>x OR y < 2 ^ n\<close> if \<open>0 \<le> x\<close> \<open>x < 2 ^ n\<close> \<open>y < 2 ^ n\<close> for x y :: int
@@ -2034,12 +2030,12 @@
   case (even x)
   from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
   show ?case
-    by (cases n) (auto simp add: or_int.rec [of \<open>_ * 2\<close>] elim: oddE)
+    by (cases n) (auto simp: or_int.rec [of \<open>_ * 2\<close>] elim: oddE)
 next
   case (odd x)
   from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
   show ?case
-    by (cases n) (auto simp add: or_int.rec [of \<open>1 + _ * 2\<close>], linarith)
+    by (cases n) (auto simp: or_int.rec [of \<open>1 + _ * 2\<close>], linarith)
 qed
 
 lemma XOR_upper: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
@@ -2056,12 +2052,12 @@
   case (even x)
   from even.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] even.prems even.hyps
   show ?case
-    by (cases n) (auto simp add: xor_int.rec [of \<open>_ * 2\<close>] elim: oddE)
+    by (cases n) (auto simp: xor_int.rec [of \<open>_ * 2\<close>] elim: oddE)
 next
   case (odd x)
   from odd.IH [of \<open>n - 1\<close> \<open>y div 2\<close>] odd.prems odd.hyps
   show ?case
-    by (cases n) (auto simp add: xor_int.rec [of \<open>1 + _ * 2\<close>])
+    by (cases n) (auto simp: xor_int.rec [of \<open>1 + _ * 2\<close>])
 qed
 
 lemma AND_lower [simp]: \<^marker>\<open>contributor \<open>Stefan Berghofer\<close>\<close>
@@ -2120,12 +2116,12 @@
   case (even x)
   from even.IH [of \<open>y div 2\<close>]
   show ?case
-    by (auto simp add: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE)
+    by (auto simp: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE)
 next
   case (odd x)
   from odd.IH [of \<open>y div 2\<close>]
   show ?case
-    by (auto simp add: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE)
+    by (auto simp: and_int.rec [of _ y] or_int.rec [of _ y] elim: oddE)
 qed
 
 lemma push_bit_minus_one:
@@ -2182,7 +2178,7 @@
 
 lemma drop_bit_nonnegative_int_iff [simp]:
   \<open>drop_bit n k \<ge> 0 \<longleftrightarrow> k \<ge> 0\<close> for k :: int
-  by (induction n) (auto simp add: drop_bit_Suc drop_bit_half)
+  by (induction n) (auto simp: drop_bit_Suc drop_bit_half)
 
 lemma drop_bit_negative_int_iff [simp]:
   \<open>drop_bit n k < 0 \<longleftrightarrow> k < 0\<close> for k :: int
@@ -2223,17 +2219,17 @@
 lemma and_int_unfold:
   \<open>k AND l = (if k = 0 \<or> l = 0 then 0 else if k = - 1 then l else if l = - 1 then k
     else (k mod 2) * (l mod 2) + 2 * ((k div 2) AND (l div 2)))\<close> for k l :: int
-  by (auto simp add: and_int.rec [of k l] zmult_eq_1_iff elim: oddE)
+  by (auto simp: and_int.rec [of k l] zmult_eq_1_iff elim: oddE)
 
 lemma or_int_unfold:
   \<open>k OR l = (if k = - 1 \<or> l = - 1 then - 1 else if k = 0 then l else if l = 0 then k
     else max (k mod 2) (l mod 2) + 2 * ((k div 2) OR (l div 2)))\<close> for k l :: int
-  by (auto simp add: or_int.rec [of k l] elim: oddE)
+  by (auto simp: or_int.rec [of k l] elim: oddE)
 
 lemma xor_int_unfold:
   \<open>k XOR l = (if k = - 1 then NOT l else if l = - 1 then NOT k else if k = 0 then l else if l = 0 then k
     else \<bar>k mod 2 - l mod 2\<bar> + 2 * ((k div 2) XOR (l div 2)))\<close> for k l :: int
-  by (auto simp add: xor_int.rec [of k l] not_int_def elim!: oddE)
+  by (auto simp: xor_int.rec [of k l] not_int_def elim!: oddE)
 
 lemma bit_minus_int_iff:
   \<open>bit (- k) n \<longleftrightarrow> bit (NOT (k - 1)) n\<close> for k :: int
@@ -2325,7 +2321,7 @@
 
 lemma take_bit_int_less_self_iff:
   \<open>take_bit n k < k \<longleftrightarrow> 2 ^ n \<le> k\<close> for k :: int
-  by (auto simp add: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
+  by (auto simp: less_le take_bit_int_less_eq_self_iff take_bit_int_eq_self_iff
     intro: order_trans [of 0 \<open>2 ^ n\<close> k])
 
 lemma take_bit_int_greater_self_iff:
@@ -2334,7 +2330,7 @@
 
 lemma take_bit_int_greater_eq_self_iff:
   \<open>k \<le> take_bit n k \<longleftrightarrow> k < 2 ^ n\<close> for k :: int
-  by (auto simp add: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
+  by (auto simp: le_less take_bit_int_greater_self_iff take_bit_int_eq_self_iff
     dest: sym not_sym intro: less_trans [of k 0 \<open>2 ^ n\<close>])
 
 lemma take_bit_tightened_less_eq_int:
@@ -2370,7 +2366,7 @@
       fix m
       assume \<open>nat k \<le> m\<close>
       then show \<open>bit k m \<longleftrightarrow> bit k (nat k)\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
+        by (auto simp: * bit_iff_odd power_add zdiv_zmult2_eq dest!: le_Suc_ex)
     qed
   next
     case False
@@ -2388,7 +2384,7 @@
       fix m
       assume \<open>nat (- k) \<le> m\<close>
       then show \<open>bit k m \<longleftrightarrow> bit k (nat (- k))\<close>
-        by (auto simp add: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
+        by (auto simp: * bit_iff_odd power_add zdiv_zmult2_eq minus_1_div_exp_eq_int dest!: le_Suc_ex)
     qed
   qed
   show thesis
@@ -2408,18 +2404,12 @@
     moreover have \<open>finite N\<close> \<open>r \<in> N\<close>
       using ** N_def \<open>r < q\<close> by auto
     moreover define n where \<open>n = Suc (Max N)\<close>
-    ultimately have \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
-      apply auto
-         apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-        apply (metis "*" Max_ge Suc_n_not_le_n \<open>finite N\<close> linorder_not_less mem_Collect_eq)
-      apply (metis (full_types, lifting) "*" Max_ge_iff Suc_n_not_le_n \<open>finite N\<close> all_not_in_conv mem_Collect_eq not_le)
-      done
+    ultimately have \<dagger>: \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m \<longleftrightarrow> bit k n\<close>
+      by (smt (verit) "*" Max_ge Suc_n_not_le_n linorder_not_less mem_Collect_eq not_less_eq_eq)
     have \<open>bit k (Max N) \<noteq> bit k n\<close>
       by (metis (mono_tags, lifting) "*" Max_in N_def \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> \<open>finite N\<close> \<open>r \<in> N\<close> empty_iff le_cases mem_Collect_eq)
-    show thesis apply (rule that [of n])
-      using \<open>\<And>m. n \<le> m \<Longrightarrow> bit k m = bit k n\<close> apply blast
-      using \<open>bit k (Max N) \<noteq> bit k n\<close> n_def by auto
+    with \<dagger> n_def that [of n] show thesis
+      by fastforce
   qed
 qed
 
@@ -2591,17 +2581,17 @@
 lemma and_nat_unfold [code]:
   \<open>m AND n = (if m = 0 \<or> n = 0 then 0 else (m mod 2) * (n mod 2) + 2 * ((m div 2) AND (n div 2)))\<close>
     for m n :: nat
-  by (auto simp add: and_rec [of m n] elim: oddE)
+  by (auto simp: and_rec [of m n] elim: oddE)
 
 lemma or_nat_unfold [code]:
   \<open>m OR n = (if m = 0 then n else if n = 0 then m
     else max (m mod 2) (n mod 2) + 2 * ((m div 2) OR (n div 2)))\<close> for m n :: nat
-  by (auto simp add: or_rec [of m n] elim: oddE)
+  by (auto simp: or_rec [of m n] elim: oddE)
 
 lemma xor_nat_unfold [code]:
   \<open>m XOR n = (if m = 0 then n else if n = 0 then m
     else (m mod 2 + n mod 2) mod 2 + 2 * ((m div 2) XOR (n div 2)))\<close> for m n :: nat
-  by (auto simp add: xor_rec [of m n] elim!: oddE)
+  by (auto simp: xor_rec [of m n] elim!: oddE)
 
 lemma [code]:
   \<open>unset_bit 0 m = 2 * (m div 2)\<close>
@@ -2680,10 +2670,11 @@
 
 lemma drop_bit_nat_eq:
   \<open>drop_bit n (nat k) = nat (drop_bit n k)\<close>
-  apply (cases \<open>k \<ge> 0\<close>)
-   apply (simp_all add: drop_bit_eq_div nat_div_distrib nat_power_eq not_le)
-  apply (simp add: divide_int_def)
-  done
+proof (cases \<open>k \<ge> 0\<close>)
+  case True
+  then show ?thesis
+    by (metis drop_bit_of_nat int_nat_eq nat_int) 
+qed (simp add: nat_eq_iff2)
 
 lemma take_bit_nat_eq:
   \<open>take_bit n (nat k) = nat (take_bit n k)\<close> if \<open>k \<ge> 0\<close>
@@ -2932,7 +2923,7 @@
   \<open>numeral (Num.Bit1 m) AND NOT (1 :: int) = numeral (Num.Bit0 m)\<close>
   \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m AND NOT (numeral n))\<close>
   \<open>numeral (Num.Bit1 m) AND NOT (numeral (Num.Bit1 n)) = (2 :: int) * (numeral m AND NOT (numeral n))\<close>
-  by (simp_all add: bit_eq_iff) (auto simp add: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
+  by (simp_all add: bit_eq_iff) (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec BitM_inc_eq sub_inc_One_eq split: nat.split)
 
 fun and_not_num :: \<open>num \<Rightarrow> num \<Rightarrow> num option\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
 where
@@ -2989,7 +2980,7 @@
   \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit0 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
   \<open>numeral (Num.Bit1 m) OR NOT (numeral (Num.Bit1 n)) = 1 + (2 :: int) * (numeral m OR NOT (numeral n))\<close>
   by (simp_all add: bit_eq_iff)
-    (auto simp add: bit_0 bit_simps bit_Suc bit_numeral_rec sub_inc_One_eq split: nat.split)
+    (auto simp: bit_0 bit_simps bit_Suc bit_numeral_rec sub_inc_One_eq split: nat.split)
 
 fun or_not_num_neg :: \<open>num \<Rightarrow> num \<Rightarrow> num\<close> \<^marker>\<open>contributor \<open>Andreas Lochbihler\<close>\<close>
 where
@@ -3055,7 +3046,7 @@
     (case take_bit_num (pred_numeral r) m of None \<Rightarrow> None | Some q \<Rightarrow> Some (Num.Bit0 q))\<close>
   \<open>take_bit_num (numeral r) (Num.Bit1 m) =
     Some (case take_bit_num (pred_numeral r) m of None \<Rightarrow> Num.One | Some q \<Rightarrow> Num.Bit1 q)\<close>
-  by (auto simp add: take_bit_num_def ac_simps mult_2 num_of_nat_double
+  by (auto simp: take_bit_num_def ac_simps mult_2 num_of_nat_double
     take_bit_Suc_bit0 take_bit_Suc_bit1 take_bit_numeral_bit0 take_bit_numeral_bit1)
 
 lemma take_bit_num_code [code]:
@@ -3085,7 +3076,7 @@
   \<open>take_bit m (numeral n) = numeral q\<close> if \<open>take_bit_num m n = Some q\<close>
 proof -
   from that have \<open>take_bit m (numeral n :: nat) = numeral q\<close>
-    by (auto simp add: take_bit_num_def Num.numeral_num_of_nat_unfold split: if_splits)
+    by (auto simp: take_bit_num_def Num.numeral_num_of_nat_unfold split: if_splits)
   then have \<open>of_nat (take_bit m (numeral n)) = of_nat (numeral q)\<close>
     by simp
   then show ?thesis
@@ -3193,7 +3184,7 @@
   \<open>Int.Neg num.One AND Int.Pos m = Int.Pos m\<close>
   \<open>Int.Neg (num.Bit0 n) AND Int.Pos m = Num.sub (or_not_num_neg (Num.BitM n) m) num.One\<close>
   \<open>Int.Neg (num.Bit1 n) AND Int.Pos m = Num.sub (or_not_num_neg (num.Bit0 n) m) num.One\<close>
-  apply (auto simp add: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int]
+  apply (auto simp: and_num_eq_None_iff [where ?'a = int] and_num_eq_Some_iff [where ?'a = int]
     split: option.split)
      apply (simp_all only: sub_one_eq_not_neg numeral_or_not_num_eq minus_minus and_not_numerals
        bit.de_Morgan_disj bit.double_compl and_not_num_eq_None_iff and_not_num_eq_Some_iff ac_simps)
@@ -3236,7 +3227,7 @@
   \<open>Int.Neg num.One OR Int.Pos m = Int.Neg num.One\<close>
   \<open>Int.Neg (num.Bit0 n) OR Int.Pos m = (case and_not_num (Num.BitM n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
   \<open>Int.Neg (num.Bit1 n) OR Int.Pos m = (case and_not_num (num.Bit0 n) m of None \<Rightarrow> -1 | Some n' \<Rightarrow> Int.Neg (Num.inc n'))\<close>
-  apply (auto simp add: numeral_or_num_eq split: option.splits)
+  apply (auto simp: numeral_or_num_eq split: option.splits)
          apply (simp_all only: and_not_num_eq_None_iff and_not_num_eq_Some_iff and_not_numerals
            numeral_or_not_num_eq or_eq_not_not_and bit.double_compl ac_simps flip: numeral_eq_iff [where ?'a = int])
          apply simp_all
@@ -3372,11 +3363,11 @@
 
 lemma concat_bit_assoc:
   \<open>concat_bit n k (concat_bit m l r) = concat_bit (m + n) (concat_bit n k l) r\<close>
-  by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps)
+  by (rule bit_eqI) (auto simp: bit_concat_bit_iff ac_simps)
 
 lemma concat_bit_assoc_sym:
   \<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close>
-  by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def)
+  by (rule bit_eqI) (auto simp: bit_concat_bit_iff ac_simps min_def)
 
 lemma concat_bit_eq_iff:
   \<open>concat_bit n k l = concat_bit n r s
@@ -3394,14 +3385,14 @@
     fix m
     from * [of m]
     show \<open>bit (take_bit n k) m \<longleftrightarrow> bit (take_bit n r) m\<close>
-      by (auto simp add: bit_take_bit_iff bit_concat_bit_iff)
+      by (auto simp: bit_take_bit_iff bit_concat_bit_iff)
   qed
   moreover have \<open>push_bit n l = push_bit n s\<close>
   proof (rule bit_eqI)
     fix m
     from * [of m]
     show \<open>bit (push_bit n l) m \<longleftrightarrow> bit (push_bit n s) m\<close>
-      by (auto simp add: bit_push_bit_iff bit_concat_bit_iff)
+      by (auto simp: bit_push_bit_iff bit_concat_bit_iff)
   qed
   then have \<open>l = s\<close>
     by (simp add: push_bit_eq_mult)
@@ -3412,7 +3403,7 @@
 lemma take_bit_concat_bit_eq:
   \<open>take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\<close>
   by (rule bit_eqI)
-    (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def)
+    (auto simp: bit_take_bit_iff bit_concat_bit_iff min_def)
 
 lemma concat_bit_take_bit_eq:
   \<open>concat_bit n (take_bit n b) = concat_bit n b\<close>
@@ -3437,7 +3428,7 @@
 
 lemma even_signed_take_bit_iff:
   \<open>even (signed_take_bit m a) \<longleftrightarrow> even a\<close>
-  by (auto simp add: bit_0 signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
+  by (auto simp: bit_0 signed_take_bit_def even_or_iff even_mask_iff bit_double_iff)
 
 lemma bit_signed_take_bit_iff [bit_simps]:
   \<open>bit (signed_take_bit m a) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit a (min m n)\<close>
@@ -3479,21 +3470,21 @@
     by (simp add: fun_eq_iff bit_signed_take_bit_iff bit_take_bit_iff not_le less_Suc_eq_le min_def)
       (use bit_imp_possible_bit in fastforce)
   then show ?thesis
-    by (auto simp add: fun_eq_iff intro: bit_eqI)
+    by (auto simp: fun_eq_iff intro: bit_eqI)
 qed
 
 lemma signed_take_bit_signed_take_bit [simp]:
   \<open>signed_take_bit m (signed_take_bit n a) = signed_take_bit (min m n) a\<close>
-  by (auto simp add: bit_eq_iff bit_simps ac_simps)
+  by (auto simp: bit_eq_iff bit_simps ac_simps)
 
 lemma signed_take_bit_take_bit:
   \<open>signed_take_bit m (take_bit n a) = (if n \<le> m then take_bit n else signed_take_bit m) a\<close>
-  by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff)
+  by (rule bit_eqI) (auto simp: bit_signed_take_bit_iff min_def bit_take_bit_iff)
 
 lemma take_bit_signed_take_bit:
   \<open>take_bit m (signed_take_bit n a) = take_bit m a\<close> if \<open>m \<le> Suc n\<close>
   using that by (rule le_SucE; intro bit_eqI)
-   (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
+   (auto simp: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq)
 
 lemma signed_take_bit_eq_take_bit_add:
   \<open>signed_take_bit n k = take_bit (Suc n) k + NOT (mask (Suc n)) * of_bool (bit k n)\<close>
@@ -3504,7 +3495,7 @@
 next
   case True
   have \<open>signed_take_bit n k = take_bit (Suc n) k OR NOT (mask (Suc n))\<close>
-    by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
+    by (rule bit_eqI) (auto simp: bit_signed_take_bit_iff min_def bit_take_bit_iff bit_or_iff bit_not_iff bit_mask_iff less_Suc_eq True)
   also have \<open>\<dots> = take_bit (Suc n) k + NOT (mask (Suc n))\<close>
     by (simp add: disjunctive_add_eq_or bit_eq_iff bit_simps)
   finally show ?thesis
@@ -3623,7 +3614,7 @@
 lemma signed_take_bit_int_eq_self_iff:
   \<open>signed_take_bit n k = k \<longleftrightarrow> - (2 ^ n) \<le> k \<and> k < 2 ^ n\<close>
   for k :: int
-  by (auto simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
+  by (auto simp: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self_iff algebra_simps)
 
 lemma signed_take_bit_int_eq_self:
   \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close>
@@ -3782,9 +3773,8 @@
 
 lemma exp_div_exp_eq:
   \<open>2 ^ m div 2 ^ n = of_bool (2 ^ m \<noteq> 0 \<and> m \<ge> n) * 2 ^ (m - n)\<close>
-  apply (rule bit_eqI)
-  using bit_exp_iff div_exp_eq apply (auto simp add: bit_iff_odd possible_bit_def)
-  done
+  using bit_exp_iff div_exp_eq
+  by (intro bit_eqI) (auto simp: bit_iff_odd possible_bit_def)
 
 lemma bits_1_div_2:
   \<open>1 div 2 = 0\<close>
@@ -3855,11 +3845,11 @@
   with that show ?thesis proof (induction n arbitrary: a b)
     case 0
     from "0.prems"(1) [of 0] show ?case
-      by (auto simp add: bit_0)
+      by (auto simp: bit_0)
   next
     case (Suc n)
     from Suc.prems(1) [of 0] have even: \<open>even a \<or> even b\<close>
-      by (auto simp add: bit_0)
+      by (auto simp: bit_0)
     have bit: \<open>\<not> bit (a div 2) n \<or> \<not> bit (b div 2) n\<close> for n
       using Suc.prems(1) [of \<open>Suc n\<close>] by (simp add: bit_Suc)
     from Suc.prems(2) have \<open>possible_bit TYPE('a) (Suc n)\<close> \<open>possible_bit TYPE('a) n\<close>
@@ -3867,7 +3857,7 @@
     have \<open>a + b = (a div 2 * 2 + a mod 2) + (b div 2 * 2 + b mod 2)\<close>
       using div_mult_mod_eq [of a 2] div_mult_mod_eq [of b 2] by simp
     also have \<open>\<dots> = of_bool (odd a \<or> odd b) + 2 * (a div 2 + b div 2)\<close>
-      using even by (auto simp add: algebra_simps mod2_eq_if)
+      using even by (auto simp: algebra_simps mod2_eq_if)
     finally have \<open>bit ((a + b) div 2) n \<longleftrightarrow> bit (a div 2 + b div 2) n\<close>
       using \<open>possible_bit TYPE('a) (Suc n)\<close> by simp (simp_all flip: bit_Suc add: bit_double_iff possible_bit_def)
     also have \<open>\<dots> \<longleftrightarrow> bit (a div 2) n \<or> bit (b div 2) n\<close>
@@ -3884,7 +3874,7 @@
 
 lemma even_mask_div_iff:
   \<open>even ((2 ^ m - 1) div 2 ^ n) \<longleftrightarrow> 2 ^ n = 0 \<or> m \<le> n\<close>
-  using bit_mask_iff [of m n] by (auto simp add: mask_eq_exp_minus_1 bit_iff_odd possible_bit_def)
+  using bit_mask_iff [of m n] by (auto simp: mask_eq_exp_minus_1 bit_iff_odd possible_bit_def)
 
 lemma mod_exp_eq:
   \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
@@ -3920,7 +3910,7 @@
 
 lemma even_mod_exp_div_exp_iff:
   \<open>even (a mod 2 ^ m div 2 ^ n) \<longleftrightarrow> m \<le> n \<or> even (a div 2 ^ n)\<close>
-  by (auto simp add: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
+  by (auto simp: even_drop_bit_iff_not_bit bit_simps simp flip: drop_bit_eq_div take_bit_eq_mod)
 
 end
 
@@ -3931,7 +3921,7 @@
   \<open>a - b = a AND NOT b\<close> if \<open>\<And>n. bit b n \<Longrightarrow> bit a n\<close>
 proof -
   have \<open>NOT a + b = NOT a OR b\<close>
-    by (rule disjunctive_add) (auto simp add: bit_not_iff dest: that)
+    by (rule disjunctive_add) (auto simp: bit_not_iff dest: that)
   then have \<open>NOT (NOT a + b) = NOT (NOT a OR b)\<close>
     by simp
   then show ?thesis
diff -r 32f0e953cc96 -r 8f96e1329845 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Aug 24 14:14:57 2024 +0100
+++ b/src/HOL/List.thy	Sat Aug 24 23:44:05 2024 +0100
@@ -3359,12 +3359,7 @@
 lemma nth_take_lemma:
   "k \<le> length xs \<Longrightarrow> k \<le> length ys \<Longrightarrow>
      (\<And>i. i < k \<longrightarrow> xs!i = ys!i) \<Longrightarrow> take k xs = take k ys"
-proof (induct k arbitrary: xs ys)
-  case (Suc k)
-  then show ?case
-    apply (simp add: less_Suc_eq_0_disj)
-    by (simp add: Suc.prems(3) take_Suc_conv_app_nth)
-qed simp
+  by (induct k arbitrary: xs ys) (simp_all add: take_Suc_conv_app_nth)
 
 lemma nth_equalityI:
   "\<lbrakk>length xs = length ys; \<And>i. i < length xs \<Longrightarrow> xs!i = ys!i\<rbrakk> \<Longrightarrow> xs = ys"
@@ -3712,7 +3707,7 @@
 
 lemma nth_eq_iff_index_eq:
   "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
-by(auto simp: distinct_conv_nth)
+  by(auto simp: distinct_conv_nth)
 
 lemma distinct_Ex1:
   "distinct xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> (\<exists>!i. i < length xs \<and> xs ! i = x)"
@@ -3733,9 +3728,7 @@
 
 lemma distinct_swap[simp]: "\<lbrakk> i < size xs; j < size xs\<rbrakk> \<Longrightarrow>
   distinct(xs[i := xs!j, j := xs!i]) = distinct xs"
-  apply (simp add: distinct_conv_nth nth_list_update)
-  apply (safe; metis)
-  done
+  by (smt (verit, del_insts) distinct_conv_nth length_list_update nth_list_update)
 
 lemma set_swap[simp]:
   "\<lbrakk> i < size xs; j < size xs \<rbrakk> \<Longrightarrow> set(xs[i := xs!j, j := xs!i]) = set xs"
@@ -4320,7 +4313,7 @@
 next
   case (Cons x xs) thus ?case
     apply(auto simp: nth_Cons' split: if_splits)
-    using diff_Suc_1[unfolded One_nat_def] less_Suc_eq_0_disj by fastforce
+    using diff_Suc_1 less_Suc_eq_0_disj by fastforce
 qed
 
 lemmas find_Some_iff2 = find_Some_iff[THEN eq_iff_swap]
@@ -4514,9 +4507,16 @@
   distinct (removeAll [] xs) \<and>
   (\<forall>ys. ys \<in> set xs \<longrightarrow> distinct ys) \<and>
   (\<forall>ys zs. ys \<in> set xs \<and> zs \<in> set xs \<and> ys \<noteq> zs \<longrightarrow> set ys \<inter> set zs = {})"
-apply (induct xs)
- apply(simp_all, safe, auto)
-by (metis Int_iff UN_I empty_iff equals0I set_empty)
+proof (induct xs)
+  case Nil
+  then show ?case by auto
+next
+  case (Cons a xs)
+  have "\<lbrakk>set a \<inter> \<Union> (set ` set xs) = {}; a \<in> set xs\<rbrakk> \<Longrightarrow> a=[]"
+    by (metis Int_iff UN_I empty_iff equals0I set_empty)
+  then show ?case
+    by (auto simp: Cons)
+qed
 
 
 subsubsection \<open>\<^const>\<open>replicate\<close>\<close>
@@ -4535,24 +4535,24 @@
 qed
 
 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
-by (rule exI[of _ "replicate n undefined"]) simp
+  by (rule exI[of _ "replicate n undefined"]) simp
 
 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
-by (induct n) auto
+  by (induct n) auto
 
 lemma map_replicate_const:
   "map (\<lambda> x. k) lst = replicate (length lst) k"
-by (induct lst) auto
+  by (induct lst) auto
 
 lemma replicate_app_Cons_same:
-"(replicate n x) @ (x # xs) = x # replicate n x @ xs"
-by (induct n) auto
+  "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
+  by (induct n) auto
 
 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
-by (induct n) (auto simp: replicate_app_Cons_same)
+  by (metis length_rev map_replicate map_replicate_const rev_map)
 
 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
-by (induct n) auto
+  by (induct n) auto
 
 text\<open>Courtesy of Matthias Daum:\<close>
 lemma append_replicate_commute:
@@ -4899,10 +4899,7 @@
 
 lemma nth_rotate:
   \<open>rotate m xs ! n = xs ! ((m + n) mod length xs)\<close> if \<open>n < length xs\<close>
-  using that apply (auto simp add: rotate_drop_take nth_append not_less less_diff_conv ac_simps dest!: le_Suc_ex)
-   apply (metis add.commute mod_add_right_eq mod_less)
-  apply (metis (no_types, lifting) Nat.diff_diff_right add.commute add_diff_cancel_right' diff_le_self dual_order.strict_trans2 length_greater_0_conv less_nat_zero_code list.size(3) mod_add_right_eq mod_add_self2 mod_le_divisor mod_less)
-  done
+  by (smt (verit) add.commute hd_rotate_conv_nth length_rotate not_less0 list.size(3) mod_less rotate_rotate that)
 
 lemma nth_rotate1:
   \<open>rotate1 xs ! n = xs ! (Suc n mod length xs)\<close> if \<open>n < length xs\<close>
@@ -4944,10 +4941,8 @@
   by (auto simp add: nths_def)
 
 lemma nths_all: "\<forall>i < length xs. i \<in> I \<Longrightarrow> nths xs I = xs"
-apply (simp add: nths_def)
-apply (subst filter_True)
- apply (auto simp: in_set_zip subset_iff)
-done
+  unfolding nths_def
+  by (metis add_0 diff_zero filter_True in_set_zip length_upt nth_upt zip_eq_conv)
 
 lemma length_nths:
   "length (nths xs I) = card{i. i < length xs \<and> i \<in> I}"
@@ -5343,8 +5338,7 @@
 
     show ?thesis
       unfolding transpose.simps \<open>i = Suc j\<close> nth_Cons_Suc "3.hyps"[OF j_less]
-      apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
-      by (simp add: nth_tl)
+      by (auto simp: nth_tl transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
   qed
 qed simp_all
 
@@ -6644,14 +6638,9 @@
   have "(xs,ys) \<in> ?L (Suc n)" if r: "(xs,ys) \<in> ?R (Suc n)" for xs ys
   proof -
     from r obtain xys where r': "?len (Suc n) xs" "?len (Suc n) ys" "?P xs ys xys" by auto
-    then show ?thesis
-    proof (cases xys)
-      case Nil
-      thus ?thesis using r' by (auto simp: image_Collect lex_prod_def)
-    next
-      case Cons
-      thus ?thesis using r' Suc by (fastforce simp: image_Collect lex_prod_def)
-    qed
+    then show ?thesis 
+      using r' Suc
+      by (cases xys; fastforce simp: image_Collect lex_prod_def)
   qed
   moreover have "(xs,ys) \<in> ?L (Suc n) \<Longrightarrow> (xs,ys) \<in> ?R (Suc n)" for xs ys
     using Suc by (auto simp add: image_Collect lex_prod_def)(blast, meson Cons_eq_appendI)
@@ -6867,25 +6856,25 @@
 
 lemma lexord_same_pref_iff:
   "(xs @ ys, xs @ zs) \<in> lexord r \<longleftrightarrow> (\<exists>x \<in> set xs. (x,x) \<in> r) \<or> (ys, zs) \<in> lexord r"
-by(induction xs) auto
+  by(induction xs) auto
 
 lemma lexord_same_pref_if_irrefl[simp]:
   "irrefl r \<Longrightarrow> (xs @ ys, xs @ zs) \<in> lexord r \<longleftrightarrow> (ys, zs) \<in> lexord r"
-by (simp add: irrefl_def lexord_same_pref_iff)
+  by (simp add: irrefl_def lexord_same_pref_iff)
 
 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
-by (metis append_Nil2 lexord_Nil_left lexord_same_pref_iff)
+  by (metis append_Nil2 lexord_Nil_left lexord_same_pref_iff)
 
 lemma lexord_append_left_rightI:
   "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+  by (simp add: lexord_same_pref_iff)
 
 lemma lexord_append_leftI: "(u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+  by (simp add: lexord_same_pref_iff)
 
 lemma lexord_append_leftD:
   "\<lbrakk>(x @ u, x @ v) \<in> lexord r; (\<forall>a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
-by (simp add: lexord_same_pref_iff)
+  by (simp add: lexord_same_pref_iff)
 
 lemma lexord_take_index_conv:
    "((x,y) \<in> lexord r) =
@@ -6897,9 +6886,13 @@
   moreover
   have "(\<exists>u a b. (a, b) \<in> r \<and> (\<exists>v. x = u @ a # v) \<and> (\<exists>w. y = u @ b # w)) =
         (\<exists>i<length x. i < length y \<and> take i x = take i y \<and> (x ! i, y ! i) \<in> r)"
-    apply safe
-    using less_iff_Suc_add apply auto[1]
-    by (metis id_take_nth_drop)
+        (is "?L=?R")
+  proof
+    show "?L\<Longrightarrow>?R"
+      by (metis append_eq_conv_conj drop_all leI list.simps(3) nth_append_length)
+    show "?R\<Longrightarrow>?L"
+      by (metis id_take_nth_drop)
+  qed
   ultimately show ?thesis
     by (auto simp: lexord_def Let_def)
 qed
@@ -7118,19 +7111,19 @@
 by(subst lexordp_eq.simps, fastforce)+
 
 lemma lexordp_append_rightI: "ys \<noteq> Nil \<Longrightarrow> lexordp xs (xs @ ys)"
-by(induct xs)(auto simp add: neq_Nil_conv)
+  by(induct xs)(auto simp add: neq_Nil_conv)
 
 lemma lexordp_append_left_rightI: "x < y \<Longrightarrow> lexordp (us @ x # xs) (us @ y # ys)"
-by(induct us) auto
+  by(induct us) auto
 
 lemma lexordp_eq_refl: "lexordp_eq xs xs"
-by(induct xs) simp_all
+  by(induct xs) simp_all
 
 lemma lexordp_append_leftI: "lexordp us vs \<Longrightarrow> lexordp (xs @ us) (xs @ vs)"
-by(induct xs) auto
+  by(induct xs) auto
 
 lemma lexordp_append_leftD: "\<lbrakk> lexordp (xs @ us) (xs @ vs); \<forall>a. \<not> a < a \<rbrakk> \<Longrightarrow> lexordp us vs"
-by(induct xs) auto
+  by(induct xs) auto
 
 lemma lexordp_irreflexive:
   assumes irrefl: "\<forall>x. \<not> x < x"
@@ -7251,21 +7244,21 @@
 definition "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
 
 lemma wf_measures[simp]: "wf (measures fs)"
-unfolding measures_def
-by blast
+  unfolding measures_def
+  by blast
 
 lemma in_measures[simp]:
   "(x, y) \<in> measures [] = False"
   "(x, y) \<in> measures (f # fs)
          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"
-unfolding measures_def
-by auto
+  unfolding measures_def
+  by auto
 
 lemma measures_less: "f x < f y \<Longrightarrow> (x, y) \<in> measures (f#fs)"
-by simp
+  by simp
 
 lemma measures_lesseq: "f x \<le> f y \<Longrightarrow> (x, y) \<in> measures fs \<Longrightarrow> (x, y) \<in> measures (f#fs)"
-by auto
+  by auto
 
 
 subsubsection \<open>Lifting Relations to Lists: one element\<close>
@@ -7286,27 +7279,27 @@
 unfolding listrel1_def by auto
 
 lemma not_Nil_listrel1 [iff]: "([], xs) \<notin> listrel1 r"
-unfolding listrel1_def by blast
+  unfolding listrel1_def by blast
 
 lemma not_listrel1_Nil [iff]: "(xs, []) \<notin> listrel1 r"
-unfolding listrel1_def by blast
+  unfolding listrel1_def by blast
 
 lemma Cons_listrel1_Cons [iff]:
   "(x # xs, y # ys) \<in> listrel1 r \<longleftrightarrow>
    (x,y) \<in> r \<and> xs = ys \<or> x = y \<and> (xs, ys) \<in> listrel1 r"
-by (simp add: listrel1_def Cons_eq_append_conv) (blast)
+  by (simp add: listrel1_def Cons_eq_append_conv) (blast)
 
 lemma listrel1I1: "(x,y) \<in> r \<Longrightarrow> (x # xs, y # xs) \<in> listrel1 r"
-by fast
+  by fast
 
 lemma listrel1I2: "(xs, ys) \<in> listrel1 r \<Longrightarrow> (x # xs, x # ys) \<in> listrel1 r"
-by fast
+  by fast
 
 lemma append_listrel1I:
   "(xs, ys) \<in> listrel1 r \<and> us = vs \<or> xs = ys \<and> (us, vs) \<in> listrel1 r
     \<Longrightarrow> (xs @ us, ys @ vs) \<in> listrel1 r"
-unfolding listrel1_def
-by auto (blast intro: append_eq_appendI)+
+  unfolding listrel1_def
+  by auto (blast intro: append_eq_appendI)+
 
 lemma Cons_listrel1E1[elim!]:
   assumes "(x # xs, ys) \<in> listrel1 r"
@@ -7333,19 +7326,19 @@
 qed
 
 lemma listrel1_eq_len: "(xs,ys) \<in> listrel1 r \<Longrightarrow> length xs = length ys"
-unfolding listrel1_def by auto
+  unfolding listrel1_def by auto
 
 lemma listrel1_mono:
   "r \<subseteq> s \<Longrightarrow> listrel1 r \<subseteq> listrel1 s"
-unfolding listrel1_def by blast
+  unfolding listrel1_def by blast
 
 
 lemma listrel1_converse: "listrel1 (r\<inverse>) = (listrel1 r)\<inverse>"
-unfolding listrel1_def by blast
+  unfolding listrel1_def by blast
 
 lemma in_listrel1_converse:
   "(x,y) \<in> listrel1 (r\<inverse>) \<longleftrightarrow> (x,y) \<in> (listrel1 r)\<inverse>"
-unfolding listrel1_def by blast
+  unfolding listrel1_def by blast
 
 lemma listrel1_iff_update:
   "(xs,ys) \<in> (listrel1 r)
@@ -7618,19 +7611,19 @@
 stack overflow in some target languages.\<close>
 
 fun map_tailrec_rev ::  "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'b list" where
-"map_tailrec_rev f [] bs = bs" |
-"map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)"
+  "map_tailrec_rev f [] bs = bs" |
+  "map_tailrec_rev f (a#as) bs = map_tailrec_rev f as (f a # bs)"
 
 lemma map_tailrec_rev:
   "map_tailrec_rev f as bs = rev(map f as) @ bs"
-by(induction as arbitrary: bs) simp_all
+  by(induction as arbitrary: bs) simp_all
 
 definition map_tailrec :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
-"map_tailrec f as = rev (map_tailrec_rev f as [])"
+  "map_tailrec f as = rev (map_tailrec_rev f as [])"
 
 text\<open>Code equation:\<close>
 lemma map_eq_map_tailrec: "map = map_tailrec"
-by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev)
+  by(simp add: fun_eq_iff map_tailrec_def map_tailrec_rev)
 
 
 subsubsection \<open>Counterparts for set-related operations\<close>
@@ -8375,7 +8368,7 @@
 
 lemma list_all_transfer [transfer_rule]:
   "((A ===> (=)) ===> list_all2 A ===> (=)) list_all list_all"
-  unfolding list_all_iff [abs_def] by transfer_prover
+  using list.pred_transfer by blast
 
 lemma list_ex_transfer [transfer_rule]:
   "((A ===> (=)) ===> list_all2 A ===> (=)) list_ex list_ex"