Add filter_remove1

--- a/src/HOL/List.thy	Thu Sep 02 10:14:32 2010 +0200
+++ b/src/HOL/List.thy	Thu Sep 02 10:18:15 2010 +0200
@@ -3076,6 +3076,10 @@
   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
 by(induct xs) auto
 
+lemma filter_remove1:
+  "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
+by (induct xs) auto
+
 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
 apply(insert set_remove1_subset)
 apply fast