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