# HG changeset patch
# User haftmann
# Date 1233992263 -3600
# Node ID c82b3e8a4dafe2a2d5c19f5639f5908fd1bd5cab
# Parent  5132da6ebca35fc734aa70108d668b4d91b73f31
code theorems for nth, list_update

diff -r 5132da6ebca3 -r c82b3e8a4daf src/HOL/List.thy
--- 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} *}