src/HOL/List.thy

 
 subsection {* @{text filter} *}
 
 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
 by (induct xs) auto
+
+lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
+by (induct xs) simp_all
 
 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
 by (induct xs) auto
 
 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"

 
 lemma distinct_append [simp]:
 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
 by (induct xs) auto
 
+lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
+by(induct xs) auto
+
 lemma set_remdups [simp]: "set (remdups xs) = set xs"
 by (induct xs) (auto simp add: insert_absorb)
 
 lemma distinct_remdups [iff]: "distinct (remdups xs)"
 by (induct xs) auto