1.1 --- a/src/HOL/List.thy	Thu Apr 28 09:21:15 2005 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Apr 28 09:21:35 2005 +0200
     1.3 @@ -865,6 +865,11 @@
     1.4  apply(simp split:nat.split)
     1.5  done
     1.6  
     1.7 +lemma list_update_append:
     1.8 +  "!!n. (xs @ ys) [n:= x] = 
     1.9 +  (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
    1.10 +by (induct xs) (auto split:nat.splits)
    1.11 +
    1.12  lemma list_update_length [simp]:
    1.13   "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
    1.14  by (induct xs, auto)
    1.15 @@ -880,6 +885,9 @@
    1.16  lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
    1.17  by (blast dest!: set_update_subset_insert [THEN subsetD])
    1.18  
    1.19 +lemma set_update_memI: "!!n. n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
    1.20 +by (induct xs) (auto split:nat.splits)
    1.21 +
    1.22  
    1.23  subsubsection {* @{text last} and @{text butlast} *}
    1.24