added remdups_filter lemma

--- a/src/HOL/List.thy	Wed Dec 02 17:53:44 2009 +0100
+++ b/src/HOL/List.thy	Fri Dec 04 08:26:25 2009 +0100
@@ -2665,6 +2665,10 @@
 apply(rule length_remdups_leq)
 done
 
+lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
+apply(induct xs)
+apply auto
+done
 
 lemma distinct_map:
   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"