# HG changeset patch
# User kleing
# Date 1114672875 -7200
# Node ID 5c63b6c2f4a5c43b6e73c4153dc72bef82153f70
# Parent  f011452b2815bdce2e53dea169c4bc8290d7cf23
some more lemmas about multiset_of

diff -r f011452b2815 -r 5c63b6c2f4a5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Thu Apr 28 01:57:15 2005 +0200
+++ b/src/HOL/Library/Multiset.thy	Thu Apr 28 09:21:15 2005 +0200
@@ -740,7 +740,10 @@
   by (induct_tac x, auto)
 
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
- by (induct_tac x, auto) 
+  by (induct_tac x, auto) 
+
+lemma mem_set_multiset_eq: "x \<in> set xs = (x :# multiset_of xs)"
+  by (induct xs) auto
 
 lemma multiset_of_append[simp]: 
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
@@ -764,6 +767,10 @@
    apply (erule_tac x=aa in allE, simp) 
    done
 
+lemma multiset_of_eq_setD: 
+  "multiset_of xs = multiset_of ys \<Longrightarrow> set xs = set ys"
+  by (rule) (auto simp add:multiset_eq_conv_count_eq set_count_greater_0)
+
 lemma set_eq_iff_multiset_of_eq_distinct: 
   "\<lbrakk>distinct x; distinct y\<rbrakk> 
    \<Longrightarrow> (set x = set y) = (multiset_of x = multiset_of y)"
@@ -782,6 +789,11 @@
  "multiset_of [x\<in>xs. P x] + multiset_of [x\<in>xs. \<not>P x] = multiset_of xs"
   by (induct xs) (auto simp: union_ac)
 
+lemma count_filter: 
+  "count (multiset_of xs) x = length [y \<in> xs. y = x]"
+  by (induct xs, auto)
+
+
 subsection {* Pointwise ordering induced by count *}
 
 consts