# HG changeset patch
# User nipkow
# Date 1101120836 -3600
# Node ID 0bd9eedaa3016f5544dd36617b0ca998676b451e
# Parent  3514ca74ac541b19f64d7184884dec70ca594248
added lemmas

diff -r 3514ca74ac54 -r 0bd9eedaa301 src/HOL/List.thy
--- 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)