cleaned up nth, nth_update, nth_map and nth_string functions
authorhaftmann
Fri Oct 28 16:35:40 2005 +0200 (2005-10-28)
changeset 18011685d95c793ff
parent 18010 c885c93a9324
child 18012 23e6cfda8c4b
cleaned up nth, nth_update, nth_map and nth_string functions
src/HOL/Tools/record_package.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/eqsubst.ML
src/Pure/General/name_space.ML
src/Pure/Isar/context_rules.ML
src/Pure/library.ML
src/Pure/pattern.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Fri Oct 28 13:52:57 2005 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Fri Oct 28 16:35:40 2005 +0200
     1.3 @@ -1125,7 +1125,7 @@
     1.4            (s = "all" orelse s = "All" orelse s = "Ex") andalso is_recT T
     1.5          | _ => false);
     1.6  
     1.7 -    val goal = List.nth (Thm.prems_of st, i - 1);
     1.8 +    val goal = nth (Thm.prems_of st) (i - 1);
     1.9      val frees = List.filter (is_recT o type_of) (term_frees goal);
    1.10  
    1.11      fun mk_split_free_tac free induct_thm i =
    1.12 @@ -1172,7 +1172,7 @@
    1.13            (s = "all" orelse s = "All") andalso is_recT T
    1.14          | _ => false);
    1.15  
    1.16 -    val goal = List.nth (Thm.prems_of st, i - 1);
    1.17 +    val goal = nth (Thm.prems_of st) (i - 1);
    1.18  
    1.19      fun is_all t =
    1.20        (case t of (Const (quantifier, _)$_) =>
    1.21 @@ -1231,7 +1231,7 @@
    1.22  fun try_param_tac s rule i st =
    1.23    let
    1.24      val cert = cterm_of (Thm.theory_of_thm st);
    1.25 -    val g = List.nth (prems_of st, i - 1);
    1.26 +    val g = nth (prems_of st) (i - 1);
    1.27      val params = Logic.strip_params g;
    1.28      val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
    1.29      val rule' = Thm.lift_rule (st, i) rule;
    1.30 @@ -1258,7 +1258,7 @@
    1.31  fun ex_inst_tac i st =
    1.32    let
    1.33      val sg = sign_of_thm st;
    1.34 -    val g = List.nth (prems_of st, i - 1);
    1.35 +    val g = nth (prems_of st) (i - 1);
    1.36      val params = Logic.strip_params g;
    1.37      val exI' = Thm.lift_rule (st, i) exI;
    1.38      val (_$(_$x)) = Logic.strip_assums_concl (hd (prems_of exI'));
    1.39 @@ -1391,7 +1391,7 @@
    1.40      (*updates*)
    1.41      fun mk_upd_prop (i,(c,T)) =
    1.42        let val x' = Free (variant variants (base c ^ "'"),T)
    1.43 -          val args' = nth_update x' (i, vars_more)
    1.44 +          val args' = nth_update (i, x') vars_more
    1.45        in mk_upd updN c x' ext === mk_ext args'  end;
    1.46      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
    1.47  
    1.48 @@ -1770,7 +1770,7 @@
    1.49      (*updates*)
    1.50      fun mk_upd_prop (i,(c,T)) =
    1.51        let val x' = Free (variant all_variants (base c ^ "'"),T)
    1.52 -          val args' = nth_update x' (parent_fields_len + i, all_vars_more)
    1.53 +          val args' = nth_update (parent_fields_len + i, x') all_vars_more
    1.54        in mk_upd updateN c x' r_rec0 === mk_rec args' 0  end;
    1.55      val upd_conv_props = ListPair.map mk_upd_prop (idxms, fields_more);
    1.56  
     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Fri Oct 28 13:52:57 2005 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Fri Oct 28 16:35:40 2005 +0200
     2.3 @@ -212,13 +212,13 @@
     2.4        val (ge,le) = List.partition (fn (_,_,cs) => el v cs > 0) ineqs
     2.5        val lb = ratrelmax(map (eval ex v) ge)
     2.6        val ub = ratrelmin(map (eval ex v) le)
     2.7 -  in nth_update (choose2 (List.nth(discr,v)) (lb,ub)) (v,ex) end;
     2.8 +  in nth_update (v, choose2 (nth discr v) (lb, ub)) ex end;
     2.9  
    2.10  fun findex discr = Library.foldl (findex1 discr);
    2.11  
    2.12  fun elim1 v x =
    2.13    map (fn (a,le,bs) => (Rat.add(a,Rat.neg(Rat.mult(el v bs,x))), le,
    2.14 -                        nth_update Rat.zero (v,bs)));
    2.15 +                        nth_update (v, Rat.zero) bs));
    2.16  
    2.17  fun single_var v (_,_,cs) = (filter_out (equal Rat.zero) cs = [el v cs]);
    2.18  
    2.19 @@ -229,7 +229,7 @@
    2.20    in case nz of [] => ex
    2.21       | (_,_,cs) :: _ =>
    2.22         let val v = find_index (not o equal Rat.zero) cs
    2.23 -           val d = List.nth(discr,v)
    2.24 +           val d = nth discr v
    2.25             val pos = Rat.ge0(el v cs)
    2.26             val sv = List.filter (single_var v) nz
    2.27             val minmax =
    2.28 @@ -240,7 +240,7 @@
    2.29             val bnds = map (fn (a,le,bs) => (Rat.mult(a,Rat.inv(el v bs)),le)) sv
    2.30             val x = minmax((Rat.zero,if pos then true else false)::bnds)
    2.31             val ineqs' = elim1 v x nz
    2.32 -           val ex' = nth_update x (v,ex)
    2.33 +           val ex' = nth_update (v, x) ex
    2.34         in pick_vars discr (ineqs',ex') end
    2.35    end;
    2.36  
    2.37 @@ -460,8 +460,8 @@
    2.38          let val thm' = trace_thm "Simplified:" (full_simplify simpset' thm)
    2.39          in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end
    2.40  
    2.41 -      fun mk(Asm i) = trace_thm "Asm" (List.nth(asms,i))
    2.42 -        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (List.nth(atoms,i)))
    2.43 +      fun mk(Asm i) = trace_thm "Asm" (nth asms i)
    2.44 +        | mk(Nat i) = (trace_msg "Nat"; LA_Logic.mk_nat_thm sg (nth atoms i))
    2.45          | mk(LessD(j)) = trace_thm "L" (hd([mk j] RL lessD))
    2.46          | mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD)
    2.47          | mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL lessD))
     3.1 --- a/src/Provers/eqsubst.ML	Fri Oct 28 13:52:57 2005 +0200
     3.2 +++ b/src/Provers/eqsubst.ML	Fri Oct 28 16:35:40 2005 +0200
     3.3 @@ -363,7 +363,7 @@
     3.4        val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
     3.5        val cfvs = rev (map ctermify fvs);
     3.6  
     3.7 -      val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
     3.8 +      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
     3.9        val asm_nprems = length (Logic.strip_imp_prems asmt);
    3.10  
    3.11        val pth = trivify asmt;
     4.1 --- a/src/Pure/General/name_space.ML	Fri Oct 28 13:52:57 2005 +0200
     4.2 +++ b/src/Pure/General/name_space.ML	Fri Oct 28 16:35:40 2005 +0200
     4.3 @@ -89,7 +89,7 @@
     4.4  fun map_base _ "" = ""
     4.5    | map_base f name =
     4.6        let val names = unpack name
     4.7 -      in pack (map_nth_elem (length names - 1) f names) end;
     4.8 +      in pack (nth_map (length names - 1) f names) end;
     4.9  
    4.10  fun suffixes_prefixes xs =
    4.11    let
     5.1 --- a/src/Pure/Isar/context_rules.ML	Fri Oct 28 13:52:57 2005 +0200
     5.2 +++ b/src/Pure/Isar/context_rules.ML	Fri Oct 28 16:35:40 2005 +0200
     5.3 @@ -96,7 +96,7 @@
     5.4  fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) =
     5.5    let val w = (case opt_w of SOME w => w | NONE => Tactic.subgoals_of_brl (b, th)) in
     5.6      make_rules (next - 1) ((w, ((i, b), th)) :: rules)
     5.7 -      (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     5.8 +      (nth_map i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers
     5.9    end;
    5.10  
    5.11  fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) =
    5.12 @@ -136,7 +136,7 @@
    5.13            k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
    5.14        val next = ~ (length rules);
    5.15        val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
    5.16 -          map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps)
    5.17 +          nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
    5.18          (empty_netpairs, next upto ~1 ~~ rules);
    5.19      in make_rules (next - 1) rules netpairs wrappers end;
    5.20  
     6.1 --- a/src/Pure/library.ML	Fri Oct 28 13:52:57 2005 +0200
     6.2 +++ b/src/Pure/library.ML	Fri Oct 28 16:35:40 2005 +0200
     6.3 @@ -103,9 +103,10 @@
     6.4    val unflat: 'a list list -> 'b list -> 'b list list
     6.5    val splitAt: int * 'a list -> 'a list * 'a list
     6.6    val dropwhile: ('a -> bool) -> 'a list -> 'a list
     6.7 -  val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list
     6.8 +  val nth: 'a list -> int -> 'a 
     6.9 +  val nth_update: int * 'a -> 'a list -> 'a list
    6.10 +  val nth_map: int -> ('a -> 'a) -> 'a list -> 'a list
    6.11    val split_last: 'a list -> 'a list * 'a
    6.12 -  val nth_update: 'a -> int * 'a list -> 'a list
    6.13    val find_index: ('a -> bool) -> 'a list -> int
    6.14    val find_index_eq: ''a -> ''a list -> int
    6.15    val find_first: ('a -> bool) -> 'a list -> 'a option
    6.16 @@ -146,7 +147,7 @@
    6.17    val oct_char: string -> string
    6.18  
    6.19    (*strings*)
    6.20 -  val nth_elem_string: int * string -> string
    6.21 +  val nth_string: string -> int -> string
    6.22    val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
    6.23    val exists_string: (string -> bool) -> string -> bool
    6.24    val forall_string: (string -> bool) -> string -> bool
    6.25 @@ -263,7 +264,6 @@
    6.26    val foldr: ('a * 'b -> 'b) -> 'a list * 'b -> 'b
    6.27    val take: int * 'a list -> 'a list
    6.28    val drop: int * 'a list -> 'a list
    6.29 -  val nth_elem: int * 'a list -> 'a
    6.30    val last_elem: 'a list -> 'a
    6.31    val flat: 'a list list -> 'a list
    6.32    val seq: ('a -> unit) -> 'a list -> unit
    6.33 @@ -539,11 +539,17 @@
    6.34  
    6.35  (*return nth element of a list, where 0 designates the first element;
    6.36    raise EXCEPTION if list too short*)
    6.37 -fun nth_elem (i,xs) = List.nth(xs,i);
    6.38 +fun nth xs i = List.nth (xs, i);
    6.39  
    6.40 -fun map_nth_elem 0 f (x :: xs) = f x :: xs
    6.41 -  | map_nth_elem n f (x :: xs) = x :: map_nth_elem (n - 1) f xs
    6.42 -  | map_nth_elem _ _ [] = raise Subscript;
    6.43 +(*update nth element*)
    6.44 +fun nth_update (n, x) xs =
    6.45 +    (case splitAt (n, xs) of
    6.46 +      (_, []) => raise Subscript
    6.47 +    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
    6.48 +
    6.49 +fun nth_map 0 f (x :: xs) = f x :: xs
    6.50 +  | nth_map n f (x :: xs) = x :: nth_map (n - 1) f xs
    6.51 +  | nth_map _ _ [] = raise Subscript;
    6.52  
    6.53  (*last element of a list*)
    6.54  val last_elem = List.last;
    6.55 @@ -553,12 +559,6 @@
    6.56    | split_last [x] = ([], x)
    6.57    | split_last (x :: xs) = apfst (cons x) (split_last xs);
    6.58  
    6.59 -(*update nth element*)
    6.60 -fun nth_update x n_xs =
    6.61 -    (case splitAt n_xs of
    6.62 -      (_,[]) => raise Subscript
    6.63 -    | (prfx, _ :: sffx') => prfx @ (x :: sffx'))
    6.64 -
    6.65  (*find the position of an element in a list*)
    6.66  fun find_index pred =
    6.67    let fun find _ [] = ~1
    6.68 @@ -762,7 +762,7 @@
    6.69  
    6.70  (* functions tuned for strings, avoiding explode *)
    6.71  
    6.72 -fun nth_elem_string (i, str) =
    6.73 +fun nth_string str i =
    6.74    (case try String.substring (str, i, 1) of
    6.75      SOME s => s
    6.76    | NONE => raise Subscript);
    6.77 @@ -1101,7 +1101,7 @@
    6.78        | qsort (xs as [_]) = xs
    6.79        | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
    6.80        | qsort xs =
    6.81 -          let val (lts, eqs, gts) = part (nth_elem (length xs div 2, xs)) xs
    6.82 +          let val (lts, eqs, gts) = part (nth xs (length xs div 2)) xs
    6.83            in qsort lts @ eqs @ qsort gts end
    6.84      and part _ [] = ([], [], [])
    6.85        | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
    6.86 @@ -1143,7 +1143,7 @@
    6.87    if h < l orelse l < 0 then raise RANDOM
    6.88    else l + Real.floor (rmod (random ()) (real (h - l + 1)));
    6.89  
    6.90 -fun one_of xs = nth_elem (random_range 0 (length xs - 1), xs);
    6.91 +fun one_of xs = nth xs (random_range 0 (length xs - 1));
    6.92  
    6.93  fun frequency xs =
    6.94    let
     7.1 --- a/src/Pure/pattern.ML	Fri Oct 28 13:52:57 2005 +0200
     7.2 +++ b/src/Pure/pattern.ML	Fri Oct 28 16:35:40 2005 +0200
     7.3 @@ -45,7 +45,7 @@
     7.4  fun string_of_term thy env binders t = Sign.string_of_term thy
     7.5    (Envir.norm_term env (subst_bounds(map Free binders,t)));
     7.6  
     7.7 -fun bname binders i = fst(List.nth(binders,i));
     7.8 +fun bname binders i = fst (nth binders i);
     7.9  fun bnames binders is = space_implode " " (map (bname binders) is);
    7.10  
    7.11  fun typ_clash thy (tye,T,U) =
    7.12 @@ -110,10 +110,8 @@
    7.13  fun idx [] j     = raise Unif
    7.14    | idx(i::is) j = if (i:int) =j then length is else idx is j;
    7.15  
    7.16 -fun at xs i = List.nth (xs,i);
    7.17 -
    7.18  fun mkabs (binders,is,t)  =
    7.19 -    let fun mk(i::is) = let val (x,T) = List.nth(binders,i)
    7.20 +    let fun mk(i::is) = let val (x,T) = nth binders i
    7.21                          in Abs(x,T,mk is) end
    7.22            | mk []     = t
    7.23      in mk is end;
    7.24 @@ -134,7 +132,7 @@
    7.25  
    7.26  fun red (Abs(_,_,s)) (i::is) js = red s is (i::js)
    7.27    | red t            []      [] = t
    7.28 -  | red t            is      jn = app (mapbnd (at jn) t,is);
    7.29 +  | red t            is      jn = app (mapbnd (nth jn) t,is);
    7.30  
    7.31  
    7.32  (* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
    7.33 @@ -144,7 +142,7 @@
    7.34  
    7.35  fun type_of_G (env as Envir.Envir {iTs, ...}) (T,n,is) =
    7.36    let val (Ts, U) = split_type (Envir.norm_type iTs T, n, [])
    7.37 -  in map (at Ts) is ---> U end;
    7.38 +  in map (nth Ts) is ---> U end;
    7.39  
    7.40  fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
    7.41