summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 15 Oct 2004 18:16:03 +0200 | |

changeset 15246 | 0984a2c2868b |

parent 15245 | 5a21d9a8f14b |

child 15247 | 98d3ca56684d |

added and renamed

src/HOL/List.ML | file | annotate | diff | comparison | revisions | |

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

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