src/HOL/List.ML
changeset 12664 acbe16e49abe
parent 12515 3fb416265ba9
child 12887 d25b43743e10
     1.1 --- a/src/HOL/List.ML	Tue Jan 08 11:52:55 2002 +0100
     1.2 +++ b/src/HOL/List.ML	Tue Jan 08 12:47:58 2002 +0100
     1.3 @@ -529,16 +529,22 @@
     1.4  qed "filter_append";
     1.5  Addsimps [filter_append];
     1.6  
     1.7 -Goal "filter (%x. True) xs = xs";
     1.8 +Goal "filter P (filter Q xs) = filter (%x. Q x & P x) xs";
     1.9  by (induct_tac "xs" 1);
    1.10  by Auto_tac;
    1.11 -qed "filter_True";
    1.12 +qed "filter_filter";
    1.13 +Addsimps [filter_filter];
    1.14 +
    1.15 +Goal "(!x : set xs. P x) --> filter P xs = xs";
    1.16 +by (induct_tac "xs" 1);
    1.17 +by Auto_tac;
    1.18 +qed_spec_mp "filter_True";
    1.19  Addsimps [filter_True];
    1.20  
    1.21 -Goal "filter (%x. False) xs = []";
    1.22 +Goal "(!x : set xs. ~P x) --> filter P xs = []";
    1.23  by (induct_tac "xs" 1);
    1.24  by Auto_tac;
    1.25 -qed "filter_False";
    1.26 +qed_spec_mp "filter_False";
    1.27  Addsimps [filter_False];
    1.28  
    1.29  Goal "length (filter P xs) <= length xs";