# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1477576314 -7200
# Node ID 91eae3a1be515d0524f36711c8ccca4509018577
# Parent  7f0edcc6c3d3122bc3ab05d2d8975bfcab7a6d3d
more lemmas

diff -r 7f0edcc6c3d3 -r 91eae3a1be51 src/HOL/Library/Multiset.thy
--- 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>
 
diff -r 7f0edcc6c3d3 -r 91eae3a1be51 src/HOL/Library/Multiset_Order.thy
--- 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)