--- 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";
--- 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} *}