changeset 15304 | 3514ca74ac54 |
parent 15303 | eedbb8d22ca2 |
child 15305 | 0bd9eedaa301 |
--- a/src/HOL/List.thy Sun Nov 21 15:44:20 2004 +0100 +++ b/src/HOL/List.thy Sun Nov 21 18:39:25 2004 +0100 @@ -1479,6 +1479,13 @@ lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)" by (induct xs) auto +lemma distinct_map_filterI: + "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))" +apply(induct xs) + apply simp +apply force +done + text {* It is best to avoid this indexed version of distinct, but sometimes it is useful. *}