adding lemma to List library for executable equation of the (refl) transitive closure

--- a/src/HOL/List.thy	Thu Sep 29 21:42:03 2011 +0200
+++ b/src/HOL/List.thy	Mon Oct 03 14:43:12 2011 +0200
@@ -2870,6 +2870,9 @@
   qed
 qed
 
+lemma distinct_length_filter: "distinct xs \<Longrightarrow> length (filter P xs) = card ({x. P x} Int set xs)"
+by (induct xs) (auto)
+
 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
 apply (induct n == "length ws" arbitrary:ws) apply simp
 apply(case_tac ws) apply simp