src/HOL/Library/Multiset.thy
changeset 58035 177eeda93a8c
parent 57966 6fab7e95587d
child 58098 ff478d85129b
     1.1 --- a/src/HOL/Library/Multiset.thy	Fri Aug 22 15:55:24 2014 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Fri Aug 22 17:35:48 2014 +0200
     1.3 @@ -530,6 +530,17 @@
     1.4    "Multiset.filter P (M #\<inter> N) = Multiset.filter P M #\<inter> Multiset.filter P N"
     1.5    by (rule multiset_eqI) simp
     1.6  
     1.7 +lemma multiset_filter_subset[simp]: "Multiset.filter f M \<le> M"
     1.8 +  unfolding less_eq_multiset.rep_eq by auto
     1.9 +
    1.10 +lemma multiset_filter_mono: assumes "A \<le> B"
    1.11 +  shows "Multiset.filter f A \<le> Multiset.filter f B"
    1.12 +proof -
    1.13 +  from assms[unfolded mset_le_exists_conv]
    1.14 +  obtain C where B: "B = A + C" by auto
    1.15 +  show ?thesis unfolding B by auto
    1.16 +qed
    1.17 +
    1.18  syntax
    1.19    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
    1.20  syntax (xsymbol)
    1.21 @@ -1325,6 +1336,17 @@
    1.22    "mcard (multiset_of xs) = length xs"
    1.23    by (induct xs) simp_all
    1.24  
    1.25 +lemma mcard_mono: assumes "A \<le> B"
    1.26 +  shows "mcard A \<le> mcard B"
    1.27 +proof -
    1.28 +  from assms[unfolded mset_le_exists_conv]
    1.29 +  obtain C where B: "B = A + C" by auto
    1.30 +  show ?thesis unfolding B by (induct C, auto)
    1.31 +qed
    1.32 +
    1.33 +lemma mcard_filter_lesseq[simp]: "mcard (Multiset.filter f M) \<le> mcard M"
    1.34 +  by (rule mcard_mono[OF multiset_filter_subset])
    1.35 +
    1.36  
    1.37  subsection {* Alternative representations *}
    1.38