# HG changeset patch
# User haftmann
# Date 1130510140 -7200
# Node ID 685d95c793ff18909490e1978d77af87e5ac9bd2
# Parent  c885c93a93248774ec6dad4c41bcdd087fdae934
cleaned up nth, nth_update, nth_map and nth_string functions

diff -r c885c93a9324 -r 685d95c793ff src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -1125,7 +1125,7 @@
           (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
         | _ => false);
 
-    val goal = List.nth (Thm.prems_of st, i - 1);
+    val goal = nth (Thm.prems_of st) (i - 1);
     val frees = List.filter (is_recT o type_of) (term_frees goal);
 
     fun mk_split_free_tac free induct_thm i =
@@ -1172,7 +1172,7 @@
           (s = "all" orelse s = "All") andalso is_recT T
         | _ => false);
 
-    val goal = List.nth (Thm.prems_of st, i - 1);
+    val goal = nth (Thm.prems_of st) (i - 1);
 
     fun is_all t =
       (case t of (Const (quantifier, _)$_) =>
@@ -1231,7 +1231,7 @@
 fun try_param_tac s rule i st =
   let
     val cert = cterm_of (Thm.theory_of_thm st);
-    val g = List.nth (prems_of st, i - 1);
+    val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
     val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
     val rule' = Thm.lift_rule (st, i) rule;
@@ -1258,7 +1258,7 @@
 fun ex_inst_tac i st =
   let
     val sg = sign_of_thm st;
-    val g = List.nth (prems_of st, i - 1);
+    val g = nth (prems_of st) (i - 1);
     val params = Logic.strip_params g;
     val exI' = Thm.lift_rule (st, i) exI;
     val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
@@ -1391,7 +1391,7 @@
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
       let val x' = Free (variant variants (base c ^ "'"),T)
-          val args' = nth_update x' (i, vars_more)
+          val args' = nth_update (i, x') vars_more
       in mk_upd updN c x' ext === mk_ext args'  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 
@@ -1770,7 +1770,7 @@
     (*updates*)
     fun mk_upd_prop (i,(c,T)) =
       let val x' = Free (variant all_variants (base c ^ "'"),T)
-          val args' = nth_update x' (parent_fields_len + i, all_vars_more)
+          val args' = nth_update (parent_fields_len + i, x') all_vars_more
       in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
     val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
 
diff -r c885c93a9324 -r 685d95c793ff src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -212,13 +212,13 @@
       val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
       val lb = ratrelmax(map (eval ex v) ge)
       val ub = ratrelmin(map (eval ex v) le)
-  in nth_update (choose2 (List.nth(discr,v)) (lb,ub)) (v,ex) end;
+  in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
 
 fun findex discr = Library.foldl (findex1 discr);
 
 fun elim1 v x =
   map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
-                        nth_update Rat.zero (v,bs)));
+                        nth_update (v, Rat.zero) bs));
 
 fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
 
@@ -229,7 +229,7 @@
   in case nz of [] => ex
      | (_,_,cs) :: _ =>
        let val v = find_index (not o equal Rat.zero) cs
-           val d = List.nth(discr,v)
+           val d = nth discr v
            val pos = Rat.ge0(el v cs)
            val sv = List.filter (single_var v) nz
            val minmax =
@@ -240,7 +240,7 @@
            val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv
            val x = minmax((Rat.zero,if pos then true else false)::bnds)
            val ineqs' = elim1 v x nz
-           val ex' = nth_update x (v,ex)
+           val ex' = nth_update (v, x) ex
        in pick_vars discr (ineqs',ex') end
   end;
 
@@ -460,8 +460,8 @@
         let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
         in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
 
-      fun mk(Asm i) = trace_thm "Asm" (List.nth(asms,i))
-        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (List.nth(atoms,i)))
+      fun mk(Asm i) = trace_thm "Asm" (nth asms i)
+        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
         | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
         | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
         | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
diff -r c885c93a9324 -r 685d95c793ff src/Provers/eqsubst.ML
--- a/src/Provers/eqsubst.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Provers/eqsubst.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -363,7 +363,7 @@
       val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
       val cfvs = rev (map ctermify fvs);
 
-      val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
+      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
       val asm_nprems = length (Logic.strip_imp_prems asmt);
 
       val pth = trivify asmt;
diff -r c885c93a9324 -r 685d95c793ff src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Pure/General/name_space.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -89,7 +89,7 @@
 fun map_base _ "" = ""
   | map_base f name =
       let val names = unpack name
-      in pack (map_nth_elem (length names - 1) f names) end;
+      in pack (nth_map (length names - 1) f names) end;
 
 fun suffixes_prefixes xs =
   let
diff -r c885c93a9324 -r 685d95c793ff src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -96,7 +96,7 @@
 fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
   let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     make_rules (next - 1) ((w, ((i, b), th)) :: rules)
-      (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
+      (nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
   end;
 
 fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
@@ -136,7 +136,7 @@
           k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
       val next = ~ (length rules);
       val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
-          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
+          nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
         (empty_netpairs, next upto ~1 ~~ rules);
     in make_rules (next - 1) rules netpairs wrappers end;
 
diff -r c885c93a9324 -r 685d95c793ff src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Pure/library.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -103,9 +103,10 @@
   val unflat: 'a list list -> 'b list -> 'b list list
   val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
-  val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
+  val nth: 'a list -> int -> 'a 
+  val nth_update: int * 'a -> 'a list -> 'a list
+  val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
   val split_last: 'a list -> 'a list * 'a
-  val nth_update: 'a -> int * 'a list -> 'a list
   val find_index: ('a -> bool) -> 'a list -> int
   val find_index_eq: ''a -> ''a list -> int
   val find_first: ('a -> bool) -> 'a list -> 'a option
@@ -146,7 +147,7 @@
   val oct_char: string -> string
 
   (*strings*)
-  val nth_elem_string: int * string -> string
+  val nth_string: string -> int -> string
   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val forall_string: (string -> bool) -> string -> bool
@@ -263,7 +264,6 @@
   val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
   val take: int * 'a list -> 'a list
   val drop: int * 'a list -> 'a list
-  val nth_elem: int * 'a list -> 'a
   val last_elem: 'a list -> 'a
   val flat: 'a list list -> 'a list
   val seq: ('a -> unit) -> 'a list -> unit
@@ -539,11 +539,17 @@
 
 (*return nth element of a list, where 0 designates the first element;
   raise EXCEPTION if list too short*)
-fun nth_elem (i,xs) = List.nth(xs,i);
+fun nth xs i = List.nth (xs, i);
 
-fun map_nth_elem 0 f (x :: xs) = f x :: xs
-  | map_nth_elem n f (x :: xs) = x :: map_nth_elem (n - 1) f xs
-  | map_nth_elem _ _ [] = raise Subscript;
+(*update nth element*)
+fun nth_update (n, x) xs =
+    (case splitAt (n, xs) of
+      (_, []) => raise Subscript
+    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
+
+fun nth_map 0 f (x :: xs) = f x :: xs
+  | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
+  | nth_map _ _ [] = raise Subscript;
 
 (*last element of a list*)
 val last_elem = List.last;
@@ -553,12 +559,6 @@
   | split_last [x] = ([], x)
   | split_last (x :: xs) = apfst (cons x) (split_last xs);
 
-(*update nth element*)
-fun nth_update x n_xs =
-    (case splitAt n_xs of
-      (_,[]) => raise Subscript
-    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
-
 (*find the position of an element in a list*)
 fun find_index pred =
   let fun find _ [] = ~1
@@ -762,7 +762,7 @@
 
 (* functions tuned for strings, avoiding explode *)
 
-fun nth_elem_string (i, str) =
+fun nth_string str i =
   (case try String.substring (str, i, 1) of
     SOME s => s
   | NONE => raise Subscript);
@@ -1101,7 +1101,7 @@
       | qsort (xs as [_]) = xs
       | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
       | qsort xs =
-          let val (lts, eqs, gts) = part (nth_elem (length xs div 2, xs)) xs
+          let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs
           in qsort lts @ eqs @ qsort gts end
     and part _ [] = ([], [], [])
       | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
@@ -1143,7 +1143,7 @@
   if h < l orelse l < 0 then raise RANDOM
   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
 
-fun one_of xs = nth_elem (random_range 0 (length xs - 1), xs);
+fun one_of xs = nth xs (random_range 0 (length xs - 1));
 
 fun frequency xs =
   let
diff -r c885c93a9324 -r 685d95c793ff src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Oct 28 13:52:57 2005 +0200
+++ b/src/Pure/pattern.ML	Fri Oct 28 16:35:40 2005 +0200
@@ -45,7 +45,7 @@
 fun string_of_term thy env binders t = Sign.string_of_term thy
   (Envir.norm_term env (subst_bounds(map Free binders,t)));
 
-fun bname binders i = fst(List.nth(binders,i));
+fun bname binders i = fst (nth binders i);
 fun bnames binders is = space_implode " " (map (bname binders) is);
 
 fun typ_clash thy (tye,T,U) =
@@ -110,10 +110,8 @@
 fun idx [] j     = raise Unif
   | idx(i::is) j = if (i:int) =j then length is else idx is j;
 
-fun at xs i = List.nth (xs,i);
-
 fun mkabs (binders,is,t)  =
-    let fun mk(i::is) = let val (x,T) = List.nth(binders,i)
+    let fun mk(i::is) = let val (x,T) = nth binders i
                         in Abs(x,T,mk is) end
           | mk []     = t
     in mk is end;
@@ -134,7 +132,7 @@
 
 fun red (Abs(_,_,s)) (i::is) js = red s is (i::js)
   | red t            []      [] = t
-  | red t            is      jn = app (mapbnd (at jn) t,is);
+  | red t            is      jn = app (mapbnd (nth jn) t,is);
 
 
 (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
@@ -144,7 +142,7 @@
 
 fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
   let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
-  in map (at Ts) is ---> U end;
+  in map (nth Ts) is ---> U end;
 
 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));