--- a/src/HOL/List.thy Wed May 27 07:28:29 2009 +0200
+++ b/src/HOL/List.thy Wed May 27 07:56:11 2009 +0200
@@ -1365,6 +1365,13 @@
"(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
by (induct xs, auto)
+lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
+by(induct xs arbitrary: k)(auto split:nat.splits)
+
+lemma rev_update:
+ "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
+by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
+
lemma update_zip:
"(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)