# HG changeset patch
# User nipkow
# Date 1097856963 -7200
# Node ID 0984a2c2868bccd117e0eb8e6fd7e2852ed42994
# Parent  5a21d9a8f14b620ec35b6a1edb5ff7de50f4fb0e
added and renamed

diff -r 5a21d9a8f14b -r 0984a2c2868b src/HOL/List.ML
--- a/src/HOL/List.ML	Thu Oct 14 12:18:52 2004 +0200
+++ b/src/HOL/List.ML	Fri Oct 15 18:16:03 2004 +0200
@@ -77,7 +77,7 @@
 val length_append = thm "length_append";
 val length_butlast = thm "length_butlast";
 val length_drop = thm "length_drop";
-val length_filter = thm "length_filter";
+val length_filter_le = thm "length_filter_le";
 val length_greater_0_conv = thm "length_greater_0_conv";
 val length_induct = thm "length_induct";
 val length_list_update = thm "length_list_update";
diff -r 5a21d9a8f14b -r 0984a2c2868b src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Oct 14 12:18:52 2004 +0200
+++ b/src/HOL/List.thy	Fri Oct 15 18:16:03 2004 +0200
@@ -769,12 +769,22 @@
 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
 by (induct xs) auto
 
-lemma length_filter [simp]: "length (filter P xs) \<le> length xs"
+lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
 by (induct xs) (auto simp add: le_SucI)
 
 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
 by auto
 
+lemma length_filter_less:
+  "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
+proof (induct xs)
+  case Nil thus ?case by simp
+next
+  case (Cons x xs) thus ?case
+    apply (auto split:split_if_asm)
+    using length_filter_le[of P xs] apply arith
+  done
+qed
 
 subsection {* @{text concat} *}