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"