--- a/src/HOL/List.thy Sun Nov 21 18:39:25 2004 +0100
+++ b/src/HOL/List.thy Mon Nov 22 11:53:56 2004 +0100
@@ -650,6 +650,9 @@
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
@@ -1452,6 +1455,9 @@
"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)