src/HOL/Library/Multiset.thy

   by (induct_tac x, auto)
 
 lemma set_of_multiset_of[simp]: "set_of(multiset_of x) = set x"
  by (induct_tac x, auto) 
 
-lemma multset_of_append[simp]: 
+lemma multiset_of_append[simp]: 
   "multiset_of (xs @ ys) = multiset_of xs + multiset_of ys"
   by (rule_tac x=ys in spec, induct_tac xs, auto simp: union_ac) 
 
 lemma surj_multiset_of: "surj multiset_of"
   apply (unfold surj_def, rule allI) 

   apply (drule distinct_remdups[THEN distinct_remdups 
                       [THEN set_eq_iff_multiset_of_eq_distinct[THEN iffD2]]]) 
   apply simp
   done
 
+lemma multiset_of_compl_union[simp]:
+ "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)
 
 subsection {* Pointwise ordering induced by count *}
 
 consts 
   mset_le :: "['a multiset, 'a multiset] \<Rightarrow> bool"