# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1469019129 -7200
# Node ID f01d1e393f3f4f898a4b4404cccfff78ae65afcc
# Parent  4ec7554857326339b963edc4d7ad9c8e24d087f9
more instantiations for multiset

diff -r 4ec755485732 -r f01d1e393f3f NEWS
--- a/NEWS	Wed Jul 20 13:51:38 2016 +0200
+++ b/NEWS	Wed Jul 20 14:52:09 2016 +0200
@@ -405,10 +405,16 @@
 * The lemma mset_map has now the attribute [simp].
 INCOMPATIBILITY.
 
+* Some theorems about multisets have been removed:
+    le_multiset_plus_plus_left_iff ~> add_less_cancel_right
+    le_multiset_plus_plus_right_iff ~> add_less_cancel_left
+    add_eq_self_empty_iff ~> add_cancel_left_right
+INCOMPATIBILITY.
+
 * Some typeclass constraints about multisets have been reduced from ordered or
 linordered to preorder. Multisets have the additional typeclasses order_bot,
 no_top, ordered_ab_semigroup_add_imp_le, ordered_cancel_comm_monoid_add,
-and linordered_cancel_ab_semigroup_add.
+linordered_cancel_ab_semigroup_add, and ordered_ab_semigroup_monoid_add_imp_le.
 INCOMPATIBILITY.
 
 * There are some new simplification rules about multisets and the multiset
diff -r 4ec755485732 -r f01d1e393f3f src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Wed Jul 20 13:51:38 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy	Wed Jul 20 14:52:09 2016 +0200
@@ -187,9 +187,6 @@
   shows "{#} \<le> M"
   by (simp add: subset_eq_imp_le_multiset)
 
-lemma add_eq_self_empty_iff: "M + N = M \<longleftrightarrow> N = {#}"
-  by (rule cancel_comm_monoid_add_class.add_cancel_left_right)
-
 lemma ex_gt_imp_less_multiset: "(\<exists>y. y \<in># N \<and> (\<forall>x. x \<in># M \<longrightarrow> x < y)) \<Longrightarrow> M < N"
   unfolding less_multiset\<^sub>H\<^sub>O
   by (metis count_eq_zero_iff count_greater_zero_iff less_le_not_le)
@@ -207,7 +204,7 @@
 lemma union_le_diff_plus: "P \<le># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
   by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)
 
-instantiation multiset :: (preorder) ordered_ab_semigroup_add_imp_le
+instantiation multiset :: (preorder) ordered_ab_semigroup_monoid_add_imp_le
 begin
 
 lemma less_eq_multiset\<^sub>H\<^sub>O:
@@ -219,24 +216,16 @@
 lemma
   fixes M N :: "'a multiset"
   shows
-    less_eq_multiset_plus_left[simp]: "N \<le> (M + N)" and
-    less_eq_multiset_plus_right[simp]: "M \<le> (M + N)"
-  using add_le_cancel_left[of N 0] add_le_cancel_left[of M 0 N] by (simp_all add: add.commute)
-
-lemma
-  fixes M N :: "'a multiset"
-  shows
-    le_multiset_plus_plus_left_iff: "M + N < M' + N \<longleftrightarrow> M < M'" and
-    le_multiset_plus_plus_right_iff: "M + N < M + N' \<longleftrightarrow> N < N'"
+    less_eq_multiset_plus_left: "N \<le> (M + N)" and
+    less_eq_multiset_plus_right: "M \<le> (M + N)"
   by simp_all
 
 lemma
   fixes M N :: "'a multiset"
   shows
-    le_multiset_plus_left_nonempty[simp]: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
-    le_multiset_plus_right_nonempty[simp]: "N \<noteq> {#} \<Longrightarrow> M < M + N"
-  using [[metis_verbose = false]]
-  by (metis add.right_neutral le_multiset_empty_left le_multiset_plus_plus_right_iff add.commute)+
+    le_multiset_plus_left_nonempty: "M \<noteq> {#} \<Longrightarrow> N < M + N" and
+    le_multiset_plus_right_nonempty: "N \<noteq> {#} \<Longrightarrow> M < M + N"
+    by simp_all
 
 end