# HG changeset patch
# User haftmann
# Date 1456523051 -3600
# Node ID 9527ff088c15799d5a7604fa974242f8b75b87a8
# Parent  25271ff79171c7a51182bf99f19decf241fed9fa
more succint formulation of membership for multisets, similar to lists;
discontinued ASCII notation for multiset membership;
more theorems on multisets, dropping redundant interpretation;
modernized notation;
some annotations concerning future work

diff -r 25271ff79171 -r 9527ff088c15 NEWS
--- a/NEWS	Fri Feb 26 22:15:09 2016 +0100
+++ b/NEWS	Fri Feb 26 22:44:11 2016 +0100
@@ -35,6 +35,23 @@
 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
 resemble the f.split naming convention, INCOMPATIBILITY.
 
+* Multiset membership is now expressed using set_mset rather than count.
+ASCII infix syntax ":#" has been discontinued.
+
+  - Expressions "count M a > 0" and similar simplify to membership
+    by default.
+
+  - Converting between "count M a = 0" and non-membership happens using
+    equations count_eq_zero_iff and not_in_iff.
+
+  - Rules count_inI and in_countE obtain facts of the form
+    "count M a = n" from membership.
+
+  - Rules count_in_diffI and in_diff_countE obtain facts of the form
+    "count M a = n + count N a" from membership on difference sets.
+
+INCOMPATIBILITY.
+
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
 
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -2169,9 +2169,8 @@
   have "\<exists>c cs. c \<in> carrier G \<and> set cs \<subseteq> carrier G \<and> wfactors G cs c \<and> fmset G cs = fmset G bs - fmset G as"
   proof (intro mset_wfactorsEx, simp)
     fix X
-    assume "count (fmset G as) X < count (fmset G bs) X"
-    hence "0 < count (fmset G bs) X" by simp
-    hence "X \<in> set_mset (fmset G bs)" by simp
+    assume "X \<in># fmset G bs - fmset G as"
+    hence "X \<in># fmset G bs" by (rule in_diffD)
     hence "X \<in> set (map (assocs G) bs)" by (simp add: fmset_def)
     hence "\<exists>x. x \<in> set bs \<and> X = assocs G x" by (induct bs) auto
     from this obtain x
@@ -2595,8 +2594,8 @@
                fmset G cs = fmset G as #\<inter> fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_mset (fmset G as #\<inter> fmset G bs)"
-    hence "X \<in> set_mset (fmset G as)" by (simp add: multiset_inter_def)
+    assume "X \<in># fmset G as #\<inter> fmset G bs"
+    hence "X \<in># fmset G as" by simp
     hence "X \<in> set (map (assocs G) as)" by (simp add: fmset_def)
     hence "\<exists>x. X = assocs G x \<and> x \<in> set as" by (induct as) auto
     from this obtain x
@@ -2673,9 +2672,9 @@
                fmset G cs = (fmset G as - fmset G bs) + fmset G bs"
   proof (intro mset_wfactorsEx)
     fix X
-    assume "X \<in> set_mset ((fmset G as - fmset G bs) + fmset G bs)"
-    hence "X \<in> set_mset (fmset G as) \<or> X \<in> set_mset (fmset G bs)"
-       by (cases "X :# fmset G bs", simp, simp)
+    assume "X \<in># (fmset G as - fmset G bs) + fmset G bs"
+    hence "X \<in># fmset G as \<or> X \<in># fmset G bs"
+      by (auto dest: in_diffD)
     moreover
     {
       assume "X \<in> set_mset (fmset G as)"
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -25,12 +25,6 @@
 
 setup_lifting type_definition_multiset
 
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
-  where "a \<in># M \<equiv> 0 < count M a"
-
-notation (ASCII)
-  Melem  ("(_/ :# _)" [50, 51] 50)  (* FIXME !? *)
-
 lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
   by (simp only: count_inject [symmetric] fun_eq_iff)
 
@@ -114,29 +108,154 @@
 
 subsection \<open>Basic operations\<close>
 
+subsubsection \<open>Conversion to set and membership\<close>
+
+definition set_mset :: "'a multiset \<Rightarrow> 'a set"
+  where "set_mset M = {x. count M x > 0}"
+
+abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
+  where "a \<in># M \<equiv> a \<in> set_mset M"
+
+abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<notin>#" 50)
+  where "a \<notin># M \<equiv> a \<notin> set_mset M"
+
+context
+begin
+
+qualified abbreviation Ball :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "Ball M \<equiv> Set.Ball (set_mset M)"
+
+qualified abbreviation Bex :: "'a multiset \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  where "Bex M \<equiv> Set.Bex (set_mset M)"
+
+end
+
+syntax
+  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
+  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)
+
+translations
+  "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
+  "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"
+
+lemma count_eq_zero_iff:
+  "count M x = 0 \<longleftrightarrow> x \<notin># M"
+  by (auto simp add: set_mset_def)
+
+lemma not_in_iff:
+  "x \<notin># M \<longleftrightarrow> count M x = 0"
+  by (auto simp add: count_eq_zero_iff)
+
+lemma count_greater_zero_iff [simp]:
+  "count M x > 0 \<longleftrightarrow> x \<in># M"
+  by (auto simp add: set_mset_def)
+
+lemma count_inI:
+  assumes "count M x = 0 \<Longrightarrow> False"
+  shows "x \<in># M"
+proof (rule ccontr)
+  assume "x \<notin># M"
+  with assms show False by (simp add: not_in_iff)
+qed
+
+lemma in_countE:
+  assumes "x \<in># M"
+  obtains n where "count M x = Suc n"
+proof -
+  from assms have "count M x > 0" by simp
+  then obtain n where "count M x = Suc n"
+    using gr0_conv_Suc by blast
+  with that show thesis .
+qed
+
+lemma count_greater_eq_Suc_zero_iff [simp]:
+  "count M x \<ge> Suc 0 \<longleftrightarrow> x \<in># M"
+  by (simp add: Suc_le_eq)
+
+lemma count_greater_eq_one_iff [simp]:
+  "count M x \<ge> 1 \<longleftrightarrow> x \<in># M"
+  by simp
+
+lemma set_mset_empty [simp]:
+  "set_mset {#} = {}"
+  by (simp add: set_mset_def)
+
+lemma set_mset_single [simp]:
+  "set_mset {#b#} = {b}"
+  by (simp add: set_mset_def)
+
+lemma set_mset_eq_empty_iff [simp]:
+  "set_mset M = {} \<longleftrightarrow> M = {#}"
+  by (auto simp add: multiset_eq_iff count_eq_zero_iff)
+
+lemma finite_set_mset [iff]:
+  "finite (set_mset M)"
+  using count [of M] by (simp add: multiset_def)
+
+
 subsubsection \<open>Union\<close>
 
-lemma count_union [simp]: "count (M + N) a = count M a + count N a"
+lemma count_union [simp]:
+  "count (M + N) a = count M a + count N a"
   by (simp add: plus_multiset.rep_eq)
 
+lemma set_mset_union [simp]:
+  "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
+
 
 subsubsection \<open>Difference\<close>
 
-instantiation multiset :: (type) comm_monoid_diff
-begin
-
-instance
-  by (standard; transfer; simp add: fun_eq_iff)
-
-end
-
-lemma count_diff [simp]: "count (M - N) a = count M a - count N a"
+instance multiset :: (type) comm_monoid_diff
+  by standard (transfer; simp add: fun_eq_iff)
+
+lemma count_diff [simp]:
+  "count (M - N) a = count M a - count N a"
   by (simp add: minus_multiset.rep_eq)
 
+lemma in_diff_count:
+  "a \<in># M - N \<longleftrightarrow> count N a < count M a"
+  by (simp add: set_mset_def)
+
+lemma count_in_diffI:
+  assumes "\<And>n. count N x = n + count M x \<Longrightarrow> False"
+  shows "x \<in># M - N"
+proof (rule ccontr)
+  assume "x \<notin># M - N"
+  then have "count N x = (count N x - count M x) + count M x"
+    by (simp add: in_diff_count not_less)
+  with assms show False by auto
+qed
+
+lemma in_diff_countE:
+  assumes "x \<in># M - N"
+  obtains n where "count M x = Suc n + count N x"
+proof -
+  from assms have "count M x - count N x > 0" by (simp add: in_diff_count)
+  then have "count M x > count N x" by simp
+  then obtain n where "count M x = Suc n + count N x"
+    using less_iff_Suc_add by auto
+  with that show thesis .
+qed
+
+lemma in_diffD:
+  assumes "a \<in># M - N"
+  shows "a \<in># M"
+proof -
+  have "0 \<le> count N a" by simp
+  also from assms have "count N a < count M a"
+    by (simp add: in_diff_count)
+  finally show ?thesis by simp
+qed
+
+lemma set_mset_diff:
+  "set_mset (M - N) = {a. count N a < count M a}"
+  by (simp add: set_mset_def)
+
 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 [simp]: "A - A = {#}"
   by (fact Groups.diff_cancel)
 
 lemma diff_union_cancelR [simp]: "M + N - N = (M::'a multiset)"
@@ -164,8 +283,22 @@
 lemma diff_union_swap: "a \<noteq> b \<Longrightarrow> M - {#a#} + {#b#} = M + {#b#} - {#a#}"
   by (auto simp add: multiset_eq_iff)
 
-lemma diff_union_single_conv: "a \<in># J \<Longrightarrow> I + J - {#a#} = I + (J - {#a#})"
-  by (simp add: multiset_eq_iff)
+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#}"
+proof -
+  from assms have "A = (A - {#a#}) + {#a#}"
+    by simp
+  with that show thesis .
+qed
+
+lemma union_iff:
+  "a \<in># A + B \<longleftrightarrow> a \<in># A \<or> a \<in># B"
+  by auto
 
 
 subsubsection \<open>Equality of multisets\<close>
@@ -186,7 +319,7 @@
   by (auto simp add: multiset_eq_iff)
 
 lemma diff_single_trivial: "\<not> x \<in># M \<Longrightarrow> M - {#x#} = M"
-  by (auto simp add: multiset_eq_iff)
+  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#}"
   by auto
@@ -197,12 +330,13 @@
 lemma union_single_eq_member: "M + {#x#} = N \<Longrightarrow> x \<in># N"
   by auto
 
-lemma union_is_single: "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N={#} \<or> M = {#} \<and> N = {#a#}"
+lemma union_is_single:
+  "M + N = {#a#} \<longleftrightarrow> M = {#a#} \<and> N = {#} \<or> M = {#} \<and> N = {#a#}"
   (is "?lhs = ?rhs")
 proof
   show ?lhs if ?rhs using that by auto
   show ?rhs if ?lhs
-    using that by (simp add: multiset_eq_iff split: if_splits) (metis add_is_1)
+    by (metis Multiset.diff_cancel add.commute add_diff_cancel_left' diff_add_zero diff_single_trivial insert_DiffM that)
 qed
 
 lemma single_is_union: "{#a#} = M + N \<longleftrightarrow> {#a#} = M \<and> N = {#} \<or> M = {#} \<and> {#a#} = N"
@@ -271,17 +405,15 @@
 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
   where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
 
-abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "supseteq_mset A B == B \<subseteq># A"
-
-abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "supset_mset A B == B \<subset># A"
+abbreviation (input) supseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supseteq>#" 50)
+  where "supseteq_mset A B \<equiv> B \<subseteq># A"
+
+abbreviation (input) supset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<supset>#" 50)
+  where "supset_mset A B \<equiv> B \<subset># A"
 
 notation (input)
   subseteq_mset  (infix "\<le>#" 50) and
-  supseteq_mset  (infix "\<ge>#" 50) and
-  supseteq_mset  (infix "\<supseteq>#" 50) and
-  supset_mset  (infix "\<supset>#" 50)
+  supseteq_mset  (infix "\<ge>#" 50)
 
 notation (ASCII)
   subseteq_mset  (infix "<=#" 50) and
@@ -291,11 +423,17 @@
 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
-
-lemma mset_less_eqI: "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
+  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+
+lemma mset_less_eqI:
+  "(\<And>a. count A a \<le> count B a) \<Longrightarrow> A \<subseteq># B"
   by (simp add: subseteq_mset_def)
 
-lemma mset_le_exists_conv: "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
+lemma mset_less_eq_count:
+  "A \<subseteq># B \<Longrightarrow> count A a \<le> count B a"
+  by (simp add: subseteq_mset_def)
+
+lemma mset_le_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"])
@@ -308,87 +446,113 @@
 declare subset_mset.zero_order[simp del]
   -- \<open>this removes some simp rules not in the usual order for multisets\<close>
 
-lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<le># B + C \<longleftrightarrow> A \<le># B"
-  by (fact subset_mset.add_le_cancel_right)
-
-lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<le># C + B \<longleftrightarrow> A \<le># B"
-  by (fact subset_mset.add_le_cancel_left)
-
-lemma mset_le_mono_add: "(A::'a multiset) \<le># B \<Longrightarrow> C \<le># D \<Longrightarrow> A + C \<le># B + D"
-  by (fact subset_mset.add_mono)
-
-lemma mset_le_add_left [simp]: "(A::'a multiset) \<le># A + B"
-  unfolding subseteq_mset_def by auto
-
-lemma mset_le_add_right [simp]: "B \<le># (A::'a multiset) + B"
-  unfolding subseteq_mset_def by auto
-
-lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<le># B"
-  by (simp add: subseteq_mset_def)
-
+lemma mset_le_mono_add_right_cancel [simp]: "(A::'a multiset) + C \<subseteq># B + C \<longleftrightarrow> A \<subseteq># B"
+   by (fact subset_mset.add_le_cancel_right)
+ 
+lemma mset_le_mono_add_left_cancel [simp]: "C + (A::'a multiset) \<subseteq># C + B \<longleftrightarrow> A \<subseteq># B"
+   by (fact subset_mset.add_le_cancel_left)
+ 
+lemma mset_le_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_le_add_left [simp]: "(A::'a multiset) \<subseteq># A + B"
+   unfolding subseteq_mset_def by auto
+ 
+lemma mset_le_add_right [simp]: "B \<subseteq># (A::'a multiset) + B"
+   unfolding subseteq_mset_def by auto
+ 
+lemma single_subset_iff [simp]:
+  "{#a#} \<subseteq># M \<longleftrightarrow> a \<in># M"
+  by (auto simp add: subseteq_mset_def Suc_le_eq)
+
+lemma mset_le_single: "a \<in># B \<Longrightarrow> {#a#} \<subseteq># B"
+  by (simp add: subseteq_mset_def Suc_le_eq)
+ 
 lemma multiset_diff_union_assoc:
   fixes A B C D :: "'a multiset"
-  shows "C \<le># B \<Longrightarrow> A + B - C = A + (B - C)"
-  by (simp add: subset_mset.diff_add_assoc)
-
+  shows "C \<subseteq># B \<Longrightarrow> A + B - C = A + (B - C)"
+  by (fact subset_mset.diff_add_assoc)
+ 
 lemma mset_le_multiset_union_diff_commute:
   fixes A B C D :: "'a multiset"
-  shows "B \<le># A \<Longrightarrow> A - B + C = A + C - B"
-by (simp add: subset_mset.add_diff_assoc2)
-
-lemma diff_le_self[simp]: "(M::'a multiset) - N \<le># M"
-by(simp add: subseteq_mset_def)
-
-lemma mset_lessD: "A <# B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: subset_mset_def subseteq_mset_def)
-apply (erule allE [where x = x])
-apply auto
-done
-
-lemma mset_leD: "A \<le># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: subset_mset_def subseteq_mset_def)
-apply (erule allE [where x = x])
-apply auto
-done
-
-lemma mset_less_insertD: "(A + {#x#} <# B) \<Longrightarrow> (x \<in># B \<and> A <# B)"
-apply (rule conjI)
- apply (simp add: mset_lessD)
-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
-
-lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)"
+  shows "B \<subseteq># A \<Longrightarrow> A - B + C = A + C - B"
+  by (fact subset_mset.add_diff_assoc2)
+
+lemma diff_le_self[simp]:
+  "(M::'a multiset) - N \<subseteq># M"
+  by (simp add: subseteq_mset_def)
+
+lemma mset_leD:
+  assumes "A \<subseteq># B" and "x \<in># A"
+  shows "x \<in># B"
+proof -
+  from \<open>x \<in># A\<close> have "count A x > 0" by simp
+  also from \<open>A \<subseteq># B\<close> have "count A x \<le> count B x"
+    by (simp add: subseteq_mset_def)
+  finally show ?thesis by simp
+qed
+  
+lemma mset_lessD:
+  "A \<subset># B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
+  by (auto intro: mset_leD [of A])
+
+lemma set_mset_mono:
+  "A \<subseteq># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
+  by (metis mset_leD subsetI)
+
+lemma mset_le_insertD:
+  "A + {#x#} \<subseteq># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
 apply (rule conjI)
  apply (simp add: mset_leD)
-apply (force simp: subset_mset_def subseteq_mset_def split: if_split_asm)
+ 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
 
-lemma mset_less_of_empty[simp]: "A <# {#} \<longleftrightarrow> False"
+lemma mset_less_insertD:
+  "A + {#x#} \<subset># B \<Longrightarrow> x \<in># B \<and> A \<subset># B"
+  by (rule mset_le_insertD) simp
+
+lemma mset_less_of_empty[simp]: "A \<subset># {#} \<longleftrightarrow> False"
   by (auto simp add: subseteq_mset_def subset_mset_def multiset_eq_iff)
 
-lemma empty_le[simp]: "{#} \<le># A"
-  unfolding mset_le_exists_conv by auto
-
-lemma le_empty[simp]: "(M \<le># {#}) = (M = {#})"
+lemma empty_le [simp]: "{#} \<subseteq># A"
   unfolding mset_le_exists_conv by auto
-
-lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}"
+ 
+lemma insert_subset_eq_iff:
+  "{#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
+
+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)
+
+lemma subset_eq_diff_conv:
+  "A - C \<subseteq># B \<longleftrightarrow> A \<subseteq># B + C"
+  by (simp add: subseteq_mset_def le_diff_conv)
+
+lemma le_empty [simp]: "M \<subseteq># {#} \<longleftrightarrow> M = {#}"
+  unfolding mset_le_exists_conv by auto
+
+lemma multi_psub_of_add_self[simp]: "A \<subset># A + {#x#}"
   by (auto simp: subset_mset_def subseteq_mset_def)
 
-lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False"
+lemma multi_psub_self[simp]: "(A::'a multiset) \<subset># A = False"
   by simp
 
-lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \<Longrightarrow> N <# M"
+lemma mset_less_add_bothsides: "N + {#x#} \<subset># M + {#x#} \<Longrightarrow> N \<subset># M"
   by (fact subset_mset.add_less_imp_less_right)
 
-lemma mset_less_empty_nonempty: "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
+lemma mset_less_empty_nonempty: "{#} \<subset># S \<longleftrightarrow> S \<noteq> {#}"
   by (fact subset_mset.zero_less_iff_neq_zero)
 
-lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} <# B"
-  by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
+lemma mset_less_diff_self: "c \<in># B \<Longrightarrow> B - {#c#} \<subset># B"
+  by (auto simp: subset_mset_def elim: mset_add)
 
 
 subsubsection \<open>Intersection\<close>
@@ -396,20 +560,32 @@
 definition inf_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
   multiset_inter_def: "inf_subset_mset A B = A - (A - B)"
 
-interpretation subset_mset: semilattice_inf inf_subset_mset "op \<le>#" "op <#"
+interpretation subset_mset: semilattice_inf inf_subset_mset "op \<subseteq>#" "op \<subset>#"
 proof -
   have [simp]: "m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" for m n q :: nat
     by arith
-  show "class.semilattice_inf op #\<inter> op \<le># op <#"
+  show "class.semilattice_inf op #\<inter> op \<subseteq># op \<subset>#"
     by standard (auto simp add: multiset_inter_def subseteq_mset_def)
 qed
-
+  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
 
 lemma multiset_inter_count [simp]:
   fixes A B :: "'a multiset"
   shows "count (A #\<inter> B) x = min (count A x) (count B x)"
   by (simp add: multiset_inter_def)
 
+lemma set_mset_inter [simp]:
+  "set_mset (A #\<inter> B) = set_mset A \<inter> set_mset B"
+  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] multiset_inter_count) simp
+
+lemma diff_intersect_left_idem [simp]:
+  "M - M #\<inter> N = M - N"
+  by (simp add: multiset_eq_iff min_def)
+
+lemma diff_intersect_right_idem [simp]:
+  "M - N #\<inter> M = M - N"
+  by (simp add: multiset_eq_iff min_def)
+
 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
   by (rule multiset_eqI) auto
 
@@ -421,11 +597,37 @@
   from assms have "min (count B x) (count C x) = 0"
     by (auto simp add: multiset_eq_iff)
   then have "count B x = 0 \<or> count C x = 0"
-    by auto
+    unfolding min_def by (auto split: if_splits)
   then show "count (A + B - C) x = count (A - C + B) x"
     by auto
 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
+
 lemma empty_inter [simp]: "{#} #\<inter> M = {#}"
   by (simp add: multiset_eq_iff)
 
@@ -433,55 +635,123 @@
   by (simp add: multiset_eq_iff)
 
 lemma inter_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<inter> N = M #\<inter> N"
-  by (simp add: multiset_eq_iff)
+  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#}"
-  by (simp add: multiset_eq_iff)
+  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"
-  by (simp add: multiset_eq_iff)
+  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#}"
-  by (simp add: multiset_eq_iff)
+  by (auto simp add: multiset_eq_iff elim: mset_add)
+
+lemma disjunct_set_mset_diff:
+  assumes "M #\<inter> N = {#}"
+  shows "set_mset (M - N) = set_mset M"
+proof (rule set_eqI)
+  fix a
+  from assms have "a \<notin># M \<or> a \<notin># N"
+    by (simp add: disjunct_not_in)
+  then show "a \<in># M - N \<longleftrightarrow> a \<in># M"
+    by (auto dest: in_diffD) (simp add: in_diff_count not_in_iff)
+qed
+
+lemma at_most_one_mset_mset_diff:
+  assumes "a \<notin># M - {#a#}"
+  shows "set_mset (M - {#a#}) = set_mset M - {a}"
+  using assms by (auto simp add: not_in_iff in_diff_count set_eq_iff)
+
+lemma more_than_one_mset_mset_diff:
+  assumes "a \<in># M - {#a#}"
+  shows "set_mset (M - {#a#}) = set_mset M"
+proof (rule set_eqI)
+  fix b
+  have "Suc 0 < count M b \<Longrightarrow> count M b > 0" by arith
+  then show "b \<in># M - {#a#} \<longleftrightarrow> b \<in># M"
+    using assms by (auto simp add: in_diff_count)
+qed
+
+lemma inter_iff:
+  "a \<in># A #\<inter> B \<longleftrightarrow> a \<in># A \<and> a \<in># B"
+  by simp
+
+lemma inter_union_distrib_left:
+  "A #\<inter> B + C = (A + C) #\<inter> (B + C)"
+  by (simp add: multiset_eq_iff min_add_distrib_left)
+
+lemma inter_union_distrib_right:
+  "C + A #\<inter> B = (C + A) #\<inter> (C + B)"
+  using inter_union_distrib_left [of A B C] by (simp add: ac_simps)
+
+lemma inter_subset_eq_union:
+  "A #\<inter> B \<subseteq># A + B"
+  by (auto simp add: subseteq_mset_def)
 
 
 subsubsection \<open>Bounded union\<close>
 
 definition sup_subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset"(infixl "#\<union>" 70)
-  where "sup_subset_mset A B = A + (B - A)"
-
-interpretation subset_mset: semilattice_sup sup_subset_mset "op \<le>#" "op <#"
+  where "sup_subset_mset A B = A + (B - A)" -- \<open>FIXME irregular fact name\<close>
+
+interpretation subset_mset: semilattice_sup sup_subset_mset "op \<subseteq>#" "op \<subset>#"
 proof -
   have [simp]: "m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" for m n q :: nat
     by arith
-  show "class.semilattice_sup op #\<union> op \<le># op <#"
+  show "class.semilattice_sup op #\<union> op \<subseteq># op \<subset>#"
     by standard (auto simp add: sup_subset_mset_def subseteq_mset_def)
 qed
-
-lemma sup_subset_mset_count [simp]: "count (A #\<union> B) x = max (count A x) (count B x)"
+  -- \<open>FIXME: avoid junk stemming from type class interpretation\<close>
+
+lemma sup_subset_mset_count [simp]: -- \<open>FIXME irregular fact name\<close>
+  "count (A #\<union> B) x = max (count A x) (count B x)"
   by (simp add: sup_subset_mset_def)
 
+lemma set_mset_sup [simp]:
+  "set_mset (A #\<union> B) = set_mset A \<union> set_mset B"
+  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] sup_subset_mset_count)
+    (auto simp add: not_in_iff elim: mset_add)
+
 lemma empty_sup [simp]: "{#} #\<union> M = M"
   by (simp add: multiset_eq_iff)
 
 lemma sup_empty [simp]: "M #\<union> {#} = M"
   by (simp add: multiset_eq_iff)
 
-lemma sup_add_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
+lemma sup_union_left1: "\<not> x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> N) + {#x#}"
+  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#}"
   by (simp add: multiset_eq_iff)
 
-lemma sup_add_left2: "x \<in># N \<Longrightarrow> (M + {#x#}) #\<union> N = (M #\<union> (N - {#x#})) + {#x#}"
+lemma sup_union_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
+  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#}"
   by (simp add: multiset_eq_iff)
 
-lemma sup_add_right1: "\<not> x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = (N #\<union> M) + {#x#}"
-  by (simp add: multiset_eq_iff)
-
-lemma sup_add_right2: "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
-  by (simp add: multiset_eq_iff)
+lemma sup_union_distrib_left:
+  "A #\<union> B + C = (A + C) #\<union> (B + C)"
+  by (simp add: multiset_eq_iff max_add_distrib_left)
+
+lemma union_sup_distrib_right:
+  "C + A #\<union> B = (C + A) #\<union> (C + B)"
+  using sup_union_distrib_left [of A B C] by (simp add: ac_simps)
+
+lemma union_diff_inter_eq_sup:
+  "A + B - A #\<inter> B = A #\<union> B"
+  by (auto simp add: multiset_eq_iff)
+
+lemma union_diff_sup_eq_inter:
+  "A + B - A #\<union> B = A #\<inter> B"
+  by (auto simp add: multiset_eq_iff)
+
 
 subsubsection \<open>Subset is an order\<close>
+
 interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
 
+
 subsubsection \<open>Filter (with comprehension syntax)\<close>
 
 text \<open>Multiset comprehension\<close>
@@ -490,9 +760,21 @@
 is "\<lambda>P M. \<lambda>x. if P x then M x else 0"
 by (rule filter_preserves_multiset)
 
-lemma count_filter_mset [simp]: "count (filter_mset P M) a = (if P a then count M a else 0)"
+syntax (ASCII)
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
+syntax
+  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
+translations
+  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
+
+lemma count_filter_mset [simp]:
+  "count (filter_mset P M) a = (if P a then count M a else 0)"
   by (simp add: filter_mset.rep_eq)
 
+lemma set_mset_filter [simp]:
+  "set_mset (filter_mset P M) = {a \<in> set_mset M. P a}"
+  by (simp only: set_eq_iff count_greater_zero_iff [symmetric] count_filter_mset) simp
+
 lemma filter_empty_mset [simp]: "filter_mset P {#} = {#}"
   by (rule multiset_eqI) simp
 
@@ -508,60 +790,44 @@
 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 multiset_filter_subset[simp]: "filter_mset f M \<le># M"
+lemma multiset_filter_subset[simp]: "filter_mset f M \<subseteq># M"
   by (simp add: mset_less_eqI)
 
 lemma multiset_filter_mono:
-  assumes "A \<le># B"
-  shows "filter_mset f A \<le># filter_mset f B"
+  assumes "A \<subseteq># B"
+  shows "filter_mset f A \<subseteq># filter_mset f B"
 proof -
   from assms[unfolded mset_le_exists_conv]
   obtain C where B: "B = A + C" by auto
   show ?thesis unfolding B by auto
 qed
 
-syntax (ASCII)
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
-syntax
-  "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
-translations
-  "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
-
-
-subsubsection \<open>Set of elements\<close>
-
-definition set_mset :: "'a multiset \<Rightarrow> 'a set"
-  where "set_mset M = {x. x \<in># M}"
-
-lemma set_mset_empty [simp]: "set_mset {#} = {}"
-by (simp add: set_mset_def)
-
-lemma set_mset_single [simp]: "set_mset {#b#} = {b}"
-by (simp add: set_mset_def)
-
-lemma set_mset_union [simp]: "set_mset (M + N) = set_mset M \<union> set_mset N"
-by (auto simp add: set_mset_def)
-
-lemma set_mset_eq_empty_iff [simp]: "(set_mset M = {}) = (M = {#})"
-by (auto simp add: set_mset_def multiset_eq_iff)
-
-lemma mem_set_mset_iff [simp]: "(x \<in> set_mset M) = (x \<in># M)"
-by (auto simp add: set_mset_def)
-
-lemma set_mset_filter [simp]: "set_mset {# x\<in>#M. P x #} = set_mset M \<inter> {x. P x}"
-by (auto simp add: set_mset_def)
-
-lemma finite_set_mset [iff]: "finite (set_mset M)"
-  using count [of M] by (simp add: multiset_def set_mset_def)
-
-lemma finite_Collect_mem [iff]: "finite {x. x \<in># M}"
-  unfolding set_mset_def[symmetric] by simp
-
-lemma set_mset_mono: "A \<le># B \<Longrightarrow> set_mset A \<subseteq> set_mset B"
-  by (metis mset_leD subsetI mem_set_mset_iff)
-
-lemma ball_set_mset_iff: "(\<forall>x \<in> set_mset M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
-  by auto
+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")
+proof
+  assume ?P then show ?Q by auto (simp add: multiset_eq_iff in_diff_count)
+next
+  assume ?Q
+  then obtain Q where M: "M = N + Q"
+    by (auto simp add: mset_le_exists_conv)
+  then have MN: "M - N = Q" by simp
+  show ?P
+  proof (rule multiset_eqI)
+    fix a
+    from \<open>?Q\<close> MN have *: "\<not> P a \<Longrightarrow> a \<notin># N" "P a \<Longrightarrow> a \<notin># Q"
+      by auto
+    show "count (filter_mset P M) a = count N a"
+    proof (cases "a \<in># M")
+      case True
+      with * show ?thesis
+        by (simp add: not_in_iff M)
+    next
+      case False then have "count M a = 0"
+        by (simp add: not_in_iff)
+      with M show ?thesis by simp
+    qed 
+  qed
+qed
 
 
 subsubsection \<open>Size\<close>
@@ -602,10 +868,8 @@
 
 lemma setsum_wcount_Int:
   "finite A \<Longrightarrow> setsum (wcount f N) (A \<inter> set_mset N) = setsum (wcount f N) A"
-apply (induct rule: finite_induct)
- apply simp
-apply (simp add: Int_insert_left set_mset_def wcount_def)
-done
+  by (induct rule: finite_induct)
+    (simp_all add: Int_insert_left wcount_def count_eq_zero_iff)
 
 lemma size_multiset_union [simp]:
   "size_multiset f (M + N::'a multiset) = size_multiset f M + size_multiset f N"
@@ -617,8 +881,9 @@
 lemma size_union [simp]: "size (M + N::'a multiset) = size M + size N"
 by (auto simp add: size_multiset_overloaded_def)
 
-lemma size_multiset_eq_0_iff_empty [iff]: "(size_multiset f M = 0) = (M = {#})"
-by (auto simp add: size_multiset_eq multiset_eq_iff)
+lemma size_multiset_eq_0_iff_empty [iff]:
+  "size_multiset f M = 0 \<longleftrightarrow> M = {#}"
+  by (auto simp add: size_multiset_eq count_eq_zero_iff)
 
 lemma size_eq_0_iff_empty [iff]: "(size M = 0) = (M = {#})"
 by (auto simp add: size_multiset_overloaded_def)
@@ -644,7 +909,7 @@
 
 lemma size_mset_mono:
   fixes A B :: "'a multiset"
-  assumes "A \<le># B"
+  assumes "A \<subseteq># B"
   shows "size A \<le> size B"
 proof -
   from assms[unfolded mset_le_exists_conv]
@@ -656,9 +921,10 @@
 by (rule size_mset_mono[OF multiset_filter_subset])
 
 lemma size_Diff_submset:
-  "M \<le># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
+  "M \<subseteq># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
 by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
 
+
 subsection \<open>Induction and case splits\<close>
 
 theorem multiset_induct [case_names empty add, induct type: multiset]:
@@ -691,7 +957,7 @@
 apply auto
 done
 
-lemma mset_less_size: "(A::'a multiset) <# B \<Longrightarrow> size A < size B"
+lemma mset_less_size: "(A::'a multiset) \<subset># B \<Longrightarrow> size A < size B"
 proof (induct A arbitrary: B)
   case (empty M)
   then have "M \<noteq> {#}" by (simp add: mset_less_empty_nonempty)
@@ -700,54 +966,55 @@
   then show ?case by simp
 next
   case (add S x T)
-  have IH: "\<And>B. S <# B \<Longrightarrow> size S < size B" by fact
-  have SxsubT: "S + {#x#} <# T" by fact
-  then have "x \<in># T" and "S <# T" by (auto dest: mset_less_insertD)
+  have IH: "\<And>B. S \<subset># B \<Longrightarrow> size S < size B" by fact
+  have SxsubT: "S + {#x#} \<subset># T" by fact
+  then have "x \<in># T" and "S \<subset># T"
+    by (auto dest: mset_less_insertD)
   then obtain T' where T: "T = T' + {#x#}"
     by (blast dest: multi_member_split)
-  then have "S <# T'" using SxsubT
+  then have "S \<subset># T'" using SxsubT
     by (blast intro: mset_less_add_bothsides)
   then have "size S < size T'" using IH by simp
   then show ?case using T by simp
 qed
 
-
 lemma size_1_singleton_mset: "size M = 1 \<Longrightarrow> \<exists>a. M = {#a#}"
 by (cases M) auto
 
+
 subsubsection \<open>Strong induction and subset induction for multisets\<close>
 
 text \<open>Well-foundedness of strict subset relation\<close>
 
-lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# N}"
+lemma wf_less_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_less_size)
 done
 
 lemma full_multiset_induct [case_names less]:
-assumes ih: "\<And>B. \<forall>(A::'a multiset). A <# B \<longrightarrow> P A \<Longrightarrow> P B"
+assumes ih: "\<And>B. \<forall>(A::'a multiset). A \<subset># B \<longrightarrow> P A \<Longrightarrow> P B"
 shows "P B"
 apply (rule wf_less_mset_rel [THEN wf_induct])
 apply (rule ih, auto)
 done
 
 lemma multi_subset_induct [consumes 2, case_names empty add]:
-  assumes "F \<le># A"
+  assumes "F \<subseteq># A"
     and empty: "P {#}"
     and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
   shows "P F"
 proof -
-  from \<open>F \<le># A\<close>
+  from \<open>F \<subseteq># A\<close>
   show ?thesis
   proof (induct F)
     show "P {#}" by fact
   next
     fix x F
-    assume P: "F \<le># A \<Longrightarrow> P F" and i: "F + {#x#} \<le># A"
+    assume P: "F \<subseteq># A \<Longrightarrow> P F" and i: "F + {#x#} \<subseteq># A"
     show "P (F + {#x#})"
     proof (rule insert)
       from i show "x \<in># A" by (auto dest: mset_le_insertD)
-      from i have "F \<le># A" by (auto dest: mset_le_insertD)
+      from i have "F \<subseteq># A" by (auto dest: mset_le_insertD)
       with P show "P F" .
     qed
   qed
@@ -775,7 +1042,8 @@
   show ?thesis
   proof (cases "x \<in> set_mset M")
     case False
-    then have *: "count (M + {#x#}) x = 1" by simp
+    then have *: "count (M + {#x#}) 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) =
       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)
@@ -893,7 +1161,7 @@
 \<close>
 
 lemma in_image_mset: "y \<in># {#f x. x \<in># M#} \<longleftrightarrow> y \<in> f ` set_mset M"
-by (metis mem_set_mset_iff set_image_mset)
+by (metis set_image_mset)
 
 functor image_mset: image_mset
 proof -
@@ -949,8 +1217,8 @@
 lemma set_mset_mset[simp]: "set_mset (mset x) = set x"
 by (induct x) auto
 
-lemma mem_set_multiset_eq: "x \<in> set xs = (x \<in># mset xs)"
-by (induct xs) auto
+lemma set_mset_comp_mset [simp]: "set_mset \<circ> mset = set"
+  by (simp add: fun_eq_iff)
 
 lemma size_mset [simp]: "size (mset xs) = length xs"
   by (induct xs) simp_all
@@ -974,23 +1242,32 @@
 apply auto
 done
 
-lemma set_count_greater_0: "set x = {a. count (mset x) a > 0}"
-by (induct x) auto
-
 lemma distinct_count_atmost_1:
   "distinct x = (\<forall>a. count (mset x) a = (if a \<in> set x then 1 else 0))"
-  apply (induct x, simp, rule iffI, simp_all)
-  subgoal for a b
-    apply (rule conjI)
-    apply (simp_all add: set_mset_mset [symmetric] del: set_mset_mset)
-    apply (erule_tac x = a in allE, simp)
-    apply clarify
-    apply (erule_tac x = aa in allE, simp)
-    done
-  done
-
-lemma mset_eq_setD: "mset xs = mset ys \<Longrightarrow> set xs = set ys"
-by (rule) (auto simp add:multiset_eq_iff set_count_greater_0)
+proof (induct x)
+  case Nil then show ?case by simp
+next
+  case (Cons x xs) show ?case (is "?lhs \<longleftrightarrow> ?rhs")
+  proof
+    assume ?lhs then show ?rhs using Cons by simp
+  next
+    assume ?rhs then have "x \<notin> set xs"
+      by (simp split: if_splits)
+    moreover from \<open>?rhs\<close> have "(\<forall>a. count (mset xs) a =
+       (if a \<in> set xs then 1 else 0))"
+      by (auto split: if_splits simp add: count_eq_zero_iff)
+    ultimately show ?lhs using Cons by simp
+  qed
+qed
+
+lemma mset_eq_setD:
+  assumes "mset xs = mset ys"
+  shows "set xs = set ys"
+proof -
+  from assms have "set_mset (mset xs) = set_mset (mset ys)"
+    by simp
+  then show ?thesis by simp
+qed
 
 lemma set_eq_iff_mset_eq_distinct:
   "distinct x \<Longrightarrow> distinct y \<Longrightarrow>
@@ -1146,7 +1423,7 @@
   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) simp_all
+  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
@@ -1157,7 +1434,7 @@
 lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
   by (induct n, simp_all)
 
-lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
+lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<subseteq># M"
   by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
 
 lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
@@ -1237,7 +1514,7 @@
 
 lemma msetsum_diff:
   fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
-  shows "N \<le># M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
+  shows "N \<subseteq># M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
   by (metis add_diff_cancel_right' msetsum.union subset_mset.diff_add)
 
 lemma size_eq_msetsum: "size M = msetsum (image_mset (\<lambda>_. 1) M)"
@@ -1246,7 +1523,7 @@
 next
   case (add M x) then show ?case
     by (cases "x \<in> set_mset M")
-      (simp_all del: mem_set_mset_iff add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb, simp)
+      (simp_all add: size_multiset_overloaded_eq setsum.distrib setsum.delta' insert_absorb not_in_iff)
 qed
 
 syntax (ASCII)
@@ -1257,7 +1534,8 @@
   "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
 
 abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
-  where "\<Union># MM \<equiv> msetsum MM"
+  where "\<Union># MM \<equiv> msetsum MM" -- \<open>FIXME ambiguous notation --
+    could likewise refer to @{text "\<Squnion>#"}\<close>
 
 lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   by (induct MM) auto
@@ -1322,10 +1600,30 @@
   then show ?thesis by simp
 qed
 
-lemma (in semidom) msetprod_zero_iff:
-  "msetprod A = 0 \<longleftrightarrow> (\<exists>a\<in>set_mset A. a = 0)"
+lemma (in semidom) msetprod_zero_iff [iff]:
+  "msetprod A = 0 \<longleftrightarrow> 0 \<in># A"
   by (induct A) auto
 
+lemma (in semidom_divide) msetprod_diff:
+  assumes "B \<subseteq># A" and "0 \<notin># B"
+  shows "msetprod (A - B) = msetprod A div msetprod B"
+proof -
+  from assms obtain C where "A = B + C"
+    by (metis subset_mset.add_diff_inverse)
+  with assms show ?thesis by simp
+qed
+
+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)
+
+lemma (in normalization_semidom) normalized_msetprodI:
+  assumes "\<And>a. a \<in># A \<Longrightarrow> normalize a = a"
+  shows "normalize (msetprod A) = msetprod A"
+  using assms by (induct A) (simp_all add: normalize_mult)
+
 
 subsection \<open>Alternative representations\<close>
 
@@ -1362,8 +1660,10 @@
     by (simp add: filter_remove1)
   with Cons.prems have "sort_key f xs = remove1 x ys"
     by (auto intro!: Cons.hyps simp add: sorted_map_remove1)
-  moreover from Cons.prems have "x \<in> set ys"
-    by (auto simp add: mem_set_multiset_eq intro!: ccontr)
+  moreover from Cons.prems have "x \<in># mset ys"
+    by auto
+  then have "x \<in> set ys"
+    by simp
   ultimately show ?case using Cons.prems by (simp add: insort_key_remove1)
 qed
 
@@ -1511,7 +1811,7 @@
 
 hide_const (open) part
 
-lemma mset_remdups_le: "mset (remdups xs) \<le># mset xs"
+lemma mset_remdups_le: "mset (remdups xs) \<subseteq># mset xs"
   by (induct xs) (auto intro: subset_mset.order_trans)
 
 lemma mset_update:
@@ -1554,6 +1854,16 @@
 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"
+  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"
+  using assms unfolding mult1_def by blast
+
 lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
 by (simp add: mult1_def)
 
@@ -1672,7 +1982,7 @@
   "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 set_mset_def)
+apply (unfold mult_def mult1_def)
 apply (erule converse_trancl_induct, clarify)
  apply (rule_tac x = M0 in exI, simp, clarify)
 apply (case_tac "a \<in># K")
@@ -1683,7 +1993,7 @@
  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 blast
+ apply (metis (no_types, hide_lams) Multiset.diff_right_commute Un_iff diff_single_trivial multi_drop_mem_not_eq)
 apply (subgoal_tac "a \<in># I")
  apply (rule_tac x = "I - {#a#}" in exI)
  apply (rule_tac x = "J + {#a#}" in exI)
@@ -1694,10 +2004,10 @@
   apply (drule_tac f = "\<lambda>M. M - {#a#}" and x="S + T" for S T in arg_cong, 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 (simp_all add: not_in_iff)
  apply blast
-apply (subgoal_tac "a \<in># (M0 + {#a#})")
- apply simp
-apply (simp (no_asm))
+ 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
 
 lemma one_step_implies_mult_aux:
@@ -1711,7 +2021,7 @@
 apply (case_tac "J' = {#}")
  apply (simp add: mult_def)
  apply (rule r_into_trancl)
- apply (simp add: mult1_def set_mset_def, blast)
+ apply (simp add: mult1_def, blast)
 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)
@@ -1725,7 +2035,7 @@
 apply (simp (no_asm_use) add: add.assoc [symmetric] mult_def)
 apply (erule trancl_trans)
 apply (rule r_into_trancl)
-apply (simp add: mult1_def set_mset_def)
+apply (simp add: mult1_def)
 apply (rule_tac x = a in exI)
 apply (rule_tac x = "I + J'" in exI)
 apply (simp add: ac_simps)
@@ -1739,6 +2049,17 @@
 
 subsubsection \<open>Partial-order properties\<close>
 
+lemma (in order) mult1_lessE:
+  assumes "(N, M) \<in> mult1 {(a, b). a < b}"
+  obtains a M0 K where "M = M0 + {#a#}" "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>b. b \<in># K \<Longrightarrow> b < a" by (blast elim: mult1E)
+  moreover from this(3) [of a] have "a \<notin># K" by auto
+  ultimately show thesis by (auto intro: that)
+qed
+
 definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subset>#" 50)
   where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
 
@@ -1774,7 +2095,7 @@
     unfolding less_multiset_def mult_def by (blast intro: trancl_trans)
   show "class.order (le_multiset :: 'a multiset \<Rightarrow> _) less_multiset"
     by standard (auto simp add: le_multiset_def irrefl dest: trans)
-qed
+qed -- \<open>FIXME avoid junk stemming from type class interpretation\<close>
 
 lemma mult_less_irrefl [elim!]:
   fixes M :: "'a::order multiset"
@@ -1989,7 +2310,7 @@
 lemma multi_union_self_other_eq: "(A::'a multiset) + X = A + Y \<Longrightarrow> X = Y"
   by (fact add_left_imp_eq)
 
-lemma mset_less_trans: "(M::'a multiset) <# K \<Longrightarrow> K <# N \<Longrightarrow> M <# N"
+lemma mset_less_trans: "(M::'a multiset) \<subset># K \<Longrightarrow> K \<subset># N \<Longrightarrow> M \<subset># N"
   by (fact subset_mset.less_trans)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
@@ -2075,7 +2396,7 @@
     if x \<in> set ys then (remove1 x ys, x # zs) else (ys, zs)) xs (ys, zs))) =
       (mset xs #\<inter> mset ys) + mset zs"
     by (induct xs arbitrary: ys)
-      (auto simp add: mem_set_multiset_eq inter_add_right1 inter_add_right2 ac_simps)
+      (auto simp add: inter_add_right1 inter_add_right2 ac_simps)
   then show ?thesis by simp
 qed
 
@@ -2118,8 +2439,8 @@
      None \<Rightarrow> None
    | Some (ys1,_,ys2) \<Rightarrow> ms_lesseq_impl xs (ys1 @ ys2))"
 
-lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<le># mset ys) \<and>
-  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs <# mset ys) \<and>
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> mset xs \<subseteq># mset ys) \<and>
+  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> mset xs \<subset># mset ys) \<and>
   (ms_lesseq_impl xs ys = Some False \<longrightarrow> mset xs = mset ys)"
 proof (induct xs arbitrary: ys)
   case (Nil ys)
@@ -2131,13 +2452,13 @@
     case None
     hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
     {
-      assume "mset (x # xs) \<le># mset ys"
+      assume "mset (x # xs) \<subseteq># mset ys"
       from set_mset_mono[OF this] x have False by simp
     } note nle = this
     moreover
     {
-      assume "mset (x # xs) <# mset ys"
-      hence "mset (x # xs) \<le># mset ys" by auto
+      assume "mset (x # xs) \<subset># mset ys"
+      hence "mset (x # xs) \<subseteq># mset ys" by auto
       from nle[OF this] have False .
     }
     ultimately show ?thesis using None by auto
@@ -2156,10 +2477,10 @@
   qed
 qed
 
-lemma [code]: "mset xs \<le># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+lemma [code]: "mset xs \<subseteq># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
-lemma [code]: "mset xs <# mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+lemma [code]: "mset xs \<subset># mset ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
   using ms_lesseq_impl[of xs ys] by (cases "ms_lesseq_impl xs ys", auto)
 
 instantiation multiset :: (equal) equal
@@ -2344,8 +2665,7 @@
   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 (no_asm),
-      metis One_nat_def Un_iff count_single mem_set_mset_iff set_mset_union zero_less_Suc)
+    by (induct X) simp_all
   show "set_mset \<circ> image_mset f = op ` f \<circ> set_mset" for f
     by auto
   show "card_order natLeq"
@@ -2476,7 +2796,7 @@
 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 mem_set_mset_iff union_single_eq_member)
+    by (metis image_iff union_single_eq_member)
   then obtain M1 where M: "M = M1 + {#a#}" 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
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -77,22 +77,29 @@
 definition less_multiset\<^sub>H\<^sub>O where
   "less_multiset\<^sub>H\<^sub>O M N \<longleftrightarrow> M \<noteq> N \<and> (\<forall>y. count N y < count M y \<longrightarrow> (\<exists>x. y < x \<and> count M x < count N x))"
 
-lemma mult_imp_less_multiset\<^sub>H\<^sub>O: "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
-proof (unfold mult_def less_multiset\<^sub>H\<^sub>O_def, induct rule: trancl_induct)
+lemma mult_imp_less_multiset\<^sub>H\<^sub>O:
+  "(M, N) \<in> mult {(x, y). x < y} \<Longrightarrow> less_multiset\<^sub>H\<^sub>O M N"
+proof (unfold mult_def, induct rule: trancl_induct)
   case (base P)
-  then show ?case unfolding mult1_def by force
+  then show ?case
+    by (auto elim!: mult1_lessE simp add: count_eq_zero_iff less_multiset\<^sub>H\<^sub>O_def split: if_splits dest!: Suc_lessD)
 next
   case (step N P)
+  from step(3) have "M \<noteq> N" and
+    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x>y. count M x < count N x)"
+    by (simp_all add: less_multiset\<^sub>H\<^sub>O_def)
   from step(2) obtain M0 a K where
-    *: "P = M0 + {#a#}" "N = M0 + K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
-    unfolding mult1_def by blast
-  then have count_K_a: "count K a = 0" by auto
-  with step(3) *(1,2) have "M \<noteq> P" by (force dest: *(3) split: if_splits)
+    *: "P = M0 + {#a#}" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> b < a"
+    by (blast elim: mult1_lessE)
+  from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P" by (force dest: *(4) split: if_splits)
   moreover
   { assume "count P a \<le> count M a"
-    with count_K_a have "count N a < count M a" unfolding *(1,2) by auto
-      with step(3) obtain z where z: "z > a" "count M z < count N z" by blast
-      with * have "count N z \<le> count P z" by force
+    with \<open>a \<notin># K\<close> have "count N a < count M a" unfolding *(1,2)
+      by (auto simp add: not_in_iff)
+      with ** obtain z where z: "z > a" "count M z < count N z"
+        by blast
+      with * have "count N z \<le> count P z" 
+        by (force simp add: not_in_iff)
       with z have "\<exists>z > a. count M z < count P z" by auto
   } note count_a = this
   { fix y
@@ -106,27 +113,29 @@
       show ?thesis
       proof (cases "y \<in># K")
         case True
-        with *(3) have "y < a" by simp
+        with *(4) have "y < a" by simp
         then show ?thesis by (cases "count P a \<le> count M a") (auto dest: count_a intro: less_trans)
       next
         case False
-        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2) by simp
-        with count_y step(3) obtain z where z: "z > y" "count M z < count N z" by auto
+        with \<open>y \<noteq> a\<close> have "count P y = count N y" unfolding *(1,2)
+          by (simp add: not_in_iff)
+        with count_y ** obtain z where z: "z > y" "count M z < count N z" by auto
         show ?thesis
         proof (cases "z \<in># K")
           case True
-          with *(3) have "z < a" by simp
+          with *(4) have "z < a" by simp
           with z(1) show ?thesis
             by (cases "count P a \<le> count M a") (auto dest!: count_a intro: less_trans)
         next
           case False
-          with count_K_a have "count N z \<le> count P z" unfolding * by auto
+          with \<open>a \<notin># K\<close> have "count N z \<le> count P z" unfolding *
+            by (auto simp add: not_in_iff)
           with z show ?thesis by auto
         qed
       qed
     qed
   }
-  ultimately show ?case by blast
+  ultimately show ?case unfolding less_multiset\<^sub>H\<^sub>O_def by blast
 qed
 
 lemma less_multiset\<^sub>D\<^sub>M_imp_mult:
@@ -157,10 +166,12 @@
   proof (intro allI impI)
     fix k
     assume "k \<in># Y"
-    then have "count N k < count M k" unfolding Y_def by auto
+    then have "count N k < count M k" unfolding Y_def
+      by (auto simp add: in_diff_count)
     with \<open>less_multiset\<^sub>H\<^sub>O M N\<close> obtain a where "k < a" and "count M a < count N a"
       unfolding less_multiset\<^sub>H\<^sub>O_def by blast
-    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def by auto
+    then show "\<exists>a. a \<in># X \<and> k < a" unfolding X_def
+      by (auto simp add: in_diff_count)
   qed
 qed
 
@@ -295,12 +306,13 @@
     add.commute)+
 
 lemma ex_gt_imp_less_multiset: "(\<exists>y :: 'a :: linorder. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M #\<subset># N"
-  unfolding less_multiset\<^sub>H\<^sub>O by (metis less_irrefl less_nat_zero_code not_gr0)
-
+  unfolding less_multiset\<^sub>H\<^sub>O
+  by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
+  
 lemma ex_gt_count_imp_less_multiset:
   "(\<forall>y :: 'a :: linorder. y \<in># M + N \<longrightarrow> y \<le> x) \<Longrightarrow> count M x < count N x \<Longrightarrow> M #\<subset># N"
-  unfolding less_multiset\<^sub>H\<^sub>O by (metis add.left_neutral add_lessD1 dual_order.strict_iff_order
-    less_not_sym mset_leD mset_le_add_left)  
+  unfolding less_multiset\<^sub>H\<^sub>O
+  by (metis add_gr_0 count_union mem_Collect_eq not_gr0 not_le not_less_iff_gr_or_eq set_mset_def)
 
 lemma union_less_diff_plus: "P \<le># M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
   by (drule subset_mset.diff_add[symmetric]) (metis union_less_mono2)
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -93,7 +93,7 @@
   next
     case False
     then show ?thesis
-      by auto
+      by (auto simp add: not_in_iff)
   qed
   finally have "a ^ count M a dvd a ^ count N a * (\<Prod>i \<in> (set_mset N - {a}). i ^ count N i)" .
   moreover
@@ -111,7 +111,7 @@
 next
   case False
   then show ?thesis
-    by auto
+    by (auto simp add: not_in_iff)
 qed
 
 lemma multiset_prime_factorization_unique:
@@ -437,7 +437,7 @@
   apply (cases "n = 0")
   apply auto
   apply (frule multiset_prime_factorization)
-  apply (auto simp add: set_mset_def multiplicity_nat_def)
+  apply (auto simp add: multiplicity_nat_def count_eq_zero_iff)
   done
 
 lemma multiplicity_not_factor_nat [simp]:
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -41,7 +41,7 @@
 lemma bag_of_append [simp]: "bag_of (l@l') = bag_of l + bag_of l'"
   by (induct l) (simp_all add: ac_simps)
 
-lemma subseteq_le_multiset: "A #<=# A + B"
+lemma subseteq_le_multiset: "A #\<subseteq># A + B"
 unfolding le_multiset_def apply (cases B; simp)
 apply (rule HOL.disjI1)
 apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/UNITY/Follows.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -36,10 +36,17 @@
 lemma Follows_constant [iff]: "F \<in> (%s. c) Fols (%s. c)"
 by (simp add: Follows_def)
 
-lemma mono_Follows_o: "mono h ==> f Fols g \<subseteq> (h o f) Fols (h o g)"
-by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD]
-                   mono_Always_o [THEN [2] rev_subsetD]
-                   mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
+lemma mono_Follows_o:
+  assumes "mono h"
+  shows "f Fols g \<subseteq> (h o f) Fols (h o g)"
+proof
+  fix x
+  assume "x \<in> f Fols g"
+  with assms show "x \<in> (h \<circ> f) Fols (h \<circ> g)"
+  by (auto simp add: Follows_def mono_Increasing_o [THEN [2] rev_subsetD]
+    mono_Always_o [THEN [2] rev_subsetD]
+    mono_LeadsTo_o [THEN [2] rev_subsetD, THEN INT_D])
+qed
 
 lemma mono_Follows_apply:
      "mono h ==> f Fols g \<subseteq> (%x. h (f x)) Fols (%x. h (g x))"
@@ -173,10 +180,10 @@
 begin
 
 definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  "M' < M \<longleftrightarrow> M' #<# M"
+  "M' < M \<longleftrightarrow> M' #\<subset># M"
 
 definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-   "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
+   "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #\<subseteq># M"
 
 instance
   by standard (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
diff -r 25271ff79171 -r 9527ff088c15 src/HOL/ex/Quicksort.thy
--- a/src/HOL/ex/Quicksort.thy	Fri Feb 26 22:15:09 2016 +0100
+++ b/src/HOL/ex/Quicksort.thy	Fri Feb 26 22:44:11 2016 +0100
@@ -25,7 +25,11 @@
   by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)
 
 lemma set_quicksort [simp]: "set (quicksort xs) = set xs"
-  by (simp add: set_count_greater_0)
+proof -
+  have "set_mset (mset (quicksort xs)) = set_mset (mset xs)"
+    by simp
+  then show ?thesis by (simp only: set_mset_mset)
+qed
 
 lemma sorted_quicksort: "sorted (quicksort xs)"
   by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)