# HG changeset patch
# User nipkow
# Date 1243403771 -7200
# Node ID 2662d1cdc51f16b061182cf8572036b5649a6cb4
# Parent  4dbe0b4c313bc468e3c0d8f9be3d88beb552536a
more lemmas

diff -r 4dbe0b4c313b -r 2662d1cdc51f src/HOL/List.thy
--- 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)