# HG changeset patch
# User nipkow
# Date 1122888259 -7200
# Node ID 46697fa536ab0e44c03b32fdf9920de1734678a5
# Parent  6a25e42eaff52fc8bc7824b5c30f3bf3aeb57b79
added map_filter lemmas

diff -r 6a25e42eaff5 -r 46697fa536ab src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 01 03:27:31 2005 +0200
+++ b/src/HOL/List.thy	Mon Aug 01 11:24:19 2005 +0200
@@ -715,6 +715,14 @@
 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
 by (induct xs) (auto simp add: le_SucI)
 
+lemma filter_map:
+  "filter P (map f xs) = map f (filter (P o f) xs)"
+by (induct xs) simp_all
+
+lemma length_filter_map[simp]:
+  "length (filter P (map f xs)) = length(filter (P o f) xs)"
+by (simp add:filter_map)
+
 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
 by auto