1.1 --- a/src/HOL/List.ML Thu Oct 14 12:18:52 2004 +0200
1.2 +++ b/src/HOL/List.ML Fri Oct 15 18:16:03 2004 +0200
1.3 @@ -77,7 +77,7 @@
1.4 val length_append = thm "length_append";
1.5 val length_butlast = thm "length_butlast";
1.6 val length_drop = thm "length_drop";
1.7 -val length_filter = thm "length_filter";
1.8 +val length_filter_le = thm "length_filter_le";
1.9 val length_greater_0_conv = thm "length_greater_0_conv";
1.10 val length_induct = thm "length_induct";
1.11 val length_list_update = thm "length_list_update";

2.1 --- a/src/HOL/List.thy Thu Oct 14 12:18:52 2004 +0200
2.2 +++ b/src/HOL/List.thy Fri Oct 15 18:16:03 2004 +0200
2.3 @@ -769,12 +769,22 @@
2.4 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
2.5 by (induct xs) auto
2.6
2.7 -lemma length_filter [simp]: "length (filter P xs) \<le> length xs"
2.8 +lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
2.9 by (induct xs) (auto simp add: le_SucI)
2.10
2.11 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
2.12 by auto
2.13
2.14 +lemma length_filter_less:
2.15 + "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
2.16 +proof (induct xs)
2.17 + case Nil thus ?case by simp
2.18 +next
2.19 + case (Cons x xs) thus ?case
2.20 + apply (auto split:split_if_asm)
2.21 + using length_filter_le[of P xs] apply arith
2.22 + done
2.23 +qed
2.24
2.25 subsection {* @{text concat} *}
2.26