diff -r 45c085c7efc6 -r 28dd6fd3d184 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu May 07 12:02:16 2009 +0200
+++ b/src/HOL/List.thy	Fri May 08 08:06:43 2009 +0200
@@ -1324,6 +1324,9 @@
 apply simp_all
 done
 
+lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
+by(metis length_0_conv length_list_update)
+
 lemma list_update_same_conv:
 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
 by (induct xs arbitrary: i) (auto split: nat.split)
@@ -1357,12 +1360,10 @@
 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
 by (induct xs arbitrary: n) (auto split:nat.splits)
 
-lemma list_update_overwrite:
+lemma list_update_overwrite[simp]:
   "xs [i := x, i := y] = xs [i := y]"
-apply (induct xs arbitrary: i)
-apply simp
-apply (case_tac i)
-apply simp_all
+apply (induct xs arbitrary: i) apply simp
+apply (case_tac i, simp_all)
 done
 
 lemma list_update_swap:
@@ -1444,6 +1445,18 @@
 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
 by (induct xs, simp, case_tac xs, simp_all)
 
+lemma last_list_update:
+  "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
+by (auto simp: last_conv_nth)
+
+lemma butlast_list_update:
+  "butlast(xs[k:=x]) =
+ (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
+apply(cases xs rule:rev_cases)
+apply simp
+apply(simp add:list_update_append split:nat.splits)
+done
+
 
 subsubsection {* @{text take} and @{text drop} *}
 
@@ -1723,6 +1736,13 @@
  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
 by(induct xs, auto)
 
+lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
+by (induct xs) (auto dest: set_takeWhileD)
+
+lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
+by (induct xs) auto
+
+
 text{* The following two lemmmas could be generalized to an arbitrary
 property. *}
 
@@ -2140,6 +2160,10 @@
 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
 by(simp add:listsum_foldr foldl_foldr1)
 
+lemma distinct_listsum_conv_Setsum:
+  "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
+by (induct xs) simp_all
+
 
 text{* Some syntactic sugar for summing a function over a list: *}