summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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";