* HOL/List: new function list_update written xs[i:=v] that updates the i-th
list position. May also be iterated as in xs[i:=a,j:=b,...].

--- a/NEWS	Wed Jun 24 11:24:52 1998 +0200
+++ b/NEWS	Wed Jun 24 13:59:45 1998 +0200
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history of user-visible changes
 ================================================
 
@@ -56,11 +55,14 @@
 
 * added option_map_eq_Some to simpset() and claset()
 
+* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
+
 * New theory HOL/Update of function updates:
   f(a:=b) == %x. if x=a then b else f x
   May also be iterated as in f(a:=b,c:=d,...).
 
-* New directory HOL/UNITY: Chandy and Misra's UNITY formalism
+* HOL/List: new function list_update written xs[i:=v] that updates the i-th
+  list position. May also be iterated as in xs[i:=a,j:=b,...].
 
 * split_all_tac is now much faster and fails if there is nothing to
 split.  Existing (fragile) proofs may require adaption because the

--- a/src/HOL/List.ML	Wed Jun 24 11:24:52 1998 +0200
+++ b/src/HOL/List.ML	Wed Jun 24 13:59:45 1998 +0200
@@ -537,6 +537,18 @@
 qed_spec_mp "nth_mem";
 Addsimps [nth_mem];
 
+(** list update **)
+
+section "list update";
+
+Goal "!i. length(xs[i:=x]) = length xs";
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsplits [split_nat_case]) 1);
+qed_spec_mp "length_list_update";
+Addsimps [length_list_update];
+
+
 (** last & butlast **)
 
 Goal "last(xs@[x]) = x";

--- a/src/HOL/List.thy	Wed Jun 24 11:24:52 1998 +0200
+++ b/src/HOL/List.thy	Wed Jun 24 13:59:45 1998 +0200
@@ -21,6 +21,7 @@
   map         :: ('a=>'b) => ('a list => 'b list)
   mem         :: ['a, 'a list] => bool                    (infixl 55)
   nth         :: ['a list, nat] => 'a			  (infixl "!" 100)
+  list_update :: 'a list => nat => 'a => 'a list
   take, drop  :: [nat, 'a list] => 'a list
   takeWhile,
   dropWhile   :: ('a => bool) => 'a list => 'a list
@@ -31,6 +32,9 @@
   nodups      :: "'a list => bool"
   replicate   :: nat => 'a => 'a list
 
+nonterminals
+  lupdbinds  lupdbind
+
 syntax
   (* list Enumeration *)
   "@list"     :: args => 'a list                          ("[(_)]")
@@ -38,11 +42,20 @@
   (* Special syntax for filter *)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_:_ ./ _])")
 
+  (* list update *)
+  "_lupdbind"      :: ['a, 'a] => lupdbind            ("(2_ :=/ _)")
+  ""               :: lupdbind => lupdbinds           ("_")
+  "_lupdbinds"     :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _")
+  "_LUpdate"       :: ['a, lupdbinds] => 'a           ("_/[(_)]" [900,0] 900)
+
 translations
   "[x, xs]"     == "x#[xs]"
   "[x]"         == "x#[]"
   "[x:xs . P]"  == "filter (%x. P) xs"
 
+  "_LUpdate xs (_lupdbinds b bs)"  == "_LUpdate (_LUpdate xs b) bs"
+  "xs[i:=x]"                       == "list_update xs i x"
+
 syntax (symbols)
   "@filter"   :: [idt, 'a list, bool] => 'a list          ("(1[_\\<in>_ ./ _])")
 
@@ -109,6 +122,10 @@
 primrec nth nat
   "xs!0 = hd xs"
   "xs!(Suc n) = (tl xs)!n"
+primrec list_update list
+ "    [][i:=v] = []"
+ "(x#xs)[i:=v] = (case i of 0     => v # xs 
+			  | Suc j => x # xs[j:=v])"
 primrec takeWhile list
   "takeWhile P [] = []"
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"