diff -r 4ccb7e635477 -r e68a0b651eb5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 05 15:00:37 2016 +0200
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 05 15:47:50 2016 +0200
@@ -98,21 +98,43 @@
 
 end
 
-
-lift_definition single :: "'a \<Rightarrow> 'a multiset" is "\<lambda>a b. if b = a then 1 else 0"
-by (rule only1_in_multiset)
+lemma add_mset_in_multiset:
+  assumes M: \<open>M \<in> multiset\<close>
+  shows \<open>(\<lambda>b. if b = a then Suc (M b) else M b) \<in> multiset\<close>
+  using assms by (simp add: multiset_def insert_Collect[symmetric])
+
+lift_definition add_mset :: "'a \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" is
+  "\<lambda>a M b. if b = a then Suc (M b) else M b"
+by (rule add_mset_in_multiset)
 
 syntax
   "_multiset" :: "args \<Rightarrow> 'a multiset"    ("{#(_)#}")
 translations
-  "{#x, xs#}" == "{#x#} + {#xs#}"
-  "{#x#}" == "CONST single x"
+  "{#x, xs#}" == "CONST add_mset x {#xs#}"
+  "{#x#}" == "CONST add_mset x {#}"
 
 lemma count_empty [simp]: "count {#} a = 0"
   by (simp add: zero_multiset.rep_eq)
 
-lemma count_single [simp]: "count {#b#} a = (if b = a then 1 else 0)"
-  by (simp add: single.rep_eq)
+lemma count_add_mset [simp]:
+  "count (add_mset b A) a = (if b = a then Suc (count A a) else count A a)"
+  by (simp add: add_mset.rep_eq)
+
+lemma count_single: "count {#b#} a = (if b = a then 1 else 0)"
+  by simp
+
+lemma
+  add_mset_not_empty [simp]: \<open>add_mset a A \<noteq> {#}\<close> and
+  empty_not_add_mset [simp]: "{#} \<noteq> add_mset a A"
+  by (auto simp: multiset_eq_iff)
+
+lemma add_mset_add_mset_same_iff [simp]:
+  "add_mset a A = add_mset a B \<longleftrightarrow> A = B"
+  by (auto simp: multiset_eq_iff)
+
+lemma add_mset_commute:
+  "add_mset x (add_mset y M) = add_mset y (add_mset x M)"
+  by (auto simp: multiset_eq_iff)
 
 
 subsection \<open>Basic operations\<close>
@@ -209,7 +231,7 @@
   "set_mset {#} = {}"
   by (simp add: set_mset_def)
 
-lemma set_mset_single [simp]:
+lemma set_mset_single:
   "set_mset {#b#} = {b}"
   by (simp add: set_mset_def)
 
@@ -221,6 +243,10 @@
   "finite (set_mset M)"
   using count [of M] by (simp add: multiset_def)
 
+lemma set_mset_add_mset_insert [simp]: \<open>set_mset (add_mset a A) = insert a (set_mset A)\<close>
+  by (auto simp del: count_greater_eq_Suc_zero_iff
+      simp: count_greater_eq_Suc_zero_iff[symmetric] split: if_splits)
+
 
 subsubsection \<open>Union\<close>
 
@@ -232,6 +258,17 @@
   "set_mset (M + N) = set_mset M \<union> set_mset N"
   by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_union) simp
 
+lemma union_mset_add_mset_left [simp]:
+  "add_mset a A + B = add_mset a (A + B)"
+  by (auto simp: multiset_eq_iff)
+
+lemma union_mset_add_mset_right [simp]:
+  "A + add_mset a B = add_mset a (A + B)"
+  by (auto simp: multiset_eq_iff)
+
+lemma add_mset_add_single: \<open>add_mset a A = A + {#a#}\<close>
+  by (subst union_mset_add_mset_right, subst add.comm_neutral) standard
+
 
 subsubsection \<open>Difference\<close>
 
@@ -242,6 +279,10 @@
   "count (M - N) a = count M a - count N a"
   by (simp add: minus_multiset.rep_eq)
 
+lemma add_mset_diff_bothsides:
+  \<open>add_mset a M - add_mset a A = M - A\<close>
+  by (auto simp: multiset_eq_iff)
+
 lemma in_diff_count:
   "a \<in># M - N \<longleftrightarrow> count N a < count M a"
   by (simp add: set_mset_def)
@@ -284,13 +325,13 @@
 lemma diff_empty [simp]: "M - {#} = M \<and> {#} - M = {#}"
   by rule (fact Groups.diff_zero, fact Groups.zero_diff)
 
-lemma diff_cancel [simp]: "A - A = {#}"
+lemma diff_cancel: "A - A = {#}"
   by (fact Groups.diff_cancel)
 
-lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
+lemma diff_union_cancelR: "M + N - N = (M::'a multiset)"
   by (fact add_diff_cancel_right')
 
-lemma diff_union_cancelL [simp]: "N + M - N = (M::'a multiset)"
+lemma diff_union_cancelL: "N + M - N = (M::'a multiset)"
   by (fact add_diff_cancel_left')
 
 lemma diff_right_commute:
@@ -303,24 +344,33 @@
   shows "M - (N + Q) = M - N - Q"
   by (rule sym) (fact diff_diff_add)
 
-lemma insert_DiffM: "x \<in># M \<Longrightarrow> {#x#} + (M - {#x#}) = M"
+lemma insert_DiffM [simp]: "x \<in># M \<Longrightarrow> add_mset x (M - {#x#}) = M"
   by (clarsimp simp: multiset_eq_iff)
 
-lemma insert_DiffM2 [simp]: "x \<in># M \<Longrightarrow> M - {#x#} + {#x#} = M"
-  by (clarsimp simp: multiset_eq_iff)
-
-lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
+lemma insert_DiffM2: "x \<in># M \<Longrightarrow> (M - {#x#}) + {#x#} = M"
+  by simp
+
+lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> add_mset b (M - {#a#}) = add_mset b M - {#a#}"
   by (auto simp add: multiset_eq_iff)
 
+lemma diff_add_mset_swap [simp]: "b \<notin># A \<Longrightarrow> add_mset b M - A = add_mset b (M - A)"
+  by (auto simp add: multiset_eq_iff simp: not_in_iff)
+
+lemma diff_union_swap2 [simp]: "y \<in># M \<Longrightarrow> add_mset x M - {#y#} = add_mset x (M - {#y#})"
+  by (metis add_mset_diff_bothsides diff_union_swap diff_zero insert_DiffM)
+
+lemma diff_diff_add_mset [simp]: "(M::'a multiset) - N - P = M - (N + P)"
+  by (rule diff_diff_add)
+
 lemma diff_union_single_conv:
   "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
   by (simp add: multiset_eq_iff Suc_le_eq)
 
 lemma mset_add [elim?]:
   assumes "a \<in># A"
-  obtains B where "A = B + {#a#}"
+  obtains B where "A = add_mset a B"
 proof -
-  from assms have "A = (A - {#a#}) + {#a#}"
+  from assms have "A = add_mset a (A - {#a#})"
     by simp
   with that show thesis .
 qed
@@ -332,9 +382,6 @@
 
 subsubsection \<open>Equality of multisets\<close>
 
-lemma single_not_empty [simp]: "{#a#} \<noteq> {#} \<and> {#} \<noteq> {#a#}"
-  by (simp add: multiset_eq_iff)
-
 lemma single_eq_single [simp]: "{#a#} = {#b#} \<longleftrightarrow> a = b"
   by (auto simp add: multiset_eq_iff)
 
@@ -344,20 +391,30 @@
 lemma empty_eq_union [iff]: "{#} = M + N \<longleftrightarrow> M = {#} \<and> N = {#}"
   by (auto simp add: multiset_eq_iff)
 
-lemma multi_self_add_other_not_self [simp]: "M = M + {#x#} \<longleftrightarrow> False"
+lemma multi_self_add_other_not_self [simp]: "M = add_mset x M \<longleftrightarrow> False"
   by (auto simp add: multiset_eq_iff)
 
+lemma add_mset_remove_trivial [simp]: \<open>add_mset x M - {#x#} = M\<close>
+  by (auto simp: multiset_eq_iff)
+
 lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
   by (auto simp add: multiset_eq_iff not_in_iff)
 
-lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = N + {#x#}"
+lemma diff_single_eq_union: "x \<in># M \<Longrightarrow> M - {#x#} = N \<longleftrightarrow> M = add_mset x N"
+  by auto
+
+lemma union_single_eq_diff: "add_mset x M = N \<Longrightarrow> M = N - {#x#}"
+  unfolding add_mset_add_single[of _ M] by (fact add_implies_diff)
+
+lemma union_single_eq_member: "add_mset x M = N \<Longrightarrow> x \<in># N"
   by auto
 
-lemma union_single_eq_diff: "M + {#x#} = N \<Longrightarrow> M = N - {#x#}"
-  by (auto dest: sym)
-
-lemma union_single_eq_member: "M + {#x#} = N \<Longrightarrow> x \<in># N"
-  by auto
+lemma add_mset_remove_trivial_If:
+  "add_mset a (N - {#a#}) = (if a \<in># N then N else add_mset a N)"
+  by (simp add: diff_single_trivial)
+
+lemma add_mset_remove_trivial_eq: \<open>N = add_mset a (N - {#a#}) \<longleftrightarrow> a \<in># N\<close>
+  by (auto simp: add_mset_remove_trivial_If)
 
 lemma union_is_single:
   "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
@@ -372,56 +429,61 @@
   by (auto simp add: eq_commute [of "{#a#}" "M + N"] union_is_single)
 
 lemma add_eq_conv_diff:
-  "M + {#a#} = N + {#b#} \<longleftrightarrow> M = N \<and> a = b \<or> M = N - {#a#} + {#b#} \<and> N = M - {#b#} + {#a#}"
+  "add_mset a M = add_mset b N \<longleftrightarrow> M = N \<and> a = b \<or> M = add_mset b (N - {#a#}) \<and> N = add_mset a (M - {#b#})"
   (is "?lhs \<longleftrightarrow> ?rhs")
 (* shorter: by (simp add: multiset_eq_iff) fastforce *)
 proof
   show ?lhs if ?rhs
     using that
-    by (auto simp add: add.assoc add.commute [of "{#b#}"])
-      (drule sym, simp add: add.assoc [symmetric])
+    by (auto simp add: add_mset_commute[of a b])
   show ?rhs if ?lhs
   proof (cases "a = b")
     case True with \<open>?lhs\<close> show ?thesis by simp
   next
     case False
-    from \<open>?lhs\<close> have "a \<in># N + {#b#}" by (rule union_single_eq_member)
+    from \<open>?lhs\<close> have "a \<in># add_mset b N" by (rule union_single_eq_member)
     with False have "a \<in># N" by auto
-    moreover from \<open>?lhs\<close> have "M = N + {#b#} - {#a#}" by (rule union_single_eq_diff)
+    moreover from \<open>?lhs\<close> have "M = add_mset b N - {#a#}" by (rule union_single_eq_diff)
     moreover note False
-    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"] diff_union_swap)
+    ultimately show ?thesis by (auto simp add: diff_right_commute [of _ "{#a#}"])
   qed
 qed
 
+lemma add_mset_eq_single [iff]: "add_mset b M = {#a#} \<longleftrightarrow> b = a \<and> M = {#}"
+  by (auto simp: add_eq_conv_diff)
+
+lemma single_eq_add_mset [iff]: "{#a#} = add_mset b M \<longleftrightarrow> b = a \<and> M = {#}"
+  by (auto simp: add_eq_conv_diff)
+
 lemma insert_noteq_member:
-  assumes BC: "B + {#b#} = C + {#c#}"
+  assumes BC: "add_mset b B = add_mset c C"
    and bnotc: "b \<noteq> c"
   shows "c \<in># B"
 proof -
-  have "c \<in># C + {#c#}" by simp
+  have "c \<in># add_mset c C" by simp
   have nc: "\<not> c \<in># {#b#}" using bnotc by simp
-  then have "c \<in># B + {#b#}" using BC by simp
+  then have "c \<in># add_mset b B" using BC by simp
   then show "c \<in># B" using nc by simp
 qed
 
 lemma add_eq_conv_ex:
-  "(M + {#a#} = N + {#b#}) =
-    (M = N \<and> a = b \<or> (\<exists>K. M = K + {#b#} \<and> N = K + {#a#}))"
+  "(add_mset a M = add_mset b N) =
+    (M = N \<and> a = b \<or> (\<exists>K. M = add_mset b K \<and> N = add_mset a K))"
   by (auto simp add: add_eq_conv_diff)
 
-lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = A + {#x#}"
+lemma multi_member_split: "x \<in># M \<Longrightarrow> \<exists>A. M = add_mset x A"
   by (rule exI [where x = "M - {#x#}"]) simp
 
 lemma multiset_add_sub_el_shuffle:
   assumes "c \<in># B"
     and "b \<noteq> c"
-  shows "B - {#c#} + {#b#} = B + {#b#} - {#c#}"
+  shows "add_mset b (B - {#c#}) = add_mset b B - {#c#}"
 proof -
-  from \<open>c \<in># B\<close> obtain A where B: "B = A + {#c#}"
+  from \<open>c \<in># B\<close> obtain A where B: "B = add_mset c A"
     by (blast dest: multi_member_split)
-  have "A + {#b#} = A + {#b#} + {#c#} - {#c#}" by simp
-  then have "A + {#b#} = A + {#c#} + {#b#} - {#c#}"
-    by (simp add: ac_simps)
+  have "add_mset b A = add_mset c (add_mset b A) - {#c#}" by simp
+  then have "add_mset b A = add_mset b (add_mset c A) - {#c#}"
+    by (simp add: ac_simps \<open>b \<noteq> c\<close>)
   then show ?thesis using B by simp
 qed
 
@@ -454,6 +516,9 @@
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
   \<comment> \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
+interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
+  by standard
+
 lemma mset_subset_eqI:
   "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
   by (simp add: subseteq_mset_def)
@@ -472,36 +537,37 @@
 interpretation subset_mset: ordered_cancel_comm_monoid_diff "op +" 0 "op \<le>#" "op <#" "op -"
   by standard (simp, fact mset_subset_eq_exists_conv)
 
-interpretation subset_mset: ordered_ab_semigroup_monoid_add_imp_le "op +" 0 "op -" "op \<le>#" "op <#"
-  by standard
-
-lemma mset_subset_eq_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
+lemma mset_subset_eq_mono_add_right_cancel: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
    by (fact subset_mset.add_le_cancel_right)
- 
-lemma mset_subset_eq_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
+
+lemma mset_subset_eq_mono_add_left_cancel: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
    by (fact subset_mset.add_le_cancel_left)
- 
+
 lemma mset_subset_eq_mono_add: "(A::'a multiset) \<subseteq># B \<Longrightarrow> C \<subseteq># D \<Longrightarrow> A + C \<subseteq># B + D"
    by (fact subset_mset.add_mono)
- 
+
 lemma mset_subset_eq_add_left: "(A::'a multiset) \<subseteq># A + B"
    by simp
- 
+
 lemma mset_subset_eq_add_right: "B \<subseteq># (A::'a multiset) + B"
    by simp
- 
+
 lemma single_subset_iff [simp]:
   "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
   by (auto simp add: subseteq_mset_def Suc_le_eq)
 
 lemma mset_subset_eq_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
   by (simp add: subseteq_mset_def Suc_le_eq)
- 
+
+lemma mset_subset_eq_add_mset_cancel: \<open>add_mset a A \<subseteq># add_mset a B \<longleftrightarrow> A \<subseteq># B\<close>
+  unfolding add_mset_add_single[of _ A] add_mset_add_single[of _ B]
+  by (rule mset_subset_eq_mono_add_right_cancel)
+
 lemma multiset_diff_union_assoc:
   fixes A B C D :: "'a multiset"
   shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
   by (fact subset_mset.diff_add_assoc)
- 
+
 lemma mset_subset_eq_multiset_union_diff_commute:
   fixes A B C D :: "'a multiset"
   shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
@@ -520,7 +586,7 @@
     by (simp add: subseteq_mset_def)
   finally show ?thesis by simp
 qed
-  
+
 lemma mset_subsetD:
   "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
   by (auto intro: mset_subset_eqD [of A])
@@ -530,7 +596,7 @@
   by (metis mset_subset_eqD subsetI)
 
 lemma mset_subset_eq_insertD:
-  "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
+  "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)
@@ -540,7 +606,7 @@
 done
 
 lemma mset_subset_insertD:
-  "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
+  "add_mset x A \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
   by (rule mset_subset_eq_insertD) simp
 
 lemma mset_subset_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
@@ -548,9 +614,9 @@
 
 lemma empty_le [simp]: "{#} \<subseteq># A"
   unfolding mset_subset_eq_exists_conv by auto
- 
+
 lemma insert_subset_eq_iff:
-  "{#a#} + A \<subseteq># B \<longleftrightarrow> a \<in># B \<and> A \<subseteq># B - {#a#}"
+  "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)
@@ -558,24 +624,25 @@
   done
 
 lemma insert_union_subset_iff:
-  "{#a#} + A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
-  by (auto simp add: insert_subset_eq_iff subset_mset_def insert_DiffM)
+  "add_mset a A \<subset># B \<longleftrightarrow> a \<in># B \<and> A \<subset># B - {#a#}"
+  by (auto simp add: insert_subset_eq_iff subset_mset_def)
 
 lemma subset_eq_diff_conv:
   "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
   by (simp add: subseteq_mset_def le_diff_conv)
 
-lemma subset_eq_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
-  unfolding mset_subset_eq_exists_conv by auto
-
-lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
+lemma subset_eq_empty: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
+  by auto
+
+lemma multi_psub_of_add_self [simp]: "A \<subset># add_mset x A"
   by (auto simp: subset_mset_def subseteq_mset_def)
 
 lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
   by simp
 
-lemma mset_subset_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
-  by (fact subset_mset.add_less_imp_less_right)
+lemma mset_subset_add_mset [simp]: "add_mset x N \<subset># add_mset x M \<longleftrightarrow> N \<subset># M"
+  unfolding add_mset_add_single[of _ N] add_mset_add_single[of _ M]
+  by (fact subset_mset.add_less_cancel_right)
 
 lemma mset_subset_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
   by (fact subset_mset.zero_less_iff_neq_zero)
@@ -657,22 +724,37 @@
   qed
 qed
 
+lemma add_mset_inter_add_mset:
+  "add_mset a A #\<inter> add_mset a B = add_mset a (A #\<inter> B)"
+  by (metis add_mset_add_single add_mset_diff_bothsides diff_subset_eq_self multiset_inter_def
+      subset_mset.diff_add_assoc2)
+
+lemma add_mset_disjoint [simp]:
+  "add_mset a A #\<inter> B = {#} \<longleftrightarrow> a \<notin># B \<and> A #\<inter> B = {#}"
+  "{#} = add_mset a A #\<inter> B \<longleftrightarrow> a \<notin># B \<and> {#} = A #\<inter> B"
+  by (auto simp: disjunct_not_in)
+
+lemma disjoint_add_mset [simp]:
+  "B #\<inter> add_mset a A = {#} \<longleftrightarrow> a \<notin># B \<and> B #\<inter> A = {#}"
+  "{#} = A #\<inter> add_mset b B \<longleftrightarrow> b \<notin># A \<and> {#} = A #\<inter> B"
+  by (auto simp: disjunct_not_in)
+
 lemma empty_inter [simp]: "{#} #\<inter> M = {#}"
   by (simp add: multiset_eq_iff)
 
 lemma inter_empty [simp]: "M #\<inter> {#} = {#}"
   by (simp add: multiset_eq_iff)
 
-lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N"
+lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = M #\<inter> N"
   by (simp add: multiset_eq_iff not_in_iff)
 
-lemma inter_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = (M #\<inter> (N - {#x#})) + {#x#}"
+lemma inter_add_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<inter> N = add_mset x (M #\<inter> (N - {#x#}))"
   by (auto simp add: multiset_eq_iff elim: mset_add)
 
-lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = N #\<inter> M"
+lemma inter_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = N #\<inter> M"
   by (simp add: multiset_eq_iff not_in_iff)
 
-lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (M + {#x#}) = ((N - {#x#}) #\<inter> M) + {#x#}"
+lemma inter_add_right2: "x \<in># N \<Longrightarrow> N #\<inter> (add_mset x M) = add_mset x ((N - {#x#}) #\<inter> M)"
   by (auto simp add: multiset_eq_iff elim: mset_add)
 
 lemma disjunct_set_mset_diff:
@@ -747,16 +829,16 @@
 lemma sup_empty [simp]: "M #\<union> {#} = M"
   by (simp add: multiset_eq_iff)
 
-lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
+lemma sup_union_left1 [simp]: "\<not> x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> N)"
   by (simp add: multiset_eq_iff not_in_iff)
 
-lemma sup_union_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
+lemma sup_union_left2: "x \<in># N \<Longrightarrow> (add_mset x M) #\<union> N = add_mset x (M #\<union> (N - {#x#}))"
   by (simp add: multiset_eq_iff)
 
-lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
+lemma sup_union_right1 [simp]: "\<not> x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x (N #\<union> M)"
   by (simp add: multiset_eq_iff not_in_iff)
 
-lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
+lemma sup_union_right2: "x \<in># N \<Longrightarrow> N #\<union> (add_mset x M) = add_mset x ((N - {#x#}) #\<union> M)"
   by (simp add: multiset_eq_iff)
 
 lemma sup_union_distrib_left:
@@ -775,12 +857,105 @@
   "A + B - A #\<union> B = A #\<inter> B"
   by (auto simp add: multiset_eq_iff)
 
+lemma add_mset_union:
+  \<open>add_mset a A #\<union> add_mset a B = add_mset a (A #\<union> B)\<close>
+  by (auto simp: multiset_eq_iff max_def)
+
 
 subsubsection \<open>Subset is an order\<close>
 
 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
 
 
+subsubsection \<open>Simprocs\<close>
+
+fun repeat_mset :: "nat \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
+  "repeat_mset 0 _ = {#}" |
+  "repeat_mset (Suc n) A = A + repeat_mset n A"
+
+lemma count_repeat_mset [simp]: "count (repeat_mset i A) a = i * count A a"
+  by (induction i) auto
+
+lemma repeat_mset_right [simp]: "repeat_mset a (repeat_mset b A) = repeat_mset (a * b) A"
+  by (auto simp: multiset_eq_iff left_diff_distrib')
+
+lemma left_diff_repeat_mset_distrib': \<open>repeat_mset (i - j) u = repeat_mset i u - repeat_mset j u\<close>
+  by (auto simp: multiset_eq_iff left_diff_distrib')
+
+lemma mset_diff_add_eq1:
+  "j \<le> (i::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = ((repeat_mset (i-j) u + m) - n)"
+  by (auto simp: multiset_eq_iff nat_diff_add_eq1)
+
+lemma mset_diff_add_eq2:
+  "i \<le> (j::nat) \<Longrightarrow> ((repeat_mset i u + m) - (repeat_mset j u + n)) = (m - (repeat_mset (j-i) u + n))"
+  by (auto simp: multiset_eq_iff nat_diff_add_eq2)
+
+lemma mset_eq_add_iff1:
+   "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (repeat_mset (i-j) u + m = n)"
+  by (auto simp: multiset_eq_iff nat_eq_add_iff1)
+
+lemma mset_eq_add_iff2:
+   "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m = repeat_mset j u + n) = (m = repeat_mset (j-i) u + n)"
+  by (auto simp: multiset_eq_iff nat_eq_add_iff2)
+
+lemma mset_subseteq_add_iff1:
+  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subseteq># n)"
+  by (auto simp add: subseteq_mset_def nat_le_add_iff1)
+
+lemma mset_subseteq_add_iff2:
+  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subseteq># repeat_mset j u + n) = (m \<subseteq># repeat_mset (j-i) u + n)"
+  by (auto simp add: subseteq_mset_def nat_le_add_iff2)
+
+lemma mset_subset_add_iff1:
+  "j \<le> (i::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (repeat_mset (i-j) u + m \<subset># n)"
+  unfolding subset_mset_def by (simp add: mset_eq_add_iff1 mset_subseteq_add_iff1)
+
+lemma mset_subset_add_iff2:
+  "i \<le> (j::nat) \<Longrightarrow> (repeat_mset i u + m \<subset># repeat_mset j u + n) = (m \<subset># repeat_mset (j-i) u + n)"
+  unfolding subset_mset_def by (simp add: mset_eq_add_iff2 mset_subseteq_add_iff2)
+
+lemma left_add_mult_distrib_mset:
+  "repeat_mset i u + (repeat_mset j u + k) = repeat_mset (i+j) u + k"
+  by (auto simp: multiset_eq_iff add_mult_distrib)
+
+lemma repeat_mset_cancel1: "repeat_mset a A = repeat_mset a B \<longleftrightarrow> A = B \<or> a = 0"
+  by (auto simp: multiset_eq_iff)
+
+lemma repeat_mset_cancel2: "repeat_mset a A = repeat_mset b A \<longleftrightarrow> a = b \<or> A = {#}"
+  by (auto simp: multiset_eq_iff)
+
+lemma repeat_mset_distrib [simp]:
+  "repeat_mset n (A + B) = repeat_mset n A + repeat_mset n B"
+  by (auto simp: multiset_eq_iff add_mult_distrib2)
+
+lemma repeat_mset_distrib_add_mset [simp]:
+  "repeat_mset n (add_mset a A) = repeat_mset n {#a#} + repeat_mset n A"
+  by (auto simp: multiset_eq_iff)
+
+ML_file "multiset_simprocs_util.ML"
+ML_file "multiset_simprocs.ML"
+
+simproc_setup mseteq_cancel_numerals
+  ("(l::'a multiset) + m = n" | "(l::'a multiset) = m + n" |
+   "add_mset a m = n" | "m = add_mset a n") =
+  \<open>fn phi => Multiset_Simprocs.eq_cancel_msets\<close>
+
+simproc_setup msetless_cancel_numerals
+  ("(l::'a multiset) + m \<subset># n" | "(l::'a multiset) \<subset># m + n" |
+   "add_mset a m \<subset># n" | "m \<subset># add_mset a n") =
+  \<open>fn phi => Multiset_Simprocs.subset_cancel_msets\<close>
+
+simproc_setup msetle_cancel_numerals
+  ("(l::'a multiset) + m \<subseteq># n" | "(l::'a multiset) \<subseteq># m + n" |
+   "add_mset a m \<subseteq># n" | "m \<subseteq># add_mset a n") =
+  \<open>fn phi => Multiset_Simprocs.subseteq_cancel_msets\<close>
+
+simproc_setup msetdiff_cancel_numerals
+  ("((l::'a multiset) + m) - n" | "(l::'a multiset) - (m + n)" |
+   "add_mset a m - n" | "m - add_mset a n") =
+  \<open>fn phi => Multiset_Simprocs.diff_cancel_msets\<close>
+
+
 subsubsection \<open>Conditionally complete lattice\<close>
 
 instantiation multiset :: (type) Inf
@@ -1001,7 +1176,7 @@
   finally show ?thesis .
 qed
 
-lemma in_Sup_multisetD: 
+lemma in_Sup_multisetD:
   assumes "x \<in># Sup A"
   shows   "\<exists>X\<in>A. x \<in># X"
 proof -
@@ -1044,7 +1219,7 @@
 lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
   by (rule multiset_eqI) simp
 
-lemma filter_single_mset [simp]: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
+lemma filter_single_mset: "filter_mset P {#x#} = (if P x then {#x#} else {#})"
   by (rule multiset_eqI) simp
 
 lemma filter_union_mset [simp]: "filter_mset P (M + N) = filter_mset P M + filter_mset P N"
@@ -1056,6 +1231,11 @@
 lemma filter_inter_mset [simp]: "filter_mset P (M #\<inter> N) = filter_mset P M #\<inter> filter_mset P N"
   by (rule multiset_eqI) simp
 
+lemma filter_mset_add_mset [simp]:
+   "filter_mset P (add_mset x A) =
+     (if P x then add_mset x (filter_mset P A) else (filter_mset P A))"
+   by (auto simp: multiset_eq_iff)
+
 lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   by (simp add: mset_subset_eqI)
 
@@ -1091,7 +1271,7 @@
       case False then have "count M a = 0"
         by (simp add: not_in_iff)
       with M show ?thesis by simp
-    qed 
+    qed
   qed
 qed
 
@@ -1103,6 +1283,10 @@
 lemma wcount_union: "wcount f (M + N) a = wcount f M a + wcount f N a"
   by (auto simp: wcount_def add_mult_distrib)
 
+lemma wcount_add_mset:
+  "wcount f (add_mset x M) a = (if x = a then Suc (f a) else 0) + wcount f M a"
+  unfolding add_mset_add_single[of _ M] wcount_union by (auto simp: wcount_def)
+
 definition size_multiset :: "('a \<Rightarrow> nat) \<Rightarrow> 'a multiset \<Rightarrow> nat" where
   "size_multiset f M = setsum (wcount f M) (set_mset M)"
 
@@ -1126,11 +1310,11 @@
 lemma size_empty [simp]: "size {#} = 0"
 by (simp add: size_multiset_overloaded_def)
 
-lemma size_multiset_single [simp]: "size_multiset f {#b#} = Suc (f b)"
+lemma size_multiset_single : "size_multiset f {#b#} = Suc (f b)"
 by (simp add: size_multiset_eq)
 
-lemma size_single [simp]: "size {#b#} = 1"
-by (simp add: size_multiset_overloaded_def)
+lemma size_single: "size {#b#} = 1"
+by (simp add: size_multiset_overloaded_def size_multiset_single)
 
 lemma setsum_wcount_Int:
   "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
@@ -1144,6 +1328,13 @@
 apply (simp add: setsum_wcount_Int)
 done
 
+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)
+
+lemma size_add_mset [simp]: "size (add_mset a A) = Suc (size A)"
+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)
 
@@ -1165,11 +1356,11 @@
 
 lemma size_eq_Suc_imp_eq_union:
   assumes "size M = Suc n"
-  shows "\<exists>a N. M = N + {#a#}"
+  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 = M - {#a#} + {#a#}" by simp
+  then have "M = add_mset a (M - {#a#})" by simp
   then show ?thesis by blast
 qed
 
@@ -1195,24 +1386,24 @@
 
 theorem multiset_induct [case_names empty add, induct type: multiset]:
   assumes empty: "P {#}"
-  assumes add: "\<And>M x. P M \<Longrightarrow> P (M + {#x#})"
+  assumes add: "\<And>x M. P M \<Longrightarrow> P (add_mset x M)"
   shows "P M"
 proof (induct n \<equiv> "size M" arbitrary: M)
   case 0 thus "P M" by (simp add: empty)
 next
   case (Suc k)
-  obtain N x where "M = N + {#x#}"
+  obtain N x where "M = add_mset x N"
     using \<open>Suc k = size M\<close> [symmetric]
     using size_eq_Suc_imp_eq_union by fast
   with Suc add show "P M" by simp
 qed
 
-lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = A + {#a#}"
+lemma multi_nonempty_split: "M \<noteq> {#} \<Longrightarrow> \<exists>A a. M = add_mset a A"
 by (induct M) auto
 
 lemma multiset_cases [cases type]:
   obtains (empty) "M = {#}"
-    | (add) N x where "M = N + {#x#}"
+    | (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"
@@ -1227,19 +1418,19 @@
 proof (induct A arbitrary: B)
   case (empty M)
   then have "M \<noteq> {#}" by (simp add: mset_subset_empty_nonempty)
-  then obtain M' x where "M = M' + {#x#}"
+  then obtain M' x where "M = add_mset x M'"
     by (blast dest: multi_nonempty_split)
   then show ?case by simp
 next
-  case (add S x T)
+  case (add x S T)
   have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
-  have SxsubT: "S + {#x#} \<subset># T" by fact
+  have SxsubT: "add_mset x S \<subset># T" by fact
   then have "x \<in># T" and "S \<subset># T"
     by (auto dest: mset_subset_insertD)
-  then obtain T' where T: "T = T' + {#x#}"
+  then obtain T' where T: "T = add_mset x T'"
     by (blast dest: multi_member_split)
   then have "S \<subset># T'" using SxsubT
-    by (blast intro: mset_subset_add_bothsides)
+    by simp
   then have "size S < size T'" using IH by simp
   then show ?case using T by simp
 qed
@@ -1267,7 +1458,7 @@
 lemma multi_subset_induct [consumes 2, case_names empty add]:
   assumes "F \<subseteq># A"
     and empty: "P {#}"
-    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
+    and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (add_mset a F)"
   shows "P F"
 proof -
   from \<open>F \<subseteq># A\<close>
@@ -1276,8 +1467,8 @@
     show "P {#}" by fact
   next
     fix x F
-    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
-    show "P (F + {#x#})"
+    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "add_mset x F \<subseteq># A"
+    show "P (add_mset x F)"
     proof (rule insert)
       from i show "x \<in># A" by (auto dest: mset_subset_eq_insertD)
       from i have "F \<subseteq># A" by (auto dest: mset_subset_eq_insertD)
@@ -1299,51 +1490,41 @@
 context comp_fun_commute
 begin
 
-lemma fold_mset_insert: "fold_mset f s (M + {#x#}) = f x (fold_mset f s M)"
+lemma fold_mset_add_mset [simp]: "fold_mset f s (add_mset x M) = f x (fold_mset f s M)"
 proof -
   interpret mset: comp_fun_commute "\<lambda>y. f y ^^ count M y"
     by (fact comp_fun_commute_funpow)
-  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (M + {#x#}) y"
+  interpret mset_union: comp_fun_commute "\<lambda>y. f y ^^ count (add_mset x M) y"
     by (fact comp_fun_commute_funpow)
   show ?thesis
   proof (cases "x \<in> set_mset M")
     case False
-    then have *: "count (M + {#x#}) x = 1"
+    then have *: "count (add_mset x M) x = 1"
       by (simp add: not_in_iff)
-    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s (set_mset M) =
+    from False have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s (set_mset M) =
       Finite_Set.fold (\<lambda>y. f y ^^ count M y) s (set_mset M)"
       by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
     with False * show ?thesis
-      by (simp add: fold_mset_def del: count_union)
+      by (simp add: fold_mset_def del: count_add_mset)
   next
     case True
     define N where "N = set_mset M - {x}"
     from N_def True have *: "set_mset M = insert x N" "x \<notin> N" "finite N" by auto
-    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (M + {#x#}) y) s N =
+    then have "Finite_Set.fold (\<lambda>y. f y ^^ count (add_mset x M) y) s N =
       Finite_Set.fold (\<lambda>y. f y ^^ count M y) s N"
       by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow)
-    with * show ?thesis by (simp add: fold_mset_def del: count_union) simp
+    with * show ?thesis by (simp add: fold_mset_def del: count_add_mset) simp
   qed
 qed
 
-corollary fold_mset_single [simp]: "fold_mset f s {#x#} = f x s"
-proof -
-  have "fold_mset f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp
-  then show ?thesis by simp
-qed
+corollary fold_mset_single: "fold_mset f s {#x#} = f x s"
+  by simp
 
 lemma fold_mset_fun_left_comm: "f x (fold_mset f s M) = fold_mset f (f x s) M"
-  by (induct M) (simp_all add: fold_mset_insert fun_left_comm)
+  by (induct M) (simp_all add: fun_left_comm)
 
 lemma fold_mset_union [simp]: "fold_mset f s (M + N) = fold_mset f (fold_mset f s M) N"
-proof (induct M)
-  case empty then show ?case by simp
-next
-  case (add M x)
-  have "M + {#x#} + N = (M + N) + {#x#}"
-    by (simp add: ac_simps)
-  with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm)
-qed
+  by (induct M) (simp_all add: fold_mset_fun_left_comm)
 
 lemma fold_mset_fusion:
   assumes "comp_fun_commute g"
@@ -1356,6 +1537,14 @@
 
 end
 
+lemma union_fold_mset_add_mset: "A + B = fold_mset add_mset A B"
+proof -
+  interpret comp_fun_commute add_mset
+    by standard auto
+  show ?thesis
+    by (induction B) auto
+qed
+
 text \<open>
   A note on code generation: When defining some function containing a
   subterm @{term "fold_mset F"}, code generation is not automatic. When
@@ -1370,31 +1559,32 @@
 subsection \<open>Image\<close>
 
 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
-  "image_mset f = fold_mset (plus \<circ> single \<circ> f) {#}"
-
-lemma comp_fun_commute_mset_image: "comp_fun_commute (plus \<circ> single \<circ> f)"
+  "image_mset f = fold_mset (add_mset \<circ> f) {#}"
+
+lemma comp_fun_commute_mset_image: "comp_fun_commute (add_mset \<circ> f)"
 proof
 qed (simp add: ac_simps fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   by (simp add: image_mset_def)
 
-lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}"
+lemma image_mset_single: "image_mset f {#x#} = {#f x#}"
 proof -
-  interpret comp_fun_commute "plus \<circ> single \<circ> f"
+  interpret comp_fun_commute "add_mset \<circ> f"
     by (fact comp_fun_commute_mset_image)
   show ?thesis by (simp add: image_mset_def)
 qed
 
 lemma image_mset_union [simp]: "image_mset f (M + N) = image_mset f M + image_mset f N"
 proof -
-  interpret comp_fun_commute "plus \<circ> single \<circ> f"
+  interpret comp_fun_commute "add_mset \<circ> f"
     by (fact comp_fun_commute_mset_image)
   show ?thesis by (induct N) (simp_all add: image_mset_def ac_simps)
 qed
 
-corollary image_mset_insert: "image_mset f (M + {#a#}) = image_mset f M + {#f a#}"
-  by simp
+corollary image_mset_add_mset [simp]:
+  "image_mset f (add_mset a M) = add_mset (f a) (image_mset f M)"
+  unfolding image_mset_union add_mset_add_single[of a M] by (simp add: image_mset_single)
 
 lemma set_image_mset [simp]: "set_mset (image_mset f M) = image f (set_mset M)"
   by (induct M) simp_all
@@ -1406,26 +1596,33 @@
   by (cases M) auto
 
 lemma image_mset_If:
-  "image_mset (\<lambda>x. if P x then f x else g x) A = 
+  "image_mset (\<lambda>x. if P x then f x else g x) A =
      image_mset f (filter_mset P A) + image_mset g (filter_mset (\<lambda>x. \<not>P x) A)"
   by (induction A) (auto simp: add_ac)
 
-lemma image_mset_Diff: 
+lemma image_mset_Diff:
   assumes "B \<subseteq># A"
   shows   "image_mset f (A - B) = image_mset f A - image_mset f B"
 proof -
   have "image_mset f (A - B + B) = image_mset f (A - B) + image_mset f B"
     by simp
   also from assms have "A - B + B = A"
-    by (simp add: subset_mset.diff_add) 
+    by (simp add: subset_mset.diff_add)
   finally show ?thesis by simp
 qed
 
-lemma count_image_mset: 
+lemma count_image_mset:
   "count (image_mset f A) x = (\<Sum>y\<in>f -` {x} \<inter> set_mset A. count A y)"
-  by (induction A)
-     (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
-
+proof (induction A)
+  case empty
+  then show ?case by simp
+next
+  case (add x A)
+  moreover have *: "(if x = y then Suc n else n) = n + (if x = y then 1 else 0)" for n y
+    by simp
+  ultimately show ?case
+    by (auto simp: setsum.distrib setsum.delta' intro!: setsum.mono_neutral_left)
+qed
 
 syntax (ASCII)
   "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
@@ -1486,7 +1683,7 @@
 
 primrec mset :: "'a list \<Rightarrow> 'a multiset" where
   "mset [] = {#}" |
-  "mset (a # x) = mset x + {# a #}"
+  "mset (a # x) = add_mset a (mset x)"
 
 lemma in_multiset_in_set:
   "x \<in># mset xs \<longleftrightarrow> x \<in> set xs"
@@ -1619,14 +1816,14 @@
   ultimately show ?case by simp
 qed
 
-lemma mset_insort [simp]: "mset (insort x xs) = mset xs + {#x#}"
-  by (induct xs) (simp_all add: ac_simps)
+lemma mset_insort [simp]: "mset (insort x xs) = add_mset x (mset xs)"
+  by (induct xs) simp_all
 
 lemma mset_map[simp]: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
-global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
-  defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
+global_interpretation mset_set: folding add_mset "{#}"
+  defines mset_set = "folding.F add_mset {#}"
   by standard (simp add: fun_eq_iff ac_simps)
 
 lemma count_mset_set [simp]:
@@ -1647,7 +1844,7 @@
 lemma elem_mset_set[simp, intro]: "finite A \<Longrightarrow> x \<in># mset_set A \<longleftrightarrow> x \<in> A"
   by (induct A rule: finite_induct) simp_all
 
-lemma mset_set_Union: 
+lemma mset_set_Union:
   "finite A \<Longrightarrow> finite B \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> mset_set (A \<union> B) = mset_set A + mset_set B"
   by (induction A rule: finite_induct) (auto simp: add_ac)
 
@@ -1655,12 +1852,12 @@
   "finite A \<Longrightarrow> filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
 proof (induction A rule: finite_induct)
   case (insert x A)
-  from insert.hyps have "filter_mset P (mset_set (insert x A)) = 
+  from insert.hyps have "filter_mset P (mset_set (insert x A)) =
       filter_mset P (mset_set A) + mset_set (if P x then {x} else {})"
     by (simp add: add_ac)
   also have "filter_mset P (mset_set A) = mset_set {x\<in>A. P x}"
     by (rule insert.IH)
-  also from insert.hyps 
+  also from insert.hyps
     have "\<dots> + mset_set (if P x then {x} else {}) =
             mset_set ({x \<in> A. P x} \<union> (if P x then {x} else {}))" (is "_ = mset_set ?A")
      by (intro mset_set_Union [symmetric]) simp_all
@@ -1700,7 +1897,7 @@
 qed
 
 lemma sorted_list_of_multiset_insert [simp]:
-  "sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)"
+  "sorted_list_of_multiset (add_mset x M) = List.insort x (sorted_list_of_multiset M)"
 proof -
   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
   show ?thesis by (simp add: sorted_list_of_multiset_def)
@@ -1738,36 +1935,36 @@
 lemma mset_upt [simp]: "mset [m..<n] = mset_set {m..<n}"
   by (induction n) (simp_all add: atLeastLessThanSuc add_ac)
 
-lemma image_mset_map_of: 
+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)"
 proof (induction xs)
   case (Cons x xs)
-  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} = 
-          {#the (if i = fst x then Some (snd x) else map_of xs i). 
-             i \<in># mset (map fst xs)#} + {#snd x#}" (is "_ = ?A + _") by simp
+  have "{#the (map_of (x # xs) i). i \<in># mset (map fst (x # xs))#} =
+          add_mset (snd x) {#the (if i = fst x then Some (snd x) else map_of xs i).
+             i \<in># mset (map fst xs)#}" (is "_ = add_mset _ ?A") by simp
   also from Cons.prems have "?A = {#the (map_of xs i). i :# mset (map fst xs)#}"
     by (cases x, intro image_mset_cong) (auto simp: in_multiset_in_set)
   also from Cons.prems have "\<dots> = mset (map snd xs)" by (intro Cons.IH) simp_all
   finally show ?case by simp
-qed simp_all  
+qed simp_all
 
 
 subsection \<open>Replicate operation\<close>
 
 definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
-  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
+  "replicate_mset n x = (add_mset x ^^ n) {#}"
 
 lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
   unfolding replicate_mset_def by simp
 
-lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
+lemma replicate_mset_Suc [simp]: "replicate_mset (Suc n) x = add_mset x (replicate_mset n x)"
   unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
 
 lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
   unfolding replicate_mset_def by (induct n) auto
 
 lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
-  unfolding replicate_mset_def by (induct n) simp_all
+  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)
@@ -1821,12 +2018,15 @@
     by (induct N) (simp_all add: left_commute eq_fold)
 qed
 
+lemma add_mset [simp]: "F (add_mset x N) = x \<^bold>* F N"
+  unfolding add_mset_add_single[of x N] union by (simp add: ac_simps)
+
 end
 
 lemma comp_fun_commute_plus_mset[simp]: "comp_fun_commute (op + :: 'a multiset \<Rightarrow> _ \<Rightarrow> _)"
   by standard (simp add: add_ac comp_def)
 
-declare comp_fun_commute.fold_mset_insert[OF comp_fun_commute_plus_mset, simp]
+declare comp_fun_commute.fold_mset_add_mset[OF comp_fun_commute_plus_mset, simp]
 
 lemma in_mset_fold_plus_iff[iff]: "x \<in># fold_mset (op +) M NN \<longleftrightarrow> x \<in># M \<or> (\<exists>N. N \<in># NN \<and> x \<in># N)"
   by (induct NN) auto
@@ -1862,9 +2062,10 @@
 proof (induct M)
   case empty then show ?case by simp
 next
-  case (add M x) then show ?case
+  case (add x M) then show ?case
     by (cases "x \<in> set_mset M")
-      (simp_all add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb not_in_iff)
+      (simp_all add: size_multiset_overloaded_eq not_in_iff setsum.If_cases Diff_eq[symmetric]
+        setsum.remove)
 qed
 
 lemma size_mset_set [simp]: "size (mset_set A) = card A"
@@ -1945,8 +2146,8 @@
   assumes "x \<in># A"
   shows "x dvd msetprod A"
 proof -
-  from assms have "A = (A - {#x#}) + {#x#}" by simp
-  then obtain B where "A = B + {#x#}" ..
+  from assms have "A = add_mset x (A - {#x#})" by simp
+  then obtain B where "A = add_mset x B" ..
   then show ?thesis by simp
 qed
 
@@ -1966,8 +2167,7 @@
 lemma (in semidom_divide) msetprod_minus:
   assumes "a \<in># A" and "a \<noteq> 0"
   shows "msetprod (A - {#a#}) = msetprod A div a"
-  using assms msetprod_diff [of "{#a#}" A]
-    by (auto simp add: single_subset_iff)
+  using assms msetprod_diff [of "{#a#}" A] by auto
 
 lemma (in normalization_semidom) normalized_msetprodI:
   assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
@@ -1983,8 +2183,8 @@
 begin
 
 lemma mset_insort [simp]:
-  "mset (insort_key k x xs) = {#x#} + mset xs"
-  by (induct xs) (simp_all add: ac_simps)
+  "mset (insort_key k x xs) = add_mset x (mset xs)"
+  by (induct xs) simp_all
 
 lemma mset_sort [simp]:
   "mset (sort_key k xs) = mset xs"
@@ -2165,7 +2365,7 @@
   by (induct xs) (auto intro: subset_mset.order_trans)
 
 lemma mset_update:
-  "i < length ls \<Longrightarrow> mset (ls[i := v]) = mset ls - {#ls ! i#} + {#v#}"
+  "i < length ls \<Longrightarrow> mset (ls[i := v]) = add_mset v (mset ls - {#ls ! i#})"
 proof (induct ls arbitrary: i)
   case Nil then show ?case by simp
 next
@@ -2176,14 +2376,7 @@
   next
     case (Suc i')
     with Cons show ?thesis
-      apply simp
-      apply (subst add.assoc)
-      apply (subst add.commute [of "{#v#}" "{#x#}"])
-      apply (subst add.assoc [symmetric])
-      apply simp
-      apply (rule mset_subset_eq_multiset_union_diff_commute)
-      apply (simp add: mset_subset_eq_single nth_mem_mset)
-      done
+      by (cases \<open>x = xs ! i'\<close>) auto
   qed
 qed
 
@@ -2198,20 +2391,20 @@
 subsubsection \<open>Well-foundedness\<close>
 
 definition mult1 :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
-  "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
+  "mult1 r = {(N, M). \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and>
       (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r)}"
 
 definition mult :: "('a \<times> 'a) set \<Rightarrow> ('a multiset \<times> 'a multiset) set" where
   "mult r = (mult1 r)\<^sup>+"
 
 lemma mult1I:
-  assumes "M = M0 + {#a#}" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
+  assumes "M = add_mset a M0" and "N = M0 + K" and "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   shows "(N, M) \<in> mult1 r"
   using assms unfolding mult1_def by blast
 
 lemma mult1E:
   assumes "(N, M) \<in> mult1 r"
-  obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
+  obtains a M0 K where "M = add_mset a M0" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> (b, a) \<in> r"
   using assms unfolding mult1_def by blast
 
 lemma mono_mult1:
@@ -2226,21 +2419,21 @@
 by (simp add: mult1_def)
 
 lemma less_add:
-  assumes mult1: "(N, M0 + {#a#}) \<in> mult1 r"
+  assumes mult1: "(N, add_mset a M0) \<in> mult1 r"
   shows
-    "(\<exists>M. (M, M0) \<in> mult1 r \<and> N = M + {#a#}) \<or>
+    "(\<exists>M. (M, M0) \<in> mult1 r \<and> N = add_mset a M) \<or>
      (\<exists>K. (\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r) \<and> N = M0 + K)"
 proof -
   let ?r = "\<lambda>K a. \<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r"
-  let ?R = "\<lambda>N M. \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and> ?r K a"
-  obtain a' M0' K where M0: "M0 + {#a#} = M0' + {#a'#}"
+  let ?R = "\<lambda>N M. \<exists>a M0 K. M = add_mset a M0 \<and> N = M0 + K \<and> ?r K a"
+  obtain a' M0' K where M0: "add_mset a M0 = add_mset a' M0'"
     and N: "N = M0' + K"
     and r: "?r K a'"
     using mult1 unfolding mult1_def by auto
   show ?thesis (is "?case1 \<or> ?case2")
   proof -
     from M0 consider "M0 = M0'" "a = a'"
-      | K' where "M0 = K' + {#a'#}" "M0' = K' + {#a#}"
+      | K' where "M0 = add_mset a' K'" "M0' = add_mset a K'"
       by atomize_elim (simp only: add_eq_conv_ex)
     then show ?thesis
     proof cases
@@ -2250,7 +2443,7 @@
       then show ?thesis ..
     next
       case 2
-      from N 2(2) have n: "N = K' + K + {#a#}" by (simp add: ac_simps)
+      from N 2(2) have n: "N = add_mset a (K' + K)" by (simp add: ac_simps)
       with r 2(1) have "?R (K' + K) M0" by blast
       with n have ?case1 by (simp add: mult1_def)
       then show ?thesis ..
@@ -2267,21 +2460,21 @@
   {
     fix M M0 a
     assume M0: "M0 \<in> ?W"
-      and wf_hyp: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
-      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R \<longrightarrow> M + {#a#} \<in> ?W"
-    have "M0 + {#a#} \<in> ?W"
-    proof (rule accI [of "M0 + {#a#}"])
+      and wf_hyp: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. add_mset b M \<in> ?W)"
+      and acc_hyp: "\<forall>M. (M, M0) \<in> ?R \<longrightarrow> add_mset a M \<in> ?W"
+    have "add_mset a M0 \<in> ?W"
+    proof (rule accI [of "add_mset a M0"])
       fix N
-      assume "(N, M0 + {#a#}) \<in> ?R"
-      then consider M where "(M, M0) \<in> ?R" "N = M + {#a#}"
+      assume "(N, add_mset a M0) \<in> ?R"
+      then consider M where "(M, M0) \<in> ?R" "N = add_mset a M"
         | K where "\<forall>b. b \<in># K \<longrightarrow> (b, a) \<in> r" "N = M0 + K"
         by atomize_elim (rule less_add)
       then show "N \<in> ?W"
       proof cases
         case 1
-        from acc_hyp have "(M, M0) \<in> ?R \<longrightarrow> M + {#a#} \<in> ?W" ..
-        from this and \<open>(M, M0) \<in> ?R\<close> have "M + {#a#} \<in> ?W" ..
-        then show "N \<in> ?W" by (simp only: \<open>N = M + {#a#}\<close>)
+        from acc_hyp have "(M, M0) \<in> ?R \<longrightarrow> add_mset a M \<in> ?W" ..
+        from this and \<open>(M, M0) \<in> ?R\<close> have "add_mset a M \<in> ?W" ..
+        then show "N \<in> ?W" by (simp only: \<open>N = add_mset a M\<close>)
       next
         case 2
         from this(1) have "M0 + K \<in> ?W"
@@ -2289,12 +2482,12 @@
           case empty
           from M0 show "M0 + {#} \<in> ?W" by simp
         next
-          case (add K x)
+          case (add x K)
           from add.prems have "(x, a) \<in> r" by simp
-          with wf_hyp have "\<forall>M \<in> ?W. M + {#x#} \<in> ?W" by blast
+          with wf_hyp have "\<forall>M \<in> ?W. add_mset x M \<in> ?W" by blast
           moreover from add have "M0 + K \<in> ?W" by simp
-          ultimately have "(M0 + K) + {#x#} \<in> ?W" ..
-          then show "M0 + (K + {#x#}) \<in> ?W" by (simp only: add.assoc)
+          ultimately have "add_mset x (M0 + K) \<in> ?W" ..
+          then show "M0 + (add_mset x K) \<in> ?W" by simp
         qed
         then show "N \<in> ?W" by (simp only: 2(2))
       qed
@@ -2310,18 +2503,18 @@
     qed
 
     fix M a assume "M \<in> ?W"
-    from \<open>wf r\<close> have "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
+    from \<open>wf r\<close> have "\<forall>M \<in> ?W. add_mset a M \<in> ?W"
     proof induct
       fix a
-      assume r: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. M + {#b#} \<in> ?W)"
-      show "\<forall>M \<in> ?W. M + {#a#} \<in> ?W"
+      assume r: "\<And>b. (b, a) \<in> r \<Longrightarrow> (\<forall>M \<in> ?W. add_mset b M \<in> ?W)"
+      show "\<forall>M \<in> ?W. add_mset a M \<in> ?W"
       proof
         fix M assume "M \<in> ?W"
-        then show "M + {#a#} \<in> ?W"
+        then show "add_mset a M \<in> ?W"
           by (rule acc_induct) (rule tedious_reasoning [OF _ r])
       qed
     qed
-    from this and \<open>M \<in> ?W\<close> show "M + {#a#} \<in> ?W" ..
+    from this and \<open>M \<in> ?W\<close> show "add_mset a M \<in> ?W" ..
   qed
 qed
 
@@ -2335,38 +2528,38 @@
 subsubsection \<open>Closure-free presentation\<close>
 
 text \<open>One direction.\<close>
-
 lemma mult_implies_one_step:
   "trans r \<Longrightarrow> (M, N) \<in> mult r \<Longrightarrow>
     \<exists>I J K. N = I + J \<and> M = I + K \<and> J \<noteq> {#} \<and>
     (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)"
 apply (unfold mult_def mult1_def)
 apply (erule converse_trancl_induct, clarify)
- apply (rule_tac x = M0 in exI, simp, clarify)
+ apply (rule_tac x = M0 in exI, simp)
+apply clarify
 apply (case_tac "a \<in># K")
  apply (rule_tac x = I in exI)
  apply (simp (no_asm))
  apply (rule_tac x = "(K - {#a#}) + Ka" in exI)
  apply (simp (no_asm_simp) add: add.assoc [symmetric])
- apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong)
- apply (simp add: diff_union_single_conv)
- apply (simp (no_asm_use) add: trans_def)
- apply (metis (no_types, hide_lams) Multiset.diff_right_commute Un_iff diff_single_trivial multi_drop_mem_not_eq)
+ apply (drule union_single_eq_diff)
+ apply (auto simp: subset_mset.add_diff_assoc dest: in_diffD)[]
+ apply (meson transD)
 apply (subgoal_tac "a \<in># I")
  apply (rule_tac x = "I - {#a#}" in exI)
- apply (rule_tac x = "J + {#a#}" in exI)
+ apply (rule_tac x = "add_mset a J" in exI)
  apply (rule_tac x = "K + Ka" in exI)
  apply (rule conjI)
-  apply (simp add: multiset_eq_iff split: nat_diff_split)
+  apply (simp add: multiset_eq_iff union_single_eq_diff split: nat_diff_split)
  apply (rule conjI)
-  apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, simp)
+ apply (drule union_single_eq_diff)
+ apply (simp add: add.assoc subset_mset.add_diff_assoc2)
+  apply (simp)
   apply (simp add: multiset_eq_iff split: nat_diff_split)
  apply (simp (no_asm_use) add: trans_def)
-apply (subgoal_tac "a \<in># (M0 + {#a#})")
+apply (subgoal_tac "a \<in># add_mset a M0")
  apply (simp_all add: not_in_iff)
  apply blast
- apply (metis add.comm_neutral add_diff_cancel_right' count_eq_zero_iff diff_single_trivial multi_self_add_other_not_self plus_multiset.rep_eq)
-done
+by (metis (no_types, lifting) not_in_iff union_iff union_single_eq_member)
 
 lemma one_step_implies_mult_aux:
   "\<forall>I J K. size J = n \<and> J \<noteq> {#} \<and> (\<forall>k \<in> set_mset K. \<exists>j \<in> set_mset J. (k, j) \<in> r)
@@ -2375,7 +2568,6 @@
  apply auto
 apply (frule size_eq_Suc_imp_eq_union, clarify)
 apply (rename_tac "J'", simp)
-apply (erule notE, auto)
 apply (case_tac "J' = {#}")
  apply (simp add: mult_def)
  apply (rule r_into_trancl)
@@ -2383,14 +2575,18 @@
 txt \<open>Now we know @{term "J' \<noteq> {#}"}.\<close>
 apply (cut_tac M = K and P = "\<lambda>x. (x, a) \<in> r" in multiset_partition)
 apply (erule_tac P = "\<forall>k \<in> set_mset K. P k" for P in rev_mp)
-apply (erule ssubst)
 apply (simp add: Ball_def, auto)
 apply (subgoal_tac
   "((I + {# x \<in># K. (x, a) \<in> r #}) + {# x \<in># K. (x, a) \<notin> r #},
     (I + {# x \<in># K. (x, a) \<in> r #}) + J') \<in> mult r")
- prefer 2
- apply force
+prefer 2
+  apply (drule_tac x = "I + {# x \<in># K. (x, a) \<in> r#}" in spec)
+  apply (drule_tac x = "J'" in spec)
+  apply (drule_tac x = "{# x \<in># K. (x, a) \<notin> r#}" in spec)
+  apply auto[]
 apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
+apply (subst (asm)(1) add.assoc)
+apply (subst (asm)(2) multiset_partition[symmetric])
 apply (erule trancl_trans)
 apply (rule r_into_trancl)
 apply (simp add: mult1_def)
@@ -2413,12 +2609,12 @@
 proof
   assume ?L thus ?R
   proof (induct Z)
-    case (add Z z)
-    obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \<noteq> {#}"
+    case (add z Z)
+    obtain X' Y' Z' where *: "add_mset z X + Z = Z' + X'" "add_mset z Y + Z = Z' + Y'" "Y' \<noteq> {#}"
       "\<forall>x \<in> set_mset X'. \<exists>y \<in> set_mset Y'. (x, y) \<in> s"
-      using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast
-    consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
-      using *(1,2) by (metis mset_add union_iff union_single_eq_member)
+      using mult_implies_one_step[OF `trans s` add(2)] by auto
+    consider Z2 where "Z' = add_mset z Z2" | X2 Y2 where "X' = add_mset z X2" "Y' = add_mset z Y2"
+      using *(1,2) by (metis add_mset_remove_trivial_If insert_iff set_mset_add_mset_insert union_iff)
     thus ?case
     proof (cases)
       case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
@@ -2508,10 +2704,10 @@
 
 lemma (in preorder) mult1_lessE:
   assumes "(N, M) \<in> mult1 {(a, b). a < b}"
-  obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K"
+  obtains a M0 K where "M = add_mset a M0" "N = M0 + K"
     "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
 proof -
-  from assms obtain a M0 K where "M = M0 + {#a#}" "N = M0 + K" and
+  from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
     *: "b \<in># K \<Longrightarrow> b < a" for b by (blast elim: mult1E)
   moreover from * [of a] have "a \<notin># K" by auto
   ultimately show thesis by (auto intro: that)
@@ -2706,10 +2902,12 @@
     fun msetT T = Type (@{type_name multiset}, [T]);
 
     fun mk_mset T [] = Const (@{const_abbrev Mempty}, msetT T)
-      | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
+      | mk_mset T [x] =
+        Const (@{const_name add_mset}, T --> msetT T --> msetT T) $ x $
+          Const (@{const_abbrev Mempty}, msetT T)
       | mk_mset T (x :: xs) =
-            Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
-                  mk_mset T [x] $ mk_mset T xs
+        Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
+          mk_mset T [x] $ mk_mset T xs
 
     fun mset_member_tac ctxt m i =
       if m <= 0 then
@@ -2759,7 +2957,7 @@
 lemma union_lcomm: "M + (N + K) = N + (M + (K::'a multiset))"
   by (fact add.left_commute)
 
-lemmas union_ac = union_assoc union_commute union_lcomm
+lemmas union_ac = union_assoc union_commute union_lcomm add_mset_commute
 
 lemma union_right_cancel: "M + K = N + K \<longleftrightarrow> M = (N::'a multiset)"
   by (fact add_right_cancel)
@@ -2816,9 +3014,8 @@
                  (if maybe_opt then [Const (Nitpick_Model.unrep_mixfix (), elem_T)] else []) of
               [] => Const (@{const_name zero_class.zero}, T)
             | ts =>
-                foldl1 (fn (t1, t2) =>
-                    Const (@{const_name plus_class.plus}, T --> T --> T) $ t1 $ t2)
-                  (map (curry (op $) (Const (@{const_name single}, elem_T --> T))) ts))
+                foldl1 (fn (s, t) => Const (@{const_name add_mset}, elem_T --> T --> T) $ s $ t)
+                  ts)
           end
       | multiset_postproc _ _ _ _ t = t
   in Nitpick_Model.register_term_postprocessor @{typ "'a multiset"} multiset_postproc end
@@ -2832,23 +3029,23 @@
 lemma [code]: "{#} = mset []"
   by simp
 
+lemma [code]: "add_mset x (mset xs) = mset (x # xs)"
+  by simp
+
 lemma [code]: "Multiset.is_empty (mset xs) \<longleftrightarrow> List.null xs"
   by (simp add: Multiset.is_empty_def List.null_def)
 
-lemma [code]: "{#x#} = mset [x]"
-  by simp
-
 lemma union_code [code]: "mset xs + mset ys = mset (xs @ ys)"
   by simp
 
 lemma [code]: "image_mset f (mset xs) = mset (map f xs)"
-  by (simp add: mset_map)
+  by simp
 
 lemma [code]: "filter_mset f (mset xs) = mset (filter f xs)"
   by (simp add: mset_filter)
 
 lemma [code]: "mset xs - mset ys = mset (fold remove1 ys xs)"
-  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute)
+  by (rule sym, induct ys arbitrary: xs) (simp_all add: diff_add diff_right_commute diff_diff_add)
 
 lemma [code]:
   "mset xs #\<inter> mset ys =
@@ -2930,7 +3127,7 @@
     obtain ys1 y ys2 where res: "res = (ys1,y,ys2)" by (cases res, auto)
     note Some = Some[unfolded res]
     from extract_SomeE[OF Some] have "ys = ys1 @ x # ys2" by simp
-    hence id: "mset ys = mset (ys1 @ ys2) + {#x#}"
+    hence id: "mset ys = add_mset x (mset (ys1 @ ys2))"
       by (auto simp: ac_simps)
     show ?thesis unfolding subset_eq_mset_impl.simps
       unfolding Some option.simps split
@@ -2966,7 +3163,7 @@
 lemma [code]: "msetprod (mset xs) = fold times xs 1"
 proof -
   have "\<And>x. fold times xs x = msetprod (mset xs) * x"
-    by (induct xs) (simp_all add: mult.assoc)
+    by (induct xs) (simp_all add: ac_simps)
   then show ?thesis by simp
 qed
 
@@ -3020,7 +3217,7 @@
 lemma mset_zip_take_Cons_drop_twice:
   assumes "length xs = length ys" "j \<le> length xs"
   shows "mset (zip (take j xs @ x # drop j xs) (take j ys @ y # drop j ys)) =
-    mset (zip xs ys) + {#(x, y)#}"
+    add_mset (x,y) (mset (zip xs ys))"
   using assms
 proof (induct xs ys arbitrary: x y j rule: list_induct2)
   case Nil
@@ -3040,7 +3237,7 @@
     hence "k \<le> length xs"
       using Cons.prems by auto
     hence "mset (zip (take k xs @ x # drop k xs) (take k ys @ y # drop k ys)) =
-      mset (zip xs ys) + {#(x, y)#}"
+      add_mset (x,y) (mset (zip xs ys))"
       by (rule Cons.hyps(2))
     thus ?thesis
       unfolding k by (auto simp: add.commute union_lcomm)
@@ -3063,10 +3260,10 @@
   define xsa where "xsa = take j xs' @ drop (Suc j) xs'"
   have "mset xs' = {#x#} + mset xsa"
     unfolding xsa_def using j_len nth_j
-    by (metis (no_types) ab_semigroup_add_class.add_ac(1) append_take_drop_id Cons_nth_drop_Suc
-      mset.simps(2) union_code add.commute)
+    by (metis Cons_nth_drop_Suc union_mset_add_mset_right add_mset_remove_trivial add_diff_cancel_left'
+        append_take_drop_id mset.simps(2) mset_append)
   hence ms_x: "mset xsa = mset xs"
-    by (metis Cons.prems add.commute add_right_imp_eq mset.simps(2))
+    by (simp add: Cons.prems)
   then obtain ysa where
     len_a: "length ysa = length xsa" and ms_a: "mset (zip xsa ysa) = mset (zip xs ys)"
     using Cons.hyps(2) by blast
@@ -3113,7 +3310,7 @@
 inductive pred_mset :: "('a \<Rightarrow> bool) \<Rightarrow> 'a multiset \<Rightarrow> bool"
 where
   "pred_mset P {#}"
-| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (M + {#a#})"
+| "\<lbrakk>P a; pred_mset P M\<rbrakk> \<Longrightarrow> pred_mset P (add_mset a M)"
 
 bnf "'a multiset"
   map: image_mset
@@ -3180,7 +3377,7 @@
 inductive rel_mset'
 where
   Zero[intro]: "rel_mset' R {#} {#}"
-| Plus[intro]: "\<lbrakk>R a b; rel_mset' R M N\<rbrakk> \<Longrightarrow> rel_mset' R (M + {#a#}) (N + {#b#})"
+| Plus[intro]: "\<lbrakk>R a b; rel_mset' R M N\<rbrakk> \<Longrightarrow> rel_mset' R (add_mset a M) (add_mset b N)"
 
 lemma rel_mset_Zero: "rel_mset R {#} {#}"
 unfolding rel_mset_def Grp_def by auto
@@ -3193,13 +3390,13 @@
 lemma rel_mset_Plus:
   assumes ab: "R a b"
     and MN: "rel_mset R M N"
-  shows "rel_mset R (M + {#a#}) (N + {#b#})"
+  shows "rel_mset R (add_mset a M) (add_mset b N)"
 proof -
-  have "\<exists>ya. image_mset fst y + {#a#} = image_mset fst ya \<and>
-    image_mset snd y + {#b#} = image_mset snd ya \<and>
+  have "\<exists>ya. add_mset a (image_mset fst y) = image_mset fst ya \<and>
+    add_mset b (image_mset snd y) = image_mset snd ya \<and>
     set_mset ya \<subseteq> {(x, y). R x y}"
     if "R a b" and "set_mset y \<subseteq> {(x, y). R x y}" for y
-    using that by (intro exI[of _ "y + {#(a,b)#}"]) auto
+    using that by (intro exI[of _ "add_mset (a,b) y"]) auto
   thus ?thesis
   using assms
   unfolding multiset.rel_compp_Grp Grp_def by blast
@@ -3213,8 +3410,8 @@
 
 lemma multiset_induct2[case_names empty addL addR]:
   assumes empty: "P {#} {#}"
-    and addL: "\<And>M N a. P M N \<Longrightarrow> P (M + {#a#}) N"
-    and addR: "\<And>M N a. P M N \<Longrightarrow> P M (N + {#a#})"
+    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)
@@ -3224,7 +3421,7 @@
 lemma multiset_induct2_size[consumes 1, case_names empty add]:
   assumes c: "size M = size N"
     and empty: "P {#} {#}"
-    and add: "\<And>M N a b. P M N \<Longrightarrow> P (M + {#a#}) (N + {#b#})"
+    and add: "\<And>a b M N a b. P M N \<Longrightarrow> P (add_mset a M) (add_mset b N)"
   shows "P M N"
   using c
 proof (induct M arbitrary: N rule: measure_induct_rule[of size])
@@ -3234,48 +3431,48 @@
     case True hence "N = {#}" using less.prems by auto
     thus ?thesis using True empty by auto
   next
-    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
+    case False then obtain M1 a where M: "M = add_mset a M1" by (metis multi_nonempty_split)
     have "N \<noteq> {#}" using False less.prems by auto
-    then obtain N1 b where N: "N = N1 + {#b#}" by (metis multi_nonempty_split)
+    then obtain N1 b where N: "N = add_mset b N1" by (metis multi_nonempty_split)
     have "size M1 = size N1" using less.prems unfolding M N by auto
     thus ?thesis using M N less.hyps add by auto
   qed
 qed
 
 lemma msed_map_invL:
-  assumes "image_mset f (M + {#a#}) = N"
-  shows "\<exists>N1. N = N1 + {#f a#} \<and> image_mset f M = N1"
+  assumes "image_mset f (add_mset a M) = N"
+  shows "\<exists>N1. N = add_mset (f a) N1 \<and> image_mset f M = N1"
 proof -
   have "f a \<in># N"
-    using assms multiset.set_map[of f "M + {#a#}"] by auto
-  then obtain N1 where N: "N = N1 + {#f a#}" using multi_member_split by metis
+    using assms multiset.set_map[of f "add_mset a M"] by auto
+  then obtain N1 where N: "N = add_mset (f a) N1" using multi_member_split by metis
   have "image_mset f M = N1" using assms unfolding N by simp
   thus ?thesis using N by blast
 qed
 
 lemma msed_map_invR:
-  assumes "image_mset f M = N + {#b#}"
-  shows "\<exists>M1 a. M = M1 + {#a#} \<and> f a = b \<and> image_mset f M1 = N"
+  assumes "image_mset f M = add_mset b N"
+  shows "\<exists>M1 a. M = add_mset a M1 \<and> f a = b \<and> image_mset f M1 = N"
 proof -
   obtain a where a: "a \<in># M" and fa: "f a = b"
     using multiset.set_map[of f M] unfolding assms
     by (metis image_iff union_single_eq_member)
-  then obtain M1 where M: "M = M1 + {#a#}" using multi_member_split by metis
+  then obtain M1 where M: "M = add_mset a M1" using multi_member_split by metis
   have "image_mset f M1 = N" using assms unfolding M fa[symmetric] by simp
   thus ?thesis using M fa by blast
 qed
 
 lemma msed_rel_invL:
-  assumes "rel_mset R (M + {#a#}) N"
-  shows "\<exists>N1 b. N = N1 + {#b#} \<and> R a b \<and> rel_mset R M N1"
+  assumes "rel_mset R (add_mset a M) N"
+  shows "\<exists>N1 b. N = add_mset b N1 \<and> R a b \<and> rel_mset R M N1"
 proof -
-  obtain K where KM: "image_mset fst K = M + {#a#}"
+  obtain K where KM: "image_mset fst K = add_mset a M"
     and KN: "image_mset snd K = N" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
     using assms
     unfolding multiset.rel_compp_Grp Grp_def by auto
-  obtain K1 ab where K: "K = K1 + {#ab#}" and a: "fst ab = a"
+  obtain K1 ab where K: "K = add_mset ab K1" and a: "fst ab = a"
     and K1M: "image_mset fst K1 = M" using msed_map_invR[OF KM] by auto
-  obtain N1 where N: "N = N1 + {#snd ab#}" and K1N1: "image_mset snd K1 = N1"
+  obtain N1 where N: "N = add_mset (snd ab) N1" and K1N1: "image_mset snd K1 = N1"
     using msed_map_invL[OF KN[unfolded K]] by auto
   have Rab: "R a (snd ab)" using sK a unfolding K by auto
   have "rel_mset R M N1" using sK K1M K1N1
@@ -3284,16 +3481,16 @@
 qed
 
 lemma msed_rel_invR:
-  assumes "rel_mset R M (N + {#b#})"
-  shows "\<exists>M1 a. M = M1 + {#a#} \<and> R a b \<and> rel_mset R M1 N"
+  assumes "rel_mset R M (add_mset b N)"
+  shows "\<exists>M1 a. M = add_mset a M1 \<and> R a b \<and> rel_mset R M1 N"
 proof -
-  obtain K where KN: "image_mset snd K = N + {#b#}"
+  obtain K where KN: "image_mset snd K = add_mset b N"
     and KM: "image_mset fst K = M" and sK: "set_mset K \<subseteq> {(a, b). R a b}"
     using assms
     unfolding multiset.rel_compp_Grp Grp_def by auto
-  obtain K1 ab where K: "K = K1 + {#ab#}" and b: "snd ab = b"
+  obtain K1 ab where K: "K = add_mset ab K1" and b: "snd ab = b"
     and K1N: "image_mset snd K1 = N" using msed_map_invR[OF KN] by auto
-  obtain M1 where M: "M = M1 + {#fst ab#}" and K1M1: "image_mset fst K1 = M1"
+  obtain M1 where M: "M = add_mset (fst ab) M1" and K1M1: "image_mset fst K1 = M1"
     using msed_map_invL[OF KM[unfolded K]] by auto
   have Rab: "R (fst ab) b" using sK b unfolding K by auto
   have "rel_mset R M1 N" using sK K1N K1M1
@@ -3312,8 +3509,8 @@
     case True hence "N = {#}" using c by simp
     thus ?thesis using True rel_mset'.Zero by auto
   next
-    case False then obtain M1 a where M: "M = M1 + {#a#}" by (metis multi_nonempty_split)
-    obtain N1 b where N: "N = N1 + {#b#}" and R: "R a b" and ms: "rel_mset R M1 N1"
+    case False then obtain M1 a where M: "M = add_mset a M1" by (metis multi_nonempty_split)
+    obtain N1 b where N: "N = add_mset b N1" and R: "R a b" and ms: "rel_mset R M1 N1"
       using msed_rel_invL[OF less.prems[unfolded M]] by auto
     have "rel_mset' R M1 N1" using less.hyps[of M1 N1] ms unfolding M by simp
     thus ?thesis using rel_mset'.Plus[of R a b, OF R] unfolding M N by simp