# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1724705975 -3600
# Node ID 623d46973cbe32b60af6c0b78d06e96d1489db36
# Parent  fe7ffe7eb265777f2c3a34dacd0a3ad016158530
More tidying of old proofs

diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/Combinatorics/Permutations.thy
--- a/src/HOL/Combinatorics/Permutations.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Combinatorics/Permutations.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -377,13 +377,10 @@
 lemma permutes_insert_lemma:
   assumes "p permutes (insert a S)"
   shows "transpose a (p a) \<circ> p permutes S"
-  apply (rule permutes_superset[where S = "insert a S"])
-  apply (rule permutes_compose[OF assms])
-  apply (rule permutes_swap_id, simp)
-  using permutes_in_image[OF assms, of a]
-  apply simp
-  apply (auto simp add: Ball_def)
-  done
+proof (rule permutes_superset[where S = "insert a S"])
+  show "Transposition.transpose a (p a) \<circ> p permutes insert a S"
+    by (meson assms insertI1 permutes_compose permutes_in_image permutes_swap_id)
+qed auto
 
 lemma permutes_insert: "{p. p permutes (insert a S)} =
   (\<lambda>(b, p). transpose a b \<circ> p) ` {(b, p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
@@ -444,11 +441,7 @@
     then have "finite ?pF"
       by (auto intro: card_ge_0_finite)
     with \<open>finite F\<close> card.insert_remove have pF'f: "finite ?pF'"
-      apply (simp only: Collect_case_prod Collect_mem_eq)
-      apply (rule finite_cartesian_product)
-      apply simp_all
-      done
-
+      by simp
     have ginj: "inj_on ?g ?pF'"
     proof -
       {
@@ -593,21 +586,10 @@
 declare permutation_id[unfolded id_def, simp]
 
 lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (transpose a b)"
-  apply clarsimp
-  using comp_Suc[of 0 id a b]
-  apply simp
-  done
+  using swapidseq.simps by fastforce
 
 lemma permutation_swap_id: "permutation (transpose a b)"
-proof (cases "a = b")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then show ?thesis
-    unfolding permutation_def
-    using swapidseq_swap[of a b] by blast
-qed
+  by (meson permutation_def swapidseq_swap)
 
 
 lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)"
@@ -616,14 +598,8 @@
   then show ?case by simp
 next
   case (comp_Suc n p a b m q)
-  have eq: "Suc n + m = Suc (n + m)"
-    by arith
-  show ?case
-    apply (simp only: eq comp_assoc)
-    apply (rule swapidseq.comp_Suc)
-    using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3)
-     apply blast+
-    done
+  then show ?case
+    by (metis add_Suc comp_assoc swapidseq.comp_Suc)
 qed
 
 lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
@@ -696,40 +672,19 @@
   shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>  P a b c d"
   using assms by metis
 
-lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
-  transpose a b \<circ> transpose c d = id \<or>
+lemma swap_general:
+  assumes "a \<noteq> b" "c \<noteq> d"
+  shows "transpose a b \<circ> transpose c d = id \<or>
   (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
     transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z)"
-proof -
-  assume neq: "a \<noteq> b" "c \<noteq> d"
-  have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
-    (transpose a b \<circ> transpose c d = id \<or>
-      (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
-        transpose a b \<circ> transpose c d = transpose x y \<circ> transpose a z))"
-    apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
-     apply (simp_all only: ac_simps)
-    apply (metis id_comp swap_id_common swap_id_common' swap_id_independent transpose_comp_involutory)
-    done
-  with neq show ?thesis by metis
-qed
+  by (metis assms swap_id_common' swap_id_independent transpose_commute transpose_comp_involutory)
 
 lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
   using swapidseq.cases[of 0 p "p = id"] by auto
 
 lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
     n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = transpose a b \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
-  apply (rule iffI)
-   apply (erule swapidseq.cases[of n p])
-    apply simp
-   apply (rule disjI2)
-   apply (rule_tac x= "a" in exI)
-   apply (rule_tac x= "b" in exI)
-   apply (rule_tac x= "pa" in exI)
-   apply (rule_tac x= "na" in exI)
-   apply simp
-  apply auto
-  apply (rule comp_Suc, simp_all)
-  done
+  by (meson comp_Suc id swapidseq.cases)
 
 lemma fixing_swapidseq_decrease:
   assumes "swapidseq n p"
@@ -757,33 +712,21 @@
     then show ?thesis
       by (simp only: cdqm o_assoc) (simp add: cdqm)
   next
-    case prems: 2
+    case 2
     then have az: "a \<noteq> z"
       by simp
-    from prems have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h
+    from 2 have *: "(transpose x y \<circ> h) a = a \<longleftrightarrow> h a = a" for h
       by (simp add: transpose_def)
     from cdqm(2) have "transpose a b \<circ> p = transpose a b \<circ> (transpose c d \<circ> q)"
       by simp
-    then have "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)"
-      by (simp add: o_assoc prems)
-    then have "(transpose a b \<circ> p) a = (transpose x y \<circ> (transpose a z \<circ> q)) a"
-      by simp
-    then have "(transpose x y \<circ> (transpose a z \<circ> q)) a = a"
-      unfolding Suc by metis
-    then have "(transpose a z \<circ> q) a = a"
-      by (simp only: *)
-    from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az this]
-    have **: "swapidseq (n - 1) (transpose a z \<circ> q)" "n \<noteq> 0"
-      by blast+
-    from \<open>n \<noteq> 0\<close> have ***: "Suc n - 1 = Suc (n - 1)"
+    then have \<section>: "transpose a b \<circ> p = transpose x y \<circ> (transpose a z \<circ> q)"
+      by (simp add: o_assoc 2)
+    obtain **: "swapidseq (n - 1) (transpose a z \<circ> q)" and "n\<noteq>0"
+      by (metis "*" "\<section>" Suc.hyps Suc.prems(3) az cdqm(3,5))
+    then have "Suc n - 1 = Suc (n - 1)"
       by auto
-    show ?thesis
-      apply (simp only: cdqm(2) prems o_assoc ***)
-      apply (simp only: Suc_not_Zero simp_thms comp_assoc)
-      apply (rule comp_Suc)
-      using ** prems
-       apply blast+
-      done
+    with 2 show ?thesis
+      using "**" \<section> swapidseq.simps by blast
   qed
 qed
 
@@ -829,15 +772,9 @@
 qed
 
 lemma evenperm_unique:
-  assumes p: "swapidseq n p"
-    and n:"even n = b"
+  assumes "swapidseq n p" and"even n = b"
   shows "evenperm p = b"
-  unfolding n[symmetric] evenperm_def
-  apply (rule swapidseq_even_even[where p = p])
-   apply (rule someI[where x = n])
-  using p
-   apply blast+
-  done
+  by (metis evenperm_def assms someI swapidseq_even_even)
 
 
 subsection \<open>And it has the expected composition properties\<close>
@@ -881,17 +818,7 @@
 lemma permutation_bijective:
   assumes "permutation p"
   shows "bij p"
-proof -
-  from assms obtain n where n: "swapidseq n p"
-    unfolding permutation_def by blast
-  from swapidseq_inverse_exists[OF n] obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
-    by blast
-  then show ?thesis
-    unfolding bij_iff
-    apply (auto simp add: fun_eq_iff)
-    apply metis
-    done
-qed
+  by (meson assms o_bij permutation_def swapidseq_inverse_exists)
 
 lemma permutation_finite_support:
   assumes "permutation p"
@@ -944,17 +871,7 @@
 qed
 
 lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
-  (is "?lhs \<longleftrightarrow> ?b \<and> ?f")
-proof
-  assume ?lhs
-  with permutation_bijective permutation_finite_support show "?b \<and> ?f"
-    by auto
-next
-  assume "?b \<and> ?f"
-  then have "?f" "?b" by blast+
-  from permutation_lemma[OF this] show ?lhs
-    by blast
-qed
+  using permutation_bijective permutation_finite_support permutation_lemma by auto
 
 lemma permutation_inverse_works:
   assumes "permutation p"
@@ -966,22 +883,7 @@
   assumes p: "permutation p"
     and q: "permutation q"
   shows "inv (p \<circ> q) = inv q \<circ> inv p"
-proof -
-  note ps = permutation_inverse_works[OF p]
-  note qs = permutation_inverse_works[OF q]
-  have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p"
-    by (simp add: o_assoc)
-  also have "\<dots> = id"
-    by (simp add: ps qs)
-  finally have *: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" .
-  have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q"
-    by (simp add: o_assoc)
-  also have "\<dots> = id"
-    by (simp add: ps qs)
-  finally have **: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" .
-  show ?thesis
-    by (rule inv_unique_comp[OF * **])
-qed
+  by (simp add: o_inv_distrib p permutation_bijective q)
 
 
 subsection \<open>Relation to \<open>permutes\<close>\<close>
@@ -1365,44 +1267,28 @@
   from permutes_natset_le[OF permutes_inv[OF p] this] have "inv p = inv id"
     by simp
   then show ?thesis
-    apply (subst permutes_inv_inv[OF p, symmetric])
-    apply (rule inv_unique_comp)
-     apply simp_all
-    done
+    using p permutes_inv_inv by fastforce
 qed
 
 lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
-  apply (rule set_eqI)
-  apply auto
-  using permutes_inv_inv permutes_inv
-   apply auto
-  apply (rule_tac x="inv x" in exI)
-  apply auto
-  done
+  using permutes_inv permutes_inv_inv by force
 
 lemma image_compose_permutations_left:
   assumes "q permutes S"
   shows "{q \<circ> p |p. p permutes S} = {p. p permutes S}"
-  apply (rule set_eqI)
-  apply auto
-   apply (rule permutes_compose)
-  using assms
-    apply auto
-  apply (rule_tac x = "inv q \<circ> x" in exI)
-  apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
-  done
+proof -
+  have "\<And>p. p permutes S \<Longrightarrow> q \<circ> p permutes S"
+    by (simp add: assms permutes_compose)
+  moreover have "\<And>x. x permutes S \<Longrightarrow> \<exists>p. x = q \<circ> p \<and> p permutes S"
+    by (metis assms id_comp o_assoc permutes_compose permutes_inv permutes_inv_o(1))
+  ultimately show ?thesis
+    by auto
+qed
 
 lemma image_compose_permutations_right:
   assumes "q permutes S"
   shows "{p \<circ> q | p. p permutes S} = {p . p permutes S}"
-  apply (rule set_eqI)
-  apply auto
-   apply (rule permutes_compose)
-  using assms
-    apply auto
-  apply (rule_tac x = "x \<circ> inv q" in exI)
-  apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
-  done
+  by (metis (no_types, opaque_lifting) assms comp_id fun.map_comp permutes_compose permutes_inv permutes_inv_o(2))
 
 lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n"
   by (simp add: permutes_def) metis
diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -326,13 +326,13 @@
 
 lemma rel_fun_liminf[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal liminf liminf"
 proof -
-  have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
+  have "\<forall>x y. rel_fun (=) pcr_ennreal x y \<longrightarrow> pcr_ennreal (sup 0 (liminf x)) (liminf y) \<Longrightarrow>
+        \<forall>x y. rel_fun (=) pcr_ennreal x y \<longrightarrow> pcr_ennreal (liminf x) (liminf y)"
+    by (auto simp: comp_def Liminf_bounded rel_fun_eq_pcr_ennreal)
+  moreover have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. sup 0 (liminf x)) liminf"
     unfolding liminf_SUP_INF[abs_def] by (transfer_prover_start, transfer_step+; simp)
-  then show ?thesis
-    apply (subst (asm) (2) rel_fun_def)
-    apply (subst (2) rel_fun_def)
-    apply (auto simp: comp_def max.absorb2 Liminf_bounded rel_fun_eq_pcr_ennreal)
-    done
+  ultimately show ?thesis
+    by (simp add: rel_fun_def)
 qed
 
 lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
@@ -633,9 +633,7 @@
   unfolding divide_ennreal_def infinity_ennreal_def
   apply transfer
   subgoal for a b c
-    apply (cases a b c rule: ereal3_cases)
-    apply (auto simp: top_ereal_def)
-    done
+    by (cases a b c rule: ereal3_cases) (auto simp: top_ereal_def)
   done
 
 lemma ennreal_mult_divide_eq:
@@ -798,7 +796,7 @@
   obtains (real) r :: real where "0 \<le> r" "x = ennreal r" | (top) "x = top"
   apply transfer
   subgoal for x thesis
-    by (cases x) (auto simp: max.absorb2 top_ereal_def)
+    by (cases x) (auto simp: top_ereal_def)
   done
 
 lemmas ennreal2_cases = ennreal_cases[case_product ennreal_cases]
@@ -1152,10 +1150,11 @@
 
 (* Contributed by Dominique Unruh *)
 lemma ennreal_of_enat_plus[simp]: \<open>ennreal_of_enat (a+b) = ennreal_of_enat a + ennreal_of_enat b\<close>
-  apply (induct a)
-   apply (metis enat.exhaust ennreal_add_eq_top ennreal_of_enat_enat ennreal_of_enat_infty infinity_ennreal_def of_nat_add plus_enat_simps(1) plus_eq_infty_iff_enat)
-  apply simp
-  done
+proof (induct a)
+  case (enat nat)
+  with enat.simps show ?case
+    by (smt (verit, del_insts) add.commute add_top_left_ennreal enat.exhaust enat_defs(4) ennreal_of_enat_def of_nat_add)
+qed auto
 
 (* Contributed by Dominique Unruh *)
 lemma sum_ennreal_of_enat[simp]: "(\<Sum>i\<in>I. ennreal_of_enat (f i)) = ennreal_of_enat (sum f I)"
@@ -1553,7 +1552,7 @@
   have *: "e2ennreal (max x 0) = e2ennreal x" for x
     by (simp add: e2ennreal_def max.commute)
   have "((\<lambda>i. max (f i) 0) \<longlongrightarrow> max l 0) F"
-    apply (intro tendsto_intros) using assms by auto
+    using assms by (intro tendsto_intros) auto
   then have "((\<lambda>i. enn2ereal(e2ennreal (max (f i) 0))) \<longlongrightarrow> enn2ereal (e2ennreal (max l 0))) F"
     by (subst enn2ereal_e2ennreal, auto)+
   then have "((\<lambda>i. e2ennreal (max (f i) 0)) \<longlongrightarrow> e2ennreal (max l 0)) F"
@@ -1574,7 +1573,7 @@
   apply transfer
   subgoal for A
     using Sup_countable_SUP[of A]
-    by (force simp add: incseq_def[symmetric] SUP_upper2 max.absorb2 image_subset_iff Sup_upper2 cong: conj_cong)
+    by (force simp add: incseq_def[symmetric] SUP_upper2 image_subset_iff Sup_upper2 cong: conj_cong)
   done
 
 lemma ennreal_Inf_countable_INF:
@@ -1582,11 +1581,7 @@
   unfolding decseq_def
   apply transfer
   subgoal for A
-    using Inf_countable_INF[of A]
-    apply (clarsimp simp flip: decseq_def)
-    subgoal for f
-      by (intro exI[of _ f]) auto
-    done
+    using Inf_countable_INF[of A] by (simp flip: decseq_def) blast
   done
 
 lemma ennreal_SUP_countable_SUP:
@@ -1617,10 +1612,7 @@
 lemma ennreal_suminf_SUP_eq:
   fixes f :: "nat \<Rightarrow> nat \<Rightarrow> ennreal"
   shows "(\<And>i. incseq (\<lambda>n. f n i)) \<Longrightarrow> (\<Sum>i. SUP n. f n i) = (SUP n. \<Sum>i. f n i)"
-  apply (rule ennreal_suminf_SUP_eq_directed)
-  subgoal for N n j
-    by (auto simp: incseq_def intro!:exI[of _ "max n j"])
-  done
+  by (metis ennreal_suminf_SUP_eq_directed incseqD nat_le_linear)
 
 lemma ennreal_SUP_add_left:
   fixes c :: ennreal
@@ -1792,6 +1784,7 @@
 lemma ennreal_tendsto_top_eq_at_top:
   "((\<lambda>z. ennreal (f z)) \<longlongrightarrow> top) F \<longleftrightarrow> (LIM z F. f z :> at_top)"
   unfolding filterlim_at_top_dense tendsto_top_iff_ennreal
+  using ennreal_less_iff eventually_mono
   apply (auto simp: ennreal_less_iff)
   subgoal for y
     by (auto elim!: eventually_mono allE[of _ "max 0 y"])
diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Finite_Map.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -500,7 +500,7 @@
 lift_definition fmadd :: "('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'b) fmap" (infixl "++\<^sub>f" 100)
   is map_add
   parametric map_add_transfer
-by simp
+  by simp
 
 lemma fmlookup_add[simp]:
   "fmlookup (m ++\<^sub>f n) x = (if x |\<in>| fmdom n then fmlookup n x else fmlookup m x)"
@@ -510,67 +510,63 @@
 lemma fmdom'_add[simp]: "fmdom' (m ++\<^sub>f n) = fmdom' m \<union> fmdom' n" by transfer' auto
 
 lemma fmadd_drop_left_dom: "fmdrop_fset (fmdom n) m ++\<^sub>f n = m ++\<^sub>f n"
-by (rule fmap_ext) auto
+  by (rule fmap_ext) auto
 
 lemma fmadd_restrict_right_dom: "fmrestrict_fset (fmdom n) (m ++\<^sub>f n) = n"
-by (rule fmap_ext) auto
+  by (rule fmap_ext) auto
 
 lemma fmfilter_add_distrib[simp]: "fmfilter P (m ++\<^sub>f n) = fmfilter P m ++\<^sub>f fmfilter P n"
-by transfer' (auto simp: map_filter_def map_add_def)
+  by transfer' (auto simp: map_filter_def map_add_def)
 
 lemma fmdrop_add_distrib[simp]: "fmdrop a (m ++\<^sub>f n) = fmdrop a m ++\<^sub>f fmdrop a n"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_set_add_distrib[simp]: "fmdrop_set A (m ++\<^sub>f n) = fmdrop_set A m ++\<^sub>f fmdrop_set A n"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_fset_add_distrib[simp]: "fmdrop_fset A (m ++\<^sub>f n) = fmdrop_fset A m ++\<^sub>f fmdrop_fset A n"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_add_distrib[simp]:
   "fmrestrict_set A (m ++\<^sub>f n) = fmrestrict_set A m ++\<^sub>f fmrestrict_set A n"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_fset_add_distrib[simp]:
   "fmrestrict_fset A (m ++\<^sub>f n) = fmrestrict_fset A m ++\<^sub>f fmrestrict_fset A n"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmadd_empty[simp]: "fmempty ++\<^sub>f m = m" "m ++\<^sub>f fmempty = m"
-by (transfer'; auto)+
+  by (transfer'; auto)+
 
 lemma fmadd_idempotent[simp]: "m ++\<^sub>f m = m"
-by transfer' (auto simp: map_add_def split: option.splits)
+  by transfer' (auto simp: map_add_def split: option.splits)
 
 lemma fmadd_assoc[simp]: "m ++\<^sub>f (n ++\<^sub>f p) = m ++\<^sub>f n ++\<^sub>f p"
-by transfer' simp
+  by transfer' simp
 
 lemma fmadd_fmupd[simp]: "m ++\<^sub>f fmupd a b n = fmupd a b (m ++\<^sub>f n)"
-by (rule fmap_ext) simp
+  by (rule fmap_ext) simp
 
 lift_definition fmpred :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> bool"
   is map_pred
   parametric map_pred_transfer
-.
+  .
 
 lemma fmpredI[intro]:
   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y"
   shows "fmpred P m"
-using assms
-by transfer' (auto simp: map_pred_def split: option.splits)
+  using assms
+  by transfer' (auto simp: map_pred_def split: option.splits)
 
 lemma fmpredD[dest]: "fmpred P m \<Longrightarrow> fmlookup m x = Some y \<Longrightarrow> P x y"
-by transfer' (auto simp: map_pred_def split: option.split_asm)
+  by transfer' (auto simp: map_pred_def split: option.split_asm)
 
 lemma fmpred_iff: "fmpred P m \<longleftrightarrow> (\<forall>x y. fmlookup m x = Some y \<longrightarrow> P x y)"
-by auto
+  by auto
 
 lemma fmpred_alt_def: "fmpred P m \<longleftrightarrow> fBall (fmdom m) (\<lambda>x. P x (the (fmlookup m x)))"
-unfolding fmpred_iff
-apply auto
-apply (rename_tac x y)
-apply (erule_tac x = x in fBallE)
-apply simp
-by (simp add: fmlookup_dom_iff)
+  unfolding fmpred_iff
+  using fmdomI by fastforce
 
 lemma fmpred_mono_strong:
   assumes "\<And>x y. fmlookup m x = Some y \<Longrightarrow> P x y \<Longrightarrow> Q x y"
@@ -578,40 +574,37 @@
 using assms unfolding fmpred_iff by auto
 
 lemma fmpred_mono[mono]: "P \<le> Q \<Longrightarrow> fmpred P \<le> fmpred Q"
-apply rule
-apply (rule fmpred_mono_strong[where P = P and Q = Q])
-apply auto
-done
+  by auto
 
 lemma fmpred_empty[intro!, simp]: "fmpred P fmempty"
-by auto
+  by auto
 
 lemma fmpred_upd[intro]: "fmpred P m \<Longrightarrow> P x y \<Longrightarrow> fmpred P (fmupd x y m)"
-by transfer' (auto simp: map_pred_def map_upd_def)
+  by transfer' (auto simp: map_pred_def map_upd_def)
 
 lemma fmpred_updD[dest]: "fmpred P (fmupd x y m) \<Longrightarrow> P x y"
-by auto
+  by auto
 
 lemma fmpred_add[intro]: "fmpred P m \<Longrightarrow> fmpred P n \<Longrightarrow> fmpred P (m ++\<^sub>f n)"
-by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
+  by transfer' (auto simp: map_pred_def map_add_def split: option.splits)
 
 lemma fmpred_filter[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmfilter Q m)"
-by transfer' (auto simp: map_pred_def map_filter_def)
+  by transfer' (auto simp: map_pred_def map_filter_def)
 
 lemma fmpred_drop[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop a m)"
-by (auto simp: fmfilter_alt_defs)
+  by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_drop_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_set A m)"
-by (auto simp: fmfilter_alt_defs)
+  by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_drop_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmdrop_fset A m)"
-by (auto simp: fmfilter_alt_defs)
+  by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_restrict_set[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_set A m)"
-by (auto simp: fmfilter_alt_defs)
+  by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_restrict_fset[intro]: "fmpred P m \<Longrightarrow> fmpred P (fmrestrict_fset A m)"
-by (auto simp: fmfilter_alt_defs)
+  by (auto simp: fmfilter_alt_defs)
 
 lemma fmpred_cases[consumes 1]:
   assumes "fmpred P m"
@@ -667,18 +660,18 @@
 unfolding fmfilter_alt_defs by (rule fmfilter_subset)
 
 lift_definition fset_of_fmap :: "('a, 'b) fmap \<Rightarrow> ('a \<times> 'b) fset" is set_of_map
-by (rule set_of_map_finite)
+  by (rule set_of_map_finite)
 
 lemma fset_of_fmap_inj[intro, simp]: "inj fset_of_fmap"
-apply rule
-apply transfer'
-using set_of_map_inj unfolding inj_def by auto
+  apply rule
+  apply transfer'
+  using set_of_map_inj unfolding inj_def by auto
 
 lemma fset_of_fmap_iff[simp]: "(a, b) |\<in>| fset_of_fmap m \<longleftrightarrow> fmlookup m a = Some b"
 by transfer' (auto simp: set_of_map_def)
 
-lemma fset_of_fmap_iff'[simp]: "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
-by transfer' (auto simp: set_of_map_def)
+lemma fset_of_fmap_iff': "(a, b) \<in> fset (fset_of_fmap m) \<longleftrightarrow> fmlookup m a = Some b"
+  by simp
 
 lift_definition fmap_of_list :: "('a \<times> 'b) list \<Rightarrow> ('a, 'b) fmap"
   is map_of
@@ -688,28 +681,25 @@
 lemma fmap_of_list_simps[simp]:
   "fmap_of_list [] = fmempty"
   "fmap_of_list ((k, v) # kvs) = fmupd k v (fmap_of_list kvs)"
-by (transfer, simp add: map_upd_def)+
+  by (transfer, simp add: map_upd_def)+
 
 lemma fmap_of_list_app[simp]: "fmap_of_list (xs @ ys) = fmap_of_list ys ++\<^sub>f fmap_of_list xs"
-by transfer' simp
+  by transfer' simp
 
 lemma fmupd_alt_def: "fmupd k v m = m ++\<^sub>f fmap_of_list [(k, v)]"
-by transfer' (auto simp: map_upd_def)
+  by simp
 
 lemma fmpred_of_list[intro]:
   assumes "\<And>k v. (k, v) \<in> set xs \<Longrightarrow> P k v"
   shows "fmpred P (fmap_of_list xs)"
-using assms
-by (induction xs) (transfer'; auto simp: map_pred_def)+
+  using assms
+  by (induction xs) (transfer'; auto simp: map_pred_def)+
 
 lemma fmap_of_list_SomeD: "fmlookup (fmap_of_list xs) k = Some v \<Longrightarrow> (k, v) \<in> set xs"
-by transfer' (auto dest: map_of_SomeD)
+  by transfer' (auto dest: map_of_SomeD)
 
 lemma fmdom_fmap_of_list[simp]: "fmdom (fmap_of_list xs) = fset_of_list (map fst xs)"
-apply transfer'
-apply (subst dom_map_of_conv_image_fst)
-apply auto
-done
+  by transfer' (simp add: dom_map_of_conv_image_fst)
 
 lift_definition fmrel_on_fset :: "'a fset \<Rightarrow> ('b \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap \<Rightarrow> bool"
   is rel_map_on_set
@@ -721,109 +711,103 @@
 lemma fmrel_on_fsetI[intro]:
   assumes "\<And>x. x |\<in>| S \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
   shows "fmrel_on_fset S P m n"
-using assms
-unfolding fmrel_on_fset_alt_def by auto
+  by (simp add: assms fmrel_on_fset_alt_def)
 
 lemma fmrel_on_fset_mono[mono]: "R \<le> Q \<Longrightarrow> fmrel_on_fset S R \<le> fmrel_on_fset S Q"
-unfolding fmrel_on_fset_alt_def[abs_def]
-apply (intro le_funI fBall_mono)
-using option.rel_mono by auto
+  unfolding fmrel_on_fset_alt_def[abs_def]
+  using option.rel_mono by blast
 
 lemma fmrel_on_fsetD: "x |\<in>| S \<Longrightarrow> fmrel_on_fset S P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
-unfolding fmrel_on_fset_alt_def
-by auto
+  unfolding fmrel_on_fset_alt_def
+  by auto
 
 lemma fmrel_on_fsubset: "fmrel_on_fset S R m n \<Longrightarrow> T |\<subseteq>| S \<Longrightarrow> fmrel_on_fset T R m n"
-unfolding fmrel_on_fset_alt_def
-by auto
+  unfolding fmrel_on_fset_alt_def
+  by auto
 
 lemma fmrel_on_fset_unionI:
   "fmrel_on_fset A R m n \<Longrightarrow> fmrel_on_fset B R m n \<Longrightarrow> fmrel_on_fset (A |\<union>| B) R m n"
-unfolding fmrel_on_fset_alt_def
-by auto
+  unfolding fmrel_on_fset_alt_def
+  by auto
 
 lemma fmrel_on_fset_updateI:
   assumes "fmrel_on_fset S P m n" "P v\<^sub>1 v\<^sub>2"
   shows "fmrel_on_fset (finsert k S) P (fmupd k v\<^sub>1 m) (fmupd k v\<^sub>2 n)"
-using assms
-unfolding fmrel_on_fset_alt_def
-by auto
+  using assms
+  unfolding fmrel_on_fset_alt_def
+  by auto
 
 lift_definition fmimage :: "('a, 'b) fmap \<Rightarrow> 'a fset \<Rightarrow> 'b fset" is "\<lambda>m S. {b|a b. m a = Some b \<and> a \<in> S}"
-subgoal for m S
-  apply (rule finite_subset[where B = "ran m"])
-  apply (auto simp: ran_def)[]
-  by (rule finite_ran)
-done
+  by (smt (verit, del_insts) Collect_mono_iff finite_surj ran_alt_def ran_def)
 
 lemma fmimage_alt_def: "fmimage m S = fmran (fmrestrict_fset S m)"
-by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
+  by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
 
 lemma fmimage_empty[simp]: "fmimage m fempty = fempty"
-by transfer' auto
+  by transfer' auto
 
 lemma fmimage_subset_ran[simp]: "fmimage m S |\<subseteq>| fmran m"
-by transfer' (auto simp: ran_def)
+  by transfer' (auto simp: ran_def)
 
 lemma fmimage_dom[simp]: "fmimage m (fmdom m) = fmran m"
-by transfer' (auto simp: ran_def)
+  by transfer' (auto simp: ran_def)
 
 lemma fmimage_inter: "fmimage m (A |\<inter>| B) |\<subseteq>| fmimage m A |\<inter>| fmimage m B"
-by transfer' auto
+  by transfer' auto
 
 lemma fimage_inter_dom[simp]:
   "fmimage m (fmdom m |\<inter>| A) = fmimage m A"
   "fmimage m (A |\<inter>| fmdom m) = fmimage m A"
-by (transfer'; auto)+
+  by (transfer'; auto)+
 
 lemma fmimage_union[simp]: "fmimage m (A |\<union>| B) = fmimage m A |\<union>| fmimage m B"
-by transfer' auto
+  by transfer' auto
 
 lemma fmimage_Union[simp]: "fmimage m (ffUnion A) = ffUnion (fmimage m |`| A)"
-by transfer' auto
+  by transfer' auto
 
 lemma fmimage_filter[simp]: "fmimage (fmfilter P m) A = fmimage m (ffilter P A)"
-by transfer' (auto simp: map_filter_def)
+  by transfer' (auto simp: map_filter_def)
 
 lemma fmimage_drop[simp]: "fmimage (fmdrop a m) A = fmimage m (A - {|a|})"
-by transfer' (auto simp: map_filter_def map_drop_def)
+  by (simp add: fmimage_alt_def)
 
 lemma fmimage_drop_fset[simp]: "fmimage (fmdrop_fset B m) A = fmimage m (A - B)"
-by transfer' (auto simp: map_filter_def map_drop_set_def)
+  by transfer' (auto simp: map_filter_def map_drop_set_def)
 
 lemma fmimage_restrict_fset[simp]: "fmimage (fmrestrict_fset B m) A = fmimage m (A |\<inter>| B)"
-by transfer' (auto simp: map_filter_def map_restrict_set_def)
+  by transfer' (auto simp: map_filter_def map_restrict_set_def)
 
 lemma fmfilter_ran[simp]: "fmran (fmfilter P m) = fmimage m (ffilter P (fmdom m))"
-by transfer' (auto simp: ran_def map_filter_def)
+  by transfer' (auto simp: ran_def map_filter_def)
 
 lemma fmran_drop[simp]: "fmran (fmdrop a m) = fmimage m (fmdom m - {|a|})"
-by transfer' (auto simp: ran_def map_drop_def map_filter_def)
+  by transfer' (auto simp: ran_def map_drop_def map_filter_def)
 
 lemma fmran_drop_fset[simp]: "fmran (fmdrop_fset A m) = fmimage m (fmdom m - A)"
-by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
+  by transfer' (auto simp: ran_def map_drop_set_def map_filter_def)
 
 lemma fmran_restrict_fset: "fmran (fmrestrict_fset A m) = fmimage m (fmdom m |\<inter>| A)"
-by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
+  by transfer' (auto simp: ran_def map_restrict_set_def map_filter_def)
 
 lemma fmlookup_image_iff: "y |\<in>| fmimage m A \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y \<and> x |\<in>| A)"
-by transfer' (auto simp: ran_def)
+  by transfer' (auto simp: ran_def)
 
 lemma fmimageI: "fmlookup m x = Some y \<Longrightarrow> x |\<in>| A \<Longrightarrow> y |\<in>| fmimage m A"
-by (auto simp: fmlookup_image_iff)
+  by (auto simp: fmlookup_image_iff)
 
 lemma fmimageE[elim]:
   assumes "y |\<in>| fmimage m A"
   obtains x where "fmlookup m x = Some y" "x |\<in>| A"
-using assms by (auto simp: fmlookup_image_iff)
+  using assms by (auto simp: fmlookup_image_iff)
 
 lift_definition fmcomp :: "('b, 'c) fmap \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" (infixl "\<circ>\<^sub>f" 55)
   is map_comp
   parametric map_comp_transfer
-by (rule dom_comp_finite)
+  by (rule dom_comp_finite)
 
 lemma fmlookup_comp[simp]: "fmlookup (m \<circ>\<^sub>f n) x = Option.bind (fmlookup n x) (fmlookup m)"
-by transfer' (auto simp: map_comp_def split: option.splits)
+  by transfer' (auto simp: map_comp_def split: option.splits)
 
 end
 
@@ -839,13 +823,14 @@
 
 
 lemma fmran'_alt_def: "fmran' m = fset (fmran m)"
-including fset.lifting
-by transfer' (auto simp: ran_def fun_eq_iff)
+  including fset.lifting
+  by transfer' (auto simp: ran_def fun_eq_iff)
 
 lemma fmlookup_ran'_iff: "y \<in> fmran' m \<longleftrightarrow> (\<exists>x. fmlookup m x = Some y)"
-by transfer' (auto simp: ran_def)
+  by transfer' (auto simp: ran_def)
 
-lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" by (auto simp: fmlookup_ran'_iff)
+lemma fmran'I: "fmlookup m x = Some y \<Longrightarrow> y \<in> fmran' m" 
+  by (auto simp: fmlookup_ran'_iff)
 
 lemma fmran'E[elim]:
   assumes "y \<in> fmran' m"
@@ -858,22 +843,19 @@
 lemma fmrelI[intro]:
   assumes "\<And>x. rel_option R (fmlookup m x) (fmlookup n x)"
   shows "fmrel R m n"
-using assms
-by transfer' auto
+  using assms
+  by transfer' auto
 
 lemma fmrel_upd[intro]: "fmrel P m n \<Longrightarrow> P x y \<Longrightarrow> fmrel P (fmupd k x m) (fmupd k y n)"
-by transfer' (auto simp: map_upd_def rel_fun_def)
+  by transfer' (auto simp: map_upd_def rel_fun_def)
 
 lemma fmrelD[dest]: "fmrel P m n \<Longrightarrow> rel_option P (fmlookup m x) (fmlookup n x)"
-by transfer' (auto simp: rel_fun_def)
+  by transfer' (auto simp: rel_fun_def)
 
 lemma fmrel_addI[intro]:
   assumes "fmrel P m n" "fmrel P a b"
   shows "fmrel P (m ++\<^sub>f a) (n ++\<^sub>f b)"
-using assms
-apply transfer'
-apply (auto simp: rel_fun_def map_add_def)
-by (metis option.case_eq_if option.collapse option.rel_sel)
+  by (smt (verit, del_insts) assms domIff fmdom.rep_eq fmlookup_add fmrel_iff option.rel_sel)
 
 lemma fmrel_cases[consumes 1]:
   assumes "fmrel P m n"
@@ -974,72 +956,77 @@
 qed
 
 lemma fmrel_rel_fmran': "fmrel P x y \<Longrightarrow> rel_set P (fmran' x) (fmran' y)"
-unfolding fmran'_alt_def
-by (metis fmrel_rel_fmran rel_fset_fset)
+  unfolding fmran'_alt_def
+  by (metis fmrel_rel_fmran rel_fset_fset)
 
 lemma pred_fmap_fmpred[simp]: "pred_fmap P = fmpred (\<lambda>_. P)"
-unfolding fmap.pred_set fmran'_alt_def
-including fset.lifting
-apply transfer'
-apply (rule ext)
-apply (auto simp: map_pred_def ran_def split: option.splits dest: )
-done
+  unfolding fmap.pred_set fmran'_alt_def
+  using fmranI by fastforce
 
 lemma pred_fmap_id[simp]: "pred_fmap id (fmmap f m) \<longleftrightarrow> pred_fmap f m"
-unfolding fmap.pred_set fmap.set_map
-by simp
+  unfolding fmap.pred_set fmap.set_map
+  by simp
 
 lemma pred_fmapD: "pred_fmap P m \<Longrightarrow> x |\<in>| fmran m \<Longrightarrow> P x"
-by auto
+  by auto
 
 lemma fmlookup_map[simp]: "fmlookup (fmmap f m) x = map_option f (fmlookup m x)"
-by transfer' auto
+  by transfer' auto
 
 lemma fmpred_map[simp]: "fmpred P (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>k v. P k (f v)) m"
-unfolding fmpred_iff pred_fmap_def fmap.set_map
-by auto
+  unfolding fmpred_iff pred_fmap_def fmap.set_map
+  by auto
 
 lemma fmpred_id[simp]: "fmpred (\<lambda>_. id) (fmmap f m) \<longleftrightarrow> fmpred (\<lambda>_. f) m"
-by simp
+  by simp
 
 lemma fmmap_add[simp]: "fmmap f (m ++\<^sub>f n) = fmmap f m ++\<^sub>f fmmap f n"
-by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
+  by transfer' (auto simp: map_add_def fun_eq_iff split: option.splits)
 
 lemma fmmap_empty[simp]: "fmmap f fmempty = fmempty"
-by transfer auto
+  by transfer auto
 
 lemma fmdom_map[simp]: "fmdom (fmmap f m) = fmdom m"
-including fset.lifting
-by transfer' simp
+  including fset.lifting
+  by transfer' simp
 
 lemma fmdom'_map[simp]: "fmdom' (fmmap f m) = fmdom' m"
-by transfer' simp
+  by transfer' simp
 
 lemma fmran_fmmap[simp]: "fmran (fmmap f m) = f |`| fmran m"
-including fset.lifting
-by transfer' (auto simp: ran_def)
+  including fset.lifting
+  by transfer' (auto simp: ran_def)
 
 lemma fmran'_fmmap[simp]: "fmran' (fmmap f m) = f ` fmran' m"
-by transfer' (auto simp: ran_def)
+  by transfer' (auto simp: ran_def)
 
 lemma fmfilter_fmmap[simp]: "fmfilter P (fmmap f m) = fmmap f (fmfilter P m)"
-by transfer' (auto simp: map_filter_def)
+  by transfer' (auto simp: map_filter_def)
+
+lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" 
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)"
+  unfolding fmfilter_alt_defs by simp
 
-lemma fmdrop_fmmap[simp]: "fmdrop a (fmmap f m) = fmmap f (fmdrop a m)" unfolding fmfilter_alt_defs by simp
-lemma fmdrop_set_fmmap[simp]: "fmdrop_set A (fmmap f m) = fmmap f (fmdrop_set A m)" unfolding fmfilter_alt_defs by simp
-lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)" unfolding fmfilter_alt_defs by simp
-lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)" unfolding fmfilter_alt_defs by simp
-lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)" unfolding fmfilter_alt_defs by simp
+lemma fmdrop_fset_fmmap[simp]: "fmdrop_fset A (fmmap f m) = fmmap f (fmdrop_fset A m)"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_set_fmmap[simp]: "fmrestrict_set A (fmmap f m) = fmmap f (fmrestrict_set A m)"
+  unfolding fmfilter_alt_defs by simp
+
+lemma fmrestrict_fset_fmmap[simp]: "fmrestrict_fset A (fmmap f m) = fmmap f (fmrestrict_fset A m)"
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmmap_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap f m \<subseteq>\<^sub>f fmmap f n"
-by transfer' (auto simp: map_le_def)
+  by transfer' (auto simp: map_le_def)
 
 lemma fmmap_fset_of_fmap: "fset_of_fmap (fmmap f m) = (\<lambda>(k, v). (k, f v)) |`| fset_of_fmap m"
-including fset.lifting
-by transfer' (auto simp: set_of_map_def)
+  including fset.lifting
+  by transfer' (auto simp: set_of_map_def)
 
 lemma fmmap_fmupd: "fmmap f (fmupd x y m) = fmupd x (f y) (fmmap f m)"
-by transfer' (auto simp: fun_eq_iff map_upd_def)
+  by transfer' (auto simp: fun_eq_iff map_upd_def)
 
 subsection \<open>\<^const>\<open>size\<close> setup\<close>
 
@@ -1056,20 +1043,18 @@
 end
 
 lemma size_fmap_overloaded_simps[simp]: "size x = size (fset_of_fmap x)"
-unfolding size_fmap_overloaded_def
-by simp
+  unfolding size_fmap_overloaded_def
+  by simp
 
-lemma fmap_size_o_map: "inj h \<Longrightarrow> size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+lemma fmap_size_o_map: "size_fmap f g \<circ> fmmap h = size_fmap f (g \<circ> h)"
+proof -
+  have inj: "inj_on (\<lambda>(k, v). (k, h v)) (fset (fset_of_fmap m))" for m
+    using inj_on_def by force
+  show ?thesis
   unfolding size_fmap_def
-  apply (auto simp: fun_eq_iff fmmap_fset_of_fmap)
-  apply (subst sum.reindex)
-  subgoal for m
-    using prod.inj_map[unfolded map_prod_def, of "\<lambda>x. x" h]
-    unfolding inj_on_def
-    by auto
-  subgoal
-    by (rule sum.cong) (auto split: prod.splits)
-  done
+  apply (clarsimp simp: fun_eq_iff fmmap_fset_of_fmap sum.reindex [OF inj])
+  by (rule sum.cong) (auto split: prod.splits)
+qed
 
 setup \<open>
 BNF_LFP_Size.register_size_global \<^type_name>\<open>fmap\<close> \<^const_name>\<open>size_fmap\<close>
@@ -1082,53 +1067,51 @@
 
 lift_definition fmmap_keys :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) fmap \<Rightarrow> ('a, 'c) fmap" is
   "\<lambda>f m a. map_option (f a) (m a)"
-unfolding dom_def
-by simp
+  unfolding dom_def
+  by simp
 
 lemma fmpred_fmmap_keys[simp]: "fmpred P (fmmap_keys f m) = fmpred (\<lambda>a b. P a (f a b)) m"
-by transfer' (auto simp: map_pred_def split: option.splits)
+  by transfer' (auto simp: map_pred_def split: option.splits)
 
 lemma fmdom_fmmap_keys[simp]: "fmdom (fmmap_keys f m) = fmdom m"
-including fset.lifting
-by transfer' auto
+  including fset.lifting
+  by transfer' auto
 
 lemma fmlookup_fmmap_keys[simp]: "fmlookup (fmmap_keys f m) x = map_option (f x) (fmlookup m x)"
-by transfer' simp
+  by transfer' simp
 
 lemma fmfilter_fmmap_keys[simp]: "fmfilter P (fmmap_keys f m) = fmmap_keys f (fmfilter P m)"
-by transfer' (auto simp: map_filter_def)
+  by transfer' (auto simp: map_filter_def)
 
 lemma fmdrop_fmmap_keys[simp]: "fmdrop a (fmmap_keys f m) = fmmap_keys f (fmdrop a m)"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_set_fmmap_keys[simp]: "fmdrop_set A (fmmap_keys f m) = fmmap_keys f (fmdrop_set A m)"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmdrop_fset_fmmap_keys[simp]: "fmdrop_fset A (fmmap_keys f m) = fmmap_keys f (fmdrop_fset A m)"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_set_fmmap_keys[simp]: "fmrestrict_set A (fmmap_keys f m) = fmmap_keys f (fmrestrict_set A m)"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmrestrict_fset_fmmap_keys[simp]: "fmrestrict_fset A (fmmap_keys f m) = fmmap_keys f (fmrestrict_fset A m)"
-unfolding fmfilter_alt_defs by simp
+  unfolding fmfilter_alt_defs by simp
 
 lemma fmmap_keys_subset[intro]: "m \<subseteq>\<^sub>f n \<Longrightarrow> fmmap_keys f m \<subseteq>\<^sub>f fmmap_keys f n"
-by transfer' (auto simp: map_le_def dom_def)
+  by transfer' (auto simp: map_le_def dom_def)
 
 definition sorted_list_of_fmap :: "('a::linorder, 'b) fmap \<Rightarrow> ('a \<times> 'b) list" where
-"sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
+  "sorted_list_of_fmap m = map (\<lambda>k. (k, the (fmlookup m k))) (sorted_list_of_fset (fmdom m))"
 
 lemma list_all_sorted_list[simp]: "list_all P (sorted_list_of_fmap m) = fmpred (curry P) m"
 unfolding sorted_list_of_fmap_def curry_def list.pred_map
-apply (auto simp: list_all_iff)
-including fset.lifting
-by (transfer; auto simp: dom_def map_pred_def split: option.splits)+
+  by (smt (verit, best) Ball_set comp_def fmpred_alt_def sorted_list_of_fset_simps(1))
 
 lemma map_of_sorted_list[simp]: "map_of (sorted_list_of_fmap m) = fmlookup m"
-unfolding sorted_list_of_fmap_def
-including fset.lifting
-by transfer (simp add: map_of_map_keys)
+  unfolding sorted_list_of_fmap_def
+  including fset.lifting
+  by transfer (simp add: map_of_map_keys)
 
 
 subsection \<open>Additional properties\<close>
@@ -1138,7 +1121,7 @@
   shows "\<exists>m. fmdom' m = S \<and> fmpred Q m"
 proof -
   obtain f where f: "Q x (f x)" if "x \<in> S" for x
-    using assms by (metis bchoice)
+    using assms by metis
   define f' where "f' x = (if x \<in> S then Some (f x) else None)" for x
 
   have "eq_onp (\<lambda>m. finite (dom m)) f' f'"
@@ -1157,15 +1140,15 @@
 context includes lifting_syntax begin
 
 lemma fmempty_transfer[simp, intro, transfer_rule]: "fmrel P fmempty fmempty"
-by transfer auto
+  by transfer auto
 
 lemma fmadd_transfer[transfer_rule]:
   "(fmrel P ===> fmrel P ===> fmrel P) fmadd fmadd"
-by (intro fmrel_addI rel_funI)
+  by (intro fmrel_addI rel_funI)
 
 lemma fmupd_transfer[transfer_rule]:
   "((=) ===> P ===> fmrel P ===> fmrel P) fmupd fmupd"
-by auto
+  by auto
 
 end
 
@@ -1176,21 +1159,18 @@
   fix m n
   assume "fmrel T m n"
   then have "fmlookup (fmmap Abs m) x = fmlookup n x" for x
-    apply (cases rule: fmrel_cases[where x = x])
-    using assms unfolding Quotient_alt_def by auto
+    using assms unfolding Quotient_alt_def 
+      by (cases rule: fmrel_cases[where x = x]) auto
   then show "fmmap Abs m = n"
     by (rule fmap_ext)
 next
   fix m
   show "fmrel T (fmmap Rep m) m"
     unfolding fmap.rel_map
-    apply (rule fmap.rel_refl)
-    using assms unfolding Quotient_alt_def
-    by auto
+    by (metis (mono_tags) Quotient_alt_def assms fmap.rel_refl)
 next
   from assms have "R = T OO T\<inverse>\<inverse>"
     unfolding Quotient_alt_def4 by simp
-
   then show "fmrel R = fmrel T OO (fmrel T)\<inverse>\<inverse>"
     by (simp add: fmap.rel_compp fmap.rel_conversep)
 qed
@@ -1201,7 +1181,7 @@
 lemma fmap_distinct[simp]:
   "fmempty \<noteq> fmupd k v m"
   "fmupd k v m \<noteq> fmempty"
-by (transfer'; auto simp: map_upd_def fun_eq_iff)+
+  by (transfer'; auto simp: map_upd_def fun_eq_iff)+
 
 lifting_update fmap.lifting
 
@@ -1259,20 +1239,13 @@
     by auto
   with insert have "P (fmdrop x m)"
     by auto
-
-  have "x |\<in>| fmdom m"
-    using insert by auto
-  then obtain y where "fmlookup m x = Some y"
-    by auto
+  moreover
+  obtain y where "fmlookup m x = Some y"
+    using insert.hyps by force
   hence "m = fmupd x y (fmdrop x m)"
     by (auto intro: fmap_ext)
-
-  show ?case
-    apply (subst \<open>m = _\<close>)
-    apply (rule assms)
-    apply fact
-    apply simp
-    done
+  ultimately show ?case
+    by (metis assms(2) fmdrop_lookup)
 qed
 
 
@@ -1339,32 +1312,27 @@
 by transfer (simp add: merge_conv')
 
 lemma fmmap_of_list[code]: "fmmap f (fmap_of_list m) = fmap_of_list (map (apsnd f) m)"
-apply transfer
-apply (subst map_of_map[symmetric])
-apply (auto simp: apsnd_def map_prod_def)
-done
+  apply transfer
+  by (metis (no_types, lifting) apsnd_conv map_eq_conv map_of_map old.prod.case old.prod.exhaust)
 
 lemma fmmap_keys_of_list[code]:
   "fmmap_keys f (fmap_of_list m) = fmap_of_list (map (\<lambda>(a, b). (a, f a b)) m)"
-apply transfer
-subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
-done
+  apply transfer
+  subgoal for f m by (induction m) (auto simp: apsnd_def map_prod_def fun_eq_iff)
+  done
 
 lemma fmimage_of_list[code]:
   "fmimage (fmap_of_list m) A = fset_of_list (map snd (filter (\<lambda>(k, _). k |\<in>| A) (AList.clearjunk m)))"
-apply (subst fmimage_alt_def)
-apply (subst fmfilter_alt_defs)
-apply (subst fmfilter_of_list)
-apply (subst fmran_of_list)
-apply transfer'
-apply (subst AList.restrict_eq[symmetric])
-apply (subst clearjunk_restrict)
-apply (subst AList.restrict_eq)
-by auto
+  apply (subst fmimage_alt_def)
+  apply (subst fmfilter_alt_defs)
+  apply (subst fmfilter_of_list)
+  apply (subst fmran_of_list)
+  apply transfer'
+  by (metis AList.restrict_eq clearjunk_restrict list.set_map)
 
 lemma fmcomp_list[code]:
   "fmap_of_list m \<circ>\<^sub>f fmap_of_list n = fmap_of_list (AList.compose n m)"
-by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
+  by (rule fmap_ext) (simp add: fmlookup_of_list compose_conv map_comp_def split: option.splits)
 
 end
 
diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/Library/Lattice_Algebras.thy
--- a/src/HOL/Library/Lattice_Algebras.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Lattice_Algebras.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -9,34 +9,25 @@
 class semilattice_inf_ab_group_add = ordered_ab_group_add + semilattice_inf
 begin
 
-lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)"
-  apply (rule order.antisym)
-   apply (simp_all add: le_infI)
-  apply (rule add_le_imp_le_left [of "uminus a"])
-  apply (simp only: add.assoc [symmetric], simp add: diff_le_eq add.commute)
-  done
+lemma add_inf_distrib_left: "a + inf b c = inf (a + b) (a + c)" (is "?L=?R")
+proof (intro order.antisym)
+  show "?R \<le> ?L"
+  by (metis add_commute diff_le_eq inf_greatest inf_le1 inf_le2)
+qed simp
 
 lemma add_inf_distrib_right: "inf a b + c = inf (a + c) (b + c)"
-proof -
-  have "c + inf a b = inf (c + a) (c + b)"
-    by (simp add: add_inf_distrib_left)
-  then show ?thesis
-    by (simp add: add.commute)
-qed
+  using add_commute add_inf_distrib_left by presburger
 
 end
 
 class semilattice_sup_ab_group_add = ordered_ab_group_add + semilattice_sup
 begin
 
-lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)"
-  apply (rule order.antisym)
-   apply (rule add_le_imp_le_left [of "uminus a"])
-   apply (simp only: add.assoc [symmetric], simp)
-   apply (simp add: le_diff_eq add.commute)
-  apply (rule le_supI)
-   apply (rule add_le_imp_le_left [of "a"], simp only: add.assoc[symmetric], simp)+
-  done
+lemma add_sup_distrib_left: "a + sup b c = sup (a + b) (a + c)" (is "?L = ?R")
+proof (rule order.antisym)
+  show "?L \<le> ?R"
+    by (metis add_commute le_diff_eq sup.bounded_iff sup_ge1 sup_ge2)
+qed simp
 
 lemma add_sup_distrib_right: "sup a b + c = sup (a + c) (b + c)"
 proof -
@@ -193,22 +184,13 @@
 qed
 
 lemma inf_0_imp_0: "inf a (- a) = 0 \<Longrightarrow> a = 0"
-  apply (simp add: inf_eq_neg_sup)
-  apply (simp add: sup_commute)
-  apply (erule sup_0_imp_0)
-  done
+  by (metis local.neg_0_equal_iff_equal neg_inf_eq_sup sup_0_imp_0)
 
-lemma inf_0_eq_0 [simp, no_atp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
-  apply (rule iffI)
-   apply (erule inf_0_imp_0)
-  apply simp
-  done
+lemma inf_0_eq_0 [simp]: "inf a (- a) = 0 \<longleftrightarrow> a = 0"
+  by (metis inf_0_imp_0 inf.idem minus_zero)
 
-lemma sup_0_eq_0 [simp, no_atp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
-  apply (rule iffI)
-   apply (erule sup_0_imp_0)
-  apply simp
-  done
+lemma sup_0_eq_0 [simp]: "sup a (- a) = 0 \<longleftrightarrow> a = 0"
+  by (metis minus_zero sup.idem sup_0_imp_0)
 
 lemma zero_le_double_add_iff_zero_le_single_add [simp]: "0 \<le> a + a \<longleftrightarrow> 0 \<le> a"
   (is "?lhs \<longleftrightarrow> ?rhs")
@@ -361,11 +343,7 @@
     have e: "- a - b = - (a + b)"
       by simp
     from a d e have "\<bar>a + b\<bar> \<le> sup ?m ?n"
-      apply -
-      apply (drule abs_leI)
-       apply (simp_all only: algebra_simps minus_add)
-      apply (metis add_uminus_conv_diff d sup_commute uminus_add_conv_diff)
-      done
+      by (metis abs_leI)
     with g[symmetric] show ?thesis by simp
   qed
 qed
@@ -418,31 +396,21 @@
   have bh: "u = a \<Longrightarrow> v = b \<Longrightarrow>
             u * v = pprt a * pprt b + pprt a * nprt b +
                     nprt a * pprt b + nprt a * nprt b" for u v :: 'a
-    apply (subst prts[of u], subst prts[of v])
-    apply (simp add: algebra_simps)
-    done
+    by (metis add.commute combine_common_factor distrib_left prts)
   note b = this[OF refl[of a] refl[of b]]
   have xy: "- ?x \<le> ?y"
     apply simp
-    apply (metis (full_types) add_increasing add_uminus_conv_diff
-      lattice_ab_group_add_class.minus_le_self_iff minus_add_distrib mult_nonneg_nonneg
-      mult_nonpos_nonpos nprt_le_zero zero_le_pprt)
-    done
+    by (meson add_increasing2 diff_le_eq neg_le_0_iff_le nprt_le_zero order.trans split_mult_pos_le zero_le_pprt)
   have yx: "?y \<le> ?x"
     apply simp
-    apply (metis (full_types) add_nonpos_nonpos add_uminus_conv_diff
-      lattice_ab_group_add_class.le_minus_self_iff minus_add_distrib mult_nonneg_nonpos
-      mult_nonpos_nonneg nprt_le_zero zero_le_pprt)
-    done
-  have i1: "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
-    by (simp only: a b yx)
-  have i2: "- (\<bar>a\<bar> * \<bar>b\<bar>) \<le> a * b"
-    by (simp only: a b xy)
+    by (metis add_decreasing2 diff_0 diff_mono diff_zero mult_nonpos_nonneg mult_right_mono_neg mult_zero_left nprt_le_zero zero_le_pprt)
   show ?thesis
-    apply (rule abs_leI)
-    apply (simp add: i1)
-    apply (simp add: i2[simplified minus_le_iff])
-    done
+  proof (rule abs_leI)
+    show "a * b \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+      by (simp only: a b yx)
+    show "- (a * b) \<le> \<bar>a\<bar> * \<bar>b\<bar>"
+      by (metis a bh minus_le_iff xy)
+  qed
 qed
 
 instance lattice_ring \<subseteq> ordered_ring_abs
@@ -452,40 +420,20 @@
   show "\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
   proof -
     have s: "(0 \<le> a * b) \<or> (a * b \<le> 0)"
-      apply auto
-      apply (rule_tac split_mult_pos_le)
-      apply (rule_tac contrapos_np[of "a * b \<le> 0"])
-      apply simp
-      apply (rule_tac split_mult_neg_le)
-      using a
-      apply blast
-      done
+      by (metis a split_mult_neg_le split_mult_pos_le)
     have mulprts: "a * b = (pprt a + nprt a) * (pprt b + nprt b)"
       by (simp flip: prts)
     show ?thesis
     proof (cases "0 \<le> a * b")
       case True
       then show ?thesis
-        apply (simp_all add: mulprts abs_prts)
-        using a
-        apply (auto simp add:
-          algebra_simps
-          iffD1[OF zero_le_iff_zero_nprt] iffD1[OF le_zero_iff_zero_pprt]
-          iffD1[OF le_zero_iff_pprt_id] iffD1[OF zero_le_iff_nprt_id])
-        apply(drule (1) mult_nonneg_nonpos[of a b], simp)
-        apply(drule (1) mult_nonneg_nonpos2[of b a], simp)
-        done
+        using a split_mult_neg_le by fastforce
     next
       case False
       with s have "a * b \<le> 0"
         by simp
       then show ?thesis
-        apply (simp_all add: mulprts abs_prts)
-        apply (insert a)
-        apply (auto simp add: algebra_simps)
-        apply(drule (1) mult_nonneg_nonneg[of a b],simp)
-        apply(drule (1) mult_nonpos_nonpos[of a b],simp)
-        done
+        using a split_mult_pos_le by fastforce
     qed
   qed
 qed
diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/Library/Word.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -14,8 +14,7 @@
 lemma signed_take_bit_decr_length_iff:
   \<open>signed_take_bit (LENGTH('a::len) - Suc 0) k = signed_take_bit (LENGTH('a) - Suc 0) l
     \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close>
-  by (cases \<open>LENGTH('a)\<close>)
-    (simp_all add: signed_take_bit_eq_iff_take_bit_eq)
+  by (simp add: signed_take_bit_eq_iff_take_bit_eq)
 
 
 subsection \<open>Fundamentals\<close>
@@ -42,19 +41,19 @@
 
 lift_definition plus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is \<open>(+)\<close>
-  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_add_cong)
 
 lift_definition minus_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is \<open>(-)\<close>
-  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
 
 lift_definition uminus_word :: \<open>'a word \<Rightarrow> 'a word\<close>
   is uminus
-  by (auto simp add: take_bit_eq_mod intro: mod_minus_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_minus_cong)
 
 lift_definition times_word :: \<open>'a word \<Rightarrow> 'a word \<Rightarrow> 'a word\<close>
   is \<open>(*)\<close>
-  by (auto simp add: take_bit_eq_mod intro: mod_mult_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_mult_cong)
 
 instance
   by (standard; transfer) (simp_all add: algebra_simps)
@@ -187,7 +186,7 @@
 lemma [code]:
   \<open>Word.the_int (- w) = (let k = Word.the_int w in if w = 0 then 0 else 2 ^ LENGTH('a) - k)\<close>
   for w :: \<open>'a::len word\<close>
-  by transfer (auto simp add: take_bit_eq_mod zmod_zminus1_eq_if)
+  by transfer (auto simp: take_bit_eq_mod zmod_zminus1_eq_if)
 
 lemma [code]:
   \<open>Word.the_int (v - w) = take_bit LENGTH('a) (Word.the_int v - Word.the_int w)\<close>
@@ -650,10 +649,10 @@
     have "k mod r = ((k mod r) div (l mod r) * (l mod r)
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: div_mult_mod_eq)
-    also have "... = (((k mod r) div (l mod r) * (l mod r)) mod r
+    also have "\<dots> = (((k mod r) div (l mod r) * (l mod r)) mod r
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: mod_add_left_eq)
-    also have "... = (((k mod r) div (l mod r) * l) mod r
+    also have "\<dots> = (((k mod r) div (l mod r) * l) mod r
       + (k mod r) mod (l mod r)) mod r"
       by (simp add: mod_mult_right_eq)
     finally have "k mod r = ((k mod r) div (l mod r) * l
@@ -695,7 +694,7 @@
 
 instance word :: (len) semiring_parity
   by (standard; transfer)
-    (auto simp add: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
+    (auto simp: mod_2_eq_odd take_bit_Suc elim: evenE dest: le_Suc_ex)
 
 lemma word_bit_induct [case_names zero even odd]:
   \<open>P a\<close> if word_zero: \<open>P 0\<close>
@@ -723,7 +722,7 @@
     with even.IH have \<open>P (of_nat n)\<close>
       by simp
     moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close>
-      by (auto simp add: word_greater_zero_iff l word_of_nat_eq_0_iff)
+      by (auto simp: word_greater_zero_iff l word_of_nat_eq_0_iff)
     moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - Suc 0)\<close>
       using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>]
       by (simp add: l take_bit_eq_mod)
@@ -774,7 +773,7 @@
         by simp
       moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
       with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
-        by (auto simp add: take_bit_Suc_from_most)
+        by (auto simp: take_bit_Suc_from_most)
       ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
       with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2)
@@ -792,12 +791,12 @@
         using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps)
       moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close>
       with \<open>LENGTH('a) = Suc n\<close> have \<open>take_bit LENGTH('a) k = take_bit n k\<close>
-        by (auto simp add: take_bit_Suc_from_most)
+        by (auto simp: take_bit_Suc_from_most)
       ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close>
         by (simp add: take_bit_eq_mod)
       with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2)
         = take_bit LENGTH('a) k\<close>
-        by (auto simp add: take_bit_Suc)
+        by (auto simp: take_bit_Suc)
     qed
     ultimately show ?thesis
       by simp
@@ -871,7 +870,7 @@
     for a :: \<open>'a word\<close> and m n :: nat
     apply transfer
     using drop_bit_eq_div [symmetric, where ?'a = int,of _ 1]
-    apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps)
+    apply (auto simp:  not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div simp del: power.simps)
     apply (simp add: drop_bit_take_bit)
     done
   show \<open>even (2 * a div 2 ^ Suc n) \<longleftrightarrow> even (a div 2 ^ n)\<close> if \<open>2 ^ Suc n \<noteq> (0::'a word)\<close>
@@ -885,7 +884,7 @@
 lemma bit_word_eqI:
   \<open>a = b\<close> if \<open>\<And>n. n < LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
   for a b :: \<open>'a::len word\<close>
-  using that by transfer (auto simp add: nat_less_le bit_eq_iff bit_take_bit_iff)
+  using that by transfer (auto simp: nat_less_le bit_eq_iff bit_take_bit_iff)
 
 lemma bit_imp_le_length:
   \<open>n < LENGTH('a)\<close> if \<open>bit w n\<close>
@@ -988,20 +987,16 @@
     by transfer (simp add: not_eq_complement)
   show \<open>v AND w = of_bool (odd v \<and> odd w) + 2 * (v div 2 AND w div 2)\<close>
     apply transfer
-    apply (rule bit_eqI)
-    apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
-    done
+    by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
   show \<open>v OR w = of_bool (odd v \<or> odd w) + 2 * (v div 2 OR w div 2)\<close>
     apply transfer
-    apply (rule bit_eqI)
-    apply (auto simp add: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
-    done
+    by (rule bit_eqI) (auto simp: even_bit_succ_iff bit_simps bit_0 simp flip: bit_Suc)
   show \<open>v XOR w = of_bool (odd v \<noteq> odd w) + 2 * (v div 2 XOR w div 2)\<close>
     apply transfer
     apply (rule bit_eqI)
     subgoal for k l n
       apply (cases n)
-       apply (auto simp add: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc)
+       apply (auto simp: even_bit_succ_iff bit_simps bit_0 even_xor_iff simp flip: bit_Suc)
       done
     done
   show \<open>mask n = 2 ^ n - (1 :: 'a word)\<close>
@@ -1173,14 +1168,14 @@
 lemma unsigned_drop_bit_eq:
   \<open>unsigned (drop_bit n w) = drop_bit n (take_bit LENGTH('b) (unsigned w))\<close>
   for w :: \<open>'b::len word\<close>
-  by (rule bit_eqI) (auto simp add: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq possible_bit_def dest: bit_imp_le_length)
+  by (rule bit_eqI) (auto simp: bit_unsigned_iff bit_take_bit_iff bit_drop_bit_eq Bit_Operations.bit_drop_bit_eq possible_bit_def dest: bit_imp_le_length)
 
 end
 
 lemma ucast_drop_bit_eq:
   \<open>ucast (drop_bit n w) = drop_bit n (ucast w :: 'b::len word)\<close>
   if \<open>LENGTH('a) \<le> LENGTH('b)\<close> for w :: \<open>'a::len word\<close>
-  by (rule bit_word_eqI) (use that in \<open>auto simp add: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)
+  by (rule bit_word_eqI) (use that in \<open>auto simp: bit_unsigned_iff bit_drop_bit_eq dest: bit_imp_le_length\<close>)
 
 context semiring_bit_operations
 begin
@@ -1260,7 +1255,7 @@
   \<open>bit (signed w) n \<longleftrightarrow> possible_bit TYPE('a) n \<and> bit w (min (LENGTH('b) - Suc 0) n)\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: bit)
-    (auto simp add: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
+    (auto simp: bit_of_int_iff Bit_Operations.bit_signed_take_bit_iff min_def)
 
 lemma signed_push_bit_eq:
   \<open>signed (push_bit n w) = signed_take_bit (LENGTH('b) - Suc 0) (push_bit n (signed w :: 'a))\<close>
@@ -1273,7 +1268,7 @@
   \<open>signed (take_bit n w) = (if n < LENGTH('b) then take_bit n (signed w) else signed w)\<close>
   for w :: \<open>'b::len word\<close>
   by (transfer fixing: take_bit; cases \<open>LENGTH('b)\<close>)
-    (auto simp add: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
+    (auto simp: Bit_Operations.signed_take_bit_take_bit Bit_Operations.take_bit_signed_take_bit take_bit_of_int min_def less_Suc_eq)
 
 context
   includes bit_operations_syntax
@@ -1318,7 +1313,7 @@
     by simp
   case False
   then show ?thesis
-    by transfer (auto simp add: signed_take_bit_eq intro: order_trans *)
+    by transfer (auto simp: signed_take_bit_eq intro: order_trans *)
 qed
 
 lemma sint_less:
@@ -1446,10 +1441,10 @@
   by simp
 
 lemma uint_0_iff: "uint x = 0 \<longleftrightarrow> x = 0"
-  by (auto simp add: unsigned_word_eqI)
+  by (auto simp: unsigned_word_eqI)
 
 lemma unat_0_iff: "unat x = 0 \<longleftrightarrow> x = 0"
-  by (auto simp add: unsigned_word_eqI)
+  by (auto simp: unsigned_word_eqI)
 
 lemma unat_0: "unat 0 = 0"
   by (fact unsigned_0)
@@ -1547,9 +1542,7 @@
 
 lemma mod_word_self [simp]:
   \<open>w mod w = 0\<close> for w :: \<open>'a::len word\<close>
-  apply (cases \<open>w = 0\<close>)
-  apply auto
-  using div_mult_mod_eq [of w w] by (simp add: div_word_self)
+  by (simp add: word_mod_def)
 
 lemma div_word_less:
   \<open>w div v = 0\<close> if \<open>w < v\<close> for w v :: \<open>'a::len word\<close>
@@ -1628,10 +1621,10 @@
   by transfer simp
 
 lift_definition word_succ :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x + 1"
-  by (auto simp add: take_bit_eq_mod intro: mod_add_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_add_cong)
 
 lift_definition word_pred :: "'a::len word \<Rightarrow> 'a word" is "\<lambda>x. x - 1"
-  by (auto simp add: take_bit_eq_mod intro: mod_diff_cong)
+  by (auto simp: take_bit_eq_mod intro: mod_diff_cong)
 
 lemma word_succ_alt [code]:
   "word_succ a = word_of_int (uint a + 1)"
@@ -1670,7 +1663,7 @@
     by simp
   have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
     using that by transfer
-      (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *)
+      (auto simp: take_bit_eq_0_iff take_bit_eq_mod *)
   moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
     by transfer simp
   then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
@@ -1712,7 +1705,7 @@
   using signed_take_bit_decr_length_iff by force+
 
 lemma signed_linorder: \<open>class.linorder word_sle word_sless\<close>
-  by (standard; transfer) (auto simp add: signed_take_bit_decr_length_iff)
+  by (standard; transfer) (auto simp: signed_take_bit_decr_length_iff)
 
 interpretation signed: linorder word_sle word_sless
   by (fact signed_linorder)
@@ -1751,7 +1744,7 @@
   by transfer (simp add: nat_le_eq_zle)
 
 lemma word_less_nat_alt: "a < b \<longleftrightarrow> unat a < unat b"
-  by transfer (auto simp add: less_le [of 0])
+  by transfer (auto simp: less_le [of 0])
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
 
@@ -1761,7 +1754,7 @@
   assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
   have "wf (measure unat)" ..
   moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
-    by (auto simp add: word_less_nat_alt)
+    by (auto simp: word_less_nat_alt)
   ultimately have "wf {(a, b :: ('a::len) word). a < b}"
     by (rule wf_subset)
   then show "P a" using *
@@ -1809,7 +1802,7 @@
 lemma bit_sint_iff:
   \<open>bit (sint w) n \<longleftrightarrow> n \<ge> LENGTH('a) \<and> bit w (LENGTH('a) - 1) \<or> bit w n\<close>
   for w :: \<open>'a::len word\<close>
-  by transfer (auto simp add: bit_signed_take_bit_iff min_def le_less not_less)
+  by transfer (auto simp: bit_signed_take_bit_iff min_def le_less not_less)
 
 lemma bit_word_ucast_iff:
   \<open>bit (ucast w :: 'b::len word) n \<longleftrightarrow> n < LENGTH('a) \<and> n < LENGTH('b) \<and> bit w n\<close>
@@ -1820,7 +1813,7 @@
   \<open>bit (scast w :: 'b::len word) n \<longleftrightarrow>
     n < LENGTH('b) \<and> (bit w n \<or> LENGTH('a) \<le> n \<and> bit w (LENGTH('a) - Suc 0))\<close>
   for w :: \<open>'a::len word\<close>
-  by transfer (auto simp add: bit_signed_take_bit_iff le_less min_def)
+  by transfer (auto simp: bit_signed_take_bit_iff le_less min_def)
 
 lemma bit_word_iff_drop_bit_and [code]:
   \<open>bit a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close> for a :: \<open>'a::len word\<close>
@@ -1856,7 +1849,7 @@
   moreover have \<open>bit (r div 2) = bit r \<circ> Suc\<close> for r :: int
     by (simp add: fun_eq_iff bit_Suc)
   moreover from Suc.prems have \<open>even k \<longleftrightarrow> even l\<close>
-    by (auto simp add: take_bit_Suc elim!: evenE oddE) arith+
+    by (auto simp: take_bit_Suc elim!: evenE oddE) arith+
   ultimately show ?case
     by (simp only: map_Suc_upt upt_conv_Cons flip: list.map_comp) (simp add: bit_0)
 qed
@@ -1886,10 +1879,10 @@
       numeral_inc numeral_eq_Suc flip: mult_2)
   have even: \<open>take_bit (Suc q) (2 * w) = 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
     by (rule bit_word_eqI)
-      (auto simp add: bit_take_bit_iff bit_double_iff)
+      (auto simp: bit_take_bit_iff bit_double_iff)
   have odd: \<open>take_bit (Suc q) (1 + 2 * w) = 1 + 2 * take_bit q w\<close> for w :: \<open>'a::len word\<close>
     by (rule bit_eqI)
-      (auto simp add: bit_take_bit_iff bit_double_iff even_bit_succ_iff)
+      (auto simp: bit_take_bit_iff bit_double_iff even_bit_succ_iff)
   show ?P
     using even [of w] by (simp add: num)
   show ?Q
@@ -1912,8 +1905,8 @@
   \<open>bit (signed_drop_bit m w) n \<longleftrightarrow> bit w (if LENGTH('a) - m \<le> n \<and> n < LENGTH('a) then LENGTH('a) - 1 else m + n)\<close>
   for w :: \<open>'a::len word\<close>
   apply transfer
-  apply (auto simp add: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
-   apply (metis add.commute le_antisym less_diff_conv less_eq_decr_length_iff)
+  apply (auto simp: bit_drop_bit_eq bit_signed_take_bit_iff not_le min_def)
+   apply (metis Suc_pred add.commute le_less_Suc_eq len_gt_0 less_diff_conv)
   apply (metis le_antisym less_eq_decr_length_iff)
   done
 
@@ -1940,7 +1933,7 @@
 next
   case (Suc n)
   then show ?thesis
-    by (force simp add: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI)
+    by (force simp: bit_signed_drop_bit_iff not_le less_diff_conv ac_simps intro!: bit_word_eqI)
 qed
 
 lemma signed_drop_bit_0 [simp]:
@@ -1954,7 +1947,7 @@
   then show ?thesis
     apply simp
     apply (rule bit_eqI)
-    by (auto simp add: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
+    by (auto simp: bit_sint_iff bit_drop_bit_eq bit_signed_drop_bit_iff dest: bit_imp_le_length)
 qed auto
 
 
@@ -1963,18 +1956,18 @@
 lemma set_bit_eq_idem_iff:
   \<open>Bit_Operations.set_bit n w = w \<longleftrightarrow> bit w n \<or> n \<ge> LENGTH('a)\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: bit_eq_iff) (auto simp add: bit_simps not_le)
+  by (simp add: bit_eq_iff) (auto simp: bit_simps not_le)
 
 lemma unset_bit_eq_idem_iff:
   \<open>unset_bit n w = w \<longleftrightarrow> bit w n \<longrightarrow> n \<ge> LENGTH('a)\<close>
   for w :: \<open>'a::len word\<close>
-  by (simp add: bit_eq_iff) (auto simp add: bit_simps dest: bit_imp_le_length)
+  by (simp add: bit_eq_iff) (auto simp: bit_simps dest: bit_imp_le_length)
 
 lemma flip_bit_eq_idem_iff:
   \<open>flip_bit n w = w \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
   for w :: \<open>'a::len word\<close>
   using linorder_le_less_linear
-  by (simp add: bit_eq_iff) (auto simp add: bit_simps)
+  by (simp add: bit_eq_iff) (auto simp: bit_simps)
 
 
 subsection \<open>Rotation\<close>
@@ -2054,7 +2047,7 @@
     n < LENGTH('a) \<and> bit k ((n + q) mod LENGTH('a))\<close>
     using \<open>q < LENGTH('a)\<close>
     by (cases \<open>q + n \<ge> LENGTH('a)\<close>)
-     (auto simp add: bit_concat_bit_iff bit_drop_bit_eq
+     (auto simp: bit_concat_bit_iff bit_drop_bit_eq
         bit_take_bit_iff le_mod_geq ac_simps)
   ultimately show \<open>n < LENGTH('a) \<and>
     bit (concat_bit (LENGTH('a) - m mod LENGTH('a))
@@ -2092,7 +2085,7 @@
     n < LENGTH('a) \<and> bit l ((n + m) mod LENGTH('a))\<close>
     using \<open>m < LENGTH('a)\<close>
     by (cases \<open>m + n \<ge> LENGTH('a)\<close>)
-     (auto simp add: bit_concat_bit_iff bit_drop_bit_eq
+     (auto simp: bit_concat_bit_iff bit_drop_bit_eq
         bit_take_bit_iff nat_less_iff not_le not_less ac_simps
         le_diff_conv le_mod_geq)
   ultimately show \<open>n < LENGTH('a)
@@ -2280,12 +2273,12 @@
 lemma word_int_split:
   "P (word_int_case f x) =
     (\<forall>i. x = (word_of_int i :: 'b::len word) \<and> 0 \<le> i \<and> i < 2 ^ LENGTH('b) \<longrightarrow> P (f i))"
-  by transfer (auto simp add: take_bit_eq_mod)
+  by transfer (auto simp: take_bit_eq_mod)
 
 lemma word_int_split_asm:
   "P (word_int_case f x) =
     (\<nexists>n. x = (word_of_int n :: 'b::len word) \<and> 0 \<le> n \<and> n < 2 ^ LENGTH('b::len) \<and> \<not> P (f n))"
-  by transfer (auto simp add: take_bit_eq_mod)
+  by transfer (auto simp: take_bit_eq_mod)
 
 lemma uint_range_size: "0 \<le> uint w \<and> uint w < 2 ^ size w"
   by transfer simp
@@ -2368,7 +2361,7 @@
 
 lemma ucast_mask_eq:
   \<open>ucast (mask n :: 'b word) = mask (min LENGTH('b::len) n)\<close>
-  by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff)
+  by (simp add: bit_eq_iff) (auto simp: bit_mask_iff bit_ucast_iff)
 
 \<comment> \<open>literal u(s)cast\<close>
 lemma ucast_bintr [simp]:
@@ -2613,8 +2606,8 @@
   \<open>signed_drop_bit n (1 :: 'a::len word) = of_bool (LENGTH('a) = 1 \<or> n = 0)\<close>
   apply (transfer fixing: n)
   apply (cases \<open>LENGTH('a)\<close>)
-   apply (auto simp add: take_bit_signed_take_bit)
-  apply (auto simp add: take_bit_drop_bit gr0_conv_Suc simp flip: take_bit_eq_self_iff_drop_bit_eq_0)
+   apply (auto simp: take_bit_signed_take_bit)
+  apply (auto simp: take_bit_drop_bit gr0_conv_Suc simp flip: take_bit_eq_self_iff_drop_bit_eq_0)
   done
 
 lemma take_bit_word_beyond_length_eq:
@@ -2816,7 +2809,7 @@
       by linarith
   qed
   ultimately have \<open>unat w = unat v * unat (word_of_nat n :: 'a word)\<close>
-    by (auto simp add: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym)
+    by (auto simp: take_bit_nat_eq_self_iff unsigned_of_nat intro: sym)
   with that show thesis .
 qed
 
@@ -2863,7 +2856,7 @@
 
 lemma udvd_nat_alt:
   \<open>a udvd b \<longleftrightarrow> (\<exists>n. unat b = n * unat a)\<close>
-  by (auto simp add: udvd_iff_dvd)
+  by (auto simp: udvd_iff_dvd)
 
 lemma udvd_unfold_int:
   \<open>a udvd b \<longleftrightarrow> (\<exists>n\<ge>0. uint b = n * uint a)\<close>
@@ -2921,8 +2914,7 @@
   unfolding uint_word_ariths by (simp add: zmod_le_nonneg_dividend) 
 
 lemma uint_sub_ge: "uint (x - y) \<ge> uint x - uint y"
-  unfolding uint_word_ariths
-  by (simp flip: take_bit_eq_mod add: take_bit_int_greater_eq_self_iff)
+  by (smt (verit, ccfv_SIG) uint_nonnegative uint_sub_lem)
 
 lemma int_mod_ge: \<open>a \<le> a mod n\<close> if \<open>a < n\<close> \<open>0 < n\<close>
   for a n :: int
@@ -2932,8 +2924,7 @@
   "\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
     (x + y) mod z = (if x + y < z then x + y else x + y - z)"
   for x y z :: int
-  apply (simp add: not_less)
-  by (metis (no_types) add_strict_mono diff_ge_0_iff_ge diff_less_eq minus_mod_self2 mod_pos_pos_trivial)
+  by (smt (verit, best) minus_mod_self2 mod_pos_pos_trivial)
 
 lemma uint_plus_if':
   "uint (a + b) =
@@ -2946,7 +2937,7 @@
   "\<lbrakk>x < z; y < z; 0 \<le> y; 0 \<le> x; 0 \<le> z\<rbrakk> \<Longrightarrow>
     (x - y) mod z = (if y \<le> x then x - y else x - y + z)"
   for x y z :: int
-  using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp add: not_le)
+  using mod_pos_pos_trivial [of "x - y + z" z] by (auto simp: not_le)
 
 lemma uint_sub_if':
   "uint (a - b) =
@@ -2962,11 +2953,11 @@
 
 lemma unat_split: "P (unat x) \<longleftrightarrow> (\<forall>n. of_nat n = x \<and> n < 2^LENGTH('a) \<longrightarrow> P n)"
   for x :: "'a::len word"
-  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+  by (auto simp: unsigned_of_nat take_bit_nat_eq_self)
 
 lemma unat_split_asm: "P (unat x) \<longleftrightarrow> (\<nexists>n. of_nat n = x \<and> n < 2^LENGTH('a) \<and> \<not> P n)"
   for x :: "'a::len word"
-  by (auto simp add: unsigned_of_nat take_bit_nat_eq_self)
+  using unat_split by auto
 
 lemma un_ui_le:
   \<open>unat a \<le> unat b \<longleftrightarrow> uint a \<le> uint b\<close>
@@ -2977,10 +2968,9 @@
     (if unat a + unat b < 2 ^ LENGTH('a)
     then unat a + unat b
     else unat a + unat b - 2 ^ LENGTH('a))\<close> for a b :: \<open>'a::len word\<close>
-  apply (auto simp add: not_less le_iff_add)
+  apply (auto simp: not_less le_iff_add)
    apply (metis (mono_tags, lifting) of_nat_add of_nat_unat take_bit_nat_eq_self_iff unsigned_less unsigned_of_nat unsigned_word_eqI)
-  apply (smt (verit, ccfv_SIG) dbl_simps(3) dbl_simps(5) numerals(1) of_nat_0_le_iff of_nat_add of_nat_eq_iff of_nat_numeral of_nat_power of_nat_unat uint_plus_if' unsigned_1)
-  done
+  by (smt (verit, ccfv_SIG) numeral_Bit0 numerals(1) of_nat_0_le_iff of_nat_1 of_nat_add of_nat_eq_iff of_nat_power of_nat_unat uint_plus_if')
 
 lemma unat_sub_if_size:
   "unat (x - y) =
@@ -2991,9 +2981,9 @@
   { assume xy: "\<not> uint y \<le> uint x"
     have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x + 2 ^ LENGTH('a) - uint y)"
       by simp
-    also have "... = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
+    also have "\<dots> = nat (uint x + 2 ^ LENGTH('a)) - nat (uint y)"
       by (simp add: nat_diff_distrib')
-    also have "... = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
+    also have "\<dots> = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)"
       by (metis nat_add_distrib nat_eq_numeral_power_cancel_iff order_less_imp_le unsigned_0 unsigned_greater_eq unsigned_less)
     finally have "nat (uint x - uint y + 2 ^ LENGTH('a)) = nat (uint x) + 2 ^ LENGTH('a) - nat (uint y)" .
   }
@@ -3006,12 +2996,12 @@
 lemma uint_split:
   "P (uint x) = (\<forall>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<longrightarrow> P i)"
   for x :: "'a::len word"
-  by transfer (auto simp add: take_bit_eq_mod)
+  by transfer (auto simp: take_bit_eq_mod)
 
 lemma uint_split_asm:
   "P (uint x) = (\<nexists>i. word_of_int i = x \<and> 0 \<le> i \<and> i < 2^LENGTH('a) \<and> \<not> P i)"
   for x :: "'a::len word"
-  by (auto simp add: unsigned_of_int take_bit_int_eq_self)
+  by (auto simp: unsigned_of_int take_bit_int_eq_self)
 
 
 subsection \<open>Some proof tool support\<close>
@@ -3111,13 +3101,13 @@
 
 lemma no_plus_overflow_uint_size: "x \<le> x + y \<longleftrightarrow> uint x + uint y < 2 ^ size x"
   for x y :: "'a::len word"
-  by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
+  by (auto simp: word_size word_le_def uint_add_lem uint_sub_lem)
 
 lemmas no_olen_add = no_plus_overflow_uint_size [unfolded word_size]
 
 lemma no_ulen_sub: "x \<ge> x - y \<longleftrightarrow> uint y \<le> uint x"
   for x y :: "'a::len word"
-  by (auto simp add: word_size word_le_def uint_add_lem uint_sub_lem)
+  by (auto simp: word_size word_le_def uint_add_lem uint_sub_lem)
 
 lemma no_olen_add': "x \<le> y + x \<longleftrightarrow> uint y + uint x < 2 ^ LENGTH('a)"
   for x y :: "'a::len word"
@@ -3328,7 +3318,7 @@
   by (cases k) auto
 
 lemma of_nat_neq_0: "0 < k \<Longrightarrow> k < 2 ^ LENGTH('a::len) \<Longrightarrow> of_nat k \<noteq> (0 :: 'a word)"
-  by (auto simp add : of_nat_0)
+  by (auto simp : of_nat_0)
 
 lemma Abs_fnat_hom_add: "of_nat a + of_nat b = of_nat (a + b)"
   by simp
@@ -3496,12 +3486,12 @@
 
 lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len)}\<close>
   apply transfer
-  apply (auto simp add: image_iff)
+  apply (auto simp: image_iff)
   apply (metis take_bit_int_eq_self_iff)
   done
 
 lemma UNIV_eq: \<open>(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len)}\<close>
-  by (auto simp add: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
+  by (auto simp: image_iff) (metis atLeastLessThan_iff linorder_not_le uint_split)
 
 lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len)"
   by (simp add: UNIV_eq card_image inj_on_word_of_int)
@@ -3720,7 +3710,7 @@
 
 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)
+    (auto simp: 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)
@@ -3889,7 +3879,7 @@
 
 lemma and_mask_wi':
   "word_of_int i AND mask n = (word_of_int (take_bit (min LENGTH('a) n) i) :: 'a::len word)"
-  by (auto simp add: and_mask_wi min_def wi_bintr)
+  by (auto simp: and_mask_wi min_def wi_bintr)
 
 lemma and_mask_no: "numeral i AND mask n = word_of_int (take_bit n (numeral i))"
   unfolding word_numeral_alt by (rule and_mask_wi)
@@ -3975,7 +3965,7 @@
   \<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 not_less not_le ac_simps
+  by (auto simp: slice1_def bit_ucast_iff bit_drop_bit_eq bit_push_bit_iff not_less not_le ac_simps
     dest: bit_imp_le_length)
 
 definition slice :: \<open>nat \<Rightarrow> 'a::len word \<Rightarrow> 'b::len word\<close>
@@ -4072,7 +4062,7 @@
 
 lemma word_cat_split_alt: "\<lbrakk>size w \<le> size u + size v; word_split w = (u,v)\<rbrakk> \<Longrightarrow> word_cat u v = w"
   unfolding word_split_def
-  by (rule bit_word_eqI) (auto simp add: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq)
+  by (rule bit_word_eqI) (auto simp: bit_word_cat_iff not_less word_size bit_ucast_iff bit_drop_bit_eq)
 
 lemmas word_cat_split_size = sym [THEN [2] word_cat_split_alt [symmetric]]
 
@@ -4091,7 +4081,7 @@
     show "bit u n = bit ((slice LENGTH('b) w)::'a word) n" if "n < LENGTH('a)" for n
       using assms bit_imp_le_length
       unfolding word_split_def bit_slice_iff
-      by (fastforce simp add: \<section> ac_simps word_size bit_ucast_iff bit_drop_bit_eq)
+      by (fastforce simp: \<section> ac_simps word_size bit_ucast_iff bit_drop_bit_eq)
   qed
   show "v = slice 0 w"
     by (metis Pair_inject assms ucast_slice word_split_bin')
@@ -4100,13 +4090,13 @@
 
 lemma slice_cat1 [OF refl]:
   "\<lbrakk>wc = word_cat a b; size a + size b \<le> size wc\<rbrakk> \<Longrightarrow> slice (size b) wc = a"
-  by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
+  by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
 
 lemmas slice_cat2 = trans [OF slice_id word_cat_id]
 
 lemma cat_slices:
   "\<lbrakk>a = slice n c; b = slice 0 c; n = size b; size c \<le> size a + size b\<rbrakk> \<Longrightarrow> word_cat a b = c"
-  by (rule bit_word_eqI) (auto simp add: bit_slice_iff bit_word_cat_iff word_size)
+  by (rule bit_word_eqI) (auto simp: bit_slice_iff bit_word_cat_iff word_size)
 
 lemma word_split_cat_alt:
   assumes "w = word_cat u v" and size: "size u + size v \<le> size w"
@@ -4114,7 +4104,7 @@
 proof -
   have "ucast ((drop_bit LENGTH('c) (word_cat u v))::'a word) = u" "ucast ((word_cat u v)::'a word) = v"
     using assms
-    by (auto simp add: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI)
+    by (auto simp: word_size bit_ucast_iff bit_drop_bit_eq bit_word_cat_iff intro: bit_eqI)
   then show ?thesis
     by (simp add: assms(1) word_split_bin')
 qed
@@ -4160,7 +4150,7 @@
 proof (rule bit_word_eqI)
   show "bit (word_rotr k (word_rotl k v)) n = bit v n" if "n < LENGTH('a)" for n
     using that
-    by (auto simp add: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
+    by (auto simp: word_rot_lem word_rotl_eq_word_rotr word_rotr_word_rotr_eq bit_word_rotr_iff algebra_simps split: nat_diff_split)
 qed
 
 lemma word_rot_gal:
@@ -4184,8 +4174,7 @@
     apply (simp add: mod_simps)
     done
   then have \<open>LENGTH('a) - Suc ((m + n) mod LENGTH('a)) =
-    (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod
-    LENGTH('a)\<close>
+            (LENGTH('a) + LENGTH('a) - Suc (m + n mod LENGTH('a))) mod LENGTH('a)\<close>
     by simp
   with \<open>m < LENGTH('a)\<close> show \<open>bit ?lhs m \<longleftrightarrow> bit ?rhs m\<close>
     by (simp add: bit_simps)
@@ -4238,7 +4227,7 @@
   "word_rotr n (x OR y) = word_rotr n x OR word_rotr n y"
   "word_rotl n (x XOR y) = word_rotl n x XOR word_rotl n y"
   "word_rotr n (x XOR y) = word_rotr n x XOR word_rotr n y"
-  by (rule bit_word_eqI, auto simp add: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
+  by (rule bit_word_eqI, auto simp: bit_word_rotl_iff bit_word_rotr_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff algebra_simps not_le)+
 
 end
 
@@ -4368,7 +4357,7 @@
 
 lemma word_le_less_eq: "x \<le> y \<longleftrightarrow> x = y \<or> x < y"
   for x y :: "'z::len word"
-  by (auto simp add: order_class.le_less)
+  by (auto simp: order_class.le_less)
 
 lemma mod_plus_cong:
   fixes b b' :: int
@@ -4491,7 +4480,7 @@
   by (induct n) auto
 
 lemma word_rec_id_eq: "(\<And>m. m < n \<Longrightarrow> f m = id) \<Longrightarrow> word_rec z f n = z"
-  by (induction n) (auto simp add: unatSuc unat_arith_simps(2))
+  by (induction n) (auto simp: unatSuc unat_arith_simps(2))
 
 lemma word_rec_max:
   assumes "\<forall>m\<ge>n. m \<noteq> - 1 \<longrightarrow> f m = id"
@@ -4502,7 +4491,7 @@
     by (metis (mono_tags, lifting) add.commute add_diff_cancel_left' comp_apply less_le olen_add_eqv plus_minus_no_overflow word_n1_ge)
   have "word_rec z f (- 1) = word_rec (word_rec z f (- 1 - (- 1 - n))) (f \<circ> (+) (- 1 - (- 1 - n))) (- 1 - n)"
     by (meson word_n1_ge word_rec_twice)
-  also have "... = word_rec z f n"
+  also have "\<dots> = word_rec z f n"
     by (metis (no_types, lifting) \<section> diff_add_cancel minus_diff_eq uminus_add_conv_diff word_rec_id_eq)
   finally show ?thesis .
 qed
diff -r fe7ffe7eb265 -r 623d46973cbe src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -11,7 +11,7 @@
 section \<open>Test of Locale Interpretation\<close>
 
 theory LocaleTest2
-imports Main
+imports Main 
 begin
 
 section \<open>Interpretation of Defined Concepts\<close>
@@ -482,33 +482,31 @@
 
 thm int.circular
 lemma "\<lbrakk> (x::int) \<le> y; y \<le> z; z \<le> x\<rbrakk> \<Longrightarrow> x = y \<and> y = z"
-  apply (rule int.circular) apply assumption apply assumption apply assumption done
+  by simp
+
 thm int.abs_test
 lemma "((<) :: [int, int] => bool) = (<)"
-  apply (rule int.abs_test) done
+  by (rule int.abs_test)
 
 interpretation int: dlat "(<=) :: [int, int] => bool"
   rewrites meet_eq: "dlat.meet (<=) (x::int) y = min x y"
     and join_eq: "dlat.join (<=) (x::int) y = max x y"
 proof -
   show "dlat ((<=) :: [int, int] => bool)"
-    apply unfold_locales
-    apply (unfold int.is_inf_def int.is_sup_def)
-    apply arith+
-    done
+  proof unfold_locales
+    fix x y :: int
+    show "\<exists>inf. int.is_inf x y inf"
+      using int.is_inf_def by fastforce
+    show "\<exists>sup. int.is_sup x y sup"
+      using int.is_sup_def by fastforce
+  qed
   then interpret int: dlat "(<=) :: [int, int] => bool" .
   txt \<open>Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation.\<close>
   show "dlat.meet (<=) (x::int) y = min x y"
-    apply (unfold int.meet_def)
-    apply (rule the_equality)
-    apply (unfold int.is_inf_def)
-    by auto
+    by (smt (verit, best) int.meet_related int.meet_related2)
   show "dlat.join (<=) (x::int) y = max x y"
-    apply (unfold int.join_def)
-    apply (rule the_equality)
-    apply (unfold int.is_sup_def)
-    by auto
+    by (smt (verit, best) int.join_related int.join_related2)
 qed
 
 interpretation int: dlo "(<=) :: [int, int] => bool"
@@ -533,9 +531,7 @@
   then interpret nat: dpo "(<=) :: [nat, nat] => bool" .
     txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
   show "dpo.less (<=) (x::nat) y = (x < y)"
-    apply (unfold nat.less_def)
-    apply auto
-    done
+    by (simp add: nat.less_def nat_less_le)
 qed
 
 interpretation nat: dlat "(<=) :: [nat, nat] => bool"
@@ -543,23 +539,20 @@
     and "dlat.join (<=) (x::nat) y = max x y"
 proof -
   show "dlat ((<=) :: [nat, nat] => bool)"
-    apply unfold_locales
-    apply (unfold nat.is_inf_def nat.is_sup_def)
-    apply arith+
-    done
+  proof
+    fix x y :: nat
+    show "\<exists>inf. nat.is_inf x y inf"
+      by (metis nat.is_inf_def nle_le)
+    show "\<exists>sup. nat.is_sup x y sup"
+      by (metis nat.is_sup_def nle_le)
+  qed
   then interpret nat: dlat "(<=) :: [nat, nat] => bool" .
   txt \<open>Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation.\<close>
   show "dlat.meet (<=) (x::nat) y = min x y"
-    apply (unfold nat.meet_def)
-    apply (rule the_equality)
-    apply (unfold nat.is_inf_def)
-    by auto
+    by (metis min_def nat.meet_connection nat.meet_connection2 nle_le)
   show "dlat.join (<=) (x::nat) y = max x y"
-    apply (unfold nat.join_def)
-    apply (rule the_equality)
-    apply (unfold nat.is_sup_def)
-    by auto
+    by (metis max_def nat.join_connection2 nat.join_related2 nle_le)
 qed
 
 interpretation nat: dlo "(<=) :: [nat, nat] => bool"
@@ -584,9 +577,8 @@
   then interpret nat_dvd: dpo "(dvd) :: [nat, nat] => bool" .
     txt \<open>Gives interpreted version of \<open>less_def\<close> (without condition).\<close>
   show "dpo.less (dvd) (x::nat) y = (x dvd y & x ~= y)"
-    apply (unfold nat_dvd.less_def)
-    apply auto
-    done
+    unfolding nat_dvd.less_def
+    by auto
 qed
 
 interpretation nat_dvd: dlat "(dvd) :: [nat, nat] => bool"
@@ -594,36 +586,33 @@
     and "dlat.join (dvd) (x::nat) y = lcm x y"
 proof -
   show "dlat ((dvd) :: [nat, nat] => bool)"
-    apply unfold_locales
-    apply (unfold nat_dvd.is_inf_def nat_dvd.is_sup_def)
-    apply (rule_tac x = "gcd x y" in exI)
-    apply auto [1]
-    apply (rule_tac x = "lcm x y" in exI)
-    apply (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
-    done
+  proof
+    fix x y :: nat
+    show "\<exists>inf. nat_dvd.is_inf x y inf"
+      unfolding nat_dvd.is_inf_def
+      by (force simp: intro: exI [where x = "gcd x y"])
+    show "\<exists>sup. nat_dvd.is_sup x y sup"
+      unfolding nat_dvd.is_sup_def
+      by (force simp: intro: exI [where x = "lcm x y"])
+  qed
   then interpret nat_dvd: dlat "(dvd) :: [nat, nat] => bool" .
   txt \<open>Interpretation to ease use of definitions, which are
     conditional in general but unconditional after interpretation.\<close>
   show "dlat.meet (dvd) (x::nat) y = gcd x y"
-    apply (unfold nat_dvd.meet_def)
-    apply (rule the_equality)
-    apply (unfold nat_dvd.is_inf_def)
-    by auto
+    by (meson gcd_unique_nat nat_dvd.meetI)
   show "dlat.join (dvd) (x::nat) y = lcm x y"
-    apply (unfold nat_dvd.join_def)
-    apply (rule the_equality)
-    apply (unfold nat_dvd.is_sup_def)
-    by (auto intro: dvd_lcm1 dvd_lcm2 lcm_least)
+    by (simp add: nat_dvd.joinI)
 qed
 
 text \<open>Interpreted theorems from the locales, involving defined terms.\<close>
 
 thm nat_dvd.less_def text \<open>from dpo\<close>
-lemma "((x::nat) dvd y & x ~= y) = (x dvd y & x ~= y)"
-  apply (rule nat_dvd.less_def) done
+lemma "((x::nat) dvd y \<and> x \<noteq> y) = (x dvd y \<and> x \<noteq> y)"
+  by simp
+
 thm nat_dvd.meet_left text \<open>from dlat\<close>
 lemma "gcd x y dvd (x::nat)"
-  apply (rule nat_dvd.meet_left) done
+  by blast
 
 
 subsection \<open>Group example with defined operations \<open>inv\<close> and \<open>unit\<close>\<close>
@@ -670,19 +659,11 @@
 
 lemma unit_l_inv:
   "unit x ==> inv x ** x = one"
-  apply (simp add: unit_def inv_def) apply (erule exE)
-  apply (rule theI2, fast)
-  apply (rule inv_unique)
-  apply fast+
-  done
+  by (smt (verit, ccfv_threshold) inv_unique local.inv_def theI' unit_def)
 
 lemma unit_r_inv:
   "unit x ==> x ** inv x = one"
-  apply (simp add: unit_def inv_def) apply (erule exE)
-  apply (rule theI2, fast)
-  apply (rule inv_unique)
-  apply fast+
-  done
+  by (metis inv_unique unit_l_inv unit_r_inv_ex)
 
 lemma unit_inv_unit [intro, simp]:
   "unit x ==> unit (inv x)"
@@ -801,15 +782,10 @@
 
 lemma inv_comm:
   "x ** y = one ==> y ** x = one"
-  by (rule unit_inv_comm) auto
+  using unit unit_inv_comm by blast
 
-lemma inv_equality:
-     "y ** x = one ==> inv x = y"
-  apply (simp add: inv_def)
-  apply (rule the_equality)
-   apply (simp add: inv_comm [of y x])
-  apply (rule r_cancel [THEN iffD1], auto)
-  done
+lemma inv_equality: "y ** x = one \<Longrightarrow> inv x = y"
+  by (metis assoc r_inv r_one)
 
 end
 
@@ -843,45 +819,20 @@
 (*
   from this interpret Dmonoid "(o)" "id :: 'a => 'a" .
 *)
+  have "\<And>y. \<lbrakk>f \<circ> y = id; y \<circ> f = id\<rbrakk> \<Longrightarrow> bij f"
+    using o_bij by auto
+  moreover have "bij f \<Longrightarrow> \<exists>y. f \<circ> y = id \<and> y \<circ> f = id"
+    by (meson bij_betw_def inv_o_cancel surj_iff)
+    ultimately
   show "Dmonoid.unit (o) (id :: 'a => 'a) f = bij f"
-    apply (unfold Dmonoid.unit_def [OF Dmonoid])
-    apply rule apply clarify
-  proof -
-    fix f g
-    assume id1: "f o g = id" and id2: "g o f = id"
-    show "bij f"
-    proof (rule bijI)
-      show "inj f"
-      proof (rule inj_onI)
-        fix x y
-        assume "f x = f y"
-        then have "(g o f) x = (g o f) y" by simp
-        with id2 show "x = y" by simp
-      qed
-    next
-      show "surj f"
-      proof (rule surjI)
-        fix x
-        from id1 have "(f o g) x = x" by simp
-        then show "f (g x) = x" by simp
-      qed
-    qed
-  next
-    fix f
-    assume bij: "bij f"
-    then
-    have inv: "f o Hilbert_Choice.inv f = id & Hilbert_Choice.inv f o f = id"
-      by (simp add: bij_def surj_iff inj_iff)
-    show "\<exists>g. f \<circ> g = id \<and> g \<circ> f = id" by rule (rule inv)
-  qed
+    by (metis Dmonoid Dmonoid.unit_def)
 qed
 
 thm Dmonoid.unit_def Dfun.unit_def
 
 thm Dmonoid.inv_inj_on_unit Dfun.inv_inj_on_unit
 
-lemma unit_id:
-  "(f :: unit => unit) = id"
+lemma unit_id: "(f :: unit => unit) = id"
   by rule simp
 
 interpretation Dfun: Dgrp "(o)" "id :: unit => unit"
@@ -891,20 +842,14 @@
   note Dmonoid = this
 
   show "Dgrp (o) (id :: unit => unit)"
-apply unfold_locales
-apply (unfold Dmonoid.unit_def [OF Dmonoid])
-apply (insert unit_id)
-apply simp
-done
+  proof
+    fix x :: "unit \<Rightarrow> unit"
+    show "Dmonoid.unit (\<circ>) id x"
+      by (simp add: Dmonoid Dmonoid.unit_def unit_id)
+  qed
   show "Dmonoid.inv (o) id f = inv (f :: unit \<Rightarrow> unit)"
-apply (unfold Dmonoid.inv_def [OF Dmonoid])
-apply (insert unit_id)
-apply simp
-apply (rule the_equality)
-apply rule
-apply rule
-apply simp
-done
+    unfolding Dmonoid.inv_def [OF Dmonoid]
+    by force
 qed
 
 thm Dfun.unit_l_inv Dfun.l_inv
diff -r fe7ffe7eb265 -r 623d46973cbe src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Sun Aug 25 21:27:25 2024 +0100
+++ b/src/ZF/ex/misc.thy	Mon Aug 26 21:59:35 2024 +0100
@@ -9,7 +9,6 @@
 
 theory misc imports ZF begin
 
-
 subsection\<open>Various Small Problems\<close>
 
 text\<open>The singleton problems are much harder in HOL.\<close>