
diff -r 646cd337bb08 -r 0f9cd1a5edbe src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Apr 10 11:32:48 2024 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Apr 12 09:58:32 2024 +0100
@@ -559,10 +559,7 @@
 
 lemma mset_subset_eq_exists_conv: "(A::'a multiset) \<subseteq># B \<longleftrightarrow> (\<exists>C. B = A + C)"
   unfolding subseteq_mset_def
-  apply (rule iffI)
-   apply (rule exI [where x = "B - A"])
-   apply (auto intro: multiset_eq_iff [THEN iffD2])
-  done
+  by (metis add_diff_cancel_left' count_diff count_union le_Suc_ex le_add_same_cancel1 multiset_eq_iff zero_le)
 
 interpretation subset_mset: ordered_cancel_comm_monoid_diff "(+)" 0 "(\<subseteq>#)" "(\<subset>#)" "(-)"
   by standard (simp, fact mset_subset_eq_exists_conv)
@@ -629,14 +626,18 @@
   by (metis mset_subset_eqD subsetI)
 
 lemma mset_subset_eq_insertD:
-  "add_mset x A \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
-apply (rule conjI)
- apply (simp add: mset_subset_eqD)
- apply (clarsimp simp: subset_mset_def subseteq_mset_def)
- apply safe
-  apply (erule_tac x = a in allE)
-  apply (auto split: if_split_asm)
-done
+  assumes "add_mset x A \<subseteq># B"
+  shows "x \<in># B \<and> A \<subset># B"
+proof 
+  show "x \<in># B"
+    using assms by (simp add: mset_subset_eqD)
+  have "A \<subseteq># add_mset x A"
+    by (metis (no_types) add_mset_add_single mset_subset_eq_add_left)
+  then have "A \<subset># add_mset x A"
+    by (meson multi_self_add_other_not_self subset_mset.le_imp_less_or_eq)
+  then show "A \<subset># B"
+    using assms subset_mset.strict_trans2 by blast
+qed
 
 lemma mset_subset_insertD:
   "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
@@ -653,11 +654,7 @@
 
 lemma insert_subset_eq_iff:
   "add_mset a A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
-  using le_diff_conv2 [of "Suc 0" "count B a" "count A a"]
-  apply (auto simp add: subseteq_mset_def not_in_iff Suc_le_eq)
-  apply (rule ccontr)
-  apply (auto simp add: not_in_iff)
-  done
+  using mset_subset_eq_insertD subset_mset.le_diff_conv2 by fastforce
 
 lemma insert_union_subset_iff:
   "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
@@ -723,11 +720,12 @@
   by (simp add: union_mset_def)
 
 global_interpretation subset_mset: semilattice_neutr_order \<open>(\<union>#)\<close> \<open>{#}\<close> \<open>(\<supseteq>#)\<close> \<open>(\<supset>#)\<close>
-  apply standard
-      apply (simp_all add: multiset_eq_iff subseteq_mset_def subset_mset_def max_def)
-   apply (auto simp add: le_antisym dest: sym)
-   apply (metis nat_le_linear)+
-  done
+proof 
+  show "\<And>a b. (b \<subseteq># a) = (a = a \<union># b)"
+    by (simp add: Diff_eq_empty_iff_mset union_mset_def)
+  show "\<And>a b. (b \<subset># a) = (a = a \<union># b \<and> a \<noteq> b)"
+    by (metis Diff_eq_empty_iff_mset add_cancel_left_right subset_mset_def union_mset_def)
+qed (auto simp: multiset_eqI union_mset_def)
 
 interpretation subset_mset: semilattice_sup \<open>(\<union>#)\<close> \<open>(\<subseteq>#)\<close> \<open>(\<subset>#)\<close>
 proof -
@@ -774,30 +772,8 @@
 qed
 
 lemma disjunct_not_in:
-  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  show ?Q
-  proof
-    fix a
-    from \<open>?P\<close> have "min (count A a) (count B a) = 0"
-      by (simp add: multiset_eq_iff)
-    then have "count A a = 0 \<or> count B a = 0"
-      by (cases "count A a \<le> count B a") (simp_all add: min_def)
-    then show "a \<notin># A \<or> a \<notin># B"
-      by (simp add: not_in_iff)
-  qed
-next
-  assume ?Q
-  show ?P
-  proof (rule multiset_eqI)
-    fix a
-    from \<open>?Q\<close> have "count A a = 0 \<or> count B a = 0"
-      by (auto simp add: not_in_iff)
-    then show "count (A \<inter># B) a = count {#} a"
-      by auto
-  qed
-qed
+  "A \<inter># B = {#} \<longleftrightarrow> (\<forall>a. a \<notin># A \<or> a \<notin># B)"
+  by (metis disjoint_iff set_mset_eq_empty_iff set_mset_inter)
 
 lemma inter_mset_empty_distrib_right: "A \<inter># (B + C) = {#} \<longleftrightarrow> A \<inter># B = {#} \<and> A \<inter># C = {#}"
   by (meson disjunct_not_in union_iff)
@@ -1148,15 +1124,7 @@
   fix X :: "'a multiset" and A
   assume "X \<in> A"
   show "Inf A \<subseteq># X"
-  proof (rule mset_subset_eqI)
-    fix x
-    from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
-    hence "count (Inf A) x = (INF X\<in>A. count X x)"
-      by (simp add: count_Inf_multiset_nonempty)
-    also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
-      by (intro cInf_lower) simp_all
-    finally show "count (Inf A) x \<le> count X x" .
-  qed
+    by (metis \<open>X \<in> A\<close> count_Inf_multiset_nonempty empty_iff image_eqI mset_subset_eqI wellorder_Inf_le1)
 next
   fix X :: "'a multiset" and A
   assume nonempty: "A \<noteq> {}" and le: "\<And>Y. Y \<in> A \<Longrightarrow> X \<subseteq># Y"
@@ -1240,8 +1208,7 @@
       using that by (auto simp: subseteq_mset_def algebra_simps not_in_iff)
     hence "Sup A \<subseteq># Sup A - {#x#}" by (intro subset_mset.cSup_least nonempty)
     with \<open>x \<in># Sup A\<close> show False
-      by (auto simp: subseteq_mset_def simp flip: count_greater_zero_iff
-               dest!: spec[of _ x])
+      using mset_subset_diff_self by fastforce
   qed
 next
   fix x X assume "x \<in> set_mset X" "X \<in> A"
@@ -1253,20 +1220,12 @@
 lemma in_Sup_multiset_iff:
   assumes "subset_mset.bdd_above A"
   shows   "x \<in># Sup A \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)"
-proof -
-  from assms have "set_mset (Sup A) = (\<Union>X\<in>A. set_mset X)" by (rule set_mset_Sup)
-  also have "x \<in> \<dots> \<longleftrightarrow> (\<exists>X\<in>A. x \<in># X)" by simp
-  finally show ?thesis .
-qed
+  by (simp add: assms set_mset_Sup)
 
 lemma in_Sup_multisetD:
   assumes "x \<in># Sup A"
   shows   "\<exists>X\<in>A. x \<in># X"
-proof -
-  have "subset_mset.bdd_above A"
-    by (rule ccontr) (insert assms, simp_all add: Sup_multiset_unbounded)
-  with assms show ?thesis by (simp add: in_Sup_multiset_iff)
-qed
+  using Sup_multiset_unbounded assms in_Sup_multiset_iff by fastforce
 
 interpretation subset_mset: distrib_lattice "(\<inter>#)" "(\<subseteq>#)" "(\<subset>#)" "(\<union>#)"
 proof
@@ -1328,11 +1287,7 @@
 lemma multiset_filter_mono:
   assumes "A \<subseteq># B"
   shows "filter_mset f A \<subseteq># filter_mset f B"
-proof -
-  from assms[unfolded mset_subset_eq_exists_conv]
-  obtain C where B: "B = A + C" by auto
-  show ?thesis unfolding B by auto
-qed
+  by (metis assms filter_sup_mset subset_mset.order_iff)
 
 lemma filter_mset_eq_conv:
   "filter_mset P M = N \<longleftrightarrow> N \<subseteq># M \<and> (\<forall>b\<in>#N. P b) \<and> (\<forall>a\<in>#M - N. \<not> P a)" (is "?P \<longleftrightarrow> ?Q")
@@ -1421,16 +1376,16 @@
   size_multiset_overloaded_def[THEN fun_cong, unfolded size_multiset_eq, simplified]
 
 lemma size_multiset_empty [simp]: "size_multiset f {#} = 0"
-by (simp add: size_multiset_def)
+  by (simp add: size_multiset_def)
 
 lemma size_empty [simp]: "size {#} = 0"
-by (simp add: size_multiset_overloaded_def)
+  by (simp add: size_multiset_overloaded_def)
 
 lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
-by (simp add: size_multiset_eq)
+  by (simp add: size_multiset_eq)
 
 lemma size_single: "size {#b#} = 1"
-by (simp add: size_multiset_overloaded_def size_multiset_single)
+  by (simp add: size_multiset_overloaded_def size_multiset_single)
 
 lemma sum_wcount_Int:
   "finite A \<Longrightarrow> sum (wcount f N) (A \<inter> set_mset N) = sum (wcount f N) A"
@@ -1439,20 +1394,18 @@
 
 lemma size_multiset_union [simp]:
   "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
-apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
-apply (subst Int_commute)
-apply (simp add: sum_wcount_Int)
-done
+  apply (simp add: size_multiset_def sum_Un_nat sum.distrib sum_wcount_Int wcount_union)
+  by (metis add_implies_diff finite_set_mset inf.commute sum_wcount_Int)
 
 lemma size_multiset_add_mset [simp]:
   "size_multiset f (add_mset a M) = Suc (f a) + size_multiset f M"
-  unfolding add_mset_add_single[of _ M] size_multiset_union by (auto simp: size_multiset_single)
+  by (metis add.commute add_mset_add_single size_multiset_single size_multiset_union)
 
 lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
-by (simp add: size_multiset_overloaded_def wcount_add_mset)
+  by (simp add: size_multiset_overloaded_def wcount_add_mset)
 
 lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
-by (auto simp add: size_multiset_overloaded_def)
+  by (auto simp add: size_multiset_overloaded_def)
 
 lemma size_multiset_eq_0_iff_empty [iff]:
   "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
@@ -1462,23 +1415,15 @@
 by (auto simp add: size_multiset_overloaded_def)
 
 lemma nonempty_has_size: "(S \<noteq> {#}) = (0 < size S)"
-by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
+  by (metis gr0I gr_implies_not0 size_empty size_eq_0_iff_empty)
 
 lemma size_eq_Suc_imp_elem: "size M = Suc n \<Longrightarrow> \<exists>a. a \<in># M"
-apply (unfold size_multiset_overloaded_eq)
-apply (drule sum_SucD)
-apply auto
-done
+  using all_not_in_conv by fastforce
 
 lemma size_eq_Suc_imp_eq_union:
   assumes "size M = Suc n"
   shows "\<exists>a N. M = add_mset a N"
-proof -
-  from assms obtain a where "a \<in># M"
-    by (erule size_eq_Suc_imp_elem [THEN exE])
-  then have "M = add_mset a (M - {#a#})" by simp
-  then show ?thesis by blast
-qed
+  by (metis assms insert_DiffM size_eq_Suc_imp_elem)
 
 lemma size_mset_mono:
   fixes A B :: "'a multiset"
@@ -1491,7 +1436,7 @@
 qed
 
 lemma size_filter_mset_lesseq[simp]: "size (filter_mset f M) \<le> size M"
-by (rule size_mset_mono[OF multiset_filter_subset])
+  by (rule size_mset_mono[OF multiset_filter_subset])
 
 lemma size_Diff_submset:
   "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
@@ -1560,22 +1505,21 @@
 qed (simp add: empty)
 
 lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
-by (induct M) auto
+  by (induct M) auto
 
 lemma multiset_cases [cases type]:
-  obtains (empty) "M = {#}"
-    | (add) x N where "M = add_mset x N"
+  obtains (empty) "M = {#}" | (add) x N where "M = add_mset x N"
   by (induct M) simp_all
 
 lemma multi_drop_mem_not_eq: "c \<in># B \<Longrightarrow> B - {#c#} \<noteq> B"
-by (cases "B = {#}") (auto dest: multi_member_split)
+  by (cases "B = {#}") (auto dest: multi_member_split)
 
 lemma union_filter_mset_complement[simp]:
   "\<forall>x. P x = (\<not> Q x) \<Longrightarrow> filter_mset P M + filter_mset Q M = M"
-by (subst multiset_eq_iff) auto
+  by (subst multiset_eq_iff) auto
 
 lemma multiset_partition: "M = {#x \<in># M. P x#} + {#x \<in># M. \<not> P x#}"
-by simp
+  by simp
 
 lemma mset_subset_size: "A \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
@@ -1587,8 +1531,7 @@
   have "add_mset x A \<subseteq># B"
     by (meson add.prems subset_mset_def)
   then show ?case
-    by (metis (no_types) add.prems add.right_neutral add_diff_cancel_left' leD nat_neq_iff
-      size_Diff_submset size_eq_0_iff_empty size_mset_mono subset_mset.le_iff_add subset_mset_def)
+    using add.prems subset_mset.less_eqE by fastforce
 qed
 
 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
@@ -1605,19 +1548,17 @@
 text \<open>Well-foundedness of strict subset relation\<close>
 
 lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
-apply (rule wf_measure [THEN wf_subset, where f1=size])
-apply (clarsimp simp: measure_def inv_image_def mset_subset_size)
-done
+  using mset_subset_size wfP_def wfP_if_convertible_to_nat by blast
 
 lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
   by (rule wf_subset_mset_rel[to_pred])
 
 lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
-shows "P B"
-apply (rule wf_subset_mset_rel [THEN wf_induct])
-apply (rule ih, auto)
-done
+  assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
+  shows "P B"
+  apply (rule wf_subset_mset_rel [THEN wf_induct])
+  apply (rule ih, auto)
+  done
 
 lemma multi_subset_induct [consumes 2, case_names empty add]:
   assumes "F \<subseteq># A"
@@ -1912,9 +1853,7 @@
   proof (cases "x \<in># B")
     case True
     with add.prems have "image_mset f A = image_mset f (B - {#x#}) + C"
-      by (smt (verit, del_insts) add.left_commute add_cancel_right_left diff_union_cancelL
-          diff_union_single_conv image_mset_union union_mset_add_mset_left
-          union_mset_add_mset_right)
+      by (smt (verit) add_mset_add_mset_same_iff image_mset_add_mset insert_DiffM union_mset_add_mset_left)
     with add.IH have "\<exists>M3'. A = B - {#x#} + M3' \<and> image_mset f M3' = C"
       by (smt (verit, del_insts) True Un_insert_left Un_insert_right add.prems(2) inj_on_insert
           insert_DiffM set_mset_add_mset_insert)
@@ -2035,12 +1974,7 @@
 
 lemma set_eq_iff_mset_remdups_eq:
   \<open>set x = set y \<longleftrightarrow> mset (remdups x) = mset (remdups y)\<close>
-apply (rule iffI)
-apply (simp add: set_eq_iff_mset_eq_distinct[THEN iffD1])
-apply (drule distinct_remdups [THEN distinct_remdups
-      [THEN set_eq_iff_mset_eq_distinct [THEN iffD2]]])
-apply simp
-done
+  using set_eq_iff_mset_eq_distinct by fastforce
 
 lemma mset_eq_imp_distinct_iff:
   \<open>distinct xs \<longleftrightarrow> distinct ys\<close> if \<open>mset xs = mset ys\<close>
@@ -2255,14 +2189,14 @@
 
 lemma set_sorted_list_of_multiset [simp]:
   "set (sorted_list_of_multiset M) = set_mset M"
-by (induct M) (simp_all add: set_insort_key)
+  by (induct M) (simp_all add: set_insort_key)
 
 lemma sorted_list_of_mset_set [simp]:
   "sorted_list_of_multiset (mset_set A) = sorted_list_of_set A"
-by (cases "finite A") (induct A rule: finite_induct, simp_all)
+  by (cases "finite A") (induct A rule: finite_induct, simp_all)
 
 lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
-  by (induction n) (simp_all add: atLeastLessThanSuc)
+  by (metis distinct_upt mset_set_set set_upt)
 
 lemma image_mset_map_of:
   "distinct (map fst xs) \<Longrightarrow> {#the (map_of xs i). i \<in># mset (map fst xs)#} = mset (map snd xs)"
@@ -2308,7 +2242,7 @@
   unfolding replicate_mset_def by (induct n) auto
 
 lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
-  by (auto split: if_splits)
+  by auto
 
 lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   by (induct n, simp_all)
@@ -2530,8 +2464,8 @@
   shows "size {#x \<in># M. P x#} < size M"
 proof -
   have "size (filter_mset P M) \<noteq> size M"
-    using assms by (metis add.right_neutral add_diff_cancel_left' count_filter_mset mem_Collect_eq
-      multiset_partition nonempty_has_size set_mset_def size_union)
+    using assms
+    by (metis dual_order.strict_iff_order filter_mset_eq_conv mset_subset_size subset_mset.nless_le)
   then show ?thesis
     by (meson leD nat_neq_iff size_filter_mset_lesseq)
 qed
@@ -3956,17 +3890,11 @@
   by (force simp: mult1_def)
 
 lemma union_le_mono2: "B < D \<Longrightarrow> C + B < C + (D::'a::preorder multiset)"
-apply (unfold less_multiset_def multp_def mult_def)
-apply (erule trancl_induct)
- apply (blast intro: mult1_union)
-apply (blast intro: mult1_union trancl_trans)
-done
+  unfolding less_multiset_def multp_def mult_def
+  by (induction rule: trancl_induct; blast intro: mult1_union trancl_trans)
 
 lemma union_le_mono1: "B < D \<Longrightarrow> B + C < D + (C::'a::preorder multiset)"
-apply (subst add.commute [of B C])
-apply (subst add.commute [of D C])
-apply (erule union_le_mono2)
-done
+  by (metis add.commute union_le_mono2)
 
 lemma union_less_mono:
   fixes A B C D :: "'a::preorder multiset"
@@ -3991,8 +3919,8 @@
 definition "ms_weak = ms_strict \<union> Id"
 
 lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
-unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
-by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+  unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+  by (auto intro: wf_mult1 wf_trancl simp: mult_def)
 
 lemma smsI:
   "(set_mset A, set_mset B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
@@ -4268,11 +4196,7 @@
 
 lemma [code]: \<comment> \<open>not very efficient, but representation-ignorant!\<close>
   "mset_set A = mset (sorted_list_of_set A)"
-  apply (cases "finite A")
-  apply simp_all
-  apply (induct A rule: finite_induct)
-  apply simp_all
-  done
+  by (metis mset_sorted_list_of_multiset sorted_list_of_mset_set)
 
 declare size_mset [code]
 
@@ -4313,18 +4237,15 @@
     hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
       by auto
     show ?thesis unfolding subset_eq_mset_impl.simps
-      unfolding Some option.simps split
-      unfolding id
-      using Cons[of "ys1 @ ys2"]
-      unfolding subset_mset_def subseteq_mset_def by auto
+      by (simp add: Some id Cons)
   qed
 qed
 
 lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys \<noteq> None"
-  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+  by (simp add: subset_eq_mset_impl)
 
 lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> subset_eq_mset_impl xs ys = Some True"
-  using subset_eq_mset_impl[of xs ys] by (cases "subset_eq_mset_impl xs ys", auto)
+  using subset_eq_mset_impl by blast
 
 instantiation multiset :: (equal) equal
 begin
@@ -4519,14 +4440,10 @@
   rel: rel_mset
   pred: pred_mset
 proof -
-  show "image_mset id = id"
-    by (rule image_mset.id)
   show "image_mset (g \<circ> f) = image_mset g \<circ> image_mset f" for f g
     unfolding comp_def by (rule ext) (simp add: comp_def image_mset.compositionality)
   show "(\<And>z. z \<in> set_mset X \<Longrightarrow> f z = g z) \<Longrightarrow> image_mset f X = image_mset g X" for f g X
     by (induct X) simp_all
-  show "set_mset \<circ> image_mset f = (`) f \<circ> set_mset" for f
-    by auto
   show "card_order natLeq"
     by (rule natLeq_card_order)
   show "BNF_Cardinal_Arithmetic.cinfinite natLeq"
@@ -4538,34 +4455,15 @@
       (auto simp: finite_iff_ordLess_natLeq[symmetric])
   show "rel_mset R OO rel_mset S \<le> rel_mset (R OO S)" for R S
     unfolding rel_mset_def[abs_def] OO_def
-    apply clarify
-    subgoal for X Z Y xs ys' ys zs
-      apply (drule list_all2_reorder_left_invariance [where xs = ys' and ys = zs and xs' = ys])
-      apply (auto intro: list_all2_trans)
-      done
-    done
+    by (smt (verit, ccfv_SIG) list_all2_reorder_left_invariance list_all2_trans predicate2I)
   show "rel_mset R =
     (\<lambda>x y. \<exists>z. set_mset z \<subseteq> {(x, y). R x y} \<and>
     image_mset fst z = x \<and> image_mset snd z = y)" for R
     unfolding rel_mset_def[abs_def]
-    apply (rule ext)+
-    apply safe
-     apply (rule_tac x = "mset (zip xs ys)" in exI;
-       auto simp: in_set_zip list_all2_iff simp flip: mset_map)
-    apply (rename_tac XY)
-    apply (cut_tac X = XY in ex_mset)
-    apply (erule exE)
-    apply (rename_tac xys)
-    apply (rule_tac x = "map fst xys" in exI)
-    apply (auto simp: mset_map)
-    apply (rule_tac x = "map snd xys" in exI)
-    apply (auto simp: mset_map list_all2I subset_eq zip_map_fst_snd)
-    done
-  show "z \<in> set_mset {#} \<Longrightarrow> False" for z
-    by auto
+    by (metis (no_types, lifting) ex_mset list.in_rel mem_Collect_eq mset_map set_mset_mset)
   show "pred_mset P = (\<lambda>x. Ball (set_mset x) P)" for P
     by (simp add: fun_eq_iff pred_mset_iff)
-qed
+qed auto
 
 inductive rel_mset' :: \<open>('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset \<Rightarrow> bool\<close>
 where
@@ -4609,10 +4507,7 @@
     and addL: "\<And>a M N. P M N \<Longrightarrow> P (add_mset a M) N"
     and addR: "\<And>a M N. P M N \<Longrightarrow> P M (add_mset a N)"
   shows "P M N"
-apply(induct N rule: multiset_induct)
-  apply(induct M rule: multiset_induct, rule empty, erule addL)
-  apply(induct M rule: multiset_induct, erule addR, erule addR)
-done
+  by (induct N rule: multiset_induct; induct M rule: multiset_induct) (auto simp: assms)
 
 lemma multiset_induct2_size[consumes 1, case_names empty add]:
   assumes c: "size M = size N"




