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

author | nipkow |

Sun, 24 Jun 2007 15:17:54 +0200 | |

changeset 23479 | 10adbdcdc65b |

parent 23478 | 26a5ef187e8b |

child 23480 | 8d01ccdc3652 |

new lemmas

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

--- a/src/HOL/List.thy Sun Jun 24 10:33:49 2007 +0200 +++ b/src/HOL/List.thy Sun Jun 24 15:17:54 2007 +0200 @@ -334,6 +334,9 @@ lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])" by (induct xs) auto +lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0" +by auto + lemma length_Suc_conv: "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)" by (induct xs) auto @@ -2052,6 +2055,12 @@ (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)" by (induct xs) auto +lemma in_set_remove1[simp]: + "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)" +apply (induct xs) +apply auto +done + lemma set_remove1_subset: "set(remove1 x xs) <= set xs" apply(induct xs) apply simp @@ -2066,6 +2075,12 @@ apply blast done +lemma length_remove1: + "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)" +apply (induct xs) + apply (auto dest!:length_pos_if_in_set) +done + lemma remove1_filter_not[simp]: "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs" by(induct xs) auto