Renaming multiset operators < ~> <#,...

--- a/NEWS	Mon Jun 08 22:04:19 2015 +0200
+++ b/NEWS	Wed Jun 10 13:24:16 2015 +0200
@@ -47,6 +47,24 @@
 separate constants, and infix syntax is usually not available during
 instantiation.
 
+* Library/Multiset:
+  - Renamed multiset inclusion operators:
+      < ~> <#
+      \<subset> ~> \<subset>#
+      <= ~> <=#
+      \<le> ~> \<le>#
+      \<subseteq> ~> \<subseteq>#
+    INCOMPATIBILITY.
+  - "'a multiset" is no longer an instance of the "order",
+    "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
+    "semilattice_inf", and "semilattice_sup" type classes. The theorems
+    previously provided by these type classes (directly or indirectly)
+    are now available through the "subset_mset" interpretation
+    (e.g. add_mono ~> subset_mset.add_mono).
+    INCOMPATIBILITY.
+  - Removing mset_le_def:
+    mset_le_def ~> subseteq_mset_def
+    mset_less_def ~> subset_mset_def
 
 New in Isabelle2015 (May 2015)
 ------------------------------

--- a/src/HOL/Algebra/Divisibility.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -2137,7 +2137,7 @@
   assumes ab: "a divides b"
     and afs: "wfactors G as a" and bfs: "wfactors G bs b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
-  shows "fmset G as \<le> fmset G bs"
+  shows "fmset G as \<le># fmset G bs"
 using ab
 proof (elim dividesE)
   fix c
@@ -2157,7 +2157,7 @@
 qed
 
 lemma (in comm_monoid_cancel) fmsubset_divides:
-  assumes msubset: "fmset G as \<le> fmset G bs"
+  assumes msubset: "fmset G as \<le># fmset G bs"
     and afs: "wfactors G as a" and bfs: "wfactors G bs b"
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
@@ -2193,7 +2193,7 @@
 
   from csmset msubset
       have "fmset G bs = fmset G as + fmset G cs"
-      by (simp add: multiset_eq_iff mset_le_def)
+      by (simp add: multiset_eq_iff subseteq_mset_def)
   hence basc: "b \<sim> a \<otimes> c"
       by (rule fmset_wfactors_mult) fact+
 
@@ -2210,7 +2210,7 @@
   assumes "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G" 
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
-  shows "a divides b = (fmset G as \<le> fmset G bs)"
+  shows "a divides b = (fmset G as \<le># fmset G bs)"
 using assms
 by (blast intro: divides_fmsubset fmsubset_divides)
 
@@ -2218,7 +2218,7 @@
 text {* Proper factors on multisets *}
 
 lemma (in factorial_monoid) fmset_properfactor:
-  assumes asubb: "fmset G as \<le> fmset G bs"
+  assumes asubb: "fmset G as \<le># fmset G bs"
     and anb: "fmset G as \<noteq> fmset G bs"
     and "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G"
@@ -2228,10 +2228,10 @@
 apply (rule fmsubset_divides[of as bs], fact+)
 proof
   assume "b divides a"
-  hence "fmset G bs \<le> fmset G as"
+  hence "fmset G bs \<le># fmset G as"
       by (rule divides_fmsubset) fact+
   with asubb
-      have "fmset G as = fmset G bs" by (rule order_antisym)
+      have "fmset G as = fmset G bs" by (rule subset_mset.antisym)
   with anb
       show "False" ..
 qed
@@ -2241,7 +2241,7 @@
     and "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
-  shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
 using pf
 apply (elim properfactorE)
 apply rule
@@ -2619,13 +2619,13 @@
   have "c gcdof a b"
   proof (simp add: isgcd_def, safe)
     from csmset
-        have "fmset G cs \<le> fmset G as"
-        by (simp add: multiset_inter_def mset_le_def)
+        have "fmset G cs \<le># fmset G as"
+        by (simp add: multiset_inter_def subset_mset_def)
     thus "c divides a" by (rule fmsubset_divides) fact+
   next
     from csmset
-        have "fmset G cs \<le> fmset G bs"
-        by (simp add: multiset_inter_def mset_le_def, force)
+        have "fmset G cs \<le># fmset G bs"
+        by (simp add: multiset_inter_def subseteq_mset_def, force)
     thus "c divides b" by (rule fmsubset_divides) fact+
   next
     fix y
@@ -2637,13 +2637,13 @@
         by auto
 
     assume "y divides a"
-    hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+
+    hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
 
     assume "y divides b"
-    hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
+    hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
 
     from ya yb csmset
-    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def)
+    have "fmset G ys \<le># fmset G cs" by (simp add: subset_mset_def)
     thus "y divides c" by (rule fmsubset_divides) fact+
   qed
 
@@ -2718,10 +2718,10 @@
 
   have "c lcmof a b"
   proof (simp add: islcm_def, safe)
-    from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)
+    from csmset have "fmset G as \<le># fmset G cs" by (simp add: subseteq_mset_def, force)
     thus "a divides c" by (rule fmsubset_divides) fact+
   next
-    from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)
+    from csmset have "fmset G bs \<le># fmset G cs" by (simp add: subset_mset_def)
     thus "b divides c" by (rule fmsubset_divides) fact+
   next
     fix y
@@ -2733,14 +2733,14 @@
         by auto
 
     assume "a divides y"
-    hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+
+    hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
 
     assume "b divides y"
-    hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+
+    hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
 
     from ya yb csmset
-    have "fmset G cs \<le> fmset G ys"
-      apply (simp add: mset_le_def, clarify)
+    have "fmset G cs \<le># fmset G ys"
+      apply (simp add: subseteq_mset_def, clarify)
       apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
        apply simp
       apply simp

--- a/src/HOL/Library/DAList_Multiset.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -18,9 +18,9 @@
 
 lemma [code, code del]: "minus = (minus :: 'a multiset \<Rightarrow> _)" ..
 
-lemma [code, code del]: "inf = (inf :: 'a multiset \<Rightarrow> _)" ..
+lemma [code, code del]: "inf_subset_mset = (inf_subset_mset :: 'a multiset \<Rightarrow> _)" ..
 
-lemma [code, code del]: "sup = (sup :: 'a multiset \<Rightarrow> _)" ..
+lemma [code, code del]: "sup_subset_mset = (sup_subset_mset :: 'a multiset \<Rightarrow> _)" ..
 
 lemma [code, code del]: "image_mset = image_mset" ..
 
@@ -38,9 +38,9 @@
 
 lemma [code, code del]: "sorted_list_of_multiset = sorted_list_of_multiset" ..
 
-lemma [code, code del]: "ord_multiset_inst.less_eq_multiset = ord_multiset_inst.less_eq_multiset" ..
+lemma [code, code del]: "subset_mset = subset_mset" ..
 
-lemma [code, code del]: "ord_multiset_inst.less_multiset = ord_multiset_inst.less_multiset" ..
+lemma [code, code del]: "subseteq_mset = subseteq_mset" ..
 
 lemma [code, code del]: "equal_multiset_inst.equal_multiset = equal_multiset_inst.equal_multiset" ..
 
@@ -203,21 +203,21 @@
   by (rule multiset_eqI) (simp add: count_of_filter DAList.filter.rep_eq)
 
 
-lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le> m2 \<and> m2 \<le> m1"
-  by (metis equal_multiset_def eq_iff)
+lemma mset_eq [code]: "HOL.equal (m1::'a::equal multiset) m2 \<longleftrightarrow> m1 \<le># m2 \<and> m2 \<le># m1"
+  by (metis equal_multiset_def subset_mset.eq_iff)
 
 text \<open>By default the code for @{text "<"} is @{prop"xs < ys \<longleftrightarrow> xs \<le> ys \<and> \<not> xs = ys"}.
 With equality implemented by @{text"\<le>"}, this leads to three calls of  @{text"\<le>"}.
 Here is a more efficient version:\<close>
-lemma mset_less[code]: "xs < (ys :: 'a multiset) \<longleftrightarrow> xs \<le> ys \<and> \<not> ys \<le> xs"
-  by (rule less_le_not_le)
+lemma mset_less[code]: "xs <# (ys :: 'a multiset) \<longleftrightarrow> xs \<le># ys \<and> \<not> ys \<le># xs"
+  by (rule subset_mset.less_le_not_le)
 
 lemma mset_less_eq_Bag0:
-  "Bag xs \<le> A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
+  "Bag xs \<le># A \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). count_of (DAList.impl_of xs) x \<le> count A x)"
     (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
-  then show ?rhs by (auto simp add: mset_le_def)
+  then show ?rhs by (auto simp add: subseteq_mset_def)
 next
   assume ?rhs
   show ?lhs
@@ -225,12 +225,12 @@
     fix x
     from \<open>?rhs\<close> have "count_of (DAList.impl_of xs) x \<le> count A x"
       by (cases "x \<in> fst ` set (DAList.impl_of xs)") (auto simp add: count_of_empty)
-    then show "count (Bag xs) x \<le> count A x" by (simp add: mset_le_def)
+    then show "count (Bag xs) x \<le> count A x" by (simp add: subset_mset_def)
   qed
 qed
 
 lemma mset_less_eq_Bag [code]:
-  "Bag xs \<le> (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
+  "Bag xs \<le># (A :: 'a multiset) \<longleftrightarrow> (\<forall>(x, n) \<in> set (DAList.impl_of xs). n \<le> count A x)"
 proof -
   {
     fix x n
@@ -266,7 +266,7 @@
 qed
 
 declare multiset_inter_def [code]
-declare sup_multiset_def [code]
+declare sup_subset_mset_def [code]
 declare multiset_of.simps [code]
 
 

--- a/src/HOL/Library/Multiset.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -280,157 +280,137 @@
 
 subsubsection {* Pointwise ordering induced by count *}
 
-instantiation multiset :: (type) ordered_ab_semigroup_add_imp_le
-begin
-
-lift_definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" is "\<lambda> A B. (\<forall>a. A a \<le> B a)" .
-
-lemmas mset_le_def = less_eq_multiset_def
-
-definition less_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
-  mset_less_def: "(A::'a multiset) < B \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
-
-instance
-  by default (auto simp add: mset_le_def mset_less_def multiset_eq_iff intro: order_trans antisym)
-
-end
-
-abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
-  "A <# B \<equiv> A < B"
-abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
-  "A \<subset># B \<equiv> A < B"
-
-abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
-  "A <=# B \<equiv> A \<le> B"
-abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
-  "A \<le># B \<equiv> A \<le> B"
-abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
-  "A \<subseteq># B \<equiv> A \<le> B"
+definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
+"subseteq_mset A B \<equiv> (\<forall>a. count A a \<le> count B a)"
+
+definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
+"subset_mset A B \<equiv> (A <=# B \<and> A \<noteq> B)"
+
+notation subseteq_mset (infix "\<le>#" 50)
+notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
+
+notation (xsymbols) subset_mset (infix "\<subset>#" 50)
+
+interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op <=#" "op <#"
+  by default (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"
-  by (simp add: mset_le_def)
+  "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le># B"
+  by (simp add: subseteq_mset_def)
 
 lemma mset_le_exists_conv:
-  "(A::'a multiset) \<le> B \<longleftrightarrow> (\<exists>C. B = A + C)"
-apply (unfold mset_le_def, rule iffI, rule_tac x = "B - A" in exI)
+  "(A::'a multiset) \<le># B \<longleftrightarrow> (\<exists>C. B = A + C)"
+apply (unfold subseteq_mset_def, rule iffI, rule_tac x = "B - A" in exI)
 apply (auto intro: multiset_eq_iff [THEN iffD2])
 done
 
-instance multiset :: (type) ordered_cancel_comm_monoid_diff
+interpretation subset_mset: ordered_cancel_comm_monoid_diff  "op +" "op -" 0 "op \<le>#" "op <#"
   by default (simp, fact mset_le_exists_conv)
 
 lemma mset_le_mono_add_right_cancel [simp]:
-  "(A::'a multiset) + C \<le> B + C \<longleftrightarrow> A \<le> B"
-  by (fact add_le_cancel_right)
+  "(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 add_le_cancel_left)
+  "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 add_mono)
+  "(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 mset_le_def by auto
+  "(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 mset_le_def by auto
+  "B \<le># (A::'a multiset) + B"
+  unfolding subseteq_mset_def by auto
 
 lemma mset_le_single:
-  "a :# B \<Longrightarrow> {#a#} \<le> B"
-  by (simp add: mset_le_def)
+  "a :# B \<Longrightarrow> {#a#} \<le># B"
+  by (simp add: subseteq_mset_def)
 
 lemma multiset_diff_union_assoc:
-  "C \<le> B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
-  by (simp add: multiset_eq_iff mset_le_def)
+  "C \<le># B \<Longrightarrow> (A::'a multiset) + B - C = A + (B - C)"
+  by (simp add: subset_mset.diff_add_assoc)
 
 lemma mset_le_multiset_union_diff_commute:
-  "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
-by (simp add: multiset_eq_iff mset_le_def)
-
-lemma diff_le_self[simp]: "(M::'a multiset) - N \<le> M"
-by(simp add: mset_le_def)
-
-lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: mset_le_def mset_less_def)
+  "B \<le># A \<Longrightarrow> (A::'a multiset) - 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_tac x=x in allE)
 apply auto
 done
 
-lemma mset_leD: "A \<le> B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
-apply (clarsimp simp: mset_le_def mset_less_def)
+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_tac x = x in allE)
 apply auto
 done
 
-lemma mset_less_insertD: "(A + {#x#} < B) \<Longrightarrow> (x \<in># B \<and> A < B)"
+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: mset_le_def mset_less_def)
+apply (clarsimp simp: subset_mset_def subseteq_mset_def)
 apply safe
  apply (erule_tac x = a in allE)
  apply (auto split: split_if_asm)
 done
 
-lemma mset_le_insertD: "(A + {#x#} \<le> B) \<Longrightarrow> (x \<in># B \<and> A \<le> B)"
+lemma mset_le_insertD: "(A + {#x#} \<le># B) \<Longrightarrow> (x \<in># B \<and> A \<le># B)"
 apply (rule conjI)
  apply (simp add: mset_leD)
-apply (force simp: mset_le_def mset_less_def split: split_if_asm)
+apply (force simp: subset_mset_def subseteq_mset_def split: split_if_asm)
 done
 
-lemma mset_less_of_empty[simp]: "A < {#} \<longleftrightarrow> False"
-  by (auto simp add: mset_less_def mset_le_def multiset_eq_iff)
-
-lemma empty_le[simp]: "{#} \<le> A"
+lemma mset_less_of_empty[simp]: "A <# {#} \<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 le_empty[simp]: "(M \<le># {#}) = (M = {#})"
   unfolding mset_le_exists_conv by auto
 
-lemma multi_psub_of_add_self[simp]: "A < A + {#x#}"
-  by (auto simp: mset_le_def mset_less_def)
-
-lemma multi_psub_self[simp]: "(A::'a multiset) < A = False"
+lemma multi_psub_of_add_self[simp]: "A <# A + {#x#}"
+  by (auto simp: subset_mset_def subseteq_mset_def)
+
+lemma multi_psub_self[simp]: "(A::'a multiset) <# A = False"
   by simp
 
-lemma mset_less_add_bothsides: "N + {#x#} < M + {#x#} \<Longrightarrow> N < M"
-  by (fact add_less_imp_less_right)
+lemma mset_less_add_bothsides: "N + {#x#} <# M + {#x#} \<Longrightarrow> N <# M"
+  by (fact subset_mset.add_less_imp_less_right)
 
 lemma mset_less_empty_nonempty:
-  "{#} < S \<longleftrightarrow> S \<noteq> {#}"
-  by (auto simp: mset_le_def mset_less_def)
+  "{#} <# S \<longleftrightarrow> S \<noteq> {#}"
+  by (auto simp: subset_mset_def subseteq_mset_def)
 
 lemma mset_less_diff_self:
-  "c \<in># B \<Longrightarrow> B - {#c#} < B"
-  by (auto simp: mset_le_def mset_less_def multiset_eq_iff)
+  "c \<in># B \<Longrightarrow> B - {#c#} <# B"
+  by (auto simp: subset_mset_def subseteq_mset_def multiset_eq_iff)
 
 
 subsubsection {* Intersection *}
 
-instantiation multiset :: (type) semilattice_inf
-begin
-
-definition inf_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
-  multiset_inter_def: "inf_multiset A B = A - (A - B)"
-
-instance
+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 <#"
 proof -
-  have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
-  show "OFCLASS('a multiset, semilattice_inf_class)"
-    by default (auto simp add: multiset_inter_def mset_le_def aux)
+   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> m \<le> q \<Longrightarrow> m \<le> n - (n - q)" by arith
+   show "class.semilattice_inf op #\<inter> op \<le># op <#"
+     by default (auto simp add: multiset_inter_def subseteq_mset_def aux)
 qed
 
-end
-
-abbreviation multiset_inter :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<inter>" 70) where
-  "multiset_inter \<equiv> inf"
 
 lemma multiset_inter_count [simp]:
-  "count (A #\<inter> B) x = min (count A x) (count B x)"
+  "count ((A::'a multiset) #\<inter> B) x = min (count A x) (count B x)"
   by (simp add: multiset_inter_def)
 
 lemma multiset_inter_single: "a \<noteq> b \<Longrightarrow> {#a#} #\<inter> {#b#} = {#}"
@@ -475,28 +455,19 @@
 
 
 subsubsection {* Bounded union *}
-
-instantiation multiset :: (type) semilattice_sup
-begin
-
-definition sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" where
-  "sup_multiset A B = A + (B - A)"
-
-instance
+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 <#"
 proof -
   have aux: "\<And>m n q :: nat. m \<le> n \<Longrightarrow> q \<le> n \<Longrightarrow> m + (q - m) \<le> n" by arith
-  show "OFCLASS('a multiset, semilattice_sup_class)"
-    by default (auto simp add: sup_multiset_def mset_le_def aux)
+  show "class.semilattice_sup op #\<union> op \<le># op <#"
+    by default (auto simp add: sup_subset_mset_def subseteq_mset_def aux)
 qed
 
-end
-
-abbreviation sup_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> 'a multiset" (infixl "#\<union>" 70) where
-  "sup_multiset \<equiv> sup"
-
-lemma sup_multiset_count [simp]:
+lemma sup_subset_mset_count [simp]:
   "count (A #\<union> B) x = max (count A x) (count B x)"
-  by (simp add: sup_multiset_def)
+  by (simp add: sup_subset_mset_def)
 
 lemma empty_sup [simp]:
   "{#} #\<union> M = M"
@@ -522,6 +493,8 @@
   "x \<in># N \<Longrightarrow> N #\<union> (M + {#x#}) = ((N - {#x#}) #\<union> M) + {#x#}"
   by (simp add: multiset_eq_iff)
 
+subsubsection {*Subset is an order*}
+interpretation subset_mset: order "op \<le>#" "op <#" by unfold_locales auto
 
 subsubsection {* Filter (with comprehension syntax) *}
 
@@ -555,11 +528,11 @@
   "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"
-  unfolding less_eq_multiset.rep_eq by auto
-
-lemma multiset_filter_mono: assumes "A \<le> B"
-  shows "filter_mset f A \<le> filter_mset f B"
+lemma multiset_filter_subset[simp]: "filter_mset f M \<le># 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"
 proof -
   from assms[unfolded mset_le_exists_conv]
   obtain C where B: "B = A + C" by auto
@@ -603,7 +576,7 @@
 lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
   unfolding set_of_def[symmetric] by simp
 
-lemma set_of_mono: "A \<le> B \<Longrightarrow> set_of A \<subseteq> set_of B"
+lemma set_of_mono: "A \<le># B \<Longrightarrow> set_of A \<subseteq> set_of B"
   by (metis mset_leD subsetI mem_set_of_iff)
 
 lemma ball_set_of_iff: "(\<forall>x \<in> set_of M. P x) \<longleftrightarrow> (\<forall>x. x \<in># M \<longrightarrow> P x)"
@@ -685,7 +658,7 @@
   then show ?thesis by blast
 qed
 
-lemma size_mset_mono: assumes "A \<le> B"
+lemma size_mset_mono: assumes "A \<le># B"
   shows "size A \<le> size(B::_ multiset)"
 proof -
   from assms[unfolded mset_le_exists_conv]
@@ -697,7 +670,7 @@
 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 \<le># M' \<Longrightarrow> size (M' - M) = size M' - size(M::'a multiset)"
 by (metis add_diff_cancel_left' size_union mset_le_exists_conv)
 
 subsection {* Induction and case splits *}
@@ -732,7 +705,7 @@
 apply auto
 done
 
-lemma mset_less_size: "(A::'a multiset) < B \<Longrightarrow> size A < size B"
+lemma mset_less_size: "(A::'a multiset) <# 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)
@@ -741,12 +714,12 @@
   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 <# 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)
   then obtain T' where T: "T = T' + {#x#}"
     by (blast dest: multi_member_split)
-  then have "S < T'" using SxsubT
+  then have "S <# 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
@@ -760,35 +733,35 @@
 
 text {* Well-foundedness of strict subset relation *}
 
-lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M < N}"
+lemma wf_less_mset_rel: "wf {(M, N :: 'a multiset). M <# 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 <# 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 \<le># A"
   and empty: "P {#}"
   and insert: "\<And>a F. a \<in># A \<Longrightarrow> P F \<Longrightarrow> P (F + {#a#})"
 shows "P F"
 proof -
-  from `F \<le> A`
+  from `F \<le># A`
   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 \<le># A \<Longrightarrow> P F" and i: "F + {#x#} \<le># 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 \<le># A" by (auto dest: mset_le_insertD)
       with P show "P F" .
     qed
   qed
@@ -1280,8 +1253,8 @@
 
 lemma msetsum_diff:
   fixes M N :: "('a \<Colon> ordered_cancel_comm_monoid_diff) multiset"
-  shows "N \<le> M \<Longrightarrow> msetsum (M - N) = msetsum M - msetsum N"
-  by (metis add_diff_cancel_left' msetsum.union ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
+  shows "N \<le># 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)"
 proof (induct M)
@@ -1404,8 +1377,9 @@
 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"
-  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset less_eq_multiset.rep_eq)
+lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># 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"
   by (induct D) simp_all
@@ -1555,8 +1529,8 @@
 
 hide_const (open) part
 
-lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le> multiset_of xs"
-  by (induct xs) (auto intro: order_trans)
+lemma multiset_of_remdups_le: "multiset_of (remdups xs) \<le># multiset_of xs"
+  by (induct xs) (auto intro: subset_mset.order_trans)
 
 lemma multiset_of_update:
   "i < length ls \<Longrightarrow> multiset_of (ls[i := v]) = multiset_of ls - {#ls ! i#} + {#v#}"
@@ -2037,17 +2011,17 @@
 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"
-  by (fact order_less_trans)
+lemma mset_less_trans: "(M::'a multiset) <# K \<Longrightarrow> K <# N \<Longrightarrow> M <# N"
+  by (fact subset_mset.less_trans)
 
 lemma multiset_inter_commute: "A #\<inter> B = B #\<inter> A"
-  by (fact inf.commute)
+  by (fact subset_mset.inf.commute)
 
 lemma multiset_inter_assoc: "A #\<inter> (B #\<inter> C) = A #\<inter> B #\<inter> C"
-  by (fact inf.assoc [symmetric])
+  by (fact subset_mset.inf.assoc [symmetric])
 
 lemma multiset_inter_left_commute: "A #\<inter> (B #\<inter> C) = B #\<inter> (A #\<inter> C)"
-  by (fact inf.left_commute)
+  by (fact subset_mset.inf.left_commute)
 
 lemmas multiset_inter_ac =
   multiset_inter_commute
@@ -2182,8 +2156,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> multiset_of xs \<le> multiset_of ys) \<and>
-  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs < multiset_of ys) \<and>
+lemma ms_lesseq_impl: "(ms_lesseq_impl xs ys = None \<longleftrightarrow> \<not> multiset_of xs \<le># multiset_of ys) \<and>
+  (ms_lesseq_impl xs ys = Some True \<longleftrightarrow> multiset_of xs <# multiset_of ys) \<and>
   (ms_lesseq_impl xs ys = Some False \<longrightarrow> multiset_of xs = multiset_of ys)"
 proof (induct xs arbitrary: ys)
   case (Nil ys)
@@ -2195,13 +2169,13 @@
     case None
     hence x: "x \<notin> set ys" by (simp add: extract_None_iff)
     {
-      assume "multiset_of (x # xs) \<le> multiset_of ys"
+      assume "multiset_of (x # xs) \<le># multiset_of ys"
       from set_of_mono[OF this] x have False by simp
     } note nle = this
     moreover
     {
-      assume "multiset_of (x # xs) < multiset_of ys"
-      hence "multiset_of (x # xs) \<le> multiset_of ys" by auto
+      assume "multiset_of (x # xs) <# multiset_of ys"
+      hence "multiset_of (x # xs) \<le># multiset_of ys" by auto
       from nle[OF this] have False .
     }
     ultimately show ?thesis using None by auto
@@ -2216,14 +2190,14 @@
       unfolding Some option.simps split
       unfolding id
       using Cons[of "ys1 @ ys2"]
-      unfolding mset_le_def mset_less_def by auto
+      unfolding subset_mset_def subseteq_mset_def by auto
   qed
 qed
 
-lemma [code]: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys \<noteq> None"
+lemma [code]: "multiset_of xs \<le># multiset_of 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]: "multiset_of xs < multiset_of ys \<longleftrightarrow> ms_lesseq_impl xs ys = Some True"
+lemma [code]: "multiset_of xs <# multiset_of 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

--- a/src/HOL/Library/Multiset_Order.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -69,7 +69,7 @@
 
 definition less_multiset\<^sub>D\<^sub>M where
   "less_multiset\<^sub>D\<^sub>M M N \<longleftrightarrow>
-   (\<exists>X Y. X \<noteq> {#} \<and> X \<le> N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
+   (\<exists>X Y. X \<noteq> {#} \<and> X \<le># N \<and> M = (N - X) + Y \<and> (\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)))"
 
 
 text {* The Huet--Oppen ordering: *}
@@ -134,12 +134,12 @@
 proof -
   assume "less_multiset\<^sub>D\<^sub>M M N"
   then obtain X Y where
-    "X \<noteq> {#}" and "X \<le> N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
+    "X \<noteq> {#}" and "X \<le># N" and "M = N - X + Y" and "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
     unfolding less_multiset\<^sub>D\<^sub>M_def by blast
   then have "(N - X + Y, N - X + X) \<in> mult {(x, y). x < y}"
     by (intro one_step_implies_mult) (auto simp: Bex_def trans_def)
-  with `M = N - X + Y` `X \<le> N` show "(M, N) \<in> mult {(x, y). x < y}"
-    by (metis ordered_cancel_comm_monoid_diff_class.diff_add)
+  with `M = N - X + Y` `X \<le># N` show "(M, N) \<in> mult {(x, y). x < y}"
+    by (metis subset_mset.diff_add)
 qed
 
 lemma less_multiset\<^sub>H\<^sub>O_imp_less_multiset\<^sub>D\<^sub>M: "less_multiset\<^sub>H\<^sub>O M N \<Longrightarrow> less_multiset\<^sub>D\<^sub>M M N"
@@ -151,7 +151,7 @@
   def X \<equiv> "N - M"
   def Y \<equiv> "M - N"
   from z show "X \<noteq> {#}" unfolding X_def by (auto simp: multiset_eq_iff not_less_eq_eq Suc_le_eq)
-  from z show "X \<le> N" unfolding X_def by auto
+  from z show "X \<le># N" unfolding X_def by auto
   show "M = (N - X) + Y" unfolding X_def Y_def multiset_eq_iff count_union count_diff by force
   show "\<forall>k. k \<in># Y \<longrightarrow> (\<exists>a. a \<in># X \<and> k < a)"
   proof (intro allI impI)
@@ -239,9 +239,9 @@
 
 lemma less_eq_imp_le_multiset:
   fixes M N :: "('a \<Colon> linorder) multiset"
-  shows "M \<le> N \<Longrightarrow> M #\<subseteq># N"
+  shows "M \<le># N \<Longrightarrow> M #\<subseteq># N"
   unfolding le_multiset_def less_multiset\<^sub>H\<^sub>O
-  by (auto dest: leD simp add: less_eq_multiset.rep_eq)
+  by (simp add: less_le_not_le subseteq_mset_def)
 
 lemma less_multiset_right_total:
   fixes M :: "('a \<Colon> linorder) multiset"
@@ -302,7 +302,7 @@
   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)  
 
-lemma union_less_diff_plus: "P \<le> M \<Longrightarrow> N #\<subset># P \<Longrightarrow> M - P + N #\<subset># M"
-  by (drule ordered_cancel_comm_monoid_diff_class.diff_add[symmetric]) (metis union_less_mono2)
+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)
 
 end

--- a/src/HOL/Library/Permutation.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/Library/Permutation.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -140,7 +140,7 @@
   apply simp
   done
 
-lemma multiset_of_le_perm_append: "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
+lemma multiset_of_le_perm_append: "multiset_of xs \<le># multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   apply (insert surj_multiset_of)
   apply (drule surjD)

--- a/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -5,7 +5,7 @@
 
 section{*Common Declarations for Chandy and Charpentier's Allocator*}
 
-theory AllocBase imports "../UNITY_Main" begin
+theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
 
 consts Nclients :: nat  (*Number of clients*)
 
@@ -41,12 +41,19 @@
 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"
+unfolding le_multiset_def apply (cases B; simp)
+apply (rule HOL.disjI1)
+apply (rule union_less_mono2[of "{#}" "_ + {#_#}" A, simplified])
+apply (simp add: less_multiset\<^sub>H\<^sub>O)
+done
+
 lemma mono_bag_of: "mono (bag_of :: 'a list => ('a::order) multiset)"
 apply (rule monoI)
 apply (unfold prefix_def)
-apply (erule genPrefix.induct, auto)
+apply (erule genPrefix.induct, simp_all add: add_right_mono)
 apply (erule order_trans)
-apply simp
+apply (simp add: less_eq_multiset_def subseteq_le_multiset)
 done
 
 (** setsum **)

--- a/src/HOL/UNITY/Follows.thy	Mon Jun 08 22:04:19 2015 +0200
+++ b/src/HOL/UNITY/Follows.thy	Wed Jun 10 13:24:16 2015 +0200
@@ -168,6 +168,19 @@
 
 
 subsection{*Multiset union properties (with the multiset ordering)*}
+(*TODO: remove when multiset is of sort ord again*)
+instantiation multiset :: (order) ordered_ab_semigroup_add
+begin
+
+definition less_multiset :: "'a\<Colon>order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+  "M' < M \<longleftrightarrow> M' #<# M"
+
+definition less_eq_multiset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" where
+   "(M'::'a multiset) \<le> M \<longleftrightarrow> M' #<=# M"
+
+instance
+  by default (auto simp add: less_eq_multiset_def less_multiset_def multiset_order.less_le_not_le add.commute multiset_order.add_right_mono)
+end
 
 lemma increasing_union: 
     "[| F \<in> increasing f;  F \<in> increasing g |]