# HG changeset patch
# User nipkow
# Date 1010490478 -3600
# Node ID acbe16e49abe16583229e0637941c1f0c3cb9865
# Parent  d33033205e2f93ac16d0d7ff908e0c1d4347a5a0
added filter_filter

diff -r d33033205e2f -r acbe16e49abe src/HOL/List.ML
--- a/src/HOL/List.ML	Tue Jan 08 11:52:55 2002 +0100
+++ b/src/HOL/List.ML	Tue Jan 08 12:47:58 2002 +0100
@@ -529,16 +529,22 @@
 qed "filter_append";
 Addsimps [filter_append];
 
-Goal "filter (%x. True) xs = xs";
+Goal "filter P (filter Q xs) = filter (%x. Q x & P x) xs";
 by (induct_tac "xs" 1);
 by Auto_tac;
-qed "filter_True";
+qed "filter_filter";
+Addsimps [filter_filter];
+
+Goal "(!x : set xs. P x) --> filter P xs = xs";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "filter_True";
 Addsimps [filter_True];
 
-Goal "filter (%x. False) xs = []";
+Goal "(!x : set xs. ~P x) --> filter P xs = []";
 by (induct_tac "xs" 1);
 by Auto_tac;
-qed "filter_False";
+qed_spec_mp "filter_False";
 Addsimps [filter_False];
 
 Goal "length (filter P xs) <= length xs";