
diff -r 5c63b6c2f4a5 -r 9634b3f9d910 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Apr 28 09:21:15 2005 +0200
+++ b/src/HOL/List.thy	Thu Apr 28 09:21:35 2005 +0200
@@ -865,6 +865,11 @@
 apply(simp split:nat.split)
 done
 
+lemma list_update_append:
+  "!!n. (xs @ ys) [n:= x] = 
+  (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
+by (induct xs) (auto split:nat.splits)
+
 lemma list_update_length [simp]:
  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
 by (induct xs, auto)
@@ -880,6 +885,9 @@
 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
 by (blast dest!: set_update_subset_insert [THEN subsetD])
 
+lemma set_update_memI: "!!n. n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
+by (induct xs) (auto split:nat.splits)
+
 
 subsubsection {* @{text last} and @{text butlast} *}
 




