src/HOL/List.thy
changeset 5077 71043526295f
parent 4643 1b40fcac5a09
child 5162 53e505c6019c
--- 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 [])"