--- a/src/HOL/Library/Multiset.thy Thu Oct 27 15:08:50 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Oct 27 15:51:54 2016 +0200
@@ -495,6 +495,10 @@
then show ?thesis using B by simp
qed
+lemma add_mset_eq_singleton_iff[iff]:
+ "add_mset x M = {#y#} \<longleftrightarrow> M = {#} \<and> x = y"
+ by auto
+
subsubsection \<open>Pointwise ordering induced by count\<close>
@@ -659,6 +663,15 @@
lemma Diff_eq_empty_iff_mset: "A - B = {#} \<longleftrightarrow> A \<subseteq># B"
by (auto simp: multiset_eq_iff subseteq_mset_def)
+lemma add_mset_subseteq_single_iff[iff]: "add_mset a M \<subseteq># {#b#} \<longleftrightarrow> M = {#} \<and> a = b"
+proof
+ assume A: "add_mset a M \<subseteq># {#b#}"
+ then have \<open>a = b\<close>
+ by (auto dest: mset_subset_eq_insertD)
+ then show "M={#} \<and> a=b"
+ using A by (simp add: mset_subset_eq_add_mset_cancel)
+qed simp
+
subsubsection \<open>Intersection and bounded union\<close>
@@ -1317,6 +1330,11 @@
lemma filter_filter_mset: "filter_mset P (filter_mset Q M) = {#x \<in># M. Q x \<and> P x#}"
by (auto simp: multiset_eq_iff)
+lemma
+ filter_mset_True[simp]: "{#y \<in># M. True#} = M" and
+ filter_mset_False[simp]: "{#y \<in># M. False#} = {#}"
+ by (auto simp: multiset_eq_iff)
+
subsubsection \<open>Size\<close>
@@ -2173,7 +2191,7 @@
lemma sum_mset_0_iff [simp]:
"sum_mset M = (0::'a::canonically_ordered_monoid_add)
\<longleftrightarrow> (\<forall>x \<in> set_mset M. x = 0)"
-by(induction M) (auto simp: add_eq_0_iff_both_eq_0)
+by(induction M) auto
lemma sum_mset_diff:
fixes M N :: "('a :: ordered_cancel_comm_monoid_diff) multiset"
@@ -2193,6 +2211,9 @@
lemma size_mset_set [simp]: "size (mset_set A) = card A"
by (simp only: size_eq_sum_mset card_eq_sum sum_unfold_sum_mset)
+lemma sum_mset_sum_list: "sum_mset (mset xs) = sum_list xs"
+ by (induction xs) auto
+
syntax (ASCII)
"_sum_mset_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add" ("(3SUM _:#_. _)" [0, 51, 10] 10)
syntax
@@ -2342,6 +2363,9 @@
then show ?thesis by (simp add: normalize_prod_mset)
qed
+lemma prod_mset_prod_list: "prod_mset (mset xs) = prod_list xs"
+ by (induct xs) auto
+
subsection \<open>Alternative representations\<close>
--- a/src/HOL/Library/Multiset_Order.thy Thu Oct 27 15:08:50 2016 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Thu Oct 27 15:51:54 2016 +0200
@@ -280,6 +280,12 @@
unfolding less_multiset\<^sub>H\<^sub>O
by (metis count_greater_zero_iff le_imp_less_or_eq less_imp_not_less not_gr_zero union_iff)
+lemma mset_lt_single_iff[iff]: "{#x#} < {#y#} \<longleftrightarrow> x < y"
+ unfolding less_multiset\<^sub>H\<^sub>O by simp
+
+lemma mset_le_single_iff[iff]: "{#x#} \<le> {#y#} \<longleftrightarrow> x \<le> y" for x y :: "'a::order"
+ unfolding less_eq_multiset\<^sub>H\<^sub>O by force
+
instance multiset :: (linorder) linordered_cancel_ab_semigroup_add
by standard (metis less_eq_multiset\<^sub>H\<^sub>O not_less_iff_gr_or_eq)