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