| changeset 58195 | 1fee63e0377d |
| parent 58135 | 0774d32fe74f |
| child 58247 | 98d0f85d247f |
--- a/src/HOL/List.thy Fri Sep 05 16:09:03 2014 +0100 +++ b/src/HOL/List.thy Sat Sep 06 20:12:32 2014 +0200 @@ -3208,6 +3208,10 @@ "distinct(map f xs) = (distinct xs & inj_on f (set xs))" by (induct xs) auto +lemma distinct_map_filter: + "distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))" + by (induct xs) auto + lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)" by (induct xs) auto