# HG changeset patch
# User blanchet
# Date 1408721748 -7200
# Node ID 177eeda93a8cc4c89d59f252e8c10a64b634fbd0
# Parent  07b5373955db39134d3f4417017a785ac3eec239
added lemmas contributed by Rene Thiemann

diff -r 07b5373955db -r 177eeda93a8c src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Aug 22 15:55:24 2014 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 22 17:35:48 2014 +0200
@@ -530,6 +530,17 @@
   "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
   by (rule multiset_eqI) simp
 
+lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
+  unfolding less_eq_multiset.rep_eq by auto
+
+lemma multiset_filter_mono: assumes "A \<le> B"
+  shows "Multiset.filter f A \<le> Multiset.filter 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
   "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
 syntax (xsymbol)
@@ -1325,6 +1336,17 @@
   "mcard (multiset_of xs) = length xs"
   by (induct xs) simp_all
 
+lemma mcard_mono: assumes "A \<le> B"
+  shows "mcard A \<le> mcard B"
+proof -
+  from assms[unfolded mset_le_exists_conv]
+  obtain C where B: "B = A + C" by auto
+  show ?thesis unfolding B by (induct C, auto)
+qed
+
+lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
+  by (rule mcard_mono[OF multiset_filter_subset])
+
 
 subsection {* Alternative representations *}