src/HOL/List.thy

 done
 
 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. *}
 lemma distinct_conv_nth:
 "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j --> xs!i \<noteq> xs!j)"