# HG changeset patch
# User nipkow
# Date 1182691074 -7200
# Node ID 10adbdcdc65b2b98b2745113d17cf0e7d69d33b0
# Parent  26a5ef187e8b29f83a7ea7f6f334516698d769a3
new lemmas

diff -r 26a5ef187e8b -r 10adbdcdc65b src/HOL/List.thy
--- 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