summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 02 Aug 2005 13:13:18 +0200 | |

changeset 16998 | e0050191e2d1 |

parent 16997 | 7dfc99f62dd9 |

child 16999 | 307b2ec590ff |

Added filter lemma

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/List.thy Mon Aug 01 19:21:38 2005 +0200 +++ b/src/HOL/List.thy Tue Aug 02 13:13:18 2005 +0200 @@ -706,14 +706,24 @@ lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs" by (induct xs) auto +lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" +by (induct xs) (auto simp add: le_SucI) + lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs" by (induct xs) auto lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []" by (induct xs) auto -lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs" -by (induct xs) (auto simp add: le_SucI) +lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" + by (induct xs) simp_all + +lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)" +apply (induct xs) + apply auto +apply(cut_tac P=P and xs=xs in length_filter_le) +apply simp +done lemma filter_map: "filter P (map f xs) = map f (filter (P o f) xs)"