# HG changeset patch
# User kleing
# Date 1114672895 -7200
# Node ID 9634b3f9d9102062a310497bd1a4c58378156377
# Parent  5c63b6c2f4a5c43b6e73c4153dc72bef82153f70
more about list_update

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