added and renamed
authornipkow
Fri Oct 15 18:16:03 2004 +0200 (2004-10-15)
changeset 152460984a2c2868b
parent 15245 5a21d9a8f14b
child 15247 98d3ca56684d
added and renamed
src/HOL/List.ML
src/HOL/List.thy
     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