code theorems for nth, list_update

--- a/src/HOL/List.thy	Sat Feb 07 08:37:42 2009 +0100
+++ b/src/HOL/List.thy	Sat Feb 07 08:37:43 2009 +0100
@@ -1215,10 +1215,10 @@
 
 subsubsection {* @{text nth} *}
 
-lemma nth_Cons_0 [simp]: "(x # xs)!0 = x"
+lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
 by auto
 
-lemma nth_Cons_Suc [simp]: "(x # xs)!(Suc n) = xs!n"
+lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
 by auto
 
 declare nth.simps [simp del]
@@ -1375,6 +1375,12 @@
 apply auto
 done
 
+lemma list_update_code [code]:
+  "[][i := y] = []"
+  "(x # xs)[0 := y] = y # xs"
+  "(x # xs)[Suc i := y] = x # xs[i := y]"
+  by simp_all
+
 
 subsubsection {* @{text last} and @{text butlast} *}